diff --git a/Main.hs b/Main.hs
index 5f45bdd5689bf60381b01451b1a436882f98df20..3e9f6be56ed4291c8b53b9cde48850f7c537edfe 100644
--- a/Main.hs
+++ b/Main.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE TupleSections #-}
+
module Main where
import Language.Java.Syntax
@@ -6,7 +8,7 @@ import Language.Java.Pretty
import Data.List
import Control.Monad
import System.FilePath(joinPath)
-
+import System.Directory
import WLP
import Types
@@ -14,33 +16,57 @@ import Verifier
import HelperFunctions
import Settings
+sourcePath, mutantsDir :: FilePath
+sourcePath = joinPath ["Tests", testFile ++ ".java"]
+mutantsDir = joinPath ["..", testFile ++ " mutants"]
main :: IO ()
main = do
- source <- readFile (joinPath ["Tests", testFile ++ ".java"])
+ -- Get the wlp per method of the original source code
+ (env, wlpOriginal) <- wlpMethods sourcePath
+
+ -- Get the names of the folders containing the mutants (MAJOR creates a folder for every mutant)
+ mutationFolders <- listDirectory mutantsDir
+
+ -- Map each folder name to the path containing the mutant (mutant name is the same as the original file name)
+ let mutationPaths = map (\n -> joinPath [mutantsDir, n, testFile ++ ".java"]) mutationFolders
+
+ -- Calculate the wlp per method of all the mutants
+ wlpMutants <- mapM (\path -> wlpMethods path >>= return . (path, ) . snd) mutationPaths
- let result = parser compilationUnit source
+ mapM_ (compareWlps env wlpOriginal) wlpMutants
- case result of
- Left error -> print error
+-- | Calculates the wlp for every method in the source file. Also returns the type environment
+wlpMethods :: FilePath -> IO (TypeEnv, [(Ident, Exp)])
+wlpMethods s = do
+ -- Get the source code
+ source <- readFile s
+
+ -- Parse the source code
+ case parser compilationUnit source of
+ Left parseError -> error (show parseError)
Right compUnit -> do
let decls = getDecls compUnit
let methods = getMethodIds decls
let env = getTypeEnv compUnit decls methods
- -- putStrLn "\r\n-----Code-----"
- -- print compUnit
- mapM_ (testMethod compUnit env decls) methods
--- | Calculates and prints the wlp for a given method
-testMethod :: CompilationUnit -> TypeEnv -> [TypeDecl] -> Ident -> IO ()
-testMethod compUnit env decls id = do
- putStrLn "--------------"
- putStrLn (prettyPrint id ++ "\r\n")
- let pred = wlpWithEnv decls env (fromJust' "testMethod" $ getMethod decls id) postCond'
- putStrLn . prettyPrint $ pred
- putStrLn ""
- if unsafeIsTrue env pred then putStrLn "WLP evaluates to true" else (if unsafeIsFalse env pred then putStrLn "WLP evaluates to false" else putStrLn "undecidable")
- putStrLn "--------------"
+ -- Calculate the wlp per method
+ r <- mapM (\ident -> wlpMethod compUnit env decls ident >>= return . (ident, )) methods
+
+ return (env, r)
+
+-- | Calculates the wlp for a given method
+wlpMethod :: CompilationUnit -> TypeEnv -> [TypeDecl] -> Ident -> IO Exp
+wlpMethod compUnit env decls ident = do
+ let pred = wlpWithEnv decls env (fromJust' "wlpMethod" $ getMethod decls ident) postCond'
+ return pred
+
+-- | Compares the wlp per method of a program S and mutation S' by verifying that (wlp (S, m) q => wlp (S', m) q) holds for every method m
+compareWlps :: TypeEnv -> [(Ident, Exp)] -> (String, [(Ident, Exp)]) -> IO ()
+compareWlps env s (path, s') = mapM_ compareMethod s where
+ compareMethod (ident, e) = case lookup ident s' of
+ Nothing -> putStrLn ("The method \'" ++ show ident ++ "\' is missing in one of the mutations.")
+ Just e' -> if unsafeIsTrue env (e `imp` e') then return () else putStrLn ("error detected in mutation: " ++ path)
-- The post-condition (for testing)
postCond' :: Exp
diff --git a/Substitute.hs b/Substitute.hs
index b8a4daa699b2af5ed8fd2359f50e3e09384860eb..337f9cc2d77b7892422d40926db3025cada797d2 100644
--- a/Substitute.hs
+++ b/Substitute.hs
@@ -28,9 +28,9 @@ substVarExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQu
fArrayCreateInit t dim arrayInit _ = ArrayCreateInit t dim arrayInit
fFieldAccess fieldAccess inh = case lhs inh of
FieldLhs fieldAccess' -> case fieldAccess of
- PrimaryFieldAccess e ident -> error "todo: fieldAccess substitution"
- SuperFieldAccess ident -> error "todo: fieldAccess substitution"
- ClassFieldAccess name ident -> error "todo: fieldAccess substitution"
+ PrimaryFieldAccess e ident -> error "fieldAccess substitution"
+ SuperFieldAccess ident -> error "fieldAccess substitution"
+ ClassFieldAccess name ident -> error "fieldAccess substitution"
_ -> FieldAccess fieldAccess
fMethodInv invocation inh = case invocation of
MethodCall name exps -> MethodInv (MethodCall name (map (flip (foldExp substVarExpAlgebra) (inh {arrayLookup = True})) exps))
@@ -87,7 +87,7 @@ substVarExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQu
fCast t e inh = Cast t (e inh)
fBinOp e1 op e2 inh = BinOp (e1 inh) op (e2 inh)
fInstanceOf e refType inh = InstanceOf (e inh) refType
- fCond g e1 e2 inh = Cond (g inh) (e1 inh) (e2 inh)
+ fCond g e1 e2 inh = Cond (g inh {arrayLookup = False}) (e1 inh) (e2 inh)
fAssign lhs assOp e inh = Assign lhs assOp (e inh)
fLambda lParams lExp _ = Lambda lParams lExp
fMethodRef className methodName _ = MethodRef className methodName
diff --git a/WLP.hs b/WLP.hs
index c84dd05fdc5d4d526b372b263c92ef64e07cc942..c9a796f77744c691fade717e08b55644e3dcb7a9 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -206,7 +206,7 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
-- gets the transformer for array access (as array access may throw an error)
arrayAccessWlp :: Exp -> [Exp] -> Inh -> Exp -> Exp
arrayAccessWlp a i inh q = case catch inh of
- Nothing -> Cond (foldr (\(i, l) e -> e &* (BinOp i LThan l) &* (BinOp i GThanE (Lit (Int 0)))) true (zip i (dimLengths a))) q false
+ Nothing -> (foldr (\(i, l) e -> e &* (BinOp i LThan l) &* (BinOp i GThanE (Lit (Int 0)))) true (zip i (dimLengths a))) &* q
Just (cs, f) -> let e = InstanceCreation [] (ClassType [(Ident "ArrayIndexOutOfBoundsException", [])]) [] Nothing
in Cond (foldr (\(i, l) e -> e &* (BinOp i LThan l) &* (BinOp i GThanE (Lit (Int 0)))) true (zip i (dimLengths a))) q ((maybe (if f then q else q &* throwException e)) (\b -> wlp' (inh {acc = id, catch = Nothing}) (StmtBlock b) q) (getCatch (decls inh) (env inh) e cs))