From 48f4b2be1dae02dc7a2d98258e9d9da578054a8b Mon Sep 17 00:00:00 2001
From: Duncan Ogilvie <mr.exodia.tpodt@gmail.com>
Date: Sun, 8 Oct 2017 22:48:24 +0200
Subject: [PATCH] implemented LogicIR.Backend.Z3
closes #10
---
src/Javawlp/Engine/Verifier.hs | 16 +--------
src/LogicIR/Backend/Pretty.hs | 5 ++-
src/LogicIR/Backend/Z3.hs | 60 +++++++++++++++++++++++++---------
src/LogicIR/Expr.hs | 5 ++-
src/LogicIR/Fold.hs | 6 ++--
src/LogicIR/Frontend/Java.hs | 10 +++---
src/SimpleFormulaChecker.hs | 45 ++++++++++++++++---------
7 files changed, 88 insertions(+), 59 deletions(-)
diff --git a/src/Javawlp/Engine/Verifier.hs b/src/Javawlp/Engine/Verifier.hs
index 990fbb1..435dc38 100644
--- a/src/Javawlp/Engine/Verifier.hs
+++ b/src/Javawlp/Engine/Verifier.hs
@@ -32,20 +32,6 @@ isFalse env decls e =
Unsat -> return True
_ -> return False
--- | Check if two formulas are equivalent
-isEquivalent :: (TypeEnv, [TypeDecl], Exp) -> (TypeEnv, [TypeDecl], Exp) -> IO (Result, Maybe Model)
-isEquivalent (env1, decls1, e1) (env2, decls2, e2) = evalZ3 z3
- where
- z3 = do
- ast1 <- foldExp expAssertAlgebra e1 env1 decls1
- ast2 <- foldExp expAssertAlgebra e2 env2 decls2
- astEq <- mkEq ast1 ast2
- blub <- mkNot astEq -- negate the question to get a model
- assert blub
- r <- solverCheckAndGetModel -- check in documentatie
- solverReset
- return r
-
zprint :: MonadZ3 z3 => (a -> z3 String) -> a -> z3 ()
zprint mshowx x = mshowx x >>= liftIO . putStrLn
@@ -86,7 +72,7 @@ testForall = evalZ3 $
where int x = mkStringSymbol x >>= mkIntVar
printFunc x = zprint funcDeclToString x
printAst x = zprint astToString x
-
+
-- | Check if a formula is satisfiable, and if so, return the model for it as well.
-- The result is a pair (r,m) where r is either Sat, Unsat, or Undef. If r is Sat,
diff --git a/src/LogicIR/Backend/Pretty.hs b/src/LogicIR/Backend/Pretty.hs
index 23af8bb..019bb2a 100644
--- a/src/LogicIR/Backend/Pretty.hs
+++ b/src/LogicIR/Backend/Pretty.hs
@@ -9,7 +9,7 @@ prettyLExpr :: LExpr -> String
prettyLExpr = foldLExpr prettyLExprAlgebra
prettyType :: Type -> String
-prettyType (TPrim PInt) = "int"
+prettyType (TPrim PInt32) = "int"
prettyType (TPrim PBool) = "bool"
prettyType (TArray t) = prettyType t ++ "[]"
@@ -25,7 +25,6 @@ prettyLBinop :: LBinop -> String
prettyLBinop LAnd = "&&"
prettyLBinop LOr = "||"
prettyLBinop LImpl = "->"
-prettyLBinop LBicond = "<->"
prettyNBinop :: NBinop -> String
prettyNBinop NAdd = "+"
@@ -53,7 +52,7 @@ prettyLExprAlgebra = (flConst, prettyVar, flNot, flBinop, flComp, flQuant, flArr
flBinop a o b = a ++ " " ++ prettyLBinop o ++ " " ++ b
flComp a o b = a ++ " " ++ prettyCOp o ++ " " ++ b
flQuant o v a = '(' : show o ++ " " ++ prettyVar v ++ " . " ++ a ++ ")"
- flArray v [a] = prettyVar v ++ "[" ++ (foldLExpr prettyLExprAlgebra a) ++ "]"
+ flArray v a = prettyVar v ++ "[" ++ a ++ "]"
flNil = "nil"
fnConst n = show n
fnUnop o a = prettyNUnop o ++ a
diff --git a/src/LogicIR/Backend/Z3.hs b/src/LogicIR/Backend/Z3.hs
index be09ac9..f40a117 100644
--- a/src/LogicIR/Backend/Z3.hs
+++ b/src/LogicIR/Backend/Z3.hs
@@ -8,13 +8,20 @@ import LogicIR.Fold
lExprToZ3Ast :: LExpr -> Z3 AST
lExprToZ3Ast = foldLExpr lExprToZ3AstAlgebra
+-- TODO: support more types
lExprToZ3AstAlgebra :: LExprAlgebra (Z3 AST)
lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, flNil, fnConst, fnUnop, fnBinop, fnIf, fnLen) where
flConst b = mkBool b
flVar (Var t n) = do symbol <- mkStringSymbol n
case t of
- TPrim PInt -> mkIntVar symbol
+ TPrim PInt32 -> mkBvVar symbol 32
TPrim PBool -> mkBoolVar symbol
+ TArray (TPrim PInt32) -> do intSort <- mkBvSort 32
+ arraySort <- mkArraySort intSort intSort
+ mkVar symbol arraySort
+ TArray (TPrim PBool) -> do intSort <- mkBvSort 32
+ arraySort <- mkBoolSort >>= mkArraySort intSort
+ mkVar symbol arraySort
_ -> error $ show n
flNot a = a >>= mkNot
flBinop a' o b' = do a <- a'
@@ -23,25 +30,48 @@ lExprToZ3AstAlgebra = (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray,
LAnd -> mkAnd [a, b]
LOr -> mkOr [a, b]
LImpl -> mkImplies a b
- LBicond -> undefined
flComp a' o b' = do a <- a'
b <- b'
case o of
CEqual -> mkEq a b
CNEqual -> mkEq a b >>= mkNot
- CLess -> mkLt a b
- CGreater -> mkGt a b
- CLeq -> mkLe a b
- CGeq -> mkGe a b
- flQuant = undefined
- flArray = undefined
- flNil = undefined
- fnConst n = mkInteger (fromIntegral n)
- fnUnop = undefined
+ CLess -> mkBvslt a b
+ CGreater -> mkBvsgt a b
+ CLeq -> mkBvsle a b
+ CGeq -> mkBvsge a b
+ flQuant o v@(Var t n) a' = do a <- a'
+ case t of
+ TPrim PInt32 -> do vApp <- flVar v >>= toApp
+ case o of
+ QAll -> mkForallConst [] [vApp] a
+ QAny -> mkExistsConst [] [vApp] a
+ _ -> error $ show (o, v)
+ flArray v a' = do v <- flVar v
+ a <- a'
+ mkSelect v a
+ flNil = do intSort <- mkBvSort 32
+ zero <- mkBitvector 32 0
+ mkConstArray intSort zero
+ fnConst n = mkBitvector 32 (fromIntegral n)
+ fnUnop o a' = do a <- a'
+ case o of
+ NNeg -> mkBvneg a
+ NNot -> mkBvnot a
fnBinop a' o b' = do a <- a'
b <- b'
case o of
- NAdd -> mkAdd [a, b]
- _ -> undefined
- fnIf = undefined
- fnLen = undefined
\ No newline at end of file
+ NAdd -> mkBvadd a b
+ NSub -> mkBvsub a b
+ NMul -> mkBvmul a b
+ NDiv -> mkBvsdiv a b -- NOTE: signed division
+ NRem -> mkBvsrem a b -- TODO: check if the correct remainder is taken
+ NShl -> mkBvshl a b
+ NShr -> mkBvashr a b -- NOTE: signed shift right will keep the sign
+ NAnd -> mkBvand a b
+ NOr -> mkBvor a b
+ NXor -> mkBvxor a b
+ fnIf c' a' b' = do c <- c'
+ a <- a'
+ b <- b'
+ mkIte c a b
+ fnLen (Var (TArray (TPrim _)) n) = mkStringSymbol (n ++ ".length") >>= flip mkBvVar 32
diff --git a/src/LogicIR/Expr.hs b/src/LogicIR/Expr.hs
index 8a1ae38..605a48f 100644
--- a/src/LogicIR/Expr.hs
+++ b/src/LogicIR/Expr.hs
@@ -4,7 +4,7 @@ module LogicIR.Expr where
-- Based on my (Duncan's) previous work: https://github.com/mrexodia/wp/blob/master/Wp.hs
data Primitive = PBool
- | PInt
+ | PInt32
deriving (Show, Eq, Read)
data Type = TPrim Primitive
@@ -39,7 +39,6 @@ data NBinop = NAdd -- a + b
data LBinop = LAnd -- Conjunction
| LOr -- Disjunction
| LImpl -- Implication
- | LBicond -- Biconditional (TODO: remove?)
deriving (Show, Eq, Read)
-- Quantifier operators
@@ -64,7 +63,7 @@ data LExpr = LConst Bool -- True/False
| LBinop LExpr LBinop LExpr -- Logical operator
| LComp NExpr COp NExpr -- Integer comparison
| LQuant QOp Var LExpr -- Logical quantifier
- | LArray Var [NExpr] -- Logical array access
+ | LArray Var NExpr -- Logical array access
| LNil -- Nil constant
| NConst Int -- Integer constant (TODO: use Integer instead of Int?)
diff --git a/src/LogicIR/Fold.hs b/src/LogicIR/Fold.hs
index a93c662..75ba32c 100644
--- a/src/LogicIR/Fold.hs
+++ b/src/LogicIR/Fold.hs
@@ -9,7 +9,7 @@ type LExprAlgebra r = (Bool -> r, -- LConst
r -> LBinop -> r -> r, -- LBinop
r -> COp -> r -> r, -- LComp
QOp -> Var -> r -> r, -- LQuant
- Var -> [NExpr] -> r, -- LArray
+ Var -> r -> r, -- LArray
r, -- LNil
Int -> r, -- NConst
NUnop -> r -> r, -- NUnop
@@ -23,12 +23,12 @@ foldLExpr :: LExprAlgebra r -> LExpr -> r
foldLExpr (flConst, flVar, flNot, flBinop, flComp, flQuant, flArray, flNil, fnConst, fnUnop, fnBinop, fnIf, fnLen) = fold where
fold e = case e of
LConst c -> flConst c
- LVar n -> flVar n
+ LVar v -> flVar v
LNot e -> flNot (fold e)
LBinop a o b -> flBinop (fold a) o (fold b)
LComp a o b -> flComp (fold a) o (fold b)
LQuant o v e -> flQuant o v (fold e)
- LArray n e -> flArray n e
+ LArray v e -> flArray v (fold e)
LNil -> flNil
NConst n -> fnConst n
NUnop o e -> fnUnop o (fold e)
diff --git a/src/LogicIR/Frontend/Java.hs b/src/LogicIR/Frontend/Java.hs
index 97dc77e..fcc1314 100644
--- a/src/LogicIR/Frontend/Java.hs
+++ b/src/LogicIR/Frontend/Java.hs
@@ -18,8 +18,8 @@ nameToVar :: Name -> TypeEnv -> [TypeDecl] -> Var
nameToVar name env decls = let (arrayType, symbol) = (lookupType decls env name, prettyPrint name) in
case arrayType of
PrimType BooleanT -> Var (TPrim PBool) symbol
- PrimType IntT -> Var (TPrim PInt) symbol
- RefType (ArrayType (PrimType IntT)) -> Var (TArray (TPrim PInt)) symbol
+ PrimType IntT -> Var (TPrim PInt32) symbol
+ RefType (ArrayType (PrimType IntT)) -> Var (TArray (TPrim PInt32)) symbol
_ -> error $ "Unimplemented nameToVar for " ++ show (name, arrayType)
javaExpToLExprAlgebra :: ExpAlgebra (TypeEnv -> [TypeDecl] -> LExpr)
@@ -39,16 +39,16 @@ javaExpToLExprAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation,
fFieldAccess = undefined
fMethodInv inv env decls = case inv of -- TODO: very hardcoded EDSL + lambdas cannot be { return expr; }
MethodCall (Name [Ident "forall"]) [ExpName name, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)]
- -> let (i, arr) = (Var (TPrim PInt) bound, nameToVar name env decls) in
+ -> let (i, arr) = (Var (TPrim PInt32) bound, nameToVar name env decls) in
LQuant QAll i (LBinop (LBinop (LComp (LVar i) CGeq (NConst 0)) LAnd (LComp (LVar i) CLess (NLen arr))) LImpl (foldExp javaExpToLExprAlgebra expr env decls))
MethodCall (Name [Ident "exists"]) [ExpName name, Lambda (LambdaSingleParam (Ident bound)) (LambdaExpression expr)]
- -> let (i, arr) = (Var (TPrim PInt) bound, nameToVar name env decls) in
+ -> let (i, arr) = (Var (TPrim PInt32) bound, nameToVar name env decls) in
LQuant QAny i (LBinop (LBinop (LComp (LVar i) CGeq (NConst 0)) LAnd (LComp (LVar i) CLess (NLen arr))) LAnd (foldExp javaExpToLExprAlgebra expr env decls))
_
-> error $ "Unimplemented fMethodInv: " ++ show inv
fArrayAccess arrayIndex env decls = case arrayIndex of -- TODO: type checking
ArrayIndex (ExpName name) [ExpName index]
- -> LArray (nameToVar name env decls) [LVar (nameToVar index env decls)]
+ -> LArray (nameToVar name env decls) (LVar (nameToVar index env decls))
_
-> error $ "Multidimensional arrays are not supported: " ++ show (arrayIndex)
fExpName name env decls = case name of -- TODO: type checking
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index f151e4f..161b978 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -109,24 +109,40 @@ orExprs = combineExprs COr
extractExpr :: Op -> [MethodInvocation] -> Exp
extractExpr op call = combineExprs op $ map (\(MethodCall (Name [Ident _]) [a]) -> a) call
+-- | Check if two formulas 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
+
+showZ3AST :: Z3 AST -> IO String
+showZ3AST ast' = evalZ3 $ ast' >>= astToString
+
determineFormulaEq :: MethodDef -> MethodDef -> String -> IO ()
determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do
-- get preconditions
let (e1, e2) = (extractCond m1 name, extractCond m2 name)
+ let (lexpr1, lexpr2) = (javaExpToLExpr e1 env1 decls1, javaExpToLExpr e2 env2 decls2)
+ let (ast1, ast2) = (lExprToZ3Ast lexpr1, lExprToZ3Ast lexpr2)
putStrLn $ "e1:\n" ++ prettyPrint e1 ++ "\n\ne2:\n" ++ prettyPrint e2 ++ "\n"
- let lexpr = javaExpToLExpr e1 env1 decls1
- putStrLn $ "LogicIR.Expr:\n" ++ show lexpr ++ "\n\nLogicIR.Pretty:\n" ++ prettyLExpr lexpr
- putStrLn "\nZ3 AST:"
- evalZ3 $ do asd <- lExprToZ3Ast lexpr
- zprint astToString asd
- return asd
- putStrLn "\nZ3 Result:"
- {--- get postconditions
- let (post1, post2) = (extractCond m1 "post", extractCond m2 "post")
- putStrLn $ "post1:\n" ++ prettyPrint post1 ++ "\npost2:\n" ++ prettyPrint post2 ++ "\n"-}
+ putStrLn $ "LogicIR.Expr 1:\n" ++ show lexpr1 ++ "\n\nLogicIR.Expr 2:\n" ++ show lexpr2 ++ "\n"
+ putStrLn $ "LogicIR.Pretty 1:\n" ++ prettyLExpr lexpr1 ++ "\n\nLogicIR.Pretty 2:\n" ++ prettyLExpr lexpr2 ++ "\n"
+ ast1s <- showZ3AST ast1
+ putStrLn $ "Z3 AST 1:\n" ++ ast1s ++ "\n"
+ ast2s <- showZ3AST ast2
+ putStrLn $ "Z3 AST 2:\n" ++ ast2s ++ "\n"
+ 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 (env1, decls1, e1) (env2, decls2, e2)
+ (result, model) <- isEquivalent ast1 ast2
case result of
Unsat -> putStrLn "formulas are equivalent!"
Undef -> putStrLn "unable to decide the satisfiablity (TODO: use QuickCheck)"
@@ -141,13 +157,13 @@ determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do
extractCond m n = extractExpr CAnd (getMethodCalls m n)
compareSpec :: (FilePath, String) -> (FilePath, String) -> IO ()
-compareSpec method1 method2 = do
+compareSpec method1@(_, name1) method2@(_, name2) = do
-- load the methods
m1@(decls1, mbody1, env1) <- parseMethod method1
m2@(decls2, mbody2, env2) <- parseMethod method2
if env1 /= env2 then fail "inconsistent method parameters" else return ()
if decls1 /= decls2 then fail "inconsistent class declarations (TODO)" else return ()
- putStrLn "----PRE----"
+ putStrLn $ "----PRE---- (" ++ name1 ++ " vs " ++ name2 ++ ")"
determineFormulaEq m1 m2 "pre"
putStrLn "\n----POST---"
determineFormulaEq m1 m2 "post"
@@ -155,5 +171,4 @@ compareSpec method1 method2 = do
edslSrc = "javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
testEq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec1")
testNeq = compareSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec2")
-
-blub = compareSpec (edslSrc, "simple1") (edslSrc, "simple1")
\ No newline at end of file
+blub = compareSpec (edslSrc, "getMax_spec1") (edslSrc, "getMax_spec2")
\ No newline at end of file
--
GitLab