diff --git a/examples/XException.java b/examples/XException.java
new file mode 100644
index 0000000000000000000000000000000000000000..508d3154d6342fa22085a4a2126536d2f2b1349d
--- /dev/null
+++ b/examples/XException.java
@@ -0,0 +1,19 @@
+public class XException {
+
+ public static int Uncaught(int x) {
+ if (x<0) throw new IllegalArgumentException() ;
+ x = x+1 ;
+ return x ;
+ }
+
+ public static int WithCatch(int x) {
+ try {
+ if (x<0) throw new IOException() ;
+ }
+ catch (IOException e) { x=0 ; }
+ x = x+1 ;
+ return x ;
+ }
+
+
+}
diff --git a/examples/loops.java b/examples/loops.java
index b22e2e2056f4fe18bcc809b6a9832d2bca48a70b..cc48e2d65bedd8e3c5307c2be2b238023eb71ed6 100644
--- a/examples/loops.java
+++ b/examples/loops.java
@@ -1,14 +1,59 @@
+// Javac will refuse to compile this file because some usage of break and continue causes
+// some code to be unreachable. To compile, preceed them with e.g. if(true) break ;
+// I don't do this on purpose to keep the generated wlp simple, so make it easier when
+// using these programs for debugging wlp.
+//
+
public class Loops
{
- public static void foo()
- {
+
+ public static void While(int N){
+ int i=0 ;
+ while (i<N) { i++ ; }
+ i = i+9 ;
+ }
+
+ public static void WhileBreak(int N){
+ int i=0 ;
+ int x = 0 ;
+ int y = 0 ;
+ while (i<N) { x=1 ; break ; y=1 ; i++ ; }
+ i = i+9 ;
+ x = x+10 ;
+ y = y+11 ;
+ }
+
+ public static void WhileContinue(int N){
+ int i=0 ;
+ int x = 0 ;
+ int y = 0 ;
+ while (i<N) { x=1 ; i++ ; continue ; y=1 ; }
+ i = i+9 ;
+ x = x+10 ;
+ y = y+11 ;
+ }
+
+ public static void WhileNestedContinue(int N){
+ int i=0 ;
+ int x = 0 ;
+ int y = 0 ;
+ while (i<N) { i++ ; while(x<N) { x++ ; continue ; y=2 ; } continue ; y=1 ; }
+ i = i+9 ;
+ x = x+10 ;
+ y = y+11 ;
+ }
+
+ public static void For(int N){
+ int i ;
+ int x ;
+ for (i=0; i<N; i++ ) { x = x+2 ; }
+ }
+
+ public static void ForNested() {
int i ;
- for(i = 0; i < 6; i++)
- {
- for(int j = 0; j < 6; j++)
- {
- if(true)
- assert j == 1;
+ for(i = 0; i < 6; i++) {
+ for(int j = 0; j < 6; j++) {
+ if(true) assert j == 1;
}
}
int x = i;
diff --git a/examples/simple.java b/examples/simple.java
index a6f462954a8d0e875d23249ce9b215322f137109..701fd747592de0a4ca8ac368e84b6ef31b190c45 100644
--- a/examples/simple.java
+++ b/examples/simple.java
@@ -21,5 +21,13 @@ public class Simple {
// try pcond: targetObj_.a >= 0
void g3(int delta) { this.a = this.a + delta ; }
+
+ int Seq(int x) { x = x + 1 ; x = x + 9 ; return x ; }
+
+ int ReturnInTheMiddle(int x) {
+ x = x + 1 ;
+ if (x==0) return x ;
+ x = x + 9 ;
+ return x ; }
}
\ No newline at end of file
diff --git a/experiments/wermer2/Experiment.hs b/experiments/wermer2/Experiment.hs
deleted file mode 100644
index 38a3c39a885ed1e178a647b23da07c3d5a06cbb2..0000000000000000000000000000000000000000
--- a/experiments/wermer2/Experiment.hs
+++ /dev/null
@@ -1,76 +0,0 @@
--- Contain various functions to automate the experiment
-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
- }
-
--- 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"
- let srcPath = "./subjects/src" </> srcName
- let mutantPath = mutantDir </> srcName
- (typeEnv1,decls1,methodNames1) <- parseJava srcPath
- (typeEnv2,decls2,methodNames2) <- parseJava mutantPath
-
- let mname = Ident methodName
- 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/WlpExperiment.hs b/experiments/wermer2/WlpExperiment.hs
new file mode 100644
index 0000000000000000000000000000000000000000..881432ffaae1cc68730529d85649c94070e42f5d
--- /dev/null
+++ b/experiments/wermer2/WlpExperiment.hs
@@ -0,0 +1,160 @@
+--
+-- Contain the script to run the wlp experiment.
+--
+module WlpExperiment 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
+import System.IO.Unsafe
+import System.FilePath
+import System.Directory
+
+
+-- ======================================================================
+-- The top-level main functions to run the wlp-experiment on one or all subjects.
+-- ======================================================================
+
+main = do
+ clean
+ sequence_ [ main1 "FN" s | s <- subjects ] -- checking wlp's false negatives rate, using Major's generated mutants
+ sequence_ [ main1 "FP" s | s <- subjectsFP ] -- checking wlp's false positives rate, using manually crafted equivalent mutants
+
+
+main1 mode subject = do
+ let (classname,targetMethodName,postconditions) = subject
+ checkAllMutants mode classname targetMethodName postconditions
+
+clean = do
+ removeFile logFile
+ removeFile dataFile
+
+-- ======================================================================
+-- List of all subjects: class name, target method name, list of post-conditions
+-- ======================================================================
+
+-- all subjects
+subjects = [ ("Triangle", "tritype1", ["returnValue == -1", "returnValue == 0", "returnValue == 1", "returnValue == 2"]) ]
+
+-- subjects which are to be included for false-positive-checking experiment
+subjectsFor_FP_experiment = [ ]
+
+subjectsFP = [ s | s@(cn,fn,_) <- subjects, (cn ++ "." ++ fn) `elem` subjectsFor_FP_experiment ]
+
+-- ======================================================================
+-- Configuration parameters
+-- ======================================================================
+
+subjectsDir = "." </> "subjects" </> "src"
+majorMutantsDir = "." </> "mutants" </> "generated"
+handcraftedMutantsDir = "." </> "mutants" </> "handcrafted"
+dataDir = "." </> "data"
+tmpDir = "." </> "tmp"
+
+-- specify the wlp global configuration here
+wlpConfiguretion = WLPConf {
+ nrOfUnroll=1,
+ ignoreLibMethods=False,
+ ignoreMainMethod =False
+ }
+
+-- ======================================================================
+-- Logging, debug, and writing to the output data-file
+-- ======================================================================
+
+logFile = tmpDir </> "wlplog.log"
+logWrite s = do { debugWrite s ; appendFile logFile s }
+logWriteLn s = logWrite (s ++ "\n")
+
+debugWrite s = hPutStr stderr s
+debugWriteLn s = debugWrite (s ++ "\n")
+
+dataFile = dataDir </> "wlpResults.txt"
+writeToDataFile items = appendFile dataFile $ (concat $ intersperse "," items) ++ "\n"
+
+-- ======================================================================
+-- Main functions to check a mutant vs orginal using wlp.
+-- ======================================================================
+
+-- Calculate the wlps of an orginal java method and its mutant, then compare them.
+-- Example:
+--
+-- rawCheckMutant Triangle mdir tritype1 ["returnValue==0", "returnValue==1"]
+--
+-- This will check the method tritype1 in subjects/src/Triangle.java vs mdir/Triangle.java
+--
+rawCheckMutant :: String -> FilePath -> String -> [String] -> IO (Maybe Bool)
+rawCheckMutant original mutantDir methodName postconds = do
+ let srcName = original ++ ".java"
+ let srcPath = subjectsDir </> srcName
+ let mutantPath = mutantDir </> srcName
+ (typeEnv1,decls1,methodNames1) <- parseJava srcPath
+ (typeEnv2,decls2,methodNames2) <- parseJava mutantPath
+
+ let mname = Ident methodName
+ 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 ]
+ logWriteLn ("## 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
+
+-- check all mutants of a single subject
+rawCheckAllMutants original mutantsRootDir methodName postconds = do
+ mdirs <- getMutantsSubdirs mutantsRootDir
+ let mdirs_ = [ mutantsRootDir </> d | d <- mdirs ]
+ results <- sequence [ rawCheckMutant original md methodName postconds | md <- mdirs_ ]
+ let killed = length $ filter (== Just False) results
+ debugWriteLn ("## " ++ original ++ "." ++ methodName ++ ", killed: " ++ show killed ++ "/" ++ show (length results))
+ return (zip mdirs results)
+ where
+ getMutantsSubdirs mutantsRootDir = do
+ fs <- listDirectory mutantsRootDir
+ let mdirs = [ name | name <- fs, not("." `isPrefixOf` name)
+ && unsafePerformIO (doesDirectoryExist (mutantsRootDir </> name))
+ ]
+ return mdirs
+
+
+checkAllMutants mode subjectClassName subjectMethodName postconds = do
+
+ let mutantsDir = if mode == "FN"
+ then majorMutantsDir </> subjectClassName
+ else handcraftedMutantsDir </> subjectClassName
+
+ results <- rawCheckAllMutants subjectClassName mutantsDir subjectMethodName postconds
+
+ let nmutants = length results
+ let killed = length $ filter (== Just False) $ map snd results
+ let undecided = length $ filter (== Nothing) $ map snd results
+ putStrLn ("** " ++ mode ++ " checking " ++ subjectClassName ++ "." ++ subjectMethodName ++ " on " ++ show nmutants ++ " mutants.")
+ putStrLn ("** Killed=" ++ show killed ++ ", Survived=" ++ show (nmutants - killed)
+ ++ " (incl. " ++ show undecided ++ " undecided)" )
+ let survivors = [ (m,r) | (m,r) <- results, not(r == Just False) ]
+ sequence_ [ putStrLn ("** Unable to kill mutant " ++ m ++ ", " ++ show r) | (m,r) <- survivors ]
+
+ writeToDataFile $ [ mode,
+ subjectClassName ++ "." ++ subjectMethodName,
+ show nmutants,
+ show killed,
+ show (nmutants - killed) ]
+ ++
+ map fst survivors
+
+
+
\ No newline at end of file
diff --git a/experiments/wermer2/generateMutants.sh b/experiments/wermer2/generateMutants.sh
index 4762757c7afe2349b7873ff3e230e28546f0e0ca..fb81ed5ae0ea69f07d206be61dde7a5abd4976c5 100755
--- a/experiments/wermer2/generateMutants.sh
+++ b/experiments/wermer2/generateMutants.sh
@@ -1,15 +1,19 @@
#!/bin/bash
+# Script to generate the source code of the mutants, which the wlp needs to do its analysis.
+#
+
# path to Major compiler:
MAJOR="../tools/major/bin/javac"
# Path to major mml compiler
MMLC="../tools/major/bin/mmlc"
-# The set and scope of mutations are specified in the file mutation.mml,
-# compile it first:
+# The set and scope of mutations are specified in the file mutation.mml, compile it first:
# $MMLC "./mutation.mml"
mutate(){
$MAJOR -J-Dmajor.export.directory="./mutants/generated/$1" -J-Dmajor.export.mutants=true -XMutator="./mutation.mml.bin" -cp "./subjects/bin" "./subjects/src/$1.java"
+ rm "./subjects/src/$1.class"
}
-mutate "Triangle"
\ No newline at end of file
+mutate "Triangle"
+mutate "MinsMaxs"
\ No newline at end of file
diff --git a/experiments/wermer2/mutation.mml b/experiments/wermer2/mutation.mml
index 8894557441c0009961e71d13a3a1557e78995925..1abb885a89f5ed2a19b71d87e291f5a33ab8c204 100644
--- a/experiments/wermer2/mutation.mml
+++ b/experiments/wermer2/mutation.mml
@@ -39,13 +39,13 @@ BIN(&&)->{==,LHS,RHS,FALSE};
BIN(||)->{!=,LHS,RHS,TRUE};
// Delete all types of supported statements
-//DEL(CALL); //don't do this...
+DEL(CALL);
DEL(INC);
DEL(DEC);
DEL(ASSIGN);
DEL(CONT);
DEL(BREAK);
-//DEL(RETURN); //don't do this...
+DEL(RETURN);
// Let's include all operators
myOp {
@@ -60,4 +60,8 @@ myOp {
}
// Specify scopes:
-myOp<"Triangle@tritype1" ;
+myOp<"Triangle@tritype1"> ;
+//myOp<"MinsMaxs@testme"> ;
+myOp<"MinsMaxs@getMinsMaxs"> ;
+
+
diff --git a/experiments/wermer2/subjects/src/MinsMaxs.java b/experiments/wermer2/subjects/src/MinsMaxs.java
new file mode 100644
index 0000000000000000000000000000000000000000..b922d8fb6d0b29dc6200cb5dad2ae4a4bf7b3ee8
--- /dev/null
+++ b/experiments/wermer2/subjects/src/MinsMaxs.java
@@ -0,0 +1,54 @@
+// package Examples.NN_InputVector;
+
+public class MinsMaxs {
+
+ /**
+ * Given an NxM matrix of double-values, calculate the minimum and maximum of every column in the matrix.
+ * The mins and maxs are returned as a pair of arrays.
+ */
+ static public double[][] getMinsMaxs(double[][] data) {
+
+ int N = data.length ;
+ if (N < 1) { throw new IllegalArgumentException() ; }
+ int rowWidth = data[0].length ;
+ // check if every row has the same length:
+ for (int r1=1; r1<N; r1++)
+ if (data[r1].length != rowWidth) { throw new IllegalArgumentException() ; }
+
+ double[] mins = new double[rowWidth] ;
+ double[] maxs = new double[rowWidth] ;
+ // initialize mins and maxs:
+ for (int c1=0; c1<rowWidth; c1++) {
+ mins[c1] =data[0][c1] ;
+ maxs[c1] =data[0][c1] ;
+ }
+ // iterate over the matrix:
+ for (int r=1; r<N; r++) {
+ for (int c=0; c<rowWidth; c++) {
+ if (data[r][c] <= mins[c]) { mins[c] = data[r][c] ; } // mutate this
+ if (data[r][c] >= maxs[c]) { maxs[c] = data[r][c] ; } // mutate this
+ }
+ }
+ double[][] output = new double[2][] ;
+ output[0] = mins ;
+ output[1] = maxs ;
+
+ return output ;
+ }
+
+
+ /*
+ static double[] testme(int m) {
+ double[] output = new double[2] ;
+ output[0] = 1 ;
+ output[1] = 2 ;
+ int k = 0 ;
+ while (k<m) {
+ if (k==10) throw new IllegalArgumentException() ;
+ k++ ;
+ }
+ return output ;
+ }
+ */
+
+}
diff --git a/experiments/wermer2/subjects/src/Triangle.java b/experiments/wermer2/subjects/src/Triangle.java
index f97f76c08da9ed2e176f6ae08fc67ddb8ce94d72..b5e7c53ec3cbda9b61f2dafddf44f91d7ca60064 100644
--- a/experiments/wermer2/subjects/src/Triangle.java
+++ b/experiments/wermer2/subjects/src/Triangle.java
@@ -12,16 +12,17 @@ public class Triangle {
// classify this triangle's type:
public int tritype1() {
- if ((this.x <= 0) || (this.y <= 0) || (this.z <= 0)) throw new IllegalArgumentException() ;
- if (this.x >= (this.y+this.z)) return -1 ; // not a triangle
- if (this.y >= (this.x+this.z)) return -1 ; // not a triangle
- if (this.z >= (this.x+this.y)) return -1 ; // not a triangle
- if ((this.x == this.y) && (this.y == this.z)) return 1 ; // equilateral
- if ((this.x == this.y) || (this.y == this.z) || (this.x == this.z)) return 2 ; // isoleces
+ if ((this.x <= 0) || (this.y <= 0) || (this.z <= 0)) { throw new IllegalArgumentException() ; }
+ if (this.x >= (this.y+this.z)) { return -1 ; } // not a triangle
+ if (this.y >= (this.x+this.z)) { return -1 ; } // not a triangle
+ if (this.z >= (this.x+this.y)) { return -1 ; } // not a triangle
+ if ((this.x == this.y) && (this.y == this.z)) { return 1 ; } // equilateral
+ if ((this.x == this.y) || (this.y == this.z) || (this.x == this.z)) { return 2 ; } // isoleces
return 0 ; // scalene
}
// static variation of tritype:
+ /*
static public int tritype2(float x, float y, float z) {
if ((x <= 0) || (y <= 0) || (z <= 0)) throw new IllegalArgumentException() ;
if (x >= (y+z)) return -1 ; // not a triangle
@@ -31,4 +32,5 @@ public class Triangle {
if ((x == y) || (y == z) || (x == z)) return 2 ; // isoleces
return 0 ; // scalene
}
+ */
}
diff --git a/src/Javawlp/Engine/WLP.hs b/src/Javawlp/Engine/WLP.hs
index 1a1de5c48d25c3bd448911fc76f32bd621649faa..fc9bd27a885f23ea628443792d449e426c5e824c 100644
--- a/src/Javawlp/Engine/WLP.hs
+++ b/src/Javawlp/Engine/WLP.hs
@@ -28,7 +28,9 @@ data WLPConf = WLPConf {
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
+ -- Wish: adding this attribute to handle "continue" commands:
+ cont :: Exp -> Exp, -- The accumulated transformer to handle the "continue" jump
+ catch :: Maybe ([(Catch, Exp->Exp)], 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
decls :: [TypeDecl], -- Class declarations
calls :: CallCount, -- The number of recursive calls per method
@@ -45,25 +47,58 @@ type Syn = Exp -> Exp -- The wlp transformer
-- Statements that pass control to the next statement have to explicitly combine their wlp function with the accumulated function, as some statements (e.g. break) ignore the accumulated function.
wlpStmtAlgebra :: StmtAlgebra (Inh -> Syn)
wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhancedFor, fEmpty, fExpStmt, fAssert, fSwitch, fDo, fBreak, fContinue, fReturn, fSynchronized, fThrow, fTry, fLabeled) where
- fStmtBlock (Block bs) inh = foldr (\b r -> wlpBlock inh {acc = r} b) (acc inh) bs -- The result of the last block-statement will be the accumulated transformer for the second-last etc. The type environment is build from the left, so it has to be done seperately.
+
+ -- The result of the last block-statement will be the accumulated transformer for the second-last etc.
+ -- The type environment is build from the left, so it has to be done seperately.
+ fStmtBlock (Block bs) inh = foldr (\b r -> wlpBlock inh{acc = r} b) (acc inh) bs
+
fIfThen e s1 = fIfThenElse e s1 acc -- if-then is just an if-then-else with an empty else-block
- fIfThenElse e s1 s2 inh = let (e', trans) = foldExp wlpExpAlgebra e inh {acc = id}
+ fIfThenElse e s1 s2 inh = let (e', trans) = foldExp wlpExpAlgebra e inh{acc = id}
var = getVar
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}
+
+ fWhile e s inh = let (e', trans) = foldExp wlpExpAlgebra e inh{acc = id}
var = getVar
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)
+ -- Wish: this seems to be wrong:
+ -- in (\q -> unrollLoopOpt inh{br = const q} numberOfUnrolling e' trans s q)
+ -- Fixing:
+ in (\q -> unrollLoopOpt inh{br = (\q'-> acc inh q)} numberOfUnrolling e' trans s q)
+
+ fBasicFor init me incr s inh = let
+ -- encode the for loop as a while-loop
+ -- loop below is the wlp-transformer over the loop without the initialization part:
+ loop = fWhile (fromMaybeGuard me) -- the guard
+ -- constructing s ; incr.
+ -- However, this looks to be wrong:
+ -- (\inh' -> s (inh'{acc = wlp' inh'{acc = id} (incrToStmt incr)}) )
+ -- Fixing to:
+ (\inh' -> s (inh'{acc = wlp' inh' (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
fExpStmt e inh = snd $ foldExp wlpExpAlgebra e inh
fAssert e _ inh = let (e', trans) = foldExp wlpExpAlgebra e inh {acc = id}
in (trans . (e' &*) . acc inh)
fSwitch e bs inh = let (e', s1, s2) = desugarSwitch e bs in fIfThenElse e' (flip wlp' s1) (flip wlp' s2) (inh {acc = id, br = acc inh})
- fDo s e inh = s (inh {acc = fWhile e s inh}) -- Do is just a while with the statement block executed one additional time. Break and continue still have to be handled in this additional execution.
+
+ fDo s e inh = -- Do is just a while with the statement block executed one additional time.
+ -- Break and continue still have to be handled in this additional execution.
+ let
+ whileTransf = fWhile e s inh
+ in
+ s (inh {acc = whileTransf, br = acc inh, cont = whileTransf })
+
fBreak _ inh = br inh -- wlp of the breakpoint. Control is passed to the statement after the loop
- fContinue _ inh = id -- at a continue statement it's as if the body of the loop is fully executed
+
+ -- Wish: his seems to be wrong
+ -- fContinue _ inh = id -- at a continue statement it's as if the body of the loop is fully executed
+ -- Fixing to:
+ fContinue _ inh = cont inh
+
fReturn me inh = case me of
Nothing -> id -- Return ignores acc, as it terminates the method
Just e -> fExpStmt (Assign (NameLhs (Name [fromJust' "fReturn" (ret inh)])) EqualA e) (inh {acc = id}) -- We treat "return e" as an assignment to a variable specifically created to store the return value in
@@ -71,12 +106,24 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
fSynchronized _ = fStmtBlock
fThrow e inh = (case catch inh of
Nothing -> ((\q -> q &* throwException e)) -- acc is ignored, as the rest of the block is not executed
- Just (cs, f) -> (maybe (if f then id else (\q -> q &* throwException e)) (flip fStmtBlock (inh {acc = id, catch = Nothing})) (getCatch (decls inh) (env inh) e cs)))
+ Just (cs, f) -> maybe (if f then id else (\q -> q &* throwException e))
+ {- (flip fStmtBlock (inh {acc = id, catch = Nothing})) -}
+ id
+ (getCatch (decls inh) (env inh) e cs)
+ )
.
(case ret inh of
Nothing -> id
_ -> fReturn (Just e) inh)
- fTry (Block bs) cs f inh = let r = (fStmtBlock (Block bs) (inh {acc = id, catch = Just (cs, isJust f)})) in (r . maybe (acc inh) (flip fStmtBlock inh) f) -- The finally-block is always executed
+ fTry (Block bs) cs f inh = let
+ finalyTranf = case f of
+ Nothing -> acc inh
+ Just b -> fStmtBlock b inh
+
+ csTransfs = [ fStmtBlock b inh{acc=finalyTranf} | Catch p b <- cs]
+ in
+ fStmtBlock (Block bs) inh{acc=finalyTranf, catch = Just (zip cs csTransfs, isJust f)}
+
fLabeled _ s = s
-- Helper functions
@@ -102,19 +149,20 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
unrollLoop inh 0 g gTrans _ = let var = getVar
-- in gTrans . substVar' inh var g . (neg (ExpName (Name [var])) `imp`) . acc inh
in gTrans . substVar' inh var g . (neg (ExpName (Name [var])) &*) . acc inh
- unrollLoop inh n g gTrans bodyTrans = let var = getVar
- -- in gTrans . substVar' inh var g . (\q -> (neg (ExpName (Name [var])) `imp` acc inh q) &* ((ExpName (Name [var])) `imp` bodyTrans inh {acc = (unrollLoop inh (n-1) g gTrans bodyTrans)} q))
- -- reformulating it as a disjunction rather than conjunction ; this should be equivalent
+ unrollLoop inh n g gTrans bodyTrans = let
+ var = getVar
+ nextUnrollingTrans = unrollLoop inh (n-1) g gTrans bodyTrans
in gTrans
. substVar' inh var g
. (\q -> (neg (ExpName (Name [var])) &* acc inh q)
|*
- ((ExpName (Name [var])) &* bodyTrans inh {acc = (unrollLoop inh (n-1) g gTrans bodyTrans)} q))
+ ((ExpName (Name [var])) &* bodyTrans inh{acc = nextUnrollingTrans, cont = nextUnrollingTrans} q))
-- An optimized version of unroll loop to reduce the size of the wlp
unrollLoopOpt :: Inh -> Int -> Exp -> (Exp -> Exp) -> (Inh -> Exp -> Exp) -> Exp -> Exp
- unrollLoopOpt inh n g gTrans bodyTrans q | gTrans (bodyTrans inh q) == acc inh q = acc inh q -- q is not affected by the loop
- | otherwise = unrollLoop inh n g gTrans bodyTrans q -- default to the standard version of unroll loop
+ unrollLoopOpt inh n g gTrans bodyTrans q
+ | gTrans (bodyTrans inh q) == acc inh q = acc inh q -- q is not affected by the loop
+ | otherwise = unrollLoop inh n g gTrans bodyTrans q -- default to the standard version of unroll loop
-- Converts initialization code of a for loop to a statement
initToStmt :: Maybe ForInit -> Stmt
@@ -152,16 +200,18 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
throwException :: Exp -> Exp
throwException e = false
-getCatch :: [TypeDecl] -> TypeEnv -> Exp -> [Catch] -> Maybe Block
+getCatch :: [TypeDecl] -> TypeEnv -> Exp -> [(Catch,Exp->Exp)] -> Maybe (Exp->Exp)
getCatch decls env e [] = Nothing
-getCatch decls env e (Catch p b:cs) = if catches decls env p e then Just b else getCatch decls env e cs
+getCatch decls env e ((Catch p b,transf):cs) = if catches decls env p e then Just transf else getCatch decls env e cs
-- Checks whether a catch block catches a certain error
catches :: [TypeDecl] -> TypeEnv -> FormalParam -> Exp -> Bool
-catches decls env (FormalParam _ t _ _) e = t == RefType (ClassRefType (ClassType [(Ident "Exception", [])])) ||
+catches decls env (FormalParam _ t _ _) e = True
+ {- t == RefType (ClassRefType (ClassType [(Ident "Exception", [])])) ||
case e of
ExpName name -> lookupType decls env name == t
InstanceCreation _ t' _ _ -> t == RefType (ClassRefType t')
+ -}
-- | The algebra that defines the wlp transformer for expressions with side effects
-- The first attribute is the expression itself (this is passed to handle substitutions in case of assignments)
@@ -251,7 +301,13 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
arrayAccessWlp a i inh q = case catch inh of
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))
+ 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) -}
+ (\transf-> transf q)
+ (getCatch (decls inh) (env inh) e cs))
dimLengths a = case a of
ArrayCreate t exps dim -> exps
@@ -344,7 +400,7 @@ wlp config decls = wlpWithEnv config decls []
-- | wlp with a given type environment
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_"]))))
+wlpWithEnv config decls env = wlp' (Inh config id id id Nothing env decls [] (Just (Ident "returnValue")) (Just (ExpName (Name [Ident "targetObj_"]))))
-- wlp' lets you specify the inherited attributes
wlp' :: Inh -> Stmt -> Syn