Mjr/dev init igen

.classpath

@@ -36,5 +36,7 @@
 	<classpathentry kind="lib" path="lib/yicesapijava.jar"/>
 	<classpathentry kind="con" path="org.eclipse.jdt.junit.JUNIT_CONTAINER/4"/>
 	<classpathentry kind="lib" path="lib/proteus.jar"/>
+	<classpathentry kind="lib" path="lib/inv-solver.jar"/>
+	<classpathentry kind="lib" path="lib/parser.jar"/>
 	<classpathentry kind="output" path="build"/>
 </classpath>

build/annotations/.gitignore

@@ -0,0 +1 @@
+/gov/

build/classes/.gitignore

@@ -0,0 +1,3 @@
+/gov/
+/java/
+/org/

build/examples/.gitignore

@@ -0,0 +1,76 @@
+/ArrayTest.class
+/Assume.class
+/ByteTest.class
+/CollectConstraints.class
+/ExampleAbort$Failure.class
+/ExampleAbort.class
+/ExampleDReal.class
+/FlapController$EmergencySensor.class
+/FlapController$FlapMovement.class
+/FlapController.class
+/ImageReading.class
+/ImplicitFlow.class
+/MyClass1.class
+/MyClass2.class
+/MyClassFP.class
+/MyClassWithFields.class
+/MyDriver1.class
+/MyDriverForFields.class
+/NumberExample.class
+/ProbExample1.class
+/SimpleStringTest.class
+/StringTest.class
+/StringTest2.class
+/SubStringTest.class
+/Test.class
+/TestArray.class
+/TestInc.class
+/TestPaths.class
+/TestZ3.class
+/TreeMapSimple$Entry.class
+/TreeMapSimple.class
+/WBS.class
+/abstractClasses/
+/arrays/
+/compositional/
+/concolic/
+/corpus/
+/coverage/
+/demo/
+/doublyNested/
+/fuzz/
+/lazyinit/
+/modpow/
+/nested/
+/perthread/
+/rbt/
+/rjc/
+/sequences/
+/simple/
+/strings/
+/summerschool/
+/symbolicheap/
+/tsafe/
+/uberlazy/
+/ArrayTest.jpf
+/Assume.jpf
+/ByteTest.jpf
+/CollectConstraints.jpf
+/E5.class
+/E5.jpf
+/ExampleDReal.jpf
+/FlapController.jpf
+/ImageReading.jpf
+/ImplicitFlow.jpf
+/NumberExample.jpf
+/PronSysmExe.jpf
+/SimpleStringTest.jpf
+/SubStringTest.jpf
+/Test.jpf
+/TestArray.jpf
+/TestInc.jpf
+/TestPaths.jpf
+/TestZ3.jpf
+/TreeMapSimple.jpf
+/WBS.jpf
+/icse13MT.jpf

build/examples/Test.up

@@ -0,0 +1,6 @@
+domain{
+ x_1_SYMINT:0,10;
+ };
+ usageProfile{
+  x_1_SYMINT>=0:100/100;
+ };

build/main/.gitignore

@@ -0,0 +1,3 @@
+/edu/
+/gov/
+/vlab/

build/peers/.gitignore

@@ -0,0 +1 @@
+/gov/

build/tests/.gitignore

@@ -0,0 +1 @@
+/gov/

eclipse/run-JPF-symbc.launch

@@ -24,5 +24,5 @@
 <stringAttribute key="org.eclipse.jdt.launching.MAIN_TYPE" value="gov.nasa.jpf.tool.RunJPF"/>
 <stringAttribute key="org.eclipse.jdt.launching.PROGRAM_ARGUMENTS" value="&quot;${resource_loc}&quot;"/>
 <stringAttribute key="org.eclipse.jdt.launching.PROJECT_ATTR" value="jpf-symbc"/>
-<stringAttribute key="org.eclipse.jdt.launching.VM_ARGUMENTS" value="-Xmx1024m -ea"/>
+<stringAttribute key="org.eclipse.jdt.launching.VM_ARGUMENTS" value="-Xmx2048m -ea -Djava.library.path=&quot;/usr/local/lib&quot;"/>
 </launchConfiguration>

jpf.load

@@ -1,3 +1,3 @@
-export JPF=/home/miroslav/Research/jpf/jpf-core/
+export JPF=/home/marlinroberts/lnx.repos/gsoc/jpf-core
 export PATH=${JPF}/bin:$PATH
 

src/examples/ByteTest.jpf

@@ -6,6 +6,6 @@ symbolic.min_int=-100
 symbolic.max_int=100
 symbolic.dp=z3
 #vm.storage.class=nil
