Slight overall improvements to the QuickCheck module:

  - Fixed bug that caused some QuickCheck tests to throw an exception because not a complete substitution was taking place.
  - Uncommented the legendary 16th bug that causes an endless loop when Z3 is used. It doesn’t cause an endless loop with QuickCheck, but QuickCheck does give the wrong answer :’(.

All in all, the very naive testing module correctly tests 13/16 tests at the moment (most of the time at least; it’s random).

src/LogicIR/Backend/QuickCheck.hs

@@ -48,8 +48,13 @@ checkRepeatedly n e1 e2 = do
 check :: LExpr -> LExpr -> IO (Bool, Model)
 check e1 e2 = do
     (result1, model) <- checkLExpr e1
-    let result2       = eval $ applyModel model $ replaceQuantifiers e2
-    return (result1 == result2, model)
+    let primFreeE     = applyModel model $ replaceQuantifiers e2
+    let finalE        = repeatedApplyModel (primFreeE, model)
+    if evalPossible finalE then do
+        let result2 = eval finalE
+        return (result1 == result2, model)
+    else
+        return (False, model)
 
 -- Given an LExpr, generates a substitution model for all variables in it,
 -- and returns whether the formula evaluates to true or to false when that model
@@ -59,7 +64,7 @@ checkLExpr :: LExpr -> IO (LConst, Model)
 checkLExpr e = do 
     primitivesModel      <- generateModel $ primitives
     let primFreeE         = applyModel primitivesModel quantFreeE
-    (finalE, arrayModel) <- repeatedApplyModel (primFreeE, empty)
+    (finalE, arrayModel) <- repeatedApplyAndExpandModel (primFreeE, empty)
     let model             = arrayModel ++ primitivesModel
     let result            = eval finalE
     return $ (result, model)
@@ -71,14 +76,15 @@ checkLExpr e = do
 
 -- applies substitution of arrays until a "pure" LExpr is the result, or no
 -- more substitutions can be applied. If the latter is the case, an error
--- will be thrown.
-repeatedApplyModel :: (LExpr, Model) -> IO (LExpr, Model)
-repeatedApplyModel (e, m) = do
+-- will be thrown. ***NOTE***: this function actually expands the model if
+-- necessary. If you don't want this, use repeatedApplyModel
+repeatedApplyAndExpandModel :: (LExpr, Model) -> IO (LExpr, Model)
+repeatedApplyAndExpandModel (e, m) = do
     if length arrays > 0 then
         if length substitutableArrays > 0 then do
             model   <- generateModel substitutableArrays
             let newE = applyModel model e
-            repeatedApplyModel (newE, m ++ model)
+            repeatedApplyAndExpandModel (newE, m ++ model)
         else
             error $ "There are unsubstitutable array accesses: " ++ (show arrays)
     else
@@ -89,6 +95,13 @@ repeatedApplyModel (e, m) = do
           -- i doesn't contain variables.
           sSubstitutable (LArray var e) = evalPossible e
 
+repeatedApplyModel :: (LExpr, Model) -> LExpr
+repeatedApplyModel (e, m) = if newE /= e then
+                                repeatedApplyModel (newE, m)
+                            else
+                                e
+    where newE = applyModel m e
+
 -- Applies substitution given a Model and an LExpr.
 applyModel :: Model -> LExpr -> LExpr
 applyModel model = foldLExpr algebra

src/SimpleFormulaChecker.hs

@@ -235,13 +235,15 @@ methodDefToLExpr m1@(decls1, _, env1) m2@(decls2, _, env2) name = do
     (lExpr1, lExpr2)
     where extractCond m n = extractExpr $ getMethodCalls m n
 
-testSpec :: (FilePath, String) -> (FilePath, String) -> IO Bool
-testSpec method1@(_, name1) method2@(_, name2) = do
+testSpec :: (FilePath, String) -> (FilePath, String) -> Int -> IO Bool
+testSpec method1@(_, name1) method2@(_, name2) n = do
     (m1, m2) <- parse method1 method2
     putStrLn $ "----PRE---- (" ++ name1 ++ " vs " ++ name2 ++ ")"
     let (lExpr1, lExpr2) = methodDefToLExpr m1 m2 "pre"
-    preAns <- testEquality 10000 lExpr1 lExpr2
+    preAns <- testEquality n lExpr1 lExpr2
     putStrLn "\n----POST---"
     let (lExpr1, lExpr2) = methodDefToLExpr m1 m2 "post"
-    postAns <- testEquality 10000 lExpr1 lExpr2
+    postAns <- testEquality n lExpr1 lExpr2
     return $ preAns && postAns
+
+res = testSpec ("examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java", "swap_spec1") ("examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java", "swap_spec2")

test/TIRQuickCheck.hs

@@ -10,7 +10,7 @@ edslSrc = "examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
 
 testEquiv :: Bool -> String -> String -> Assertion
 testEquiv b s s' =
-  unsafePerformIO (silence $ testSpec (edslSrc, s) (edslSrc, s')) @?= b
+  unsafePerformIO (silence $ testSpec (edslSrc, s) (edslSrc, s') 100000) @?= b
 (.==) = testEquiv True
 (.!=) = testEquiv False
 
@@ -30,5 +30,5 @@ quickCheckTests =
   , "sorted1".!= "sorted3"
   , "test2" .!= "sorted3"
   , "sorted3" .!= "sorted4"
-  -- , equivalent "sorted1" "sorted4" -- does not terminate (TODO: should time out, but this does not work)
+  , "sorted1" .== "sorted4"
   ]