Z3: timeout fix + Tests: Arrays

examples/test_equiv/Arrays.java

+package nl.uu;
+import static nl.uu.impress.EDSL.*;
+
+public class Arrays {
+
+    // // 1) Simple array arithmetic
+    // public static void swap1_1(int[] a, int i, int j) {
+    //     pre(i >= 0 && j >= 0);
+    //     swap(a, i, j);
+    //     post(a[j] == oldai && a[i] == oldaj);
+    // }
+    // public static void swap2_1(int[] a, int i, int j) {
+    //     pre(i >= 0);
+    //     pre(j > 0 || (i + 1) * j >= 0);
+    //     swap(a, i, j);
+    //     post(a[i] == oldaj);
+    //     post(a[j] == oldai);
+    // }
+    //
+    // // 2) Quantifying over array (max)
+    // public static void max1_2(int[] a) {
+    //     pre(a != null && a.length > 0);
+    //     int retval = getMax(a);
+    //     post(exists(a, i -> a[i] == retval));
+    //     post(forall(a, i -> a[i] <= retval));
+    // }
+    // public static void max2_2(int[] a) {
+    //     pre(a != null && a.length >= 1);
+    //     int retval = getMax(a);
+    //     post(exists(a, i -> retval * 2 == a[i] + a[i]));
+    //     post(!exists(a, i -> a[i] > retval));
+    // }
+
+    // 3) Quantifying over array (sort)
+    public static void sort1_3(int[] a) {
+        pre(a != null && a.length >= 0);
+        int[] sa = a.sort();
+        post(forall(a, i ->
+                forallr(a,  i + 1, a.length, j -> a[i] <= a[j])));
+    }
+    // public static void sort2_3(int[] a) {
+    //     pre(a != null && a.length > -1);
+    //     int[] sa = a.sort();
+    //     post(forall(a, i ->
+    //             !existsr(a, i + 1, a.length, j -> a[i] > a[j])));
+    // }
+
+    // 4) Quantifying over array (unique sort)
+    public static void sort1_4(int[] a) {
+        pre(a != null && a.length > 1);
+        pre(forall(a, i ->
+              forall(a, j -> i == j || a[i] != a[j])));
+        int[] sa = a.sort();
+        post(a.length > 1);
+        post(forallr(a, 0, a.length - 1, i -> a[i] < a[i + 1]));
+    }
+    // public static void sort2_4(int[] a) {
+    //     pre(a != null);
+    //     pre(a.length >= 2);
+    //     pre(forall(a, i ->
+    //           forall(a, j -> i == j || a[i] != a[j])));
+    //           // forallr(a, i + 1, a.length, j -> a[i] != a[j])));
+    //     // pre(forallr(a, a.length, 0, i ->
+    //     //       forallr(a, 0, i, j -> a[j] != a[i])));
+    //     int[] sa = a.sort();
+    //     // post(forall(a, i ->
+    //     //         forallr(a, i + 1, a.length, j -> a[i] < a[j])));
+    //     post(a.length >= 2);
+    //     post(forallr(a, 1, a.length, i -> a[i] > a[i - 1]));
+    // }
+}

examples/test_equiv/Doubles.java → examples/test_equiv/Reals.java

 package nl.uu;
 import static nl.uu.impress.EDSL.*;
 
