From 5e27d5b96bd08186b34731782b0cd61d3ae46676 Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Tue, 6 Feb 2018 13:59:37 +0100
Subject: [PATCH] Model pretty-pretting (revisited)
---
.../src/nl/uu/javawlp_edsl/Main.java | 8 +-
examples/model.txt | 7 -
javawlp.cabal | 3 +-
src/LogicIR/Backend/Z3/API.hs | 80 ++++++---
src/LogicIR/Backend/Z3/Model.hs | 106 +++++------
src/LogicIR/Backend/Z3/Pretty.hs | 78 --------
src/LogicIR/Backend/Z3/Z3.hs | 169 ++++++++++--------
src/LogicIR/Fold.hs | 6 +-
src/LogicIR/Frontend/Java.hs | 2 +-
src/SimpleFormulaChecker.hs | 5 +-
test/Spec.hs | 4 +-
test/TEquivalenceClasses.hs | 5 +-
test/TExamples.hs | 7 +-
test/TIRTest.hs | 36 ++--
test/TModelParser.hs | 15 ++
test/TZ3Model.hs | 57 ------
16 files changed, 244 insertions(+), 344 deletions(-)
delete mode 100644 examples/model.txt
delete mode 100644 src/LogicIR/Backend/Z3/Pretty.hs
create mode 100644 test/TModelParser.hs
delete mode 100644 test/TZ3Model.hs
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 785bb97..9383714 100644
--- a/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
+++ b/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
@@ -198,13 +198,15 @@ public class Main {
System.out.println("Hello, world!");
}
- public static void arr1(int[] a) {
- pre(true);
+ public static void arr1(double[] a) {
+ pre(a.length == 2 && forall(a, i -> forallr(a, i, a.length, j -> a[i] <= a[j])));
post(true);
}
public static void arr2(double[] a) {
- pre(forallr(a, 0, a.length - 1, i -> a[i] <= a[i + 1]));
+ // pre(a.length == 2);
+ // pre(forall(a, i -> forallr(a, i, a.length, j -> a[j] >= a[i])));
+ pre(a.length == 2 && forall(a, i -> forallr(a, i+1, a.length, j -> a[i] < a[j] + 1)));
post(true);
}
}
diff --git a/examples/model.txt b/examples/model.txt
deleted file mode 100644
index 81c08c7..0000000
--- a/examples/model.txt
+++ /dev/null
@@ -1,7 +0,0 @@
-a?length -> 2
-i!0 -> 1
-a -> (_ as-array k!1)
-k!1 -> {
- 1 -> (- 2)
- else -> (- 2)
-}
diff --git a/javawlp.cabal b/javawlp.cabal
index eb917c3..9d5d226 100644
--- a/javawlp.cabal
+++ b/javawlp.cabal
@@ -34,7 +34,6 @@ library
, 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
@@ -64,7 +63,7 @@ test-suite javawlp-tests
, TIRParser
, TIRTest
, TEquivalenceClasses
- , TZ3Model
+ , TModelParser
build-depends: base
, javawlp
, test-framework
diff --git a/src/LogicIR/Backend/Z3/API.hs b/src/LogicIR/Backend/Z3/API.hs
index d6c8347..f26f978 100644
--- a/src/LogicIR/Backend/Z3/API.hs
+++ b/src/LogicIR/Backend/Z3/API.hs
@@ -3,41 +3,33 @@ module LogicIR.Backend.Z3.API where
import Z3.Monad
import Z3.Opts
+import Data.String
import Control.Exception.Base (tryJust)
-import Control.Monad (when, forM_)
+import Control.Monad (forM, forM_, when)
import Control.Monad.Trans (liftIO)
import Data.Maybe (fromJust)
import Data.Monoid ((<>))
+import qualified Data.Map as M
+import LogicIR.Expr (LExpr)
import LogicIR.Backend.Z3.Model
-
-import LogicIR.Backend.Z3.Pretty (showRelevantModel)
import LogicIR.Backend.Z3.Z3
-import LogicIR.Expr (LExpr)
-- | Z3 Response type.
-data Z3Response = Equivalent | NotEquivalent (Maybe String) | Timeout | Undefined
+data Z3Response = Equivalent | NotEquivalent Z3Model | Timeout | Undefined
-- | Determine the equality of two method's pre/post conditions.
equivalentTo :: LExpr -> LExpr -> IO Z3Response
equivalentTo lexpr lexpr' = do
- let (ast1, ast2) = (lExprToZ3Ast lexpr, lExprToZ3Ast lexpr')
- ast1s <- showZ3AST ast1
- ast2s <- showZ3AST ast2
- putStrLn $ "Z3_AST1:\n" ++ ast1s ++ "\n\nZ3_AST2:\n" ++ ast2s ++ "\n"
- res <- tryJust errorSelector (ast1 `equivalentToZ3` ast2)
+ let fv = freeVars2 lexpr lexpr'
+ let (ast, ast') = (lExprToZ3Ast lexpr, lExprToZ3Ast lexpr')
+ asts <- showZ3AST ast
+ asts' <- showZ3AST ast'
+ -- putStrLn $ "Z3_AST1:\n" ++ asts ++ "\n\nZ3_AST2:\n" ++ asts' ++ "\n"
+ res <- tryJust errorSelector $ equivalentToZ3 fv ast ast'
case res of
Left () -> return Timeout
- Right (result, model) ->
- case result of
- Unsat -> return Equivalent
- Undef -> return Undefined
- Sat -> do modelStr <- tryZ3 $ showModel $ fromJust model
- putStrLn $ "\nModel:\n" ++ modelStr
- case runP' modelP modelStr of
- Left err -> putStrLn $ "Cannot parse model:\n" ++ show err
- Right m -> showRelevantModel m
- return $ NotEquivalent (Just modelStr)
+ Right r -> return r
where
errorSelector :: Z3Error -> Maybe ()
errorSelector err =
@@ -52,9 +44,11 @@ equivalentTo lexpr lexpr' = do
andThenTactic tt tt'
-- | Check if two Z3 AST's are equivalent.
-equivalentToZ3 :: Z3 AST -> Z3 AST -> IO (Result, Maybe Model)
-equivalentToZ3 ast1' ast2' =
+equivalentToZ3 :: Z3 FreeVars -> Z3 AST -> Z3 AST -> IO Z3Response
+equivalentToZ3 freeVars ast1' ast2' =
tryZ3 $ do
+ fv <- freeVars
+ -- liftIO $ putStr "FreeVars: " >> print (M.keys fv)
ast1 <- ast1'
ast2 <- ast2'
astEq <- mkEq ast1 ast2
@@ -66,16 +60,46 @@ equivalentToZ3 ast1' ast2' =
t <- "qe" --> "aig"
a <- applyTactic t g
asts <- getGoalFormulas =<< getApplyResultSubgoal a 0
- liftIO $ putStrLn "After tactics:"
- astStrs <- mapM astToString asts
- forM_ astStrs (liftIO . putStrLn)
+ -- liftIO $ putStrLn "After tactics:"
+ -- astStrs <- mapM astToString asts
+ -- forM_ astStrs (liftIO . putStrLn)
g' <- mkAnd asts
assert g'
-- assert astNeq
- r <- solverCheckAndGetModel -- check in documentation
- solverReset
- return r
+ (r, model) <- solverCheckAndGetModel -- check in documentation
+
+ case r of
+ Unsat -> return Equivalent
+ Undef -> return Undefined
+ Sat -> do
+ let m = fromJust model
+ ms <- M.fromList <$> forM (M.toList fv) (evalAST fv m)
+ let ms' = sanitize ms
+ liftIO $ putStr "Model: " >> print ms'
+ return $ NotEquivalent ms'
+ -- solverReset
+ where evalAST :: FreeVars -> 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 = evalZ3With Nothing ( opt "timeout" (5000 :: Integer)
diff --git a/src/LogicIR/Backend/Z3/Model.hs b/src/LogicIR/Backend/Z3/Model.hs
index cfa8ec6..943585f 100644
--- a/src/LogicIR/Backend/Z3/Model.hs
+++ b/src/LogicIR/Backend/Z3/Model.hs
@@ -2,91 +2,71 @@
{-# LANGUAGE OverloadedStrings #-}
module LogicIR.Backend.Z3.Model where
+import qualified Data.Map as M
+
import Data.String
-import System.IO.Unsafe (unsafePerformIO)
-import Text.Parsec
+import Text.Parsec hiding (runP)
import Text.Parsec.Char
import Text.Parsec.Expr
import Text.Parsec.Language
import Text.Parsec.String
import qualified Text.Parsec.Token as Tokens
-data FuncInst = InstVal Integer ModelVal
- | InstElse ModelVal
- deriving (Show, Read, Eq, Ord)
-
data ModelVal = BoolVal Bool
| IntVal Integer
| RealVal Double
- | ArrayRef String
- | ArrayFunc [FuncInst]
- deriving (Read, Eq, Ord)
+ | ManyVal [ModelVal]
+ deriving (Eq)
-type Z3Model = [(String, ModelVal)]
+type Z3Model = M.Map String ModelVal
+emptyZ3Model = M.empty :: Z3Model
instance Show ModelVal where
- show (BoolVal b) = show b
- show (IntVal i) = show i
- show (RealVal i) = show i
- show (ArrayRef s) = s
- show (ArrayFunc fs) = show fs
+ show (BoolVal b) = show b
+ show (IntVal i) = show i
+ show (RealVal i) = show i
+ show (ManyVal vs) = show vs
+
+-- | Crop arrays until their specified length.
+sanitize :: Z3Model -> Z3Model
+sanitize model = M.mapWithKey f model
+ where f k (ManyVal array) = ManyVal $ take (counts k) array
+ f _ x = x
+ counts k = fromInteger $
+ case model M.! (k ++ "?length") of
+ (IntVal i) -> i
+ _ -> error "non-int length"
+
+-- | Implicit conversion from strings.
+instance IsString ModelVal where
+ fromString = runP modelP
-- | Parser.
runP :: Parser a -> String -> a
-runP p s = unsafePerformIO $
+runP p s =
case runParser (p <* eof) () "" s of
- Left err -> fail $ show err
- Right lExp -> return lExp
-
-runP' :: Parser a -> String -> Either ParseError a
-runP' p = runParser (p <* eof) () ""
-
-modelP :: Parser Z3Model
-modelP = many1 (lexeme asgP)
-
-asgP :: Parser (String, ModelVal)
-asgP = do
- identifier <- idP <~ "->"
- val <- valP
- return (identifier, val)
-
-valP :: Parser ModelVal
-valP = try (parens valP)
- <|> try (ArrayFunc <$> funcP)
- <|> try (ArrayRef <$> arrP)
- <|> try (RealVal <$> realP)
- <|> try (IntVal <$> intP)
- <|> (BoolVal <$> boolP)
-
-funcP :: Parser [FuncInst]
-funcP = "{" ~> many1 funcInstP <~ "}"
-
-arrP :: Parser String
-arrP = "(_ as-array" ~> idP <~ ")"
-
-funcInstP :: Parser FuncInst
-funcInstP = try instElse
- <|> try instVal
- <|> instConst
- where instVal = do
- i <- (indexP <~ "->") <?> "index"
- v <- valP <?> "val"
- return $ InstVal i v
- instElse = do
- v <- "else ->" ~> valP
- return $ InstElse v
- instConst = InstElse <$> valP
+ Left err -> error $ show err
+ Right r -> r
-idP :: Parser String
-idP = many1 (letter <|> digit <|> oneOf ['!', '?'])
+modelP :: Parser ModelVal
+modelP = try (BoolVal <$> boolP)
+ <|> try (RealVal <$> realP)
+ <|> (IntVal <$> intP)
realP :: Parser Double
-realP = negRealP <|> Tokens.float haskell
- where negRealP = do v <- "-" ~> Tokens.float haskell
- return (-v)
+realP = try negRealP <|> try divRealP <|> Tokens.float haskell
+ where divRealP = do
+ v <- "(/" ~> realP
+ v' <- realP <~ ")"
+ return $ v / v'
+ negRealP = do
+ v <- "(-" ~> realP <~ ")"
+ return $ -v
intP :: Parser Integer
-intP = Tokens.integer haskell
+intP = try negIntP <|> Tokens.integer haskell
+ where negIntP = do v <- "(-" ~> intP <~ ")"
+ return $ -v
indexP :: Parser Integer
indexP = Tokens.natural haskell
diff --git a/src/LogicIR/Backend/Z3/Pretty.hs b/src/LogicIR/Backend/Z3/Pretty.hs
deleted file mode 100644
index 7868b41..0000000
--- a/src/LogicIR/Backend/Z3/Pretty.hs
+++ /dev/null
@@ -1,78 +0,0 @@
-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.Z3.Model
-
--- | Function that shows a human-readable model and also highlights potential inconsistencies.
-showRelevantModel :: Z3Model -> IO ()
-showRelevantModel model = do
- putStrLn "Pretty model:"
- mapM_ (putStrLn . prettyModelVal) $ fromKeys (consts ++ arrays)
- where modelMap :: M.Map String ModelVal
- modelMap = M.fromList model
- modelClean :: M.Map String ModelVal
- modelClean = M.filterWithKey (\k _ -> '!' `notElem` k) $ M.map modelCleanFunc modelMap
- fromKeys :: [String] -> [(String, ModelVal)]
- fromKeys = map (\k -> let v = M.findWithDefault defaultArray k modelClean in (k, v))
- defaultArray :: ModelVal
- defaultArray = ArrayFunc [InstElse $ IntVal (-111)] -- nullTest2
- -- Pretty print the model value
- prettyModelVal :: (String, ModelVal) -> String
- prettyModelVal (k, BoolVal b) = k ++ " = " ++ if b then "true" else "false"
- prettyModelVal (k, IntVal n) = k ++ " = " ++ show n
- prettyModelVal (k, RealVal n) = k ++ " = " ++ show n
- prettyModelVal (k, ArrayFunc a) = k ++ " = " ++ final ++ " " -- ++ show (aNull, aLength, a, arrKv, elseVal, length (buildArray 0))
- where (BoolVal aNull) = M.findWithDefault (BoolVal False) (k ++ "?null") modelClean
- (IntVal aLength) = M.findWithDefault (IntVal (-1)) (k ++ "?length") modelClean
- [InstElse elseVal] = filter (not . isInst) a
- arrKv :: [(Integer, ModelVal)]
- arrKv = filter (\(k, v) -> v /= elseVal) (sort (map (\(InstVal k v) -> (k, v)) (filter isInst a)))
- isInst :: FuncInst -> Bool
- isInst (InstVal _ v) = True
- isInst _ = False
- isValidArray :: Bool
- isValidArray = null arrKv || (minIndex >= 0 && maxIndex <= aLength)
- where minIndex = minimum indices
- maxIndex = maximum indices
- indices = map fst arrKv
- arrMap :: M.Map Integer ModelVal
- arrMap = M.fromList arrKv
- buildArray :: Integer -> [ModelVal]
- buildArray i = if aLength == 0 then [] else M.findWithDefault elseVal i arrMap : if i + 1 == aLength || i + 1 > 100 then [] else buildArray (i + 1)
- final :: String
- final | aNull = "null"
- | isValidArray = show (buildArray 0) ++ if aLength > 100 then " (TRUNCATED, length: " ++ show aLength ++ ")" else "" --let xs = buildArray 0 in if length xs > 100 then show (take 100 xs) ++ " (TRUNCATED)" else show xs
- | otherwise = "inconsistent array representation" -- blub2
- -- Remove all occurrences of ArrayRef and ArrayAsConst for easier processing later, also does type casting
- modelCleanFunc :: ModelVal -> ModelVal
- modelCleanFunc (ArrayRef s) = let Just v = M.lookup s modelMap in v
- -- modelCleanFunc (ArrayAsConst n) = ArrayFunc [InstElse n]
- modelCleanFunc x = x
- -- Names of the array variables
- arrays :: [String]
- arrays = nub $ M.keys (M.filter isArray modelClean) ++ mapMaybe arrayName (M.keys modelClean)
- -- Names of the constant variables
- consts :: [String]
- consts = filter (\v -> not (isSuffixOf "?length" v || isSuffixOf "?null" v)) $ M.keys (M.filter isConst modelClean)
- -- Returns Just "a" for "a?length" and "a?null"
- arrayName :: String -> Maybe String
- arrayName s
- | "?length" `isSuffixOf` s = Just $ take (length s - 7) s
- | "?null" `isSuffixOf` s = Just $ take (length s - 5) s
- | otherwise = Nothing
- -- Whether a ModelVal is an array
- isArray :: ModelVal -> Bool
- isArray (ArrayFunc _) = True
- isArray _ = False
- -- Whether a ModelVal is a constant
- isConst :: ModelVal -> Bool
- isConst v = case v of
- BoolVal _ -> True
- IntVal _ -> True
- RealVal _ -> True
- _ -> False
diff --git a/src/LogicIR/Backend/Z3/Z3.hs b/src/LogicIR/Backend/Z3/Z3.hs
index f03babc..6d5ea09 100644
--- a/src/LogicIR/Backend/Z3/Z3.hs
+++ b/src/LogicIR/Backend/Z3/Z3.hs
@@ -1,8 +1,9 @@
{-# LANGUAGE OverloadedStrings #-}
module LogicIR.Backend.Z3.Z3 where
-import Z3.Monad
import Control.Monad.Trans (liftIO)
+import qualified Data.Map as M
+import Z3.Monad
import LogicIR.Expr
import LogicIR.Fold
@@ -11,80 +12,98 @@ import LogicIR.Parser
lExprToZ3Ast :: LExpr -> Z3 AST
lExprToZ3Ast = foldLExpr lExprToZ3AstAlgebra
--- TODO: support more types
lExprToZ3AstAlgebra :: LExprAlgebra (Z3 AST)
-lExprToZ3AstAlgebra = (fConst, fVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull, fLen) where
- fConst c = case c of
- 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)"
- fVar (Var t n) =
- mkStringSymbol n >>=
- case t of
- "int" -> mkIntVar
- "bool" -> mkBoolVar
- "real" -> mkRealVar
- "[int]" -> mkIntArrayVar
- "[real]" -> mkRealArrayVar
- "[bool]" -> mkBoolArrayVar
- _ -> error $ "unsupported type: " ++ show t
- fUnop o a' = do
- a <- a'
- case o of
- NNeg -> mkUnaryMinus a
- LNot -> mkNot a
- fBinop a' o b' = do
- a <- a'
- b <- b'
- case o of
- NAdd -> mkAdd [a, b]
- NSub -> mkSub [a, b]
- NMul -> mkMul [a, b]
- NDiv -> mkDiv a b
- NRem -> mkRem a b
- LAnd -> mkAnd [a, b]
- LOr -> mkOr [a, b]
- LImpl -> mkImplies a b
- CEqual -> mkEq a b
- CLess -> mkLt a b
- CGreater -> mkGt a b
- fIf c' a' b' = do
- c <- c'
- a <- a'
- b <- b'
- mkIte c a b
- fQuant o v@(Var t n) d' a' = do
- a <- a'
- d <- d'
- case t of
- "int" -> do
- vApp <- fVar v >>= toApp
- case o of
- QAll -> do e <- mkImplies d a
- mkForallConst [] [vApp] e
- QAny -> do e <- mkAnd [d, a]
- mkExistsConst [] [vApp] e
- _ -> error $ "unsupported quantifier domain type: " ++ show (o, v)
- fArray v a' = do
- v <- fVar v
- a <- a'
- mkSelect v a
- fIsnull (Var (TArray _) n) = mkStringSymbol (n ++ "?null") >>= mkBoolVar
- fLen (Var (TArray _) n) = mkStringSymbol (n ++ "?length") >>= mkIntVar -- TODO: support proper array lengths
+lExprToZ3AstAlgebra =
+ (fConst, genVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull, fLen) where
+ fConst c = case c of
+ 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)"
+ fUnop o a' = do
+ a <- a'
+ case o of
+ NNeg -> mkUnaryMinus a
+ LNot -> mkNot a
+ fBinop a' o b' = do
+ a <- a'
+ b <- b'
+ case o of
+ NAdd -> mkAdd [a, b]
+ NSub -> mkSub [a, b]
+ NMul -> mkMul [a, b]
+ NDiv -> mkDiv a b
+ NRem -> mkRem a b
+ LAnd -> mkAnd [a, b]
+ LOr -> mkOr [a, b]
+ LImpl -> mkImplies a b
+ CEqual -> mkEq a b
+ CLess -> mkLt a b
+ CGreater -> mkGt a b
+ fIf c' a' b' = do
+ c <- c'
+ a <- a'
+ b <- b'
+ mkIte c a b
+ fQuant o v@(Var t n) d' a' = do
+ a <- a'
+ d <- d'
+ case t of
+ "int" -> do
+ vApp <- genVar v >>= toApp
+ case o of
+ QAll -> do e <- mkImplies d a
+ mkForallConst [] [vApp] e
+ QAny -> do e <- mkAnd [d, a]
+ mkExistsConst [] [vApp] e
+ _ -> error $ "unsupported quantifier domain type: " ++ show (o, v)
+ fArray v a' = do
+ v <- genVar v
+ a <- a'
+ mkSelect v a
+ fIsnull (Var (TArray _) n) = genNullVar n
+ fLen (Var (TArray _) n) = genLenVar n -- TODO: support proper array lengths
-mkArrayVar :: Z3 Sort -> Symbol -> Z3 AST
-mkArrayVar mkValSort symbol = do
- intSort <- mkIntSort
- valSort <- mkValSort
- arraySort <- mkArraySort intSort valSort
- mkVar symbol arraySort
-mkRealArrayVar = mkArrayVar mkRealSort
-mkIntArrayVar = mkArrayVar mkIntSort
-mkBoolArrayVar = mkArrayVar mkBoolSort
+-- | Get formula's free variables (to be included in model).
+type FreeVars = M.Map String AST
+freeVars2 :: LExpr -> LExpr -> Z3 FreeVars
+freeVars2 l l' = M.unions <$> mapM (foldLExpr freeVarsAlgebra) [l, l']
+freeVars :: LExpr -> Z3 FreeVars
+freeVars = foldLExpr freeVarsAlgebra
+freeVarsAlgebra :: LExprAlgebra (Z3 FreeVars)
+freeVarsAlgebra =
+ (fConst, fVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull, fLen) where
+ fConst _ = return M.empty
+ fVar v@(Var t n) = M.singleton n <$> genVar v
+ fUnop _ r = r
+ fBinop r _ r' = M.unions <$> sequence [r, r']
+ fIf r r' r'' = M.unions <$> sequence [r, r', r'']
+ fQuant _ (Var _ n) d r = M.unions . fmap (M.delete n) <$> sequence [r, d]
+ fArray v _ = M.unions <$> sequence [fIsnull v, fLen v, fVar v]
+ fIsnull (Var (TArray _) n) = M.singleton (n ++ "?null") <$> genNullVar n
+ fLen (Var (TArray _) n) = M.singleton (n ++ "?length") <$> genLenVar n
-getSorts :: AST -> AST -> Z3 (String, String)
-getSorts a b = do
- as <- getSort a
- bs <- getSort b
- return (show as, show bs)
+-- | Generate a new Z3 variable, depending on the expression's type.
+genVar :: Var -> Z3 AST
+genVar (Var t n) =
+ mkStringSymbol n >>=
+ case t of
+ "int" -> mkIntVar
+ "bool" -> mkBoolVar
+ "real" -> mkRealVar
+ "[int]" -> mkIntArrayVar
+ "[real]" -> mkRealArrayVar
+ "[bool]" -> mkBoolArrayVar
+ _ -> error $ "unsupported type: " ++ show t
+ where mkArrayVar mkValSort symbol = do
+ intSort <- mkIntSort
+ valSort <- mkValSort
+ arraySort <- mkArraySort intSort valSort
+ mkVar symbol arraySort
+ mkRealArrayVar = mkArrayVar mkRealSort
+ mkIntArrayVar = mkArrayVar mkIntSort
+ mkBoolArrayVar = mkArrayVar mkBoolSort
+genNullVar :: String -> Z3 AST
+genNullVar s = genVar $ Var "bool" (s ++ "?null")
+genLenVar :: String -> Z3 AST
+genLenVar s = genVar $ Var "int" (s ++ "?length")
diff --git a/src/LogicIR/Fold.hs b/src/LogicIR/Fold.hs
index fb9f4c3..82acb89 100644
--- a/src/LogicIR/Fold.hs
+++ b/src/LogicIR/Fold.hs
@@ -2,7 +2,7 @@ module LogicIR.Fold where
import LogicIR.Expr
--- Fold algebra for logical expressions
+-- | Fold algebra for logical expressions.
type LExprAlgebra r = (LConst -> r, -- LConst
Var -> r, -- LVar
LUnop -> r -> r, -- LUnop
@@ -14,7 +14,7 @@ type LExprAlgebra r = (LConst -> r, -- LConst
Var -> r -- LLen
)
--- Fold for logical expressions
+-- | Fold for logical expressions.
foldLExpr :: LExprAlgebra r -> LExpr -> r
foldLExpr (fConst, fVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull, fLen) = fold where
fold e = case e of
@@ -26,4 +26,4 @@ foldLExpr (fConst, fVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull, fLen) = fo
LQuant o b d a -> fQuant o b (fold d) (fold a)
LArray v a -> fArray v (fold a)
LIsnull v -> fIsnull v
- LLen v -> fLen v
\ No newline at end of file
+ LLen v -> fLen v
diff --git a/src/LogicIR/Frontend/Java.hs b/src/LogicIR/Frontend/Java.hs
index 42cb2a4..1706600 100644
--- a/src/LogicIR/Frontend/Java.hs
+++ b/src/LogicIR/Frontend/Java.hs
@@ -95,7 +95,7 @@ javaExpToLExprAlgebra =
"existsr" -> lquantr QAny i begin end expr
_ -> error $ "Unimplemented fMethodInv: " ++ show inv
lquantr op i begin end expr =
- LQuant op i (LBinop (v i .> begin) LAnd (LBinop (LVar i) CLess end)) (refold expr)
+ LQuant op i (LBinop (v i .>= begin) LAnd (LBinop (LVar i) CLess end)) (refold expr)
refold expr =
foldExp javaExpToLExprAlgebra expr env decls
fArrayAccess arrayIndex env decls =
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index db2c459..a61b8aa 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -16,16 +16,17 @@ import qualified LogicIR.Backend.Z3.API as Z3
import LogicIR.Expr
import LogicIR.Eval
import LogicIR.Backend.Z3.Z3
+import LogicIR.Backend.Z3.Model
import LogicIR.Backend.QuickCheck.Test
-import LogicIR.Backend.Z3.Pretty
import LogicIR.Frontend.Java (javaExpToLExpr)
import LogicIR.Null (lExprPreprocessNull)
import LogicIR.Pretty (prettyLExpr)
-- | Response type.
-data Response = Equivalent | NotEquivalent (Maybe String) | Undefined | Timeout
+data Response = Equivalent | NotEquivalent Z3Model | Undefined | Timeout
deriving (Eq, Show)
+
(<>) :: Response -> Response -> Response
Equivalent <> r = r
NotEquivalent s <> _ = NotEquivalent s
diff --git a/test/Spec.hs b/test/Spec.hs
index d7ec9c8..5442f1c 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -5,14 +5,14 @@ import TExamples
import TIRParser
import TIRTest
import TEquivalenceClasses
-import TZ3Model
+import TModelParser
main = defaultMain
[ constructTestSuite testName testSuite
| (testName, testSuite) <- [
("LIR_PARSER", parserTests)
- , ("Z3_MODEL", modelTests)
, ("EXAMPLES", examples)
+ , ("MODEL_PARSER", modelParserTests)
, ("AUTOMATED_TESTING_CHECK", testingModuleTests)
, ("EQUIV_REAL", genEquivTests "examples/test_equiv/Reals.java")
, ("EQUIV_ARRAY", genEquivTests "examples/test_equiv/Arrays.java")
diff --git a/test/TEquivalenceClasses.hs b/test/TEquivalenceClasses.hs
index b3ee8d4..ace7572 100644
--- a/test/TEquivalenceClasses.hs
+++ b/test/TEquivalenceClasses.hs
@@ -9,16 +9,17 @@ import System.IO.Unsafe (unsafePerformIO)
import Test.HUnit
import Javawlp.Engine.HelperFunctions (parseMethodIds)
+import LogicIR.Backend.Z3.Model
import SimpleFormulaChecker
testEquiv :: Response -> String -> String -> String -> Assertion
testEquiv b src s s' =
(case unsafePerformIO (silence $ compareSpec (src, s) (src, s')) of
- NotEquivalent x -> NotEquivalent Nothing
+ NotEquivalent x -> NotEquivalent emptyZ3Model
x -> x
) @?= b
(.==) = testEquiv Equivalent
-(.!=) = testEquiv $ NotEquivalent Nothing
+(.!=) = testEquiv $ NotEquivalent emptyZ3Model
genEquivTests edslSrc =
let methodIds = unsafePerformIO (silence $ parseMethodIds edslSrc)
diff --git a/test/TExamples.hs b/test/TExamples.hs
index b95861f..6359785 100644
--- a/test/TExamples.hs
+++ b/test/TExamples.hs
@@ -3,6 +3,7 @@ import System.IO.Unsafe (unsafePerformIO)
import System.IO.Silently (silence)
import Test.HUnit
+import LogicIR.Backend.Z3.Model
import SimpleFormulaChecker
src = "examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
@@ -10,11 +11,11 @@ src = "examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
testEquiv :: Response -> String -> String -> Assertion
testEquiv b s s' =
(case unsafePerformIO (silence $ compareSpec (src, s) (src, s')) of
- NotEquivalent _ -> NotEquivalent Nothing
+ NotEquivalent _ -> NotEquivalent emptyZ3Model
x -> x
) @?= b
(.==) = testEquiv Equivalent
-(.!=) = testEquiv $ NotEquivalent Nothing
+(.!=) = testEquiv $ NotEquivalent emptyZ3Model
(.??) = testEquiv Timeout
examples =
@@ -35,5 +36,5 @@ examples =
, "sorted1".!= "sorted3"
, "test2" .!= "sorted3"
, "sorted3" .!= "sorted4"
- , "sorted1" .!= "sorted4"
+ , "sorted1" .== "sorted4"
]
diff --git a/test/TIRTest.hs b/test/TIRTest.hs
index 2270962..d3de368 100644
--- a/test/TIRTest.hs
+++ b/test/TIRTest.hs
@@ -11,24 +11,24 @@ edslSrc = "examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
testEquiv :: Bool -> String -> String -> Int -> Assertion
testEquiv b s s' n =
unsafePerformIO (silence $ testSpec (edslSrc, s) (edslSrc, s') n) @?= b
-eq s s' n = testEquiv True s s' n
-neq s s' n = testEquiv False s s' n
+eq = testEquiv True
+neq = testEquiv False
testingModuleTests =
- [ (eq "swap_spec1" "swap_spec1" 100)
- , (neq "swap_spec1" "swap_spec2" 100)
- , (neq "getMax_spec1" "getMax_spec2" 500)
- , (neq "test1" "test2" 100)
- , (eq "blob1" "blob1" 100)
- , (neq "test1_" "test2" 100)
- , (neq "null1" "null2" 100)
- , (neq "swap_spec1" "swap_spec3" 100)
- , (neq "swap_spec1" "swap_spec4" 100)
- , (neq "null3" "test2" 1000)
- , (neq "sorted1" "test2" 100)
- , (neq "sorted1" "sorted2" 500)
- , (neq "sorted1" "sorted3" 100)
- , (neq "sorted3" "test2" 100)
- , (neq "sorted3" "sorted4" 500)
- , (neq "sorted1" "sorted4" 100)
+ [ eq "swap_spec1" "swap_spec1" 100
+ , neq "swap_spec1" "swap_spec2" 100
+ , neq "getMax_spec1" "getMax_spec2" 500
+ , neq "test1" "test2" 100
+ , eq "blob1" "blob1" 100
+ , neq "test1_" "test2" 100
+ , neq "null1" "null2" 100
+ , neq "swap_spec1" "swap_spec3" 100
+ , neq "swap_spec1" "swap_spec4" 100
+ , neq "null3" "test2" 1000
+ , neq "sorted1" "test2" 100
+ , neq "sorted1" "sorted2" 500
+ , neq "sorted1" "sorted3" 100
+ , neq "sorted3" "test2" 100
+ , neq "sorted3" "sorted4" 500
+ , eq "sorted1" "sorted4" 100
]
diff --git a/test/TModelParser.hs b/test/TModelParser.hs
new file mode 100644
index 0000000..2dd03d2
--- /dev/null
+++ b/test/TModelParser.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE OverloadedStrings #-}
+module TModelParser where
+import Test.HUnit
+
+import Data.String
+import LogicIR.Backend.Z3.Model
+
+modelParserTests =
+ [ "true" @?= BoolVal True
+ , "false" @?= BoolVal False
+ , "1" @?= IntVal 1
+ , "1.0" @?= RealVal 1.0
+ , "(- 1.0)" @?= RealVal (-1.0)
+ , "(- (/ 1.0 2.0))" @?= RealVal (-0.5)
+ ]
diff --git a/test/TZ3Model.hs b/test/TZ3Model.hs
deleted file mode 100644
index 9246154..0000000
--- a/test/TZ3Model.hs
+++ /dev/null
@@ -1,57 +0,0 @@
-module TZ3Model where
-import System.IO.Unsafe (unsafePerformIO)
-import System.IO.Silently (silence)
-import Test.HUnit
-
-import LogicIR.Backend.Z3.Model
-
-(~~) model ast = runP modelP model @?= ast
-
-modelTests =
- [ "a?length -> 2 \n\
- \ i!0 -> 1 \n\
- \ a -> (_ as-array k!1) \n\
- \ k!1 -> { \n\
- \ 1 -> (- 2) \n\
- \ else -> (- 2) \n\
- \ }" ~~
- [ ("a?length", IntVal 2)
- , ("i!0", IntVal 1)
- , ("a", ArrayRef "k!1")
- , ("k!1", ArrayFunc [ InstVal 1 $ IntVal (-2)
- , InstElse $ IntVal (-2)
- ])
- ]
- , "a?length -> 3 \n\
- \ i!0 -> 1 \n\
- \ a -> (_ as-array k!2) \n\
- \ j!1 -> 2 \n\
- \ k!2 -> { \n\
- \ 2 -> 1.0 \n\
- \ else -> 1.0 \n\
- \ }" ~~
- [ ("a?length", IntVal 3)
- , ("i!0", IntVal 1)
- , ("a", ArrayRef "k!2")
- , ("j!1", IntVal 2)
- , ("k!2", ArrayFunc [ InstVal 2 $ RealVal 1.0
- , InstElse $ RealVal 1.0
- ])
- ]
- , "a?length -> 3 \n\
- \ i!0 -> 1 \n\
- \ a -> (_ as-array k!2) \n\
- \ j!1 -> 2 \n\
- \ k!2 -> { \n\
- \ 2 -> (- 2.0) \n\
- \ else -> (- 2.0) \n\
- \ }" ~~
- [ ("a?length", IntVal 3)
- , ("i!0", IntVal 1)
- , ("a", ArrayRef "k!2")
- , ("j!1", IntVal 2)
- , ("k!2", ArrayFunc [ InstVal 2 $ RealVal (-2.0)
- , InstElse $ RealVal (-2.0)
- ])
- ]
- ]
--
GitLab