Update to new version

jpf-symbc/src/examples/TestZ3.java

@@ -1,3 +1,4 @@
+
 /*
  * Copyright (C) 2014, United States Government, as represented by the
  * Administrator of the National Aeronautics and Space Administration.
@@ -18,15 +19,202 @@
 
 import gov.nasa.jpf.symbc.Debug;
 
-
 public class TestZ3 {
-	public static void test(int x, int y) {
-		if(x-y<=y)
-			System.out.println("eq "+Debug.getSolvedPC());
+	public static void testSimple(int x, int y) {
+		if (x - y <= y)
+			printResult("x - y <= y: " + Debug.getSolvedPC());
 		else
-			System.out.println("neq "+Debug.getSolvedPC());
+			printResult("x - y  > y: " + Debug.getSolvedPC());
+	}
+
+	public static void testBitwiseOr(int x, int y) {
+		if ((x | y) == 37) {
+			printResult("x | y was 37");
+		} else {
+			printResult("x | y was 37");
+		}
+
+		if (37 == (x | y)) {
+			printResult("x | y was 37");
+		} else {
+			printResult("x | y was 37");
+		}
+
+		if ((x | 31) == 31) {
+			printResult("x | 31 was 31");
+		} else {
+			printResult("x | 31 was not 31");
+		}
+
+		if (31 == (x | 31)) {
+			printResult("x | 31 was 31");
+		} else {
+			printResult("x | 31 was not 31");
+		}
+	}
+
+	public static void testBitwiseAnd(int x, int y) {
+		if ((x & y) == 37) {
+			printResult("x & y was 37");
+		} else {
+			printResult("x & y was not 37");
+		}
+
+//		if (37 == (x & y)) {
+//			printResult("x & y was 37");
+//		} else {
+//			printResult("x & y was not 37");
+//		}
+//
+//		if ((x & 31) == 31) {
+//			printResult("x & 31 was 31");
+//		} else {
+//			printResult("x & 31 was not 31");
+//		}
+//
+//		if (31 == (x & 31)) {
+//			printResult("x & 31 was 31");
+//		} else {
+//			printResult("x & 31 was not 31");
+//		}		
+	}
+
+	public static void testShiftLeft(int x, int y) {
+		if (x << 2 == 4) {
+			printResult("x << 2 == 4");
+		} else {
+			printResult("x << 2 != 4");
+		}
+
+		if (2 << y == 4) {
+			printResult("2 << y == 4");
+		} else {
+			printResult("2 << y != 4");
+		}
+
+		if (x << y == 4) {
+			printResult("x << y == 4");
+		} else {
+			printResult("x << y != 4");
+		}
+	}
+
+	public static void testShiftRight(int x, int y) {
+		if (x >> 2 == 4) {
+			printResult("x >> 2 == 4");
+		} else {
+			printResult("x >> 2 != 4");
+		}
+
+		if (8 >> y == 4) {
+			printResult("8 >> y == 4");
+		} else {
+			printResult("8 >> y != 4");
+		}
+
+		if (x >> y == 4) {
+			printResult("x >> y == 4");
+		} else {
+			printResult("x >> y != 4");
+		}
 	}
+
+	public static void testLogicalShiftRight(int x, int y) {
+		if (x >>> 2 == 4) {
+			printResult("x >>> 2 == 4");
+		} else {
+			printResult("x >>> 2 != 4");
+		}
+
+		if (8 >>> y == 4) {
+			printResult("8 >>> y == 4");
+		} else {
+			printResult("8 >>> y != 4");
+		}
+
+		if (x >>> y == 4) {
+			printResult("x >>> y == 4");
+		} else {
+			printResult("x >>> y != 4");
+		}
+	}
+
+	public static void testCombination(int x, int y) {
+			if ((x >> y) == 1) {
+				printResult("x >> y was 1");
+
+				if (x + y == 4) {
+					printResult("x >> y == 1 and x + y == 4");
+				} else {
+					printResult("NOT x >> y == 1 and x + y == 4");
+				}
+			}
+	}
+
+	public static void testBitwiseXor(int x, int y) {
+		if ((x ^ y) == 37) {
+			printResult("x ^ y was 37");
+		} else {
+			printResult("x ^ y was not 37");
+		}
+
+		if (37 == (x ^ y)) {
+			printResult("x ^ y was 37");
+		} else {
+			printResult("x ^ y was not 37");
+		}
+
+		if ((x ^ 31) == 31) {
+			printResult("x ^ 31 was 31");
+		} else {
+			printResult("x ^ 31 was not 31");
+		}
+
+		if (31 == (x ^ 31)) {
+			printResult("x ^ 31 was 31");
+		} else {
+			printResult("x ^ 31 was not 31");		
+		}
+	}
+
+	public static void testBitwiseCombination(int x, int y) {
+		if ((x ^ y) == 3) {
+			printResult("x ^ y was 3");
+		} 
+
+		if ((x | y) == 15) {
+			printResult("x | y was 15");
+		}
+
+		if ((x + y) == 27) {
+			printResult("x | y was 15");
+		}
+	}
+
+	public static void testMod(int x, int y) {
+		if (x % y == 23) {
+			printResult("x % y was 23");
+		} else {
+			printResult("x % y was not 23");
+		}
+	}
+
+	public static void printResult(String str) {
+		System.out.println(str + (ISDEBUG ? ": " + Debug.getSolvedPC() : "."));
+	}
+
+	private static boolean ISDEBUG = true;
+
 	public static void main(String[] args) {
-		test(0,0);
+		testMod(0, 0);
+//		testSimple(0, 0);
+//		testBitwiseXor(0, 0);
+//		testBitwiseOr(0, 0);
+//		testBitwiseAnd(0, 0);
+//		testShiftLeft(0, 0);
+//		testShiftRight(0, 0);
+//		testLogicalShiftRight(0, 0);
+//		testCombination(0, 0);
+//		testBitwiseCombination(0, 0);
 	}
 }

jpf-symbc/src/examples/TestZ3.jpf

@@ -1,10 +1,11 @@
 target=TestZ3
 classpath=${jpf-symbc}/build/examples
 sourcepath=${jpf-symbc}/src/examples
-symbolic.method = TestZ3.test(sym#sym)
+symbolic.method = TestZ3.test(sym#sym),TestZ3.testSimple(sym#sym),TestZ3.testBitwiseXor(sym#sym),TestZ3.testBitwiseOr(sym#sym),TestZ3.testBitwiseAnd(sym#sym),TestZ3.testShiftLeft(sym#sym),TestZ3.testShiftRight(sym#sym),TestZ3.testLogicalShiftRight(sym#sym)#,TestZ3.testCombination(sym#sym),TestZ3.testBitwiseCombination(sym#sym),TestZ3.testMod(sym#sym)
 symbolic.min_int=-100
 symbolic.max_int=100
-symbolic.dp=z3
+#symbolic.dp=cvc3bitvec
+symbolic.dp=z3bitvector
 #vm.storage.class=nil
 #listener = .symbc.SymbolicListener
 #listener = .listener.ChoiceTracker

jpf-symbc/src/examples/arrays/ArrayLength.jpf

@@ -1,8 +1,8 @@
-target = Arrays
+target = arrays.Arrays
 
-symbolic.method=Arrays.check_length(sym#sym)
+symbolic.method=arrays.Arrays.check_length(sym#sym)
 symbolic.lazy=on
+symbolic.arrays=true
 classpath=${jpf-symbc}/build/examples
 search.multiple_errors=true
-listener = gov.nasa.jpf.symbc.SymbolicListener
 symbolic.dp = z3

jpf-symbc/src/examples/arrays/Arrays.java

@@ -1,28 +1,32 @@
+package arrays;
+
 public class Arrays {
     public static int counter(int i, int[] arr) {
         arr[1] = i;
         arr[2] = i;
         int a = arr[1];
-        int b = 1/a;
+        int b = 1/(1+a);
         return a;
     }
 
     public static int counter_bis(int i, int[] arr) {
         int a = arr[i];
-        int b = arr[i];
-        int c = 1/a;
-        return a;
+        return 1/(a+1);
     }
 
     public static int check_length(int i, int[] arr) {
         int j = arr.length;
         int a = arr[1];
-        int b = 10/(i-j);
+        int b = 10/j;
         return b;
     }
 
+    public static int[] create_array(int i) {
+        return new int[i];
+    }
+
     public static void obj_array(int i, ObjTest[] arr) {
-        int a = 1/(arr[i].y);
+        int a = 1/(arr[i].y + 1);
     }
 
     public static void check_obj_length(int i, ObjTest[] arr) {
@@ -36,14 +40,15 @@ public static void obj_store(ObjTest i, ObjTest[] arr) {
     }        
 
     public static void main(String[] args) {
-        int[] test = {1,2,3};
+        int[] test = new int[30];
         ObjTest[] objTest = {new ObjTest(1,2), new ObjTest(1,0)};
         obj_array(0, objTest);
         check_obj_length(0, objTest);
         obj_store(new ObjTest(1,2), objTest);
         int j = counter_bis(1, test);
         int k = counter(1, test);
         int b = check_length(2, test);
+        create_array(1);
     }
 
 

jpf-symbc/src/examples/arrays/Arrays.jpf

@@ -1,8 +1,9 @@
-target = Arrays
+target = arrays.Arrays
 
-symbolic.method=Arrays.counter(sym#sym)
+symbolic.method=arrays.Arrays.counter(sym#sym)
 symbolic.lazy=on
 classpath=${jpf-symbc}/build/examples
 search.multiple_errors=true
-listener = gov.nasa.jpf.symbc.SymbolicListener
-symbolic.dp=z3
+symbolic.dp=z3bitvector
+#listener=gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener
+symbolic.arrays=true

jpf-symbc/src/examples/arrays/Arraysbis.jpf

@@ -1,8 +1,11 @@
-target = Arrays
+target = arrays.Arrays
 
-symbolic.method=Arrays.counter_bis(sym#sym)
+symbolic.method=arrays.Arrays.counter_bis(sym#sym)
 symbolic.lazy=on
 classpath=${jpf-symbc}/build/examples
 search.multiple_errors=true
-listener = gov.nasa.jpf.symbc.SymbolicListener
 symbolic.dp = z3
+#symbolic.dp = z3inc
+symbolic.arrays=true
+#listener=gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener
+#listener=.symbc.numeric.solvers.IncrementalListener

jpf-symbc/src/examples/arrays/ObjArray.jpf

@@ -1,8 +1,8 @@
-target = Arrays
+target = arrays.Arrays
 
-symbolic.method=Arrays.obj_array(sym#sym)
+symbolic.method=arrays.Arrays.obj_array(sym#sym)
 symbolic.lazy=on
 classpath=${jpf-symbc}/build/examples
 search.multiple_errors=true
-listener = gov.nasa.jpf.symbc.SymbolicListener
 symbolic.dp=z3
+symbolic.arrays=true

jpf-symbc/src/examples/arrays/ObjLength.jpf

@@ -1,8 +1,9 @@
-target = Arrays
+target = arrays.Arrays
 
-symbolic.method=Arrays.check_obj_length(sym#sym)
+symbolic.method=arrays.Arrays.check_obj_length(sym#sym)
 symbolic.lazy=on
 classpath=${jpf-symbc}/build/examples
 search.multiple_errors=true
 listener = gov.nasa.jpf.symbc.SymbolicListener
 symbolic.dp=z3
+symbolic.arrays=true

jpf-symbc/src/examples/arrays/ObjStore.jpf

@@ -1,8 +1,9 @@
-target = Arrays
+target = arrays.Arrays
 
-symbolic.method=Arrays.obj_store(con#sym)
+symbolic.method=arrays.Arrays.obj_store(con#sym)
 symbolic.lazy=on
 classpath=${jpf-symbc}/build/examples
 search.multiple_errors=true
-listener = gov.nasa.jpf.symbc.SymbolicListener
+#listener = gov.nasa.jpf.symbc.SymbolicListener
 symbolic.dp=z3
+symbolic.arrays=true

jpf-symbc/src/examples/arrays/TestAALOAD.java

@@ -21,22 +21,14 @@
 
 public class TestAALOAD {
 
-	public void run(Node[] nlist) {
-        for (int i = 0; i< 2; i++) {
-            Node n = nlist[i];
-    		if(n != null) {
-                int curr = 100/n.elem;
-
-	    	} else {
-		    	System.out.println("n is null");
-	    	}
-        }
+	public void run(int i, Node[] nlist) {
+       Node n = nlist[i];
 	}
 
 
 	public static void main(String[] args) {
 		TestAALOAD taaload = new TestAALOAD();
 		Node[] n = {new Node()}; 
-		taaload.run(n);
+		taaload.run(0, n);
 	}
 }

jpf-symbc/src/examples/arrays/TestAALOAD.jpf

@@ -8,8 +8,8 @@ symbolic.lazy = true
 
 type_classpath = ${jpf-symbc}/build/examples/arrays
 
-symbolic.method = arrays.TestAALOAD.run(sym)
+symbolic.method = arrays.TestAALOAD.run(sym#sym)
 
 search.multiple_errors=true
-listener = gov.nasa.jpf.symbc.SymbolicListener
 symbolic.dp = z3
+symbolic.arrays=true