From b91e4bda7c26adc7e18a90ad3edfb200b8f6f223 Mon Sep 17 00:00:00 2001
From: ISWB Prasetya <iswbprasetya@iswbs-mbp.home>
Date: Sun, 20 Aug 2017 16:53:49 +0200
Subject: [PATCH] extending Experiment.hs, we now can check against a whole
directory of mutants
---
experiments/wermer2/Experiment.hs | 74 +++++++++++++++++++++++++------
experiments/wermer2/mutation.mml | 7 ++-
2 files changed, 65 insertions(+), 16 deletions(-)
diff --git a/experiments/wermer2/Experiment.hs b/experiments/wermer2/Experiment.hs
index aad8dde..38a3c39 100644
--- a/experiments/wermer2/Experiment.hs
+++ b/experiments/wermer2/Experiment.hs
@@ -4,27 +4,73 @@ module Experiment where
import Javawlp.API
import Javawlp.Engine.HelperFunctions
import Javawlp.Engine.Verifier
+import Javawlp.Engine.WLP
import Language.Java.Syntax
import Z3.Monad
+import Data.List
+import System.IO.Unsafe
+import System.FilePath
+import System.Directory
+-- specify the wlp global configuration here
+wlpConfiguretion = WLPConf {
+ nrOfUnroll=1,
+ ignoreLibMethods=False,
+ ignoreMainMethod =False
+ }
-
-checkMutant original mutantDir methodName postcond = do
+-- Calculate the wlps of an orginal java method and its mutant, then compare them.
+-- Example:
+--
+-- checkMutant Triangle mutantdir tritype1 ["returnValue==0", "returnValue==1"]
+--
+-- This will check the method tritype1 in subjects/src/Triangle.java vs mdir/Triangle.java
+--
+checkMutant :: String -> FilePath -> String -> [String] -> IO (Maybe Bool)
+checkMutant original mutantDir methodName postconds = do
let srcName = original ++ ".java"
- (typeEnv1,decls1,methodNames1) <- parseJava ("./subjects/src/" ++ srcName)
- (typeEnv2,decls2,methodNames2) <- parseJava (mutantDir ++ "/" ++ srcName)
+ let srcPath = "./subjects/src" </> srcName
+ let mutantPath = mutantDir </> srcName
+ (typeEnv1,decls1,methodNames1) <- parseJava srcPath
+ (typeEnv2,decls2,methodNames2) <- parseJava mutantPath
let mname = Ident methodName
- let q = post_ postcond
- p1 <- wlpMethod defaultConf typeEnv1 decls1 mname q
- p2 <- wlpMethod defaultConf typeEnv2 decls2 mname q
- let tocheck = PreNot (p1 ==* p2)
- let (result,_) = unsafeIsSatisfiable (extendEnv typeEnv1 decls1 mname) decls1 tocheck
- case result of
- Sat -> putStrLn "** KILLED."
- Unsat -> putStrLn "** SURVIVED."
- _ -> putStrLn "** UNDECIDED."
-
+ let qs = [ post_ q | q <- postconds ]
+ -- this function will be used to compare the resulting wlps
+ let comparePreC p1 p2 = let
+ f = PreNot (p1 ==* p2)
+ (result,_) = unsafeIsSatisfiable (extendEnv typeEnv1 decls1 mname) decls1 f
+ in
+ result
+
+ ps1 <- sequence [ wlpMethod wlpConfiguretion typeEnv1 decls1 mname q | q <- qs ]
+ ps2 <- sequence [ wlpMethod wlpConfiguretion typeEnv2 decls2 mname q | q <- qs ]
+ putStrLn ("## Checking mutant " ++ mutantPath)
+ let z = zipWith comparePreC ps1 ps2
+ if any (== Sat) z then return $ Just False -- the mutant is killed
+ else if all (== Unsat) z then return $ Just True -- the mutant definitely survives
+ else return Nothing -- some of the wlps are undecidable
+
+
+checkAllMutants original mutantsRootDir methodName postconds = do
+ mdirs <- getMutantsSubdirs mutantsRootDir
+ let mdirs_ = [ mutantsRootDir </> d | d <- mdirs ]
+ results <- sequence [ checkMutant original md methodName postconds | md <- mdirs_ ]
+ let nmutants = length results
+ let killed = length $ filter (== Just False) results
+ let undecided = length $ filter (== Nothing) results
+ putStrLn ("** Checking " ++ original ++ "." ++ methodName ++ " on " ++ show nmutants ++ " mutants.")
+ putStrLn ("** Killed=" ++ show killed ++ ", Survived=" ++ show (nmutants - killed)
+ ++ " (incl. " ++ show undecided ++ " undecided)" )
+ let survivors = [ (m,r) | (m,r) <- zip mdirs results, not(r == Just False) ]
+ sequence_ [ putStrLn ("** Unable to kill mutant " ++ m ++ ", " ++ show r) | (m,r) <- survivors ]
+ where
+ getMutantsSubdirs mutantsRootDir = do
+ fs <- listDirectory mutantsRootDir
+ let mdirs = [ name | name <- fs, not("." `isPrefixOf` name)
+ && unsafePerformIO (doesDirectoryExist (mutantsRootDir </> name))
+ ]
+ return mdirs
\ No newline at end of file
diff --git a/experiments/wermer2/mutation.mml b/experiments/wermer2/mutation.mml
index a27f808..8894557 100644
--- a/experiments/wermer2/mutation.mml
+++ b/experiments/wermer2/mutation.mml
@@ -1,12 +1,15 @@
// A simple mml file to generate all mutants
list_aor={+,-,*,/,%};
+list_aorPM={+,-};
list_lor={&,|,^};
list_sor={<<,>>,>>>};
list_oru={+,-,~};
-BIN(+)->list_aor;
-BIN(-)->list_aor;
+//BIN(+)->list_aor;
+//BIN(-)->list_aor;
+BIN(+)->list_aorPM;
+BIN(-)->list_aorPM;
BIN(*)->list_aor;
BIN(/)->list_aor;
BIN(%)->list_aor;
--
GitLab