-#listener = .symbc.SymbolicListener
+listener = .symbc.SymbolicListener
 #listener = .listener.ChoiceTracker
 #listener = gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener

src/examples/E5.java

@@ -0,0 +1,112 @@
+
+public class E5 {
+
+	public static void main(String[] args) {
+		String r1 = "A";
+		String r2 = "BA";
+		String r5 = "aa";
+		strEx(r1,r2);
+		strEx1(r1,r2);
+		strEx2(r5);
+		strEx3(r5);
+		strEx4(r5);
+		strEx6(r5);
+		strEx7(r5);
+		strEx8(r5);
+	}
+
+	public static void strEx (String r1, String r2) {
+		String r3 = r2.concat(r1);
+		//if (r2.concat(r1).contains("BAA")) {
+
+		if (r3.contains("BAA")) {	
+			// true branch 
+			System.out.println("r3 contains BAA");
+		} else {
+			// false branch
+			System.out.println("r3 does not contain BAA");
+		}
+	}
+
+
+	public static void strEx1 (String r1, String r2) {
+		String r3 = r2.concat(r1);
+		//if (r2.concat(r1).contains("BAA")) {
+
+		if (r3.contains("BAA")) {	
+			// true branch 
+			System.out.println("r3 contains BAA");
+			if (r3.equals("BAA")) {
+				System.out.println("r3 equals BAA");
+			} else {
+				System.out.println("r3 contains but does not equal BAA");
+			}
+		} else {
+			// false branch
+			System.out.println("r3 does not contain BAA");
+		}
+	}
+
+
+
+
+
+
+
+	public static void strEx2 (String r5) {
+		if (r5.toUpperCase().concat(r5).contains("AAaa")) {
+			// true branch 
+		} else {
+			// false branch
+		}
+	}
+
+	public static void strEx3 (String r5) {
+		if (r5.trim().concat(r5).contains("AAaa")) {
+			// true branch 
+		} else {
+			// false branch
+		}
+	}
+
+	public static void strEx4 (String r5) {
+		r5 = r5.concat(r5);
+		if (r5.contains("AAaa")) {
+			// true branch 
+		} else {
+			// false branch
+		}
+	}
+
+	public static void strEx6 (String r5) {
+		if (r5.contains("aa")) {
+			if (r5.toUpperCase().concat(r5).contains("AAaa")) {
+			// true branch 
+		} else {
+			// false branch
+		}
+		}
+
+	}
+
+	public static void strEx7 (String r5) {
+		if (r5.contains("aa")) {
+			if (r5.concat(r5).toUpperCase().contains("AAAA")) {
+			// true branch 
+		} else {
+			// false branch
+		}
+		}
+
+	}
+
+	public static void strEx8 (String r5) {
+		if (r5.trim().concat(r5).toUpperCase().contains("AA")) {
+			// true branch 
+		} else {
+			// false branch
+		}
+	}
+
+
+}

src/examples/E5.jpf

