diff --git a/.classpath b/.classpath index 80c81000..c9a0eb2b 100644 --- a/.classpath +++ b/.classpath @@ -36,5 +36,7 @@ + + diff --git a/build/annotations/.gitignore b/build/annotations/.gitignore new file mode 100644 index 00000000..1f446ae4 --- /dev/null +++ b/build/annotations/.gitignore @@ -0,0 +1 @@ +/gov/ diff --git a/build/classes/.gitignore b/build/classes/.gitignore new file mode 100644 index 00000000..6b5e3d35 --- /dev/null +++ b/build/classes/.gitignore @@ -0,0 +1,3 @@ +/gov/ +/java/ +/org/ diff --git a/build/examples/.gitignore b/build/examples/.gitignore new file mode 100644 index 00000000..0bc00933 --- /dev/null +++ b/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 diff --git a/build/examples/Test.up b/build/examples/Test.up new file mode 100644 index 00000000..aa71e0de --- /dev/null +++ b/build/examples/Test.up @@ -0,0 +1,6 @@ +domain{ + x_1_SYMINT:0,10; + }; + usageProfile{ + x_1_SYMINT>=0:100/100; + }; \ No newline at end of file diff --git a/build/examples/fuzz.tar.gz b/build/examples/fuzz.tar.gz new file mode 100644 index 00000000..187f4a2a Binary files /dev/null and b/build/examples/fuzz.tar.gz differ diff --git a/build/jpf-symbc-annotations.jar b/build/jpf-symbc-annotations.jar new file mode 100644 index 00000000..c1d21278 Binary files /dev/null and b/build/jpf-symbc-annotations.jar differ diff --git a/build/jpf-symbc-classes.jar b/build/jpf-symbc-classes.jar new file mode 100644 index 00000000..a256d2b0 Binary files /dev/null and b/build/jpf-symbc-classes.jar differ diff --git a/build/jpf-symbc.jar b/build/jpf-symbc.jar new file mode 100644 index 00000000..0cd7a97d Binary files /dev/null and b/build/jpf-symbc.jar differ diff --git a/build/main/.gitignore b/build/main/.gitignore new file mode 100644 index 00000000..0ab1c462 --- /dev/null +++ b/build/main/.gitignore @@ -0,0 +1,3 @@ +/edu/ +/gov/ +/vlab/ diff --git a/build/peers/.gitignore b/build/peers/.gitignore new file mode 100644 index 00000000..1f446ae4 --- /dev/null +++ b/build/peers/.gitignore @@ -0,0 +1 @@ +/gov/ diff --git a/build/tests/.gitignore b/build/tests/.gitignore new file mode 100644 index 00000000..1f446ae4 --- /dev/null +++ b/build/tests/.gitignore @@ -0,0 +1 @@ +/gov/ diff --git a/eclipse/run-JPF-symbc.launch b/eclipse/run-JPF-symbc.launch index 7c4c8d4a..adf90380 100644 --- a/eclipse/run-JPF-symbc.launch +++ b/eclipse/run-JPF-symbc.launch @@ -24,5 +24,5 @@ - + diff --git a/jpf.load b/jpf.load index 319f90eb..389ac80e 100644 --- a/jpf.load +++ b/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 diff --git a/lib/com.microsoft.z3.jar b/lib/com.microsoft.z3.jar index ba34f2c6..e46805fd 100644 Binary files a/lib/com.microsoft.z3.jar and b/lib/com.microsoft.z3.jar differ diff --git a/lib/inv-solver.jar b/lib/inv-solver.jar new file mode 100755 index 00000000..6f0a6e61 Binary files /dev/null and b/lib/inv-solver.jar differ diff --git a/lib/libz3.so b/lib/libz3.so index 0ab8dbca..90e882d6 100755 Binary files a/lib/libz3.so and b/lib/libz3.so differ diff --git a/lib/libz3java.so b/lib/libz3java.so index 656a5b2e..17146796 100755 Binary files a/lib/libz3java.so and b/lib/libz3java.so differ diff --git a/lib/org.hamcrest.core_1.3.0.v20180420-1519.jar b/lib/org.hamcrest.core_1.3.0.v20180420-1519.jar new file mode 100644 index 00000000..659fc372 Binary files /dev/null and b/lib/org.hamcrest.core_1.3.0.v20180420-1519.jar differ diff --git a/lib/parser.jar b/lib/parser.jar new file mode 100644 index 00000000..8f78905e Binary files /dev/null and b/lib/parser.jar differ diff --git a/src/examples/ByteTest.jpf b/src/examples/ByteTest.jpf index 00459a90..9897c42e 100644 --- a/src/examples/ByteTest.jpf +++ b/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 \ No newline at end of file diff --git a/src/examples/E5.java b/src/examples/E5.java new file mode 100755 index 00000000..15bd86b3 --- /dev/null +++ b/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 + } + } + + +} diff --git a/src/examples/E5.jpf b/src/examples/E5.jpf new file mode 100755 index 00000000..7e1e77e2 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/src/examples/SubStringTest.jpf b/src/examples/SubStringTest.jpf index ed5aaff4..e1ac6d3e 100644 --- a/src/examples/SubStringTest.jpf +++ b/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 diff --git a/src/examples/strings/ChallengeTest.jpf b/src/examples/strings/ChallengeTest.jpf index ffe0bbac..17aa4b56 100644 --- a/src/examples/strings/ChallengeTest.jpf +++ b/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 diff --git a/src/examples/strings/DelimSearchz.jpf b/src/examples/strings/DelimSearchz.jpf index 2aede631..206d2008 100644 --- a/src/examples/strings/DelimSearchz.jpf +++ b/src/examples/strings/DelimSearchz.jpf @@ -4,8 +4,8 @@ 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 @@ -13,5 +13,5 @@ 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 diff --git a/src/examples/strings/GoodbyeWorld.jpf b/src/examples/strings/GoodbyeWorld.jpf index d52e487a..8e7e2fdd 100644 --- a/src/examples/strings/GoodbyeWorld.jpf +++ b/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 diff --git a/src/examples/strings/HelloWorld.jpf b/src/examples/strings/HelloWorld.jpf index 5ca28fde..a63a2d84 100644 --- a/src/examples/strings/HelloWorld.jpf +++ b/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) diff --git a/src/examples/strings/IndexOfTest.jpf b/src/examples/strings/IndexOfTest.jpf index 6c4abaac..e63a3d36 100644 --- a/src/examples/strings/IndexOfTest.jpf +++ b/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 diff --git a/src/examples/strings/MSExample.jpf b/src/examples/strings/MSExample.jpf index 1dafad94..f27007f7 100644 --- a/src/examples/strings/MSExample.jpf +++ b/src/examples/strings/MSExample.jpf @@ -28,7 +28,8 @@ symbolic.dp=choco # "sat". At the moment symbolic.dp must be equal to # "choco" for it to work. symbolic.strings=true -symbolic.string_dp=z3str2 +symbolic.string_dp=z3str3 +#symbolic.string_dp=ABC #Set the symbolic string executioner timeout (in ms) #zero for no timeout. diff --git a/src/examples/strings/MysteryQuestionMin.jpf b/src/examples/strings/MysteryQuestionMin.jpf index 88e40260..579b2c7b 100644 --- a/src/examples/strings/MysteryQuestionMin.jpf +++ b/src/examples/strings/MysteryQuestionMin.jpf @@ -15,13 +15,14 @@ sourcepath=${jpf-symbc}/src/examples # in this particular configuration all the input # parameters to methods test2 and test are symbolic -symbolic.dp=z3str2 +symbolic.dp=z3str3 +#symbolic.string_dp=ABC # settings for the symbolic string support, either # "none" (default), "cvc", "automata" (recommended) or # "sat". At the moment symbolic.dp must be equal to # "choco" for it to work. -symbolic.string_dp=automata +#symbolic.string_dp=automata #symbolic.string_dp_timeout_ms=0 symbolic.string_dp_timeout_ms=3000 # As a side note for eclipse users, to run cvc3 diff --git a/src/examples/strings/NaivePWCheck.jpf b/src/examples/strings/NaivePWCheck.jpf index e7abea7d..604439d1 100644 --- a/src/examples/strings/NaivePWCheck.jpf +++ b/src/examples/strings/NaivePWCheck.jpf @@ -4,8 +4,8 @@ sourcepath=${jpf-symbc}/src/examples symbolic.strings = true symbolic.dp=choco -#symbolic.string_dp=z3str2 -symbolic.string_dp=ABC +symbolic.string_dp=z3str3 +#symbolic.string_dp=ABC symbolic.string_dp_timeout_ms=3000 symbolic.debug=true @@ -13,5 +13,5 @@ symbolic.method = strings.NaivePWCheck.verifyPassword(sym) 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 diff --git a/src/examples/strings/NaivePWCheckz.jpf b/src/examples/strings/NaivePWCheckz.jpf index 046cfb70..604439d1 100644 --- a/src/examples/strings/NaivePWCheckz.jpf +++ b/src/examples/strings/NaivePWCheckz.jpf @@ -4,8 +4,8 @@ sourcepath=${jpf-symbc}/src/examples symbolic.strings = true symbolic.dp=choco -#symbolic.string_dp=z3str2 -symbolic.string_dp=ABC +symbolic.string_dp=z3str3 +#symbolic.string_dp=ABC symbolic.string_dp_timeout_ms=3000 symbolic.debug=true diff --git a/src/examples/strings/PassCheck01.jpf b/src/examples/strings/PassCheck01.jpf index 3b458ff0..2116b59e 100644 --- a/src/examples/strings/PassCheck01.jpf +++ b/src/examples/strings/PassCheck01.jpf @@ -3,9 +3,9 @@ classpath=${jpf-symbc}/build/examples sourcepath=${jpf-symbc}/src/examples symbolic.strings = true -symbolic.dp=z3 +symbolic.dp=choco #symbolic.string_dp=ABC -symbolic.string_dp=z3str +symbolic.string_dp=z3str2 symbolic.string_dp_timeout_ms=3000 symbolic.debug=true diff --git a/src/examples/strings/PassCheck01z.jpf b/src/examples/strings/PassCheck01z.jpf index 370eeeaa..4b64fc54 100644 --- a/src/examples/strings/PassCheck01z.jpf +++ b/src/examples/strings/PassCheck01z.jpf @@ -13,5 +13,5 @@ symbolic.method= strings.PassCheck.passCheckInsecure(sym) 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 diff --git a/src/examples/strings/PassCheck02.jpf b/src/examples/strings/PassCheck02.jpf index 307b3afb..ae558b1e 100644 --- a/src/examples/strings/PassCheck02.jpf +++ b/src/examples/strings/PassCheck02.jpf @@ -5,6 +5,7 @@ sourcepath=${jpf-symbc}/src/examples symbolic.strings = true symbolic.dp=choco symbolic.string_dp=z3str2 +#symbolic.string_dp=ABC symbolic.string_dp_timeout_ms=3000 symbolic.debug=true @@ -12,5 +13,5 @@ symbolic.method= strings.PassCheck.passCheckSecure(sym) search.depth_limit=17 search.multiple_errors=true #listener = gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener -listener = sidechannel.TimingChannelListener +#listener = sidechannel.TimingChannelListener vm.storage.class=nil diff --git a/src/examples/strings/StringSearch01.jpf b/src/examples/strings/StringSearch01.jpf index cc34dacd..90234f6c 100644 --- a/src/examples/strings/StringSearch01.jpf +++ b/src/examples/strings/StringSearch01.jpf @@ -4,7 +4,8 @@ sourcepath=${jpf-symbc}/src/examples symbolic.strings = true symbolic.dp=choco -symbolic.string_dp=z3str2 +symbolic.string_dp=z3str3 +#symbolic.string_dp=ABC symbolic.string_dp_timeout_ms=3000 symbolic.debug=true @@ -12,5 +13,5 @@ symbolic.method= strings.StringSearch.search_1(conc#sym) search.depth_limit = 12 search.multiple_errors=true #listener = gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener -listener = sidechannel.TimingChannelListener +#listener = sidechannel.TimingChannelListener vm.storage.class=nil diff --git a/src/examples/strings/StringSearch02.jpf b/src/examples/strings/StringSearch02.jpf index c03e3d8b..41e38ecf 100644 --- a/src/examples/strings/StringSearch02.jpf +++ b/src/examples/strings/StringSearch02.jpf @@ -4,6 +4,7 @@ sourcepath=${jpf-symbc}/src/examples symbolic.strings = true symbolic.dp=choco +#symbolic.string_dp=z3str2 symbolic.string_dp=ABC symbolic.string_dp_timeout_ms=3000 symbolic.debug=true diff --git a/src/examples/strings/SubStr.jpf b/src/examples/strings/SubStr.jpf index 8c1d3c38..e8a86e58 100644 --- a/src/examples/strings/SubStr.jpf +++ b/src/examples/strings/SubStr.jpf @@ -4,8 +4,8 @@ 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 diff --git a/src/examples/strings/Tricky.jpf b/src/examples/strings/Tricky.jpf index 08499ba4..7e257f61 100644 --- a/src/examples/strings/Tricky.jpf +++ b/src/examples/strings/Tricky.jpf @@ -15,13 +15,15 @@ sourcepath=${jpf-symbc}/src/examples # in this particular configuration all the input # parameters to methods test2 and test are symbolic -symbolic.dp=coral +#symbolic.dp=coral +symbolic.dp=choco # settings for the symbolic string support, either # "none" (default), "cvc", "automata" (recommended) or # "sat". At the moment symbolic.dp must be equal to # "choco" for it to work. -symbolic.string_dp=z3str2 +#symbolic.string_dp=z3str2 +symbolic.string_dp=ABC # As a side note for eclipse users, to run cvc3 # enabled programs, the eclipse plugin which allows # you to right click on a .jpf test file and click diff --git a/src/main/edu/ucsb/cs/vlab/Z3Interface.java b/src/main/edu/ucsb/cs/vlab/Z3Interface.java index 63787a77..36def06c 100644 --- a/src/main/edu/ucsb/cs/vlab/Z3Interface.java +++ b/src/main/edu/ucsb/cs/vlab/Z3Interface.java @@ -24,7 +24,7 @@ import edu.ucsb.cs.vlab.modelling.Output; import edu.ucsb.cs.vlab.modelling.Output.Model; -import edu.ucsb.cs.vlab.versions.Z3StringProcessor; +import edu.ucsb.cs.vlab.versions.Z3String3Processor; public class Z3Interface { /** @@ -99,7 +99,7 @@ public static class Factory { public static Processor create(Class processableClass) { try { final Kind processableInstance = processableClass.newInstance(); - final ProcessLambda process = () -> Runtime.getRuntime().exec(Z3.getInteractive()); + final ProcessLambda process = () -> Runtime.getRuntime().exec(Z3_3.getInteractive()); return new Processor(processableInstance, process); } catch (InstantiationException | IllegalAccessException e) { e.printStackTrace(); @@ -186,7 +186,8 @@ public Output finish(String message) throws IOException, RuntimeException { * @return the processor to use */ public static Z3Interface.Processor create() { - return Z3Interface.Processor.Factory.create(Z3StringProcessor.class); + return null; + //return Z3Interface.Processor.Factory.create(Z3String3Processor.class); } public static class ExternalToolException extends RuntimeException { diff --git a/src/main/edu/ucsb/cs/vlab/Z3_3.java b/src/main/edu/ucsb/cs/vlab/Z3_3.java new file mode 100644 index 00000000..14c75c68 --- /dev/null +++ b/src/main/edu/ucsb/cs/vlab/Z3_3.java @@ -0,0 +1,50 @@ +package edu.ucsb.cs.vlab; + +import java.io.FileInputStream; +import java.io.FileNotFoundException; +import java.io.IOException; +import java.util.Properties; +import java.util.Random; + +import edu.ucsb.cs.vlab.Z3Interface.Processor; + +public class Z3_3 { + private static final Properties PROPERTIES; + + static { + PROPERTIES = new Properties(); + try (final FileInputStream in = new FileInputStream(System.getProperty("user.home") + "/.jpf/site.properties")) { + PROPERTIES.load(in); + } catch (FileNotFoundException e) { + e.printStackTrace(); + } catch (IOException e) { + e.printStackTrace(); + } + } + + public static Properties getProperties() { + return PROPERTIES; + } + + public static String getBinary() { + return getProperties().getProperty("strings.z3", "/usr/local/bin/z3"); + } + + public static String getInteractive() { + return getBinary() + " " + getProperties().getProperty("strings.interactive_flags", " -smt2 -file:./temp.z3str smt.string_solver=z3str3"); + } + + public static boolean saveTempFileAfterRun() { + return getProperties().getProperty("strings.keep_temp", "yes").equalsIgnoreCase("yes"); + } + + public static Processor create() { + return Z3Interface.create(); + } + + public static final int random = new Random(System.currentTimeMillis()).nextInt(); + + public static String getTempFile() { + return "./temp.z3str"; + } +} diff --git a/src/main/edu/ucsb/cs/vlab/translate/smtlib/from/Translator.java b/src/main/edu/ucsb/cs/vlab/translate/smtlib/from/Translator.java index ac517b75..8fb53357 100644 --- a/src/main/edu/ucsb/cs/vlab/translate/smtlib/from/Translator.java +++ b/src/main/edu/ucsb/cs/vlab/translate/smtlib/from/Translator.java @@ -130,11 +130,17 @@ public String getHeader() { } public String getFooter() { + return "(check-sat)\n(get-model)\n"; } public String createSymbolicDeclaration(final Set symbolicVars, String type) { - return symbolicVars.parallelStream().map((var) -> "(declare-variable " + var + " " + type + ")") + + //return symbolicVars.parallelStream().map((var) -> "(declare-variable " + var + " " + type + ")") + // .collect(Collectors.joining("\n")); + + // MJR 06/25/21 smt-lib 2.5 uses declare-const for variable declarations + return symbolicVars.parallelStream().map((var) -> "(declare-const " + var + " " + type + ")") .collect(Collectors.joining("\n")); } diff --git a/src/main/edu/ucsb/cs/vlab/translate/smtlib/from/z3str3/Z3Translator.java b/src/main/edu/ucsb/cs/vlab/translate/smtlib/from/z3str3/Z3Translator.java new file mode 100644 index 00000000..b6affd57 --- /dev/null +++ b/src/main/edu/ucsb/cs/vlab/translate/smtlib/from/z3str3/Z3Translator.java @@ -0,0 +1,235 @@ +package edu.ucsb.cs.vlab.translate.smtlib.from.z3str3; + +import java.util.HashMap; +import java.util.function.Function; + +import edu.ucsb.cs.vlab.translate.smtlib.Results; +import edu.ucsb.cs.vlab.translate.smtlib.StringOrOperation; +import edu.ucsb.cs.vlab.translate.smtlib.TranslationManager; +import edu.ucsb.cs.vlab.translate.smtlib.from.Translator; +import edu.ucsb.cs.vlab.translate.smtlib.generic.NumericConstraintTranslator; +import edu.ucsb.cs.vlab.translate.smtlib.generic.NumericExpressionTranslator; +import edu.ucsb.cs.vlab.translate.smtlib.generic.StringConstraintTranslator; +import edu.ucsb.cs.vlab.translate.smtlib.generic.StringExpressionTranslator; +import gov.nasa.jpf.symbc.numeric.BinaryLinearIntegerExpression; +import gov.nasa.jpf.symbc.numeric.Comparator; +import gov.nasa.jpf.symbc.numeric.IntegerConstant; +import gov.nasa.jpf.symbc.numeric.IntegerExpression; +import gov.nasa.jpf.symbc.numeric.SymbolicInteger; +import gov.nasa.jpf.symbc.string.DerivedStringExpression; +import gov.nasa.jpf.symbc.string.StringComparator; +import gov.nasa.jpf.symbc.string.StringConstant; +import gov.nasa.jpf.symbc.string.StringExpression; +import gov.nasa.jpf.symbc.string.StringSymbolic; +import gov.nasa.jpf.symbc.string.SymbolicCharAtInteger; +import gov.nasa.jpf.symbc.string.SymbolicIndexOf2Integer; +import gov.nasa.jpf.symbc.string.SymbolicIndexOfChar2Integer; +import gov.nasa.jpf.symbc.string.SymbolicIndexOfCharInteger; +import gov.nasa.jpf.symbc.string.SymbolicIndexOfInteger; +import gov.nasa.jpf.symbc.string.SymbolicLastIndexOf2Integer; +import gov.nasa.jpf.symbc.string.SymbolicLastIndexOfChar2Integer; +import gov.nasa.jpf.symbc.string.SymbolicLastIndexOfCharInteger; +import gov.nasa.jpf.symbc.string.SymbolicLastIndexOfInteger; +import gov.nasa.jpf.symbc.string.SymbolicLengthInteger; + +class Manager extends TranslationManager { + + /* + * Numeric constraints + */ + public static class NumericConstraints extends NumericConstraintTranslator { + public NumericConstraints(TranslationManager manager) { + super(manager); + } + + public void init() { + rules.put(Comparator.EQ, createConstraint("(=")); + rules.put(Comparator.GE, createConstraint("(>=")); + rules.put(Comparator.GT, createConstraint("(>")); + rules.put(Comparator.LE, createConstraint("(<=")); + rules.put(Comparator.LT, createConstraint("(<")); + rules.put(Comparator.NE, createConstraint("(not (=")); + } + } + + /* + * Numeric expressions + */ + public static class NumericExpressions extends NumericExpressionTranslator { + public NumericExpressions(TranslationManager manager) { + super(manager); + } + + public void init() { + replacements = new HashMap<>(); + replacements.put("/", "div"); + + map(SymbolicLastIndexOfCharInteger.class, "LastIndexof $getSource ?getExpression"); + map(SymbolicLastIndexOfChar2Integer.class, + "LastIndexof ( str.substr $getSource %getMinDist ( - (str.len $getSource ) %getMinDist )) ?getExpression"); + + map(BinaryLinearIntegerExpression.class, "_getOp %getLeft %getRight"); + map(SymbolicCharAtInteger.class, "str.at $getExpression %getIndex"); + map(SymbolicIndexOf2Integer.class, "str.indexof $getSource $getExpression %getMinIndex"); + map(SymbolicIndexOfInteger.class, "str.indexof $getSource $getExpression"); + + map(SymbolicLastIndexOf2Integer.class, + "LastIndexof ( str.substr $getSource %getMinIndex ( - (str.len $getSource ) %getMinIndex )) $getExpression"); + map(SymbolicLastIndexOfInteger.class, "LastIndexof $getSource $getExpression"); + + map(SymbolicLengthInteger.class, "str.len $getExpression"); + map(SymbolicIndexOfCharInteger.class, "str.indexof $getSource ?getExpression"); + map(SymbolicIndexOfChar2Integer.class, "str.indexof $getSource ?getExpression %getMinDist"); + + rules.put(IntegerConstant.class, (x) -> { + final int v = (int) ((IntegerConstant) x).value; + if (v >= 0) + return Integer.toString(v); + else + return "(- " + Integer.toString(-v) + ")"; + }); + + rules.put(SymbolicInteger.class, (x) -> { + final SymbolicInteger si = (SymbolicInteger) x; + Results.numericVariables.add(si.getName()); + return si.getName(); + }); + } + } + + /* + * String constraints + */ + public static class StringConstraints extends StringConstraintTranslator { + public StringConstraints(TranslationManager manager) { + super(manager); + } + + public void init() { + map(StringComparator.CONTAINS, "(str.contains"); + map(StringComparator.NOTCONTAINS, "(not (str.contains"); + map(StringComparator.STARTSWITH, "(str.prefixof"); + map(StringComparator.NOTSTARTSWITH, "(not (str.prefixof"); + map(StringComparator.ENDSWITH, "(str.suffixof"); + map(StringComparator.NOTENDSWITH, "(not (str.suffixof"); + map(StringComparator.EQUALS, "(="); + map(StringComparator.NOTEQUALS, "(not (="); + map(StringComparator.EQUALSIGNORECASE, "(equalsIgnoreCase"); + map(StringComparator.NOTEQUALSIGNORECASE, "(not (equalsIgnoreCase"); + map(StringComparator.EMPTY, "(empty"); + map(StringComparator.NOTEMPTY, "(not (empty"); + map(StringComparator.MATCHES, "(matches"); + map(StringComparator.NOMATCHES, "(not (matches"); + map(StringComparator.REGIONMATCHES, "(regionMatches"); + map(StringComparator.NOREGIONMATCHES, "(not (regionMatches"); + map(StringComparator.ISINTEGER, "(isInteger"); + map(StringComparator.ISFLOAT, "(isFloat"); + map(StringComparator.ISLONG, "(isLong"); + map(StringComparator.ISDOUBLE, "(isDouble"); + map(StringComparator.ISBOOLEAN, "(isBoolean"); + map(StringComparator.NOTINTEGER, "(not (isInteger"); + map(StringComparator.NOTFLOAT, "(not (isFloat"); + map(StringComparator.NOTLONG, "(not (isLong"); + map(StringComparator.NOTDOUBLE, "(not (isDouble"); + map(StringComparator.NOTBOOLEAN, "(not (isBoolean"); + } + } + + /* + * String Expressions + */ + public static class StringExpressions extends StringExpressionTranslator { + public StringExpressions(TranslationManager manager) { + super(manager); + } + + public void init() { + final Function> ReplaceTemplate = (prefix) -> { + return (expr) -> { + final DerivedStringExpression dse = (DerivedStringExpression) expr; + final String arg0 = manager.strExpr.collect((StringExpression) dse.oprlist[0]); + final String arg1 = manager.strExpr.collect((StringExpression) dse.oprlist[1]); + final String arg2 = manager.strExpr.collect((StringExpression) dse.oprlist[2]); + return prefix + " " + arg0 + " " + arg1 + " " + arg2 + ")"; + }; + }; + + final Function> RightTemplate = (prefix) -> { + return (expr) -> { + final DerivedStringExpression dse = (DerivedStringExpression) expr; + final String rightArg = manager.strExpr.collect(dse.right); + return prefix + " " + rightArg + ")"; + }; + }; + + map(StringOrOperation.NONSYM, (expr) -> { + return "\"" + ((StringConstant) expr).value + "\""; + }); + + map(StringOrOperation.SYM, (expr) -> { + final String symVarName = ((StringSymbolic) expr).fixName(((StringSymbolic) expr).getName()); + Results.stringVariables.add(symVarName); + return symVarName; + }); + + map(StringOrOperation.CONCAT, (expr) -> { + final DerivedStringExpression dse = (DerivedStringExpression) expr; + final String leftArg = manager.strExpr.collect(dse.left); + final String rightArg = manager.strExpr.collect(dse.right); + return "(str.++ " + leftArg + " " + rightArg + ")"; + }); + + map(StringOrOperation.SUBSTRING, (expr) -> { + final DerivedStringExpression dse = (DerivedStringExpression) expr; + final String arg1 = manager.strExpr.collect((StringExpression) dse.oprlist[0]); + final String arg2 = manager.numExpr.collect((IntegerExpression) dse.oprlist[1]); + + if (dse.oprlist.length == 2) + return "(str.substr " + arg1 + " " + arg2 + "(- (str.len " + arg1 + ") " + arg2 + "))"; + else { + final String arg3 = manager.numExpr.collect((IntegerExpression) dse.oprlist[2]); + return "(str.substr " + arg1 + " " + arg3 + " (- " + arg2 + " " + arg3 + "))"; + } + }); + + map(StringOrOperation.REPLACE, ReplaceTemplate.apply("(str.replace")); + map(StringOrOperation.REPLACEALL, ReplaceTemplate.apply("(replaceAll")); + map(StringOrOperation.REPLACEFIRST, ReplaceTemplate.apply("(replaceFirst")); + + map(StringOrOperation.TRIM, RightTemplate.apply("(trim")); + map(StringOrOperation.TOLOWERCASE, RightTemplate.apply("(toLowerCase")); + map(StringOrOperation.TOUPPERCASE, RightTemplate.apply("(toUpperCase")); + + map(StringOrOperation.VALUEOF, (expr) -> { + String arg = null; + final DerivedStringExpression dse = (DerivedStringExpression) expr; + if (dse.oprlist[0] instanceof StringExpression) { + arg = manager.strExpr.collect((StringExpression) dse.oprlist[0]); + } else if (dse.oprlist[0] instanceof IntegerExpression) { + arg = manager.numExpr.collect((IntegerExpression) dse.oprlist[0]); + } + + try { + Integer.parseInt(arg); + return "\"" + arg + "\""; + } catch (NumberFormatException e) { + return arg; + } + }); + } + } + + public Manager() { + super(); + this.numCons = new NumericConstraints(this); + this.numExpr = new NumericExpressions(this); + this.strCons = new StringConstraints(this); + this.strExpr = new StringExpressions(this); + } +} + +public class Z3Translator extends Translator { + public Z3Translator() { + super(new Manager()); + } +} diff --git a/src/main/edu/ucsb/cs/vlab/versions/Z3String3Processor.java b/src/main/edu/ucsb/cs/vlab/versions/Z3String3Processor.java new file mode 100644 index 00000000..507175c3 --- /dev/null +++ b/src/main/edu/ucsb/cs/vlab/versions/Z3String3Processor.java @@ -0,0 +1,158 @@ +package edu.ucsb.cs.vlab.versions; + +import java.io.BufferedReader; +import java.io.IOException; +//import java.io.InputStreamReader; +import java.io.StringReader; +//import java.nio.file.Files; +//import java.nio.file.Paths; +import java.util.ArrayList; +import java.util.List; + +//import edu.ucsb.cs.vlab.Z3_3; +//import edu.ucsb.cs.vlab.Z3Interface.ExternalToolException; +import edu.ucsb.cs.vlab.Z3Interface.Processable; +import edu.ucsb.cs.vlab.Z3Interface.Processor; +import edu.ucsb.cs.vlab.modelling.Output; +import edu.ucsb.cs.vlab.modelling.Output.Model; + +import gov.nasa.jpf.symbc.SymbolicInstructionFactory; + +import com.microsoft.z3.*; + +// TODO: This will not need to implement Processable in final version. +public class Z3String3Processor { + final Model model = new Model(); + final StringBuilder currentQuery = new StringBuilder(); + + + public void send(String message) { + currentQuery.append(message + "\n"); + } + + + public void query(String message) { + currentQuery.append(message + "\n"); + + // MJR not doing file IO, using JNI interface + //Files.write(Paths.get(Z3_3.getTempFile()), currentQuery.toString().getBytes()); + } + + public Output getOutput() throws IOException { + + boolean sat = false; + + + Context context1 = new Context(); + Solver solver1 = context1.mkSolver(); + + Params params = context1.mkParams(); + //params.add("candidate_models", true); + //params.add("fail_if_inconclusive", false); + params.add("smt.string_solver", "z3str3"); + + // SymbolicInstructionFactory populated these public vars since z3str3 was specified. + params.add("str.aggressive_length_testing", SymbolicInstructionFactory.z3str3_aggressive_length_testing); + params.add("str.aggressive_unroll_testing", SymbolicInstructionFactory.z3str3_aggressive_unroll_testing); + params.add("str.aggressive_value_testing", SymbolicInstructionFactory.z3str3_aggressive_value_testing); + params.add("str.fast_length_tester_cache", SymbolicInstructionFactory.z3str3_fast_length_tester_cache); + params.add("str.fast_value_tester_cache", SymbolicInstructionFactory.z3str3_fast_value_tester_cache); + params.add("str.fixed_length_naive_cex", SymbolicInstructionFactory.z3str3_fixed_length_naive_cex); + params.add("str.fixed_length_refinement", SymbolicInstructionFactory.z3str3_fixed_length_refinement); + params.add("str.string_constant_cache", SymbolicInstructionFactory.z3str3_string_constant_cache); + params.add("str.strong_arrangements", SymbolicInstructionFactory.z3str3_strong_arrangements); + + solver1.setParameters(params); + + // Translator added (check-sat) and (get-model) to our query. We need to remove them since we will be + // performing those functions through our JNI/JAR interface. The query is multiple lines, so a + // reader allows us to check line by line. + + final BufferedReader queryReader = new BufferedReader(new StringReader(currentQuery.toString())); + StringBuilder finalQuery = new StringBuilder(); + + String queryLine = queryReader.readLine(); + + while (queryLine != null) { + if (!queryLine.startsWith("(check-sat)") && !queryLine.startsWith("(get-model)")) { + finalQuery.append(queryLine + "\n"); + } + queryLine = queryReader.readLine(); + } + queryReader.close(); + + if (SymbolicInstructionFactory.debugMode) { + System.out.println("current query... " + finalQuery.toString()); + } + + // attempt to parse the query, if successful continue with checking satisfiability + try { + + // throws z3 exception if malformed or unknown constant/operation + BoolExpr[] assertions = context1.parseSMTLIB2String(finalQuery.toString(),null, null, null, null); + + solver1.add(assertions); + + // check sat, if so we can go ahead and get the model.... + if (solver1.check() == Status.SATISFIABLE) { + sat = true; + + if (SymbolicInstructionFactory.debugMode) { + System.out.println(solver1.getModel().toString()); + } + + String returned = solver1.getModel().toString(); + final BufferedReader reader = new BufferedReader(new StringReader(returned)); + + List solutions = new ArrayList<>(); + + String line = reader.readLine(); + while (line != null) { + + if (line.contains("define-fun")) { + solutions.add(line + reader.readLine()); + } + line = reader.readLine(); + } + + // output returned solutions and populate SPF output model. + System.out.println("Returned solutions: "); + for(String s : solutions) { + System.out.println(s.trim()); + String value = s.substring(s.indexOf("\""), s.length() -1); + String[] parts = s.split(" "); + + model.put(parts[1], value); + + } + + reader.close(); + + } // end of sat section + + context1.close(); + + } + catch (com.microsoft.z3.Z3Exception e) { + System.out.println("Z3 exception: " + e.getMessage()); + } + + return new Output(sat, assembleModel()); + } + + public void process(String line) { + final String[] parts = line.split(" -> "); + final String[] typeAndName = parts[0].split(" : "); + + final String name = typeAndName[0].trim(); + final String type = typeAndName[1].trim(); + final String value = parts[1].trim(); + + model.put(name, value); + } + + public Model assembleModel() { + return model; + } + +} diff --git a/src/main/gov/nasa/jpf/symbc/SymbolicInstructionFactory.java b/src/main/gov/nasa/jpf/symbc/SymbolicInstructionFactory.java index 6920ae18..c54dfbdc 100644 --- a/src/main/gov/nasa/jpf/symbc/SymbolicInstructionFactory.java +++ b/src/main/gov/nasa/jpf/symbc/SymbolicInstructionFactory.java @@ -544,6 +544,12 @@ public Instruction multianewarray(String clsName, int dimensions){ static public String[] string_dp; static public int stringTimeout; static public boolean preprocesOnly; + + /* MJR Additional config options for strings */ + static public int stringLowerBound; + static public int stringUpperBound; + static public String stringAlphabet; + static public int stringAlphabetSize; /* * This is intended to serve as a catchall debug flag. @@ -601,6 +607,18 @@ public Instruction multianewarray(String clsName, int dimensions){ static public int maxPcLength; static public long maxPcMSec; static public long startSystemMillis; + + // MJR additional properties for z3str3. + // The defaults will be set if the property is not present in the jpf file. + static public boolean z3str3_aggressive_length_testing; + static public boolean z3str3_aggressive_unroll_testing; + static public boolean z3str3_aggressive_value_testing; + static public boolean z3str3_fast_length_tester_cache; + static public boolean z3str3_fast_value_tester_cache; + static public boolean z3str3_fixed_length_naive_cex; + static public boolean z3str3_fixed_length_refinement; + static public boolean z3str3_string_constant_cache; + static public boolean z3str3_strong_arrangements; ClassInfo ci; ClassInfoFilter filter; // TODO: fix; do we still need this? @@ -651,6 +669,32 @@ public SymbolicInstructionFactory (Config conf){ stringTimeout = conf.getInt("symbolic.string_dp_timeout_ms"); if (debugMode) System.out.println("symbolic.string_dp_timeout_ms="+stringTimeout); + + // MJR additional string parameters from JPF file + stringAlphabet = conf.getString("symbolic.string_dp_alpha"); + if (stringAlphabet == null) { + stringAlphabet = "A-Z"; + } + if (debugMode) System.out.println("symbolic.string_dp_alpha="+stringAlphabet); + + stringAlphabetSize = conf.getInt("symbolic.string_dp_alphaSize", 0); + if (stringAlphabetSize == 0) { + stringAlphabetSize = 26; + } + if (debugMode) System.out.println("symbolic.string_dp_alphaSize="+stringAlphabetSize); + + stringUpperBound = conf.getInt("symbolic.string_dp_upper", 0); + if (stringUpperBound == 0) { + stringUpperBound = 10; + } + if (debugMode) System.out.println("symbolic.string_dp_upper="+stringUpperBound); + + stringLowerBound = conf.getInt("symbolic.string_dp_lower", -1); + if (stringLowerBound == -1) { + stringLowerBound = 1; + } + if (debugMode) System.out.println("symbolic.string_dp_lower="+stringLowerBound); + // MJR end of additional string parameters string_dp = conf.getStringArray("symbolic.string_dp"); if (string_dp == null) { @@ -658,6 +702,22 @@ public SymbolicInstructionFactory (Config conf){ string_dp[0] = "none"; } if (debugMode) System.out.println("symbolic.string_dp="+string_dp[0]); + + // MJR Populate z3str3 properties, get each from the jpf file and populate the conf properties. + // Choose the default if the property is not present. + if (string_dp[0].equals("z3str3")) { + + z3str3_aggressive_length_testing = conf.getBoolean("symbolic.z3str3_aggressive_length_testing", false); + z3str3_aggressive_unroll_testing = conf.getBoolean("symbolic.z3str3_aggressive_unroll_testing", true); + z3str3_aggressive_value_testing = conf.getBoolean("symbolic.z3str3_aggressive_value_testing", false); + z3str3_fast_length_tester_cache = conf.getBoolean("symbolic.z3str3_fast_length_tester_cache", true); + z3str3_fast_value_tester_cache = conf.getBoolean("symbolic.z3str3_fast_value_tester_cache", true); + z3str3_fixed_length_naive_cex = conf.getBoolean("symbolic.z3str3_fixed_length_naive_cex", true); + z3str3_fixed_length_refinement = conf.getBoolean("symbolic.z3str3_fixed_length_refinement", false); + z3str3_string_constant_cache = conf.getBoolean("symbolic.z3str3_string_constant_cache", true); + z3str3_strong_arrangements = conf.getBoolean("symbolic.z3str3_strong_arrangements", true); + + } preprocesOnly = conf.getBoolean("symbolic.string_preprocess_only", false); String[] concolic = conf.getStringArray("symbolic.concolic"); diff --git a/src/main/gov/nasa/jpf/symbc/string/StringPathCondition.java b/src/main/gov/nasa/jpf/symbc/string/StringPathCondition.java index a8255b5c..120b2e21 100644 --- a/src/main/gov/nasa/jpf/symbc/string/StringPathCondition.java +++ b/src/main/gov/nasa/jpf/symbc/string/StringPathCondition.java @@ -149,7 +149,11 @@ public boolean simplify() { public String stringPC() { return "SPC # = " + count + ((header == null) ? "" : "\n" + header.stringPC()) +"\n" + "NPC "+npc.stringPC(); - } + } + + public String stringSPC() { + return header.stringPC(); + } public String toString() { return "SPC # = " + count + ((header == null) ? "" : "\n" + header.toString()) +"\n" diff --git a/src/main/gov/nasa/jpf/symbc/string/SymbolicStringConstraintsGeneral.java b/src/main/gov/nasa/jpf/symbc/string/SymbolicStringConstraintsGeneral.java index 385b11f7..4c44025e 100644 --- a/src/main/gov/nasa/jpf/symbc/string/SymbolicStringConstraintsGeneral.java +++ b/src/main/gov/nasa/jpf/symbc/string/SymbolicStringConstraintsGeneral.java @@ -67,10 +67,12 @@ import gov.nasa.jpf.symbc.string.translate.TranslateToAutomata2; import gov.nasa.jpf.symbc.string.translate.TranslateToCVC; import gov.nasa.jpf.symbc.string.translate.TranslateToCVCInc; +import gov.nasa.jpf.symbc.string.translate.TranslateToIGEN; import gov.nasa.jpf.symbc.string.translate.TranslateToSAT; import gov.nasa.jpf.symbc.string.translate.TranslateToZ3; import gov.nasa.jpf.symbc.string.translate.TranslateToZ3Inc; import gov.nasa.jpf.symbc.string.translate.TranslateToZ3str2; +import gov.nasa.jpf.symbc.string.translate.TranslateToZ3str3; import gov.nasa.jpf.util.LogManager; /** @@ -115,6 +117,7 @@ public class SymbolicStringConstraintsGeneral { /*Possible sovlers for now */ public static final String ABC = "ABC"; public static final String Z3STR2 = "Z3str2"; + public static final String Z3STR3 = "Z3str3"; public static final String AUTOMATA = "Automata"; public static final String SAT = "Sat"; public static final String CVC = "CVC"; @@ -122,6 +125,7 @@ public class SymbolicStringConstraintsGeneral { public static final String Z3 = "Z3"; public static final String Z3_INC = "Z3_INC"; public static final String WRAPPER = "WRAPPER"; //automata+z3 + public static final String IGEN = "IGEN"; // BSU Input generator /* Default solver */ public static String solver = AUTOMATA; @@ -393,12 +397,18 @@ private boolean inner_isSatisfiable(StringPathCondition pc) { else if (string_dp[0].equals("z3str2")) { solver = Z3STR2; } + else if (string_dp[0].equals("z3str3")) { + solver = Z3STR3; + } else if (string_dp[0].equals("ABC")) { solver = ABC; } else if (string_dp[0].equals("sat")) { solver = SAT; } + else if (string_dp[0].equals("igen")) { + solver = IGEN; + } else if (string_dp[0].equals("cvc")) { solver = CVC; } @@ -434,6 +444,14 @@ else if(solver.equals(Z3STR2)){ return dpresult.isSAT(); } + else if(solver.equals(Z3STR3)){ + System.out.println("$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$"); + System.out.println("Calling Z3str3\n"); + final Output dpresult = TranslateToZ3str3.solve(pc); + constraintCount = constraintCount + 1; + return dpresult.isSAT(); + } + TIMEOUT = SymbolicInstructionFactory.stringTimeout; SymbolicStringConstraintsGeneral.timedOut = false; @@ -538,7 +556,32 @@ else if(solver.equals(Z3STR2)){ //println ("[isSatisfiable] Using SAT Solver"); decisionProcedure = TranslateToSAT.isSat(global_graph, pc.getNpc()); } - if (solver.equals(ABC)) { + else if (solver.equals(IGEN)) { + System.out.println("[SymbolicStringConstraintGeneral] Using Solver IGEN"); +// System.out.println("global graph start -----------------------------"); +// System.out.println(global_graph.toDot()); +// System.out.println("global graph end -----------------------------"); + + +// System.out.println("========= npc: " + pc.getNpc().toString()); +// System.out.println("========= spc: " + pc.stringPC()); + + // pc is a string path condition, containing a numeric pc from the numeric solver. + // this inner npc has + decisionProcedure = TranslateToIGEN.isSat(global_graph, pc.getNpc()); + + + // **** instead of passing solution in GG, pass it back in pc.solution Map + // --- no ---- populate setOfSolution with strings from pc.solution. + // after setOfSolutions is rebuilt from global_graph, match TranslateToIGEN.solution + // back to entries in setOfSolutions + + // report results, return decisionProcedure + + + + } + else if (solver.equals(ABC)) { logger.info ("[isSatisfiable] Using ABC Solver"); //decisionProcedure = TranslateToSAT.isSat(global_graph, pc.npc); decisionProcedure = false; @@ -715,6 +758,18 @@ else if (!e.isHyper() && (e.getSource().equals (v) || e.getDest().equals(v))) { } } //} + + // MJR: At this point setOfSolution has been rebuilt from the global graph + // in the case of IGEN, the global graph did not have solutions encoded in it + // add code here to update the setOfSolutions with the solutions from TranslateToIGEN + // hack to update setOfSolution with returned inputs from TranslateToIGEN + // should be replaced by placing solutions into global graph? + if (solver.equals(IGEN)) { + for (StringSymbolic ss : setOfSolution) { + ss.solution = TranslateToIGEN.solution.get(ss.getName()); + } + } + StringPathCondition.flagSolved = true; //println ("StringPC: " + getSolution()); cancelTimer(); diff --git a/src/main/gov/nasa/jpf/symbc/string/translate/TranslateToIGEN.java b/src/main/gov/nasa/jpf/symbc/string/translate/TranslateToIGEN.java new file mode 100755 index 00000000..36eb87fc --- /dev/null +++ b/src/main/gov/nasa/jpf/symbc/string/translate/TranslateToIGEN.java @@ -0,0 +1,148 @@ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * Symbolic Pathfinder (jpf-symbc) is licensed 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 gov.nasa.jpf.symbc.string.translate; + +import java.io.File; +import java.io.IOException; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.nio.file.Files; +import java.nio.file.Paths; + +import gov.nasa.jpf.symbc.SymbolicInstructionFactory; +import gov.nasa.jpf.symbc.numeric.PathCondition; +import gov.nasa.jpf.symbc.string.graph.StringGraph; + +import parser.Alphabet; +import parser.StoJ; +import edu.boisestate.cs.SPFFileRunner; + +import com.fasterxml.jackson.core.JsonParseException; +import com.fasterxml.jackson.databind.JsonMappingException; +import com.fasterxml.jackson.databind.ObjectMapper; +import com.fasterxml.jackson.databind.SerializationFeature; + + + +public class TranslateToIGEN { + + public static Map solution; + + @SuppressWarnings("unchecked") + public static boolean isSat (StringGraph g, PathCondition pc) { + + // declare alphabet and set size and declaration to the values + // obtained from the jpf file (or the defaults that were populated) + Alphabet alpha = new Alphabet(); + alpha.size = SymbolicInstructionFactory.stringAlphabetSize; + alpha.declaration = SymbolicInstructionFactory.stringAlphabet; + + // set the initial bound to the value from the jpf file + int initialBound = SymbolicInstructionFactory.stringUpperBound; + + // output file name + String outputFile = "spc_graph_" + Long.toString(System.nanoTime()) + ".json"; + + // reference to the string path condition inside the path condition + String thisPC = pc.spc.stringSPC(); + System.out.println("[TranslateToIGEN] Converting SPC: " + thisPC); + + // attempt to convert SPC to JSON file for input to solver + StoJ converter = new StoJ(); + if (!converter.toJSONFile(thisPC, initialBound, alpha, outputFile)) { + System.out.println("[TranslateToIGEN] Something went horribly wrong ..."); + }; + + System.out.println("[TranslateToIGEN] Passing SPC Graph File: " + outputFile); + + // SPFFileRunner is the entry point for running solver on graph file with output back to file + SPFFileRunner fr = new SPFFileRunner(); + + // solve the graph and return the solution file name + String solutionFile = fr.solveGraph(outputFile); + + System.out.println("[TranslateToIGEN] Receiving Solution File: " + solutionFile); + + // setup object mapper + ObjectMapper mapper = new ObjectMapper(); + mapper.enable(SerializationFeature.INDENT_OUTPUT); + + // reference to solution file + File SPFSolutions = new File(solutionFile); + + // default to UNSAT + boolean SAT = false; + + // this will hold the solutions obtained from the JSON solution file + Map solutions; + + // this will hold the string/string solutions to put back into the spc + solution = new HashMap(); + + try { + + // read the solutions from the JSON file + solutions = mapper.readValue(SPFSolutions, Map.class); + + // get the SAT entry + SAT = (boolean) solutions.get("SAT"); + + // get the input node section from the JSON data + List> solutionData = (List>) solutions.get("inputs"); + + // for every input node, get the symbolic var name and input value, populate solution + for (Map obj : solutionData) { + + String symVar = (String) obj.get("SPFsym"); + String symInp = (String) obj.get("input"); + solution.put(symVar, symInp); + + System.out.println("[TranslateToIGEN] SPF Input: " + symVar + " Value: " + symInp); + + // place solutions back into the SPC + // not sure why the original pc.spc.solution is immutable? + pc.spc.solution = solution; + + } + + // cleanup + Files.deleteIfExists(Paths.get(solutionFile)); + Files.deleteIfExists(Paths.get(outputFile)); + + + } catch (JsonParseException e) { + // TODO Auto-generated catch block + e.printStackTrace(); + } catch (JsonMappingException e) { + // TODO Auto-generated catch block + e.printStackTrace(); + } catch (IOException e) { + // TODO Auto-generated catch block + e.printStackTrace(); + } + + // The solution contains the input to string solution mappings, it is public. + // The calling SymbolicStringConstraintGeneral can access it or look in pc.spc.solution + + return SAT; + } + + +} diff --git a/src/main/gov/nasa/jpf/symbc/string/translate/TranslateToZ3str3.java b/src/main/gov/nasa/jpf/symbc/string/translate/TranslateToZ3str3.java new file mode 100644 index 00000000..f24a6dfd --- /dev/null +++ b/src/main/gov/nasa/jpf/symbc/string/translate/TranslateToZ3str3.java @@ -0,0 +1,54 @@ +package gov.nasa.jpf.symbc.string.translate; + +import java.io.IOException; +import java.util.logging.Logger; + +import edu.ucsb.cs.vlab.Z3_3; +import edu.ucsb.cs.vlab.Z3Interface.Processor; +import edu.ucsb.cs.vlab.modelling.Output; +import edu.ucsb.cs.vlab.translate.smtlib.from.z3str3.Z3Translator; +import edu.ucsb.cs.vlab.versions.Z3String3Processor; +import gov.nasa.jpf.symbc.string.StringPathCondition; +import gov.nasa.jpf.util.LogManager; + +public class TranslateToZ3str3 { + static Logger logger = LogManager.getLogger("TranslateToZ3str3"); + + public static Output solve(StringPathCondition pc) { + Output o = null; + + final Z3Translator translator = new Z3Translator(); + final String constraintZ3str3 = translator.translate(pc); + + //try (final Processor p = Z3_3.create()) { + Z3String3Processor stringProcessor = new Z3String3Processor(); + stringProcessor.query(constraintZ3str3); + + // TODO: move this exception handling into Z3String3Processor + try { + final Output out = stringProcessor.getOutput(); + + o = new Output(out.isSAT(), out.getModel()); + + System.out.println("*************************************"); + System.out.println("Satisfiable: " + o.isSAT()); + for (String k : o.getModel().keySet()) { + System.out.println(k + " => " + o.getModel().get(k)); + } + System.out.println("*************************************\n"); + + } catch (IOException e) { + + } + + + //} catch (IOException e) { + //e.printStackTrace(); + //} catch (RuntimeException e) { + // e.printStackTrace(); + //} + + return o; + } + +} diff --git a/string-solver-integration.md b/string-solver-integration.md new file mode 100644 index 00000000..a29f3216 --- /dev/null +++ b/string-solver-integration.md @@ -0,0 +1,60 @@ +string-solver-integration.md + +## String Constraint Solvers in SPF ## + +These are general notes on integrating string solvers into SPF. While there are many ways this can be accomplished, these notes present a straightforward approach that can be adapted to most any solver. + +### Accessing the solver from Java ### + +First, the solver must be accessible through Java, ideally through a .jar file placed in the lib directory. In the case of a solver that is written in a language other than Java, this .jar file acts as a wrapper around the native language solver methods and objects using the Java Native Interface, JNI. These methods will be called by the solver translation code developed specifically for the given solver. + +Example .jar files: +__com.microsoft.z3.jar__ +__automaton.jar__ + +If a .jar file does not exist for a solver, JNI code can be placed directly in the translation class as an alternative. In both cases, the native libraries needed to support JNI for a specific platform need to be accessible in the lib directory. + +Example JNI code: +__edu.ucsb.cs.vlab.DriverProxy.java__ + +### Translating SPF constructs to solver inputs ### + +Second, a translation class needs to be created in SPF that provides the method _isSat()_ that returns the satisfiability of a given string path condition. It takes as parameters the SPF global graph and a path condition. The translation class is responsible for interpreting the path condition and global graph and translating them into a set of constructs compatible with the given solver. The translation class accesses the solver using the methods and objects provided in the .jar file, or with JNI code accessing the solver libraries directly. + +If the solver returns a solution for variables in addition to satisfiability, the translation class is responsible for populating the string path condition solution property with the solution values. This allows SPF to access the solution values. + +Location: +__gov.nasa.jpf.symbc.string.translate__ + +Examples: +__gov.nasa.jpf.symbc.string.translate.TranslateToIGEN.java__ +__gov.nasa.jpf.symbc.string.translate.TranslateToABC.java__ +__edu.ucsb.cs.vlab.versions.Z3String3Processor.java__ + +### Identifying the solver, executing the translation isSat() method + +Third, the __SymbolicStringConstraintsGeneral__ class needs to be modified to include the identity and actions for the new solver. The solver identity is provided by a class property that is a unique string identifier for the solver (public static final String _identifier_). This identifier is used to specify the string solver in the .jpf file at runtime. The class instance variable solver is set to the correct identifier at the start of the _inner_isSatisfiable()_ method. + +Finally, the solver needs to be added to the section in the _inner_isSatisfiable()_ method that contains the set of conditionals that execute the correct actions for a given solver. Typically this action will be setting the _decisionProcedure_ variable to the output of the translation classes _isSat()_ method. + +Location: +__gov.nasa.jpf.symbc.string.SymbolicStringConstraintsGeneral__ + +### Alternative to JNI or .jar files ### + +If a solver does not have a .jar file exposing the required functionality, it may be possible to interface the solver if it has command line functionality that can return results that a translation class can interpret. For example, a translation class can create an instance of a binary executable and redirect the input and output of the instance in order to issue commands and receive results. + +### Setting solver properties in the .jpf file ### + +If a solver accommodates or requires special settings, these can be specified at runtime through the .jpf file if modifications are made to SPF. Properties specified in the .jpf file are exposed to classes in SPF through static public properties of the __SymbolicInstructionFactory__ class. The static public properties need to be declared in the class, and subsequently set in the constructor method. Properties in the .jpf file are discovered by interrogating the __Config__ object passed to the constructor. + +Once the __SymbolicInstructionFactory__ class has been modified to set the solver properties, they can be accessed within the solver translation code by importing the __SymbolicInstructionFactory__ class and accessing its public static properties. + +Location: +__gov.nasa.jpf.symbc.SymbolicInstructionFactory__ + +Example in .jpf file: +__symbolic.z3str3_aggressive_length_testing=true__ + +Accessible in translator class as: +__SymbolicInstructionFactory.z3str3_aggressive_length_testing__ diff --git a/z3str3-integration.md b/z3str3-integration.md new file mode 100644 index 00000000..9be70e35 --- /dev/null +++ b/z3str3-integration.md @@ -0,0 +1,82 @@ +z3str3-integration.md + +## z3str3 Support in SPF ## + +The string solver z3str3 is integrated into the SMT solver z3. The source for z3 is available at: +https://github.com/Z3Prover/Z3 + +### Building z3/z3str3 ### + +The build process for z3 includes the option for creating a Java .jar file that exposes the functionality of z3/z3str3 for use in Java programs such as SPF. Check the instructions for building with CMAKE at: +https://github.com/Z3Prover/z3/blob/master/README-CMake.md + +Once the build is complete, the .jar file and all corresponding library files must be placed in the bin directory in SPF: + +Files: | +------ | +com.microsoft.z3.jar +libz3.dll +libz3.dylib +libz3.so +libz3java.dll +libz3java.dylib +libz3java.so + +### Specifying z3str3 ### + +z3str3 can be specified in the .jpf file. Example: + + symbolic.string_dp=z3str3 + +### Setting z3str3 Options ### + +There are options specific to z3str3 that can be set in the .jpf file: + +__z3str3 String Option__ | Corresponding .jpf Property: +------------------------ | ---------------------------- +__str.aggressive_length_testing__ (bool) (default: false) | symbolic.z3str3_aggressive_length_testing +__str.aggressive_unroll_testing__ (bool) (default: true) | symbolic.z3str3_aggressive_unroll_testing +__str.aggressive_value_testing__ (bool) (default: false) | symbolic.z3str3_aggressive_value_testing +__str.fast_length_tester_cache__ (bool) (default: false) | symbolic.z3str3_fast_length_tester_cache +__str.fast_value_tester_cache__ (bool) (default: true) | symbolic.z3str3_fast_value_tester_cache +__str.fixed_length_naive_cex__ (bool) (default: true) | symbolic.z3str3_fixed_length_naive_cex +__str.fixed_length_refinement__ (bool) (default: false) | symbolic.z3str3_fixed_length_refinement +__str.string_constant_cache__ (bool) (default: true) | symbolic.z3str3_string_constant_cache +__str.strong_arrangements__ (bool) (default: true) | symbolic.z3str3_strong_arrangements + + +For example, to set str.string_constant_cache to _false_, the following entry would be made in the .jpf file: + + symbolic.z3str3_string_constant_cache=false + +Specific information about these options can be found through the z3 executable parameters option: + + z3 -p + +### Limitations of z3str3 in SPF ### + +z3str3 is compliant with the SMT-LIB standard located at: +http://smtlib.cs.uiowa.edu/ + +The input language of z3str3 is limited to SMT-LIB constructs, and does not directly implement Java string operations one-for-one. The input language specification can be found at: +https://zyh1121.github.io/z3str3Docs/inputLanguage.html#input-language-summary + +### Supported String Operations ### + +Due to the limits of the input language, z3str3 does not support all Java string operations. The following table presents those string operations available in z3str3. + +Supported Operations: | +--------------------- | +concat(String str) | +startsWith(String prefix) | +endsWith(String suffix) | +charAt(int index) | +length() | +replace(char oldChar, char newChar) | +replace(CharSequence target, CharSequence replacement) | +substring(int beginIndex, int endIndex) | +substring(int beginIndex) | +contains(CharSequence s) | +indexOf(String str) | +indexOf(String str, int fromIndex) | +equals(Object anObject) |