From 903de2617119e4e38f16f4f426afb2c485072650 Mon Sep 17 00:00:00 2001
From: Joris ten Tusscher <joristt@gmail.com>
Date: Sun, 4 Feb 2018 21:17:42 +0100
Subject: [PATCH] Some cleanup, added null check functionality on arrays.
Test.hs correctly tests all 16 examples now.
---
src/LogicIR/Backend/Test.hs | 21 ++++++++++-----------
src/SimpleFormulaChecker.hs | 5 -----
test/TIRTest.hs | 4 ++--
3 files changed, 12 insertions(+), 18 deletions(-)
diff --git a/src/LogicIR/Backend/Test.hs b/src/LogicIR/Backend/Test.hs
index 9d5c876..facb844 100644
--- a/src/LogicIR/Backend/Test.hs
+++ b/src/LogicIR/Backend/Test.hs
@@ -44,9 +44,6 @@ testEquality 0 e1 e2 = do
testEquality n e1 e2 = do
(r,m1,m2) <- test e1 e2
if not r then do
- putStrLn $ show r
- putStrLn $ show m1
- putStrLn $ show m2
return (False, (m1, m2))
else do
(rs, model) <- testEquality (n-1) e1 e2
@@ -59,11 +56,14 @@ testEquality n e1 e2 = do
testLExpr :: LExpr -> IO (LConst, EvalInfo)
testLExpr e = do
let vs@(regularVs, (arrayVs, arrayOpVs), quantVs) = findVariables e
- primitivesModel <- generateModel regularVs
+ let isNullExprs = filter sIsnullExpr arrayOpVs
+ primitivesModel <- generateModel (regularVs ++ isNullExprs)
arrayModel <- generateArrayModel arrayVs
testResult <- testModel e (primitivesModel, arrayModel, quantVs)
let evalInfo = (primitivesModel, arrayModel, quantVs)
return (testResult, evalInfo)
+ where sIsnullExpr (LIsnull _) = True
+ sIsnullExpr _ = False
testModel :: LExpr -> EvalInfo -> IO LConst
testModel e evalInfo = do
@@ -120,9 +120,13 @@ subst q@(LQuant qop v domain e) evalInfo = do
q
else
LConst $ CBool $ op $ map fromJust results
-subst (LIsnull v) (_,arrayModel,_) = LConst (CBool (0 == length (tr arrayModel v)))
subst (LLen v) (_,arrayModel,_) = LConst (CInt (length (tr arrayModel v)))
subst v (model,_,_) = fromMaybe v (fmap snd $ find (\(old,new) -> v == old) model)
+-- Note that firstly, LIsnull can only be applied to arrays since ints/bools cannot be null in Java,
+-- secondly, LIsnull is not substituted based on the actual value of the array in the
+-- ArrayModel. Instead, it's just a random bool that is present in the primitives model.
+-- 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...
-- Returns, given a domain LExpr that concerns a certain Var, all
-- Ints that fall in that domain.
@@ -136,8 +140,6 @@ evalQuantifier v domain e (m1,m2,quantVs) = do
getResult newM1 = do
let newEvalInfo = (newM1,m2,quantVs)
let newDomain = applyModel domain newEvalInfo
- --let !x = unsafePerformIO $ putStrLn $ prettyLExpr domain
- --let !x = unsafePerformIO $ putStrLn $ prettyLExpr newDomain ++ "\n"
if evalPossible newDomain then
if isTrue newDomain then do
let newE = applyModel e newEvalInfo
@@ -184,11 +186,8 @@ generateModelEntry e@(LVar (Var (TPrim t) _)) = do
generatePrimitive t >>= \v -> return (e, v)
generateModelEntry e@(LIsnull (Var (TArray _) _)) = do
generatePrimitive PBool >>= \v -> return (e, v)
-generateModelEntry e = do
+generateModelEntry e =
error $ "Cannot generate model entry for " ++ show e
- return (e, e)
---generateModelEntry e@(LArray (Var (TArray (TPrim t)) _) _) = do
- --generatePrimitive t >>= \v -> return (e, v)
generatePrimitive :: Primitive -> IO LExpr
generatePrimitive t = generatePrimitiveWithBounds t (bounds t)
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index f9439f5..393dfb4 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -245,11 +245,6 @@ testSpec method1@(_, name1) method2@(_, name2) n = do
putStrLn "\n----POST---"
let (lExpr1, lExpr2) = methodDefToLExpr m1 m2 "post"
(postAns, counterModel) <- testEquality n lExpr1 lExpr2
-
- appendFile "results.txt" (name1 ++ ", " ++ name2 ++ "\n")
- appendFile "results.txt" ("Pre condition equality counter model: " ++ (show counterModel) ++ "\n")
- appendFile "results.txt" ("Post condition equality counter model: " ++ (show counterModel) ++ "\n")
-
return $ preAns && postAns
test9 = testSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec4") 1000
diff --git a/test/TIRTest.hs b/test/TIRTest.hs
index 8e16ff6..448e892 100644
--- a/test/TIRTest.hs
+++ b/test/TIRTest.hs
@@ -23,8 +23,8 @@ testingModuleTests =
, (neq "test1_" "test2" 100)
, (neq "null1" "null2" 100)
, (neq "swap_spec1" "swap_spec3" 100)
- , (neq "swap_spec1" "swap_spec4" 100) --9
- , (neq "null3" "test2" 1000) --10
+ , (neq "swap_spec1" "swap_spec4" 100)
+ , (neq "null3" "test2" 1000)
, (neq "sorted1" "test2" 100)
, (neq "sorted1" "sorted2" 500)
, (neq "sorted1" "sorted3" 100)
--
GitLab