Skip to content

Commit 8e6244c

Browse files
peterschrammelpeterschrammel
authored
Merge pull request diffblue#2043 from peterschrammel/fail-on-uncaught-exception
JBMC report FAILURE on uncaught exception
2 parents ec3010f + cd2ef4b commit 8e6244c

File tree

45 files changed

+206
-131
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

45 files changed

+206
-131
lines changed

‎jbmc/regression/jbmc-strings/max-length/test1.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ Test.class
33
--refine-strings --verbosity 10 --string-max-input-length 499999 --function Test.checkMaxInputLength
44
^EXIT=0$
55
^SIGNAL=0$
6-
assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 16: SUCCESS
6+
assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 17: SUCCESS

‎jbmc/regression/jbmc-strings/max-length/test2.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ Test.class
33
--refine-strings --verbosity 10 --string-max-input-length 500000 --function Test.checkMaxInputLength
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 16: FAILURE
6+
assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 17: FAILURE

‎jbmc/regression/jbmc-strings/max-length/test3.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ Test.class
33
--refine-strings --verbosity 10 --string-max-length 4001 --function Test.checkMaxLength
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 26: FAILURE
6+
assertion.* line 25 function java::Test.checkMaxLength.* bytecode-index 27: FAILURE

‎jbmc/regression/jbmc/ClassCastException2/A.class

-52 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ClassCastException2/B.class

-52 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ClassCastException2/C.class

-52 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/ClassCastException2/ClassCastExceptionTest.class

-251 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/assert3/test_throw_no_uncaught.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
assert3.class
3+
--throw-assertion-error --disable-uncaught-exception-check
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎jbmc/regression/jbmc/assert7/Test.class

300 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/assert7/Test.java

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
class Test
2+
{
3+
public static void main(String[] args)
4+
{
5+
AssertionError a = new AssertionError();
6+
if(false)
7+
throw a;
8+
}
9+
}

‎jbmc/regression/jbmc/assert7/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
Test.class
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎jbmc/regression/jbmc/catch1/catch1.class

0 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/catch1/test.desc

+3-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,9 @@
11
CORE
22
catch1.class
33

4-
^EXIT=0$
4+
^EXIT=10$
55
^SIGNAL=0$
6-
^VERIFICATION SUCCESSFUL$
6+
^VERIFICATION FAILED$
7+
^\[.*\] no uncaught exception: FAILURE$
78
--
89
^warning: ignoring

‎jbmc/regression/jbmc/catch1/test_no_uncaught_exceptions.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
catch1.class
3+
--disable-uncaught-exception-check
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎jbmc/regression/jbmc/exceptions18/test.desc

+3-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,9 @@
11
CORE
22
Test.class
33
--function Test.goo
4-
^EXIT=0$
4+
^EXIT=10$
55
^SIGNAL=0$
6-
^VERIFICATION SUCCESSFUL$
6+
^VERIFICATION FAILED$
7+
no uncaught exception: FAILURE
78
--
89
^warning: ignoring

‎jbmc/regression/jbmc/exceptions23/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ test.class
44
^EXIT=10$
55
^SIGNAL=0$
66
VERIFICATION FAILED
7-
assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 12: FAILURE
7+
assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 13: FAILURE
88
--
99
^warning: ignoring
1010
--

‎jbmc/regression/jbmc/exceptions24/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ test.class
44
^EXIT=10$
55
^SIGNAL=0$
66
VERIFICATION FAILED
7-
assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 10: FAILURE
7+
assertion at file test\.java line 9 function java::test\.main:\(\)V bytecode-index 11: FAILURE
88
--
99
^warning: ignoring
1010
--

‎jbmc/regression/jbmc/finally1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ test.class
33
--function test.main
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 9: FAILURE
6+
assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 10: FAILURE
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

‎jbmc/regression/jbmc/finally2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ test.class
33
--function test.main
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 9: FAILURE
6+
assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 10: FAILURE
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

