From 1e590561f9fdc3069070c3800b8306a3841c2049 Mon Sep 17 00:00:00 2001
From: Koen Wermer <koenwermer@gmail.com>
Date: Tue, 14 Feb 2017 21:22:05 +0100
Subject: [PATCH] checked wishnu's mutations and applies manual
preprocessing/desugaring where needed. Also fixed a bug where introduced
variables in the wlp would result in an error (introduced variables may be
part of the wlp when the code contains non-void functions that don't
terminate within the set limit of iterations)
---
Equivalent mutations/MinsMaxs.java | 10 +-
Equivalent mutations/Mutants/MinsMaxs_R1.java | 10 +-
Equivalent mutations/Mutants/MinsMaxs_R2.java | 6 +-
Equivalent mutations/Mutants/MinsMaxs_R3.java | 10 +-
.../Mutants/Normalizer_R2.java | 2 +-
Equivalent mutations/Mutants/Vector_R1.java | 17 +-
Equivalent mutations/Mutants/Vector_R2.java | 19 +-
Equivalent mutations/Mutants/Vector_R3.java | 19 +-
Equivalent mutations/Vector.java | 7 +-
HelperFunctions.hs | 2 +-
Main.hs | 5 +-
...eturnValueVar == returnValue_False_False_1 | 11 +
.../true_true_true_False_False_1 | 9 +
Settings.hs | 4 +-
Tests/OpenIntToDoubleHashMap.java | 608 ------------------
Tests/{ => simple tests}/arrays1.class | Bin
Tests/{ => simple tests}/arrays1.java | 0
Verifier.hs | 35 +-
18 files changed, 99 insertions(+), 675 deletions(-)
create mode 100644 Results/False Positives/true_returnValue != null_returnValueVar == returnValue_False_False_1
create mode 100644 Results/False Positives/true_true_true_False_False_1
delete mode 100644 Tests/OpenIntToDoubleHashMap.java
rename Tests/{ => simple tests}/arrays1.class (100%)
rename Tests/{ => simple tests}/arrays1.java (100%)
diff --git a/Equivalent mutations/MinsMaxs.java b/Equivalent mutations/MinsMaxs.java
index d1808c8..4c91968 100644
--- a/Equivalent mutations/MinsMaxs.java
+++ b/Equivalent mutations/MinsMaxs.java
@@ -11,15 +11,15 @@ public class MinsMaxs {
if (N < 1) throw new IllegalArgumentException() ;
int rowWidth = data[0].length ;
// check if every row has the same length:
- for (int r=1; r<N; r++)
- if (data[r].length != rowWidth) throw new IllegalArgumentException() ;
+ 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 c=0; c<rowWidth; c++) {
- mins[c] =data[0][c] ;
- maxs[c] =data[0][c] ;
+ 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++) {
diff --git a/Equivalent mutations/Mutants/MinsMaxs_R1.java b/Equivalent mutations/Mutants/MinsMaxs_R1.java
index 3cb0511..fd690dd 100644
--- a/Equivalent mutations/Mutants/MinsMaxs_R1.java
+++ b/Equivalent mutations/Mutants/MinsMaxs_R1.java
@@ -10,15 +10,15 @@ public class MinsMaxs_R1 {
if (N < 1) throw new IllegalArgumentException() ;
int rowWidth = data[0].length ;
// check if every row has the same lenght:
- for (int r=1; r<N; r++)
- if (data[r].length != rowWidth) throw new IllegalArgumentException() ;
+ 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 c=0; c<rowWidth; c++) {
- mins[c] =data[0][c] ;
- maxs[c] =data[0][c] ;
+ 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<data.length; r++) {
diff --git a/Equivalent mutations/Mutants/MinsMaxs_R2.java b/Equivalent mutations/Mutants/MinsMaxs_R2.java
index 1603f1d..dc29b8a 100644
--- a/Equivalent mutations/Mutants/MinsMaxs_R2.java
+++ b/Equivalent mutations/Mutants/MinsMaxs_R2.java
@@ -14,9 +14,9 @@ public class MinsMaxs_R2 {
double[] maxs = new double[rowWidth] ;
// initialize mins and maxs:
- for (int c=0; c<rowWidth; c++) {
- mins[c] =data[0][c] ;
- maxs[c] =data[0][c] ;
+ 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<data.length; r++) {
diff --git a/Equivalent mutations/Mutants/MinsMaxs_R3.java b/Equivalent mutations/Mutants/MinsMaxs_R3.java
index d89b304..ed365d2 100644
--- a/Equivalent mutations/Mutants/MinsMaxs_R3.java
+++ b/Equivalent mutations/Mutants/MinsMaxs_R3.java
@@ -10,15 +10,15 @@ public class MinsMaxs_R3 {
if (N < 1) throw new IllegalArgumentException() ;
int rowWidth = data[0].length ;
// check if every row has the same length:
- for (int r=1; r<N; r++)
- if (data[r].length != rowWidth) throw new IllegalArgumentException() ;
+ 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 c=0; c<rowWidth; c++) {
- mins[c] =data[0][c] ;
- maxs[c] =data[0][c] ;
+ for (int c1=0; c1<rowWidth; c1++) {
+ mins[c1] =data[0][c1] ;
+ maxs[c1] =data[0][c1] ;
}
// iterate over the matrix:
for (int c=0; c<rowWidth; c++) {
diff --git a/Equivalent mutations/Mutants/Normalizer_R2.java b/Equivalent mutations/Mutants/Normalizer_R2.java
index 782e1f5..4fb494a 100644
--- a/Equivalent mutations/Mutants/Normalizer_R2.java
+++ b/Equivalent mutations/Mutants/Normalizer_R2.java
@@ -13,7 +13,7 @@ public class Normalizer_R2 {
if (data[row].length != rowWidth) { throw new IllegalArgumentException() ; }
int col = 0 ;
while (col < rowWidth) {
- data[row][col] = normalizeValue(data[row][col] ,mins[col],maxs[col]) ;
+ data[row][col] = this.normalizeValue(data[row][col] ,mins[col],maxs[col]) ;
col++ ;
}
row++ ;
diff --git a/Equivalent mutations/Mutants/Vector_R1.java b/Equivalent mutations/Mutants/Vector_R1.java
index 47bc86f..2878703 100644
--- a/Equivalent mutations/Mutants/Vector_R1.java
+++ b/Equivalent mutations/Mutants/Vector_R1.java
@@ -1,15 +1,15 @@
package Examples.NN_InputVector;
-public class Vector_R1 {
+public class Vector {
private double[] vector;
- public Vector_R1(double[] vec) {
+ public Vector(double[] vec) {
this.vector = new double[vec.length] ;
System.arraycopy(vec, 0, this.vector, 0, vec.length);
}
- public double[] getVector() {
+ public double[] getVector() {
int N = this.vector.length ;
double[] V = new double[N] ;
for (int k=0; k<N; k++) V[k] = this.vector[k] ;
@@ -22,7 +22,7 @@ public class Vector_R1 {
/**
* R1 replaces the return in the INPRODUCT-case with a break.
*/
- public Vector_R1 combine_R1(int operation, Vector_R1 Z) {
+ public Vector combine(int operation, Vector Z) {
if (Z.getSize() != this.vector.length) throw new IllegalArgumentException() ;
double[] result = new double[this.vector.length] ;
double[] vector2 = Z.getVector() ;
@@ -30,18 +30,19 @@ public class Vector_R1 {
case VectorCONST.ACCUMULATE: ; // does nothing, deliberately falling through to the code of INPRODUCT
case VectorCONST.INPRODUCT: {
int r = 0 ;
- for (int k=0; k<this.vector.length; k++) r += this.vector[k]*vector2[k] ;
- double[] rr = {r} ;
+ for (int k1=0; k1<this.vector.length; k1++) r += this.vector[k1]*vector2[k1] ;
+ double[] rr = new double[1];
+ rr[0] = r;
result = rr ;
break ;
}
case VectorCONST.PLUS: {
- for (int k=0; k<this.vector.length; k++) result[k] = this.vector[k] + vector2[k] ;
+ for (int k2=0; k2<this.vector.length; k2++) result[k2] = this.vector[k2] + vector2[k2] ;
break ;
}
default: return null ;
}
- return new Vector_R1(result) ;
+ return new Vector(result) ;
}
}
diff --git a/Equivalent mutations/Mutants/Vector_R2.java b/Equivalent mutations/Mutants/Vector_R2.java
index 532e278..2ed6569 100644
--- a/Equivalent mutations/Mutants/Vector_R2.java
+++ b/Equivalent mutations/Mutants/Vector_R2.java
@@ -1,10 +1,10 @@
package Examples.NN_InputVector;
-public class Vector_R2 {
+public class Vector {
private double[] vector;
- public Vector_R2(double[] vec) {
+ public Vector(double[] vec) {
this.vector = new double[vec.length] ;
System.arraycopy(vec, 0, this.vector, 0, vec.length);
}
@@ -22,25 +22,26 @@ public class Vector_R2 {
/**
* R2 replaces the fall through in the ACCUMULATE case with a recursive call with INPRODUCT.
*/
- public Vector_R2 combine_R2(int operation, Vector_R2 Z) {
+ public Vector combine(int operation, Vector Z) {
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 combine_R2(VectorCONST.INPRODUCT,Z) ;
+ case VectorCONST.ACCUMULATE: return this.combine(VectorCONST.INPRODUCT,Z) ;
case VectorCONST.INPRODUCT: {
int r = 0 ;
- for (int k=0; k<this.vector.length; k++) r += this.vector[k]*vector2[k] ;
- double[] rr = {r} ;
- return new Vector_R2(rr) ;
+ 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: {
- for (int k=0; k<this.vector.length; k++) result[k] = this.vector[k] + vector2[k] ;
+ for (int k2=0; k2<this.vector.length; k2++) result[k2] = this.vector[k2] + vector2[k2] ;
break ;
}
default: return null ;
}
- return new Vector_R2(result) ;
+ return new Vector(result) ;
}
}
diff --git a/Equivalent mutations/Mutants/Vector_R3.java b/Equivalent mutations/Mutants/Vector_R3.java
index 4982918..2e384ef 100644
--- a/Equivalent mutations/Mutants/Vector_R3.java
+++ b/Equivalent mutations/Mutants/Vector_R3.java
@@ -1,10 +1,10 @@
package Examples.NN_InputVector;
-public class Vector_R3 {
+public class Vector {
private double[] vector;
- public Vector_R3(double[] vec) {
+ public Vector(double[] vec) {
this.vector = new double[vec.length] ;
System.arraycopy(vec, 0, this.vector, 0, vec.length);
}
@@ -22,22 +22,23 @@ public class Vector_R3 {
/**
* R3 reorder the cases, and remove the use of return from the case arms.
*/
- public Vector_R3 combine_R3(int operation, Vector_R3 Z) {
+ public Vector combine(int operation, Vector Z) {
if (Z.getSize() != this.vector.length) throw new IllegalArgumentException() ;
double[] result = new double[this.vector.length] ;
double[] vector2 = Z.getVector() ;
- Vector_R3 resultingVector = null ;
+ Vector resultingVector = null ;
switch (operation) {
case VectorCONST.PLUS: {
- for (int k=0; k<this.vector.length; k++) result[k] = this.vector[k] + vector2[k] ;
- resultingVector = new Vector_R3(result) ;
+ 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: {
int r = 0 ;
- for (int k=0; k<this.vector.length; k++) r += this.vector[k]*vector2[k] ;
- double[] rr = {r} ;
- resultingVector = new Vector_R3(rr) ; // we will just let it fall through
+ for (int k2=0; k2<this.vector.length; k2++) r += this.vector[k2]*vector2[k2] ;
+ double[] rr = new double[1];
+ rr[0] = r;
+ resultingVector = new Vector(rr) ; // we will just let it fall through
}
default: ;
}
diff --git a/Equivalent mutations/Vector.java b/Equivalent mutations/Vector.java
index fedb202..fe437b8 100644
--- a/Equivalent mutations/Vector.java
+++ b/Equivalent mutations/Vector.java
@@ -26,12 +26,13 @@ public class Vector {
case VectorCONST.ACCUMULATE: ; // does nothing, deliberately falling through to the code of INPRODUCT
case VectorCONST.INPRODUCT: {
int r = 0 ;
- for (int k=0; k<this.vector.length; k++) r += this.vector[k]*vector2[k] ;
- double[] rr = {r} ;
+ 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: {
- for (int k=0; k<this.vector.length; k++) result[k] = this.vector[k] + vector2[k] ;
+ for (int k2=0; k2<this.vector.length; k2++) result[k2] = this.vector[k2] + vector2[k2] ;
break ;
}
default: return null ;
diff --git a/HelperFunctions.hs b/HelperFunctions.hs
index 3580e2a..2a278ea 100644
--- a/HelperFunctions.hs
+++ b/HelperFunctions.hs
@@ -18,7 +18,7 @@ lookupType decls env (Name ((Ident s@('$':_)) : idents)) = getFieldType decls (g
lookupType decls env (Name ((Ident s@('#':_)) : idents)) = PrimType undefined -- Names starting with a '#' symbol are generated and represent a variable introduced by handling operators
lookupType decls env (Name idents) = case lookup (Name [head idents]) env of
Just t -> getFieldType decls t (Name (tail idents))
- Nothing -> error ("can't find type of " ++ prettyPrint (Name idents) ++ "\r\n TypeEnv: " ++ show env)
+ Nothing -> PrimType IntT -- For now we assume library variables to be ints error ("can't find type of " ++ prettyPrint (Name idents) ++ "\r\n TypeEnv: " ++ show env)
-- | Gets the type of a field of an object of given type
getFieldType :: [TypeDecl] -> Type -> Name -> Type
diff --git a/Main.hs b/Main.hs
index 6f952b3..7ca126b 100644
--- a/Main.hs
+++ b/Main.hs
@@ -151,8 +151,11 @@ testFalsePositives = do
n1 <- testFalsePositives' results "BST.java" ["BST_no_parent.java"]
n2 <- testFalsePositives' results "Fibonacci.java" ["Fibonacci_no_extra_prints.java"]
n3 <- testFalsePositives' results "Stack.java" ["Stack_bool_is_result.java", "Stack_constructor_duplication.java", "Stack_useless_property.java"]
+ n4 <- testFalsePositives' results "MinsMaxs.java" ["MinsMaxs_R1.java", "MinsMaxs_R2.java", "MinsMaxs_R3.java"]
+ n5 <- testFalsePositives' results "Normalizer.java" ["Normalizer_R1.java", "Normalizer_R2.java", "Normalizer_R3.java", "Normalizer_R4.java"]
+ n6 <- testFalsePositives' results "Vector.java" ["Vector_R1.java", "Vector_R2.java", "Vector_R3.java"]
- printAndAppend results ("Total number of false positives: " ++ show (n1 + n2 + n3))
+ printAndAppend results ("Total number of false positives: " ++ show (n1 + n2 + n3 + n4 + n5 + n6))
where
testFalsePositives' :: FilePath -> FilePath -> [FilePath] -> IO Int
testFalsePositives' results source mutations = testFalsePositives'' results (joinPath ["Equivalent mutations", source]) (map (\mutant -> joinPath ["Equivalent mutations", "Mutants", mutant]) mutations)
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
new file mode 100644
index 0000000..15d8186
--- /dev/null
+++ b/Results/False Positives/true_returnValue != null_returnValueVar == returnValue_False_False_1
@@ -0,0 +1,11 @@
+False positives test
+postCondVoid: true
+postCondRefType: returnValue != null
+postCondPrimType: returnValueVar == returnValue
+ignoreLibMethods: False
+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
diff --git a/Results/False Positives/true_true_true_False_False_1 b/Results/False Positives/true_true_true_False_False_1
new file mode 100644
index 0000000..5304262
--- /dev/null
+++ b/Results/False Positives/true_true_true_False_False_1
@@ -0,0 +1,9 @@
+False positives test
+postCondVoid: true
+postCondRefType: true
+postCondPrimType: true
+ignoreLibMethods: False
+ignoreMainMethod: False
+nrOfUnroll: 1
+False positives found in:
+Total number of false positives: 0
\ No newline at end of file
diff --git a/Settings.hs b/Settings.hs
index d246977..2264333 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -3,7 +3,7 @@ module Settings where
import System.FilePath(joinPath)
testFile, postCondVoid, postCondRefType, postCondPrimType :: String
-testFile = test3
+testFile = "Vector"
-- The post condition may depend on the type of the method we are looking at
postCondVoid = "true"
@@ -13,7 +13,7 @@ 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
ignoreLibMethods, ignoreMainMethod :: Bool
-ignoreLibMethods = False
+ignoreLibMethods = False -- No longer supported
ignoreMainMethod = False
diff --git a/Tests/OpenIntToDoubleHashMap.java b/Tests/OpenIntToDoubleHashMap.java
deleted file mode 100644
index 03fa648..0000000
--- a/Tests/OpenIntToDoubleHashMap.java
+++ /dev/null
@@ -1,608 +0,0 @@
-/*
- * Licensed to the Apache Software Foundation (ASF) under one or more
- * contributor license agreements. See the NOTICE file distributed with
- * this work for additional information regarding copyright ownership.
- * The ASF licenses this file to You under the Apache License, Version 2.0
- * (the "License"); you may not use this file except in compliance with
- * the License. You may obtain a copy of the License at
- *
- * http://www.apache.org/licenses/LICENSE-2.0
- *
- * Unless required by applicable law or agreed to in writing, software
- * distributed under the License is distributed on an "AS IS" BASIS,
- * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
- * See the License for the specific language governing permissions and
- * limitations under the License.
- */
-
-package org.apache.commons.math3.util;
-
-import java.io.IOException;
-import java.io.ObjectInputStream;
-import java.io.Serializable;
-import java.util.ConcurrentModificationException;
-import java.util.NoSuchElementException;
-
-/**
- * Open addressed map from int to double.
- * <p>This class provides a dedicated map from integers to doubles with a
- * much smaller memory overhead than standard <code>java.util.Map</code>.</p>
- * <p>This class is not synchronized. The specialized iterators returned by
- * {@link #iterator()} are fail-fast: they throw a
- * <code>ConcurrentModificationException</code> when they detect the map has been
- * modified during iteration.</p>
- * @since 2.0
- */
-public class OpenIntToDoubleHashMap implements Serializable {
-
- /** Status indicator for free table entries. */
- protected static final byte FREE = 0;
-
- /** Status indicator for full table entries. */
- protected static final byte FULL = 1;
-
- /** Status indicator for removed table entries. */
- protected static final byte REMOVED = 2;
-
- /** Serializable version identifier */
- private static final long serialVersionUID = -3646337053166149105L;
-
- /** Load factor for the map. */
- private static final float LOAD_FACTOR = 0.5f;
-
- /** Default starting size.
- * <p>This must be a power of two for bit mask to work properly. </p>
- */
- private static final int DEFAULT_EXPECTED_SIZE = 16;
-
- /** Multiplier for size growth when map fills up.
- * <p>This must be a power of two for bit mask to work properly. </p>
- */
- private static final int RESIZE_MULTIPLIER = 2;
-
- /** Number of bits to perturb the index when probing for collision resolution. */
- private static final int PERTURB_SHIFT = 5;
-
- /** Keys table. */
- private int[] keys;
-
- /** Values table. */
- private double[] values;
-
- /** States table. */
- private byte[] states;
-
- /** Return value for missing entries. */
- private final double missingEntries;
-
- /** Current size of the map. */
- private int size;
-
- /** Bit mask for hash this.values. */
- private int mask;
-
- /** Modifications count. */
- private transient int count;
-
- /**
- * Build an empty map with default this.size and using NaN for missing entries.
- */
- public OpenIntToDoubleHashMap() {
- this(this.DEFAULT_EXPECTED_SIZE, Double.NaN);
- }
-
- /**
- * Build an empty map with default this.size
- * @param this.missingEntries value to return when a missing entry is fetched
- */
- public OpenIntToDoubleHashMap(final double missingEntries1) {
- this(this.DEFAULT_EXPECTED_SIZE, missingEntries1);
- }
-
- /**
- * Build an empty map with specified this.size and using NaN for missing entries.
- * @param expectedSize expected number of elements in the map
- */
- public OpenIntToDoubleHashMap(final int expectedSize) {
- this(expectedSize, Double.NaN);
- }
-
- /**
- * Build an empty map with specified this.size.
- * @param expectedSize expected number of elements in the map
- * @param this.missingEntries value to return when a missing entry is fetched
- */
- public OpenIntToDoubleHashMap(final int expectedSize1,
- final double missingEntries2) {
- final int capacity = computeCapacity(expectedSize1);
- this.keys = new int[capacity];
- this.values = new double[capacity];
- this.states = new byte[capacity];
- this.missingEntries = missingEntries2;
- this.mask = capacity - 1;
- }
-
- /**
- * Copy constructor.
- * @param source map to copy
- */
- public OpenIntToDoubleHashMap(final OpenIntToDoubleHashMap source) {
- final int length = source.keys.length;
- this.keys = new int[length];
- System.arraycopy(source.keys, 0, this.keys, 0, length);
- this.values = new double[length];
- System.arraycopy(source.values, 0, this.values, 0, length);
- this.states = new byte[length];
- System.arraycopy(source.states, 0, this.states, 0, length);
- this.missingEntries = source.missingEntries;
- this.size = source.size;
- this.mask = source.mask;
- this.count = source.count;
- }
-
- /**
- * Compute the capacity needed for a given this.size.
- * @param expectedSize expected this.size of the map
- * @return capacity to use for the specified this.size
- */
- private static int computeCapacity(final int expectedSize2) {
- if (expectedSize2 == 0) {
- return 1;
- }
- final int capacity1 = (int) FastMath.ceil(expectedSize2 / this.LOAD_FACTOR);
- final int powerOfTwo = Integer.highestOneBit(capacity1);
- if (powerOfTwo == capacity1) {
- return capacity1;
- }
- return nextPowerOfTwo(capacity1);
- }
-
- /**
- * Find the smallest power of two greater than the input value
- * @param i input value
- * @return smallest power of two greater than the input value
- */
- private static int nextPowerOfTwo(final int i) {
- return Integer.highestOneBit(i) << 1;
- }
-
- /**
- * Get the stored value associated with the given key
- * @param key key associated with the data
- * @return data associated with the key
- */
- /*
- public double get(final int key) {
-
- final int hash = hashOf(key);
- int index = hash & this.mask;
- if (this.containsKey1(key, index)) {
- return this.values[index];
- }
-
- if (this.states[index] == this.FREE) {
- return this.missingEntries;
- }
-
- int j = index;
- for (int perturb = perturb(hash); this.states[index] != this.FREE; perturb >>= this.PERTURB_SHIFT) {
- j = this.probe(perturb, j);
- index = j & this.mask;
- if (this.containsKey1(key, index)) {
- return this.values[index];
- }
- }
-
- return this.missingEntries;
-
- }
- */
-
- /**
- * Check if a value is associated with a key.
- * @param key key to check
- * @return true if a value is associated with key
- */
- /*
- public boolean containsKey(final int key1) {
-
- final int hash1 = hashOf(key1);
- int index1 = hash1 & this.mask;
- if (this.containsKey1(key1, index1)) {
- return true;
- }
-
- if (this.states[index1] == this.FREE) {
- return false;
- }
-
- int j = index1;
- for (int perturb1 = perturb1(hash1); this.states[index1] != this.FREE; perturb1 >>= this.PERTURB_SHIFT) {
- j = probe(perturb1, j);
- index1 = j & this.mask;
- if (this.containsKey1(key1, index1)) {
- return true;
- }
- }
-
- return false;
-
- }
- */
-
- /**
- * Get an iterator over map elements.
- * <p>The specialized iterators returned are fail-fast: they throw a
- * <code>ConcurrentModificationException</code> when they detect the map
- * has been modified during iteration.</p>
- * @return iterator over the map elements
- */
- public Iterator iterator() {
- return new Iterator();
- }
-
- /**
- * Perturb the hash for starting probing.
- * @param hash initial hash
- * @return perturbed hash
- */
- private static int perturb(final int hash2) {
- return hash2 & 0x7fffffff;
- }
-
- /**
- * Find the index at which a key should be inserted
- * @param key key to lookup
- * @return index at which key should be inserted
- */
- private int findInsertionIndex(final int key2) {
- return this.findInsertionIndex1(this.keys, this.states, key2, this.mask);
- }
-
- /**
- * Find the index at which a key should be inserted
- * @param this.keys this.keys table
- * @param this.states this.states table
- * @param key key to lookup
- * @param this.mask bit this.mask for hash this.values
- * @return index at which key should be inserted
- */
- /*
- private static int findInsertionIndex1(final int[] keys3, final byte[] states3,
- final int key3, final int mask3) {
- final int hash3 = hashOf(key3);
- int index3 = hash3 & mask3;
- if (states3[index3] == this.FREE) {
- return index3;
- } else if ((states3[index3] == this.FULL) && (keys3[index3] == key3)) {
- return this.changeIndexSign(index3);
- }
-
- int perturb2 = perturb(hash3);
- int j3 = index3;
- if (states3[index3] == this.FULL) {
- while (true) {
- j3 = probe(perturb2, j3);
- index3 = j3 & mask3;
- perturb2 >>= this.PERTURB_SHIFT;
-
- if ((states3[index3] != this.FULL) || (keys3[index3] == key3)) {
- break;
- }
- }
- }
-
- if (states3[index3] == this.FREE) {
- return index3;
- } else if (states3[index3] == this.FULL) {
- // due to the loop exit condition,
- // if (this.states[index] == this.FULL) then this.keys[index] == key
- return this.changeIndexSign(index3);
- }
-
- final int firstRemoved = index3;
- while (true) {
- j3 = probe(perturb2, j3);
- index3 = j3 & mask3;
-
- if (states3[index3] == this.FREE) {
- return firstRemoved;
- } else if ((states3[index3] == this.FULL) && (keys3[index3] == key3)) {
- return this.changeIndexSign(index3);
- }
-
- perturb2 >>= this.PERTURB_SHIFT;
-
- }
-
- }
- */
-
- /**
- * Compute next probe for collision resolution
- * @param perturb perturbed hash
- * @param j previous probe
- * @return next probe
- */
- private static int probe(final int perturb4, final int j4) {
- return (j4 << 2) + j4 + perturb4 + 1;
- }
-
- /**
- * Change the index sign
- * @param index initial index
- * @return changed index
- */
- private static int changeIndexSign(final int index5) {
- return -index5 - 1;
- }
-
- /**
- * Get the number of elements stored in the map.
- * @return number of elements stored in the map
- */
- public int size() {
- return this.size;
- }
-
-
- /**
- * Remove the value associated with a key.
- * @param key key to which the value is associated
- * @return removed value
- */
- /*
- public double remove(final int key6) {
-
- final int hash6 = hashOf(key6);
- int index6 = hash6 & this.mask;
- if (this.containsKey1(key6, index6)) {
- return this.doRemove(index6);
- }
-
- if (this.states[index6] == this.FREE) {
- return this.missingEntries;
- }
-
- int j6 = index6;
- for (int perturb6 = perturb6(hash6); this.states[index6] != this.FREE; perturb6 >>= this.PERTURB_SHIFT) {
- j6 = this.probe(perturb6, j6);
- index = j6 & this.mask;
- if (this.containsKey1(key6, index6)) {
- return this.doRemove(index6);
- }
- }
-
- return this.missingEntries;
-
- }
- */
-
- /**
- * Check if the tables contain an element associated with specified key
- * at specified index.
- * @param key key to check
- * @param index index to check
- * @return true if an element is associated with key at index
- */
- private boolean containsKey1(final int key7, final int index7) {
- return ((key7 != 0) || (this.states[index7] == this.FULL)) && (this.keys[index7] == key7);
- }
-
- /**
- * Remove an element at specified index.
- * @param index index of the element to remove
- * @return removed value
- */
- private double doRemove(int index8) {
- this.keys[index8] = 0;
- this.states[index8] = this.REMOVED;
- final double previous = this.values[index8];
- this.values[index8] = this.missingEntries;
- --this.size;
- ++this.count;
- return previous;
- }
-
- /**
- * Put a value associated with a key in the map.
- * @param key key to which value is associated
- * @param value value to put in the map
- * @return previous value associated with the key
- */
- /*
- public double put(final int key9, final double value9) {
- int index9 = this.findInsertionIndex(key9);
- double previous9 = this.missingEntries;
- boolean newMapping = true;
- if (index9 < 0) {
- index9 = this.changeIndexSign(index9);
- previous9 = this.values[index9];
- newMapping = false;
- }
- this.keys[index9] = key9;
- this.states[index9] = this.FULL;
- this.values[index9] = value9;
- if (newMapping) {
- ++this.size;
- if (this.shouldGrowTable()) {
- this.growTable();
- }
- ++this.count;
- }
- return previous9;
-
- }
- */
-
- /**
- * Grow the tables.
- */
- private void growTable() {
-
- final int oldLength = this.states.length;
- final int[] oldKeys = this.keys;
- final double[] oldValues = this.values;
- final byte[] oldStates = this.states;
-
- final int newLength = this.RESIZE_MULTIPLIER * oldLength;
- final int[] newKeys = new int[newLength];
- final double[] newValues = new double[newLength];
- final byte[] newStates = new byte[newLength];
- final int newMask = newLength - 1;
- for (int i11 = 0; i11 < oldLength; ++i11) {
- if (oldStates[i11] == this.FULL) {
- final int key11 = oldKeys[i11];
- final int index11 = this.findInsertionIndex1(newKeys, newStates, key11, newMask);
- newKeys[index11] = key11;
- newValues[index11] = oldValues[i11];
- newStates[index11] = this.FULL;
- }
- }
-
- this.mask = newMask;
- this.keys = newKeys;
- this.values = newValues;
- this.states = newStates;
-
- }
-
- /**
- * Check if tables should grow due to increased this.size.
- * @return true if tables should grow
- */
- private boolean shouldGrowTable() {
- return this.size > ((this.mask + 1) * this.LOAD_FACTOR);
- }
-
- /**
- * Compute the hash value of a key
- * @param key key to hash
- * @return hash value of the key
- */
- /*
- private static int hashOf(final int key12) {
- final int h12 = key12 ^ ((key12 >>> 20) ^ (key12 >>> 12));
- return h12 ^ (h12 >>> 7) ^ (h12 >>> 4);
- }
- */
-
-
- /** Iterator class for the map. */
- public class Iterator {
-
- /** Reference modification this.count. */
- private final int referenceCount;
-
- /** Index of current element. */
- private int current;
-
- /** Index of next element. */
- private int next;
-
- /**
- * Simple constructor.
- */
- private Iterator() {
-
- // preserve the modification this.count of the map to detect concurrent modifications later
- this.referenceCount = this.count;
-
- // initialize this.current index
- this.next = -1;
- try {
- this.advance();
- } catch (NoSuchElementException nsee) { // NOPMD
- // ignored
- }
-
- }
-
- /**
- * Check if there is a this.next element in the map.
- * @return true if there is a this.next element
- */
- public boolean hasNext() {
- return this.next >= 0;
- }
-
- /**
- * Get the key of this.current entry.
- * @return key of this.current entry
- * @exception ConcurrentModificationException if the map is modified during iteration
- * @exception NoSuchElementException if there is no element left in the map
- */
- public int key()
- throws ConcurrentModificationException, NoSuchElementException {
- if (this.referenceCount != this.count) {
- throw new ConcurrentModificationException();
- }
- if (this.current < 0) {
- throw new NoSuchElementException();
- }
- return this.keys[this.current];
- }
-
- /**
- * Get the value of this.current entry.
- * @return value of this.current entry
- * @exception ConcurrentModificationException if the map is modified during iteration
- * @exception NoSuchElementException if there is no element left in the map
- */
- public double value()
- throws ConcurrentModificationException, NoSuchElementException {
- if (this.referenceCount != this.count) {
- throw new ConcurrentModificationException();
- }
- if (this.current < 0) {
- throw new NoSuchElementException();
- }
- return this.values[this.current];
- }
-
- /**
- * Advance iterator one step further.
- * @exception ConcurrentModificationException if the map is modified during iteration
- * @exception NoSuchElementException if there is no element left in the map
- */
- public void advance()
- throws ConcurrentModificationException, NoSuchElementException {
-
- if (this.referenceCount != this.count) {
- throw new ConcurrentModificationException();
- }
-
- // advance on step
- this.current = this.next;
-
- // prepare this.next step
- try {
- while (this.states[++this.next] != this.FULL) { // NOPMD
- // nothing to do
- }
- } catch (ArrayIndexOutOfBoundsException e) {
- this.next = -2;
- if (this.current < 0) {
- throw new NoSuchElementException();
- }
- }
-
- }
-
- }
-
- /**
- * Read a serialized object.
- * @param stream input stream
- * @throws IOException if object cannot be read
- * @throws ClassNotFoundException if the class corresponding
- * to the serialized object cannot be found
- */
- private void readObject(final ObjectInputStream stream)
- throws IOException, ClassNotFoundException {
- stream.defaultReadObject();
- this.count = 0;
- }
-
-
-}
diff --git a/Tests/arrays1.class b/Tests/simple tests/arrays1.class
similarity index 100%
rename from Tests/arrays1.class
rename to Tests/simple tests/arrays1.class
diff --git a/Tests/arrays1.java b/Tests/simple tests/arrays1.java
similarity index 100%
rename from Tests/arrays1.java
rename to Tests/simple tests/arrays1.java
diff --git a/Verifier.hs b/Verifier.hs
index 629dcae..1a17ad2 100644
--- a/Verifier.hs
+++ b/Verifier.hs
@@ -42,6 +42,13 @@ stringToBv (c:cs) = do
cs' <- stringToBv cs
mkConcat c' cs'
+-- Creates a string to represent a name as a z3 variable
+getVarName :: Name -> String
+getVarName name = case prettyPrint name of
+ -- The wlp may contain variables introduced by method call (since methods may loop indefinitely we can't always get the return value)
+ -- We must ignore the exact number of the call, as it would introduce false positives
+ '$':s -> '$' : takeWhile (/= '$') s
+ s -> s
-- | Defines the convertion from an expression to AST so that Z3 can assert satisfiability
-- This is used to fold expressions generated by the WLP transformer, so not all valid Java expressions need to be handled
@@ -76,7 +83,7 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
ArrayCreate t exps dim -> foldExp expAssertAlgebra (if fromEnum n < length exps then (exps !! fromEnum n) else Lit (Int 0)) env decls
ArrayCreateInit t dim arrayInit -> mkInteger 0
ExpName name -> do
- symbol <- mkStringSymbol ("*length(" ++ prettyPrint name ++ ", " ++ show n ++ ")")
+ symbol <- mkStringSymbol ("*length(" ++ getVarName name ++ ", " ++ show n ++ ")")
mkIntVar symbol
Cond g a1 a2 -> foldExp expAssertAlgebra (Cond g (MethodInv (MethodCall (Name [Ident "*length"]) [a1, (Lit (Int n))])) (MethodInv (MethodCall (Name [Ident "*length"]) [a2, (Lit (Int n))]))) env decls
Lit Null -> mkInteger (-1)
@@ -86,7 +93,7 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
ArrayIndex (ArrayCreate t _ _) _ -> foldExp expAssertAlgebra (getInitValue t) env decls
ArrayIndex (ArrayCreateInit t _ _) _ -> foldExp expAssertAlgebra (getInitValue t) env decls
ArrayIndex (ExpName name) i -> do
- symbol <- mkStringSymbol (prettyPrint name ++ "[" ++ show i ++ "]")
+ symbol <- mkStringSymbol (getVarName name ++ "[" ++ show i ++ "]")
case arrayContentType (lookupType decls env name) of
PrimType BooleanT -> mkBoolVar symbol
PrimType FloatT -> mkRealVar symbol
@@ -95,19 +102,17 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
ArrayIndex (Cond g a1 a2) i -> foldExp expAssertAlgebra (Cond g (ArrayAccess (ArrayIndex a1 i)) (ArrayAccess (ArrayIndex a2 i))) env decls
ArrayIndex e _ -> foldExp expAssertAlgebra e env decls
fExpName name env decls = do
- symbol <- mkStringSymbol (prettyPrint name)
- case prettyPrint name of
- -- For now, we assume library methods return ints. Fixing this would require type information of library methods.
- '$':_ -> if ignoreLibMethods then mkStringSymbol "libMethodCall" >>= mkIntVar else error "introduced variable in WLP expression"
- -- If we're not dealing with library methods, we should be able to get the type from the type environment
- _ -> case lookupType decls env name of
- PrimType BooleanT -> mkBoolVar symbol
- PrimType FloatT -> mkRealVar symbol
- PrimType DoubleT -> mkRealVar symbol
- PrimType IntT -> mkIntVar symbol
- PrimType ByteT -> mkIntVar symbol
- RefType _ -> mkIntVar symbol
- t -> error ("Verifier: Type of " ++ prettyPrint name ++ " unknown or not implemented: " ++ show t)
+ symbol <- mkStringSymbol (getVarName name)
+
+ -- If we're not dealing with library methods, we should be able to get the type from the type environment
+ case lookupType decls env name of
+ PrimType BooleanT -> mkBoolVar symbol
+ PrimType FloatT -> mkRealVar symbol
+ PrimType DoubleT -> mkRealVar symbol
+ PrimType IntT -> mkIntVar symbol
+ PrimType ByteT -> mkIntVar symbol
+ RefType _ -> mkIntVar symbol
+ t -> error ("Verifier: Type of " ++ prettyPrint name ++ " unknown or not implemented: " ++ show t)
fPostIncrement = undefined
fPostDecrement = undefined
fPreIncrement = undefined
--
GitLab