diff --git a/README.md b/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..3cbd4cddec45a3aaf368738067099d953c9a5168
--- /dev/null
+++ b/README.md
@@ -0,0 +1,22 @@
+### To run the mutation test:
+
+- Create the mutation files using Major in the right location (described below):
+ $MAJOR_HOME/bin/javac -J-Dmajor.export.directory="$SOURCE mutants" -J-Dmajor.export.mutants=true -XMutator:ALL -cp "wlp/tests" wlp/Tests/$SOURCE.java
+- Edit settings.hs to specify the post-condition and test file
+- Run the main function (this can be done using ghci)
+- The results will be stored in wlp/Results, overwriting any existing results file that uses the same parameters (the analysis is static, so the results should be the same in this case anyway)
+
+### To run the false positive test:
+
+- Edit settings.hs to specify the post-condition
+- Run the testFalsePositives function (this can be done using ghci)
+- The results will be stored in wlp/Results
+
+### Folder structure:
+
+The folder generated by Major must be in the same folder as the wlp folder, and must be named "SOURCE mutants" (where SOURCE is the name of the test class)
+A path to a mutant (the 5th mutant in this example) looks like this: "SOURCE mutants/5/classPath/SOURCE.java" Because of this, to analyse a new test class the classPath function in Settings.hs has to be extended with the corresponding class path
+
+### Dependency
+
+- language-java Haskell package
\ No newline at end of file
diff --git a/README.txt b/README.txt
deleted file mode 100644
index 284c151e847140d35451c6cbef39813cb2fd5707..0000000000000000000000000000000000000000
--- a/README.txt
+++ /dev/null
@@ -1,15 +0,0 @@
-To run the mutation test:
--Create the mutation files using Major in the right location (described below):
- $MAJOR_HOME/bin/javac -J-Dmajor.export.directory="$SOURCE mutants" -J-Dmajor.export.mutants=true -XMutator:ALL -cp "wlp/tests" wlp/Tests/$SOURCE.java
--Edit settings.hs to specify the post-condition and test file
--Run the main function (this can be done using ghci)
--The results will be stored in wlp/Results, overwriting any existing results file that uses the same parameters (the analysis is static, so the results should be the same in this case anyway)
-
-To run the false positive test:
--Edit settings.hs to specify the post-condition
--Run the testFalsePositives function (this can be done using ghci)
--The results will be stored in wlp/Results
-
-Folder structure:
-The folder generated by Major must be in the same folder as the wlp folder, and must be named "SOURCE mutants" (where SOURCE is the name of the test class)
-A path to a mutant (the 5th mutant in this example) looks like this: "SOURCE mutants/5/classPath/SOURCE.java" Because of this, to analyse a new test class the classPath function in Settings.hs has to be extended with the corresponding class path
\ No newline at end of file
diff --git a/examples/simple.java b/examples/simple.java
new file mode 100644
index 0000000000000000000000000000000000000000..75c864ceafcd4b8446a2a4ffdfadfd122092a9fe
--- /dev/null
+++ b/examples/simple.java
@@ -0,0 +1,25 @@
+public class simple
+{
+ // try for example with postcond: returnValue >= 0
+ int f1(int x) { x++ ; return x ; }
+
+ // try post-cond returnValue == 0
+ int f2(int x) { return x++ ; }
+
+ // try post-cond returnValue == 0
+ int f3(int x) { return ++x ; }
+
+ // An example from the thesis; try post-cond returnValue == 0
+ int f4(int x) { int y = x++ - x++ ; return y ; }
+
+ int a ;
+ // try pcond: returnValue.a >= 0
+ simple g1(int delta) { this.a = this.a + delta ; return this ; }
+
+ // try pcond: returnValue >= 0
+ int g2(int delta) { this.a = this.a + delta ; return this.a ; }
+
+ // try pcond: targetObj_.a >= 0
+ void g3(int delta) { this.a = this.a + delta ; }
+
+}
\ No newline at end of file
diff --git a/src/Daikon.hs b/experiments/wermer/Daikon.hs
similarity index 100%
rename from src/Daikon.hs
rename to experiments/wermer/Daikon.hs
diff --git a/src/Main.hs b/experiments/wermer/Main.hs
similarity index 100%
rename from src/Main.hs
rename to experiments/wermer/Main.hs
diff --git a/src/Settings.hs b/experiments/wermer/Settings.hs
similarity index 100%
rename from src/Settings.hs
rename to experiments/wermer/Settings.hs
diff --git a/src/Javawlp/API.hs b/src/Javawlp/API.hs
new file mode 100644
index 0000000000000000000000000000000000000000..30c99269baae6622abb26e7875dd435b20131941
--- /dev/null
+++ b/src/Javawlp/API.hs
@@ -0,0 +1,85 @@
+-- Copyright (c) 2017 Utrecht University
+-- Author: Koen Wermer, Wishnu Prasetya
+
+module Javawlp.API where
+
+import Language.Java.Syntax
+import Language.Java.Parser
+import Language.Java.Pretty
+
+import Javawlp.Engine.WLP
+import Javawlp.Engine.Types
+import Javawlp.Engine.HelperFunctions
+import Javawlp.Engine.Verifier
+
+-- | Parses a Java source file, and extracts the necessary information from the compilation unit
+parseJava :: FilePath -> IO (TypeEnv, [TypeDecl], [Ident])
+parseJava 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
+
+ return (env, decls, methods)
+
+
+-- | Parse a string containing a Java-expression to a parse tree. This is intended to formulate
+-- a post-condition to be passed to the wlp transformer.
+post_ :: String -> Exp
+post_ e = case parser Language.Java.Parser.exp e of
+ Right e_ -> e_
+ _ -> error "syntax error in post-condition"
+
+-- | Calculates the wlp for a given method
+wlpMethod :: WLPConf -> TypeEnv -> [TypeDecl] -> Ident -> Exp -> IO Exp
+wlpMethod conf env decls methodName postCondition = do
+ -- Find the return type of the method
+ let returnType = getMethodType decls methodName -- for now, ignored
+
+ -- Add returnValue to the type environment with the correct type
+ let env' = extendEnv env decls methodName
+
+ let methodBody = case getMethod decls methodName of
+ Just stmt -> stmt
+ _ -> error "wlpMethod: cannot get the method body."
+
+ -- Calculate the wlp:
+ return $ wlpWithEnv conf decls env' methodBody postCondition
+
+-- | Calculates the wlps of a list of methods
+wlpMethods :: WLPConf -> TypeEnv -> [TypeDecl] -> [(Ident,Exp)] -> IO [(Ident, Exp)]
+wlpMethods conf env decls methods_and_postconds
+ =
+ sequence $ map (\(mname,pcond) -> do { q <- wlpMethod conf env decls mname pcond ; return (mname,q) }) methods'
+ where
+ methods' = if ignoreMainMethod conf
+ then filter (\(mname,_) -> mname /= Ident "main") methods_and_postconds
+ else methods_and_postconds
+
+
+defaultConf :: WLPConf
+defaultConf = WLPConf {
+ nrOfUnroll=1,
+ ignoreLibMethods=False,
+ ignoreMainMethod =False
+ }
+
+-- | Print the wlp of a method with respect to a given post-condition.
+printWlp :: String -> String -> String -> IO ()
+printWlp sourcePath methodName postCond = do
+ (typeEnv,decls,methodNames) <- parseJava sourcePath
+ let q = post_ postCond
+ p <- wlpMethod defaultConf typeEnv decls (Ident methodName) q
+ putStrLn $ showMethodWlp methodName q p
+
+showMethodWlp :: String -> Exp -> Exp -> String
+showMethodWlp methodName postCond wlp =
+ "wlp of " ++ methodName ++ " over " ++ prettyPrint postCond
+ ++ " is "
+ ++ prettyPrint wlp
diff --git a/src/Folds.hs b/src/Javawlp/Engine/Folds.hs
similarity index 98%
rename from src/Folds.hs
rename to src/Javawlp/Engine/Folds.hs
index 13238df2c7f45d10119a0daac90713f55febbcee..208187b6c1fb8806092883ea6472181c9238e840 100644
--- a/src/Folds.hs
+++ b/src/Javawlp/Engine/Folds.hs
@@ -1,5 +1,8 @@
+-- Copyright (c) 2017 Utrecht University
+-- Author: Koen Wermer
+
-- Folds over Java data structures
-module Folds where
+module Javawlp.Engine.Folds where
import Language.Java.Syntax
diff --git a/src/HelperFunctions.hs b/src/Javawlp/Engine/HelperFunctions.hs
similarity index 99%
rename from src/HelperFunctions.hs
rename to src/Javawlp/Engine/HelperFunctions.hs
index 24608a2a4583c93f9acc8c76b0ffc92196b30077..37b989e7dc3770cedb750c01e5b442c14448374f 100644
--- a/src/HelperFunctions.hs
+++ b/src/Javawlp/Engine/HelperFunctions.hs
@@ -1,5 +1,8 @@
+-- Copyright (c) 2017 Utrecht University
+-- Author: Koen Wermer
+
-- Helper functions for the Java data structure
-module HelperFunctions where
+module Javawlp.Engine.HelperFunctions where
import Language.Java.Syntax
import Language.Java.Pretty
diff --git a/src/Substitute.hs b/src/Javawlp/Engine/Substitute.hs
similarity index 97%
rename from src/Substitute.hs
rename to src/Javawlp/Engine/Substitute.hs
index 337f9cc2d77b7892422d40926db3025cada797d2..91c5100384373f832a01f8335e7d8a515be50794 100644
--- a/src/Substitute.hs
+++ b/src/Javawlp/Engine/Substitute.hs
@@ -1,10 +1,16 @@
-module Substitute (substVar, desugarAssign) where
+-- Copyright (c) 2017 Utrecht University
+-- Author: Koen Wermer
+
+--
+-- Providing functions to do variable substitution [e/v] and to desugar assignments.
+--
+module Javawlp.Engine.Substitute (substVar, desugarAssign) where
import Language.Java.Syntax
import Data.List
-import Folds
-import HelperFunctions
+import Javawlp.Engine.Folds
+import Javawlp.Engine.HelperFunctions
-- | A type for the inherited attribute
diff --git a/src/Types.hs b/src/Javawlp/Engine/Types.hs
similarity index 95%
rename from src/Types.hs
rename to src/Javawlp/Engine/Types.hs
index 26d984dd9f39a226072d356c8bcd927f6aeaaf0e..c8b2b8413a221bb4c978b9154c57a5b6d2a255ca 100644
--- a/src/Types.hs
+++ b/src/Javawlp/Engine/Types.hs
@@ -1,13 +1,14 @@
-module Types where
+-- Copyright (c) 2017 Utrecht University
+-- Author: Koen Wermer
+
+module Javawlp.Engine.Types where
import Language.Java.Syntax
import Data.Maybe
import Data.List
-import Folds
-import HelperFunctions
-import Settings
-
+import Javawlp.Engine.Folds
+import Javawlp.Engine.HelperFunctions
typesStmtAlgebra :: StmtAlgebra TypeEnv
typesStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhancedFor, fEmpty, fExpStmt, fAssert, fSwitch, fDo, fBreak, fContinue, fReturn, fSynchronized, fThrow, fTry, fLabeled) where
diff --git a/src/Verifier.hs b/src/Javawlp/Engine/Verifier.hs
similarity index 98%
rename from src/Verifier.hs
rename to src/Javawlp/Engine/Verifier.hs
index 1a17ad2bbb5c1586884bbdc6947c775867bbaa80..d5e4c79489bdf05f5691da49a0f0a23b3cf89d54 100644
--- a/src/Verifier.hs
+++ b/src/Javawlp/Engine/Verifier.hs
@@ -1,13 +1,16 @@
-module Verifier where
+-- Copyright (c) 2017 Utrecht University
+-- Author: Koen Wermer
+
+-- Providing a converter from Java expression to Z3 expression
+module Javawlp.Engine.Verifier where
import Language.Java.Syntax
import Language.Java.Pretty
import Z3.Monad
import System.IO.Unsafe
-import Folds
-import HelperFunctions
-import Settings
+import Javawlp.Engine.Folds
+import Javawlp.Engine.HelperFunctions
-- | Checks wether the negation is unsatisfiable
diff --git a/src/WLP.hs b/src/Javawlp/Engine/WLP.hs
similarity index 88%
rename from src/WLP.hs
rename to src/Javawlp/Engine/WLP.hs
index 41f368b9002cfd4a95d2e55dc9a5cb56fa183fa5..d09dab05043913882bfe9656cf7231ae6529780f 100644
--- a/src/WLP.hs
+++ b/src/Javawlp/Engine/WLP.hs
@@ -1,4 +1,8 @@
-module WLP where
+-- Copyright (c) 2017 Utrecht University
+-- Author: Koen Wermer
+
+-- Implementing the wlp transformer.
+module Javawlp.Engine.WLP where
import Language.Java.Syntax
import Language.Java.Lexer
@@ -6,16 +10,23 @@ import Language.Java.Parser
import Data.Maybe
import Data.List
-import Folds
-import Verifier
-import Substitute
-import HelperFunctions
-import Settings
+import Javawlp.Engine.Folds
+import Javawlp.Engine.Verifier
+import Javawlp.Engine.Substitute
+import Javawlp.Engine.HelperFunctions
-
+data WLPConf = WLPConf {
+ -- the max. number of times a loop/recursion is unrolled
+ nrOfUnroll :: Int,
+ -- When ignoreLibMethods is true, library calls will simply be ignored (treated as skip).
+ -- When false, we consider library methods but make no assumptions about them (so the WLP will be true)
+ ignoreLibMethods :: Bool,
+ ignoreMainMethod :: Bool
+ }
-- | A type for the inherited attribute
-data Inh = Inh {acc :: Exp -> Exp, -- The accumulated transformer of the current block up until the current statement
+data Inh = Inh {wlpConfig :: WLPConf, -- Some configuration parameters for the wlp
+ acc :: Exp -> Exp, -- The accumulated transformer of the current block up until the current statement
br :: Exp -> Exp, -- The accumulated transformer up until the last loop (this is used when handling break statements etc.)
catch :: Maybe ([Catch], Bool), -- The catches when executing a block in a try statement, and a Bool indicating wether there is a finally-block
env :: TypeEnv, -- The type environment for typing expressions
@@ -41,7 +52,8 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
in trans . substVar' inh var e' . (\q -> (ExpName (Name [var]) &* s1 inh q) |* (neg (ExpName (Name [var])) &* s2 inh q))
fWhile e s inh = let (e', trans) = foldExp wlpExpAlgebra e inh {acc = id}
var = getVar
- in (\q -> unrollLoopOpt inh {br = const q} nrOfUnroll e' trans s q)
+ numberOfUnrolling = nrOfUnroll $ wlpConfig $ inh
+ in (\q -> unrollLoopOpt inh {br = const q} numberOfUnrolling e' trans s q)
fBasicFor init me incr s inh = let loop = (fWhile (fromMaybeGuard me) (\inh' -> s (inh' {acc = (wlp' inh' {acc = id} (incrToStmt incr))})) inh) in wlp' (inh {acc = loop}) (initToStmt init)
fEnhancedFor = error "EnhancedFor"
fEmpty inh = (acc inh) -- Empty does nothing, but still passes control to the next statement
@@ -163,9 +175,12 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
fArrayCreate t dimLengths dim inh = (ArrayCreate t (map (\e -> fst (e inh)) dimLengths) dim, acc inh)
fArrayCreateInit t dim init inh = error "ArrayCreateInit" -- (ArrayCreateInit t dim init, acc inh)
fFieldAccess fieldAccess inh = (foldFieldAccess inh fieldAccess, (acc inh))
- fMethodInv invocation inh = case invocation of
+ fMethodInv invocation inh = let
+ numberOfUnrolling = nrOfUnroll $ wlpConfig $ inh
+ in
+ case invocation of
MethodCall (Name [Ident "*assume"]) [e] -> (false, (if e == false then const true else imp e)) -- *assume is the regular assume function
- _ -> if getCallCount (calls inh) (invocationToId invocation) >= nrOfUnroll -- Check the recursion depth
+ _ -> if getCallCount (calls inh) (invocationToId invocation) >= numberOfUnrolling -- Check the recursion depth
then (undefined, const true) -- Recursion limit reached: we just assume the post codition will hold
else let varId = getReturnVar invocation
callWlp = wlp' (inh {acc = id, calls = incrCallCount (calls inh) (invocationToId invocation), ret = Just varId, object = getObject inh invocation}) (inlineMethod inh invocation)
@@ -178,20 +193,30 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
-- x++ increments x but evaluates to the original value
fPostIncrement e inh = let (e', trans) = e inh in
case e' of
- var@(ExpName name) -> (var, substVar (env inh) (decls inh) (NameLhs name) (BinOp var Add (Lit (Int 1))) . trans)
+ -- Wish: this is incorrect
+ -- var@(ExpName name) -> (var, substVar (env inh) (decls inh) (NameLhs name) (BinOp var Add (Lit (Int 1))) . trans)
+ -- fix:
+ var@(ExpName name) -> (BinOp var Sub (Lit (Int 1)), substVar (env inh) (decls inh) (NameLhs name) (BinOp var Add (Lit (Int 1))) . trans)
exp -> (exp, trans)
fPostDecrement e inh = let (e', trans) = e inh in
case e' of
- var@(ExpName name) -> (var, substVar (env inh) (decls inh) (NameLhs name) (BinOp var Sub (Lit (Int 1))) . trans)
+ -- incorrect
+ -- var@(ExpName name) -> (var, substVar (env inh) (decls inh) (NameLhs name) (BinOp var Sub (Lit (Int 1))) . trans)
+ var@(ExpName name) -> (BinOp var Add (Lit (Int 1)), substVar (env inh) (decls inh) (NameLhs name) (BinOp var Sub (Lit (Int 1))) . trans)
exp -> (exp, trans)
-- ++x increments x and evaluates to the new value of x
fPreIncrement e inh = let (e', trans) = e inh in
case e' of
- var@(ExpName name) -> (BinOp var Add (Lit (Int 1)), substVar (env inh) (decls inh) (NameLhs name) (BinOp var Add (Lit (Int 1))) . trans)
+ -- Wish: this is incorrect
+ -- var@(ExpName name) -> (BinOp var Add (Lit (Int 1)), substVar (env inh) (decls inh) (NameLhs name) (BinOp var Add (Lit (Int 1))) . trans)
+ -- fix:
+ var@(ExpName name) -> (var, substVar (env inh) (decls inh) (NameLhs name) (BinOp var Add (Lit (Int 1))) . trans)
exp -> (BinOp exp Add (Lit (Int 1)), trans)
fPreDecrement e inh = let (e', trans) = e inh in
case e' of
- var@(ExpName name) -> (BinOp var Sub (Lit (Int 1)), substVar (env inh) (decls inh) (NameLhs name) (BinOp var Sub (Lit (Int 1))) . trans)
+ -- incorrect
+ -- var@(ExpName name) -> (BinOp var Sub (Lit (Int 1)), substVar (env inh) (decls inh) (NameLhs name) (BinOp var Sub (Lit (Int 1))) . trans)
+ var@(ExpName name) -> (var, substVar (env inh) (decls inh) (NameLhs name) (BinOp var Sub (Lit (Int 1))) . trans)
exp -> (BinOp exp Sub (Lit (Int 1)), trans)
fPrePlus e inh = let (e', trans) = e inh in (e', trans)
fPreMinus e inh = let (e', trans) = e inh in (PreMinus e', trans)
@@ -238,10 +263,14 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
-- Gets the body of the method
getBody :: Inh -> MethodInvocation -> Stmt
getBody inh (MethodCall name _) = case getMethod (decls inh) (getMethodId name) of
- Nothing -> if ignoreLibMethods then Empty else ExpStmt $ MethodInv (MethodCall (Name [Ident "*assume"]) [false])
+ Nothing -> if (ignoreLibMethods $ wlpConfig $ inh)
+ then Empty
+ else ExpStmt $ MethodInv (MethodCall (Name [Ident "*assume"]) [false])
Just s -> s
getBody inh (PrimaryMethodCall _ _ id _) = case getMethod (decls inh) id of
- Nothing -> if ignoreLibMethods then Empty else ExpStmt $ MethodInv (MethodCall (Name [Ident "*assume"]) [false])
+ Nothing -> if (ignoreLibMethods $ wlpConfig $ inh)
+ then Empty
+ else ExpStmt $ MethodInv (MethodCall (Name [Ident "*assume"]) [false])
Just s -> s
getBody inh _ = undefined
-- Assigns the supplied parameter values to the parameter variables
@@ -303,12 +332,12 @@ substVar' :: Inh -> Ident -> Exp -> Syn
substVar' inh var e = substVar (env inh) (decls inh) (NameLhs (Name [var])) e
-- | Calculates the weakest liberal pre-condition of a statement and a given post-condition
-wlp :: [TypeDecl] -> Stmt -> Exp -> Exp
-wlp decls = wlpWithEnv decls []
+wlp :: WLPConf -> [TypeDecl] -> Stmt -> Exp -> Exp
+wlp config decls = wlpWithEnv config decls []
-- | wlp with a given type environment
-wlpWithEnv :: [TypeDecl] -> TypeEnv -> Stmt -> Exp -> Exp
-wlpWithEnv decls env = wlp' (Inh id id Nothing env decls [] (Just (Ident "returnValue")) (Just (ExpName (Name [Ident "*obj"]))))
+wlpWithEnv :: WLPConf -> [TypeDecl] -> TypeEnv -> Stmt -> Exp -> Exp
+wlpWithEnv config decls env = wlp' (Inh config id id Nothing env decls [] (Just (Ident "returnValue")) (Just (ExpName (Name [Ident "targetObj_"]))))
-- wlp' lets you specify the inherited attributes
wlp' :: Inh -> Stmt -> Syn