‎jbmc/regression/jbmc/finally3/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ test.class
33
--function test.main
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 9: SUCCESS
7-
assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 22: FAILURE
6+
assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 10: SUCCESS
7+
assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 23: FAILURE
88
^VERIFICATION FAILED$
99
--
1010
^warning: ignoring

‎jbmc/regression/jbmc/finally4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ test.class
33
--function test.main
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file test\.java line 11 function java::test\.main:\(\)V bytecode-index 7: FAILURE
6+
assertion at file test\.java line 11 function java::test\.main:\(\)V bytecode-index 8: FAILURE
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

‎jbmc/regression/jbmc/finally5/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ test.class
33
--function test.main
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 12: FAILURE
6+
assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 13: FAILURE
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

‎jbmc/regression/jbmc/finally6/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ test.class
33
--function test.main
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 12: FAILURE
6+
assertion at file test\.java line 8 function java::test\.main:\(\)V bytecode-index 13: FAILURE
77
^VERIFICATION FAILED$
88
--
99
^warning: ignoring

‎jbmc/regression/jbmc/finally7/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ test.class
33
--function test.main
44
^EXIT=10$
55
^SIGNAL=0$
6-
assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 12: SUCCESS
7-
assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 25: FAILURE
6+
assertion at file test\.java line 7 function java::test\.main:\(\)V bytecode-index 13: SUCCESS
7+
assertion at file test\.java line 10 function java::test\.main:\(\)V bytecode-index 26: FAILURE
88
^VERIFICATION FAILED$
99
--
1010
^warning: ignoring

‎jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,9 @@ Main.class
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
assertion at file Main\.java line 5 function .* bytecode-index 6: FAILURE
8-
assertion at file Main\.java line 6 function .* bytecode-index 14: FAILURE
9-
assertion at file Main\.java line 12 function .* bytecode-index 31: SUCCESS
7+
assertion at file Main\.java line 5 function .* bytecode-index 7: FAILURE
8+
assertion at file Main\.java line 6 function .* bytecode-index 15: FAILURE
9+
assertion at file Main\.java line 12 function .* bytecode-index 32: SUCCESS
1010
\*\* 2 of .* failed
1111
--
1212
^warning: ignoring

‎jbmc/regression/jbmc/no-main-multi-array-maybe-null1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Main.class
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE
7+
assertion at file Main\.java line 5 function .* bytecode-index 25: FAILURE
88
\*\* 1 of .* failed
99
--
1010
^warning: ignoring

‎jbmc/regression/jbmc/no-main-multi-array-maybe-null2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Main.class
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE
7+
assertion at file Main\.java line 5 function .* bytecode-index 25: FAILURE
88
\*\* 1 of .* failed
99
--
1010
^warning: ignoring

‎jbmc/regression/jbmc/no-main-object-array-elements-maybe-null1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Main.class
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
assertion at file Main\.java line 6 function .* bytecode-index 13: FAILURE
7+
assertion at file Main\.java line 6 function .* bytecode-index 14: FAILURE
88
\*\* 1 of .* failed
99
--
1010
^warning: ignoring

‎jbmc/regression/jbmc/no-main-object-array-elements-maybe-null2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Main.class
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
assertion at file Main\.java line 6 function .* bytecode-index 13: FAILURE
7+
assertion at file Main\.java line 6 function .* bytecode-index 14: FAILURE
88
\*\* 1 of .* failed
99
--
1010
^warning: ignoring

‎jbmc/regression/jbmc/no-main-object-array-maybe-null1/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ Main.class
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
assertion at file Main\.java line 10 function .* bytecode-index 6: FAILURE
8-
assertion at file Main\.java line 14 function .* bytecode-index 26: FAILURE
7+
assertion at file Main\.java line 10 function .* bytecode-index 7: FAILURE
8+
assertion at file Main\.java line 14 function .* bytecode-index 27: FAILURE
99
\*\* 2 of .* failed
1010
--
1111
^warning: ignoring

