From 241dbee1659d343d6104442695783d0567bbe0d4 Mon Sep 17 00:00:00 2001 From: reuk Date: Tue, 14 Mar 2017 16:33:45 +0000 Subject: [PATCH 1/7] Add org.cprover package and makefile --- src/java_bytecode/library/Makefile | 26 ++++ .../library/src/org/cprover/CProver.java | 121 +++++++++++++++++- 2 files changed, 144 insertions(+), 3 deletions(-) create mode 100644 src/java_bytecode/library/Makefile 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..0dcae58c67e 100644 --- a/src/java_bytecode/library/src/org/cprover/CProver.java +++ b/src/java_bytecode/library/src/org/cprover/CProver.java @@ -3,9 +3,124 @@ 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()"); - } + { + throw new RuntimeException( + "Cannot execute program with CProver.assume()"); + } + } } From 7ed66a1a0632d278706056a9395947478a9a43ef Mon Sep 17 00:00:00 2001 From: reuk Date: Tue, 14 Mar 2017 16:58:20 +0000 Subject: [PATCH 2/7] Add tests --- regression/cbmc-java/Makefile | 13 ++++++++ .../cbmc-java/NondetArray/NondetArray.class | Bin 0 -> 722 bytes .../cbmc-java/NondetArray/NondetArray.java | 10 ++++++ regression/cbmc-java/NondetArray/test.desc | 6 ++++ .../cbmc-java/NondetArray2/NondetArray2.class | Bin 0 -> 907 bytes .../cbmc-java/NondetArray2/NondetArray2.java | 15 +++++++++ regression/cbmc-java/NondetArray2/test.desc | 6 ++++ .../cbmc-java/NondetArray3/NondetArray3.class | Bin 0 -> 935 bytes .../cbmc-java/NondetArray3/NondetArray3.java | 16 ++++++++++ regression/cbmc-java/NondetArray3/test.desc | 6 ++++ .../cbmc-java/NondetArray4/NondetArray4.class | Bin 0 -> 806 bytes .../cbmc-java/NondetArray4/NondetArray4.java | 14 ++++++++ regression/cbmc-java/NondetArray4/test.desc | 6 ++++ .../NondetAssume1/NondetAssume1.class | Bin 0 -> 722 bytes .../NondetAssume1/NondetAssume1.java | 11 +++++++ regression/cbmc-java/NondetAssume1/test.desc | 6 ++++ regression/cbmc-java/NondetAssume2/A.class | Bin 0 -> 256 bytes regression/cbmc-java/NondetAssume2/B.class | Bin 0 -> 258 bytes regression/cbmc-java/NondetAssume2/C.class | Bin 0 -> 258 bytes .../NondetAssume2/NondetAssume2.class | Bin 0 -> 759 bytes .../NondetAssume2/NondetAssume2.java | 17 ++++++++++ regression/cbmc-java/NondetAssume2/test.desc | 6 ++++ .../NondetBoolean/NondetBoolean.class | Bin 0 -> 659 bytes .../NondetBoolean/NondetBoolean.java | 10 ++++++ regression/cbmc-java/NondetBoolean/test.desc | 6 ++++ .../cbmc-java/NondetByte/NondetByte.class | Bin 0 -> 657 bytes .../cbmc-java/NondetByte/NondetByte.java | 10 ++++++ regression/cbmc-java/NondetByte/test.desc | 6 ++++ .../NondetCastToObject.class | Bin 0 -> 779 bytes .../NondetCastToObject.java | 11 +++++++ .../cbmc-java/NondetCastToObject/test.desc | 6 ++++ .../cbmc-java/NondetChar/NondetChar.class | Bin 0 -> 657 bytes .../cbmc-java/NondetChar/NondetChar.java | 10 ++++++ regression/cbmc-java/NondetChar/test.desc | 6 ++++ .../cbmc-java/NondetDirectFromMethod/A.class | Bin 0 -> 265 bytes .../NondetDirectFromMethod.class | Bin 0 -> 808 bytes .../NondetDirectFromMethod.java | 19 +++++++++++ .../NondetDirectFromMethod/test.desc | 6 ++++ .../cbmc-java/NondetDouble/NondetDouble.class | Bin 0 -> 667 bytes .../cbmc-java/NondetDouble/NondetDouble.java | 10 ++++++ regression/cbmc-java/NondetDouble/test.desc | 6 ++++ .../cbmc-java/NondetFloat/NondetFloat.class | Bin 0 -> 663 bytes .../cbmc-java/NondetFloat/NondetFloat.java | 10 ++++++ regression/cbmc-java/NondetFloat/test.desc | 6 ++++ .../cbmc-java/NondetGenericArray/A.class | Bin 0 -> 287 bytes .../cbmc-java/NondetGenericArray/B.class | Bin 0 -> 263 bytes .../cbmc-java/NondetGenericArray/C.class | Bin 0 -> 263 bytes .../NondetGenericArray.class | Bin 0 -> 953 bytes .../NondetGenericArray.java | 30 ++++++++++++++++++ .../cbmc-java/NondetGenericArray/test.desc | 6 ++++ .../cbmc-java/NondetGenericRecursive/A.class | Bin 0 -> 249 bytes .../cbmc-java/NondetGenericRecursive/B.class | Bin 0 -> 267 bytes .../cbmc-java/NondetGenericRecursive/C.class | Bin 0 -> 267 bytes .../NondetGenericRecursive.class | Bin 0 -> 731 bytes .../NondetGenericRecursive.java | 24 ++++++++++++++ .../NondetGenericRecursive/test.desc | 6 ++++ .../cbmc-java/NondetGenericRecursive2/A.class | Bin 0 -> 250 bytes .../cbmc-java/NondetGenericRecursive2/B.class | Bin 0 -> 268 bytes .../cbmc-java/NondetGenericRecursive2/C.class | Bin 0 -> 268 bytes .../NondetGenericRecursive2.class | Bin 0 -> 879 bytes .../NondetGenericRecursive2.java | 27 ++++++++++++++++ .../NondetGenericRecursive2/test.desc | 6 ++++ .../cbmc-java/NondetGenericWithNull/B.class | Bin 0 -> 264 bytes .../NondetGenericWithNull.class | Bin 0 -> 772 bytes .../NondetGenericWithNull.java | 13 ++++++++ .../cbmc-java/NondetGenericWithNull/test.desc | 6 ++++ .../NondetGenericWithoutNull/B.class | Bin 0 -> 267 bytes .../NondetGenericWithoutNull.class | Bin 0 -> 740 bytes .../NondetGenericWithoutNull.java | 12 +++++++ .../NondetGenericWithoutNull/test.desc | 6 ++++ .../cbmc-java/NondetInt/NondetInt.class | Bin 0 -> 653 bytes regression/cbmc-java/NondetInt/NondetInt.java | 10 ++++++ regression/cbmc-java/NondetInt/test.desc | 6 ++++ .../cbmc-java/NondetLong/NondetLong.class | Bin 0 -> 659 bytes .../cbmc-java/NondetLong/NondetLong.java | 10 ++++++ regression/cbmc-java/NondetLong/test.desc | 6 ++++ .../cbmc-java/NondetShort/NondetShort.class | Bin 0 -> 661 bytes .../cbmc-java/NondetShort/NondetShort.java | 10 ++++++ regression/cbmc-java/NondetShort/test.desc | 6 ++++ 79 files changed, 438 insertions(+) create mode 100644 regression/cbmc-java/NondetArray/NondetArray.class create mode 100644 regression/cbmc-java/NondetArray/NondetArray.java create mode 100644 regression/cbmc-java/NondetArray/test.desc create mode 100644 regression/cbmc-java/NondetArray2/NondetArray2.class create mode 100644 regression/cbmc-java/NondetArray2/NondetArray2.java create mode 100644 regression/cbmc-java/NondetArray2/test.desc create mode 100644 regression/cbmc-java/NondetArray3/NondetArray3.class create mode 100644 regression/cbmc-java/NondetArray3/NondetArray3.java create mode 100644 regression/cbmc-java/NondetArray3/test.desc create mode 100644 regression/cbmc-java/NondetArray4/NondetArray4.class create mode 100644 regression/cbmc-java/NondetArray4/NondetArray4.java create mode 100644 regression/cbmc-java/NondetArray4/test.desc create mode 100644 regression/cbmc-java/NondetAssume1/NondetAssume1.class create mode 100644 regression/cbmc-java/NondetAssume1/NondetAssume1.java create mode 100644 regression/cbmc-java/NondetAssume1/test.desc create mode 100644 regression/cbmc-java/NondetAssume2/A.class create mode 100644 regression/cbmc-java/NondetAssume2/B.class create mode 100644 regression/cbmc-java/NondetAssume2/C.class create mode 100644 regression/cbmc-java/NondetAssume2/NondetAssume2.class create mode 100644 regression/cbmc-java/NondetAssume2/NondetAssume2.java create mode 100644 regression/cbmc-java/NondetAssume2/test.desc create mode 100644 regression/cbmc-java/NondetBoolean/NondetBoolean.class create mode 100644 regression/cbmc-java/NondetBoolean/NondetBoolean.java create mode 100644 regression/cbmc-java/NondetBoolean/test.desc create mode 100644 regression/cbmc-java/NondetByte/NondetByte.class create mode 100644 regression/cbmc-java/NondetByte/NondetByte.java create mode 100644 regression/cbmc-java/NondetByte/test.desc create mode 100644 regression/cbmc-java/NondetCastToObject/NondetCastToObject.class create mode 100644 regression/cbmc-java/NondetCastToObject/NondetCastToObject.java create mode 100644 regression/cbmc-java/NondetCastToObject/test.desc create mode 100644 regression/cbmc-java/NondetChar/NondetChar.class create mode 100644 regression/cbmc-java/NondetChar/NondetChar.java create mode 100644 regression/cbmc-java/NondetChar/test.desc create mode 100644 regression/cbmc-java/NondetDirectFromMethod/A.class create mode 100644 regression/cbmc-java/NondetDirectFromMethod/NondetDirectFromMethod.class create mode 100644 regression/cbmc-java/NondetDirectFromMethod/NondetDirectFromMethod.java create mode 100644 regression/cbmc-java/NondetDirectFromMethod/test.desc create mode 100644 regression/cbmc-java/NondetDouble/NondetDouble.class create mode 100644 regression/cbmc-java/NondetDouble/NondetDouble.java create mode 100644 regression/cbmc-java/NondetDouble/test.desc create mode 100644 regression/cbmc-java/NondetFloat/NondetFloat.class create mode 100644 regression/cbmc-java/NondetFloat/NondetFloat.java create mode 100644 regression/cbmc-java/NondetFloat/test.desc create mode 100644 regression/cbmc-java/NondetGenericArray/A.class create mode 100644 regression/cbmc-java/NondetGenericArray/B.class create mode 100644 regression/cbmc-java/NondetGenericArray/C.class create mode 100644 regression/cbmc-java/NondetGenericArray/NondetGenericArray.class create mode 100644 regression/cbmc-java/NondetGenericArray/NondetGenericArray.java create mode 100644 regression/cbmc-java/NondetGenericArray/test.desc create mode 100644 regression/cbmc-java/NondetGenericRecursive/A.class create mode 100644 regression/cbmc-java/NondetGenericRecursive/B.class create mode 100644 regression/cbmc-java/NondetGenericRecursive/C.class create mode 100644 regression/cbmc-java/NondetGenericRecursive/NondetGenericRecursive.class create mode 100644 regression/cbmc-java/NondetGenericRecursive/NondetGenericRecursive.java create mode 100644 regression/cbmc-java/NondetGenericRecursive/test.desc create mode 100644 regression/cbmc-java/NondetGenericRecursive2/A.class create mode 100644 regression/cbmc-java/NondetGenericRecursive2/B.class create mode 100644 regression/cbmc-java/NondetGenericRecursive2/C.class create mode 100644 regression/cbmc-java/NondetGenericRecursive2/NondetGenericRecursive2.class create mode 100644 regression/cbmc-java/NondetGenericRecursive2/NondetGenericRecursive2.java create mode 100644 regression/cbmc-java/NondetGenericRecursive2/test.desc create mode 100644 regression/cbmc-java/NondetGenericWithNull/B.class create mode 100644 regression/cbmc-java/NondetGenericWithNull/NondetGenericWithNull.class create mode 100644 regression/cbmc-java/NondetGenericWithNull/NondetGenericWithNull.java create mode 100644 regression/cbmc-java/NondetGenericWithNull/test.desc create mode 100644 regression/cbmc-java/NondetGenericWithoutNull/B.class create mode 100644 regression/cbmc-java/NondetGenericWithoutNull/NondetGenericWithoutNull.class create mode 100644 regression/cbmc-java/NondetGenericWithoutNull/NondetGenericWithoutNull.java create mode 100644 regression/cbmc-java/NondetGenericWithoutNull/test.desc create mode 100644 regression/cbmc-java/NondetInt/NondetInt.class create mode 100644 regression/cbmc-java/NondetInt/NondetInt.java create mode 100644 regression/cbmc-java/NondetInt/test.desc create mode 100644 regression/cbmc-java/NondetLong/NondetLong.class create mode 100644 regression/cbmc-java/NondetLong/NondetLong.java create mode 100644 regression/cbmc-java/NondetLong/test.desc create mode 100644 regression/cbmc-java/NondetShort/NondetShort.class create mode 100644 regression/cbmc-java/NondetShort/NondetShort.java create mode 100644 regression/cbmc-java/NondetShort/test.desc 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 0000000000000000000000000000000000000000..57858ac292f69439cc0e65d1d6c7b77fb150b7f8 GIT binary patch literal 722 zcmZvZ&2G~`6ot>kPR4bd=BI5)!ao#9K*F2us1Q|vl?g~iMU>UV9<>u(yBgb-c$K~Y zYe1q1q?R2L&x8=yPDm=j!k&9)?)~mLGe3WSJq56VfsG~fY+S@8j%DPArsZ$k4$zzp>aVP@@w#!i2RFO&_G8p~A4ud(21IbYLR3t~)!C2~- zc`-xFi+vI92(9vbwrQsODq*O3qc{p=x}~*v_kbV=LPbQ3#}gX;#+!&E;f5mGbDxhV z(odu!QYIpdeSQ(m8VeFMk_v0)bWnsv$+8_MS zQGLN2hIHEu?La0<%V4gFJf|5Q&{gl!({Oq_fHgX~3yKW-$Q&4!DROCLw3hFlfPJ8# zggX5z#ioG<#m=+3+xxVoVqMrm`~g&v;fT({|xIG+@V>r_$1z43MJ8OX78Ol_v4&1^YhQQBLH)lvtVJ&!WCTQ$XU3C@f4D{ z&T+$ni7}1|3zL}Qm}cl7cUmo>0_l6L$Fk*Yx}wg&HWB-yDDqz8%zqhHNqPRI0vL7s0Yp&b#sh>e6(iNBt#Du53HI zPRVt=th!>0TN(K!-4632)64A-23rtVzNrp_PXImTMN7Af2 zZb+2qN=Sp=PST1?*T^tf7cHqo{Tw-|6ohm@1sfQnS76Z-Vd-4Nl{}3WNdf9bUWqIt zYfK-4eIh4;H2uvus3AkXeVTwi^wSO)I4?e?Y)+A-uSooWR?!w`s>P#uU7I(uMpplb zp<>o3-!}_+^8k8d@x8(JPkw!dv4`Hm2XuXh`T7w2IGU@)b4TKSoc<~LEQ}K939?0k z{D|g8c&4FKJc%p@2`5c&BjdP-A>;^c3U`smFrm9d=Xq!+lwxueI5ZY5V*DG!8ESI* moXlKI6Ug)>50Kge*Y}}oUts*JO4QXr!d{BB8=*}CqkjQF8L<8U literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..e07d736d747d1f5db68cd8c7326775ef18db25e5 GIT binary patch literal 935 zcmZuv%T5$Q6g@TFJvB59!vF)rLqSC4A&fkNQ9&iB32_`B7>u}TW;)Q=bd#EH68HXu zEZwkH6EK>fI}?AwAMg`g81VEkG9tn=sLD;v5Dfat%n~ zyu_dhBQ9RRMTtu$hA=EKBG5KyS1OJQ-N3KhaVz$!=adD+ia>JK_1*BMfHpL|ETAt0 zWk(=gaDAs3ZLT`%Y1}N(S_n$Ew`?mn-q(tHxb9X2nhV9iFFWD9QueE<8${W(U7z?a zZ!T=u+jicw{k8m}A3AG}iW^)%tUZ&fd(B!Sdy$*WN| zmx4%@oO^CeFmsy2czmgaCNxWoTDXic3yrV@a&IGsF%zxIWPk#| zTO?x_rSwq71UX$}yhSFDDI;b%0-f~~vgjata;ou_xQ|ZcsG$c}iO@~XJv{G&{u^Bq z+7UsM61_}Cyy(U+bY}>4=0xap)dC>Xn%YCd4y3*dUHbt2U&mr>0}1PP?CV)>66pH_ DFp{_m literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..dbe5532ccfb0e88fb8371545e5b337bd776ef8f7 GIT binary patch literal 806 zcmZWmO-~b16g_V~I;9NsgNiLG2%@&AbkmhqBB`2?)MA3ch^y)Jr3?-;z zt2x}nEep2==2o33k}CGXAbRXYPS2Np0kJ2LX?cMcZwTnM`mTV{4*OCd-|+(39Uk_i zdXY2>lscj7_`8nslKZ%5#QR<(Fx%;dL0`t3N;z+v56E)pcmeqx#ulT;a9Q?(nC<1) zodf6CY4}bsXlwty+lm$;=J{Q%!Z8_ z3pE>ctl7w6TA(tSvU%qIiBh2wurCr=xMSlk?gd zenP)*e1vg=Le=<%>2EM!og(uiVb)XT1#*L;G-P2=T85%#Ib)fu$+YH(aXd|xI?%6|()mLUF;#pB U82{T&=uBw#qvUa}@uFezA4iRp3IG5A literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..bcdca197547fabfd5126639491b8e34bc80dbaba GIT binary patch literal 722 zcmZWnO>fgc5PchO;@EXan$i#&J_@9e7KDY=8xblBAXO@*Qc)#x+t{nJ#j&fkQ}J7R zfg5K)q7{|Oo!^8IvyPRj;;^%`J2UUio88}kf1U$a$0HXGmRxjj!_dPs7&x4COhPH|Nk%;$w;+<-Hsdb`> z?h=fRRS#=;$k4bbc{4hYK}Lf~^u8Y)>f}gjf3TD93{ITu*^DWJ=0XZ8G(XZt%6daH zr}_odAfgyUE0n3yGMqI-nzIQ72w;e1dK!lwjWyb)eex_?Bn=E#$n$Auw3pXTz`l}G zLY-_SzqHUG-=Ypgf)KP&>|f$TpTq?65wB$>Sa<*rC2pd{?#|54 ze%_zw3%~?j3mRG`+9o;#x^b)s#!Q7OofEYFU{BB&(LoYgt_tNkyLd9*2`^x!>qfo^ z_99j}|BHHhQVEZ`&Xiznqb&C2QWf@f6dq*iBuRFW!~?8UnAu$OUU~Qc-5HcnFTI#2G0!u735j!G5V%4x9_S2d$Qf<;7?`0*i@Bki4+@XuP^PMyI zo;&Z)^95jnu8lGr3vCM>0trIdTTBV&Ohqc2v+NHJ1Y;E+CBgAjBsclhm&soEAv;|! z4n%kmiPE|-jqI#aowVd6dl%tAG$p@$Ox40oT3;?EETsSd literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NondetAssume2/C.class b/regression/cbmc-java/NondetAssume2/C.class new file mode 100644 index 0000000000000000000000000000000000000000..bbf6b9b7eaefdf0ebb7df435b7e489815784f53e GIT binary patch literal 258 zcmXX=%MQU%5IsY+)Y}(WVxfuH5eZGK8WzOoBZm_WH0=Xm7W&| zB0PvhY5o_D?5t9qDSXi`h9XCweOzct-1>7=m+d>|T zChk~R#)^qmf%>u=MN-Eq45BA0a)-Vg35bC}ep3Z1ek71>wRZ)KZa9(xm7WS@e=;6Q z{W2*QsP#h6^>xw@++LT7@=ok}Z=Sn{ zX(tH_6gEA7Hrv_>C)$(GR66Mb*!qEc&ct0CEwl;SwXuedjS_5uW>Vq!Zm{Q& zz*OW@twYVJ7obesvvD8m0@d@D7sCVT#oSP+_Z;s~heuL7-R;y0%mt~iS1R7`PkdjX z(Q5bpZKk|D*GuUX-Wnupten?$eZC1SjAW#=9Gy|*LgEP@xc32;csYw_71d@Uie8o< zMT1!M99lt}TRVYxPbY&a|M@go#5{d_T7VkrjDW^j^IKMDm{~nV<~#4v`2o{-2P1n5 z;{$TXsC0g!^ac6XCosPy=-Cv#27`VXCXwo-vBGRJX<>>so5Wk<5_1BV`Bp;qH!3EY oTcSZtSI$Umr1XIKTHzCl$1?^Wk^5gwf|EnW-byrIWst$Ozfjqa#Q*>R literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..0b4ed3f79156e27d3d0dfb59472e18e7af84d0cb GIT binary patch literal 659 zcmZWn%TC)s6g?9=u`z~(P(sS9yaip<8+IT>N!t|#BpwpoP3#d27!MjdsJ{X~z#5PM zQK{_vO$c$v3ZV#D<9lc3+;i@^_P?k5zW^36>%m3c!$%Btp@d-vBOYwj9gKPy!zTyh z4E@tQO@+>+O44sK<;_?`4D1&}X-OtBTV}B4=64zFhKdA3c}*r_y>;9adfR{*s%t9b z@h;cW?AwQSb|6!OUROyZvQ?#G!IMRzIp#7Uf!_>0TNw|Je)5xcjk^@aZAouSwR9+c z$XwtJ$CpEX%6)XhcQD~&5>r09;4#$AMG*63Klu7$>ATiSlhPXo2h%=gFvU=LE!k)u ziZG*jD7_zqCt95f9W*xcNCe6MHu90sgvzhwjhM#BP>Vz=wTL+K$YgqN*V$Q=n7RFG+eFqOb*qC$h(8D5@ z96TaSt%y9Ax=>k~zg4;DCNd__KB2auQdPVnSgX%>33fY+B_ZgjRBrW-yHbBPU_zsl zMIzZ1TA6eI(k>2FPVhThSsKe?^J^j3nd4Zfl-bYNHVOB(3lV+!AWr&4?nadKdwSbh zPe<~-G97{u$;%^gDtwH?cktN9GFE(y!6URxB1}Yj5WX2K^iJzc6TDHmgC{2-Dnuat`poJDl8o-y{s8CUWQwT_{ipXtaui7n+U9IgtOkaRA zAkhjWxPinoA;hc`l0!Inc6N8>`=lhH76%VvvnTLLKO0 zhI&8td3eZ`)cfh7l^)B4q0t}2Q6SPDPtt?<)#ya{>0`nga~Tm!th-P68TUdS9eK0+ zrTvuq?_ToL94*&b+V#V!9%nz!lrLUL&Az%w@JJ)NaIs|Lu8VuP@1l*43kMa3)|~I@ zKj+VtiWO;D#ImvNqKgL%wRzt}C(SNaN1lJG;xnPV-s^m2xDw@--^lcMkcA-)q22kP z$s!Ft8Zzl$rFAYmf%Y zJX#s8h3yNl50n_FQY_|&CTf(slL9QGPCH;_)|^tcK_{D+F#6peu&wv7%uARbVV$Ge z{fWv~6y9E-_+3MrIdmNsPFw4!keFx)+D_!?~tT>lG)G@1VZ literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..4d05d0b75dd80a169aae2e690cb7c767f0671844 GIT binary patch literal 657 zcmZWnT~E|d5IwW)ZcC|jS#((t1r+)4!M^YYA)2aBE0~}p@OHPofs3Ujw_U|L}*#UB}MatmO#X&_c#Zmvp|dKwsj92Pe}IcN&oQL6F~iS&#yw!;rnhKQg&EGbSv3Hr fTa6!ZuHe{TU|Zi|{XeUrsH5h;G#kzGp@z;sAX0gW literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..6d3758b230af9b1e55332b653b5f147e7ef1bce6 GIT binary patch literal 265 zcmXX=yKcfj5S+y?;+XJgX;K0OZqfxsLLj6_4iq5zvwaGOj8D28`L9%wQse{pD8wF6 z?C#9$?BjI)`v>rXUJMWI2%QLB0tt?HLO4;ivTp=$Fx(RSnJy)vovB(bkB3~EjmRrj zdYLXnwG~D=eiwbaQ(ruqOrmK9OBe)|TV5P|{JTh{N IT36T81-_0i*#H0l literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NondetDirectFromMethod/NondetDirectFromMethod.class b/regression/cbmc-java/NondetDirectFromMethod/NondetDirectFromMethod.class new file mode 100644 index 0000000000000000000000000000000000000000..6dafdc80b07ffff6f12571880630e21e02bc602f GIT binary patch literal 808 zcmZuuO>fgc5Ph3C+0=Dunl>R2K1y342?z_RH!4Jw(o+%;MMdHP*9Jg!~ z(coCKv5pOn+YHMaB95g_R20VBDi*^)`V4HJp}3_&l{{w1H(PrQRyXn`!(vZ`a*&RP zQol6K43%EwiC|A?W$u%rl^m#;q23!rp)ZqdrKOkb=xE%R$wA~lVknQZ?1fBH9jb8D zVJI|Py$=1d#zKV*3%iN%-t@)MgtN5e1rtg3Zj@?I?kFRmaq$}u4#lx>uz*V(cO2YB zlYDg?%)@c8f-0#q9d01Pk=yw@gr{0ZnxS?vCr8Uc8}~^54Et<&Nakpiksi6;k&cd~ zcDv8B$gmV<6L_V_cbW{+AYfP_qyOT`_u{P94QMSS!^&tpl<6#H#S)e%cm6b>f@QkF%!Mij{E(sn^H0cq zNB$k9=i$ydIG@66)3^K7ZQ!*Juuf2EpQ7*s^IuSWeFpx`h{+weCdq}ffC>n3Q|!Ky>0AO+2VSuwNvp=5d8z3 z0jaG(f;+znA!e;Kjl^MgX6NyJ^Z5Pu`%eJtSPK!L7veIm%%P5}KCXrE(DQLU#0@O_ zxJg)85k(0meo8$eFG_P$kp)=Hp z$hL)1_CIlYS5evA;d5bJe`v+Z@bC#wg j>lHoF?$nRrAHnxN!*jpE{l8laQG*jbwliJgkAv<%3fFzr literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..9b26f72c773ab21696c86a2784ef8a1711bd2201 GIT binary patch literal 663 zcmZWnO;6iE5PfSqv2k4TL4gF?LMd%2hx)>;sG>^ADbPw(Ah>Pp6|NeV(3t$CHK0LI1%wTp5Wjt~5)Q5wXi)TLO zFz@0y!^9%bGNE&+((I$mcrOt#1KVRLugX;B?-}f+H`@$OTg8H*+Lfu;>>u`o{$h$5 z8eJ9fWSeVg&Vx%Q|0*+vN8L@8#v<<|is$c$%>WRuYppfykwl4s;g%U59M6j&IiZ@IX%QKi_FQUPkHllRaVf_JFe z?z7f(4Fpj${H7&!R%Q;vT@GPOO2# z>zUcv*}eb&{s9=E?W2sqL(@ZxK!Q+?CPRWdQd$*broH}_;LP%!Bm|Mta(ViRrP+u$ zW2GJCiO9CXD9hiXQykRMCQUiXU*{*2$hori&NA0KSuCWMMkNzt#N|5`XHka>kM~ar zP0Pbf=zX|~Q<)U#qQpl6#Lq$Hjd*~SDzlJ(+pB!tKvxDO)VR7&u?nAY{bj%hBOBCs Gx;`J~t}e*{ literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NondetGenericArray/C.class b/regression/cbmc-java/NondetGenericArray/C.class new file mode 100644 index 0000000000000000000000000000000000000000..27903564a63e3a08c332282492d21f5c9f1fa959 GIT binary patch literal 263 zcmXX=yN<#z5S)dOK!D@X&{6^gY3M*mcaflppa9W3!2+Y;NG2fhSyU%o!3XeBC)PmW z^~~(->^}bg?f^z;`zWH}q3NMTpqNmMe#QiMqO{7VOndze!3ndiBs3zW<>GvdrCEzO zWu+ZuiAXoXD9b;hlke5ZCWV~jud=gACoa+e literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NondetGenericArray/NondetGenericArray.class b/regression/cbmc-java/NondetGenericArray/NondetGenericArray.class new file mode 100644 index 0000000000000000000000000000000000000000..76c6f43ab08f3eaa6fce6ec960d629d4d1acbb07 GIT binary patch literal 953 zcmZWn+fGwK6kXGnPJ4QQLb;RzqKI0mQZIM~wWVG{tZ0J4h)>hg2@D?2A=6V56a5i> zz-N^R(L{aH#E~QU}WS8h2Gg)LdC-V5m1JxzptIObl^rTi!S!?lX zj(Tkh<TLW0jep5U0zB1PhcXpiF5Zl5=8hso^ z8y9eqdRJ^*!eyJ}xx#VP#x-2$xMAZa=4|w!mmzClMOS!h#qxg*?rH67;?#Kw$GnYO zAU)CtxW}~(=>(*ruh)vsmiD)$E>@m|mZ8TB$v;!U`cl(%Nsjz<^(dIw$LR^0o5U@a zUo}#*n$cx}PS^r1VWP5$%2cAffP{^_SfsZ&=v8s42g6WZHk6k2HXqV8Xwm__;VS)$ z6nzwcrL#r>@}jgzHV|X-iewqtuEHMJJ8~k(&>jzy{TLwM{#SrO3{jN8a2x!Kstx$f zJ|f=`eOUMo9(#*ebRV(8F1n6{yNGvYcEJxN-y^YuL4&2@A4q*h^7$UDuVFsh$`jn<_@AK1XX1)^GH3jFwn;iKR;{ pQ)0OswHs@5oeh}+ef_DAuyGTdyCvPg=Fj)?BzW)x_@Sh; z)q$CL@5dXMpWm-<0FRg?2yhwWDn>?#o{Tl^GatUK43o*xdXS1Cda2{b26 zyw59Tclld+VBO*t19{IENlQ?6Br2Ef$?*OY^dVw^SY~vF0WL(Re*uh;h$D>8sq_Sy CYA+}N literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NondetGenericRecursive/B.class b/regression/cbmc-java/NondetGenericRecursive/B.class new file mode 100644 index 0000000000000000000000000000000000000000..8a18024f50bec9a3a4833f0bba7ce327a7d3c43f GIT binary patch literal 267 zcmXX=F;2rk5S)!28%)5#Ee$15;3i!V5{U$jWh6l9&zBXPWzN#Y&cCRTD0n~~g|Zi1 z?C#9$>}Yp?KfeHG$PxrdV@zY56G#z);$cpR?u<3vz0j-c6(L-kR$tPu!6u(uC)4VX=e!r^hmg^;3c1EvRH|}K4{CH4jl^{eU zKV*b~=V__zE`2QytZR(Xl1BlO3edSCIS}PWSSr)+IuDY^q45_Zf`-V4J~o<3KXhJr&7Ob}*6pb>7U- z@?u|v+d`{6K1-VEu1Xj>-YAX&nLd?~)XIM){Y)onD(?~Aflv`K`9$Ekl$hU2g}?t? z92O8HnxVSshi4+JtvJ)Ze4=v7-o>bQ_rz4#urbeZ%f@Z26TWN1!W>D-i%uw_9p~ZS zjUQ_rYlim4a2$Ob0}L4&=d&*+d(uzo-D17t_=h^4O6|BW3(K$&73;oH>Fy{CLx!dP z!25TYcCDZ1+>j1H8UmRpErXdhdW|%r0=@nit8~8_-IX;u`8MPk^wFXqPVyYGjBI&$ z4ECO!66*A?6v-wU2m7NFVUpHMvlH{ZcDKEnK8a1K&N N$$pTp)uo_>mETmHlY#&M literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..5628564f73de76f1351bb4a729940bdd352fce99 GIT binary patch literal 250 zcmXYrPfNo<5XIj#|7?u5c=pg^?ZJR}Qwl}UOQ@iw_sw>&8{!7Gn|?1(LJxibKa@CI z9hjN-e!PMC{yBUBxWza}gtH9i8AgQk-dN-3glKxTCd3cjh6$s}SYGz;HM^CnTOk)! zr&YUF&IJDtW4|>!Ijt6Vg#5MZo#saq;+M)!3mo^P%jwO0jVBm`Oz z#=)1ZvTx;c-LUqUU?Bg6B54WAPDPcn14(9|pbrrPWHQqujBp~l_zPf&TpZ!_m@0k& D)om|Z literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NondetGenericRecursive2/B.class b/regression/cbmc-java/NondetGenericRecursive2/B.class new file mode 100644 index 0000000000000000000000000000000000000000..606067dcdb8b8be87b1a342f717de25a96a891fc GIT binary patch literal 268 zcmXX=!A`hx61^V)NQhC`(K<)Jn#X2lyMe& zn3?z9ym^_Q-|qu}JB(9wF-$N@a6uqN=;jYILOeIt_ETXsgjvaa3EG<Q|xn4=X~DRcj{nb7OhlYzuZD zswhPn=9O0EN;%{CMGWdMv-3%rB*pJl<228Vx8KbxyXN|hEjy!^tQ)s8dmcY+)LtbB z5y=x7Vc>aMD*Kr(iVf=;BedjGfTRL+E=UeUxe}Jj^t;aE59nJ!3tj2qNlXw6PR<7O L1o@!rlk4UPmB%o_ literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NondetGenericRecursive2/NondetGenericRecursive2.class b/regression/cbmc-java/NondetGenericRecursive2/NondetGenericRecursive2.class new file mode 100644 index 0000000000000000000000000000000000000000..ed328ac8e04844934c5d2ce66417ec021e5b92e6 GIT binary patch literal 879 zcmZ`%OHUI~6#h3fy?f<_F+?xxclxH!y^J5zoPOE<1n zB198)rHQ}E7|*Sx7z~Ru=W);DJKvd~zdwBeFpql{Y)o1>hbe*cMo*^^$AvUza4`)F zmjo_bNMTZ-V4;YTz!k#Kj1z`ZM=J2chbnX$o@^4RPDm~&UqufH@j`K(kf;VtNyyZc zFIQXJ4XIz4WWr!Aa2;>m(aQLpU?SR7Az{3>8u(2aJ(j-I%6%@~mJZdfoV(8rw;kp4 zD3>SHsvPKBiyZg$inG)1!AlTQ3$E8eVXXx%?aF0kW=@>ac6Q6zb!=pi6}W2S8fJMw z)kYcDZQQ_|z)hREx@Dse{e+xJFME!^QC>V^;gQyXCXAgjLEyHHJGe{89v44tY)Lm_ zG6TI)c6W5JD|Na0tgQ+Cew%}rD%xCac^+Z7P^_IS=KYg=iPko6mnhT?|F`WGaf+4FY literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..80c9824e5191d58d4cea7551e4470546b0b1f6be GIT binary patch literal 264 zcmXX=yKcfj5S+!v4(4SjQ>6roxJd`104Y%<%M^)7eKsdJbU91roc~INM8OB-qY!(9 zVs~d|XCHr;(;2`Eh7mmUL&PBl1QHzYgkYwOvU7qr8m|fdvfM~QKUGF%^>;3-Pmya@ zhG|&{y%v>n{4V--rw%-tE~bR&qpYh!zA9&b%u2J7_DvdDsp3o7T~=%Tyca*Bg8(5P zUl3x)6D`a(S>=0KSUjP@UjoG8qj^U>z{&%&gsbZ{Cr8jPg9cihgPZ6fV%+&Rpv}lF I>fT(vD{ZJRegFUf literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NondetGenericWithNull/NondetGenericWithNull.class b/regression/cbmc-java/NondetGenericWithNull/NondetGenericWithNull.class new file mode 100644 index 0000000000000000000000000000000000000000..0b52a47bd0a58b584da059f5eddecf2f327ffbd8 GIT binary patch literal 772 zcmZuuOK;Oa5dJoHvWe@qshhS*DNvw55+J_xMuni^A%qD?MMdn@{QdbWfK9j-EUZ~Lj|&_ZD=1@~KEB#2FHti5$+1Dvim4$rUxovSn+ys6v*_EjHFinOO+n<24Q%c;Esffh^SBa-Zmv> zcT(ZMekzW01QO0r-txnd25ToCXkR{58RP1ipq)c;B5cfJj^nzGCRzl)ZDR&DLp>|H zp@{a~dt<*3w2rlnHf}I1oe9Zt)5a}y7^>6$XZ=Izr}T5N-go_D9iK?;cAw`b!(5ab z9y?{IHCx`l&19DeT94^Jr?qZKqhMGLWTLbTCOYY3(g77{4trRqaauHHR;_2wC^Be~ zX%H4gE}e|dV*3>AEd>QsX)pavVu50N6gya?TN$-Ub4stXX7>{c-(fs?2Xlz|_7BW_ zLGjfoO5gH~)BXTHoF+3GBd2j-Qd|KijSbS*A+j+gr;#jSnd&R~o5C+NIO;W0(3mLL j%=v)@r~DC>A-MSlrtu!;|5h@TA`151%{33>Kt$uhkTRanzciT3Vd{N$hn_E*$_bQESRQ0Lc+O{rlwVrOoR`d`d z=KBl6$n#VS^Odg3jjSB*(BVe`;t0{bARb`lido9l_qvaJ(2hX|*PNrX7$9NX`#0c* Kkzdq5y9OtR#xU6c literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NondetGenericWithoutNull/NondetGenericWithoutNull.class b/regression/cbmc-java/NondetGenericWithoutNull/NondetGenericWithoutNull.class new file mode 100644 index 0000000000000000000000000000000000000000..c369eae01fc067d724c1b3f4ba974f4e798d47ec GIT binary patch literal 740 zcmZ`%%Wl&^6g?9=nZ$LQM@vak3T-Kn1PO1tqe9T|SP(*`q9U@J*rRreYgc2tAJZRT z4M-G$1niLbCWN?S(iDNZu;)I{xo7VD`1R=vfDPPsP{EReD_G{ZS^>v3jui(*EOD$l zSi^OWb%yzMkt9;5DvpweDiPyQ1`KS(P})?HO7AgPo$fA!-H!vwP#vg94zt6t)Gtgi zLt_y8BHR^P8GjPA(|wgNvUBmSLgO z9sJu*lB?&jen^{OSPW#Mv<#*L(xs#sC1?#Jtk5DWv|v_i8cAeX^pRRH%#r2M$>=Qh zPQl)iQ9zacr9VN`$aW`o9S!ozn4dO}sM<8QKcesr*3);ePf+cB$INFGU!9`#)gW3q z;#^K_-j#zE4RVIe32yCZmnr}N literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..0af2adcb60811e4da89d1fc4900955c147598059 GIT binary patch literal 653 zcmZWmO;6iE5PcInvE!H|gf;{U<+CmAp}uefRjtxiLJA)e1qp5&dj$)|Mr#N0SKtry z+*T@8E4BCjrmE_!m4riOjc0b}&6_u~zyE&!31A&-9$d_Ln8l+iDwuOH@4?25gU22g zu;^fkFtsYOOzK>vN%mG{q94nMK*xm2rb<-)ieRlhKP1@QG?IiyPbG3^aM73gg8>s- zy)+c@q0q{lhnIGKsxm^Yx05E3%(s$!gDEbAN|^kbZHq9mpNsH(TU-un+|4i^w)FPX zfez(+Wg67S952trmGDu6?_k--3RZno;So9}5yT=n3Eqsxd8c)%3Dt46gC{Q0IT8xU|sV*gzS8CMMatXpM^x7;SRX z-%#544C@w+*&Eb;z&^S|`In)y3c7mH)#2B7(PkYZS{qaRJz(5JHg5U{Z7MJ$ed|R7 hV6s*D3g;G%{SmhH1=jys4MiCx|FxNDnhzy({sAPYctrpJ literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..27a693dee6ecb161b060f2971d1277c321b4ac0d GIT binary patch literal 659 zcmZWmOK;Oa5dOw?V#hVjqqHPEN`b!MfG@pK@lb#R3I(aCh~75#Ds1a|tF=?{L%7gC zz!{Jz0txQ?CWM%^(&WHlc4lY4`M#Oi-+#aV1h9q85CM82F5^lAbzJpvErf@jkL3{8 zvEt(fVPRDig*2todGS~kVwlO4K>LLHw#rp`pWtrZ-XnN@ok~J;pmMo0J{n5%%7O`< zflfrWCycW9NzyCds)7&=c66S~a-j3kJ?1zPDrfe0Y|jW6c1w{QJ{QN6qF_78CYs@{ z9-BlyRaT)nBe{DZPDF$`L_TgtxP{dS4TOZQeTXxWkK#w?13fWD8$viM_pugX9UFw! z4F6(yAd`|;q0J~xj*UK%ChotiJXhz_3940a-_2QVKjZZgmQq}ZI&aKjb{MwfTNf_v9H}Z1AXGa!91V!D(Rxhv4t`KEwtGO=uC@W^OriD z>wSas;4|D)w3i$2KVa?$yfdS#Vk!l kwkmm`-Kl?te+u9G2+#cj_y2A!MGa2$(9U#;FAlo@0PQ+@mH+?% literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..32e0868de3ed525ffab450275ba48c87d4ef40ca GIT binary patch literal 661 zcmZWn%Wl&^6g?9=vFn&7O(9Lot3ZLm0&lu&g+KvTp&$h+wY!NuYNxn%HFhd~h5i6* zK%xjF*z-*YamGrTO2``DJ9E!D_c8PP@AsboHn1MR$8vxbT%AJ$*F0Pg;9}XsjQ}^X z>fx5a;+iZ9WlEiA#WP*VQK}LFu_w^j(wQzF3pnc!b_Cpho+yFVKxb-ud^A$#jRgyI z26-&g9ci@PPY&JkKoA65gQd4-ipOWf4Z`v>}Fd-VVS literal 0 HcmV?d00001 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 From f85494b07d4610767a55aa65ac9ad39690669de0 Mon Sep 17 00:00:00 2001 From: reuk Date: Tue, 28 Mar 2017 11:18:41 +0100 Subject: [PATCH 3/7] Add remove_java_nondet Use specialised member functions instead of `get` Fix indentation Remove insert_before --- src/cbmc/cbmc_parse_options.cpp | 16 ++ src/goto-programs/Makefile | 1 + src/goto-programs/remove_java_nondet.cpp | 330 +++++++++++++++++++++++ src/goto-programs/remove_java_nondet.h | 39 +++ 4 files changed, 386 insertions(+) create mode 100644 src/goto-programs/remove_java_nondet.cpp create mode 100644 src/goto-programs/remove_java_nondet.h diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 1619143ce6c..9d36e749cf9 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -41,6 +41,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -53,6 +54,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 +924,19 @@ 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; + remove_java_nondet( + ui_message_handler, + symbol_table, + max_nondet_array_length, + goto_functions); + // 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..da3e3e63628 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -25,6 +25,7 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \ remove_const_function_pointers.cpp \ system_library_symbols.cpp \ string_refine_preprocess.cpp \ + remove_java_nondet.cpp \ # Empty last line INCLUDES= -I .. diff --git a/src/goto-programs/remove_java_nondet.cpp b/src/goto-programs/remove_java_nondet.cpp new file mode 100644 index 00000000000..86962fddc64 --- /dev/null +++ b/src/goto-programs/remove_java_nondet.cpp @@ -0,0 +1,330 @@ +/*******************************************************************\ + +Module: Remove Java Nondet expressions + +Author: Reuben Thomas, reuben.thomas@diffblue.com + +\*******************************************************************/ + +#include "goto-programs/remove_java_nondet.h" +#include "goto-programs/goto_convert.h" +#include "goto-programs/goto_model.h" + +#include "java_bytecode/java_object_factory.h" + +#include "util/irep_ids.h" + +#include +#include + +/*******************************************************************\ + + Struct: nondet_instruction_infot + + Purpose: Hold information about a nondet instruction invocation. + +\*******************************************************************/ + +struct nondet_instruction_infot final +{ + bool is_nondet_instruction; + bool is_never_null; +}; + +/*******************************************************************\ + +Function: is_nondet_returning_object + + Inputs: + function_call: A function call expression. + + Outputs: Whether the function has a nondet signature, and whether the nondet + item may be null. + + + Purpose: Find whether the supplied function call has a recognised 'nondet' + library signature. If so, specify whether the function call is + expected to return non-null. + +\*******************************************************************/ + +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()); + std::smatch match_results; + if(!std::regex_match( + function_name, + match_results, + std::regex(".*org\\.cprover\\.CProver\\.nondetWith(out)?Null.*"))) + { + return {false, false}; + } + + return {true, match_results[1].matched}; +} + +/*******************************************************************\ + +Function: get_nondet_instruction_info + + Inputs: + instr: A goto program instruction. + + Outputs: Whether the instruction is a function with a nondet signature, and + whether the nondet item may be null. + + Purpose: Return whether the instruction has a recognised 'nondet' library + signature. + +\*******************************************************************/ + +static nondet_instruction_infot get_nondet_instruction_info( + const goto_programt::targett &instr) +{ + if(!(instr->is_function_call() && instr->code.id()==ID_code)) + { + return {false, false}; + } + const auto &code=to_code(instr->code); + if(code.get_statement()!=ID_function_call) + { + return {false, false}; + } + 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 dstringt& 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 dstringt& 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 dstringt &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: process_target + + Inputs: + message_handler: Handles logging. + symbol_table: The table of known symbols. + max_nondet_array_length: Max length of arrays in new nondet objects. + instructions: The list of all instructions. + instr: The instruction to check. + + 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::targett process_target( + message_handlert &message_handler, + symbol_tablet &symbol_table, + const size_t max_nondet_array_length, + goto_programt &prog, + const goto_programt::targett &instr) +{ + // Check whether this is our nondet library method, and return if not + const auto instr_info=get_nondet_instruction_info(instr); + const auto next_instr=std::next(instr); + if(!instr_info.is_nondet_instruction) + { + 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=prog.instructions; + const auto end=std::end(instructions); + + // 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=instr->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= + instructions.erase(instr, after_matching_assignment); + + // Generate nondet init code + code_blockt init_code; + gen_nondet_init( + nondet_var, + init_code, + symbol_table, + source_loc, + false, + true, + instr_info.is_never_null, + 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 + prog.destructive_insert(after_erased, new_instructions); + prog.update(); + + return after_erased; +} + +/*******************************************************************\ + +Function: remove_java_nondet + + Inputs: + message_handler: Object which prints messages. + symbol_table: The list of known symbols. + max_nondet_array_length: The maximum length of new nondet arrays. + goto_program: The program to modify. + + Purpose: Modify a goto_programt to replace 'nondet' library functions with + CBMC-native nondet expressions. + +\*******************************************************************/ + +static void remove_java_nondet( + message_handlert &message_handler, + symbol_tablet &symbol_table, + const size_t max_nondet_array_length, + goto_programt &goto_program) +{ + // Check each instruction. + // `process_target` may modify the list in place, and returns the next + // iterator to look at. + for(auto instruction_iterator=std::begin(goto_program.instructions), + end=std::end(goto_program.instructions); + instruction_iterator!=end; + instruction_iterator=process_target( + message_handler, + symbol_table, + max_nondet_array_length, + goto_program, + instruction_iterator)) + { + // Loop body deliberately empty. + } +} + +void remove_java_nondet( + message_handlert &message_handler, + symbol_tablet &symbol_table, + const size_t max_nondet_array_length, + goto_functionst &goto_functions) +{ + for(auto &f : goto_functions.function_map) + { + remove_java_nondet( + message_handler, + symbol_table, + max_nondet_array_length, + f.second.body); + } + goto_functions.compute_location_numbers(); +} diff --git a/src/goto-programs/remove_java_nondet.h b/src/goto-programs/remove_java_nondet.h new file mode 100644 index 00000000000..0af514b5b11 --- /dev/null +++ b/src/goto-programs/remove_java_nondet.h @@ -0,0 +1,39 @@ +/*******************************************************************\ + +Module: Remove Java Nondet expressions + +Author: Reuben Thomas, reuben.thomas@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_JAVA_NONDET_H +#define CPROVER_GOTO_PROGRAMS_REMOVE_JAVA_NONDET_H + +#include // size_t + +class message_handlert; +class symbol_tablet; +class goto_functionst; + +/*******************************************************************\ + +Function: remove_java_nondet + + Inputs: + message_handler: Object which prints instructions. + symbol_table: The list of known symbols. + max_nondet_array_length: The maximum length of new nondet arrays. + goto_functions: The set of goto programs to modify. + + Purpose: Modify a goto_functionst to replace 'nondet' library functions with + CBMC-native nondet expressions. + +\*******************************************************************/ + +void remove_java_nondet( + message_handlert &message_handler, + symbol_tablet &symbol_table, + size_t max_nondet_array_length, + goto_functionst &goto_functions); + +#endif From 19c8d8d7c85cad8689772f6c87ac49ff96cfe713 Mon Sep 17 00:00:00 2001 From: reuk Date: Tue, 28 Mar 2017 11:04:21 +0100 Subject: [PATCH 4/7] Suppress loading methods with nondet signatures --- .../java_bytecode_convert_method.cpp | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) 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, From dc94557d87a310d4bdf1e848f8eafc8f0ac61cca Mon Sep 17 00:00:00 2001 From: reuk Date: Tue, 4 Apr 2017 17:00:52 +0100 Subject: [PATCH 5/7] Rearrange loop in remove_java_nondet --- src/goto-programs/remove_java_nondet.cpp | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/goto-programs/remove_java_nondet.cpp b/src/goto-programs/remove_java_nondet.cpp index 86962fddc64..ce1543ab7f3 100644 --- a/src/goto-programs/remove_java_nondet.cpp +++ b/src/goto-programs/remove_java_nondet.cpp @@ -298,17 +298,18 @@ static void remove_java_nondet( // Check each instruction. // `process_target` may modify the list in place, and returns the next // iterator to look at. + // Can't use forall_goto_program_instructions because we don't want to + // increment the iterator by one after every iteration. for(auto instruction_iterator=std::begin(goto_program.instructions), end=std::end(goto_program.instructions); - instruction_iterator!=end; - instruction_iterator=process_target( - message_handler, - symbol_table, - max_nondet_array_length, - goto_program, - instruction_iterator)) + instruction_iterator!=end;) { - // Loop body deliberately empty. + instruction_iterator=process_target( + message_handler, + symbol_table, + max_nondet_array_length, + goto_program, + instruction_iterator); } } From f4a47f9e1d64b013d054f0ae0529200c222b2bd7 Mon Sep 17 00:00:00 2001 From: reuk Date: Wed, 5 Apr 2017 12:01:39 +0100 Subject: [PATCH 6/7] Split java nondet pass in two --- src/cbmc/cbmc_parse_options.cpp | 12 +- src/goto-programs/Makefile | 3 +- src/goto-programs/convert_nondet.cpp | 164 ++++++++++++++ ...{remove_java_nondet.h => convert_nondet.h} | 30 +-- ...ava_nondet.cpp => replace_java_nondet.cpp} | 206 +++++++++--------- src/goto-programs/replace_java_nondet.h | 28 +++ src/util/irep_ids.txt | 3 +- src/util/std_code.h | 27 +++ 8 files changed, 342 insertions(+), 131 deletions(-) create mode 100644 src/goto-programs/convert_nondet.cpp rename src/goto-programs/{remove_java_nondet.h => convert_nondet.h} (51%) rename src/goto-programs/{remove_java_nondet.cpp => replace_java_nondet.cpp} (58%) create mode 100644 src/goto-programs/replace_java_nondet.h diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 9d36e749cf9..2c5806ed868 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -41,7 +41,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include +#include +#include #include #include @@ -931,11 +932,12 @@ bool cbmc_parse_optionst::process_goto_program( cmdline.isset("java-max-input-array-length") ? std::stoi(cmdline.get_value("java-max-input-array-length")) : MAX_NONDET_ARRAY_LENGTH_DEFAULT; - remove_java_nondet( - ui_message_handler, + replace_java_nondet(goto_functions); + convert_nondet( + goto_functions, symbol_table, - max_nondet_array_length, - goto_functions); + ui_message_handler, + max_nondet_array_length); // add generic checks status() << "Generic Property Instrumentation" << eom; diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index da3e3e63628..e873310b0c7 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -25,7 +25,8 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \ remove_const_function_pointers.cpp \ system_library_symbols.cpp \ string_refine_preprocess.cpp \ - remove_java_nondet.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/remove_java_nondet.h b/src/goto-programs/convert_nondet.h similarity index 51% rename from src/goto-programs/remove_java_nondet.h rename to src/goto-programs/convert_nondet.h index 0af514b5b11..919d977a94e 100644 --- a/src/goto-programs/remove_java_nondet.h +++ b/src/goto-programs/convert_nondet.h @@ -1,39 +1,39 @@ /*******************************************************************\ -Module: Remove Java Nondet expressions +Module: Convert side_effect_expr_nondett expressions Author: Reuben Thomas, reuben.thomas@diffblue.com \*******************************************************************/ -#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_JAVA_NONDET_H -#define CPROVER_GOTO_PROGRAMS_REMOVE_JAVA_NONDET_H +#ifndef CPROVER_GOTO_PROGRAMS_CONVERT_NONDET_H +#define CPROVER_GOTO_PROGRAMS_CONVERT_NONDET_H #include // size_t -class message_handlert; -class symbol_tablet; class goto_functionst; +class symbol_tablet; +class message_handlert; /*******************************************************************\ -Function: remove_java_nondet +Function: convert_nondet Inputs: - message_handler: Object which prints instructions. - symbol_table: The list of known symbols. - max_nondet_array_length: The maximum length of new nondet arrays. 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: Modify a goto_functionst to replace 'nondet' library functions with - CBMC-native nondet expressions. + Purpose: Replace calls to nondet library functions with an internal + nondet representation. \*******************************************************************/ -void remove_java_nondet( - message_handlert &message_handler, +void convert_nondet( + goto_functionst &goto_functions, symbol_tablet &symbol_table, - size_t max_nondet_array_length, - goto_functionst &goto_functions); + message_handlert &message_handler, + size_t max_nondet_array_length); #endif diff --git a/src/goto-programs/remove_java_nondet.cpp b/src/goto-programs/replace_java_nondet.cpp similarity index 58% rename from src/goto-programs/remove_java_nondet.cpp rename to src/goto-programs/replace_java_nondet.cpp index ce1543ab7f3..b78a0819cac 100644 --- a/src/goto-programs/remove_java_nondet.cpp +++ b/src/goto-programs/replace_java_nondet.cpp @@ -1,17 +1,15 @@ /*******************************************************************\ -Module: Remove Java Nondet expressions +Module: Replace Java Nondet expressions Author: Reuben Thomas, reuben.thomas@diffblue.com \*******************************************************************/ -#include "goto-programs/remove_java_nondet.h" +#include "goto-programs/replace_java_nondet.h" #include "goto-programs/goto_convert.h" #include "goto-programs/goto_model.h" -#include "java_bytecode/java_object_factory.h" - #include "util/irep_ids.h" #include @@ -19,16 +17,37 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com /*******************************************************************\ - Struct: nondet_instruction_infot + Class: nondet_instruction_infot - Purpose: Hold information about a nondet instruction invocation. + Purpose: Holds information about any discovered nondet methods, + with extreme type-safety. \*******************************************************************/ -struct nondet_instruction_infot final +class nondet_instruction_infot final { - bool is_nondet_instruction; - bool is_never_null; +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; }; /*******************************************************************\ @@ -36,15 +55,14 @@ struct nondet_instruction_infot final Function: is_nondet_returning_object Inputs: - function_call: A function call expression. - - Outputs: Whether the function has a nondet signature, and whether the nondet - item may be null. + 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: Find whether the supplied function call has a recognised 'nondet' - library signature. If so, specify whether the function call is - expected to return non-null. + Purpose: Checks whether the function call is one of our nondet + library functions. \*******************************************************************/ @@ -53,16 +71,17 @@ static nondet_instruction_infot is_nondet_returning_object( { 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, - std::regex(".*org\\.cprover\\.CProver\\.nondetWith(out)?Null.*"))) + if(!std::regex_match(function_name, match_results, reg)) { - return {false, false}; + return nondet_instruction_infot(); } - return {true, match_results[1].matched}; + return nondet_instruction_infot( + nondet_instruction_infot::is_nullablet(!match_results[1].matched)); } /*******************************************************************\ @@ -70,27 +89,27 @@ static nondet_instruction_infot is_nondet_returning_object( Function: get_nondet_instruction_info Inputs: - instr: A goto program instruction. + instr: A goto-program instruction to check. - Outputs: Whether the instruction is a function with a nondet signature, and - whether the nondet item may be null. + Outputs: A structure detailing the properties of the nondet method. - Purpose: Return whether the instruction has a recognised 'nondet' library - signature. + 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::targett &instr) + const goto_programt::const_targett &instr) { if(!(instr->is_function_call() && instr->code.id()==ID_code)) { - return {false, false}; + return nondet_instruction_infot(); } const auto &code=to_code(instr->code); if(code.get_statement()!=ID_function_call) { - return {false, false}; + return nondet_instruction_infot(); } const auto &function_call=to_code_function_call(code); return is_nondet_returning_object(function_call); @@ -111,7 +130,7 @@ Function: is_symbol_with_id \*******************************************************************/ -static bool is_symbol_with_id(const exprt& expr, const dstringt& 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; @@ -133,7 +152,7 @@ Function: is_typecast_with_id \*******************************************************************/ -static bool is_typecast_with_id(const exprt& expr, const dstringt& identifier) +static bool is_typecast_with_id(const exprt& expr, const irep_idt& identifier) { if(!(expr.id()==ID_typecast && expr.operands().size()==1)) { @@ -167,7 +186,7 @@ Function: is_assignment_from static bool is_assignment_from( const goto_programt::instructiont &instr, - const dstringt &identifier) + const irep_idt &identifier) { // If not an assignment, return false if(!instr.is_assign()) @@ -181,14 +200,12 @@ static bool is_assignment_from( /*******************************************************************\ -Function: process_target +Function: check_and_replace_target Inputs: - message_handler: Handles logging. - symbol_table: The table of known symbols. - max_nondet_array_length: Max length of arrays in new nondet objects. - instructions: The list of all instructions. - instr: The instruction to check. + 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. @@ -198,17 +215,15 @@ Function: process_target \*******************************************************************/ -static goto_programt::targett process_target( - message_handlert &message_handler, - symbol_tablet &symbol_table, - const size_t max_nondet_array_length, - goto_programt &prog, - const goto_programt::targett &instr) +static goto_programt::const_targett check_and_replace_target( + goto_programt &goto_program, + const goto_programt::const_targett &target) { - // Check whether this is our nondet library method, and return if not - const auto instr_info=get_nondet_instruction_info(instr); - const auto next_instr=std::next(instr); - if(!instr_info.is_nondet_instruction) + // 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; } @@ -225,8 +240,8 @@ static goto_programt::targett process_target( const auto return_identifier= to_symbol_expr(next_instr_assign_lhs).get_identifier(); - auto &instructions=prog.instructions; - const auto end=std::end(instructions); + 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( @@ -242,90 +257,63 @@ static goto_programt::targett process_target( // 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=instr->source_location; + 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= - instructions.erase(instr, after_matching_assignment); - - // Generate nondet init code - code_blockt init_code; - gen_nondet_init( - nondet_var, - init_code, - symbol_table, - source_loc, - false, - true, - instr_info.is_never_null, - 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 - prog.destructive_insert(after_erased, new_instructions); - prog.update(); + + 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: remove_java_nondet +Function: replace_java_nondet Inputs: - message_handler: Object which prints messages. - symbol_table: The list of known symbols. - max_nondet_array_length: The maximum length of new nondet arrays. - goto_program: The program to modify. + goto_program: The goto program to modify. - Purpose: Modify a goto_programt to replace 'nondet' library functions with - CBMC-native nondet expressions. + 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 remove_java_nondet( - message_handlert &message_handler, - symbol_tablet &symbol_table, - const size_t max_nondet_array_length, - goto_programt &goto_program) +static void replace_java_nondet(goto_programt &goto_program) { - // Check each instruction. - // `process_target` may modify the list in place, and returns the next - // iterator to look at. - // Can't use forall_goto_program_instructions because we don't want to - // increment the iterator by one after every iteration. - for(auto instruction_iterator=std::begin(goto_program.instructions), - end=std::end(goto_program.instructions); + for(auto instruction_iterator=goto_program.instructions.cbegin(), + end=goto_program.instructions.cend(); instruction_iterator!=end;) { - instruction_iterator=process_target( - message_handler, - symbol_table, - max_nondet_array_length, + instruction_iterator=check_and_replace_target( goto_program, instruction_iterator); } } -void remove_java_nondet( - message_handlert &message_handler, - symbol_tablet &symbol_table, - const size_t max_nondet_array_length, - goto_functionst &goto_functions) + + +void replace_java_nondet(goto_functionst &goto_functions) { - for(auto &f : goto_functions.function_map) + for(auto &goto_program : goto_functions.function_map) { - remove_java_nondet( - message_handler, - symbol_table, - max_nondet_array_length, - f.second.body); + 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/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 From ff72ddc8c5693331cf2c6141193aaf614dc6f08a Mon Sep 17 00:00:00 2001 From: reuk Date: Tue, 18 Apr 2017 16:18:09 +0100 Subject: [PATCH 7/7] Ensure assume only throws upon predicate failure --- src/java_bytecode/library/src/org/cprover/CProver.java | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/java_bytecode/library/src/org/cprover/CProver.java b/src/java_bytecode/library/src/org/cprover/CProver.java index 0dcae58c67e..6aadd228e9e 100644 --- a/src/java_bytecode/library/src/org/cprover/CProver.java +++ b/src/java_bytecode/library/src/org/cprover/CProver.java @@ -117,10 +117,9 @@ public static T nondetWithoutNull() public static void assume(boolean condition) { - if(enableAssume) + if(enableAssume && !condition) { - throw new RuntimeException( - "Cannot execute program with CProver.assume()"); + throw new RuntimeException("CProver.assume() predicate is false"); } } }