reorganizing. Also fixing wlp bug with x++ and ++x; also re-making APIs

README.txt → README.md

-To run the mutation test:
--Create the mutation files using Major in the right location (described below):
+### 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)
+- 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
 
-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:
 
-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
+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

examples/simple.java

+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

src/Javawlp/API.hs

+-- 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

src/Folds.hs → src/Javawlp/Engine/Folds.hs

+-- 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
 

src/HelperFunctions.hs → src/Javawlp/Engine/HelperFunctions.hs

+-- 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

src/Substitute.hs → src/Javawlp/Engine/Substitute.hs

-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

src/Types.hs → src/Javawlp/Engine/Types.hs

-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

src/Verifier.hs → src/Javawlp/Engine/Verifier.hs

-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

src/WLP.hs → src/Javawlp/Engine/WLP.hs

-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