From 304a8d3bf2c7b037769c36f3465c1dbe7a645c0d Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Mon, 5 Feb 2018 16:18:08 +0100
Subject: [PATCH] Rebased Z3 onto QuickCheck.
---
javawlp.cabal | 23 ++++++-----
.../{ => QuickCheck}/ModelGenerator.hs | 15 +++----
src/LogicIR/Backend/{ => QuickCheck}/Test.hs | 13 +++---
src/LogicIR/Backend/{ => Z3}/API.hs | 8 ++--
src/LogicIR/Backend/{ => Z3}/Model.hs | 4 +-
src/LogicIR/Backend/{ => Z3}/Pretty.hs | 5 ++-
src/LogicIR/Backend/{ => Z3}/Z3.hs | 2 +-
src/LogicIR/Eval.hs | 22 +++-------
src/LogicIR/Pretty.hs | 1 -
src/SimpleFormulaChecker.hs | 41 +++++++++++++++----
test/Spec.hs | 1 +
test/TIRTest.hs | 2 +-
test/TZ3Model.hs | 3 +-
13 files changed, 76 insertions(+), 64 deletions(-)
rename src/LogicIR/Backend/{ => QuickCheck}/ModelGenerator.hs (87%)
rename src/LogicIR/Backend/{ => QuickCheck}/Test.hs (97%)
rename src/LogicIR/Backend/{ => Z3}/API.hs (94%)
rename src/LogicIR/Backend/{ => Z3}/Model.hs (98%)
rename src/LogicIR/Backend/{ => Z3}/Pretty.hs (97%)
rename src/LogicIR/Backend/{ => Z3}/Z3.hs (98%)
diff --git a/javawlp.cabal b/javawlp.cabal
index a4f01e0..eb917c3 100644
--- a/javawlp.cabal
+++ b/javawlp.cabal
@@ -20,28 +20,31 @@ library
exposed-modules: Javawlp.Engine.Types
, Javawlp.Engine.HelperFunctions
, Javawlp.Engine.Folds
+ -- LIR
, LogicIR.Expr
, LogicIR.Fold
, LogicIR.Parser
, LogicIR.Null
, LogicIR.Pretty
, LogicIR.Frontend.Java
- , LogicIR.Backend.Z3
- , LogicIR.Backend.Test
- , LogicIR.Backend.ModelGenerator
- , LogicIR.Backend.Pretty
- , LogicIR.Backend.Null
- , LogicIR.Fold
, LogicIR.Eval
- , LogicIR.Backend.API
- , LogicIR.Backend.Model
+ -- Checker
+ , SimpleFormulaChecker
+ -- Z3
+ , LogicIR.Backend.Z3.Z3
+ , LogicIR.Backend.Z3.API
+ , LogicIR.Backend.Z3.Model
+ , LogicIR.Backend.Z3.Pretty
+ -- QuickCheck
+ , LogicIR.Backend.QuickCheck.Test
+ , LogicIR.Backend.QuickCheck.ModelGenerator
+ -- Java EDSL
, Language.Java.Lexer
, Language.Java.Parser
, Language.Java.Pretty
, Language.Java.Syntax
, Language.Java.Syntax.Exp
, Language.Java.Syntax.Types
- , SimpleFormulaChecker
build-depends: base >= 4.7 && < 5
, random
, parsec
@@ -52,8 +55,6 @@ library
, mtl
, containers
default-language: Haskell2010
- -- build-tools: alex, happy
- -- other-modules: ModelParser.Lexer, ModelParser.Parser
test-suite javawlp-tests
type: exitcode-stdio-1.0
diff --git a/src/LogicIR/Backend/ModelGenerator.hs b/src/LogicIR/Backend/QuickCheck/ModelGenerator.hs
similarity index 87%
rename from src/LogicIR/Backend/ModelGenerator.hs
rename to src/LogicIR/Backend/QuickCheck/ModelGenerator.hs
index 425cf6e..ac57a56 100644
--- a/src/LogicIR/Backend/ModelGenerator.hs
+++ b/src/LogicIR/Backend/QuickCheck/ModelGenerator.hs
@@ -1,18 +1,19 @@
-module LogicIR.Backend.ModelGenerator (generateModel, generateArrayModel, Model, ArrayModel) where
+module LogicIR.Backend.QuickCheck.ModelGenerator (generateModel, generateArrayModel, Model, ArrayModel) where
-import LogicIR.Expr
import Data.List (find, nub, (\\))
import System.Random
import Data.Maybe (isNothing, fromJust)
import Data.Map (Map)
import qualified Data.Map.Lazy as M
+import LogicIR.Expr
+
type Model = [(LExpr, LExpr)]
type ArrayModel = Map Var [LConst]
-- Generates a constant value for all vars vars in the given list.
generateModel :: [LExpr] -> IO Model
-generateModel exprs = mapM generateModelEntry exprs
+generateModel = mapM generateModelEntry
generateArrayModel :: [LExpr] -> IO ArrayModel
generateArrayModel es = mapM generateArray es >>= \l -> return (M.fromList l)
@@ -31,9 +32,9 @@ generateArrayModel es = mapM generateArray es >>= \l -> return (M.fromList l)
This is because otherwise, the evaluation of an LExpr should be changed drastically.
After all, How do you evaluate a[0] or a.length if a == null... -}
generateModelEntry :: LExpr -> IO (LExpr, LExpr)
-generateModelEntry e@(LVar (Var (TPrim t) _)) = do
+generateModelEntry e@(LVar (Var (TPrim t) _)) =
generatePrimitive t >>= \v -> return (e, v)
-generateModelEntry e@(LIsnull (Var (TArray _) _)) = do
+generateModelEntry e@(LIsnull (Var (TArray _) _)) =
generatePrimitive PBool >>= \v -> return (e, v)
generateModelEntry e =
error $ "Cannot generate model entry for " ++ show e
@@ -54,9 +55,9 @@ generateIntWithBounds b = getStdRandom (randomR b)
-- some type primitive type.
bounds :: Primitive -> (Int, Int)
bounds PBool = (0, 1)
-bounds PInt32 = (-10, 10)
+bounds PInt = (-10, 10)
-- Generates an LExpr given a Primitive type and a value.
toLExpr :: Primitive -> Int -> LExpr
toLExpr PBool v = LConst $ CBool $ v == 1
-toLExpr PInt32 v = LConst $ CInt $ v
\ No newline at end of file
+toLExpr PInt v = LConst $ CInt v
diff --git a/src/LogicIR/Backend/Test.hs b/src/LogicIR/Backend/QuickCheck/Test.hs
similarity index 97%
rename from src/LogicIR/Backend/Test.hs
rename to src/LogicIR/Backend/QuickCheck/Test.hs
index 902110c..9184458 100644
--- a/src/LogicIR/Backend/Test.hs
+++ b/src/LogicIR/Backend/QuickCheck/Test.hs
@@ -1,12 +1,11 @@
-module LogicIR.Backend.Test (testEquality) where
+module LogicIR.Backend.QuickCheck.Test (testEquality) where
import LogicIR.Expr
import LogicIR.Fold
import LogicIR.Eval
-import LogicIR.Backend.ModelGenerator
-import Data.Maybe (fromMaybe)
+import LogicIR.Backend.QuickCheck.ModelGenerator
+import Data.Maybe (fromMaybe, isNothing, fromJust)
import Data.List (find, nub, (\\))
-import Data.Maybe (isNothing, fromJust)
import Data.Map (Map)
import qualified Data.Map.Lazy as M
@@ -26,7 +25,7 @@ testEquality 0 e1 e2 = do
return (True, ([], M.empty))
testEquality n e1 e2 = do
(r,m1,m2) <- test e1 e2
- if not r then do
+ if not r then do
return (False, (m1, m2))
else do
(rs, model) <- testEquality (n-1) e1 e2
@@ -37,7 +36,7 @@ testEquality n e1 e2 = do
-- is used, and the model itself. If the formula, after substitution, cannot
-- be evaluated - i.e. there's still a variable in the LExpr - an error will be thrown.
testLExpr :: LExpr -> IO (LConst, EvalInfo)
-testLExpr e = do
+testLExpr e = do
let vs@(regularVs, (arrayVs, arrayOpVs), quantVs) = findVariables e
let isNullExprs = filter sIsnullExpr arrayOpVs
primitivesModel <- generateModel (regularVs ++ isNullExprs)
@@ -74,7 +73,7 @@ applyModel e evalInfo = foldLExpr algebra e
get arr model = do
let res = (M.lookup) arr model
- if res == Nothing then do
+ if res == Nothing then do
error $ "Bug in Test.hs made substitution of Array expression impossible. This should never happen. Array: " ++ show arr ++ ", ArrayModel: " ++ show model
[]
else do
diff --git a/src/LogicIR/Backend/API.hs b/src/LogicIR/Backend/Z3/API.hs
similarity index 94%
rename from src/LogicIR/Backend/API.hs
rename to src/LogicIR/Backend/Z3/API.hs
index 67fdae9..d6c8347 100644
--- a/src/LogicIR/Backend/API.hs
+++ b/src/LogicIR/Backend/Z3/API.hs
@@ -1,4 +1,4 @@
-module LogicIR.Backend.API where
+module LogicIR.Backend.Z3.API where
import Z3.Monad
import Z3.Opts
@@ -9,10 +9,10 @@ import Control.Monad.Trans (liftIO)
import Data.Maybe (fromJust)
import Data.Monoid ((<>))
-import LogicIR.Backend.Model
+import LogicIR.Backend.Z3.Model
-import LogicIR.Backend.Pretty (showRelevantModel)
-import LogicIR.Backend.Z3
+import LogicIR.Backend.Z3.Pretty (showRelevantModel)
+import LogicIR.Backend.Z3.Z3
import LogicIR.Expr (LExpr)
-- | Z3 Response type.
diff --git a/src/LogicIR/Backend/Model.hs b/src/LogicIR/Backend/Z3/Model.hs
similarity index 98%
rename from src/LogicIR/Backend/Model.hs
rename to src/LogicIR/Backend/Z3/Model.hs
index 78bcd68..cfa8ec6 100644
--- a/src/LogicIR/Backend/Model.hs
+++ b/src/LogicIR/Backend/Z3/Model.hs
@@ -1,6 +1,6 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
-module LogicIR.Backend.Model where
+module LogicIR.Backend.Z3.Model where
import Data.String
import System.IO.Unsafe (unsafePerformIO)
@@ -11,8 +11,6 @@ import Text.Parsec.Language
import Text.Parsec.String
import qualified Text.Parsec.Token as Tokens
-import Debug.Trace
-
data FuncInst = InstVal Integer ModelVal
| InstElse ModelVal
deriving (Show, Read, Eq, Ord)
diff --git a/src/LogicIR/Backend/Pretty.hs b/src/LogicIR/Backend/Z3/Pretty.hs
similarity index 97%
rename from src/LogicIR/Backend/Pretty.hs
rename to src/LogicIR/Backend/Z3/Pretty.hs
index 4d96c8f..7868b41 100644
--- a/src/LogicIR/Backend/Pretty.hs
+++ b/src/LogicIR/Backend/Z3/Pretty.hs
@@ -1,11 +1,12 @@
-module LogicIR.Backend.Pretty (showRelevantModel) where
+module LogicIR.Backend.Z3.Pretty (showRelevantModel) where
+
import Data.List
import Data.Maybe
import qualified Data.Map as M
import Z3.Monad
import Z3.Opts
-import LogicIR.Backend.Model
+import LogicIR.Backend.Z3.Model
-- | Function that shows a human-readable model and also highlights potential inconsistencies.
showRelevantModel :: Z3Model -> IO ()
diff --git a/src/LogicIR/Backend/Z3.hs b/src/LogicIR/Backend/Z3/Z3.hs
similarity index 98%
rename from src/LogicIR/Backend/Z3.hs
rename to src/LogicIR/Backend/Z3/Z3.hs
index e30794d..f03babc 100644
--- a/src/LogicIR/Backend/Z3.hs
+++ b/src/LogicIR/Backend/Z3/Z3.hs
@@ -1,5 +1,5 @@
{-# LANGUAGE OverloadedStrings #-}
-module LogicIR.Backend.Z3 where
+module LogicIR.Backend.Z3.Z3 where
import Z3.Monad
import Control.Monad.Trans (liftIO)
diff --git a/src/LogicIR/Eval.hs b/src/LogicIR/Eval.hs
index 939e89b..5fc82fc 100644
--- a/src/LogicIR/Eval.hs
+++ b/src/LogicIR/Eval.hs
@@ -10,7 +10,7 @@ eval :: LExpr -> LConst
eval = foldLExpr evalAlgebra
evalIfPossible :: LExpr -> LExpr
-evalIfPossible e = if evalPossible e then (LConst (eval e)) else e
+evalIfPossible e = if evalPossible e then LConst (eval e) else e
-- Returns True if an LExpr only contains constants and no variables whatsoever.
evalPossible :: LExpr -> Bool
@@ -33,21 +33,14 @@ evalAlgebra :: LExprAlgebra LConst
evalAlgebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
where cnst b@(CBool _) = b
cnst i@(CInt _) = i
-
uni NNeg (CInt i) = CInt (-i)
- uni NNot (CInt i) = CInt (-i - 1)
uni LNot (CBool b) = CBool (not b)
-
- bin le o re = evalBin le o re
-
- iff ge e1 e2 = if ge == (CBool True) then e1 else e2
-
+ bin = evalBin
+ iff ge e1 e2 = if ge == CBool True then e1 else e2
-- This possibly needs to be changed.
len v = CInt 10 -- error "Array length cannot yet be evaluated."
-
snull (Var (TPrim _) _) = CBool False -- Primitive type is never null.
snull (Var (TArray _) _) = error "You can't call eval on an LExpr that has an (LIsnull someArrayVar) that wasn't converted to a boolean first."
-
-- Things that should never happen.
quant _ _ e1 e2 = error "Quantifiers cannot be evaluated and should be replaced using LogicIR.Rewrite.replaceQuantifiers."
arr v a = error "You can't call eval on an LExpr that contains uninstantiated arrays."
@@ -61,9 +54,9 @@ evalBin (CInt l) CGreater (CInt r) = CBool (l > r)
-- Logical operators
evalBin (CBool l) LAnd (CBool r) = CBool (l && r)
evalBin (CBool l) LOr (CBool r) = CBool (l || r)
-evalBin (CBool l) LImpl (CBool r) = CBool ((not l) || (l && r))
+evalBin (CBool l) LImpl (CBool r) = CBool (not l || (l && r))
-- Numerical operators
-evalBin (CInt l) o (CInt r) = CInt ((convert o) l r)
+evalBin (CInt l) o (CInt r) = CInt (convert o l r)
-- Both NShr and NShl are evaluated using the Data.Bits.shift function,
-- where a right shift is achieved by inverting the r integer.
where convert NAdd = (+)
@@ -71,8 +64,3 @@ evalBin (CInt l) o (CInt r) = CInt ((convert o) l r)
convert NMul = (*)
convert NDiv = div
convert NRem = mod
- convert NShl = shiftL
- convert NShr = shiftR
- convert NAnd = (.&.)
- convert NOr = (.|.)
- convert NXor = xor
diff --git a/src/LogicIR/Pretty.hs b/src/LogicIR/Pretty.hs
index c24fb1f..10df1c7 100644
--- a/src/LogicIR/Pretty.hs
+++ b/src/LogicIR/Pretty.hs
@@ -7,7 +7,6 @@ import qualified Data.Map as M
import Z3.Monad
import Z3.Opts
-import LogicIR.Backend.Model
import LogicIR.Expr
import LogicIR.Fold
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index 518329c..db2c459 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -12,14 +12,12 @@ import Language.Java.Parser
import Language.Java.Pretty
import Language.Java.Syntax
-import qualified LogicIR.Backend.API as Z3
+import qualified LogicIR.Backend.Z3.API as Z3
import LogicIR.Expr
import LogicIR.Eval
-import LogicIR.Frontend.Java
-import LogicIR.Backend.Z3
-import LogicIR.Backend.Test
-import LogicIR.Backend.Pretty
-import LogicIR.Backend.Null
+import LogicIR.Backend.Z3.Z3
+import LogicIR.Backend.QuickCheck.Test
+import LogicIR.Backend.Z3.Pretty
import LogicIR.Frontend.Java (javaExpToLExpr)
import LogicIR.Null (lExprPreprocessNull)
@@ -98,5 +96,32 @@ extractExpr call = combineExprs $ map (\(MethodCall (Name [Ident _]) [a]) -> a)
combineExprs [e] = e
combineExprs (e:es) = e &* combineExprs es
-test9 = testSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec4") 1000
- where edslSrc = "examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
+parse :: (FilePath, String) -> (FilePath, String) -> IO (MethodDef, MethodDef)
+parse method1@(_, name1) method2@(_, name2) = do
+ -- load the methods
+ m1@(decls1, mbody1, env1) <- parseMethod method1
+ m2@(decls2, mbody2, env2) <- parseMethod method2
+ when (env1 /= env2) $ fail "inconsistent method parameters"
+ when (decls1 /= decls2) $ fail "inconsistent class declarations (TODO)"
+ return (m1, m2)
+
+methodDefToLExpr :: MethodDef -> MethodDef -> String -> (LExpr, LExpr)
+methodDefToLExpr m1@(decls1, _, env1) m2@(decls2, _, env2) name = do
+ -- get pre/post condition
+ let (e1, e2) = (extractCond m1 name, extractCond m2 name)
+ let (lExpr1', lExpr2') = (javaExpToLExpr e1 env1 decls1, javaExpToLExpr e2 env2 decls2)
+ -- preprocess "a == null" to "isNull(a)"
+ let (lExpr1, lExpr2) = (lExprPreprocessNull lExpr1', lExprPreprocessNull lExpr2')
+ (lExpr1, lExpr2)
+ where extractCond m n = extractExpr $ getMethodCalls m n
+
+testSpec :: (FilePath, String) -> (FilePath, String) -> Int -> IO Bool
+testSpec method1@(_, name1) method2@(_, name2) n = do
+ (m1, m2) <- parse method1 method2
+ putStrLn $ "----PRE---- (" ++ name1 ++ " vs " ++ name2 ++ ")"
+ let (lExpr1, lExpr2) = methodDefToLExpr m1 m2 "pre"
+ (preAns, counterModel) <- testEquality n lExpr1 lExpr2
+ putStrLn "\n----POST---"
+ let (lExpr1, lExpr2) = methodDefToLExpr m1 m2 "post"
+ (postAns, counterModel) <- testEquality n lExpr1 lExpr2
+ return $ preAns && postAns
diff --git a/test/Spec.hs b/test/Spec.hs
index 4b11dcc..d7ec9c8 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -13,6 +13,7 @@ main = defaultMain
("LIR_PARSER", parserTests)
, ("Z3_MODEL", modelTests)
, ("EXAMPLES", examples)
+ , ("AUTOMATED_TESTING_CHECK", testingModuleTests)
, ("EQUIV_REAL", genEquivTests "examples/test_equiv/Reals.java")
, ("EQUIV_ARRAY", genEquivTests "examples/test_equiv/Arrays.java")
]
diff --git a/test/TIRTest.hs b/test/TIRTest.hs
index 448e892..2270962 100644
--- a/test/TIRTest.hs
+++ b/test/TIRTest.hs
@@ -31,4 +31,4 @@ testingModuleTests =
, (neq "sorted3" "test2" 100)
, (neq "sorted3" "sorted4" 500)
, (neq "sorted1" "sorted4" 100)
- ]
\ No newline at end of file
+ ]
diff --git a/test/TZ3Model.hs b/test/TZ3Model.hs
index 7fb1298..9246154 100644
--- a/test/TZ3Model.hs
+++ b/test/TZ3Model.hs
@@ -3,8 +3,7 @@ import System.IO.Unsafe (unsafePerformIO)
import System.IO.Silently (silence)
import Test.HUnit
-import LogicIR.Backend.Model
-import Debug.Trace
+import LogicIR.Backend.Z3.Model
(~~) model ast = runP modelP model @?= ast
--
GitLab