‎jbmc/regression/jbmc/no-main-object-array-maybe-null2/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ Main.class
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7-
assertion at file Main\.java line 10 function .* bytecode-index 6: FAILURE
8-
assertion at file Main\.java line 14 function .* bytecode-index 26: FAILURE
7+
assertion at file Main\.java line 10 function .* bytecode-index 7: FAILURE
8+
assertion at file Main\.java line 14 function .* bytecode-index 27: FAILURE
99
\*\* 2 of .* failed
1010
--
1111
^warning: ignoring

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

+39-4
Original file line numberDiff line numberDiff line change
@@ -32,11 +32,14 @@ Author: Daniel Kroening, [email protected]
3232
#include <util/simplify_expr.h>
3333
#include <util/std_expr.h>
3434
#include <util/string2int.h>
35+
#include <util/string_constant.h>
3536

3637
#include <goto-programs/cfg.h>
3738
#include <goto-programs/class_hierarchy.h>
3839
#include <goto-programs/resolve_inherited_component.h>
40+
3941
#include <analyses/cfg_dominators.h>
42+
#include <analyses/uncaught_exceptions_analysis.h>
4043

4144
#include <limits>
4245
#include <algorithm>
@@ -2248,10 +2251,40 @@ void java_bytecode_convert_methodt::convert_athrow(
22482251
codet &c,
22492252
exprt::operandst &results) const
22502253
{
2251-
side_effect_expr_throwt throw_expr;
2252-
throw_expr.add_source_location() = location;
2253-
throw_expr.copy_to_operands(op[0]);
2254-
c = code_expressiont(throw_expr);
2254+
if(
2255+
!throw_assertion_error &&
2256+
uncaught_exceptions_domaint::get_exception_type(op[0].type()) ==
2257+
"java::java.lang.AssertionError")
2258+
{
2259+
// we translate athrow into
2260+
// ASSERT false;
2261+
// ASSUME false:
2262+
code_assertt assert_code;
2263+
assert_code.assertion() = false_exprt();
2264+
source_locationt assert_location = location; // copy
2265+
assert_location.set_comment("assertion at " + location.as_string());
2266+
assert_location.set("user-provided", true);
2267+
assert_location.set_property_class(ID_assertion);
2268+
assert_code.add_source_location() = assert_location;
2269+
2270+
code_assumet assume_code;
2271+
assume_code.assumption() = false_exprt();
2272+
source_locationt assume_location = location; // copy
2273+
assume_location.set("user-provided", true);
2274+
assume_code.add_source_location() = assume_location;
2275+
2276+
code_blockt ret_block;
2277+
ret_block.move_to_operands(assert_code);
2278+
ret_block.move_to_operands(assume_code);
2279+
c = ret_block;
2280+
}
2281+
else
2282+
{
2283+
side_effect_expr_throwt throw_expr;
2284+
throw_expr.add_source_location() = location;
2285+
throw_expr.copy_to_operands(op[0]);
2286+
c = code_expressiont(throw_expr);
2287+
}
22552288
results[0] = op[0];
22562289
}
22572290

@@ -3055,6 +3088,7 @@ void java_bytecode_convert_method(
30553088
symbol_table_baset &symbol_table,
30563089
message_handlert &message_handler,
30573090
size_t max_array_length,
3091+
bool throw_assertion_error,
30583092
optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
30593093
java_string_library_preprocesst &string_preprocess,
30603094
const class_hierarchyt &class_hierarchy)
@@ -3073,6 +3107,7 @@ void java_bytecode_convert_method(
30733107
symbol_table,
30743108
message_handler,
30753109
max_array_length,
3110+
throw_assertion_error,
30763111
needed_lazy_methods,
30773112
string_preprocess,
30783113
class_hierarchy);

‎jbmc/src/java_bytecode/java_bytecode_convert_method.h

