diff --git a/regression/cbmc-java/Makefile b/regression/cbmc-java/Makefile index cee83cba67a..89c7c9da139 100644 --- a/regression/cbmc-java/Makefile +++ b/regression/cbmc-java/Makefile @@ -18,3 +18,16 @@ show: vim -o "$$dir/*.java" "$$dir/*.out"; \ fi; \ done; + +%.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/nondetAssume1/NondetAssume1.class b/regression/cbmc-java/nondetAssume1/NondetAssume1.class new file mode 100644 index 00000000000..e05127a4413 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..2883e69dd08 --- /dev/null +++ b/regression/cbmc-java/nondetAssume1/NondetAssume1.java @@ -0,0 +1,11 @@ +import org.cprover.CProver; + +class NondetAssume1 +{ + void foo() + { + 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..17e769ddad0 --- /dev/null +++ b/regression/cbmc-java/nondetAssume1/test.desc @@ -0,0 +1,6 @@ +CORE +NondetAssume1.class +--function NondetAssume1.foo +^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..5a956c6827f 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..ebff45ddd53 --- /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 foo() + { + 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..4b4f91eadc1 --- /dev/null +++ b/regression/cbmc-java/nondetAssume2/test.desc @@ -0,0 +1,6 @@ +CORE +NondetAssume2.class +--function NondetAssume2.foo +^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..ee3af8a020c 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..34ad5829237 --- /dev/null +++ b/regression/cbmc-java/nondetBoolean/NondetBoolean.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetBoolean +{ + static void foo() + { + 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..9913935eb03 --- /dev/null +++ b/regression/cbmc-java/nondetBoolean/test.desc @@ -0,0 +1,6 @@ +CORE +NondetBoolean.class +--function NondetBoolean.foo +^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..208b0bd3aba 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..b300c9c3c5f --- /dev/null +++ b/regression/cbmc-java/nondetByte/NondetByte.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetByte +{ + static void foo() + { + 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..c1fbe8bd0fb --- /dev/null +++ b/regression/cbmc-java/nondetByte/test.desc @@ -0,0 +1,6 @@ +CORE +NondetByte.class +--function NondetByte.foo +^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..2b767b750bd 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..2d698439f74 --- /dev/null +++ b/regression/cbmc-java/nondetCastToObject/NondetCastToObject.java @@ -0,0 +1,11 @@ +import org.cprover.CProver; + +class NondetCastToObject +{ + void foo() + { + 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..c59f81d644f --- /dev/null +++ b/regression/cbmc-java/nondetCastToObject/test.desc @@ -0,0 +1,6 @@ +CORE +NondetCastToObject.class +--function NondetCastToObject.foo +^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..315206062ab 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..62de7d3eb66 --- /dev/null +++ b/regression/cbmc-java/nondetChar/NondetChar.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetChar +{ + static void foo() + { + 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..306394b706c --- /dev/null +++ b/regression/cbmc-java/nondetChar/test.desc @@ -0,0 +1,6 @@ +CORE +NondetChar.class +--function NondetChar.foo +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/nondetDouble/NondetDouble.class b/regression/cbmc-java/nondetDouble/NondetDouble.class new file mode 100644 index 00000000000..9e71dc4c959 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..c431d52db1e --- /dev/null +++ b/regression/cbmc-java/nondetDouble/NondetDouble.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetDouble +{ + static void foo() + { + 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..9c9228fdd24 --- /dev/null +++ b/regression/cbmc-java/nondetDouble/test.desc @@ -0,0 +1,6 @@ +CORE +NondetDouble.class +--function NondetDouble.foo +^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..4e8d8557ccb 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..31a8241f51b --- /dev/null +++ b/regression/cbmc-java/nondetFloat/NondetFloat.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetFloat +{ + static void foo() + { + 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..7370f25ae93 --- /dev/null +++ b/regression/cbmc-java/nondetFloat/test.desc @@ -0,0 +1,6 @@ +CORE +NondetFloat.class +--function NondetFloat.foo +^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..d0aa1cbfaef 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..d481494fe8b --- /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 foo() + { + 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..c91a230aa69 --- /dev/null +++ b/regression/cbmc-java/nondetGenericArray/test.desc @@ -0,0 +1,6 @@ +KNOWNBUG +NondetGenericArray.class +--function NondetGenericArray.foo +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/nondetGenericImplicitType/Foo.class b/regression/cbmc-java/nondetGenericImplicitType/Foo.class new file mode 100644 index 00000000000..fa7a99ecf42 Binary files /dev/null and b/regression/cbmc-java/nondetGenericImplicitType/Foo.class differ diff --git a/regression/cbmc-java/nondetGenericImplicitType/NondetGenericImplicitType.class b/regression/cbmc-java/nondetGenericImplicitType/NondetGenericImplicitType.class new file mode 100644 index 00000000000..6cc50d38fa2 Binary files /dev/null and b/regression/cbmc-java/nondetGenericImplicitType/NondetGenericImplicitType.class differ diff --git a/regression/cbmc-java/nondetGenericNoAssignment/NondetGenericNoAssignment.class b/regression/cbmc-java/nondetGenericNoAssignment/NondetGenericNoAssignment.class new file mode 100644 index 00000000000..6139221c11f Binary files /dev/null and b/regression/cbmc-java/nondetGenericNoAssignment/NondetGenericNoAssignment.class differ 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..47255fc0445 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..39aab3b241f --- /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 foo() + { + 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..33ea1bc39ea --- /dev/null +++ b/regression/cbmc-java/nondetGenericRecursive/test.desc @@ -0,0 +1,6 @@ +CORE +NondetGenericRecursive.class +--function NondetGenericRecursive.foo +^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..835d3a60251 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..4cb14e5945b --- /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 foo() + { + 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..821072235a2 --- /dev/null +++ b/regression/cbmc-java/nondetGenericRecursive2/test.desc @@ -0,0 +1,6 @@ +KNOWNBUG +NondetGenericRecursive2.class +--function NondetGenericRecursive2.foo +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/nondetGenericWithNull/A.class b/regression/cbmc-java/nondetGenericWithNull/A.class new file mode 100644 index 00000000000..39c11a22d15 Binary files /dev/null and b/regression/cbmc-java/nondetGenericWithNull/A.class differ 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..7f80aedd941 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..d7c4bdb993e --- /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 foo() + { + 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..d3c4f793445 --- /dev/null +++ b/regression/cbmc-java/nondetGenericWithNull/test.desc @@ -0,0 +1,6 @@ +CORE +NondetGenericWithNull.class +--function NondetGenericWithNull.foo +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/nondetGenericWithoutNull/A.class b/regression/cbmc-java/nondetGenericWithoutNull/A.class new file mode 100644 index 00000000000..1a0d5663bb2 Binary files /dev/null and b/regression/cbmc-java/nondetGenericWithoutNull/A.class differ diff --git a/regression/cbmc-java/nondetGenericWithoutNull/B.class b/regression/cbmc-java/nondetGenericWithoutNull/B.class new file mode 100644 index 00000000000..1173660d6c2 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..a7d51841920 Binary files /dev/null and b/regression/cbmc-java/nondetGenericWithoutNull/NondetGenericWithoutNull.class differ diff --git a/regression/cbmc-java/nondetInt/NondetInt.class b/regression/cbmc-java/nondetInt/NondetInt.class new file mode 100644 index 00000000000..3b244fcdd0c 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..4b2babdc4fa --- /dev/null +++ b/regression/cbmc-java/nondetInt/NondetInt.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetInt +{ + static void foo() + { + 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..7669da239ec --- /dev/null +++ b/regression/cbmc-java/nondetInt/test.desc @@ -0,0 +1,6 @@ +CORE +NondetInt.class +--function NondetInt.foo +^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..8ed4f3042e8 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..1d2ebb98703 --- /dev/null +++ b/regression/cbmc-java/nondetLong/NondetLong.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetLong +{ + static void foo() + { + 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..60e03901419 --- /dev/null +++ b/regression/cbmc-java/nondetLong/test.desc @@ -0,0 +1,6 @@ +CORE +NondetLong.class +--function NondetLong.foo +^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..24e76af762b 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..d54418e263c --- /dev/null +++ b/regression/cbmc-java/nondetShort/NondetShort.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetShort +{ + static void foo() + { + 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..882806378b6 --- /dev/null +++ b/regression/cbmc-java/nondetShort/test.desc @@ -0,0 +1,6 @@ +CORE +NondetShort.class +--function NondetShort.foo +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index a3124f3b898..19add7771c6 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -6,6 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#ifdef DEBUG +#include +#endif + #include #include @@ -905,6 +909,7 @@ void goto_convertt::convert_assign( copy(new_assign, ASSIGN, dest); } + else { clean_expr(rhs, dest); diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index f34ee9d03a0..501804e017e 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -6,6 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#ifdef DEBUG +#include +#endif + #include #include #include diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 447b5dacb80..98d95046cfe 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -5,6 +5,7 @@ Module: JAVA Bytecode Language Conversion Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ + #ifdef DEBUG #include #endif @@ -15,21 +16,75 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include +#include "bytecode_info.h" #include "java_bytecode_convert_method.h" #include "java_bytecode_convert_method_class.h" -#include "bytecode_info.h" +#include "java_object_factory.h" #include "java_types.h" #include #include #include #include +#include +#include + +/*******************************************************************\ + +Function: traverse_expr_tree + + Inputs: `expr`: an expression tree + + Outputs: None + + Purpose: Looks for a symbol node with identifier 'nondetWith(out?)Null'. + Finds the following statement, checks if it is an "assert", and + replaces it with a code_skipt if so. + +\*******************************************************************/ + +static void remove_assert_after_generic_nondet(exprt &expr) +{ + traverse_expr_tree( + expr, + [] (exprt &expr, const std::vector &parents) + { + const std::regex id_regex( + ".*org.cprover.CProver.(nondetWithNull|nondetWithoutNull).*"); + if(expr.id()==ID_symbol && + std::regex_match(id2string(to_symbol_expr(expr).get_identifier()), + id_regex)) + { + assert(2<=parents.size()); + const auto before_1=*std::prev(parents.end(), 1); + const auto before_2=*std::prev(parents.end(), 2); + + for(auto it=before_2->operands().begin(), + end=before_2->operands().end(); + it!=end; + ++it) + { + if(&(*it)==before_1) + { + const auto next_it=std::next(it); + if(next_it!=end && + next_it->id()==ID_code && + to_code(*next_it).get_statement()=="assert") + { + *next_it=code_skipt(); + } + } + } + } + }); +} class patternt { @@ -396,7 +451,11 @@ void java_bytecode_convert_methodt::convert( if((!m.is_abstract) && (!m.is_native)) method_symbol.value=convert_instructions(m, code_type); + remove_assert_after_generic_nondet(method_symbol.value); + // Replace the existing stub symbol with the real deal: + + // do we have the method symbol already? const auto s_it=symbol_table.symbols.find(method.get_name()); assert(s_it!=symbol_table.symbols.end()); symbol_table.symbols.erase(s_it); @@ -840,23 +899,59 @@ void java_bytecode_convert_methodt::check_static_field_stub( /*******************************************************************\ -Function: java_bytecode_convert_methodt::convert_instructions +Function: get_bytecode_type_width - Inputs: + Inputs: `type`: A bytecode type. - Outputs: + Outputs: The width of the type, in bits. - Purpose: + Purpose: Used to check the size of the item on the top of the stack. \*******************************************************************/ -static unsigned get_bytecode_type_width(const typet &ty) +static unsigned get_bytecode_type_width(const typet &type) { - if(ty.id()==ID_pointer) + if(type.id()==ID_pointer) return 32; - return ty.get_unsigned_int(ID_width); + return type.get_unsigned_int(ID_width); +} + +/*******************************************************************\ + +Function: statement_is_static_with_name + +Inputs: `statement`: A statement to check. + `arg0`: The first argument of the statement. + `desired_name`: The desired identifier of arg0. + + Outputs: True if statement matches "invokestatic" and arg0's identifier + matches the desired name, false otherwise. + + Purpose: Used to match nondet library methods concisely. + +\*******************************************************************/ + +static bool statement_is_static_with_name( + const irep_idt &statement, + const exprt &arg0, + const std::string &desired_name) +{ + return statement=="invokestatic" && + id2string(arg0.get(ID_identifier))==desired_name; } +/*******************************************************************\ + +Function: java_bytecode_convert_methodt::convert_instructions + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + codet java_bytecode_convert_methodt::convert_instructions( const methodt &method, const code_typet &method_type) @@ -993,8 +1088,9 @@ codet java_bytecode_convert_methodt::convert_instructions( if(a_it->second.done) continue; - working_set - .insert(a_it->second.successors.begin(), a_it->second.successors.end()); + + working_set.insert( + a_it->second.successors.begin(), a_it->second.successors.end()); instructionst::const_iterator i_it=a_it->second.source; stack.swap(a_it->second.stack); @@ -1092,16 +1188,16 @@ codet java_bytecode_convert_methodt::convert_instructions( get_message_handler()); } } + // replace calls to CProver.assume - else if(statement=="invokestatic" && - id2string(arg0.get(ID_identifier))== - "java::org.cprover.CProver.assume:(Z)V") + else if(statement_is_static_with_name( + statement, arg0, "java::org.cprover.CProver.assume:(Z)V")) { const code_typet &code_type=to_code_type(arg0.type()); // sanity check: function has the right number of args assert(code_type.parameters().size()==1); - exprt operand = pop(1)[0]; + exprt operand=pop(1)[0]; // we may need to adjust the type of the argument if(operand.type()!=bool_typet()) operand.make_typecast(bool_typet()); @@ -1111,6 +1207,121 @@ codet java_bytecode_convert_methodt::convert_instructions( loc.set_function(method_id); c.add_source_location()=loc; } + + // if the statement is a nondet boolean + else if(statement_is_static_with_name( + statement, arg0, "java::org.cprover.CProver.nondetBoolean:()Z")) + { + results.resize(1); + results[0]=side_effect_expr_nondett(java_boolean_type()); + results[0].add_source_location()=i_it->source_location; + } + + // if the statement is a nondet byte + else if(statement_is_static_with_name( + statement, arg0, "java::org.cprover.CProver.nondetByte:()B")) + { + results.resize(1); + results[0]=side_effect_expr_nondett(java_byte_type()); + results[0].add_source_location()=i_it->source_location; + } + + // if the statement is a nondet char + else if(statement_is_static_with_name( + statement, arg0, "java::org.cprover.CProver.nondetChar:()C")) + { + results.resize(1); + results[0]=side_effect_expr_nondett(java_char_type()); + results[0].add_source_location()=i_it->source_location; + } + + // if the statement is a nondet short + else if(statement_is_static_with_name( + statement, arg0, "java::org.cprover.CProver.nondetShort:()S")) + { + results.resize(1); + results[0]=side_effect_expr_nondett(java_short_type()); + results[0].add_source_location()=i_it->source_location; + } + + // if the statement is a nondet int + else if(statement_is_static_with_name( + statement, arg0, "java::org.cprover.CProver.nondetInt:()I")) + { + results.resize(1); + results[0]=side_effect_expr_nondett(java_int_type()); + results[0].add_source_location()=i_it->source_location; + } + + // if the statement is a nondet long + else if(statement_is_static_with_name( + statement, arg0, "java::org.cprover.CProver.nondetLong:()J")) + { + results.resize(1); + results[0]=side_effect_expr_nondett(java_long_type()); + results[0].add_source_location()=i_it->source_location; + } + + // if the statement is a nondet float + else if(statement_is_static_with_name( + statement, arg0, "java::org.cprover.CProver.nondetFloat:()F")) + { + results.resize(1); + results[0]=side_effect_expr_nondett(java_float_type()); + results[0].add_source_location()=i_it->source_location; + } + + // if the statement is a nondet double + else if(statement_is_static_with_name( + statement, arg0, "java::org.cprover.CProver.nondetDouble:()D")) + { + results.resize(1); + results[0]=side_effect_expr_nondett(java_double_type()); + results[0].add_source_location()=i_it->source_location; + } + + else if( + statement=="invokestatic" && + std::regex_match( + id2string(arg0.get(ID_identifier)), + std::regex( + ".*org.cprover.CProver.(nondetWithNull|nondetWithoutNull).*")) && + !working_set.empty()) + { + // Get the nondet function code type. + auto func_type=to_code_type(arg0.type()); + + // Find the next instruction. + const auto working_set_begin=working_set.begin(); + const auto next_address=address_map.find(*working_set_begin); + assert(next_address!=address_map.end()); + + // Find the correct return type. + const auto next_source=next_address->second.source; + const auto next_statement=next_source->statement; + // The next return type is the casted-to type *if* the next statement is + // a checkcast. Otherwise, we leave it as-is. + const auto return_type= + (next_statement=="checkcast" && next_source->args.size()>=1) ? + pointer_typet(next_source->args[0].type()) : + func_type.return_type(); + + // Reconstruct a function call with the correct return type. + code_function_callt call; + + source_locationt loc=i_it->source_location; + loc.set_function(method_id); + call.add_source_location()=loc; + call.function().add_source_location()=loc; + func_type.return_type()=return_type; + call.function()=symbol_exprt(arg0.get(ID_identifier), func_type); + call.lhs()=tmp_variable("return", return_type); + + results.resize(1); + results[0]=java_bytecode_promotion(call.lhs()); + c=call; + } + else if(statement=="invokeinterface" || statement=="invokespecial" || statement=="invokevirtual" || @@ -1712,8 +1923,7 @@ codet java_bytecode_convert_methodt::convert_instructions( results[2]=op[1]; results[3]=op[2]; } - // dup2* behaviour depends on the size of the operands on the - // stack + // dup2* behaviour depends on the size of the operands on the stack else if(statement=="dup2") { assert(!stack.empty() && results.empty()); @@ -2271,6 +2481,14 @@ void java_bytecode_convert_method( safe_pointer > needed_methods, safe_pointer > needed_classes) { + if(class_symbol.name=="org.cprover.CProver" && + (method.name=="nondetWithNull" || + method.name=="nondetWithoutNull")) + { + // 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/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 668960dbe17..eb6d81c42a9 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -43,7 +43,6 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) { disable_runtime_checks=cmd.isset("disable-runtime-check"); assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null"); - string_refinement_enabled=cmd.isset("string-refine"); if(cmd.isset("java-max-input-array-length")) max_nondet_array_length= std::stoi(cmd.get_value("java-max-input-array-length")); diff --git a/src/java_bytecode/java_bytecode_typecheck_code.cpp b/src/java_bytecode/java_bytecode_typecheck_code.cpp index 788f5fa592b..7cc93a991a6 100644 --- a/src/java_bytecode/java_bytecode_typecheck_code.cpp +++ b/src/java_bytecode/java_bytecode_typecheck_code.cpp @@ -6,7 +6,12 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#ifdef DEBUG +#include +#endif + #include "java_bytecode_typecheck.h" +#include "java_object_factory.h" /*******************************************************************\ @@ -27,6 +32,7 @@ void java_bytecode_typecheckt::typecheck_code(codet &code) if(statement==ID_assign) { code_assignt &code_assign=to_code_assign(code); + typecheck_expr(code_assign.lhs()); typecheck_expr(code_assign.rhs()); @@ -35,8 +41,10 @@ void java_bytecode_typecheckt::typecheck_code(codet &code) } else if(statement==ID_block) { - Forall_operands(it, code) + Forall_operands(it, to_code_block(code)) + { typecheck_code(to_code(*it)); + } } else if(statement==ID_label) { diff --git a/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/src/java_bytecode/java_bytecode_typecheck_expr.cpp index 11e488ff7fe..d49e017b37e 100644 --- a/src/java_bytecode/java_bytecode_typecheck_expr.cpp +++ b/src/java_bytecode/java_bytecode_typecheck_expr.cpp @@ -7,6 +7,9 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include +#ifdef DEBUG +#include +#endif #include #include @@ -47,11 +50,16 @@ void java_bytecode_typecheckt::typecheck_expr(exprt &expr) typecheck_expr_symbol(to_symbol_expr(expr)); else if(expr.id()==ID_side_effect) { - const irep_idt &statement=to_side_effect_expr(expr).get_statement(); + auto &side_effect_expr=to_side_effect_expr(expr); + const irep_idt &statement=side_effect_expr.get_statement(); if(statement==ID_java_new) - typecheck_expr_java_new(to_side_effect_expr(expr)); + { + typecheck_expr_java_new(side_effect_expr); + } else if(statement==ID_java_new_array) - typecheck_expr_java_new_array(to_side_effect_expr(expr)); + { + typecheck_expr_java_new_array(side_effect_expr); + } } else if(expr.id()==ID_java_string_literal) typecheck_expr_java_string_literal(expr); diff --git a/src/java_bytecode/library/src/org/cprover/CProver.java b/src/java_bytecode/library/src/org/cprover/CProver.java index 72c3eeb1d70..3780450a37d 100644 --- a/src/java_bytecode/library/src/org/cprover/CProver.java +++ b/src/java_bytecode/library/src/org/cprover/CProver.java @@ -3,9 +3,113 @@ public final class CProver { public static boolean enableAssume=true; + 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 void assume(boolean condition) { if(enableAssume) - throw new RuntimeException("Cannot execute program with CProver.assume()"); + { + throw new RuntimeException( + "Cannot execute program with CProver.assume()"); + } } } diff --git a/src/java_bytecode/library/target/org/cprover/CProver.class b/src/java_bytecode/library/target/org/cprover/CProver.class new file mode 100644 index 00000000000..02f1504b616 Binary files /dev/null and b/src/java_bytecode/library/target/org/cprover/CProver.class differ diff --git a/src/util/expr_util.h b/src/util/expr_util.h index f5d33b95cad..819db8838f9 100644 --- a/src/util/expr_util.h +++ b/src/util/expr_util.h @@ -17,8 +17,10 @@ Author: Daniel Kroening, kroening@kroening.com */ #include "irep.h" +#include "expr.h" + +#include -class exprt; class symbol_exprt; class update_exprt; class with_exprt; @@ -51,4 +53,59 @@ bool has_subexpr(const exprt &, const irep_idt &); /*! lift up an if_exprt one level */ if_exprt lift_if(const exprt &, std::size_t operand_number); +/*******************************************************************\ + +Function: traverse_expr_tree + + Inputs: `expr`: an expression tree to traverse + `parents`: will hold previously-visited nodes + `func`: will be called on each node, takes the node and the `parents` + stack as arguments + + Outputs: None + + Purpose: Abstracts the process of calling a function on each node of the + expression tree. + +\*******************************************************************/ + +template +inline void traverse_expr_tree( + exprt &expr, + std::vector &parents, + Func func) +{ + const auto &parents_ref=parents; + func(expr, parents_ref); + + parents.push_back(&expr); + for(auto &op : expr.operands()) + { + traverse_expr_tree(op, parents, func); + } + parents.pop_back(); +} + +/*******************************************************************\ + +Function: traverse_expr_tree + + Inputs: `expr`: an expression tree to traverse + `func`: will be called on each node, takes the node and the `parents` + stack as arguments + + Outputs: None + + Purpose: Behaves exactly like traverse_expr_tree with three arguments, but + sets up the `parents` vector internally. + +\*******************************************************************/ + +template +inline void traverse_expr_tree(exprt &expr, Func &&func) +{ + std::vector parents; + traverse_expr_tree(expr, parents, std::forward(func)); +} + #endif // CPROVER_UTIL_EXPR_UTIL_H diff --git a/src/util/irep_ids.txt b/src/util/irep_ids.txt index 29907f11040..37585ceba96 100644 --- a/src/util/irep_ids.txt +++ b/src/util/irep_ids.txt @@ -802,4 +802,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 +nondet_allow_null diff --git a/src/util/std_code.h b/src/util/std_code.h index 08aec694e9e..1ab10a01450 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -1044,6 +1044,22 @@ class side_effect_expr_nondett:public side_effect_exprt } }; +static inline const side_effect_expr_nondett & + to_side_effect_expr_nondet(const exprt &expr) +{ + const auto &side_effect_expr=to_side_effect_expr(expr); + assert(side_effect_expr.get_statement() == ID_nondet); + return static_cast(side_effect_expr); +} + +static inline side_effect_expr_nondett & + to_side_effect_expr_nondet(exprt &expr) +{ + auto &side_effect_expr=to_side_effect_expr(expr); + assert(side_effect_expr.get_statement() == ID_nondet); + return static_cast(side_effect_expr); +} + /*! \brief A function call side effect */ class side_effect_expr_function_callt:public side_effect_exprt