@@ -0,0 +1,51 @@
+target=E5
+classpath=${jpf-symbc}/build/examples
+sourcepath=${jpf-symbc}/src/examples
+
+symbolic.method = E5.strEx(sym#sym)
+#symbolic.method = E5.strEx1(sym#sym)
+#symbolic.method = E5.strEx2(sym)
+#symbolic.method = E5.strEx3(sym)
+#symbolic.method = E5.strEx4(sym)
+#symbolic.method = E5.strEx6(sym)
+#symbolic.method = E5.strEx7(sym)
+#symbolic.method = E5.strEx8(sym)
+
+symbolic.min_int=-100
+symbolic.max_int=100
+
+
+#symbolic.dp=z3
+symbolic.dp=choco
+
+symbolic.strings=true
+
+#symbolic.string_dp=z3str2
+#symbolic.string_dp=cvc
+
+symbolic.string_dp=igen
+symbolic.string_dp_upper=2
+symbolic.string_dp_lower=1
+symbolic.string_dp_alphaSize=6
+symbolic.string_dp_alpha=A,B,C,a,b,c
+
+symbolic.string_dp_timeout_ms=3000
+symbolic.debug=false
+
+
+#vm.storage.class=nil
+
+#listener = .symbc.SymbolicListener
+
+#listener = .listener.ChoiceTracker
+#choice.trace=test.trc
+#choice.class=E5
+
+#listener = gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener
+
+#listener=gov.nasa.jpf.listener.CoverageAnalyzer
+
+listener = gov.nasa.jpf.symbc.HeuristicListener
+# these two are exclusive of one another.
+#symbolic.heuristicRandom=true
+#symbolic.heuristicPartition=true

src/examples/SubStringTest.jpf

@@ -4,7 +4,7 @@ sourcepath=${jpf-symbc}/src/examples
 symbolic.method = SubStringTest.substr(sym#sym#sym)
 symbolic.min_int=-100
 symbolic.max_int=100
-#symbolic.dp=z3
+symbolic.dp=z3
 #vm.storage.class=nil
 #listener = .symbc.SymbolicListener
 #listener = .listener.ChoiceTracker

src/examples/strings/ChallengeTest.jpf

@@ -3,9 +3,11 @@ classpath=${jpf-symbc}/build/examples
 sourcepath=${jpf-symbc}/src/examples
 
 symbolic.strings = true
-#symbolic.dp=choco
+symbolic.dp=choco
+#symbolic.string_dp=z3str2
+symbolic.string_dp=z3str3
 #symbolic.string_dp=ABC
-symbolic.string_dp=no_solver
+#symbolic.string_dp=no_solver
 symbolic.string_dp_timeout_ms=3000
 symbolic.debug=true
 

src/examples/strings/DelimSearchz.jpf

@@ -4,14 +4,14 @@ sourcepath=${jpf-symbc}/src/examples
 
 symbolic.strings = true
 symbolic.dp=choco
-#symbolic.string_dp=z3str2
-symbolic.string_dp=ABC
+symbolic.string_dp=z3str2
+#symbolic.string_dp=ABC
 symbolic.string_dp_timeout_ms=3000
 symbolic.debug=true
 
 symbolic.method= strings.DelimSearch.search(sym, con) 
 search.depth_limit = 20
 search.multiple_errors=true
 #listener = gov.nasa.jpf.symbc.sequences.TimingChannelListener
-listener = sidechannel.TimingChannelListener
+#listener = sidechannel.TimingChannelListener
 vm.storage.class=nil

src/examples/strings/GoodbyeWorld.jpf

@@ -4,9 +4,22 @@ sourcepath=${jpf-symbc}/src/examples
 
 #symbolic.dp=choco
 symbolic.strings=true
-symbolic.string_dp=z3str2
+#symbolic.string_dp=z3str2
+symbolic.string_dp=z3str3
+#symbolic.string_dp=ABC
 symbolic.string_dp_timeout_ms=3000
-symbolic.debug=true
+#symbolic.debug=true
+
+#z3str3 parameters with defaults
+symbolic.z3str3_aggressive_length_testing=false
+symbolic.z3str3_aggressive_unroll_testing=true
+symbolic.z3str3_aggressive_value_testing=false
+symbolic.z3str3_fast_length_tester_cache=true
+symbolic.z3str3_fast_value_tester_cache=true
+symbolic.z3str3_fixed_length_naive_cex=true
+symbolic.z3str3_fixed_length_refinement=false
+symbolic.z3str3_string_constant_cache=true
+symbolic.z3str3_strong_arrangements=true
 
 symbolic.method= strings.GoodbyeWorld.hello(sym)
 search.depth_limit = 10

src/examples/strings/HelloWorld.jpf

@@ -1,12 +1,15 @@
 target=strings.HelloWorld
-#classpath=${jpf-symbc}/build/examples
-#sourcepath=${jpf-symbc}/src/examples
-classpath=/home/miroslav/Research/jpf/jpf-symbc/build/examples
-sourcepath=/home/miroslav/Research/jpf/jpf-symbc/src/examples
+classpath=${jpf-symbc}/build/examples
+sourcepath=${jpf-symbc}/src/examples
+#classpath=/home/miroslav/Research/jpf/jpf-symbc/build/examples
+#sourcepath=/home/miroslav/Research/jpf/jpf-symbc/src/examples
 symbolic.strings = true
 
-#symbolic.dp=choco
-symbolic.string_dp=ABC
+symbolic.dp=choco
+#symbolic.dp=z3
+symbolic.string_dp=z3str3
+#symbolic.string_dp=igen
+#symbolic.string_dp=ABC
 symbolic.string_dp_timeout_ms=3000
 symbolic.debug=true
 symbolic.method= strings.HelloWorld.hello(sym)

src/examples/strings/IndexOfTest.jpf

@@ -4,7 +4,9 @@ sourcepath=${jpf-symbc}/src/examples
 
 symbolic.strings = true
 #symbolic.dp=choco
-symbolic.string_dp=ABC
+#symbolic.string_dp=z3str2
+symbolic.string_dp=z3str3
+#symbolic.string_dp=ABC
 #symbolic.string_dp=no_solver
 symbolic.string_dp_timeout_ms=3000
 symbolic.debug=true