From ab608522c1a59f94a62b9dacd8b5486f1e1abc32 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 7 Jun 2018 17:27:11 +0100 Subject: [PATCH] Add org.cprover.MustNotThrow method attribute This asserts that a particular method must not throw exceptions, intended for use with internal methods such as cproverNondetInitialize, which must not propagate exceptions to their callsite. In such a case, instead of an exception dispatch table we introduce an assumption checking one was not in fact thrown. --- .../jbmc/must-not-throw-annotation/Test.class | Bin 0 -> 773 bytes .../jbmc/must-not-throw-annotation/Test.java | 17 ++++++++++ .../org/cprover/MustNotThrow.class | Bin 0 -> 156 bytes .../org/cprover/MustNotThrow.java | 3 ++ .../jbmc/must-not-throw-annotation/test.desc | 8 +++++ .../java_bytecode_convert_method.cpp | 7 ++++ jbmc/src/java_bytecode/remove_exceptions.cpp | 30 ++++++++++++------ src/util/irep_ids.def | 1 + 8 files changed, 56 insertions(+), 10 deletions(-) create mode 100644 jbmc/regression/jbmc/must-not-throw-annotation/Test.class create mode 100644 jbmc/regression/jbmc/must-not-throw-annotation/Test.java create mode 100644 jbmc/regression/jbmc/must-not-throw-annotation/org/cprover/MustNotThrow.class create mode 100644 jbmc/regression/jbmc/must-not-throw-annotation/org/cprover/MustNotThrow.java create mode 100644 jbmc/regression/jbmc/must-not-throw-annotation/test.desc diff --git a/jbmc/regression/jbmc/must-not-throw-annotation/Test.class b/jbmc/regression/jbmc/must-not-throw-annotation/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..cd2a1c01b968f763f07669fe090f8b6d041a1dbc GIT binary patch literal 773 zcmYjPT~AX%5Ix%uw!K{1(%M=<6cDwbu`j$qj07Pu7D#Mk0x#tDc2gGHdz-!6>Tlr> z@QfzbNFwk4DC5i(T3=>%XU@zyGrPb4{QL!A6E7XOcqp-y!6OF=Ja*tt9LJ=GBqCjv9uI?(pDK(e;}Q6RM&c9cNAp#ya| z?6;L^F<2niA4c{x2<@poGvQ}}#Sg>4>b`mxjC7<4vlCF(izx&a8lmad{ecNb%G3|2 z_As<9uG}J$zNZ6$xu*5}PY2#0rXc+SnQgy!tH)`EL*uJ`&FtBhitMX%Z{)eiqd@)n zT<>{7w|=W*?~AVn%q}30&XzmMGmNddC~-k)S`f?Nsa(t;tq{%wOn4_2r zN#e^S`#wb_68jR>9R0=z6N1gS1u$Q9zGLl|Pzy!q1K$kE8X%-;K#J~yw8s{pl literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/must-not-throw-annotation/org/cprover/MustNotThrow.java b/jbmc/regression/jbmc/must-not-throw-annotation/org/cprover/MustNotThrow.java new file mode 100644 index 00000000000..ab5edbe35f9 --- /dev/null +++ b/jbmc/regression/jbmc/must-not-throw-annotation/org/cprover/MustNotThrow.java @@ -0,0 +1,3 @@ +package org.cprover; + +public @interface MustNotThrow { } diff --git a/jbmc/regression/jbmc/must-not-throw-annotation/test.desc b/jbmc/regression/jbmc/must-not-throw-annotation/test.desc new file mode 100644 index 00000000000..a39e4029a74 --- /dev/null +++ b/jbmc/regression/jbmc/must-not-throw-annotation/test.desc @@ -0,0 +1,8 @@ +CORE +Test.class +--function Test.main +^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 a6f2996a215..67809f059a7 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -406,6 +406,13 @@ void java_bytecode_convert_method_lazy( // Not used in jbmc at present, but other codebases that use jbmc as a library // use this information. method_symbol.type.set(ID_C_abstract, m.is_abstract); + + if(java_bytecode_parse_treet::find_annotation( + m.annotations, "java::org.cprover.MustNotThrow")) + { + method_symbol.type.set(ID_C_must_not_throw, true); + } + symbol_table.add(method_symbol); } diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp index 25ee5b2985c..fb398919736 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.cpp +++ b/jbmc/src/java_bytecode/remove_exceptions.cpp @@ -432,19 +432,29 @@ bool remove_exceptionst::instrument_function_call( if(function_may_throw(callee_id)) { - add_exception_dispatch_sequence( - goto_program, instr_it, stack_catch, locals); - - // add a null check (so that instanceof can be applied) - equal_exprt eq_null( + equal_exprt no_exception_currently_in_flight( get_inflight_exception_global(), null_pointer_exprt(pointer_type(empty_typet()))); - goto_programt::targett t_null=goto_program.insert_after(instr_it); - t_null->make_goto(next_it); - t_null->source_location=instr_it->source_location; - t_null->function=instr_it->function; - t_null->guard=eq_null; + if(symbol_table.lookup_ref(callee_id).type.get_bool(ID_C_must_not_throw)) + { + // Function is annotated must-not-throw, but we can't prove that here. + // Insert an ASSUME(@inflight_exception == null): + goto_programt::targett assume_null = goto_program.insert_after(instr_it); + assume_null->make_assumption(no_exception_currently_in_flight); + } + else + { + add_exception_dispatch_sequence( + goto_program, instr_it, stack_catch, locals); + + // add a null check (so that instanceof can be applied) + goto_programt::targett t_null=goto_program.insert_after(instr_it); + t_null->make_goto(next_it); + t_null->source_location=instr_it->source_location; + t_null->function=instr_it->function; + t_null->guard=no_exception_currently_in_flight; + } return true; } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index bf10417a60b..99e1374dec5 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -670,6 +670,7 @@ IREP_ID_ONE(bits_per_byte) IREP_ID_TWO(C_abstract, #abstract) IREP_ID_ONE(synthetic) IREP_ID_ONE(interface) +IREP_ID_TWO(C_must_not_throw, #must_not_throw) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.h in their source tree and