Z3: Feedback for stronger/weaker

javawlp.cabal

@@ -86,6 +86,7 @@ test-suite javawlp-tests
                      , TIRParser
                      , TEquivalenceClasses
                      , TModelParser
+                     , TFeedback
   build-depends:       base
                      , javawlp
                      , test-framework

src/API.hs

@@ -31,10 +31,10 @@ data ParseMode = Raw | File
 
 type Source = String
 
-type EquivImpl = LExpr -> LExpr -> IO Response
-
 type MethodDef = ([TypeDecl], Stmt, TypeEnv)
 
+type EquivImpl = LExpr -> LExpr -> IO Response
+
 -- | Calls proveSpec and testSpec on different threads and returns
 --   their response. If the function is called in debug mode, it
 --   compares the result of testSpec and proveSpec. Otherwise, it
@@ -71,15 +71,15 @@ compareSpec m pMode methodA methodB = do
 
             mv1 <- newEmptyMVar
             mv2 <- if m == Debug then newEmptyMVar else return mv1
-            mapM_ compareSpecHelper [ (mv1, "Z3", Z3.equivalentTo)
+            mapM_ compareSpecHelper [ (mv1, "Z3", Test.equivalentTo)
                                     , (mv2, "Test", Test.equivalentTo)
                                     ]
             res1 <- readMVar mv1
             res2 <- readMVar mv2 -- if Release, this won't block
             return $ getRes m res1 res2
             where -- | Runs f on a separate thread and stores the result in mv.
-            compareSpecHelper (mv, name, impl) = forkIO $ do
-                    res <- checkSpec name impl (preL, preL') (postL, postL') 
+                  compareSpecHelper (mv, name, impl) = forkIO $ do
+                    res <- checkEquiv name impl (preL, preL') (postL, postL')
                     res `seq` putMVar mv res
 
 -- | Makes sure that both Responses are the same, otherwise, if we
@@ -90,16 +90,17 @@ getRes :: Mode     -- ^ True if debug mode, False otherwise
        -> Response -- ^ The response from proveSpec
        -> Response -- ^ The response from testSpec
        -> Response -- ^ The final response.
-getRes _        Timeout           testRes           = testRes
-getRes _        Undefined         testRes           = testRes
-getRes _        Equivalent        Equivalent        = Equivalent
-getRes _        (NotEquivalent m) (NotEquivalent _) = NotEquivalent m
-getRes Release  resp              _                 = resp
-getRes Debug    resp              resp'             =
-    error $ "proveSpec says " ++ show resp ++ ", testSpec says " ++ show resp'
-
-checkSpec :: String -> EquivImpl -> (LExpr, LExpr) -> (LExpr, LExpr) -> IO Response
-checkSpec name equivTo (preL, preL') (postL, postL') = do
+getRes _        Timeout             testRes             = testRes
+getRes _        Undefined           testRes             = testRes
+getRes _        Equivalent          Equivalent          = Equivalent
+getRes _        (NotEquivalent m f) (NotEquivalent _ _) = NotEquivalent m f
+getRes Release  resp                _                   = resp
+getRes Debug    resp                resp'               =
+  error $ "proveSpec says " ++ show resp ++ ", testSpec says " ++ show resp'
+
+-- | Check if two logic statements are equivalent.
+checkEquiv :: String -> EquivImpl -> (LExpr, LExpr) -> (LExpr, LExpr) -> IO Response
+checkEquiv name equivTo (preL, preL') (postL, postL') = do
     preRes <- preL `equivTo` preL'
     log $ "PreResponse (" ++ name ++ "):\n" ++ show preRes ++ "\n"
     postRes <- postL `equivTo` postL'

src/LogicIR/Backend/QuickCheck/API.hs

@@ -14,9 +14,10 @@ import Model
 equivalentTo :: LExpr -> LExpr -> IO Response
 equivalentTo lexpr lexpr' = do
     (eq, testModel) <- testEquality 1000 lexpr lexpr'
+    let feedback = NoFeedback -- TODO check implication (stronger + weaker)
     if eq
     then return Equivalent
-    else return $ NotEquivalent $ toZ3Model testModel
+    else return $ NotEquivalent (toZ3Model testModel) (feedback, NoFeedback)
 
 toZ3Model :: (QC.Model, QC.ArrayModel) -> Model
 toZ3Model (m, arrayM) =

src/LogicIR/Backend/Z3/API.hs

-module LogicIR.Backend.Z3.API where
+module LogicIR.Backend.Z3.API
+       ( equivalentTo
+       , showZ3AST
+       )
+       where
 
-import qualified Z3.Base as Z3
-import Z3.Monad hiding (Model)
+import qualified Z3.Base  as Z3
+import           Z3.Monad hiding (Model)
 
-import Control.Exception.Base (tryJust)
-import Control.Monad (forM)
-import Data.String
-import Data.Maybe (fromJust)
-import qualified Data.Map as M
+import           Control.Exception.Base (tryJust)
+import           Control.Monad          (forM, when)
+import qualified Data.Map               as M
+import           Data.Maybe             (fromJust)
+import           Data.String
 
+import Control.Monad.Trans   (liftIO)
 import LogicIR.Backend.Z3.Z3
-import LogicIR.Expr (LExpr)
+import LogicIR.Expr          (LExpr, lnot, (.<==>), (.==>))
 import Model
 
+data Z3Response = Satisfiable Model | Unsatisfiable | Undecidable
+                  deriving Show
+
 -- | Determine the equality of two method's pre/post conditions.
 equivalentTo :: LExpr -> LExpr -> IO Response
-equivalentTo lexpr lexpr' = do
-    let fv = freeVars2 lexpr lexpr'
-    let (ast, ast') = (lExprToZ3Ast lexpr, lExprToZ3Ast lexpr')
-    res <- tryJust errorSelector $ equivalentToZ3 fv ast ast'
-    case res of
-      Left () -> return Timeout
-      Right r -> return r
+equivalentTo l l' = do
+  equiv <- checkZ3 $ lnot (l .<==> l')
+  case equiv of
+    Satisfiable m -> do
+      feedback <- do
+        stronger <- checkZ3 $ lnot (l .==> l')
+        case stronger of
+          Unsatisfiable -> return Stronger
+          _ -> do
+            weaker <- checkZ3 $ lnot (l' .==> l)
+            case weaker of
+              Unsatisfiable -> return Weaker
+              _             -> return NoFeedback
+      return $ NotEquivalent m (feedback, NoFeedback)
+    Unsatisfiable -> return Equivalent
+    Undecidable -> return Undefined
+
+-- | Checks the validity of a logical statement.
+checkZ3 :: LExpr -> IO Z3Response
+checkZ3 l = catchTimeout $ tryZ3 $ do
+  -- solverReset
+  fv <- freeVars l
+  ast <- lExprToZ3Ast l
+  -- Get model
+  (r, model) <- local $ assert ast >> solverCheckAndGetModel
+  response <- case r of
+    Sat   -> do
+      -- Construct counter-model
+      ms <- local (sanitize . M.fromList <$>
+         forM (M.toList fv) (evalAST fv (fromJust model)))
+      return $ Satisfiable ms
+    Unsat -> return Unsatisfiable
+    _ -> return Undecidable
+  solverReset
+  return response
+  where
+    -- Construct model values
+    evalAST :: FreeVars -> Z3.Model -> (String, AST) -> Z3 (String, ModelVal)
+    evalAST fv m (k, ast) = do
+      v <- fromJust <$> modelEval m ast True
+      sortKind <- getSort v >>= getSortKind
+      if sortKind == Z3_ARRAY_SORT then do
+        -- Retrieve array's length
+        lenName <- mkStringSymbol (k ++ "?length") >>= mkIntVar
+        f <- snd <$> evalAST fv m (k ++ "?length", lenName)
+        let len = case f of
+              (IntVal i) -> i
+              _          -> error "non-int length"
+        -- Iterate array "points"
+        modelVals <- forM [0..(len-1)] (\i -> do
+          indexAST <- mkInteger $ toInteger i
+          pointAST <- mkSelect v indexAST
+          snd <$> evalAST fv m ("", pointAST)
+          )
+        return (k, ManyVal modelVals)
+      else do
+        v' <- astToString v
+        return (k, fromString v' :: ModelVal)
+
+
+-- | Run a Z3 action in 'IO', but catch timeouts.
+catchTimeout :: IO Z3Response -> IO Z3Response
+catchTimeout prog = do
+  res <- tryJust errorSelector prog
+  return $ case res of
+    Left () -> Undecidable
+    Right r -> r
     where
       errorSelector :: Z3Error -> Maybe ()
       errorSelector err =
@@ -29,75 +97,16 @@ equivalentTo lexpr lexpr' = do
           InvalidUsage -> Just ()
           _            -> Nothing
 
--- | Check if two Z3 AST's are equivalent.
-equivalentToZ3 :: Z3 FreeVars -> Z3 AST -> Z3 AST -> IO Response
-equivalentToZ3 fVars ast1' ast2' =
-  tryZ3 $ do
-    -- Setup
-    fv <- fVars
-    ast1 <- ast1'
-    ast2 <- ast2'
-    astEq <- mkEq ast1 ast2
-    astNeq <- mkNot astEq -- negate the question to get a model
-
-    -- Tactics
-    g <- mkGoal True True False
-    goalAssert g astNeq
-    t <- "qe" --> "aig"
-    a <- applyTactic t g
-    asts <- getGoalFormulas =<< getApplyResultSubgoal a 0
-    g' <- mkAnd asts
-    assert g'
-
-    -- Get model
-    (r, model) <- solverCheckAndGetModel
-    response <- case r of
-      Unsat -> return Equivalent
-      Undef -> return Undefined
-      Sat   -> do
-        ms <- M.fromList <$> forM (M.toList fv) (evalAST fv (fromJust model))
-        return $ NotEquivalent (sanitize ms)
-    solverReset
-    return response
-    where
-      -- Construct model values
-      evalAST :: FreeVars -> Z3.Model -> (String, AST) -> Z3 (String, ModelVal)
-      evalAST fv m (k, ast) = do
-        v <- fromJust <$> modelEval m ast True
-        sortKind <- getSort v >>= getSortKind
-        if sortKind == Z3_ARRAY_SORT then do
-          -- Retrieve array's length
-          lenName <- mkStringSymbol (k ++ "?length") >>= mkIntVar
-          f <- snd <$> evalAST fv m (k ++ "?length", lenName)
-          let len = case f of
-                (IntVal i) -> i
-                _          -> error "non-int length"
-          -- Iterate array "points"
-          modelVals <- forM [0..(len-1)] (\i -> do
-            indexAST <- mkInteger $ toInteger i
-            pointAST <- mkSelect v indexAST
-            snd <$> evalAST fv m ("", pointAST)
-            )
-          return (k, ManyVal modelVals)
-        else do
-          v' <- astToString v
-          return (k, fromString v' :: ModelVal)
-
 -- | Z3 try evaluation with timeout.
 tryZ3 :: Z3 a -> IO a
-tryZ3 = evalZ3With Nothing (  opt "timeout" (5000 :: Integer)
-                           +? opt "model_validate" True
-                           +? opt "well_sorted_check" True
-                           +? opt "auto_config" True
-                           -- +? opt "unsat_core" True
-                           )
-
--- | Sequence tactics.
-(-->) :: String -> String -> Z3 Z3.Tactic
-(-->) t t' = do
-  tt <- mkTactic t
-  tt' <- mkTactic t'
-  andThenTactic tt tt'
+tryZ3 prog = do
+  env <- newEnv Nothing (  opt "timeout" (5000 :: Integer)
+                        +? opt "model_validate" True
+                        +? opt "well_sorted_check" True
+                        +? opt "auto_config" True
+                        -- +? opt "unsat_core" True
+                        )
+  evalZ3WithEnv prog env
 
 -- | Pretty-print Z3 AST.
 showZ3AST :: Z3 AST -> IO String

src/LogicIR/Backend/Z3/Z3.hs

@@ -18,7 +18,7 @@ lExprToZ3AstAlgebra =
     CBool b -> mkBool b
     CInt n -> mkInteger $ toInteger n
     CReal f -> mkRealNum f
-    CNil -> error "null constants cannot be used directly with Z3 (use LogicIR.Backend.Null)"
+    CNil -> error "null constants cannot be used directly with Z3 (see LogicIR.Null)"
   fUnop o a' = do
     a <- a'
     case o of

src/LogicIR/Expr.hs

@@ -86,7 +86,7 @@ infix 1 .: ; infix 1 .!
 (.!) = LArray
 
 binOp op e = LBinop e op
-infix 2 .==> ; infix 3 .&& ; infix 3 .||
+infix 2 .<==> ; infix 2 .==> ; infix 3 .&& ; infix 3 .||
 infix 4 .== ; infix 4 .!= ; infix 4 .> ; infix 4 .< ; infix 4 .<= ; infix 4 .>=
 infix 5 .* ; infix 5 ./ ; infix 5 .%
 infix 6 .+ ; infix 6 .-
@@ -95,4 +95,5 @@ infix 6 .+ ; infix 6 .-
 (.==) = binOp CEqual ; (.!=) x y = lnot $ x .== y
 (.<) = binOp CLess ; (.<=) x y = x .< y .|| x.== y
 (.>) = binOp CGreater ; (.>=) x y = x .> y .|| x.== y
-(.&&) = binOp LAnd ; (.||) = binOp LOr ; (.==>) = binOp LImpl
+(.&&) = binOp LAnd ; (.||) = binOp LOr
+(.==>) = binOp LImpl ; (.<==>) = (.==)

src/Model.hs

@@ -4,36 +4,39 @@
 {-# LANGUAGE TypeSynonymInstances #-}
 module Model where
 
-import Data.List (isSuffixOf)
-import qualified Data.Map as M
-import Data.String
-import GHC.Generics
-import Text.Parsec hiding (runP)
-import Text.Parsec.Language
-import Text.Parsec.String
-import qualified Text.Parsec.Token as Tokens
+import           Data.List            (isSuffixOf)
+import qualified Data.Map             as M
+import           Data.String
+import           GHC.Generics
+import           Text.Parsec          hiding (runP)
+import           Text.Parsec.Language
+import           Text.Parsec.String
+import qualified Text.Parsec.Token    as Tokens
 
 import LogicIR.ParserUtils
 
+-- | Feedback type.
+data Feedback = Stronger   -- A ==> B
+              | Weaker     -- A <== B
+              | NoFeedback -- A ??? B
+                deriving (Eq, Show, Generic)
+
 -- | Response type.
-data Response = Equivalent | NotEquivalent Model | ErrorResponse String | Undefined | Timeout
-                deriving (Eq)
+data Response = Equivalent
+              | NotEquivalent Model (Feedback, Feedback)
+              | ErrorResponse String
+              | Undefined
+              | Timeout
+                deriving (Eq, Show)
 
 (<>) :: Response -> Response -> Response
-ErrorResponse e <> _ = ErrorResponse e
-_ <> ErrorResponse e = ErrorResponse e
-Equivalent <> r = r
-NotEquivalent s <> _ = NotEquivalent s
-Timeout <> _ = Timeout
-Undefined <> _ = Undefined
-
-instance Show Response where
-  show Equivalent = "Formulas are equivalent"
-  show (NotEquivalent model) = "Not equivalent: " ++ show model
-  show (ErrorResponse e) = "*** Error: " ++ show e
-  show Undefined = "Oops... could not determine if formulas are equivalent"
-  show Timeout = "Timeout occured"
-
+ErrorResponse e        <> _                       = ErrorResponse e
+_                      <> ErrorResponse e         = ErrorResponse e
+Timeout                <> _                       = Timeout
+Undefined              <> _                       = Undefined
+Equivalent             <> r                       = r
+NotEquivalent s (f, _) <> NotEquivalent _ (f', _) = NotEquivalent s (f, f')
+r                      <> _                       = r
 
 -- | Model type.
 data ModelVal = BoolVal Bool
@@ -46,6 +49,8 @@ type Model = M.Map String ModelVal
 
 emptyModel :: Model
 emptyModel = M.empty
+emptyFeedback :: (Feedback, Feedback)
+emptyFeedback = (NoFeedback, NoFeedback)
 
 -- | Pretty-printing.
 instance Show ModelVal where

src/Server.hs

@@ -52,8 +52,10 @@ data ApiResponse = ApiResponse
   { responseType :: ApiResponseType
   , model        :: Maybe Model
   , err          :: Maybe String
+  , feedback     :: Maybe (Feedback, Feedback)
   }
   deriving (Eq, Show, Generic)
+instance ToJSON Feedback
 instance ToJSON ApiResponseType
 instance ToJSON ApiResponse
 instance ToJSON ModelVal where
@@ -62,6 +64,13 @@ instance ToJSON ModelVal where
   toJSON (RealVal n)  = toJSON n
   toJSON (ManyVal vs) = Array $ fromList $ map toJSON vs
 
+-- | Default API response.
+defResp = ApiResponse { responseType = Undef
+                      , model = Nothing
+                      , err = Nothing
+                      , feedback = Nothing
+                      }
+
 type CompareApi = "compare"
   :> ReqBody '[JSON] ApiReqBody
   :> Post '[JSON] ApiResponse
@@ -74,13 +83,16 @@ getCompareResponse ApiReqBody {sourceA = srcA, sourceB = srcB} = do
     resp <- liftIO $ compareSpec Release Raw (wrap srcA) (wrap srcB)
     return $ case resp of
                   Equivalent ->
-                    ApiResponse { responseType = Equiv, model = Nothing, err = Nothing }
-                  NotEquivalent m ->
-                    ApiResponse { responseType = NotEquiv, model = Just m, err = Nothing }
+                    defResp { responseType = Equiv }
+                  NotEquivalent m f ->
+                    defResp { responseType = NotEquiv
+                            , model = Just m
+                            , feedback = Just f
+                            }
                   ErrorResponse e ->
-                    ApiResponse { responseType = ResponseErr, model = Nothing, err = Just e }
+                    defResp { responseType = ResponseErr, err = Just e }
                   _ ->
-                    ApiResponse { responseType = Undef, model = Nothing, err = Nothing }
+                    defResp { responseType = Undef }
     where
       wrap s = ( "public class Main {" ++ s ++ "}"
                , last $ splitOn " " $ head $ splitOn "(" s
@@ -106,6 +118,7 @@ instance ToSample ApiResponse where
       , ("i", IntVal 10)
       ]
     , err = Nothing
+    , feedback = Just (NoFeedback, Stronger)
     }
 
 docsBS :: ByteString
@@ -117,6 +130,7 @@ docsBS = encodeUtf8
         opts = DocOptions 1
 
 -- | API documentation (Swagger).
+instance ToSchema Feedback
 instance ToSchema ApiReqBody
 instance ToSchema ApiResponseType
 instance ToSchema ApiResponse

test/Spec.hs

@@ -5,6 +5,7 @@ import TExamples
 import TIRParser
 import TEquivalenceClasses
 import TModelParser
+import TFeedback
 
 main = defaultMain
   [ constructTestSuite testName testSuite
@@ -14,8 +15,9 @@ main = defaultMain
       , ("EXAMPLES", examples)
       , ("EQUIV_REAL", genEquivTests "examples/test_equiv/Reals.java")
       , ("EQUIV_ARRAY", genEquivTests "examples/test_equiv/Arrays.java")
+      , ("FEEDBACK", feedbackTests)
       ]
   ]
-
-constructTestSuite s suite =
-  testGroup s [testCase (s ++ "_" ++ show i) t | (i, t) <- zip [1..] suite]
+  where
+    constructTestSuite s suite =
+      testGroup s [testCase (s ++ "_" ++ show i) t | (i, t) <- zip [1..] suite]

test/TEquivalenceClasses.hs

@@ -17,10 +17,10 @@ testEquiv :: Response -> String -> String -> String -> Assertion
 testEquiv b src s s' = do
   res <- hSilence [stdout, stderr] $ compareSpec Debug File (src, s) (src, s')
   (case res of
-    NotEquivalent x -> NotEquivalent emptyModel
+    NotEquivalent _ _ -> NotEquivalent emptyModel emptyFeedback
     x               -> x) @?= b
 (.==) = testEquiv Equivalent
-(.!=) = testEquiv $ NotEquivalent emptyModel
+(.!=) = testEquiv $ NotEquivalent emptyModel emptyFeedback
 
 genEquivTests edslSrc =
   let methodIds = unsafePerformIO (hSilence [stdout, stderr] $ parseMethodIds edslSrc)

test/TExamples.hs

@@ -11,12 +11,12 @@ src = "examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
 
 testEquiv :: Response -> String -> String -> Assertion
 testEquiv b s s' = do
-  res <- hSilence [stdout, stderr] $ compareSpec Debug File (src, s) (src, s')
+  res <- hSilence [stdout, stderr] $ compareSpec Release File (src, s) (src, s')
   (case res of
-    NotEquivalent _ -> NotEquivalent emptyModel
-    x               -> x) @?= b
+    NotEquivalent _ _ -> NotEquivalent emptyModel emptyFeedback
+    x                 -> x) @?= b
 (.==) = testEquiv Equivalent
-(.!=) = testEquiv $ NotEquivalent emptyModel
+(.!=) = testEquiv $ NotEquivalent emptyModel emptyFeedback
 (.??) = testEquiv Timeout
 
 examples =

test/TFeedback.hs

+{-# LANGUAGE OverloadedStrings #-}
+module TFeedback where
+import System.IO          (stderr, stdout)
+import System.IO.Silently (hSilence)
+import System.IO.Unsafe   (unsafePerformIO)
+import Test.HUnit
+
+import LogicIR.Expr
+import LogicIR.Parser
+import LogicIR.Backend.Z3.API
+import Model
+
+testEquiv :: Response -> LExpr -> LExpr -> Assertion
+testEquiv b s s' = do
+  res <- hSilence [stdout, stderr] $ equivalentTo s s'
+  (case res of
+    NotEquivalent _ f -> NotEquivalent emptyModel f
+    x                 -> x) @?= b
+(!!=) s s' f = testEquiv (NotEquivalent emptyModel (f, NoFeedback)) s s'
+
+feedbackTests =
+  [ ("true /\\ x:int == 1" !!= "false \\/ x:int >= 1") Stronger
+  , ("true /\\ x:int >= 1" !!= "false \\/ x:int == 1") Weaker
+  , ("x:int == 1 /\\ y:int == 1" !!= "x:int == 2 /\\ y:int == 1") NoFeedback
+  , ("x:[int][0] != 0 /\\ x:[int][1] != 0"
+      !!= "x:[int][0] != 0 \\/ x:[int][1] != 0") Stronger
+  ]