-public class Doubles {
+public class Reals {
 
     // 1) Simple real arithmetic
     public static float real1_1(float a) {
@@ -9,13 +9,11 @@ public class Doubles {
         a += a;
         post(a >= (4 - 3 + 3));
     }
-
     public static float real2_1(float a) {
         pre(a > 2 || a == 2);
         a = a * 2;
         post(a > 4 || a == 4);
     }
-
     public static float real3_1(float a) {
         pre(a > 1);
         pre(a > 2 || a == 2);
@@ -32,7 +30,6 @@ public class Doubles {
         c = a / b;
         post(c == 1.0 || c == 7.0);
     }
-
     public static float real2_2(float a, double b) {
         pre(a % b == 0 || false);
         pre(a == 3 * 10 - 23 && true);
@@ -46,7 +43,6 @@ public class Doubles {
         b += 1;
         post(a < b - .7);
     }
-
     public static float real2_3(float a, int b) {
         pre(a > b);
         pre(a - (10 * .3 / 10) < b);

src/SimpleFormulaChecker.hs

@@ -26,6 +26,7 @@ import ModelParser.Parser
 
 import Control.Monad (when)
 import Control.Monad.Trans (liftIO)
+import Control.Exception.Base (catch)
 import Data.Int
 import Data.List
 import qualified Data.Map as M
@@ -87,23 +88,26 @@ getMethodCalls (_, StmtBlock (Block bs), _) name = mapMaybe extractMethodInv bs
 extractExpr :: [MethodInvocation] -> Exp
 extractExpr call = combineExprs $ map (\(MethodCall (Name [Ident _]) [a]) -> a) call
     where combineExprs :: [Exp] -> Exp
-          combineExprs [] = true
+          combineExprs []     = true
           combineExprs [e]    = e
           combineExprs (e:es) = e &* combineExprs es
 
+
+-- | Z3 try evaluation with timeout.
+tryZ3 = evalZ3With Nothing (Z3.Opts.opt "timeout" "3000")
+
 -- Check if two Z3 AST's are equivalent
 isEquivalent :: Z3 AST -> Z3 AST -> IO (Result, Maybe Model)
-isEquivalent ast1' ast2' = evalZ3 z3
-    where
-    z3 = do
-         ast1 <- ast1'
-         ast2 <- ast2'
-         astEq <- mkEq ast1 ast2
-         astNeq <- mkNot astEq -- negate the question to get a model
-         assert astNeq
-         r <- solverCheckAndGetModel -- check in documentatie
-         solverReset
-         return r
+isEquivalent ast1' ast2' =
+  tryZ3 $ do
+    ast1 <- ast1'
+    ast2 <- ast2'
+    astEq <- mkEq ast1 ast2
+    astNeq <- mkNot astEq -- negate the question to get a model
+    assert astNeq
+    r <- solverCheckAndGetModel -- check in documentatie
+    solverReset
+    return r
 
 -- Function that shows a human-readable model and also highlights potential inconsistencies.
 -- Sorry for the code, it is quite awful...
@@ -200,7 +204,10 @@ determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do
     putStrLn "Z3 Result:"
     -- Check if the formula is satisfiable. If it is, print the instantiation of its free
     -- variables that would make it true:
-    (result, model) <- isEquivalent ast1 ast2
+    (result, model) <- isEquivalent ast1 ast2 `catch` (\err -> do
+                                putStrLn $ "ERROR: " ++ show (err :: Z3Error)
+                                return (Undef, Nothing)
+                                )
     case result of
        Unsat -> do
          putStrLn "formulas are equivalent!"
@@ -211,7 +218,7 @@ determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do
        Sat   -> do
                 putStrLn "formulas are NOT equivalent, model:"
                 case model of
-                  Just m -> do s <- evalZ3With Nothing (Z3.Opts.opt "timeout" (1000 :: Int)) (modelToString m) -- TODO: the option is set, but does not actually work :(
+                  Just m -> do s <- tryZ3 (modelToString m)
                                putStrLn s
                                -- showRelevantModel $ parseModel s
                                return False
@@ -220,7 +227,7 @@ determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do
         extractCond :: MethodDef -> String -> Exp
         extractCond m n = extractExpr (getMethodCalls m n)
         showZ3AST :: Z3 AST -> IO String
-        showZ3AST ast' = evalZ3 $ ast' >>= astToString
+        showZ3AST ast' = tryZ3 $ ast' >>= astToString
 
 -- Function that compares both the pre and the post condition for two methods.
 -- It is assumed that both methods have the same environment (parameter names, class member names, etc).

test/TEquivalenceClasses.hs

@@ -9,15 +9,13 @@ import Test.HUnit
 
 import SimpleFormulaChecker (compareSpec, parseMethodIds)
 
-edslSrc = "examples/test_equiv/Doubles.java"
-
-testEquiv :: Bool -> String -> String -> Assertion
-testEquiv b s s' =
-  unsafePerformIO (silence $ compareSpec (edslSrc, s) (edslSrc, s')) @?= b
+testEquiv :: Bool -> String -> String -> String -> Assertion
+testEquiv b src s s' =
+  unsafePerformIO (id $ compareSpec (src, s) (src, s')) @?= b
 (.==) = testEquiv True
 (.!=) = testEquiv False
 
-equivClassesTests =
+genEquivTests edslSrc =
   let methodIds = unsafePerformIO (silence $ parseMethodIds edslSrc)
       getClass = last . splitOn "_"
       tailFrom :: Eq a => [a] -> a -> [a]
@@ -30,5 +28,5 @@ equivClassesTests =
                         let eq = getClass a == getClass b
                         putStrLn $ foldl1 (++)
                           ["  (", a, if eq then " == " else " != ", b, ")"]
-                        return $ if eq then (.==) else (.!=)
+                        return $ (if eq then (.==) else (.!=)) edslSrc
                 ]

test/TExamples.hs

@@ -14,8 +14,7 @@ testEquiv b s s' =
 (.!=) = testEquiv False
 
 equivalenceTests =
-  [ "real1" .== "real2"
-  , "swap_spec1" .== "swap_spec1"
+  [ "swap_spec1" .== "swap_spec1"
   , "swap_spec1" .!= "swap_spec2"
   , "getMax_spec1" .!= "getMax_spec2"
   , "test1" .!= "test2"

test/TIRParser.hs

@@ -27,6 +27,8 @@ parserTests =
       LLen xArr .== n 0 .&& lnot (LIsnull xArr)
   , "len(x:[real]) == 0 /\\ ! x:[real] == null" @?=
       LLen xArr' .== n 0 .&& lnot (LIsnull xArr')
+  , "len(x:[[real]]) == 0 /\\ ! x:[[real]] == null" @?=
+      LLen xArr'' .== n 0 .&& lnot (LIsnull xArr'')
   ]
   where x = var "x" "int"
         x' = v x