diff --git a/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java b/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
index 4803c498ab49ac0acbbff62a7c1ccc7199db9f67..3c1a15a2d1fa11b6843e17b095898552f614291f 100644
--- a/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
+++ b/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
@@ -5,6 +5,12 @@ import static nl.uu.impress.EDSL.*;
public class Main {
+ public static void test1(int[] b) {
+ pre(~(-a * c) == (79 & 41));
+ pre(a * c > 0);
+ pre(exists(b, i -> b[i] > 0));
+ }
+
public static int simple_eval1() {
pre(~(-5 * 2) == (79 & 41)); // evaluates to 9 == 9
}
diff --git a/javawlp.cabal b/javawlp.cabal
index e4b516bfff6398273e1eb9592f59ee36c7134614..e1c975b1cc4e712f2448ceea3646dbdd5b5eb67b 100644
--- a/javawlp.cabal
+++ b/javawlp.cabal
@@ -31,6 +31,7 @@ library
, Language.Java.Syntax.Types
, SimpleFormulaChecker
build-depends: base >= 4.7 && < 5
+ , random
, parsec
, z3
, QuickCheck
diff --git a/src/LogicIR/Backend/QuickCheck.hs b/src/LogicIR/Backend/QuickCheck.hs
index 2505961d9cb61bff16fb6701d0f27e18fe0f6aa4..aac758369eebc0695448e263f04e99912c8e9a59 100644
--- a/src/LogicIR/Backend/QuickCheck.hs
+++ b/src/LogicIR/Backend/QuickCheck.hs
@@ -1,88 +1,144 @@
-module LogicIR.Backend.QuickCheck () where
+module LogicIR.Backend.QuickCheck (check) where
import LogicIR.Expr
import LogicIR.Fold
import LogicIR.Eval
+import LogicIR.Backend.Rewrite
+import LogicIR.Backend.Pretty
import Test.QuickCheck
-import Data.Maybe
-import Data.List (find)
+import Data.Maybe (fromMaybe)
+import Data.List (find, nub)
+import System.Random
import Control.Exception
-{-
+type Model = [(LExpr, LExpr)]
+empty :: Model
+empty = []
-This module checks whether two LExprs are equal in the following manner:
+-- Takes two LExprs as input. Generates a model for them, a tuple in
+-- which the first value indicates whether the two LExprs evaluate to
+-- the same boolean value when the generated model is used for substitution,
+-- and in which the second value is the generated model itself.
+check :: LExpr -> LExpr -> IO (Bool, Model)
+check e1 e2 = do
+ (result1, model) <- checkLExpr e1
+ let result2 = eval $ applyModel model $ replaceQuantifiers e2
+ return (result1 == result2, model)
-1. collect all currently known bounds of all variables in both LExprs
-2.
+-- Given an LExpr, generates a substitution model for all variables in it,
+-- and returns whether the formula evaluates to true or to false when that model
+-- 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.
+checkLExpr :: LExpr -> IO (LConst, Model)
+checkLExpr e = do
+ primitivesModel <- generateModel $ primitives
+ let primFreeE = applyModel primitivesModel quantFreeE
+ (finalE, arrayModel) <- repeatedApplyModel (primFreeE, empty)
+ let model = arrayModel ++ primitivesModel
+ let result = eval finalE
+ return $ (result, model)
+ where quantFreeE = replaceQuantifiers e
+ vars = findPrimitives quantFreeE
+ primitives = filter sPrim vars
+ sPrim (LVar (Var (TPrim _) _)) = True
+ sPrim _ = False
--}
+-- applies substitution of arrays until a "pure" LExpr is the result, or no
+-- more substitutions can be applied. If the latter is the case, an error
+-- will be thrown.
+repeatedApplyModel :: (LExpr, Model) -> IO (LExpr, Model)
+repeatedApplyModel (e, m) = do
+ if length arrays > 0 then
+ if length substitutableArrays > 0 then do
+ model <- generateModel substitutableArrays
+ let newE = applyModel model e
+ repeatedApplyModel (newE, m ++ model)
+ else
+ error $ "There are unsubstitutable array accesses: " ++ (show arrays)
+ else
+ return (e, m)
+ where arrays = findArrays e
+ substitutableArrays = filter sSubstitutable arrays
+ -- An array access a[i] is substitutable if the indexer
+ -- i doesn't contain variables.
+ sSubstitutable (LArray var e) = evalPossible e
----- Tells, given a formula and a list of ranges for all variables in the formula,
----- whether the formula evaluates to true or to false.
---check :: LExpr -> [(Var, LExpr, LExpr)] -> LExpr
---check e [] = e
---check e varBounds = do
--- let purelyBoundedVar = fstPureBounds varBounds
--- let t@(v, mn, mx) = if isJust purelyBoundedVar
--- then fromJust purelyBoundedVar
--- else head varBounds
--- value <- choose (mn,mx)
--- where randomVal = 1
--- cnst _ = []
--- var v = [v]
--- uni _ a = a
--- bin a1 _ a2 = a1 ++ a2
--- iff a1 a2 a3 = a1 ++ a2 ++ a3
--- quant _ _ a1 a2 = a1 ++ a2
--- arr v a = v : a
--- snull v = [v]
--- len v = [v]
+-- Applies substitution given a Model and an LExpr.
+applyModel :: Model -> LExpr -> LExpr
+applyModel model = foldLExpr algebra
+ where algebra :: LExprAlgebra LExpr
+ algebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
+ cnst c = LConst c
+ uni op e = evalIfPossible $ LUnop op e
+ bin le op re = evalIfPossible $ LBinop le op re
+ iff ge e1 e2 = evalIfPossible $ LIf ge e1 e2
+ var v = substitute (LVar v) model
+ quant _ _ e1 e2 = error "applyModel expects a quantifier-free LExpr."
+ arr v e = substitute (LArray v e) model
+ snull v = LIsnull v
+ len v = LLen v
--- Returns the first tuple in the given list that has pure bounds, i.e.
--- both the minimum and maximum contain no variables.
---fstPurelyBounded :: [(Var, LExpr, LExpr)] -> Maybe (Var, LExpr, LExpr)
---fstPurelyBounded ranges = find pureBound ranges
--- where pureBound (_, mn, mx) = (evalPossible mn) && (evalPossible mx)
+-- Substitutes an LExpr if a valid substitute can be found in the given list.
+substitute :: LExpr -> Model -> LExpr
+substitute v model = fromMaybe v (fmap snd $ find (\(old,new) -> v == old) model)
+-- Generates a constant value for all vars vars in the given list.
+generateModel :: [LExpr] -> IO Model
+generateModel exprs = mapM generateModelEntry exprs
+
+-- Generates an entry for the substitution Model for a given LExpr.
+generateModelEntry :: LExpr -> IO (LExpr, LExpr)
+generateModelEntry e@(LVar (Var (TPrim t) _)) = do
+ generateValue t >>= \v -> return (e, v)
+generateModelEntry e@(LArray (Var (TArray (TPrim t)) _) _) = do
+ generateValue t >>= \v -> return (e, v)
---getInstance :: (Var, LExpr, LExpr) -> LExpr
---getInstance ((Var t s), mn, mx)
+-- Generates a random LExpr of a certain Primitive type.
+generateValue :: Primitive -> IO LExpr
+generateValue t = do
+ v <- getStdRandom (randomR $ (0, 1))
+ return $ toLExpr t v
--- Replaces all occurences in the secon argument of the first tuple argument
--- with the second tuple argument, e.g.
--- substitute ("x", 5) "x + y" = "5 + y"
---substitute :: (LExpr, LExpr) -> LExpr -> Bool
---substitute t e = foldLExpr (substituteAlgebra t)
+-- Returns the bounds within which a random value should be generated for
+-- some type primitive type.
+bounds :: Primitive -> (Int, Int)
+bounds PBool = (0, 1)
+bounds PInt32 = (-10, 10)
---substituteAlgebra :: (LExpr, LExpr) -> LExprAlgebra Bool
---substituteAlgebra (old, new) = (cnst, var, uni, bin, iff, quant, arr, snull, len)
--- where cnst c = subst (LConst c)
--- uni op e = LUnop op (subst e)
--- bin le op re = LBinop (subst le) op (subst re)
--- iff ge e1 e2 = LIf (subst ge) (subst e1) (subst e2)
--- var v = subst (LVar v)
--- quant op v a1 a2 = LQuant op (subst (LVar v)) (subst a1) (subst a2)
--- arr v a = subst (LArray (subst (LVar v)) (subst a))
--- snull v = subst (LVar v)
--- len v = subst (LVar v)
+-- 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
--- subVar v = if (LVar v) == old then new else (LVar v)
--- subst e = if e == old then new else e
+-- Returns a list with all Vars in the LExpr.
+findPrimitives :: LExpr -> [LExpr]
+findPrimitives expr = nub $ foldLExpr algebra expr
+ where algebra :: LExprAlgebra [LExpr]
+ algebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
+ cnst _ = []
+ uni _ e = e
+ bin le _ re = le ++ re
+ iff ge e1 e2 = ge ++ e1 ++ e2
+ var v = [LVar v]
+ quant _ _ e1 e2 = error "findPrimitives expects a quantifier-free LExpr."
+ arr v e = e
+ snull v = [LVar v]
+ len v = [LVar v]
----- Returns the minimum and maximum range, expressed in LExprs, for
----- every LVar in the given LExpr
---findRanges :: LExpr -> [Var] -> [(LExpr, LExpr, LExpr)]
---findRanges e = []
-
----- Returns a list with all LVar's that appear in a given LExpr.
---variables :: LExpr -> [Var]
---variables = foldLExpr (cnst, var, uni, bin, iff, quant, arr, snull, len)
--- where cnst _ = []
--- var v = [v]
--- uni _ a = a
--- bin a1 _ a2 = a1 ++ a2
--- iff a1 a2 a3 = a1 ++ a2 ++ a3
--- quant _ _ a1 a2 = a1 ++ a2
--- arr v a = v : a
--- snull v = [v]
--- len v = [v]
\ No newline at end of file
+-- Returns a list with all LArrays in the LExpr.
+findArrays :: LExpr -> [LExpr]
+findArrays expr = nub $ arrs
+ where (arrs,_) = foldLExpr algebra expr
+ algebra :: LExprAlgebra ([LExpr], LExpr)
+ algebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
+ cnst c = ([], LConst c)
+ uni op e = (fst e, LUnop op (snd e))
+ bin le op re = (fst le ++ fst re, LBinop (snd le) op (snd re))
+ iff ge e1 e2 = (fst ge ++ fst e1 ++ fst e2, LIf (snd ge) (snd e1) (snd e2))
+ var v = error "findArrays expects an LVar-free LExpr"
+ quant _ _ e1 e2 = error "findArrays expects a quantifier-free LExpr."
+ arr v e = do
+ let array = LArray v (snd e)
+ (array : (fst e), array)
+ snull v = ([], LVar v)
+ len v = ([], LVar v)
diff --git a/src/LogicIR/Backend/Rewrite.hs b/src/LogicIR/Backend/Rewrite.hs
new file mode 100644
index 0000000000000000000000000000000000000000..e426f9a43d7915f67c648cf61c091a7d07921818
--- /dev/null
+++ b/src/LogicIR/Backend/Rewrite.hs
@@ -0,0 +1,51 @@
+module LogicIR.Backend.Rewrite (replaceQuantifiers) where
+
+import LogicIR.Expr
+import LogicIR.Fold
+import LogicIR.Backend.Pretty
+
+
+-- Expands quantifiers in given LExpr and returns a quantifier free LExpr.
+replaceQuantifiers :: LExpr -> LExpr
+replaceQuantifiers = foldLExpr replaceQuantifiersAlgebra
+
+replaceQuantifiersAlgebra :: LExprAlgebra LExpr
+replaceQuantifiersAlgebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
+ where cnst = LConst
+ uni = LUnop
+ bin = LBinop
+ iff = LIf
+ var = LVar
+ quant t v d e = replaceQuantifier t v d e
+ arr = LArray
+ snull = LIsnull
+ len = LLen
+
+-- replaces an LQuant with a conjunction (if universal) or disjunction (if
+-- existential). In the second argument of the con/disjunct, the quantifier Var
+-- is replaced by Var'. This makes it possible to just substitute both of them
+-- with a value in the end. Since Java identifiers can't contain the ' char,
+-- we can safely assume that Varname ++ ' is always a fresh identifier.
+replaceQuantifier :: QOp -> Var -> LExpr -> LExpr -> LExpr
+replaceQuantifier op var domain e = LBinop e1 combiner e2
+ where prime (Var t name) = Var t (name ++ "'")
+ e1 = LBinop domain LAnd e
+ e2 = replace var (prime var) (LBinop domain LAnd e)
+ combiner = if op == QAll then LAnd else LOr
+
+-- Returns an LExpr where all occurences of vOld in the given LExpr are
+-- replaced by vNew.
+replace :: Var -> Var -> LExpr -> LExpr
+replace vOld vNew = foldLExpr algebra
+ where algebra :: LExprAlgebra LExpr
+ algebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
+ subst v = if v == vOld then vNew else v
+ cnst c = LConst c
+ uni o c = LUnop o c
+ bin le o re = LBinop le o re
+ iff ge e1 e2 = LIf ge e1 e2
+ var v = LVar (subst v)
+ quant t v d e = replaceQuantifier t v d e
+ arr v e = LArray (subst v) e
+ snull v = LIsnull (subst v)
+ len v = LLen (subst v)
diff --git a/src/LogicIR/Eval.hs b/src/LogicIR/Eval.hs
index 93aec1ebcd9dfc51d0cbf7aa2cea7841c1b6b0af..e9f9eeede5492f5a26f922a0aede6a03ba3c72d0 100644
--- a/src/LogicIR/Eval.hs
+++ b/src/LogicIR/Eval.hs
@@ -1,4 +1,4 @@
-module LogicIR.Eval (eval, evalPossible) where
+module LogicIR.Eval (eval, evalPossible, evalIfPossible) where
import LogicIR.Expr
import LogicIR.Fold
@@ -6,6 +6,13 @@ import LogicIR.Backend.Pretty
import Data.Bits
+-- Tells to which LConst a given LExpr evaluates.
+eval :: LExpr -> LConst
+eval = foldLExpr evalAlgebra
+
+evalIfPossible :: LExpr -> LExpr
+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
evalPossible = foldLExpr evalPossibleAlgebra
@@ -19,12 +26,8 @@ evalPossibleAlgebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
var v = False
quant _ _ a1 a2 = a1 && a2
arr v a = False
- snull v = False
- len v = False
-
--- Tells to which LConst a given LExpr evaluates.
-eval :: LExpr -> LConst
-eval = foldLExpr evalAlgebra
+ snull v = True -- This possibly needs to be changed. See evalAlgebra
+ len v = True -- This possibly needs to be changed. See evalAlgebra
evalAlgebra :: LExprAlgebra LConst
evalAlgebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
@@ -38,12 +41,15 @@ evalAlgebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
bin le o re = evalBin le o re
iff ge e1 e2 = if ge == (CBool True) then e1 else e2
- -- TODO.
- var v = error "You can't call eval on an LExpr that contains vars"
- quant _ _ a1 a2 = error "Quantifiers cannot yet be evaluated."
- arr v a = error "Arrays cannot yet be evaluated"
- snull v = error "Null checks cannot yet be evaluated"
- len v = error "Array length cannot yet be evaluated"
+
+ -- This possibly needs to be changed.
+ snull v = CBool False -- error "Null checks cannot yet be evaluated."
+ len v = CInt 10 -- error "Array length cannot yet be evaluated."
+
+ -- 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 contain eval on an LExpr that contains uninstantiated arrays."
+ var v = error "You can't call eval on an LExpr that contains uninstantiated vars."
-- Evaluates a binary operator expression.
-- Comparison operators
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index ed0de20cf8dd54a54344e2319041763d78aec368..8297ec2f22ae9a0ce5a411d8c71f5ab635e41068 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -14,7 +14,7 @@ import LogicIR.Expr
import LogicIR.Eval
import LogicIR.Frontend.Java
import LogicIR.Backend.Z3
---import LogicIR.Backend.QuickCheck
+import LogicIR.Backend.QuickCheck
import LogicIR.Backend.Pretty
import LogicIR.Backend.Null
@@ -220,11 +220,19 @@ compareSpec method1@(_, name1) method2@(_, name2) = do
postAns <- determineFormulaEq m1 m2 "post"
return $ preAns && postAns
-evaluate :: (FilePath, String) -> IO (Bool, Maybe Bool)
+quickCheckTest = do
+ (result, model) <- LogicIR.Backend.QuickCheck.check e e
+ putStrLn $ "Expressions are equal: " ++ (show result)
+ putStrLn $ "Model used: " ++ (show model)
+ return ()
+ where e = LBinop (LBinop (LUnop NNot (LBinop (LUnop NNeg (LVar (Var (TPrim PInt32) "a"))) NMul (LVar (Var (TPrim PInt32) "c")))) CEqual (LBinop (LConst (CInt 79)) NAnd (LConst (CInt 41)))) LAnd (LBinop (LBinop (LBinop (LVar (Var (TPrim PInt32) "a")) NMul (LVar (Var (TPrim PInt32) "c"))) CGreater (LConst (CInt 0))) LAnd (LQuant QAny (Var (TPrim PInt32) "i") (LBinop (LBinop (LVar (Var (TPrim PInt32) "i")) CGreater (LConst (CInt 0))) LAnd (LBinop (LVar (Var (TPrim PInt32) "i")) CLess (LLen (Var (TArray (TPrim PInt32)) "b")))) (LBinop (LArray (Var (TArray (TPrim PInt32)) "b") (LVar (Var (TPrim PInt32) "i"))) CEqual (LVar (Var (TPrim PInt32) "retval")))))
+
+evaluate :: String -> IO (Bool, Maybe Bool)
evaluate method = do
- m@(decls, mbody, env) <- parseMethod method
+ m@(decls, mbody, env) <- parseMethod ("examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java", method)
let e = extractExpr (getMethodCalls m "pre")
let lexpr = javaExpToLExpr e env decls
+ putStrLn (show lexpr)
putStrLn (prettyLExpr lexpr)
let t = CBool True
let possible = LogicIR.Eval.evalPossible lexpr