+1
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,7 @@ void java_bytecode_convert_method(
3333
symbol_table_baset &symbol_table,
3434
message_handlert &message_handler,
3535
size_t max_array_length,
36+
bool throw_assertion_error,
3637
optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
3738
java_string_library_preprocesst &string_preprocess,
3839
const class_hierarchyt &class_hierarchy);

‎jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

+3
Original file line numberDiff line numberDiff line change
@@ -36,12 +36,14 @@ class java_bytecode_convert_methodt:public messaget
3636
symbol_table_baset &symbol_table,
3737
message_handlert &_message_handler,
3838
size_t _max_array_length,
39+
bool throw_assertion_error,
3940
optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
4041
java_string_library_preprocesst &_string_preprocess,
4142
const class_hierarchyt &class_hierarchy)
4243
: messaget(_message_handler),
4344
symbol_table(symbol_table),
4445
max_array_length(_max_array_length),
46+
throw_assertion_error(throw_assertion_error),
4547
needed_lazy_methods(std::move(needed_lazy_methods)),
4648
string_preprocess(_string_preprocess),
4749
slots_for_parameters(0),
@@ -64,6 +66,7 @@ class java_bytecode_convert_methodt:public messaget
6466
protected:
6567
symbol_table_baset &symbol_table;
6668
const size_t max_array_length;
69+
const bool throw_assertion_error;
6770
optionalt<ci_lazy_methods_neededt> needed_lazy_methods;
6871

6972
/// Fully qualified name of the method under translation.

‎jbmc/src/java_bytecode/java_bytecode_instrument.cpp

+22
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ Date: June 2017
1919
#include <goto-programs/goto_functions.h>
2020

2121
#include "java_bytecode_convert_class.h"
22+
#include "java_entry_point.h"
2223
#include "java_utils.h"
2324

2425
class java_bytecode_instrumentt:public messaget
@@ -592,6 +593,27 @@ void java_bytecode_instrument_symbol(
592593
instrument(to_code(symbol.value));
593594
}
594595

596+
/// Instruments the start function with an assertion that checks whether
597+
/// an exception has escaped the entry point
598+
/// \param init_code: the code block to which the assertion is appended
599+
/// \param exc_symbol: the top-level exception symbol
600+
/// \param source_location: the source location to attach to the assertion
601+
void java_bytecode_instrument_uncaught_exceptions(
602+
codet &init_code,
603+
const symbolt &exc_symbol,
604+
const source_locationt &source_location)
605+
{
606+
// check that there is no uncaught exception
607+
code_assertt assert_no_exception;
608+
assert_no_exception.assertion() = equal_exprt(
609+
exc_symbol.symbol_expr(),
610+
null_pointer_exprt(to_pointer_type(exc_symbol.type)));
611+
source_locationt assert_location = source_location;
612+
assert_location.set_comment("no uncaught exception");
613+
assert_no_exception.add_source_location() = assert_location;
614+
init_code.move_to_operands(assert_no_exception);
615+
}
616+
595617
/// Instruments all the code in the symbol_table with
596618
/// runtime exceptions or corresponding assertions.
597619
/// Exceptions are thrown when the `throw_runtime_exceptions` flag is set.

‎jbmc/src/java_bytecode/java_bytecode_instrument.h

+7
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,8 @@ Date: June 2017
1515
#include <util/message.h>
1616
#include <util/irep.h>
1717

18+
class codet;
19+
1820
void java_bytecode_instrument_symbol(
1921
symbol_table_baset &symbol_table,
2022
symbolt &symbol,
@@ -26,6 +28,11 @@ void java_bytecode_instrument(
2628
const bool throw_runtime_exceptions,
2729
message_handlert &_message_handler);
2830

31+
void java_bytecode_instrument_uncaught_exceptions(
32+
codet &init_code,
33+
const symbolt &exc_symbol,
34+
const source_locationt &source_location);
35+
2936
extern const std::vector<std::string> exception_needed_classes;
3037

3138
#endif

0 commit comments

Comments
 (0)