From 55bdbc71600ce380195def6677f921ebbcba7a40 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 11 Apr 2018 17:44:23 +0100 Subject: [PATCH 1/5] Recompile regression test class files The java files were changed in previous commits, but the class files were not recompiled, which caused confusing mismatches in line numbers. --- .../regression/jbmc/ClassCastException2/A.class | Bin 249 -> 197 bytes .../regression/jbmc/ClassCastException2/B.class | Bin 234 -> 182 bytes .../regression/jbmc/ClassCastException2/C.class | Bin 234 -> 182 bytes .../ClassCastExceptionTest.class | Bin 902 -> 651 bytes jbmc/regression/jbmc/catch1/catch1.class | Bin 360 -> 360 bytes 5 files changed, 0 insertions(+), 0 deletions(-) diff --git a/jbmc/regression/jbmc/ClassCastException2/A.class b/jbmc/regression/jbmc/ClassCastException2/A.class index 5400c088442da1dc2e18fb898c5fdd4ef64a7bf7..a6f4a62227db5d5645502208b359844e85f1adb3 100644 GIT binary patch delta 73 zcmey#c$87})W2Q(7#J8#7Ia(8MxUQcqWQ!O-zi_kY!*5LIws_t?dkq8-WZ) S26iCH1{MTKaR7Nt44eQFPzkmG delta 124 zcmX@g_>)oe)W2Q(7#J8#7zDT&m>GE48Ti;4_$P{LDG2%GCnx5FB^G5SCgr4tfCxqg zmXeIjVnzmLA4ltnwh31H42(d?z`&}toq=&9kio>j4kX#Yf{Y9tKsFCV0Rtxk7m&xu JzztT#0|2JY6RZFL diff --git a/jbmc/regression/jbmc/ClassCastException2/B.class b/jbmc/regression/jbmc/ClassCastException2/B.class index 57c02bfbefd2cf121d19be5c3ccef41f58cc1bbd..93bd28ff0ee4b2aee0672e2dd0f00ee4db994d8b 100644 GIT binary patch delta 73 zcmaFGxQ$Wt)W2Q(7#J8#7Ia(8MxUQcqWQ!O-%IHkY!*5LIws_t?dkq8-WZ) T26iCH1{P!nk{m!D69Xpz27n2R delta 124 zcmdnS_=-{V)W2Q(7#J8#7zDT&m>GE48Ti;4_$P{LDG2%GCnx5FB^G5SCgr4tfCxqg zmXeIjVnzmLA1CXHwt-gq42(d?z`&}toq=&9kio>j4kX#Yg3JsYKsFCV0Rtxk7m&xu JzztT#0|1p-6M_H$ diff --git a/jbmc/regression/jbmc/ClassCastException2/C.class b/jbmc/regression/jbmc/ClassCastException2/C.class index 3bff3313aa1ec28b55e0f9d2a44817e36a272510..207b0f2baea0d42dbc7f356b340be45c252e1f7e 100644 GIT binary patch delta 73 zcmaFGxQ$Wt)W2Q(7#J8#7Ia(8MxUQcqWQ!O-%IHkY!*5LIws_t?dkq8-WZ) S26iCH1`!0396%lu11A6mmI;jj delta 124 zcmdnS_=-{V)W2Q(7#J8#7zDT&m>GE48Ti;4_$P{LDG2%GCnx5FB^G5SCgr4tfCxqg zmXeIjVnzmLA7|@{wt-gq42(d?z`&}toq=&9kio>j4kXzif(#r$HV>4|$-o8VF*0z2 HRq+4-mD3Z2 diff --git a/jbmc/regression/jbmc/ClassCastException2/ClassCastExceptionTest.class b/jbmc/regression/jbmc/ClassCastException2/ClassCastExceptionTest.class index 503940e149abffa0c54dee4e007c706110245670..1d0c73b81b3b5dc4c574f6049c1f32669156a517 100644 GIT binary patch delta 370 zcmY*UEl&eM6r8=U*W0@*z2mDCO0Rqgu!Ueq_)0KsLIMVP5EK;%1P+HmHRtM3)rEu- zng9mFk0Q*TAVKWB-S=kZ&ECs{yZQa|_70$hHH`psf|`b9>bzjVhmX2oQA13tp^>5~ zSnBN@_FmICI=RU%t~%NEX?EVdBtPF%+d&x<3hIDoKYvtBJ4BR!sV#3g#0pk(WgXr5 zTm`5~6&&(rLxD14g|9lRVs+O?P(wpRO!SJTFj9g^-VHTlR+}{)!#W$mZf|_T=?svx zpWyWoj3I27K8A%hqQ<4-*4Wi(2xyd;CF1T1F=mPeaf%axbu5@JlQ8oatyTB{apJ!~ b_aV*zj{OYJ#I*j!G#*?Q?wZfc7USwKzS}4m literal 902 zcmZuv%Wl&^6g}fSoH$OK2MwVug+c;p3Js6!S|Qp{RxU`SRHCdLXB1o#r?MT?FJaLi zU|o=?L?p_Zk3yU=B|!=cd+xn+?m71{KYxAu4xovqfh_LmxNAUDXHCbNfrK*aX=Jdj zl%b`b8KIPzG@?8_kBB;UYxJ%Li~ zt#xF7up52b>owY;?|QvWr6(LJTiZm6j)+H(4ry&CP|$amy(S9P{D%dU#wQ1zO~AgNz=G&B_XPewroZcP$c&MuYh0W~Gz+BBnWRJ(DFYZt zMK#XxCP#@pDwI{ib;Nm>#Wfvu diff --git a/jbmc/regression/jbmc/catch1/catch1.class b/jbmc/regression/jbmc/catch1/catch1.class index ef8368dd862e7c50a7f469427ede8a5daec1a782..7af4da2e97f391b89849835953bc33e9c44d129e 100644 GIT binary patch delta 17 ZcmaFC^n!`w)W2Q(7#J8#HgY5|0sus+25SHS delta 17 ZcmaFC^n!`w)W2Q(7#J9gHgY5|0susy25A5Q From 04c0205679d04d023aa370de28cb4725726e81af Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 30 May 2018 14:56:26 +0100 Subject: [PATCH 2/5] Assert that there is uncaught exception That's the default behaviour because an escaping exception makes the JVM abort. The user can override this behaviour using the --disable-uncaught-exception-check option. --- jbmc/regression/jbmc/catch1/test.desc | 5 ++-- .../catch1/test_no_uncaught_exceptions.desc | 8 +++++ jbmc/regression/jbmc/exceptions18/test.desc | 5 ++-- .../java_bytecode_instrument.cpp | 22 ++++++++++++++ .../java_bytecode/java_bytecode_instrument.h | 7 +++++ .../java_bytecode/java_bytecode_language.cpp | 29 +++++++++---------- .../java_bytecode/java_bytecode_language.h | 26 ++++++++++------- jbmc/src/java_bytecode/java_entry_point.cpp | 13 ++++++++- jbmc/src/java_bytecode/java_entry_point.h | 4 ++- 9 files changed, 87 insertions(+), 32 deletions(-) create mode 100644 jbmc/regression/jbmc/catch1/test_no_uncaught_exceptions.desc diff --git a/jbmc/regression/jbmc/catch1/test.desc b/jbmc/regression/jbmc/catch1/test.desc index 4a3ac12a615..ddfa132953f 100644 --- a/jbmc/regression/jbmc/catch1/test.desc +++ b/jbmc/regression/jbmc/catch1/test.desc @@ -1,8 +1,9 @@ CORE catch1.class -^EXIT=0$ +^EXIT=10$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ +^VERIFICATION FAILED$ +^\[.*\] no uncaught exception: FAILURE$ -- ^warning: ignoring diff --git a/jbmc/regression/jbmc/catch1/test_no_uncaught_exceptions.desc b/jbmc/regression/jbmc/catch1/test_no_uncaught_exceptions.desc new file mode 100644 index 00000000000..c56b7711d75 --- /dev/null +++ b/jbmc/regression/jbmc/catch1/test_no_uncaught_exceptions.desc @@ -0,0 +1,8 @@ +CORE +catch1.class +--disable-uncaught-exception-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/exceptions18/test.desc b/jbmc/regression/jbmc/exceptions18/test.desc index eff4927d2da..cd52d2e9ea1 100644 --- a/jbmc/regression/jbmc/exceptions18/test.desc +++ b/jbmc/regression/jbmc/exceptions18/test.desc @@ -1,8 +1,9 @@ CORE Test.class --function Test.goo -^EXIT=0$ +^EXIT=10$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ +^VERIFICATION FAILED$ +no uncaught exception: FAILURE -- ^warning: ignoring diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp index cbdf8dab7c1..f0aae000897 100644 --- a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp @@ -19,6 +19,7 @@ Date: June 2017 #include #include "java_bytecode_convert_class.h" +#include "java_entry_point.h" #include "java_utils.h" class java_bytecode_instrumentt:public messaget @@ -592,6 +593,27 @@ void java_bytecode_instrument_symbol( instrument(to_code(symbol.value)); } +/// Instruments the start function with an assertion that checks whether +/// an exception has escaped the entry point +/// \param init_code: the code block to which the assertion is appended +/// \param exc_symbol: the top-level exception symbol +/// \param source_location: the source location to attach to the assertion +void java_bytecode_instrument_uncaught_exceptions( + codet &init_code, + const symbolt &exc_symbol, + const source_locationt &source_location) +{ + // check that there is no uncaught exception + code_assertt assert_no_exception; + assert_no_exception.assertion() = equal_exprt( + exc_symbol.symbol_expr(), + null_pointer_exprt(to_pointer_type(exc_symbol.type))); + source_locationt assert_location = source_location; + assert_location.set_comment("no uncaught exception"); + assert_no_exception.add_source_location() = assert_location; + init_code.move_to_operands(assert_no_exception); +} + /// Instruments all the code in the symbol_table with /// runtime exceptions or corresponding assertions. /// Exceptions are thrown when the `throw_runtime_exceptions` flag is set. diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.h b/jbmc/src/java_bytecode/java_bytecode_instrument.h index 075b6467765..5dfd5fdd918 100644 --- a/jbmc/src/java_bytecode/java_bytecode_instrument.h +++ b/jbmc/src/java_bytecode/java_bytecode_instrument.h @@ -15,6 +15,8 @@ Date: June 2017 #include #include +class codet; + void java_bytecode_instrument_symbol( symbol_table_baset &symbol_table, symbolt &symbol, @@ -26,6 +28,11 @@ void java_bytecode_instrument( const bool throw_runtime_exceptions, message_handlert &_message_handler); +void java_bytecode_instrument_uncaught_exceptions( + codet &init_code, + const symbolt &exc_symbol, + const source_locationt &source_location); + extern const std::vector exception_needed_classes; #endif diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index ec09d38c24a..b890b3a8b9c 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -46,6 +46,9 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null"); string_refinement_enabled=cmd.isset("refine-strings"); throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions"); + assert_uncaught_exceptions = !cmd.isset("disable-uncaught-exception-check"); + threading_support = cmd.isset("java-threading"); + if(cmd.isset("java-max-input-array-length")) object_factory_parameters.max_nondet_array_length= std::stoi(cmd.get_value("java-max-input-array-length")); @@ -69,14 +72,8 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) else lazy_methods_mode=LAZY_METHODS_MODE_EAGER; - if(cmd.isset("java-threading")) - threading_support = true; - else - threading_support = false; - - if(cmd.isset("java-throw-runtime-exceptions")) + if(throw_runtime_exceptions) { - throw_runtime_exceptions = true; java_load_classes.insert( java_load_classes.end(), exception_needed_classes.begin(), @@ -777,15 +774,15 @@ bool java_bytecode_languaget::generate_support_functions( convert_lazy_method(res.main_function.name, symbol_table); // generate the test harness in __CPROVER__start and a call the entry point - return - java_entry_point( - symbol_table, - main_class, - get_message_handler(), - assume_inputs_non_null, - object_factory_parameters, - get_pointer_type_selector(), - string_refinement_enabled); + return java_entry_point( + symbol_table, + main_class, + get_message_handler(), + assume_inputs_non_null, + assert_uncaught_exceptions, + object_factory_parameters, + get_pointer_type_selector(), + string_refinement_enabled); } /// Uses a simple context-insensitive ('ci') analysis to determine which methods diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index f7c0ac17020..ec80fff81f6 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -26,19 +26,23 @@ Author: Daniel Kroening, kroening@kroening.com #include -#define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \ - "(java-assume-inputs-non-null)" \ - "(java-throw-runtime-exceptions)" \ - "(java-max-input-array-length):" \ - "(java-max-input-tree-depth):" \ - "(java-max-vla-length):" \ - "(java-cp-include-files):" \ - "(lazy-methods)" \ - "(lazy-methods-extra-entry-point):" \ - "(java-load-class):" \ +// clang-format off +#define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \ + "(disable-uncaught-exception-check)" \ + "(java-assume-inputs-non-null)" \ + "(java-throw-runtime-exceptions)" \ + "(java-max-input-array-length):" \ + "(java-max-input-tree-depth):" \ + "(java-max-vla-length):" \ + "(java-cp-include-files):" \ + "(lazy-methods)" \ + "(lazy-methods-extra-entry-point):" \ + "(java-load-class):" \ "(java-no-load-class):" #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \ + " --disable-uncaught-exception-check" \ + " ignore uncaught exceptions and errors\n" \ " --java-assume-inputs-non-null never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \ " entry point with null\n" /* NOLINT(*) */ \ " --java-throw-runtime-exceptions make implicit runtime exceptions explicit\n" /* NOLINT(*) */ \ @@ -55,6 +59,7 @@ Author: Daniel Kroening, kroening@kroening.com " treat METHODNAME as a possible program entry point for\n" /* NOLINT(*) */ \ " the purpose of lazy method loading\n" /* NOLINT(*) */ \ " A '.*' wildcard is allowed to specify all class members\n" +// clang-format on class symbolt; @@ -167,6 +172,7 @@ class java_bytecode_languaget:public languaget std::vector lazy_methods_extra_entry_points; bool string_refinement_enabled; bool throw_runtime_exceptions; + bool assert_uncaught_exceptions; java_string_library_preprocesst string_preprocess; std::string java_cp_include_files; diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index fff6b0631a1..6c56faa228c 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "java_bytecode_instrument.h" #include "java_object_factory.h" #include "java_string_literals.h" #include "java_utils.h" @@ -520,6 +521,7 @@ bool java_entry_point( const irep_idt &main_class, message_handlert &message_handler, bool assume_init_pointers_not_null, + bool assert_uncaught_exceptions, const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled) @@ -554,6 +556,7 @@ bool java_entry_point( symbol_table, message_handler, assume_init_pointers_not_null, + assert_uncaught_exceptions, object_factory_parameters, pointer_type_selector); } @@ -576,7 +579,8 @@ bool generate_java_start_function( symbol_table_baset &symbol_table, message_handlert &message_handler, bool assume_init_pointers_not_null, - const object_factory_parameterst& object_factory_parameters, + bool assert_uncaught_exceptions, + const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector) { messaget message(message_handler); @@ -699,6 +703,13 @@ bool generate_java_start_function( // declare certain (which?) variables as test outputs java_record_outputs(symbol, main_arguments, init_code, symbol_table); + // add uncaught-exception check if requested + if(assert_uncaught_exceptions) + { + java_bytecode_instrument_uncaught_exceptions( + init_code, exc_symbol, symbol.location); + } + // create a symbol for the __CPROVER__start function, associate the code that // we just built and register it in the symbol table symbolt new_symbol; diff --git a/jbmc/src/java_bytecode/java_entry_point.h b/jbmc/src/java_bytecode/java_entry_point.h index 3fcdee49388..dd0b1fca004 100644 --- a/jbmc/src/java_bytecode/java_entry_point.h +++ b/jbmc/src/java_bytecode/java_entry_point.h @@ -24,6 +24,7 @@ bool java_entry_point( const irep_idt &main_class, class message_handlert &message_handler, bool assume_init_pointers_not_null, + bool assert_uncaught_exceptions, const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled); @@ -74,7 +75,8 @@ bool generate_java_start_function( class symbol_table_baset &symbol_table, class message_handlert &message_handler, bool assume_init_pointers_not_null, - const object_factory_parameterst& object_factory_parameters, + bool assert_uncaught_exceptions, + const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector); #endif // CPROVER_JAVA_BYTECODE_JAVA_ENTRY_POINT_H From 07acde40b451e434402ecf1e411bc69fe8bd933c Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 13 Jun 2018 13:18:33 +0100 Subject: [PATCH 3/5] Refactor user-defined assertion translation for Java Assertions in Java are "throw a;" statements where a is of type java.lang.AssertionError (an exception, or Throwable, to be precise). Sometimes we want to translate it into an ASSERT instruction in the goto program. Special-casing in order to handle that was scattered across multiple classes. In this commit we special-case it only once in the Java frontend and translate it into assert(false); assume(false); which is then correctly handled by later stages of the translation. --- .../jbmc-strings/max-length/test1.desc | 2 +- .../jbmc-strings/max-length/test2.desc | 2 +- .../jbmc-strings/max-length/test3.desc | 2 +- jbmc/regression/jbmc/assert7/Test.class | Bin 0 -> 300 bytes jbmc/regression/jbmc/assert7/Test.java | 9 ++++ jbmc/regression/jbmc/assert7/test.desc | 8 ++++ jbmc/regression/jbmc/exceptions23/test.desc | 2 +- jbmc/regression/jbmc/exceptions24/test.desc | 2 +- jbmc/regression/jbmc/finally1/test.desc | 2 +- jbmc/regression/jbmc/finally2/test.desc | 2 +- jbmc/regression/jbmc/finally3/test.desc | 4 +- jbmc/regression/jbmc/finally4/test.desc | 2 +- jbmc/regression/jbmc/finally5/test.desc | 2 +- jbmc/regression/jbmc/finally6/test.desc | 2 +- jbmc/regression/jbmc/finally7/test.desc | 4 +- .../no-main-int-array-maybe-null1/test.desc | 6 +-- .../no-main-multi-array-maybe-null1/test.desc | 2 +- .../no-main-multi-array-maybe-null2/test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 4 +- .../test.desc | 4 +- .../java_bytecode_convert_method.cpp | 40 ++++++++++++++++-- .../java_bytecode_typecheck_expr.cpp | 4 +- jbmc/src/java_bytecode/remove_exceptions.cpp | 17 +------- src/analyses/uncaught_exceptions_analysis.cpp | 17 +++----- src/goto-programs/builtin_functions.cpp | 28 ------------ 27 files changed, 88 insertions(+), 85 deletions(-) create mode 100644 jbmc/regression/jbmc/assert7/Test.class create mode 100644 jbmc/regression/jbmc/assert7/Test.java create mode 100644 jbmc/regression/jbmc/assert7/test.desc diff --git a/jbmc/regression/jbmc-strings/max-length/test1.desc b/jbmc/regression/jbmc-strings/max-length/test1.desc index 1cdaf80b01e..db6b0190670 100644 --- a/jbmc/regression/jbmc-strings/max-length/test1.desc +++ b/jbmc/regression/jbmc-strings/max-length/test1.desc @@ -3,4 +3,4 @@ Test.class --refine-strings --verbosity 10 --string-max-input-length 499999 --function Test.checkMaxInputLength ^EXIT=0$ ^SIGNAL=0$ -assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 16: SUCCESS +assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 17: SUCCESS diff --git a/jbmc/regression/jbmc-strings/max-length/test2.desc b/jbmc/regression/jbmc-strings/max-length/test2.desc index e705d18deda..b5f70b5658d 100644 --- a/jbmc/regression/jbmc-strings/max-length/test2.desc +++ b/jbmc/regression/jbmc-strings/max-length/test2.desc @@ -3,4 +3,4 @@ Test.class --refine-strings --verbosity 10 --string-max-input-length 500000 --function Test.checkMaxInputLength ^EXIT=10$ ^SIGNAL=0$ -assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 16: FAILURE +assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 17: FAILURE diff --git a/jbmc/regression/jbmc-strings/max-length/test3.desc b/jbmc/regression/jbmc-strings/max-length/test3.desc index ab4c3b62db5..f8e970cc618 100644 --- a/jbmc/regression/jbmc-strings/max-length/test3.desc +++ b/jbmc/regression/jbmc-strings/max-length/test3.desc @@ -3,4 +3,4 @@ Test.class --refine-strings --verbosity 10 --string-max-length 4001 --function Test.checkMaxLength ^EXIT=10$ ^SIGNAL=0$ -assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 26: FAILURE +assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 27: FAILURE diff --git a/jbmc/regression/jbmc/assert7/Test.class b/jbmc/regression/jbmc/assert7/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..fbf9949d0e6ab0258388c62969571aa5c59c48a0 GIT binary patch literal 300 zcmYL_L2JT55QX2wXf#@r_E35$^dhK-dhuo{l%l859+X1qX_GFpq8r$({;!^d7WxDH zQPP=Svar0z@Vz(7p3dLD0H(N#(L_H&5+e{zBU}<%55^k*NN5a4Z-nr<{M3XbGgiOs zce!>em2Y_x?v$~F>)}VXQ3o~ID!ZO6y)$+_lVH3o_pZD}OIs4=qH5n>zDU zRoZz|+PQP3<6>b6X-&N58(nzZA>;?k3HWji2yJ$^ti;+JA3;hI{M-T>Jr&sWssM literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/assert7/Test.java b/jbmc/regression/jbmc/assert7/Test.java new file mode 100644 index 00000000000..94aa947981c --- /dev/null +++ b/jbmc/regression/jbmc/assert7/Test.java @@ -0,0 +1,9 @@ +class Test +{ + public static void main(String[] args) + { + AssertionError a = new AssertionError(); + if(false) + throw a; + } +} diff --git a/jbmc/regression/jbmc/assert7/test.desc b/jbmc/regression/jbmc/assert7/test.desc new file mode 100644 index 00000000000..de97168986e --- /dev/null +++ b/jbmc/regression/jbmc/assert7/test.desc @@ -0,0 +1,8 @@ +CORE +Test.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/jbmc/regression/jbmc/exceptions23/test.desc b/jbmc/regression/jbmc/exceptions23/test.desc index d9ccdcfc182..c99eef557dd 100644 --- a/jbmc/regression/jbmc/exceptions23/test.desc +++ b/jbmc/regression/jbmc/exceptions23/test.desc @@ -4,7 +4,7 @@ test.class ^EXIT=10$ ^SIGNAL=0$ VERIFICATION FAILED -assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 12: FAILURE +assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 13: FAILURE -- ^warning: ignoring -- diff --git a/jbmc/regression/jbmc/exceptions24/test.desc b/jbmc/regression/jbmc/exceptions24/test.desc index 523a3078bce..a58943b5d28 100644 --- a/jbmc/regression/jbmc/exceptions24/test.desc +++ b/jbmc/regression/jbmc/exceptions24/test.desc @@ -4,7 +4,7 @@ test.class ^EXIT=10$ ^SIGNAL=0$ VERIFICATION FAILED -assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 10: FAILURE +assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 11: FAILURE -- ^warning: ignoring -- diff --git a/jbmc/regression/jbmc/finally1/test.desc b/jbmc/regression/jbmc/finally1/test.desc index 9a6a879eae8..f784d2a8638 100644 --- a/jbmc/regression/jbmc/finally1/test.desc +++ b/jbmc/regression/jbmc/finally1/test.desc @@ -3,7 +3,7 @@ test.class --function test.main ^EXIT=10$ ^SIGNAL=0$ -assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 9: FAILURE +assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 10: FAILURE ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/jbmc/regression/jbmc/finally2/test.desc b/jbmc/regression/jbmc/finally2/test.desc index ae776b8ed1f..f55fdf67b90 100644 --- a/jbmc/regression/jbmc/finally2/test.desc +++ b/jbmc/regression/jbmc/finally2/test.desc @@ -3,7 +3,7 @@ test.class --function test.main ^EXIT=10$ ^SIGNAL=0$ -assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 9: FAILURE +assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 10: FAILURE ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/jbmc/regression/jbmc/finally3/test.desc b/jbmc/regression/jbmc/finally3/test.desc index fb6be4be278..d7d0d875093 100644 --- a/jbmc/regression/jbmc/finally3/test.desc +++ b/jbmc/regression/jbmc/finally3/test.desc @@ -3,8 +3,8 @@ test.class --function test.main ^EXIT=10$ ^SIGNAL=0$ -assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 9: SUCCESS -assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 22: FAILURE +assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 10: SUCCESS +assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 23: FAILURE ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/jbmc/regression/jbmc/finally4/test.desc b/jbmc/regression/jbmc/finally4/test.desc index 60ea3c4cb9e..726bf1fbabe 100644 --- a/jbmc/regression/jbmc/finally4/test.desc +++ b/jbmc/regression/jbmc/finally4/test.desc @@ -3,7 +3,7 @@ test.class --function test.main ^EXIT=10$ ^SIGNAL=0$ -assertion at file test\.java line 11 function java::test\.main:\(\)V bytecode-index 7: FAILURE +assertion at file test\.java line 11 function java::test\.main:\(\)V bytecode-index 8: FAILURE ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/jbmc/regression/jbmc/finally5/test.desc b/jbmc/regression/jbmc/finally5/test.desc index dcf21ec2d2d..02a6377beac 100644 --- a/jbmc/regression/jbmc/finally5/test.desc +++ b/jbmc/regression/jbmc/finally5/test.desc @@ -3,7 +3,7 @@ test.class --function test.main ^EXIT=10$ ^SIGNAL=0$ -assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 12: FAILURE +assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 13: FAILURE ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/jbmc/regression/jbmc/finally6/test.desc b/jbmc/regression/jbmc/finally6/test.desc index 3a05a209373..8c854c3044e 100644 --- a/jbmc/regression/jbmc/finally6/test.desc +++ b/jbmc/regression/jbmc/finally6/test.desc @@ -3,7 +3,7 @@ test.class --function test.main ^EXIT=10$ ^SIGNAL=0$ -assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 12: FAILURE +assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 13: FAILURE ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/jbmc/regression/jbmc/finally7/test.desc b/jbmc/regression/jbmc/finally7/test.desc index 27fd61ddad6..93252fa1c7e 100644 --- a/jbmc/regression/jbmc/finally7/test.desc +++ b/jbmc/regression/jbmc/finally7/test.desc @@ -3,8 +3,8 @@ test.class --function test.main ^EXIT=10$ ^SIGNAL=0$ -assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 12: SUCCESS -assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 25: FAILURE +assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 13: SUCCESS +assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 26: FAILURE ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc index 46abab6236b..57b29af8ed2 100644 --- a/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc +++ b/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc @@ -4,9 +4,9 @@ Main.class ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -assertion at file Main\.java line 5 function .* bytecode-index 6: FAILURE -assertion at file Main\.java line 6 function .* bytecode-index 14: FAILURE -assertion at file Main\.java line 12 function .* bytecode-index 31: SUCCESS +assertion at file Main\.java line 5 function .* bytecode-index 7: FAILURE +assertion at file Main\.java line 6 function .* bytecode-index 15: FAILURE +assertion at file Main\.java line 12 function .* bytecode-index 32: SUCCESS \*\* 2 of .* failed -- ^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc index a631452f5f6..1c3eaaa7630 100644 --- a/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc +++ b/jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc @@ -4,7 +4,7 @@ Main.class ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE +assertion at file Main\.java line 5 function .* bytecode-index 25: FAILURE \*\* 1 of .* failed -- ^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc index a631452f5f6..1c3eaaa7630 100644 --- a/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc +++ b/jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc @@ -4,7 +4,7 @@ Main.class ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE +assertion at file Main\.java line 5 function .* bytecode-index 25: FAILURE \*\* 1 of .* failed -- ^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc index 145c918788c..e5d26e7a2e6 100644 --- a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc +++ b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc @@ -4,7 +4,7 @@ Main.class ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -assertion at file Main\.java line 6 function .* bytecode-index 13: FAILURE +assertion at file Main\.java line 6 function .* bytecode-index 14: FAILURE \*\* 1 of .* failed -- ^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc index 145c918788c..e5d26e7a2e6 100644 --- a/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc +++ b/jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc @@ -4,7 +4,7 @@ Main.class ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -assertion at file Main\.java line 6 function .* bytecode-index 13: FAILURE +assertion at file Main\.java line 6 function .* bytecode-index 14: FAILURE \*\* 1 of .* failed -- ^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc index 58989b56c0c..19af5a25191 100644 --- a/jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc +++ b/jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc @@ -4,8 +4,8 @@ Main.class ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -assertion at file Main\.java line 10 function .* bytecode-index 6: FAILURE -assertion at file Main\.java line 14 function .* bytecode-index 26: FAILURE +assertion at file Main\.java line 10 function .* bytecode-index 7: FAILURE +assertion at file Main\.java line 14 function .* bytecode-index 27: FAILURE \*\* 2 of .* failed -- ^warning: ignoring diff --git a/jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc index 58989b56c0c..19af5a25191 100644 --- a/jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc +++ b/jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc @@ -4,8 +4,8 @@ Main.class ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -assertion at file Main\.java line 10 function .* bytecode-index 6: FAILURE -assertion at file Main\.java line 14 function .* bytecode-index 26: FAILURE +assertion at file Main\.java line 10 function .* bytecode-index 7: FAILURE +assertion at file Main\.java line 14 function .* bytecode-index 27: FAILURE \*\* 2 of .* failed -- ^warning: ignoring diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 70308954f9e..d35e2336fc2 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -32,11 +32,14 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include + #include +#include #include #include @@ -2248,10 +2251,39 @@ void java_bytecode_convert_methodt::convert_athrow( codet &c, exprt::operandst &results) const { - side_effect_expr_throwt throw_expr; - throw_expr.add_source_location() = location; - throw_expr.copy_to_operands(op[0]); - c = code_expressiont(throw_expr); + if( + uncaught_exceptions_domaint::get_exception_type(op[0].type()) == + "java::java.lang.AssertionError") + { + // we translate athrow into + // ASSERT false; + // ASSUME false: + code_assertt assert_code; + assert_code.assertion() = false_exprt(); + source_locationt assert_location = location; // copy + assert_location.set_comment("assertion at " + location.as_string()); + assert_location.set("user-provided", true); + assert_location.set_property_class(ID_assertion); + assert_code.add_source_location() = assert_location; + + code_assumet assume_code; + assume_code.assumption() = false_exprt(); + source_locationt assume_location = location; // copy + assume_location.set("user-provided", true); + assume_code.add_source_location() = assume_location; + + code_blockt ret_block; + ret_block.move_to_operands(assert_code); + ret_block.move_to_operands(assume_code); + c = ret_block; + } + else + { + side_effect_expr_throwt throw_expr; + throw_expr.add_source_location() = location; + throw_expr.copy_to_operands(op[0]); + c = code_expressiont(throw_expr); + } results[0] = op[0]; } diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp index 83dcaa6dd9b..deeb269eb76 100644 --- a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp @@ -81,7 +81,9 @@ void java_bytecode_typecheckt::typecheck_expr_symbol(symbol_exprt &expr) if(s_it==symbol_table.symbols.end()) { - PRECONDITION(has_prefix(id2string(identifier), "java::")); + PRECONDITION( + has_prefix(id2string(identifier), "java::") || + has_prefix(id2string(identifier), CPROVER_PREFIX)); // no, create the symbol symbolt new_symbol; diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp index b0ae6decb3d..f189eea79ee 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.cpp +++ b/jbmc/src/java_bytecode/remove_exceptions.cpp @@ -164,13 +164,7 @@ bool remove_exceptionst::function_or_callees_may_throw( { if(instr_it->is_throw()) { - const exprt &exc = - uncaught_exceptions_domaint::get_exception_symbol(instr_it->code); - bool is_assertion_error = - id2string(uncaught_exceptions_domaint::get_exception_type(exc.type())). - find("java.lang.AssertionError")!=std::string::npos; - if(!is_assertion_error) - return true; + return true; } if(instr_it->is_function_call()) @@ -380,15 +374,6 @@ bool remove_exceptionst::instrument_throw( const exprt &exc_expr= uncaught_exceptions_domaint::get_exception_symbol(instr_it->code); - bool assertion_error=id2string( - uncaught_exceptions_domaint::get_exception_type(exc_expr.type())). - find("java.lang.AssertionError")!=std::string::npos; - - // we don't count AssertionError (we couldn't catch it anyway - // and this may reduce the instrumentation considerably if the programmer - // used assertions) - if(assertion_error) - return false; add_exception_dispatch_sequence( goto_program, instr_it, stack_catch, locals); diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp index dfd0d9a51ca..21e4c47ec67 100644 --- a/src/analyses/uncaught_exceptions_analysis.cpp +++ b/src/analyses/uncaught_exceptions_analysis.cpp @@ -70,17 +70,12 @@ void uncaught_exceptions_domaint::transform( const exprt &exc_symbol=get_exception_symbol(instruction.code); // retrieve the static type of the thrown exception const irep_idt &type_id=get_exception_type(exc_symbol.type()); - bool assertion_error= - id2string(type_id).find("java.lang.AssertionError")!=std::string::npos; - if(!assertion_error) - { - join(type_id); - // we must consider all the subtypes given that - // the runtime type is a subtype of the static type - std::vector subtypes= - class_hierarchy.get_children_trans(type_id); - join(subtypes); - } + join(type_id); + // we must consider all the subtypes given that + // the runtime type is a subtype of the static type + std::vector subtypes = + class_hierarchy.get_children_trans(type_id); + join(subtypes); break; } case CATCH: diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 74bf5ede7a4..330c4c1f152 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -736,34 +736,6 @@ void goto_convertt::do_function_call_symbol( a->source_location=function.source_location(); a->source_location.set("user-provided", true); } - else if(has_prefix( - id2string(identifier), "java::java.lang.AssertionError.:")) - { - // insert function call anyway - code_function_callt function_call; - function_call.lhs()=lhs; - function_call.function()=function; - function_call.arguments()=arguments; - function_call.add_source_location()=function.source_location(); - - copy(function_call, FUNCTION_CALL, dest); - - if(arguments.size() != 1 && arguments.size() != 2 && arguments.size() != 3) - { - error().source_location=function.find_source_location(); - error() << "`" << identifier - << "' expected to have one, two or three arguments" << eom; - throw 0; - } - - goto_programt::targett t=dest.add_instruction(ASSERT); - t->guard=false_exprt(); - t->source_location=function.source_location(); - t->source_location.set("user-provided", true); - t->source_location.set_property_class(ID_assertion); - t->source_location.set_comment( - "assertion at "+function.source_location().as_string()); - } else if(identifier=="assert" && !ns.lookup(identifier).location.get_function().empty()) { From 653d88744e8a9700c4237d30cf6f343fbf9fee00 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 13 Jun 2018 13:20:18 +0100 Subject: [PATCH 4/5] Remove wrong assumption from goto check The argument of throw might be null even if it is of type java.lang.AssertionError. --- src/analyses/goto_check.cpp | 23 +++++++++-------------- 1 file changed, 9 insertions(+), 14 deletions(-) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 4b47085b745..cb35ef0cef9 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1627,21 +1627,16 @@ void goto_checkt::goto_check( exprt pointer=i.code.op0().op0(); - if(pointer.type().subtype().get(ID_identifier)!= - "java::java.lang.AssertionError") - { - notequal_exprt not_eq_null( - pointer, - null_pointer_exprt(to_pointer_type(pointer.type()))); + const notequal_exprt not_eq_null( + pointer, null_pointer_exprt(to_pointer_type(pointer.type()))); - add_guarded_claim( - not_eq_null, - "throwing null", - "pointer dereference", - i.source_location, - pointer, - guardt()); - } + add_guarded_claim( + not_eq_null, + "throwing null", + "pointer dereference", + i.source_location, + pointer, + guardt()); } // this has no successor From cd2ef4b0700cb3581e0fa7f4e9e19721124fe0ef Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 13 Jun 2018 13:32:59 +0100 Subject: [PATCH 5/5] Enable throwing of AssertionError Introduces --throw-assertion-error which allows to propgate AssertionError as performed in the JVM rather than using a goto ASSERT statement. --- jbmc/regression/jbmc/assert3/test_throw_no_uncaught.desc | 8 ++++++++ jbmc/src/java_bytecode/java_bytecode_convert_method.cpp | 3 +++ jbmc/src/java_bytecode/java_bytecode_convert_method.h | 1 + .../java_bytecode/java_bytecode_convert_method_class.h | 3 +++ jbmc/src/java_bytecode/java_bytecode_language.cpp | 2 ++ jbmc/src/java_bytecode/java_bytecode_language.h | 5 +++++ 6 files changed, 22 insertions(+) create mode 100644 jbmc/regression/jbmc/assert3/test_throw_no_uncaught.desc diff --git a/jbmc/regression/jbmc/assert3/test_throw_no_uncaught.desc b/jbmc/regression/jbmc/assert3/test_throw_no_uncaught.desc new file mode 100644 index 00000000000..306a0a45408 --- /dev/null +++ b/jbmc/regression/jbmc/assert3/test_throw_no_uncaught.desc @@ -0,0 +1,8 @@ +CORE +assert3.class +--throw-assertion-error --disable-uncaught-exception-check +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index d35e2336fc2..7829d813b08 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -2252,6 +2252,7 @@ void java_bytecode_convert_methodt::convert_athrow( exprt::operandst &results) const { if( + !throw_assertion_error && uncaught_exceptions_domaint::get_exception_type(op[0].type()) == "java::java.lang.AssertionError") { @@ -3087,6 +3088,7 @@ void java_bytecode_convert_method( symbol_table_baset &symbol_table, message_handlert &message_handler, size_t max_array_length, + bool throw_assertion_error, optionalt needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy) @@ -3105,6 +3107,7 @@ void java_bytecode_convert_method( symbol_table, message_handler, max_array_length, + throw_assertion_error, needed_lazy_methods, string_preprocess, class_hierarchy); diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.h b/jbmc/src/java_bytecode/java_bytecode_convert_method.h index 2ef174dbda9..a3c6ad6ebe0 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.h @@ -33,6 +33,7 @@ void java_bytecode_convert_method( symbol_table_baset &symbol_table, message_handlert &message_handler, size_t max_array_length, + bool throw_assertion_error, optionalt needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy); diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h index 205cdfccbfa..6e2975ed337 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h @@ -36,12 +36,14 @@ class java_bytecode_convert_methodt:public messaget symbol_table_baset &symbol_table, message_handlert &_message_handler, size_t _max_array_length, + bool throw_assertion_error, optionalt needed_lazy_methods, java_string_library_preprocesst &_string_preprocess, const class_hierarchyt &class_hierarchy) : messaget(_message_handler), symbol_table(symbol_table), max_array_length(_max_array_length), + throw_assertion_error(throw_assertion_error), needed_lazy_methods(std::move(needed_lazy_methods)), string_preprocess(_string_preprocess), slots_for_parameters(0), @@ -64,6 +66,7 @@ class java_bytecode_convert_methodt:public messaget protected: symbol_table_baset &symbol_table; const size_t max_array_length; + const bool throw_assertion_error; optionalt needed_lazy_methods; /// Fully qualified name of the method under translation. diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index b890b3a8b9c..6baf3216e63 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -47,6 +47,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) string_refinement_enabled=cmd.isset("refine-strings"); throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions"); assert_uncaught_exceptions = !cmd.isset("disable-uncaught-exception-check"); + throw_assertion_error = cmd.isset("throw-assertion-error"); threading_support = cmd.isset("java-threading"); if(cmd.isset("java-max-input-array-length")) @@ -1030,6 +1031,7 @@ bool java_bytecode_languaget::convert_single_method( symbol_table, get_message_handler(), max_user_array_length, + throw_assertion_error, std::move(needed_lazy_methods), string_preprocess, class_hierarchy); diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index ec80fff81f6..e4fcfaf8c14 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -29,6 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com // clang-format off #define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \ "(disable-uncaught-exception-check)" \ + "(throw-assertion-error)" \ "(java-assume-inputs-non-null)" \ "(java-throw-runtime-exceptions)" \ "(java-max-input-array-length):" \ @@ -43,6 +44,9 @@ Author: Daniel Kroening, kroening@kroening.com #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \ " --disable-uncaught-exception-check" \ " ignore uncaught exceptions and errors\n" \ + " --throw-assertion-error throw java.lang.AssertionError on violated\n" /* NOLINT(*) */ \ + " assert statements instead of failing\n" \ + " at the location of the assert statement\n" /* NOLINT(*) */ \ " --java-assume-inputs-non-null never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \ " entry point with null\n" /* NOLINT(*) */ \ " --java-throw-runtime-exceptions make implicit runtime exceptions explicit\n" /* NOLINT(*) */ \ @@ -173,6 +177,7 @@ class java_bytecode_languaget:public languaget bool string_refinement_enabled; bool throw_runtime_exceptions; bool assert_uncaught_exceptions; + bool throw_assertion_error; java_string_library_preprocesst string_preprocess; std::string java_cp_include_files;