From 4f188800ab88da00a403e61352cb8c43b1081dc3 Mon Sep 17 00:00:00 2001
From: Joris ten Tusscher <joristt@gmail.com>
Date: Tue, 16 Jan 2018 12:21:03 +0100
Subject: [PATCH] =?UTF-8?q?-=20Fixed=20QuickCheck=20bugs,=20it=20works=20o?=
=?UTF-8?q?n=2015/16=20tests=20now.=20-=20Added=20correct=20handling=20of?=
=?UTF-8?q?=20LIsnull=20in=20QuickCheck.=20-=20Fixed=20a=20bug=20in=20Rewr?=
=?UTF-8?q?ite.hs=20that=20wasn=E2=80=99t=20causing=20issues=20yet,=20but?=
=?UTF-8?q?=20was=20a=20bug=20nonetheless.=20-=20Sped=20up=20QuickCheck=20?=
=?UTF-8?q?tests=20by=20making=20the=20number=20of=20iterations=20dependen?=
=?UTF-8?q?t=20on=20the=20specific=20test.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/LogicIR/Backend/QuickCheck.hs | 22 +++++++++-------
src/LogicIR/Backend/Rewrite.hs | 4 +--
src/LogicIR/Eval.hs | 23 +++++++++-------
src/SimpleFormulaChecker.hs | 5 ++++
test/TIRQuickCheck.hs | 44 +++++++++++++++----------------
5 files changed, 55 insertions(+), 43 deletions(-)
diff --git a/src/LogicIR/Backend/QuickCheck.hs b/src/LogicIR/Backend/QuickCheck.hs
index ffe475b..8fa73fa 100644
--- a/src/LogicIR/Backend/QuickCheck.hs
+++ b/src/LogicIR/Backend/QuickCheck.hs
@@ -62,17 +62,14 @@ check e1 e2 = do
-- 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
+ --putStrLn $ (show $ findPrimitives quantFreeE)
+ primitivesModel <- generateModel $ findPrimitives quantFreeE
let primFreeE = applyModel primitivesModel quantFreeE
(finalE, arrayModel) <- repeatedApplyAndExpandModel (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
+ where quantFreeE = replaceQuantifiers e
-- 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
@@ -114,7 +111,7 @@ applyModel model = foldLExpr algebra
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
+ snull v = substitute (LIsnull v) model
len v = LLen v
-- Substitutes an LExpr if a valid substitute can be found in the given list.
@@ -131,6 +128,11 @@ 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)
+generateModelEntry e@(LIsnull (Var (TArray _) _)) = do
+ generateValue PBool >>= \v -> return (e, v)
+generateModelEntry e = do
+ error $ "Cannot generate model entry for " ++ show e
+ return (e, e)
-- Generates a random LExpr of a certain Primitive type.
generateValue :: Primitive -> IO LExpr
@@ -151,7 +153,7 @@ toLExpr PInt32 v = LConst $ CInt $ v
-- Returns a list with all Vars in the LExpr.
findPrimitives :: LExpr -> [LExpr]
-findPrimitives expr = nub $ foldLExpr algebra expr
+findPrimitives expr = filter isPrim $ nub $ foldLExpr algebra expr
where algebra :: LExprAlgebra [LExpr]
algebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
cnst _ = []
@@ -161,8 +163,10 @@ findPrimitives expr = nub $ foldLExpr algebra expr
var v = [LVar v]
quant _ _ e1 e2 = error "findPrimitives expects a quantifier-free LExpr."
arr v e = e
- snull v = [LVar v]
+ snull v = [LIsnull v]
len v = [LVar v]
+ isPrim (LVar (Var (TArray _) _)) = False
+ isPrim _ = True
-- Returns a list with all LArrays in the LExpr.
findArrays :: LExpr -> [LExpr]
diff --git a/src/LogicIR/Backend/Rewrite.hs b/src/LogicIR/Backend/Rewrite.hs
index e426f9a..7762ed5 100644
--- a/src/LogicIR/Backend/Rewrite.hs
+++ b/src/LogicIR/Backend/Rewrite.hs
@@ -29,8 +29,8 @@ replaceQuantifiersAlgebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
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)
+ e1 = LBinop domain LImpl e
+ e2 = replace var (prime var) (LBinop domain LImpl e)
combiner = if op == QAll then LAnd else LOr
-- Returns an LExpr where all occurences of vOld in the given LExpr are
diff --git a/src/LogicIR/Eval.hs b/src/LogicIR/Eval.hs
index d274afa..a60393b 100644
--- a/src/LogicIR/Eval.hs
+++ b/src/LogicIR/Eval.hs
@@ -19,15 +19,16 @@ evalPossible = foldLExpr evalPossibleAlgebra
evalPossibleAlgebra :: LExprAlgebra Bool
evalPossibleAlgebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
- where cnst _ = True
- uni _ c = c
- bin le _ re = le && re
- iff ge e1 e2 = ge && e1 && e2
- var v = False
- quant _ _ a1 a2 = a1 && a2
- arr v a = False
- snull v = True -- This possibly needs to be changed. See evalAlgebra
- len v = True -- This possibly needs to be changed. See evalAlgebra
+ where cnst _ = True
+ uni _ c = c
+ bin le _ re = le && re
+ iff ge e1 e2 = ge && e1 && e2
+ var v = False
+ quant _ _ a1 a2 = a1 && a2
+ arr v a = False
+ snull (Var (TPrim _) _) = True -- Primitive type is never null.
+ snull (Var (TArray _) _) = False
+ len v = True -- This possibly needs to be changed. See evalAlgebra
evalAlgebra :: LExprAlgebra LConst
evalAlgebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
@@ -43,9 +44,11 @@ evalAlgebra = (cnst, var, uni, bin, iff, quant, arr, snull, len)
iff ge e1 e2 = if ge == (CBool True) then e1 else e2
-- 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."
+ 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."
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index 535992e..4582599 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -245,3 +245,8 @@ testSpec method1@(_, name1) method2@(_, name2) n = do
let (lExpr1, lExpr2) = methodDefToLExpr m1 m2 "post"
postAns <- testEquality n lExpr1 lExpr2
return $ preAns && postAns
+
+-- The legendary 16th test that causes an endless loop in Z3 and that gives
+-- incorrect test results in the case of QuickCheck.
+test16 = testSpec (edslSrc, "sorted1") (edslSrc, "sorted4") 10000
+ where edslSrc = "examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
diff --git a/test/TIRQuickCheck.hs b/test/TIRQuickCheck.hs
index 5336c43..da62964 100644
--- a/test/TIRQuickCheck.hs
+++ b/test/TIRQuickCheck.hs
@@ -8,27 +8,27 @@ import SimpleFormulaChecker
edslSrc = "examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
-testEquiv :: Bool -> String -> String -> Assertion
-testEquiv b s s' =
- unsafePerformIO (silence $ testSpec (edslSrc, s) (edslSrc, s') 100000) @?= b
-(.==) = testEquiv True
-(.!=) = testEquiv False
+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
quickCheckTests =
- [ "swap_spec1" .== "swap_spec1"
- , "swap_spec1" .!= "swap_spec2"
- , "getMax_spec1" .!= "getMax_spec2"
- , "test1" .!= "test2"
- , "blob1" .== "blob1"
- , "test1_" .!= "test2"
- , "null1" .!= "null2"
- , "swap_spec1" .!= "swap_spec3"
- , "swap_spec1" .!= "swap_spec4"
- , "null3" .!= "test2"
- , "sorted1" .!= "test2"
- , "sorted1" .!= "sorted2"
- , "sorted1".!= "sorted3"
- , "test2" .!= "sorted3"
- , "sorted3" .!= "sorted4"
- , "sorted1" .== "sorted4"
- ]
+ [ (eq "swap_spec1" "swap_spec1" 10)
+ , (neq "swap_spec1" "swap_spec2" 10)
+ , (neq "getMax_spec1" "getMax_spec2" 1000)
+ , (neq "test1" "test2" 10)
+ , (eq "blob1" "blob1" 10)
+ , (neq "test1_" "test2" 10)
+ , (neq "null1" "null2" 10)
+ , (neq "swap_spec1" "swap_spec3" 10)
+ , (neq "swap_spec1" "swap_spec4" 100)
+ , (neq "null3" "test2" 10)
+ , (neq "sorted1" "test2" 10)
+ , (neq "sorted1" "sorted2" 1000)
+ , (neq "sorted1" "sorted3" 1000)
+ , (neq "test2" "sorted3" 10)
+ , (neq "sorted3" "sorted4" 1000)
+ , (eq "sorted1" "sorted4" 1000)
+ ]
\ No newline at end of file
--
GitLab