diff --git a/regression/cbmc-java/Makefile b/regression/cbmc-java/Makefile index a1b44c5a948..dcdf752aea1 100644 --- a/regression/cbmc-java/Makefile +++ b/regression/cbmc-java/Makefile @@ -23,3 +23,16 @@ clean: find -name '*.out' -execdir $(RM) '{}' \; find -name '*.gb' -execdir $(RM) '{}' \; $(RM) tests.log + +%.class: %.java ../../src/org.cprover.jar + javac -g -cp ../../src/org.cprover.jar:. $< + +nondet_java_files := $(shell find . -name "Nondet*.java") +nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files)) + +.PHONY: nondet-class-files +nondet-class-files: $(nondet_class_files) + +.PHONY: clean-nondet-class-files +clean-nondet-class-files: + -rm $(nondet_class_files) diff --git a/regression/cbmc-java/NondetArray/NondetArray.class b/regression/cbmc-java/NondetArray/NondetArray.class new file mode 100644 index 00000000000..57858ac292f Binary files /dev/null and b/regression/cbmc-java/NondetArray/NondetArray.class differ diff --git a/regression/cbmc-java/NondetArray/NondetArray.java b/regression/cbmc-java/NondetArray/NondetArray.java new file mode 100644 index 00000000000..21dd4416b4e --- /dev/null +++ b/regression/cbmc-java/NondetArray/NondetArray.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetArray +{ + void main() + { + Object[] obj = CProver.nondetWithoutNull(); + assert obj != null; + } +} diff --git a/regression/cbmc-java/NondetArray/test.desc b/regression/cbmc-java/NondetArray/test.desc new file mode 100644 index 00000000000..63cf6d4cbc0 --- /dev/null +++ b/regression/cbmc-java/NondetArray/test.desc @@ -0,0 +1,6 @@ +CORE +NondetArray.class +--function NondetArray.main +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetArray2/NondetArray2.class b/regression/cbmc-java/NondetArray2/NondetArray2.class new file mode 100644 index 00000000000..0ab85c2bb1d Binary files /dev/null and b/regression/cbmc-java/NondetArray2/NondetArray2.class differ diff --git a/regression/cbmc-java/NondetArray2/NondetArray2.java b/regression/cbmc-java/NondetArray2/NondetArray2.java new file mode 100644 index 00000000000..2f9bcedd797 --- /dev/null +++ b/regression/cbmc-java/NondetArray2/NondetArray2.java @@ -0,0 +1,15 @@ +import org.cprover.CProver; + +class NondetArray2 +{ + void main() + { + Integer[] ints = CProver.nondetWithoutNull(); + + int num = 0; + for (Integer i : ints) { + num *= i.intValue(); + } + assert num == 0; + } +} diff --git a/regression/cbmc-java/NondetArray2/test.desc b/regression/cbmc-java/NondetArray2/test.desc new file mode 100644 index 00000000000..5e84e0dbf7c --- /dev/null +++ b/regression/cbmc-java/NondetArray2/test.desc @@ -0,0 +1,6 @@ +CORE +NondetArray2.class +--function NondetArray2.main --unwind 5 +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetArray3/NondetArray3.class b/regression/cbmc-java/NondetArray3/NondetArray3.class new file mode 100644 index 00000000000..e07d736d747 Binary files /dev/null and b/regression/cbmc-java/NondetArray3/NondetArray3.class differ diff --git a/regression/cbmc-java/NondetArray3/NondetArray3.java b/regression/cbmc-java/NondetArray3/NondetArray3.java new file mode 100644 index 00000000000..c061aa693f2 --- /dev/null +++ b/regression/cbmc-java/NondetArray3/NondetArray3.java @@ -0,0 +1,16 @@ +import org.cprover.CProver; + +class NondetArray3 +{ + void main() + { + Integer[] ints = CProver.nondetWithoutNull(); + assert ints != null; + + int num = 0; + for (Integer i : ints) { + num *= i.intValue(); + } + assert num == 0; + } +} diff --git a/regression/cbmc-java/NondetArray3/test.desc b/regression/cbmc-java/NondetArray3/test.desc new file mode 100644 index 00000000000..a0f68ce5a41 --- /dev/null +++ b/regression/cbmc-java/NondetArray3/test.desc @@ -0,0 +1,6 @@ +CORE +NondetArray3.class +--function NondetArray3.main --unwind 5 +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetArray4/NondetArray4.class b/regression/cbmc-java/NondetArray4/NondetArray4.class new file mode 100644 index 00000000000..dbe5532ccfb Binary files /dev/null and b/regression/cbmc-java/NondetArray4/NondetArray4.class differ diff --git a/regression/cbmc-java/NondetArray4/NondetArray4.java b/regression/cbmc-java/NondetArray4/NondetArray4.java new file mode 100644 index 00000000000..4b4e15aaad7 --- /dev/null +++ b/regression/cbmc-java/NondetArray4/NondetArray4.java @@ -0,0 +1,14 @@ +import org.cprover.CProver; + +class NondetArray4 +{ + void main() + { + int a = 1; + int b = 2; + int c = 3; + + Integer[] ints = CProver.nondetWithoutNull(); + assert ints != null; + } +} diff --git a/regression/cbmc-java/NondetArray4/test.desc b/regression/cbmc-java/NondetArray4/test.desc new file mode 100644 index 00000000000..fd419bab2d4 --- /dev/null +++ b/regression/cbmc-java/NondetArray4/test.desc @@ -0,0 +1,6 @@ +CORE +NondetArray4.class +--function NondetArray4.main +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetAssume1/NondetAssume1.class b/regression/cbmc-java/NondetAssume1/NondetAssume1.class new file mode 100644 index 00000000000..bcdca197547 Binary files /dev/null and b/regression/cbmc-java/NondetAssume1/NondetAssume1.class differ diff --git a/regression/cbmc-java/NondetAssume1/NondetAssume1.java b/regression/cbmc-java/NondetAssume1/NondetAssume1.java new file mode 100644 index 00000000000..9177bcece6b --- /dev/null +++ b/regression/cbmc-java/NondetAssume1/NondetAssume1.java @@ -0,0 +1,11 @@ +import org.cprover.CProver; + +class NondetAssume1 +{ + void main() + { + int x = CProver.nondetInt(); + CProver.assume(x == 1); + assert x == 1; + } +} diff --git a/regression/cbmc-java/NondetAssume1/test.desc b/regression/cbmc-java/NondetAssume1/test.desc new file mode 100644 index 00000000000..bbff9abb9f2 --- /dev/null +++ b/regression/cbmc-java/NondetAssume1/test.desc @@ -0,0 +1,6 @@ +CORE +NondetAssume1.class +--function NondetAssume1.main +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetAssume2/A.class b/regression/cbmc-java/NondetAssume2/A.class new file mode 100644 index 00000000000..66636e271af Binary files /dev/null and b/regression/cbmc-java/NondetAssume2/A.class differ diff --git a/regression/cbmc-java/NondetAssume2/B.class b/regression/cbmc-java/NondetAssume2/B.class new file mode 100644 index 00000000000..9978b0f14de Binary files /dev/null and b/regression/cbmc-java/NondetAssume2/B.class differ diff --git a/regression/cbmc-java/NondetAssume2/C.class b/regression/cbmc-java/NondetAssume2/C.class new file mode 100644 index 00000000000..bbf6b9b7eae Binary files /dev/null and b/regression/cbmc-java/NondetAssume2/C.class differ diff --git a/regression/cbmc-java/NondetAssume2/NondetAssume2.class b/regression/cbmc-java/NondetAssume2/NondetAssume2.class new file mode 100644 index 00000000000..45efb7811e2 Binary files /dev/null and b/regression/cbmc-java/NondetAssume2/NondetAssume2.class differ diff --git a/regression/cbmc-java/NondetAssume2/NondetAssume2.java b/regression/cbmc-java/NondetAssume2/NondetAssume2.java new file mode 100644 index 00000000000..1f8f74a3464 --- /dev/null +++ b/regression/cbmc-java/NondetAssume2/NondetAssume2.java @@ -0,0 +1,17 @@ +import org.cprover.CProver; + +class A { int x; } + +class B { A a; } + +class C { B b; } + +class NondetAssume2 +{ + void main() + { + C c = CProver.nondetWithNull(); + CProver.assume(c != null); + assert c != null; + } +} diff --git a/regression/cbmc-java/NondetAssume2/test.desc b/regression/cbmc-java/NondetAssume2/test.desc new file mode 100644 index 00000000000..19abaa63e8a --- /dev/null +++ b/regression/cbmc-java/NondetAssume2/test.desc @@ -0,0 +1,6 @@ +CORE +NondetAssume2.class +--function NondetAssume2.main +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetBoolean/NondetBoolean.class b/regression/cbmc-java/NondetBoolean/NondetBoolean.class new file mode 100644 index 00000000000..0b4ed3f7915 Binary files /dev/null and b/regression/cbmc-java/NondetBoolean/NondetBoolean.class differ diff --git a/regression/cbmc-java/NondetBoolean/NondetBoolean.java b/regression/cbmc-java/NondetBoolean/NondetBoolean.java new file mode 100644 index 00000000000..4b05ae056ea --- /dev/null +++ b/regression/cbmc-java/NondetBoolean/NondetBoolean.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetBoolean +{ + static void main() + { + boolean x = CProver.nondetBoolean(); + assert x == false; + } +} diff --git a/regression/cbmc-java/NondetBoolean/test.desc b/regression/cbmc-java/NondetBoolean/test.desc new file mode 100644 index 00000000000..c0bfc954449 --- /dev/null +++ b/regression/cbmc-java/NondetBoolean/test.desc @@ -0,0 +1,6 @@ +CORE +NondetBoolean.class +--function NondetBoolean.main +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetByte/NondetByte.class b/regression/cbmc-java/NondetByte/NondetByte.class new file mode 100644 index 00000000000..d066e46704c Binary files /dev/null and b/regression/cbmc-java/NondetByte/NondetByte.class differ diff --git a/regression/cbmc-java/NondetByte/NondetByte.java b/regression/cbmc-java/NondetByte/NondetByte.java new file mode 100644 index 00000000000..36b7b209014 --- /dev/null +++ b/regression/cbmc-java/NondetByte/NondetByte.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetByte +{ + static void main() + { + byte x = CProver.nondetByte(); + assert x == 0; + } +} diff --git a/regression/cbmc-java/NondetByte/test.desc b/regression/cbmc-java/NondetByte/test.desc new file mode 100644 index 00000000000..d05a462245a --- /dev/null +++ b/regression/cbmc-java/NondetByte/test.desc @@ -0,0 +1,6 @@ +CORE +NondetByte.class +--function NondetByte.main +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetCastToObject/NondetCastToObject.class b/regression/cbmc-java/NondetCastToObject/NondetCastToObject.class new file mode 100644 index 00000000000..65e622d872c Binary files /dev/null and b/regression/cbmc-java/NondetCastToObject/NondetCastToObject.class differ diff --git a/regression/cbmc-java/NondetCastToObject/NondetCastToObject.java b/regression/cbmc-java/NondetCastToObject/NondetCastToObject.java new file mode 100644 index 00000000000..133df3f9f4e --- /dev/null +++ b/regression/cbmc-java/NondetCastToObject/NondetCastToObject.java @@ -0,0 +1,11 @@ +import org.cprover.CProver; + +class NondetCastToObject +{ + void main() + { + Object o = CProver.nondetWithNull(); + CProver.assume(o != null); + assert o != null; + } +} diff --git a/regression/cbmc-java/NondetCastToObject/test.desc b/regression/cbmc-java/NondetCastToObject/test.desc new file mode 100644 index 00000000000..5d3b98bb583 --- /dev/null +++ b/regression/cbmc-java/NondetCastToObject/test.desc @@ -0,0 +1,6 @@ +CORE +NondetCastToObject.class +--function NondetCastToObject.main +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetChar/NondetChar.class b/regression/cbmc-java/NondetChar/NondetChar.class new file mode 100644 index 00000000000..4d05d0b75dd Binary files /dev/null and b/regression/cbmc-java/NondetChar/NondetChar.class differ diff --git a/regression/cbmc-java/NondetChar/NondetChar.java b/regression/cbmc-java/NondetChar/NondetChar.java new file mode 100644 index 00000000000..f9570d8a5d2 --- /dev/null +++ b/regression/cbmc-java/NondetChar/NondetChar.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetChar +{ + static void main() + { + char x = CProver.nondetChar(); + assert x == '\0'; + } +} diff --git a/regression/cbmc-java/NondetChar/test.desc b/regression/cbmc-java/NondetChar/test.desc new file mode 100644 index 00000000000..96ecd2f6735 --- /dev/null +++ b/regression/cbmc-java/NondetChar/test.desc @@ -0,0 +1,6 @@ +CORE +NondetChar.class +--function NondetChar.main +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetDirectFromMethod/A.class b/regression/cbmc-java/NondetDirectFromMethod/A.class new file mode 100644 index 00000000000..6d3758b230a Binary files /dev/null and b/regression/cbmc-java/NondetDirectFromMethod/A.class differ diff --git a/regression/cbmc-java/NondetDirectFromMethod/NondetDirectFromMethod.class b/regression/cbmc-java/NondetDirectFromMethod/NondetDirectFromMethod.class new file mode 100644 index 00000000000..6dafdc80b07 Binary files /dev/null and b/regression/cbmc-java/NondetDirectFromMethod/NondetDirectFromMethod.class differ diff --git a/regression/cbmc-java/NondetDirectFromMethod/NondetDirectFromMethod.java b/regression/cbmc-java/NondetDirectFromMethod/NondetDirectFromMethod.java new file mode 100644 index 00000000000..dbd7960c880 --- /dev/null +++ b/regression/cbmc-java/NondetDirectFromMethod/NondetDirectFromMethod.java @@ -0,0 +1,19 @@ +import org.cprover.CProver; + +class A +{ + int a; +} + +class NondetDirectFromMethod +{ + A methodReturningA() + { + return CProver.nondetWithoutNull(); + } + + void main() + { + assert methodReturningA() != null; + } +} diff --git a/regression/cbmc-java/NondetDirectFromMethod/test.desc b/regression/cbmc-java/NondetDirectFromMethod/test.desc new file mode 100644 index 00000000000..10989391e46 --- /dev/null +++ b/regression/cbmc-java/NondetDirectFromMethod/test.desc @@ -0,0 +1,6 @@ +CORE +NondetDirectFromMethod.class +--function NondetDirectFromMethod.main +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetDouble/NondetDouble.class b/regression/cbmc-java/NondetDouble/NondetDouble.class new file mode 100644 index 00000000000..5d298bcfa63 Binary files /dev/null and b/regression/cbmc-java/NondetDouble/NondetDouble.class differ diff --git a/regression/cbmc-java/NondetDouble/NondetDouble.java b/regression/cbmc-java/NondetDouble/NondetDouble.java new file mode 100644 index 00000000000..451fcf4db7e --- /dev/null +++ b/regression/cbmc-java/NondetDouble/NondetDouble.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetDouble +{ + static void main() + { + double x = CProver.nondetDouble(); + assert x == 0; + } +} diff --git a/regression/cbmc-java/NondetDouble/test.desc b/regression/cbmc-java/NondetDouble/test.desc new file mode 100644 index 00000000000..631edbe5024 --- /dev/null +++ b/regression/cbmc-java/NondetDouble/test.desc @@ -0,0 +1,6 @@ +CORE +NondetDouble.class +--function NondetDouble.main +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetFloat/NondetFloat.class b/regression/cbmc-java/NondetFloat/NondetFloat.class new file mode 100644 index 00000000000..9b26f72c773 Binary files /dev/null and b/regression/cbmc-java/NondetFloat/NondetFloat.class differ diff --git a/regression/cbmc-java/NondetFloat/NondetFloat.java b/regression/cbmc-java/NondetFloat/NondetFloat.java new file mode 100644 index 00000000000..e461162d0d5 --- /dev/null +++ b/regression/cbmc-java/NondetFloat/NondetFloat.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetFloat +{ + static void main() + { + float x = CProver.nondetFloat(); + assert x == 0; + } +} diff --git a/regression/cbmc-java/NondetFloat/test.desc b/regression/cbmc-java/NondetFloat/test.desc new file mode 100644 index 00000000000..27bc33761b6 --- /dev/null +++ b/regression/cbmc-java/NondetFloat/test.desc @@ -0,0 +1,6 @@ +CORE +NondetFloat.class +--function NondetFloat.main +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetGenericArray/A.class b/regression/cbmc-java/NondetGenericArray/A.class new file mode 100644 index 00000000000..1323ce430e5 Binary files /dev/null and b/regression/cbmc-java/NondetGenericArray/A.class differ diff --git a/regression/cbmc-java/NondetGenericArray/B.class b/regression/cbmc-java/NondetGenericArray/B.class new file mode 100644 index 00000000000..730946d3d80 Binary files /dev/null and b/regression/cbmc-java/NondetGenericArray/B.class differ diff --git a/regression/cbmc-java/NondetGenericArray/C.class b/regression/cbmc-java/NondetGenericArray/C.class new file mode 100644 index 00000000000..27903564a63 Binary files /dev/null and b/regression/cbmc-java/NondetGenericArray/C.class differ diff --git a/regression/cbmc-java/NondetGenericArray/NondetGenericArray.class b/regression/cbmc-java/NondetGenericArray/NondetGenericArray.class new file mode 100644 index 00000000000..76c6f43ab08 Binary files /dev/null and b/regression/cbmc-java/NondetGenericArray/NondetGenericArray.class differ diff --git a/regression/cbmc-java/NondetGenericArray/NondetGenericArray.java b/regression/cbmc-java/NondetGenericArray/NondetGenericArray.java new file mode 100644 index 00000000000..1c7d62a5b73 --- /dev/null +++ b/regression/cbmc-java/NondetGenericArray/NondetGenericArray.java @@ -0,0 +1,30 @@ +import org.cprover.CProver; + +class A +{ + int[] ints = new int[10]; +} + +class B +{ + A a; +} + +class C +{ + B b; +} + +class NondetGenericArray +{ + static void main() + { + C c = CProver.nondetWithNull(); + CProver.assume(c != null); + CProver.assume(c.b != null); + CProver.assume(c.b.a != null); + CProver.assume(c.b.a.ints != null); + assert c.b.a != null; + assert c.b.a.ints != null; + } +} diff --git a/regression/cbmc-java/NondetGenericArray/test.desc b/regression/cbmc-java/NondetGenericArray/test.desc new file mode 100644 index 00000000000..e9ace0bad35 --- /dev/null +++ b/regression/cbmc-java/NondetGenericArray/test.desc @@ -0,0 +1,6 @@ +CORE +NondetGenericArray.class +--function NondetGenericArray.main +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetGenericRecursive/A.class b/regression/cbmc-java/NondetGenericRecursive/A.class new file mode 100644 index 00000000000..005c8063d51 Binary files /dev/null and b/regression/cbmc-java/NondetGenericRecursive/A.class differ diff --git a/regression/cbmc-java/NondetGenericRecursive/B.class b/regression/cbmc-java/NondetGenericRecursive/B.class new file mode 100644 index 00000000000..8a18024f50b Binary files /dev/null and b/regression/cbmc-java/NondetGenericRecursive/B.class differ diff --git a/regression/cbmc-java/NondetGenericRecursive/C.class b/regression/cbmc-java/NondetGenericRecursive/C.class new file mode 100644 index 00000000000..acc2b11ef63 Binary files /dev/null and b/regression/cbmc-java/NondetGenericRecursive/C.class differ diff --git a/regression/cbmc-java/NondetGenericRecursive/NondetGenericRecursive.class b/regression/cbmc-java/NondetGenericRecursive/NondetGenericRecursive.class new file mode 100644 index 00000000000..c0040fb2f5f Binary files /dev/null and b/regression/cbmc-java/NondetGenericRecursive/NondetGenericRecursive.class differ diff --git a/regression/cbmc-java/NondetGenericRecursive/NondetGenericRecursive.java b/regression/cbmc-java/NondetGenericRecursive/NondetGenericRecursive.java new file mode 100644 index 00000000000..33d2b8d68bc --- /dev/null +++ b/regression/cbmc-java/NondetGenericRecursive/NondetGenericRecursive.java @@ -0,0 +1,24 @@ +import org.cprover.CProver; + +class A +{ +} + +class B +{ + A a; +} + +class C +{ + B b; +} + +class NondetGenericRecursive +{ + static void main() + { + C c = CProver.nondetWithNull(); + assert c == null; + } +} diff --git a/regression/cbmc-java/NondetGenericRecursive/test.desc b/regression/cbmc-java/NondetGenericRecursive/test.desc new file mode 100644 index 00000000000..34af1b2e6c1 --- /dev/null +++ b/regression/cbmc-java/NondetGenericRecursive/test.desc @@ -0,0 +1,6 @@ +CORE +NondetGenericRecursive.class +--function NondetGenericRecursive.main +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetGenericRecursive2/A.class b/regression/cbmc-java/NondetGenericRecursive2/A.class new file mode 100644 index 00000000000..5628564f73d Binary files /dev/null and b/regression/cbmc-java/NondetGenericRecursive2/A.class differ diff --git a/regression/cbmc-java/NondetGenericRecursive2/B.class b/regression/cbmc-java/NondetGenericRecursive2/B.class new file mode 100644 index 00000000000..606067dcdb8 Binary files /dev/null and b/regression/cbmc-java/NondetGenericRecursive2/B.class differ diff --git a/regression/cbmc-java/NondetGenericRecursive2/C.class b/regression/cbmc-java/NondetGenericRecursive2/C.class new file mode 100644 index 00000000000..fe32a4afb54 Binary files /dev/null and b/regression/cbmc-java/NondetGenericRecursive2/C.class differ diff --git a/regression/cbmc-java/NondetGenericRecursive2/NondetGenericRecursive2.class b/regression/cbmc-java/NondetGenericRecursive2/NondetGenericRecursive2.class new file mode 100644 index 00000000000..ed328ac8e04 Binary files /dev/null and b/regression/cbmc-java/NondetGenericRecursive2/NondetGenericRecursive2.class differ diff --git a/regression/cbmc-java/NondetGenericRecursive2/NondetGenericRecursive2.java b/regression/cbmc-java/NondetGenericRecursive2/NondetGenericRecursive2.java new file mode 100644 index 00000000000..de5ef46c4cb --- /dev/null +++ b/regression/cbmc-java/NondetGenericRecursive2/NondetGenericRecursive2.java @@ -0,0 +1,27 @@ +import org.cprover.CProver; + +class A +{ +} + +class B +{ + A a; +} + +class C +{ + B b; +} + +class NondetGenericRecursive2 +{ + static void main() + { + C c = CProver.nondetWithNull(); + CProver.assume(c != null); + CProver.assume(c.b != null); + CProver.assume(c.b.a != null); + assert c.b.a != null; + } +} diff --git a/regression/cbmc-java/NondetGenericRecursive2/test.desc b/regression/cbmc-java/NondetGenericRecursive2/test.desc new file mode 100644 index 00000000000..52558889313 --- /dev/null +++ b/regression/cbmc-java/NondetGenericRecursive2/test.desc @@ -0,0 +1,6 @@ +CORE +NondetGenericRecursive2.class +--function NondetGenericRecursive2.main +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetGenericWithNull/B.class b/regression/cbmc-java/NondetGenericWithNull/B.class new file mode 100644 index 00000000000..80c9824e519 Binary files /dev/null and b/regression/cbmc-java/NondetGenericWithNull/B.class differ diff --git a/regression/cbmc-java/NondetGenericWithNull/NondetGenericWithNull.class b/regression/cbmc-java/NondetGenericWithNull/NondetGenericWithNull.class new file mode 100644 index 00000000000..0b52a47bd0a Binary files /dev/null and b/regression/cbmc-java/NondetGenericWithNull/NondetGenericWithNull.class differ diff --git a/regression/cbmc-java/NondetGenericWithNull/NondetGenericWithNull.java b/regression/cbmc-java/NondetGenericWithNull/NondetGenericWithNull.java new file mode 100644 index 00000000000..9c89b92b31f --- /dev/null +++ b/regression/cbmc-java/NondetGenericWithNull/NondetGenericWithNull.java @@ -0,0 +1,13 @@ +import org.cprover.CProver; + +class B { int a; } + +class NondetGenericWithNull +{ + static void main() + { + B b = CProver.nondetWithNull(); + assert b != null; + assert b.a != 0; + } +} diff --git a/regression/cbmc-java/NondetGenericWithNull/test.desc b/regression/cbmc-java/NondetGenericWithNull/test.desc new file mode 100644 index 00000000000..c2feb23068d --- /dev/null +++ b/regression/cbmc-java/NondetGenericWithNull/test.desc @@ -0,0 +1,6 @@ +CORE +NondetGenericWithNull.class +--function NondetGenericWithNull.main +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetGenericWithoutNull/B.class b/regression/cbmc-java/NondetGenericWithoutNull/B.class new file mode 100644 index 00000000000..c7e4fbbf832 Binary files /dev/null and b/regression/cbmc-java/NondetGenericWithoutNull/B.class differ diff --git a/regression/cbmc-java/NondetGenericWithoutNull/NondetGenericWithoutNull.class b/regression/cbmc-java/NondetGenericWithoutNull/NondetGenericWithoutNull.class new file mode 100644 index 00000000000..c369eae01fc Binary files /dev/null and b/regression/cbmc-java/NondetGenericWithoutNull/NondetGenericWithoutNull.class differ diff --git a/regression/cbmc-java/NondetGenericWithoutNull/NondetGenericWithoutNull.java b/regression/cbmc-java/NondetGenericWithoutNull/NondetGenericWithoutNull.java new file mode 100644 index 00000000000..6a3ef4ad6f3 --- /dev/null +++ b/regression/cbmc-java/NondetGenericWithoutNull/NondetGenericWithoutNull.java @@ -0,0 +1,12 @@ +import org.cprover.CProver; + +class B { int a; } + +class NondetGenericWithoutNull +{ + static void main() + { + B b = CProver.nondetWithoutNull(); + assert b != null; + } +} diff --git a/regression/cbmc-java/NondetGenericWithoutNull/test.desc b/regression/cbmc-java/NondetGenericWithoutNull/test.desc new file mode 100644 index 00000000000..e9ada8b935c --- /dev/null +++ b/regression/cbmc-java/NondetGenericWithoutNull/test.desc @@ -0,0 +1,6 @@ +CORE +NondetGenericWithoutNull.class +--function NondetGenericWithoutNull.main +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetInt/NondetInt.class b/regression/cbmc-java/NondetInt/NondetInt.class new file mode 100644 index 00000000000..0af2adcb608 Binary files /dev/null and b/regression/cbmc-java/NondetInt/NondetInt.class differ diff --git a/regression/cbmc-java/NondetInt/NondetInt.java b/regression/cbmc-java/NondetInt/NondetInt.java new file mode 100644 index 00000000000..f2ae6890fb0 --- /dev/null +++ b/regression/cbmc-java/NondetInt/NondetInt.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetInt +{ + static void main() + { + int x = CProver.nondetInt(); + assert x == 0; + } +} diff --git a/regression/cbmc-java/NondetInt/test.desc b/regression/cbmc-java/NondetInt/test.desc new file mode 100644 index 00000000000..324d69b8c91 --- /dev/null +++ b/regression/cbmc-java/NondetInt/test.desc @@ -0,0 +1,6 @@ +CORE +NondetInt.class +--function NondetInt.main +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetLong/NondetLong.class b/regression/cbmc-java/NondetLong/NondetLong.class new file mode 100644 index 00000000000..27a693dee6e Binary files /dev/null and b/regression/cbmc-java/NondetLong/NondetLong.class differ diff --git a/regression/cbmc-java/NondetLong/NondetLong.java b/regression/cbmc-java/NondetLong/NondetLong.java new file mode 100644 index 00000000000..57707eb07cb --- /dev/null +++ b/regression/cbmc-java/NondetLong/NondetLong.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetLong +{ + static void main() + { + long x = CProver.nondetLong(); + assert x == 0; + } +} diff --git a/regression/cbmc-java/NondetLong/test.desc b/regression/cbmc-java/NondetLong/test.desc new file mode 100644 index 00000000000..f92db994e00 --- /dev/null +++ b/regression/cbmc-java/NondetLong/test.desc @@ -0,0 +1,6 @@ +CORE +NondetLong.class +--function NondetLong.main +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetShort/NondetShort.class b/regression/cbmc-java/NondetShort/NondetShort.class new file mode 100644 index 00000000000..32e0868de3e Binary files /dev/null and b/regression/cbmc-java/NondetShort/NondetShort.class differ diff --git a/regression/cbmc-java/NondetShort/NondetShort.java b/regression/cbmc-java/NondetShort/NondetShort.java new file mode 100644 index 00000000000..941ee23ffd2 --- /dev/null +++ b/regression/cbmc-java/NondetShort/NondetShort.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetShort +{ + static void main() + { + short x = CProver.nondetShort(); + assert x == 0; + } +} diff --git a/regression/cbmc-java/NondetShort/test.desc b/regression/cbmc-java/NondetShort/test.desc new file mode 100644 index 00000000000..24ac39c540b --- /dev/null +++ b/regression/cbmc-java/NondetShort/test.desc @@ -0,0 +1,6 @@ +CORE +NondetShort.class +--function NondetShort.main +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 1619143ce6c..2c5806ed868 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -41,6 +41,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include +#include #include #include @@ -53,6 +55,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "java_bytecode/java_bytecode_language.h" + #include "cbmc_solvers.h" #include "cbmc_parse_options.h" #include "bmc.h" @@ -921,6 +925,20 @@ bool cbmc_parse_optionst::process_goto_program( remove_complex(symbol_table, goto_functions); rewrite_union(goto_functions, ns); + // Similar removal of java nondet statements: + // TODO Should really get this from java_bytecode_language somehow, but we + // don't have an instance of that here. + const auto max_nondet_array_length= + cmdline.isset("java-max-input-array-length") + ? std::stoi(cmdline.get_value("java-max-input-array-length")) + : MAX_NONDET_ARRAY_LENGTH_DEFAULT; + replace_java_nondet(goto_functions); + convert_nondet( + goto_functions, + symbol_table, + ui_message_handler, + max_nondet_array_length); + // add generic checks status() << "Generic Property Instrumentation" << eom; goto_check(ns, options, goto_functions); diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 6b2832e3481..e873310b0c7 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -25,6 +25,8 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \ remove_const_function_pointers.cpp \ system_library_symbols.cpp \ string_refine_preprocess.cpp \ + replace_java_nondet.cpp \ + convert_nondet.cpp \ # Empty last line INCLUDES= -I .. diff --git a/src/goto-programs/convert_nondet.cpp b/src/goto-programs/convert_nondet.cpp new file mode 100644 index 00000000000..148323c1d67 --- /dev/null +++ b/src/goto-programs/convert_nondet.cpp @@ -0,0 +1,164 @@ +/*******************************************************************\ + +Module: Convert side_effect_expr_nondett expressions + +Author: Reuben Thomas, reuben.thomas@diffblue.com + +\*******************************************************************/ + +#include "goto-programs/convert_nondet.h" +#include "goto-programs/goto_convert.h" +#include "goto-programs/goto_model.h" + +#include "java_bytecode/java_object_factory.h" // gen_nondet_init + +#include "util/irep_ids.h" + +/*******************************************************************\ + +Function: insert_nondet_init_code + + Inputs: + goto_program: The goto program to modify. + target: One of the steps in that goto program. + symbol_table: The global symbol table. + message_handler: Handles logging. + max_nondet_array_length: Maximum size of new nondet arrays. + + Outputs: The next instruction to process with this function. + + Purpose: Checks an instruction to see whether it contains an assignment + from side_effect_expr_nondet. If so, replaces the instruction + with a range of instructions to properly nondet-initialize + the lhs. + +\*******************************************************************/ + +static goto_programt::const_targett insert_nondet_init_code( + goto_programt &goto_program, + const goto_programt::const_targett &target, + symbol_tablet &symbol_table, + message_handlert &message_handler, + size_t max_nondet_array_length) +{ + // Return if the instruction isn't an assignment + const auto next_instr=std::next(target); + if(!target->is_assign()) + { + return next_instr; + } + + // Return if the rhs of the assignment isn't a side effect expression + const auto &assign=to_code_assign(target->code); + if(assign.rhs().id()!=ID_side_effect) + { + return next_instr; + } + + // Return if the rhs isn't nondet + const auto &side_effect=to_side_effect_expr(assign.rhs()); + if(side_effect.get_statement()!=ID_nondet) + { + return next_instr; + } + + const auto lhs=assign.lhs(); + // If the lhs type doesn't have a subtype then I guess it's primitive and + // we want to bail out now + if(!lhs.type().has_subtype()) + { + return next_instr; + } + + // Although, if the type is a ptr-to-void then we also want to bail + if(lhs.type().subtype().id()==ID_empty) + { + return next_instr; + } + + // Check whether the nondet object may be null + const auto nullable=to_side_effect_expr_nondet(side_effect).get_nullable(); + // Get the symbol to nondet-init + const auto source_loc=target->source_location; + + // Erase the nondet assignment + const auto after_erased=goto_program.instructions.erase(target); + + // Generate nondet init code + code_blockt init_code; + gen_nondet_init( + lhs, + init_code, + symbol_table, + source_loc, + false, + true, + !nullable, + message_handler, + max_nondet_array_length); + + // Convert this code into goto instructions + goto_programt new_instructions; + goto_convert(init_code, symbol_table, new_instructions, message_handler); + + // Insert the new instructions into the instruction list + goto_program.destructive_insert(after_erased, new_instructions); + goto_program.update(); + + return after_erased; +} + +/*******************************************************************\ + +Function: convert_nondet + + Inputs: + goto_program: The goto program to modify. + symbol_table: The global symbol table. + message_handler: Handles logging. + max_nondet_array_length: Maximum size of new nondet arrays. + + Purpose: For each instruction in the goto program, checks if it is + an assignment from nondet and replaces it with the appropriate + composite initialization code if so. + +\*******************************************************************/ + +static void convert_nondet( + goto_programt &goto_program, + symbol_tablet &symbol_table, + message_handlert &message_handler, + size_t max_nondet_array_length) +{ + for(auto instruction_iterator=goto_program.instructions.cbegin(), + end=goto_program.instructions.cend(); + instruction_iterator!=end;) + { + instruction_iterator=insert_nondet_init_code( + goto_program, + instruction_iterator, + symbol_table, + message_handler, + max_nondet_array_length); + } +} + + + +void convert_nondet( + goto_functionst &goto_functions, + symbol_tablet &symbol_table, + message_handlert &message_handler, + size_t max_nondet_array_length) +{ + for(auto &goto_program : goto_functions.function_map) + { + convert_nondet( + goto_program.second.body, + symbol_table, + message_handler, + max_nondet_array_length); + } + + goto_functions.compute_location_numbers(); +} diff --git a/src/goto-programs/convert_nondet.h b/src/goto-programs/convert_nondet.h new file mode 100644 index 00000000000..919d977a94e --- /dev/null +++ b/src/goto-programs/convert_nondet.h @@ -0,0 +1,39 @@ +/*******************************************************************\ + +Module: Convert side_effect_expr_nondett expressions + +Author: Reuben Thomas, reuben.thomas@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_PROGRAMS_CONVERT_NONDET_H +#define CPROVER_GOTO_PROGRAMS_CONVERT_NONDET_H + +#include // size_t + +class goto_functionst; +class symbol_tablet; +class message_handlert; + +/*******************************************************************\ + +Function: convert_nondet + + Inputs: + goto_functions: The set of goto programs to modify. + symbol_table: The symbol table to query/update. + message_handler: For error logging. + max_nondet_array_length: The maximum length of any new arrays. + + Purpose: Replace calls to nondet library functions with an internal + nondet representation. + +\*******************************************************************/ + +void convert_nondet( + goto_functionst &goto_functions, + symbol_tablet &symbol_table, + message_handlert &message_handler, + size_t max_nondet_array_length); + +#endif diff --git a/src/goto-programs/replace_java_nondet.cpp b/src/goto-programs/replace_java_nondet.cpp new file mode 100644 index 00000000000..b78a0819cac --- /dev/null +++ b/src/goto-programs/replace_java_nondet.cpp @@ -0,0 +1,319 @@ +/*******************************************************************\ + +Module: Replace Java Nondet expressions + +Author: Reuben Thomas, reuben.thomas@diffblue.com + +\*******************************************************************/ + +#include "goto-programs/replace_java_nondet.h" +#include "goto-programs/goto_convert.h" +#include "goto-programs/goto_model.h" + +#include "util/irep_ids.h" + +#include +#include + +/*******************************************************************\ + + Class: nondet_instruction_infot + + Purpose: Holds information about any discovered nondet methods, + with extreme type-safety. + +\*******************************************************************/ + +class nondet_instruction_infot final +{ +public: + enum class is_nondett:bool { FALSE, TRUE }; + enum class is_nullablet:bool { FALSE, TRUE }; + + nondet_instruction_infot(): + is_nondet(is_nondett::FALSE), + is_nullable(is_nullablet::FALSE) + { + } + + explicit nondet_instruction_infot(is_nullablet is_nullable): + is_nondet(is_nondett::TRUE), + is_nullable(is_nullable) + { + } + + is_nondett get_instruction_type() const { return is_nondet; } + is_nullablet get_nullable_type() const { return is_nullable; } + +private: + is_nondett is_nondet; + is_nullablet is_nullable; +}; + +/*******************************************************************\ + +Function: is_nondet_returning_object + + Inputs: + function_call: The function call declaration to check. + + Outputs: A structure detailing whether the function call appears to + be one of our nondet library methods, and if so, whether + or not it allows null results. + + Purpose: Checks whether the function call is one of our nondet + library functions. + +\*******************************************************************/ + +static nondet_instruction_infot is_nondet_returning_object( + const code_function_callt &function_call) +{ + const auto &function_symbol=to_symbol_expr(function_call.function()); + const auto function_name=id2string(function_symbol.get_identifier()); + const std::regex reg( + R"(.*org\.cprover\.CProver\.nondet)" + R"((?:Boolean|Byte|Char|Short|Int|Long|Float|Double|With(out)?Null.*))"); + std::smatch match_results; + if(!std::regex_match(function_name, match_results, reg)) + { + return nondet_instruction_infot(); + } + + return nondet_instruction_infot( + nondet_instruction_infot::is_nullablet(!match_results[1].matched)); +} + +/*******************************************************************\ + +Function: get_nondet_instruction_info + + Inputs: + instr: A goto-program instruction to check. + + Outputs: A structure detailing the properties of the nondet method. + + Purpose: Check whether the instruction is a function call which + matches one of the recognised nondet library methods, and + return some information about it. + +\*******************************************************************/ + +static nondet_instruction_infot get_nondet_instruction_info( + const goto_programt::const_targett &instr) +{ + if(!(instr->is_function_call() && instr->code.id()==ID_code)) + { + return nondet_instruction_infot(); + } + const auto &code=to_code(instr->code); + if(code.get_statement()!=ID_function_call) + { + return nondet_instruction_infot(); + } + const auto &function_call=to_code_function_call(code); + return is_nondet_returning_object(function_call); +} + +/*******************************************************************\ + +Function: is_symbol_with_id + + Inputs: + expr: The expression which may be a symbol. + identifier: Some identifier. + + Outputs: True if the expression is a symbol with the specified identifier. + + Purpose: Return whether the expression is a symbol with the specified + identifier. + +\*******************************************************************/ + +static bool is_symbol_with_id(const exprt& expr, const irep_idt& identifier) +{ + return expr.id()==ID_symbol && + to_symbol_expr(expr).get_identifier()==identifier; +} + +/*******************************************************************\ + +Function: is_typecast_with_id + + Inputs: + expr: The expression which may be a typecast. + identifier: Some identifier. + + Outputs: True if the expression is a typecast with one operand, and the + typecast's identifier matches the specified identifier. + + Purpose: Return whether the expression is a typecast with the specified + identifier. + +\*******************************************************************/ + +static bool is_typecast_with_id(const exprt& expr, const irep_idt& identifier) +{ + if(!(expr.id()==ID_typecast && expr.operands().size()==1)) + { + return false; + } + const auto &typecast=to_typecast_expr(expr); + if(!(typecast.op().id()==ID_symbol && !typecast.op().has_operands())) + { + return false; + } + const auto &op_symbol=to_symbol_expr(typecast.op()); + // Return whether the typecast has the expected operand + return op_symbol.get_identifier()==identifier; +} + +/*******************************************************************\ + +Function: is_assignment_from + + Inputs: + instr: A goto program instruction. + identifier: Some identifier. + + Outputs: True if the expression is a typecast with one operand, and the + typecast's identifier matches the specified identifier. + + Purpose: Return whether the instruction is an assignment, and the rhs is a + symbol or typecast expression with the specified identifier. + +\*******************************************************************/ + +static bool is_assignment_from( + const goto_programt::instructiont &instr, + const irep_idt &identifier) +{ + // If not an assignment, return false + if(!instr.is_assign()) + { + return false; + } + const auto &rhs=to_code_assign(instr.code).rhs(); + return is_symbol_with_id(rhs, identifier) || + is_typecast_with_id(rhs, identifier); +} + +/*******************************************************************\ + +Function: check_and_replace_target + + Inputs: + goto_program: The goto program to modify. + target: A single step of the goto program which may be erased and + replaced. + + Outputs: The next instruction to process, probably with this function. + + Purpose: Given an iterator into a list of instructions, modify the list to + replace 'nondet' library functions with CBMC-native nondet + expressions, and return an iterator to the next instruction to check. + +\*******************************************************************/ + +static goto_programt::const_targett check_and_replace_target( + goto_programt &goto_program, + const goto_programt::const_targett &target) +{ + // Check whether this is a nondet library method, and return if not + const auto instr_info=get_nondet_instruction_info(target); + const auto next_instr=std::next(target); + if(instr_info.get_instruction_type()== + nondet_instruction_infot::is_nondett::FALSE) + { + return next_instr; + } + + // Look at the next instruction, ensure that it is an assignment + assert(next_instr->is_assign()); + // Get the name of the LHS of the assignment + const auto &next_instr_assign_lhs=to_code_assign(next_instr->code).lhs(); + if(!(next_instr_assign_lhs.id()==ID_symbol && + !next_instr_assign_lhs.has_operands())) + { + return next_instr; + } + const auto return_identifier= + to_symbol_expr(next_instr_assign_lhs).get_identifier(); + + auto &instructions=goto_program.instructions; + const auto end=instructions.cend(); + + // Look for an instruction where this name is on the RHS of an assignment + const auto matching_assignment=std::find_if( + next_instr, + end, + [&return_identifier](const goto_programt::instructiont &instr) + { + return is_assignment_from(instr, return_identifier); + }); + + assert(matching_assignment!=end); + + // Assume that the LHS of *this* assignment is the actual nondet variable + const auto &code_assign=to_code_assign(matching_assignment->code); + const auto nondet_var=code_assign.lhs(); + const auto source_loc=target->source_location; + + // Erase from the nondet function call to the assignment + const auto after_matching_assignment=std::next(matching_assignment); + assert(after_matching_assignment!=end); + + const auto after_erased=goto_program.instructions.erase( + target, after_matching_assignment); + + const auto inserted=goto_program.insert_before(after_erased); + inserted->make_assignment(); + side_effect_expr_nondett inserted_expr(nondet_var.type()); + inserted_expr.set_nullable( + instr_info.get_nullable_type()== + nondet_instruction_infot::is_nullablet::TRUE); + inserted->code=code_assignt(nondet_var, inserted_expr); + inserted->code.add_source_location()=source_loc; + inserted->source_location=source_loc; + + goto_program.update(); + + return after_erased; +} + +/*******************************************************************\ + +Function: replace_java_nondet + + Inputs: + goto_program: The goto program to modify. + + Purpose: Checks each instruction in the goto program to see whether + it is a method returning nondet. If it is, replaces the + function call with an irep representing a nondet side + effect with an appropriate type. + +\*******************************************************************/ + +static void replace_java_nondet(goto_programt &goto_program) +{ + for(auto instruction_iterator=goto_program.instructions.cbegin(), + end=goto_program.instructions.cend(); + instruction_iterator!=end;) + { + instruction_iterator=check_and_replace_target( + goto_program, + instruction_iterator); + } +} + + + +void replace_java_nondet(goto_functionst &goto_functions) +{ + for(auto &goto_program : goto_functions.function_map) + { + replace_java_nondet(goto_program.second.body); + } + goto_functions.compute_location_numbers(); +} diff --git a/src/goto-programs/replace_java_nondet.h b/src/goto-programs/replace_java_nondet.h new file mode 100644 index 00000000000..077f95ab84c --- /dev/null +++ b/src/goto-programs/replace_java_nondet.h @@ -0,0 +1,28 @@ +/*******************************************************************\ + +Module: Replace Java Nondet expressions + +Author: Reuben Thomas, reuben.thomas@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_PROGRAMS_REPLACE_JAVA_NONDET_H +#define CPROVER_GOTO_PROGRAMS_REPLACE_JAVA_NONDET_H + +class goto_functionst; + +/*******************************************************************\ + +Function: replace_java_nondet + + Inputs: + goto_functions: The set of goto programs to modify. + + Purpose: Replace calls to nondet library functions with an internal + nondet representation. + +\*******************************************************************/ + +void replace_java_nondet(goto_functionst &goto_functions); + +#endif diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 4888810bd83..65696e7877a 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -31,6 +31,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include class patternt { @@ -2531,6 +2532,29 @@ void java_bytecode_convert_method( safe_pointer > needed_methods, safe_pointer > needed_classes) { + static const std::unordered_set methods_to_ignore + { + "nondetBoolean", + "nondetByte", + "nondetChar", + "nondetShort", + "nondetInt", + "nondetLong", + "nondetFloat", + "nondetDouble", + "nondetWithNull", + "nondetWithoutNull", + }; + + if(std::regex_match( + id2string(class_symbol.name), + std::regex(".*org\\.cprover\\.CProver.*")) && + methods_to_ignore.find(id2string(method.name))!=methods_to_ignore.end()) + { + // Ignore these methods, rely on default stubbing behaviour. + return; + } + java_bytecode_convert_methodt java_bytecode_convert_method( symbol_table, message_handler, diff --git a/src/java_bytecode/library/Makefile b/src/java_bytecode/library/Makefile new file mode 100644 index 00000000000..aa51ec1694a --- /dev/null +++ b/src/java_bytecode/library/Makefile @@ -0,0 +1,26 @@ +all: org.cprover.jar + +SOURCE_DIR := src +BINARY_DIR := classes + +FIND := find + +JAVAC := javac +JFLAGS := -sourcepath $(SOURCE_DIR) -d $(BINARY_DIR) + +CLASSPATH := SOURCE_DIR + +all_javas := $(shell $(FIND) $(SOURCE_DIR) -name '*.java') + +$(BINARY_DIR): + mkdir -p $(BINARY_DIR) + +.PHONY: compile +compile: $(BINARY_DIR) + $(JAVAC) $(JFLAGS) $(all_javas) + +JAR := jar +JARFLAGS := -cf + +org.cprover.jar: compile + $(JAR) $(JARFLAGS) $@ -C $(BINARY_DIR) org diff --git a/src/java_bytecode/library/src/org/cprover/CProver.java b/src/java_bytecode/library/src/org/cprover/CProver.java index 72c3eeb1d70..6aadd228e9e 100644 --- a/src/java_bytecode/library/src/org/cprover/CProver.java +++ b/src/java_bytecode/library/src/org/cprover/CProver.java @@ -3,9 +3,123 @@ public final class CProver { public static boolean enableAssume=true; - public static void assume(boolean condition) + public static boolean enableNondet=true; + + public static boolean nondetBoolean() + { + if (enableNondet) + { + throw new RuntimeException( + "Cannot execute program with CProver.nondetBoolean()"); + } + + return false; + } + + public static byte nondetByte() + { + if (enableNondet) + { + throw new RuntimeException( + "Cannot execute program with CProver.nondetByte()"); + } + + return 0; + } + + public static char nondetChar() + { + if (enableNondet) + { + throw new RuntimeException( + "Cannot execute program with CProver.nondetChar()"); + } + + return '\0'; + } + + public static short nondetShort() + { + if (enableNondet) + { + throw new RuntimeException( + "Cannot execute program with CProver.nondetShort()"); + } + + return 0; + } + + public static int nondetInt() + { + if (enableNondet) + { + throw new RuntimeException( + "Cannot execute program with CProver.nondetInt()"); + } + + return 0; + } + + public static long nondetLong() + { + if (enableNondet) + { + throw new RuntimeException( + "Cannot execute program with CProver.nondetLong()"); + } + + return 0; + } + + public static float nondetFloat() + { + if (enableNondet) + { + throw new RuntimeException( + "Cannot execute program with CProver.nondetFloat()"); + } + + return 0; + } + + public static double nondetDouble() + { + if (enableNondet) + { + throw new RuntimeException( + "Cannot execute program with CProver.nondetDouble()"); + } + + return 0; + } + + public static T nondetWithNull() + { + if (enableNondet) + { + throw new RuntimeException( + "Cannot execute program with CProver.nondetWithNull(T)"); + } + + return null; + } + + public static T nondetWithoutNull() + { + if (enableNondet) + { + throw new RuntimeException( + "Cannot execute program with CProver.nondetWithoutNull(T)"); + } + + return null; + } + + public static void assume(boolean condition) { - if(enableAssume) - throw new RuntimeException("Cannot execute program with CProver.assume()"); - } + if(enableAssume && !condition) + { + throw new RuntimeException("CProver.assume() predicate is false"); + } + } } diff --git a/src/util/irep_ids.txt b/src/util/irep_ids.txt index 5e364d97ea0..a9672b2cec7 100644 --- a/src/util/irep_ids.txt +++ b/src/util/irep_ids.txt @@ -804,4 +804,5 @@ cprover_string_to_lower_case_func cprover_string_to_upper_case_func cprover_string_trim_func cprover_string_value_of_func -basic_block_covered_lines \ No newline at end of file +basic_block_covered_lines +is_nondet_nullable diff --git a/src/util/std_code.h b/src/util/std_code.h index 17d038274a3..85a35252dfb 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -1036,14 +1036,41 @@ class side_effect_expr_nondett:public side_effect_exprt public: side_effect_expr_nondett():side_effect_exprt(ID_nondet) { + set_nullable(true); } explicit side_effect_expr_nondett(const typet &_type): side_effect_exprt(ID_nondet, _type) { + set_nullable(true); + } + + void set_nullable(bool nullable) + { + set(ID_is_nondet_nullable, nullable); + } + + bool get_nullable() const + { + return get_bool(ID_is_nondet_nullable); } }; +inline side_effect_expr_nondett &to_side_effect_expr_nondet(exprt &expr) +{ + auto &side_effect_expr_nondet=to_side_effect_expr(expr); + assert(side_effect_expr_nondet.get_statement()==ID_nondet); + return static_cast(side_effect_expr_nondet); +} + +inline const side_effect_expr_nondett &to_side_effect_expr_nondet( + const exprt &expr) +{ + const auto &side_effect_expr_nondet=to_side_effect_expr(expr); + assert(side_effect_expr_nondet.get_statement()==ID_nondet); + return static_cast(side_effect_expr_nondet); +} + /*! \brief A function call side effect */ class side_effect_expr_function_callt:public side_effect_exprt