From 6e24b29c0ad0a916aec04dd3602fbadd55c60f24 Mon Sep 17 00:00:00 2001
From: Orestis Melkonian <melkon.or@gmail.com>
Date: Sun, 4 Mar 2018 15:24:25 +0100
Subject: [PATCH] Tests: fix
---
src/API.hs | 10 +++++-----
src/LogicIR/Backend/QuickCheck/API.hs | 20 ++++++++------------
test/TEquivalenceClasses.hs | 8 ++++----
test/TExamples.hs | 8 ++++----
4 files changed, 21 insertions(+), 25 deletions(-)
diff --git a/src/API.hs b/src/API.hs
index 125d1f1..81a3f59 100644
--- a/src/API.hs
+++ b/src/API.hs
@@ -71,15 +71,15 @@ compareSpec m pMode methodA methodB = do
mv1 <- newEmptyMVar
mv2 <- if m == Debug then newEmptyMVar else return mv1
- mapM_ (compareSpecHelper mv1) [ ("Z3", Z3.equivalentTo)
- , ("Test", Test.equivalentTo)
- ]
+ mapM_ compareSpecHelper [ (mv1, "Z3", Z3.equivalentTo)
+ , (mv2, "Test", Test.equivalentTo)
+ ]
res1 <- readMVar mv1
res2 <- readMVar mv2 -- if Release, this won't block
return $ getRes m res1 res2
where -- | Runs f on a separate thread and stores the result in mv.
- compareSpecHelper mv (name, impl) = forkIO $ do
- res <- checkSpec name impl (preL, preL') (postL, postL')
+ compareSpecHelper (mv, name, impl) = forkIO $ do
+ res <- checkSpec name impl (preL, preL') (postL, postL')
res `seq` putMVar mv res
-- | Makes sure that both Responses are the same, otherwise, if we
diff --git a/src/LogicIR/Backend/QuickCheck/API.hs b/src/LogicIR/Backend/QuickCheck/API.hs
index b6c9196..7e7d233 100644
--- a/src/LogicIR/Backend/QuickCheck/API.hs
+++ b/src/LogicIR/Backend/QuickCheck/API.hs
@@ -1,6 +1,6 @@
module LogicIR.Backend.QuickCheck.API (equivalentTo) where
-import Control.Arrow (second)
+import Control.Arrow ((***))
import Data.Map (Map)
import qualified Data.Map.Lazy as M
import Data.Maybe (fromJust, fromMaybe, isNothing)
@@ -16,17 +16,13 @@ equivalentTo lexpr lexpr' = do
(eq, testModel) <- testEquality 1000 lexpr lexpr'
if eq
then return Equivalent
- else return $ NotEquivalent $ toModel testModel
+ else return $ NotEquivalent $ toZ3Model testModel
-toModel :: (QC.Model, QC.ArrayModel) -> Model
-toModel (m, arrayM) = do
- let arrayKeys = map LVar $ M.keys arrayM
- let arrayVals = map (map LConst) $ M.elems arrayM
- let arrayKVs = zip arrayKeys (map toModelVals arrayVals)
- let modelKVs = map (second toModelVal) m
- let model = arrayKVs ++ modelKVs
- M.fromList $ map makePretty model
- where makePretty (k,v) = (prettyLExpr k, v)
+toZ3Model :: (QC.Model, QC.ArrayModel) -> Model
+toZ3Model (m, arrayM) =
+ M.fromList $
+ map (prettyLExpr *** toModelVal) m ++
+ map ((prettyLExpr *** toModelVals) . (LVar *** fmap LConst)) (M.toList arrayM)
toModelVal :: LExpr -> ModelVal
toModelVal (LConst (CBool b)) = BoolVal b
@@ -34,4 +30,4 @@ toModelVal (LConst (CInt i)) = IntVal $ toInteger i
toModelVal (LConst (CReal r)) = RealVal r
toModelVals :: [LExpr] -> ModelVal
-toModelVals es@(x:xs) = ManyVal $ map toModelVal es
+toModelVals = ManyVal . map toModelVal
diff --git a/test/TEquivalenceClasses.hs b/test/TEquivalenceClasses.hs
index ed07077..855d1f2 100644
--- a/test/TEquivalenceClasses.hs
+++ b/test/TEquivalenceClasses.hs
@@ -14,11 +14,11 @@ import Javawlp.Engine.HelperFunctions (parseMethodIds)
import Model
testEquiv :: Response -> String -> String -> String -> Assertion
-testEquiv b src s s' =
- (case unsafePerformIO (hSilence [stdout, stderr] $ compareSpec Debug File (src, s) (src, s')) of
+testEquiv b src s s' = do
+ res <- hSilence [stdout, stderr] $ compareSpec Debug File (src, s) (src, s')
+ (case res of
NotEquivalent x -> NotEquivalent emptyModel
- x -> x
- ) @?= b
+ x -> x) @?= b
(.==) = testEquiv Equivalent
(.!=) = testEquiv $ NotEquivalent emptyModel
diff --git a/test/TExamples.hs b/test/TExamples.hs
index 30ff8b5..6a03032 100644
--- a/test/TExamples.hs
+++ b/test/TExamples.hs
@@ -10,11 +10,11 @@ import Model
src = "examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java"
testEquiv :: Response -> String -> String -> Assertion
-testEquiv b s s' =
- (case unsafePerformIO (hSilence [stdout, stderr] $ compareSpec Debug File (src, s) (src, s')) of
+testEquiv b s s' = do
+ res <- hSilence [stdout, stderr] $ compareSpec Debug File (src, s) (src, s')
+ (case res of
NotEquivalent _ -> NotEquivalent emptyModel
- x -> x
- ) @?= b
+ x -> x) @?= b
(.==) = testEquiv Equivalent
(.!=) = testEquiv $ NotEquivalent emptyModel
(.??) = testEquiv Timeout
--
GitLab