From 720eb88fa49afed6f6b5ba8332881fc627810500 Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Thu, 8 Mar 2018 23:56:29 +0100
Subject: [PATCH] Z3: Feedback for stronger/weaker
---
javawlp.cabal | 1 +
src/API.hs | 31 ++---
src/LogicIR/Backend/QuickCheck/API.hs | 3 +-
src/LogicIR/Backend/Z3/API.hs | 175 ++++++++++++++------------
src/LogicIR/Backend/Z3/Z3.hs | 2 +-
src/LogicIR/Expr.hs | 5 +-
src/Model.hs | 53 ++++----
src/Server.hs | 24 +++-
test/Spec.hs | 8 +-
test/TEquivalenceClasses.hs | 4 +-
test/TExamples.hs | 8 +-
test/TFeedback.hs | 27 ++++
12 files changed, 201 insertions(+), 140 deletions(-)
create mode 100644 test/TFeedback.hs
diff --git a/javawlp.cabal b/javawlp.cabal
index b2eb980..ddf2366 100644
--- a/javawlp.cabal
+++ b/javawlp.cabal
@@ -86,6 +86,7 @@ test-suite javawlp-tests
, TIRParser
, TEquivalenceClasses
, TModelParser
+ , TFeedback
build-depends: base
, javawlp
, test-framework
diff --git a/src/API.hs b/src/API.hs
index 81a3f59..a577fda 100644
--- a/src/API.hs
+++ b/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'
diff --git a/src/LogicIR/Backend/QuickCheck/API.hs b/src/LogicIR/Backend/QuickCheck/API.hs
index 7e7d233..e2fcc8b 100644
--- a/src/LogicIR/Backend/QuickCheck/API.hs
+++ b/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) =
diff --git a/src/LogicIR/Backend/Z3/API.hs b/src/LogicIR/Backend/Z3/API.hs
index f761068..0fe5a16 100644
--- a/src/LogicIR/Backend/Z3/API.hs
+++ b/src/LogicIR/Backend/Z3/API.hs
@@ -1,27 +1,95 @@
-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
diff --git a/src/LogicIR/Backend/Z3/Z3.hs b/src/LogicIR/Backend/Z3/Z3.hs
index f77c055..6440998 100644
--- a/src/LogicIR/Backend/Z3/Z3.hs
+++ b/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
diff --git a/src/LogicIR/Expr.hs b/src/LogicIR/Expr.hs
index 8645935..51394d2 100644
--- a/src/LogicIR/Expr.hs
+++ b/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 ; (.<==>) = (.==)
diff --git a/src/Model.hs b/src/Model.hs
index 59d9658..f23e717 100644
--- a/src/Model.hs
+++ b/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
diff --git a/src/Server.hs b/src/Server.hs
index 6fbb0e3..ddacd7d 100644
--- a/src/Server.hs
+++ b/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
diff --git a/test/Spec.hs b/test/Spec.hs
index 4baa535..d8f8ac9 100644
--- a/test/Spec.hs
+++ b/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]
diff --git a/test/TEquivalenceClasses.hs b/test/TEquivalenceClasses.hs
index 855d1f2..7d4ac12 100644
--- a/test/TEquivalenceClasses.hs
+++ b/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)
diff --git a/test/TExamples.hs b/test/TExamples.hs
index 6a03032..5afa55b 100644
--- a/test/TExamples.hs
+++ b/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 =
diff --git a/test/TFeedback.hs b/test/TFeedback.hs
new file mode 100644
index 0000000..0065748
--- /dev/null
+++ b/test/TFeedback.hs
@@ -0,0 +1,27 @@
+{-# 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
+ ]
--
GitLab