EDSL: Implication + Variable introduction

impress_edsl/src/nl/uu/impress/Main.java

@@ -12,37 +12,37 @@ public class Main {
 
     public static void empty2() {}
 
-    public static void quickcheck_test1(int[] b) {
+    public static void quickcheck_test1(int[] b, int a, int c) {
         pre(~(-a * c) == (79 & 41));
         pre(a > 0);
         pre(forall(b, i -> b[i] > -10));
     }
 
-    public static void quickcheck_test2(int[] b) {
+    public static void quickcheck_test2(int[] b, int a, int c) {
         pre(~(-a * c) == (79 & 41));
         pre(a > 0);
         pre(forall(b, i -> b[i] >= -10)); // note the >=, whereas quickcheck_test1 has >.
     }
 
-    public static int simple_eval1() {
+    public static void simple_eval1() {
         pre(~(-5 * 2) == (79 & 41)); // evaluates to 9 == 9
     }
 
-    public static int simple_eval2() {
+    public static void simple_eval2() {
         pre(~(-5 * 2) == (79 & 40)); // evaluates to 9 == 8
     }
 
-    public static int simple_eval3(int a) {
+    public static void simple_eval3(int a) {
         pre(~(a * 2) == (79 & 40)); // can't evaluate due to undefined variable
     }
 
-    public static float real1(float a) {
+    public static void real1(float a) {
         pre(a >= (2 - 1 + 1));
         a += a;
         post(a >= (4 - 3 + 3));
     }
 
-    public static float real2(float a) {
+    public static void real2(float a) {
         pre(a > 2 || a == 2);
         a = a * 2;
         post(a > 4 || a == 4);
@@ -206,7 +206,7 @@ public class Main {
     }
 
     public static void arr1(double[] a) {
-        pre(a.length == 2 && forall(a, i -> forallr(a, i, a.length, j -> a[i] <= a[j])));
+        pre((a.length == 2) && forall(a, i -> forallr(a, i, a.length, j -> a[i] <= a[j])));
         post(true);
     }
 
@@ -216,4 +216,23 @@ public class Main {
         pre(a.length == 2 && forall(a, i -> forallr(a, i+1, a.length, j -> a[i] < (a[j] + 1))));
         post(true);
     }
+
+    public static void imp1(int[] b) {
+      pre(b.length == 5);
+      post(forall(b, i -> imp(i > 2, b[i] > 0)));
+    }
+    public static void imp2(int[] b) {
+      pre(b.length == 5);
+      post(forall(b, i -> imp(i > 3, b[i] > 0)));
+    }
+
+    public static void varIntro1(int[] b) {
+      pre(b.length == 5);
+      post(forall(b, i -> imp(i > 2, with(b[i], x -> x > 0))));
+    }
+    public static void varIntro2(int[] b) {
+      pre(b.length == 5);
+      post(forall(b, i -> imp(i > 3, with(b[i], x -> x > 0))));
+    }
+
 }

impress_edsl/src/nl/uu/impress/specchecker/EDSL.java

@@ -5,17 +5,18 @@ public class EDSL {
         boolean invoke(int i);
     }
 
-    public interface IntPred2 {
-        boolean invoke(int i, int j);
+    public interface Pred<A> {
+        boolean invoke(A i);
     }
-    
+
+//    public interface IntPred2 {
+//        boolean invoke(int i, int j);
+//    }
+
     private static boolean g_forall(int aLength, int rBegin, int rEnd, IntPred pred) {
         for (int index = rBegin; index < rEnd; index++) {
-            //TODO: determine if pred should be called with indices outside of the array range
-            //NOTE: only relevant for the runtime implementation
             if (index < 0 || index >= aLength)
-            	throw new ArrayIndexOutOfBoundsException("index=" + index + ", array length=" + aLength) ;
-                // continue; //assert false;
+            	throw new ArrayIndexOutOfBoundsException("index=" + index + ", array length=" + aLength);
             if (!pred.invoke(index))
                 return false;
         }
@@ -24,17 +25,18 @@ public class EDSL {
 
     private static boolean g_exists(int aLength, int rBegin, int rEnd, IntPred pred) {
         for (int index = rBegin; index < rEnd; index++) {
-            //TODO: determine if pred should be called with indices outside of the array range
-            //NOTE: only relevant for the runtime implementation
             if (index < 0 || index >= aLength)
-            	throw new ArrayIndexOutOfBoundsException("index=" + index + ", array length=" + aLength) ;
-                //continue; //assert false;
+            	throw new ArrayIndexOutOfBoundsException("index=" + index + ", array length=" + aLength);
             if (pred.invoke(index))
                 return true;
         }
         return false;
     }
 
+    public static <A> boolean with(A a, Pred<A> pred) {
+      return pred.invoke(a);
+    }
+
     public static boolean imp(boolean p, boolean q) {
     	return !p || q;
     }
@@ -45,7 +47,11 @@ public class EDSL {
     public static boolean forall(int[] array, IntPred pred) {
         return g_forall(array.length, 0, array.length, pred);
     }
-    
+
+    public static boolean forall(double[] array, IntPred pred) {
+        return g_forall(array.length, 0, array.length, pred);
+    }
+
     //public static boolean forall(int[][] array, IntPred2 pred) {
     //    return g_forall(array.length, 0, array.length, pred);
     //}
@@ -58,6 +64,10 @@ public class EDSL {
         return g_forall(array.length, rBegin, rEnd, pred);
     }
 
+    public static boolean forallr(double[] array, int rBegin, int rEnd, IntPred pred) {
+        return g_forall(array.length, rBegin, rEnd, pred);
+    }
+
     public static boolean exists(Object[] array, IntPred pred) {
         return g_exists(array.length, 0, array.length, pred);
     }
@@ -66,6 +76,10 @@ public class EDSL {
         return g_exists(array.length, 0, array.length, pred);
     }
 
+    public static boolean exists(double[] array, IntPred pred) {
+        return g_exists(array.length, 0, array.length, pred);
+    }
+
     public static boolean existsr(Object[] array, int rBegin, int rEnd, IntPred pred) {
         return g_exists(array.length, rBegin, rEnd, pred);
     }
@@ -74,14 +88,22 @@ public class EDSL {
         return g_exists(array.length, rBegin, rEnd, pred);
     }
 
+    public static boolean existsr(double[] array, int rBegin, int rEnd, IntPred pred) {
+        return g_exists(array.length, rBegin, rEnd, pred);
+    }
+
     public static class PreConditionError extends AssertionError { }
     public static class PostConditionError extends AssertionError { }
-    
+
+    public static void pre() {}
+
     public static void pre(boolean pre) {
         if(!pre) throw new PreConditionError() ;
     }
 
+    public static void post() {}
+
     public static void post(boolean post) {
         if (!post) throw new PostConditionError() ;
     }
-}
+}
\ No newline at end of file

src/API.hs

@@ -19,8 +19,8 @@ import qualified LogicIR.Backend.Z3.API         as Z3
 import           LogicIR.Expr
 import           LogicIR.Frontend.Java          (javaExpToLExpr)
 import           LogicIR.Preprocess             (preprocess)
-import           LogicIR.TypeChecker            (typeCheck)
 import           LogicIR.Pretty
+import           LogicIR.TypeChecker            (typeCheck)
 import           Model
 
 import Control.DeepSeq
@@ -80,13 +80,22 @@ compareSpec m pMode methodA methodB = do
           mapM_ compareSpecHelper [ (mv1, "Z3",   Z3.equivalentTo)
                                   , (mv2, "Test", Test.equivalentTo)
                                   ]
-          waitForResult m mv1 mv2
+          resp <- waitForResult m mv1 mv2
+          let ((_, _, tenvA), (_, _, tenvB)) = (mA, mB)
+          let minResp = minifyResponse (tenvA ++ tenvB) resp
+          log $ "FinalResponse: " ++ show minResp
+          return minResp
           where -- | Runs f on a separate thread and stores the result in mv.
                 compareSpecHelper :: (MVar Response, String, EquivImpl) -> IO ThreadId
                 compareSpecHelper (mv, name, impl) = forkIO $ do
                   resp <- checkEquiv name impl (preL, preL') (postL, postL')
                   resp `seq` putMVar mv resp
 
+-- Exclude internal variables in Response's model.
+minifyResponse :: TypeEnv -> Response -> Response
+minifyResponse tenv (NotEquivalent md fb) = NotEquivalent (minify tenv md) fb
+minifyResponse _    res                   = res
+
 -- Waits (blocking) until it has a Response to return.
 waitForResult :: Mode -> MVar Response -> MVar Response -> IO Response
 waitForResult Debug   = waitForResultDebug
@@ -104,19 +113,15 @@ waitForResultDebug z3mv testmv = do
 --   test is too slow as well, give up.
 waitForResultRelease :: MVar Response -> MVar Response -> IO Response
 waitForResultRelease z3mv testmv = do
-      let t      = fromIntegral (Z3.timeoutTime * 1000) -- one second in microseconds
+      let t      = fromIntegral (Z3.timeoutTime * 1000) -- 1 ms == 1000 μs
       maybeZ3Res <- timeout t (readMVar z3mv)
-      -- Z3 is too slow.
-      if maybeZ3Res == Nothing then do
+      case maybeZ3Res of
+        Nothing -> do -- Z3 too slow
           maybeTestRes <- timeout t (readMVar testmv)
-          -- Test is too slow as well.
-          if maybeTestRes == Nothing then
-            return Timeout
-          else
-            return $ fromJust maybeTestRes
-      -- Z3 was fast enough
-      else
-        return $ fromJust maybeZ3Res
+          case maybeTestRes of
+            Nothing -> return Timeout -- test too slow
+            Just m  -> return m -- test fast enough
+        Just m -> return m -- Z3 fast enough
 
 -- | Makes sure that both Responses are the same, otherwise, if we
 --   run in debug mode, an error will be thrown. If not in debug mode,

src/LogicIR/Frontend/Java.hs

@@ -63,6 +63,12 @@ javaExpToLExprAlgebra =
                         ClassFieldAccess (Name name) id -> mkStringSymbol (prettyPrint (Name (name ++ [id]))) >>= mkIntVar -}
     fMethodInv inv env decls =
       case inv of -- TODO: very hardcoded EDSL + lambdas cannot be { return expr; } + ranged
+        -- Java: imp(exp1, exp2);
+        MethodCall (Name [Ident "imp"]) [exp1, exp2]
+            -> refold exp1 .==> refold exp2
+        -- Java: with(exp1, bound -> exp2);
+        MethodCall (Name [Ident "with"]) [exp1, Lambda (LambdaSingleParam bound) (LambdaExpression exp2)]
+            -> (LVar (nameToVar (Name [bound]) env decls) .== refold exp1) .==> refold exp2
         -- Java: method(name, bound -> expr);
         MethodCall (Name [Ident method]) [ExpName name, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)]
             -> quant method name bound expr

src/LogicIR/Pretty.hs

@@ -15,7 +15,7 @@ prettyLExpr =
     fUnop o a = prettyNUnop o ++ parens a
     fBinop x o y = "(" ++ x ++ " " ++ prettyLBinop o ++ " " ++ y ++ ")"
     fIf c x y = parens c ++ "?" ++ parens x ++ ":" ++ parens y
-    fQuant o x d a = parens $ prettyQuant o ++ prettyVar x ++ " :: " ++ d ++ " -> " ++ a
+    fQuant o x d a = parens $ prettyQuant o ++ " " ++ prettyVar x ++ " :: " ++ d ++ " -> " ++ a
     fArray x a = prettyVar x ++ "[" ++ a ++ "]"
     fIsnull x = "isNull" ++ parens (prettyVar x)
     fLen x = "len" ++ parens (prettyVar x)

src/Model.hs

@@ -13,6 +13,9 @@ import           Text.Parsec.Language
 import           Text.Parsec.String
 import qualified Text.Parsec.Token    as Tokens
 
+import Language.Java.Syntax
+import JavaHelpers.HelperFunctions
+
 import LogicIR.ParserUtils
 
 -- | Feedback type.
@@ -89,6 +92,11 @@ sanitize model =
             _           -> error "non-bool null"
         isNotLen k _ = not $ "?length" `isSuffixOf` k
 
+-- | Exclude model's variables that are not actual input arguments.
+minify :: TypeEnv -> Model -> Model
+minify typeEnv = M.filterWithKey (\k _ -> k `elem` vars)
+  where vars = concatMap (\(Name ids, _) -> (\(Ident s) -> s) <$> ids) typeEnv
+
 -- | Parsers.
 modelP :: Parser ModelVal
 modelP = try (BoolVal <$> boolP)

test/TExamples.hs

@@ -42,4 +42,6 @@ examples =
   , "test2" .!= "sorted3"
   , "sorted3" .!= "sorted4"
   , "sorted1" .== "sorted4"
+  , "imp1" .!= "imp2"
+  , "varIntro1" .!= "varIntro2"
   ]