Added test iterations heuristic, added threading in LogicIR.Backend.Test

javawlp.cabal

@@ -42,6 +42,7 @@ library
                      , LogicIR.Backend.QuickCheck.API
                      , LogicIR.Backend.QuickCheck.Test
                      , LogicIR.Backend.QuickCheck.ModelGenerator
+                     , LogicIR.Backend.QuickCheck.Iterations
   build-depends:       base >= 4.7 && < 5
                      , random
                      , parsec
@@ -70,6 +71,7 @@ library
                      , lens
                      , deepseq
                      , language-java ==0.2.9
+                     , async
   default-language:    Haskell2010
   ghc-options:         -Wall
 

src/LogicIR/Backend/QuickCheck/API.hs

@@ -6,12 +6,14 @@ import qualified LogicIR.Backend.QuickCheck.ModelGenerator as QC
 import           LogicIR.Backend.QuickCheck.Test
 import           LogicIR.Expr                              hiding (b,r,n)
 import           LogicIR.Pretty                            (prettyLExpr)
+import           LogicIR.Backend.QuickCheck.Iterations     (iterations)
 import           Model
 
 -- | Determine the equality of two method's pre/post conditions.
 equivalentTo :: LExprTeacher -> LExprStudent -> IO Response
 equivalentTo lexpr lexpr' = do
-    (feedbackCount, counterModel) <- testEquality 500 lexpr lexpr'
+    let iters = max (iterations lexpr) (iterations lexpr')
+    (feedbackCount, counterModel) <- testEquality iters lexpr lexpr'
     if equal feedbackCount then
       return Equivalent
     else do

src/LogicIR/Backend/QuickCheck/Iterations.hs

+-- | Module used to calculate the complexity of an LExpr.
+module LogicIR.Backend.QuickCheck.Iterations (iterations) where
+
+import LogicIR.Expr
+import LogicIR.Fold
+import LogicIR.Normalizer
+
+-- | Calculates the probability that, given a random model generated by
+--   ModelGenerator, the LExpr evaluates to true.
+iterations :: LExpr -> Int
+iterations e = min 500 (foldLExpr algebra (skolemize e))
+
+  where algebra :: LAlgebra Int
+        algebra = LAlgebra fcns fvar funi fbin fiff fqnt farr fnll flen
+
+        fcns _                     = 1
+        funi _ e1                  = 2 * e1
+        fbin e1 _ e2               = e1 * e2
+        fiff ge e1 e2              = ge * e1 * e2
+        fvar (Var (TPrim PInt) _)  = 3
+        fvar (Var (TPrim PReal) _) = 3
+        fvar (Var (TPrim PBool) _) = 2
+        fvar _                     = 3
+        fqnt _ _ e1 e2             = 3 * e1 * e2
+        farr _ _                   = 3
+        fnll _                     = 2
+        flen _                     = 3

src/LogicIR/Backend/QuickCheck/Test.hs

@@ -12,6 +12,7 @@ import LogicIR.Backend.QuickCheck.ModelGenerator
 import Data.Maybe (fromMaybe, isNothing, fromJust)
 import Data.List (find, (\\))
 import qualified Data.Map.Lazy as M
+import Control.Concurrent.Async (mapConcurrently)
 
 type LExprTeacher = LExpr
 type LExprStudent = LExpr
@@ -48,8 +49,8 @@ equal (_,tf,ft,_) = tf == 0 && ft == 0
 -- Calls 'test' multiple times.
 testEquality :: Int -> LExprTeacher -> LExprStudent -> IO (FeedbackCount, (Model, ArrayModel))
 testEquality 0 _ _ = error "testEquality won't work with 0 iterations."
-testEquality x e1 e2 = do
-  results <- mapM (const (test e1 e2)) [1..x]
+testEquality iters e1 e2 = do
+  results <- testAsync iters e1 e2 --  mapM (const (test e1 e2)) [1..iters]
   let feedback = foldr add defFbCount (map fst results) -- sum of feedbacks
   -- get list of counter models where
   let counters = map snd (filter (not . equal . fst) results)
@@ -58,6 +59,14 @@ testEquality x e1 e2 = do
   else
     return (feedback, head counters)
 
+testAsync :: Int -> LExprTeacher -> LExprStudent -> IO [(FeedbackCount, (Model, ArrayModel))]
+testAsync iters e1 e2 = do
+  let granularity = 50 :: Double
+  let nrThreads = ceiling ((fromIntegral iters) / granularity) :: Integer
+  let threads = [1..nrThreads]
+  results <- mapConcurrently (const (mapM (const (test e1 e2)) [(1::Integer)..50])) threads
+  return $ concat results
+
 test :: LExprTeacher -> LExprStudent -> IO (FeedbackCount, (Model, ArrayModel))
 test e1 e2 = do
     ((CBool res1),(m,arrM,_)) <- testLExpr e1