diff --git a/Daikon.hs b/Daikon.hs
new file mode 100644
index 0000000000000000000000000000000000000000..1061d0ecf2d3a506510f6bc885113f543d421e78
--- /dev/null
+++ b/Daikon.hs
@@ -0,0 +1,35 @@
+module Daikon where
+
+import Control.Monad
+import System.FilePath(joinPath)
+import System.Directory
+
+source, pathDir, packageDir, methodName :: String
+source = "GradientFunction"
+pathDir = "org/apache/commons/math3/analysis/differentiation"
+methodName = "value"
+
+packageDir = map (\c -> if c == '/' then '.' else c) pathDir
+
+-- Creates a shell script that checks the daikon invariants against all mutations for the current test file
+createDaikonScript :: IO ()
+createDaikonScript = do
+ writeFile scriptName ("#!/bin/sh\nHOME=\"T3Daikon\"\nSOURCE=\"" ++ source ++ "\"\nPATHDIR=\"" ++ pathDir ++ "\"\nPACKAGEDIR=\"" ++ packageDir ++ "\"\nMETHODNAME=\"" ++ methodName ++ "\"\n\n")
+
+ mutationFolders <- listDirectory (joinPath ["..", source ++ " mutants"])
+ checkMutants (length mutationFolders)
+
+ appendFile scriptName "read -p \"Press enter to continue\""
+
+
+scriptName :: FilePath
+scriptName = joinPath["..", "Daikon check inv " ++ source ++ ".sh"]
+
+-- Adds the code to check the mutants
+checkMutants :: Int -> IO ()
+checkMutants 0 = return ()
+checkMutants n = do
+ appendFile scriptName ("echo \"compiling mutation " ++ show n ++ "..\"\njavac -cp \".;wlp/Tests/\" -d \"wlp/Tests\" \"$SOURCE mutants/" ++ show n ++ "/$PATHDIR/$SOURCE.java\"\n\n")
+ appendFile scriptName ("echo \"generating test suite\"\njava -cp \".;$HOME/KWT3daikon.jar;$HOME/libs/T3.jar;$HOME/libs/T3Daikon.jar;wlp/tests\" MyT3Daikon.Generator wlp/tests $PACKAGEDIR.$SOURCE $METHODNAME 50 1000 \"Daikon test suites/$SOURCE\"\n\n")
+ appendFile scriptName ("echo \"checking invariants " ++ show n ++ "..\"\njava -cp \".;$HOME/KWT3daikon.jar;$HOME/libs/T3.jar;$HOME/libs/T3Daikon.jar;wlp/Tests\" MyT3Daikon.Miner -check \"Daikon test suites/$SOURCE.tr\" $METHODNAME \"Daikon invariants/$SOURCE\"\n\n")
+ checkMutants (n-1)
\ No newline at end of file
diff --git a/Equivalent mutations/Mutants/Vector_R1.java b/Equivalent mutations/Mutants/Vector_R1.java
index 2878703f427815c49e4bab0777c780be081a317c..88710aecb92eb20aa487422b663c6b63b9e8e895 100644
--- a/Equivalent mutations/Mutants/Vector_R1.java
+++ b/Equivalent mutations/Mutants/Vector_R1.java
@@ -23,12 +23,15 @@ public class Vector {
* R1 replaces the return in the INPRODUCT-case with a break.
*/
public Vector combine(int operation, Vector Z) {
+ int ACCUMULATE = 1;
+ int INPRODUCT = 2;
+ int PLUS = 3;
if (Z.getSize() != this.vector.length) throw new IllegalArgumentException() ;
double[] result = new double[this.vector.length] ;
double[] vector2 = Z.getVector() ;
switch (operation) {
- case VectorCONST.ACCUMULATE: ; // does nothing, deliberately falling through to the code of INPRODUCT
- case VectorCONST.INPRODUCT: {
+ case ACCUMULATE: ; // does nothing, deliberately falling through to the code of INPRODUCT
+ case INPRODUCT: {
int r = 0 ;
for (int k1=0; k1<this.vector.length; k1++) r += this.vector[k1]*vector2[k1] ;
double[] rr = new double[1];
@@ -36,7 +39,7 @@ public class Vector {
result = rr ;
break ;
}
- case VectorCONST.PLUS: {
+ case PLUS: {
for (int k2=0; k2<this.vector.length; k2++) result[k2] = this.vector[k2] + vector2[k2] ;
break ;
}
diff --git a/Equivalent mutations/Mutants/Vector_R2.java b/Equivalent mutations/Mutants/Vector_R2.java
index 2ed6569c7a036a5e8f5daae2465b1fd1cc5aae92..7fb421648dd1d5465b168bf39cc83d58c10224de 100644
--- a/Equivalent mutations/Mutants/Vector_R2.java
+++ b/Equivalent mutations/Mutants/Vector_R2.java
@@ -23,19 +23,22 @@ public class Vector {
* R2 replaces the fall through in the ACCUMULATE case with a recursive call with INPRODUCT.
*/
public Vector combine(int operation, Vector Z) {
+ int ACCUMULATE = 1;
+ int INPRODUCT = 2;
+ int PLUS = 3;
if (Z.getSize() != this.vector.length) throw new IllegalArgumentException() ;
double[] result = new double[this.vector.length] ;
double[] vector2 = Z.getVector() ;
switch (operation) {
- case VectorCONST.ACCUMULATE: return this.combine(VectorCONST.INPRODUCT,Z) ;
- case VectorCONST.INPRODUCT: {
+ case ACCUMULATE: return this.combine(INPRODUCT,Z) ;
+ case INPRODUCT: {
int r = 0 ;
for (int k1=0; k1<this.vector.length; k1++) r += this.vector[k1]*vector2[k1] ;
double[] rr = new double[1];
rr[0] = r;
return new Vector(rr) ;
}
- case VectorCONST.PLUS: {
+ case PLUS: {
for (int k2=0; k2<this.vector.length; k2++) result[k2] = this.vector[k2] + vector2[k2] ;
break ;
}
diff --git a/Equivalent mutations/Mutants/Vector_R3.java b/Equivalent mutations/Mutants/Vector_R3.java
index 2e384ef5c3583803130167c769c54f372eadade5..715a74d0220bdccaeaee3116b86c98658fb404fc 100644
--- a/Equivalent mutations/Mutants/Vector_R3.java
+++ b/Equivalent mutations/Mutants/Vector_R3.java
@@ -23,17 +23,20 @@ public class Vector {
* R3 reorder the cases, and remove the use of return from the case arms.
*/
public Vector combine(int operation, Vector Z) {
+ int ACCUMULATE = 1;
+ int INPRODUCT = 2;
+ int PLUS = 3;
if (Z.getSize() != this.vector.length) throw new IllegalArgumentException() ;
double[] result = new double[this.vector.length] ;
double[] vector2 = Z.getVector() ;
Vector resultingVector = null ;
switch (operation) {
- case VectorCONST.PLUS: {
+ case PLUS: {
for (int k1=0; k1<this.vector.length; k1++) result[k1] = this.vector[k1] + vector2[k1] ;
resultingVector = new Vector(result) ;
break ; }
- case VectorCONST.ACCUMULATE: ; // does nothing, deliberately falling through to the code of INPRODUCT
- case VectorCONST.INPRODUCT: {
+ case ACCUMULATE: ; // does nothing, deliberately falling through to the code of INPRODUCT
+ case INPRODUCT: {
int r = 0 ;
for (int k2=0; k2<this.vector.length; k2++) r += this.vector[k2]*vector2[k2] ;
double[] rr = new double[1];
diff --git a/Equivalent mutations/Vector.java b/Equivalent mutations/Vector.java
index fe437b89a7bd77d0a7bc66fb8a2f471e41285018..a091323843eaa8e25c9db8970d3515ed9f7196f0 100644
--- a/Equivalent mutations/Vector.java
+++ b/Equivalent mutations/Vector.java
@@ -19,19 +19,22 @@ public class Vector {
public int getSize() { return this.vector.length ; }
public Vector combine(int operation, Vector Z) {
+ int ACCUMULATE = 1;
+ int INPRODUCT = 2;
+ int PLUS = 3;
if (Z.getSize() != this.vector.length) throw new IllegalArgumentException() ;
double[] result = new double[this.vector.length] ;
double[] vector2 = Z.getVector() ;
switch (operation) {
- case VectorCONST.ACCUMULATE: ; // does nothing, deliberately falling through to the code of INPRODUCT
- case VectorCONST.INPRODUCT: {
+ case ACCUMULATE: ; // does nothing, deliberately falling through to the code of INPRODUCT
+ case INPRODUCT: {
int r = 0 ;
for (int k1=0; k1<this.vector.length; k1++) r += this.vector[k1]*vector2[k1] ;
double[] rr = new double[1];
rr[0] = r;
return new Vector(rr) ;
}
- case VectorCONST.PLUS: {
+ case PLUS: {
for (int k2=0; k2<this.vector.length; k2++) result[k2] = this.vector[k2] + vector2[k2] ;
break ;
}
diff --git a/HelperFunctions.hs b/HelperFunctions.hs
index 2a278eaedb0add096fcb735bb65d6f64ca2d6d73..24608a2a4583c93f9acc8c76b0ffc92196b30077 100644
--- a/HelperFunctions.hs
+++ b/HelperFunctions.hs
@@ -58,12 +58,17 @@ getMethodClassType decls id = head $ concatMap (flip getMethodTypeFromClassDecl
extendEnv :: TypeEnv -> [TypeDecl] -> Ident -> TypeEnv
extendEnv env decls methodId = case getMethodType decls methodId of
Nothing -> (Name [Ident "*obj"], getMethodClassType decls methodId) : env
+ Just (RefType _) -> (Name [Ident "returnValue"], returnValueType) : (Name [Ident "returnValueVar"], returnValueType) : (Name [Ident "*obj"], getMethodClassType decls methodId) : env
Just t -> (Name [Ident "returnValue"], t) : (Name [Ident "returnValueVar"], t) : (Name [Ident "*obj"], getMethodClassType decls methodId) : env
-- | Creates a string that that represents the return var name of a method call. This name is extended by a number to indicate the depth of the recursive calls
makeReturnVarName :: Ident -> String
makeReturnVarName (Ident s) = "$" ++ s ++ "$"
+-- | We introduce a special type for the return value,
+returnValueType :: Type
+returnValueType = RefType (ClassRefType (ClassType [(Ident "ReturnValueType", [])]))
+
-- | Get's the type of a generated variable
getReturnVarType :: [TypeDecl] -> String -> Type
getReturnVarType decls s = case getMethodType decls (Ident (takeWhile (/= '$') (tail s))) of
diff --git a/Main.hs b/Main.hs
index d3bf36fb7a3f078d89a1f0b3741fac27ae1a4671..e65ad46029a1a92793bcb9bb888bf608bd62796b 100644
--- a/Main.hs
+++ b/Main.hs
@@ -19,7 +19,7 @@ import Settings
sourcePath, mutantsDir, resultsPath :: FilePath
sourcePath = joinPath ["Tests", testFile ++ ".java"]
mutantsDir = joinPath ["..", testFile ++ " mutants"]
-resultsPath = joinPath ["Results", testFile ++ "_" ++ postCondVoid ++ "_" ++ postCondRefType ++ "_" ++ postCondPrimType ++ "_" ++ show ignoreLibMethods ++ "_" ++ show ignoreMainMethod ++ "_" ++ show nrOfUnroll]
+resultsPath = joinPath ["Results", testFile ++ "_" ++ postCondVoid ++ "_" ++ postCondRefType ++ "_" ++ postCondPrimType ++ "_" ++ show ignoreLibMethods ++ "_" ++ show ignoreMainMethod ++ "_" ++ show nrOfUnroll ++ if eitherWay then "_either way" else ""]
-- The main functions performs the mutation test on the test file, given that the mutations of the source are already created in the right location
main :: IO ()
@@ -110,7 +110,7 @@ compareWlps results env decls s (path, s') = do
where
compareMethod (ident, e) = case lookup ident s' of
Nothing -> putStrLn ("The method \'" ++ prettyPrint ident ++ "\' is missing in mutation " ++ path) >> return 0 -- print a warning and return 0 errors found
- Just e' -> if unsafeIsTrue (extendEnv env decls ident) decls (e `imp` e') then return 0 else printAndAppend results (path ++ " " ++ prettyPrint ident) >> return 1 -- print a message and return 1 error found
+ Just e' -> if unsafeIsTrue (extendEnv env decls ident) decls (if eitherWay then (e `imp` e') |* (e' `imp` e) else (e `imp` e')) then return 0 else printAndAppend results (path ++ " " ++ prettyPrint ident) >> return 1 -- print a message and return 1 error found
-- Gets the right post-condition given the type of a method
getPostCond :: Maybe Type -> Exp
@@ -136,7 +136,7 @@ getMutantNumber path = takeWhile (/= '\\') (path \\ (mutantsDir ++ "\\"))
-- Performs the false-positives-test on the set of test programs with equivalent mutations
testFalsePositives :: IO ()
testFalsePositives = do
- let results = joinPath ["Results", "False Positives", postCondVoid ++ "_" ++ postCondRefType ++ "_" ++ postCondPrimType ++ "_" ++ show ignoreLibMethods ++ "_" ++ show ignoreMainMethod ++ "_" ++ show nrOfUnroll]
+ let results = joinPath ["Results", "False Positives", postCondVoid ++ "_" ++ postCondRefType ++ "_" ++ postCondPrimType ++ "_" ++ show ignoreLibMethods ++ "_" ++ show ignoreMainMethod ++ "_" ++ show nrOfUnroll ++ if eitherWay then "_either way" else ""]
-- Create the file for the results
writeFile results ("False positives test")
diff --git a/Results/False Positives/true_returnValue != null_returnValueVar == returnValue_False_False_1 b/Results/False Positives/true_returnValue != null_returnValueVar == returnValue_False_False_1
index 15d8186ff113a1b9691e82c4580f8bddce36824f..a7be12d8e1ad41f47b7c7fee4097c05084c8b3d7 100644
--- a/Results/False Positives/true_returnValue != null_returnValueVar == returnValue_False_False_1
+++ b/Results/False Positives/true_returnValue != null_returnValueVar == returnValue_False_False_1
@@ -7,5 +7,4 @@ ignoreMainMethod: False
nrOfUnroll: 1
False positives found in:
Equivalent mutations\Mutants\Vector_R2.java combine
-Equivalent mutations\Mutants\Vector_R3.java combine
-Total number of false positives: 2
\ No newline at end of file
+Total number of false positives: 1
\ No newline at end of file
diff --git a/Results/False Positives/true_returnValue != null_true_False_False_1 b/Results/False Positives/true_returnValue != null_true_False_False_1
index 09c9e4283ecb6b19cc732908b90d71948ccbab74..f91b1643600048448167684913955309f886f17f 100644
--- a/Results/False Positives/true_returnValue != null_true_False_False_1
+++ b/Results/False Positives/true_returnValue != null_true_False_False_1
@@ -7,5 +7,4 @@ ignoreMainMethod: False
nrOfUnroll: 1
False positives found in:
Equivalent mutations\Mutants\Vector_R2.java combine
-Equivalent mutations\Mutants\Vector_R3.java combine
-Total number of false positives: 2
\ No newline at end of file
+Total number of false positives: 1
\ No newline at end of file
diff --git a/Results/basesecantsolver_true_returnValue != null_returnValueVar == returnValue_False_False_1 b/Results/basesecantsolver_true_returnValue != null_returnValueVar == returnValue_False_False_1
index 2521dc090f46d95cebfe6032b9eccc561438ef46..ad587ee9f1a46ceed235c38aef0961dad8f61f04 100644
--- a/Results/basesecantsolver_true_returnValue != null_returnValueVar == returnValue_False_False_1
+++ b/Results/basesecantsolver_true_returnValue != null_returnValueVar == returnValue_False_False_1
@@ -5,30 +5,4 @@ postCondPrimType: returnValueVar == returnValue
ignoreLibMethods: False
ignoreMainMethod: False
nrOfUnroll: 1
-erronous mutations detected:
-206 verifyBracketing
-200 verifyInterval1
-200 verifySequence1
-200 verifyBracketing
-197 isSequence1
-196 isSequence1
-195 isSequence1
-194 isSequence1
-193 isSequence1
-192 isSequence1
-191 isSequence1
-190 isSequence1
-189 isSequence1
-188 isSequence1
-152 midpoint
-151 midpoint
-150 midpoint
-149 midpoint
-148 midpoint
-147 midpoint
-146 midpoint
-145 midpoint
-144 midpoint
-143 midpoint
-Total number of mutants: 207
-Number of mutants in which we found an error: 22
\ No newline at end of file
+erronous mutations detected:
\ No newline at end of file
diff --git a/Settings.hs b/Settings.hs
index cb8f58de15de0c0a3b266b5914d09df822edb6c9..362dc7bfb8c14e090754f0219afc6b0648c182f3 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -8,7 +8,7 @@ testFile = test3
-- The post condition may depend on the type of the method we are looking at
postCondVoid = "true"
postCondRefType = heur1
-postCondPrimType = heur0
+postCondPrimType = heur2
-- When ignoreLibMethods is true, library calls will simply be ignored. When false, we consider library methods but make no assumptions about them (so the WLP will be true)
-- To prevent insanely long calculation times, we may decide to not calculate the wlp of the main method when ignoring library methods
@@ -16,6 +16,9 @@ ignoreLibMethods, ignoreMainMethod :: Bool
ignoreLibMethods = False -- No longer supported
ignoreMainMethod = False
+-- If true, we accept mutations that satisfy either diraction of the implication, if false mutation must satisfy WLP(S, Q) => WLP(S', Q), where S' is the mutation.
+-- This does not seem to catch any mutations at all
+eitherWay = False
nrOfUnroll :: Int
nrOfUnroll = 1
diff --git a/Tests/BaseSecantSolver$1.class b/Tests/BaseSecantSolver$1.class
deleted file mode 100644
index bec0ed2fba45f003679dbdd52cc1df95e176387f..0000000000000000000000000000000000000000
Binary files a/Tests/BaseSecantSolver$1.class and /dev/null differ
diff --git a/Tests/BaseSecantSolver$Method.class b/Tests/BaseSecantSolver$Method.class
deleted file mode 100644
index 2c436a53bcdc9bc2c78059d3eeba86dc646cff4e..0000000000000000000000000000000000000000
Binary files a/Tests/BaseSecantSolver$Method.class and /dev/null differ
diff --git a/Tests/BaseSecantSolver.class b/Tests/BaseSecantSolver.class
deleted file mode 100644
index 2bb94aed62ecc60b5a296eeb85e071bb882e16da..0000000000000000000000000000000000000000
Binary files a/Tests/BaseSecantSolver.class and /dev/null differ
diff --git a/Tests/GradientFunction.class b/Tests/GradientFunction.class
deleted file mode 100644
index 8648b1d5a58f7ba2bed2dc561cb18398a6673006..0000000000000000000000000000000000000000
Binary files a/Tests/GradientFunction.class and /dev/null differ
diff --git a/Tests/Iterator.class b/Tests/Iterator.class
deleted file mode 100644
index a209b6b574657a7ac5db7235255a081371c700f4..0000000000000000000000000000000000000000
Binary files a/Tests/Iterator.class and /dev/null differ
diff --git a/WLP.hs b/WLP.hs
index c4dc1f60c25f8336385e1dcbe5ed1953d5178eb1..41f368b9002cfd4a95d2e55dc9a5cb56fa183fa5 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -116,12 +116,13 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
-- Converts a switch into nested if-then-else statements. The switch is assumed to be non-trivial.
desugarSwitch :: Exp -> [SwitchBlock] -> (Exp, Stmt, Stmt)
desugarSwitch e [SwitchBlock l bs] = case l of
- SwitchCase e' -> (BinOp e Equal e', StmtBlock (Block bs), Empty)
- Default -> (true, StmtBlock (Block bs), Empty)
+ SwitchCase e' -> (BinOp e Equal e', StmtBlock (Block (addBreak bs)), Break Nothing)
+ Default -> (true, StmtBlock (Block (addBreak bs)), Empty)
+ where addBreak bs = bs ++ [BlockStmt (Break Nothing)] -- Adds an explicit break statement add the end of a block (used for the final block)
desugarSwitch e sbs@(SwitchBlock l bs:sbs') = case l of
SwitchCase e' -> (BinOp e Equal e', StmtBlock (switchBlockToBlock sbs), otherCases)
Default -> (true, StmtBlock (switchBlockToBlock sbs), otherCases)
- where otherCases = let (e', s1, s2) = desugarSwitch e sbs' in IfThenElse e' s1 s2
+ where otherCases = let (e', s1, s2) = desugarSwitch e sbs' in IfThenElse e' s1 s2
-- Gets the statements from a switch statement
switchBlockToBlock :: [SwitchBlock] -> Block