From 27b4597494f14ca59d9c3779a1418283e1f23ee3 Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 11 May 2017 15:13:10 +0100 Subject: [PATCH 01/13] Add instrumentation that throws exceptions --- .../java_bytecode_convert_method.cpp | 203 ++++++++++++++++++ .../java_bytecode_convert_method_class.h | 18 ++ 2 files changed, 221 insertions(+) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 9e295f2dcc6..811aa5a0a46 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -570,6 +570,209 @@ codet java_bytecode_convert_methodt::get_array_bounds_check( /*******************************************************************\ +Function: get_array_access_check + + Inputs: + + Outputs: + + Purpose: Checks whether the array access array_struct[idx] + is out-of-bounds, and throws ArrayIndexOutofBoundsException + if necessary + +\*******************************************************************/ + +codet java_bytecode_convert_methodt::get_array_access_check( + const exprt &array_struct, + const exprt &idx, + const source_locationt &original_sloc) +{ + symbolt exc_symbol; + if(!symbol_table.has_symbol("ArrayIndexOutOfBoundsException")) + { + exc_symbol.is_static_lifetime=true; + exc_symbol.base_name="ArrayIndexOutOfBoundsException"; + exc_symbol.name="ArrayIndexOutOfBoundsException"; + exc_symbol.mode=ID_java; + exc_symbol.type=typet(ID_pointer, empty_typet()); + symbol_table.add(exc_symbol); + } + else + exc_symbol=symbol_table.lookup("ArrayIndexOutOfBoundsException"); + + const symbol_exprt &exc=exc_symbol.symbol_expr(); + side_effect_expr_throwt throw_expr; + throw_expr.add_source_location()=original_sloc; + throw_expr.copy_to_operands(exc); + + const constant_exprt &zero=from_integer(0, java_int_type()); + const binary_relation_exprt lt_zero(idx, ID_lt, zero); + const member_exprt length_field(array_struct, "length", java_int_type()); + const binary_relation_exprt ge_length(idx, ID_ge, length_field); + const and_exprt and_expr(lt_zero, ge_length); + + code_ifthenelset if_code; + if_code.add_source_location()=original_sloc; + if_code.cond()=and_expr; + if_code.then_case()=code_expressiont(throw_expr); + + return if_code; +} + +/*******************************************************************\ + +Function: get_array_length_check + + Inputs: + + Outputs: + + Purpose: Throws NegativeArraySizeException when necessary + +\*******************************************************************/ + +codet java_bytecode_convert_methodt::get_array_length_check( + const exprt &length, + const source_locationt &original_sloc) +{ + symbolt exc_symbol; + if(!symbol_table.has_symbol("NegativeArraySizeException")) + { + exc_symbol.is_static_lifetime=true; + exc_symbol.base_name="NegativeArraySizeException"; + exc_symbol.name="NegativeArraySizeException"; + exc_symbol.mode=ID_java; + exc_symbol.type=typet(ID_pointer, empty_typet()); + symbol_table.add(exc_symbol); + } + else + exc_symbol=symbol_table.lookup("NegativeArraySizeException"); + + const symbol_exprt &exc=exc_symbol.symbol_expr(); + side_effect_expr_throwt throw_expr; + throw_expr.add_source_location()=original_sloc; + throw_expr.copy_to_operands(exc); + + const constant_exprt &zero=from_integer(0, java_int_type()); + const binary_relation_exprt ge_zero(length, ID_ge, zero); + + code_ifthenelset if_code; + if_code.add_source_location()=original_sloc; + if_code.cond()=ge_zero; + if_code.then_case()=code_expressiont(throw_expr); + + return if_code; +} + +/*******************************************************************\ + +Function: get_null_dereference_check + + Inputs: + + Outputs: + + Purpose: Checks whether expr is null, and throws + NullPointerException if necessary + +\*******************************************************************/ + +codet java_bytecode_convert_methodt::get_null_dereference_check( + const exprt &expr, + const source_locationt &original_sloc) +{ + symbolt exc_symbol; + if(!symbol_table.has_symbol("ArrayIndexOutOfBoundsException")) + { + exc_symbol.is_static_lifetime=true; + exc_symbol.base_name="NullPointerException"; + exc_symbol.name="NullPointerException"; + exc_symbol.mode=ID_java; + exc_symbol.type=typet(ID_pointer, empty_typet()); + symbol_table.add(exc_symbol); + } + else + exc_symbol=symbol_table.lookup("NullPointerException"); + + const symbol_exprt &exc=exc_symbol.symbol_expr(); + + side_effect_expr_throwt throw_expr; + throw_expr.add_source_location()=original_sloc; + throw_expr.copy_to_operands(exc); + + const equal_exprt equal_expr( + expr, + null_pointer_exprt(pointer_typet(empty_typet()))); + code_ifthenelset if_code; + if_code.add_source_location()=original_sloc; + if_code.cond()=equal_expr; + if_code.then_case()=code_expressiont(throw_expr); + + return if_code; +} + + +/*******************************************************************\ + +Function: get_class_cast_check + + Inputs: + + Outputs: + + Purpose: Throws ClassCastException when necessary + +\*******************************************************************/ + +codet java_bytecode_convert_methodt::get_class_cast_check( + const exprt &class1, + const exprt &class2, + const source_locationt &original_sloc) +{ + // TODO: use std::move + + symbolt exc_symbol; + if(!symbol_table.has_symbol("ClassCastException")) + { + exc_symbol.is_static_lifetime=true; + exc_symbol.base_name="ClassCastException"; + exc_symbol.name="ClassCastException"; + exc_symbol.mode=ID_java; + exc_symbol.type=typet(ID_pointer, empty_typet()); + symbol_table.add(exc_symbol); + } + else + exc_symbol=symbol_table.lookup("ClassCastException"); + + const symbol_exprt &exc=exc_symbol.symbol_expr(); + + side_effect_expr_throwt throw_expr; + throw_expr.add_source_location()=original_sloc; + throw_expr.copy_to_operands(exc); + + binary_predicate_exprt class_cast_check( + class1, ID_java_instanceof, class2); + + empty_typet voidt; + pointer_typet voidptr(voidt); + exprt null_check_op=class1; + if(null_check_op.type()!=voidptr) + null_check_op.make_typecast(voidptr); + notequal_exprt op_not_null(null_check_op, null_pointer_exprt(voidptr)); + + // checkcast passes when the operand is null + and_exprt and_expr(op_not_null, class_cast_check); + + code_ifthenelset if_code; + if_code.add_source_location()=original_sloc; + if_code.cond()=and_expr; + if_code.then_case()=code_expressiont(throw_expr); + + return if_code; +} + +/*******************************************************************\ + Function: replace_goto_target Inputs: 'repl', a block of code in which to perform replacement, and diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h index da9196e6a67..f936d4c55f3 100644 --- a/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/src/java_bytecode/java_bytecode_convert_method_class.h @@ -106,6 +106,24 @@ class java_bytecode_convert_methodt:public messaget const exprt &idx, const source_locationt &original_sloc); + codet get_array_access_check( + const exprt &arraystruct, + const exprt &idx, + const source_locationt &original_sloc); + + codet get_array_length_check( + const exprt &length, + const source_locationt &original_sloc); + + codet get_null_dereference_check( + const exprt &expr, + const source_locationt &original_sloc); + + codet get_class_cast_check( + const exprt &class1, + const exprt &class2, + const source_locationt &original_sloc); + // return corresponding reference of variable const variablet &find_variable_for_slot( size_t address, From b8d94157f0941bbc0d4465ee339e7b7b4045e0bf Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 11 May 2017 17:27:48 +0100 Subject: [PATCH 02/13] Add --java-throw-runtime-exceptions flag --- src/cbmc/cbmc_parse_options.h | 1 + src/java_bytecode/java_bytecode_convert_method.h | 5 ++++- src/java_bytecode/java_bytecode_convert_method_class.h | 3 +++ src/java_bytecode/java_bytecode_language.cpp | 8 ++++++-- src/java_bytecode/java_bytecode_language.h | 4 +++- 5 files changed, 17 insertions(+), 4 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 2c54dfc7353..e6e47fba84a 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -61,6 +61,7 @@ class optionst; "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \ "(graphml-witness):" \ "(java-max-vla-length):(java-unwind-enum-static)" \ + "(java-throw-runtime-exceptions)" \ "(java-cp-include-files):" \ "(localize-faults)(localize-faults-method):" \ "(lazy-methods)" \ diff --git a/src/java_bytecode/java_bytecode_convert_method.h b/src/java_bytecode/java_bytecode_convert_method.h index db6fcc729e1..b9a863184ee 100644 --- a/src/java_bytecode/java_bytecode_convert_method.h +++ b/src/java_bytecode/java_bytecode_convert_method.h @@ -24,6 +24,7 @@ void java_bytecode_convert_method( symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, + bool throw_runtime_exceptions, safe_pointer lazy_methods); inline void java_bytecode_convert_method( @@ -31,7 +32,8 @@ inline void java_bytecode_convert_method( const java_bytecode_parse_treet::methodt &method, symbol_tablet &symbol_table, message_handlert &message_handler, - size_t max_array_length) + size_t max_array_length, + bool throw_runtime_exceptions) { java_bytecode_convert_method( class_symbol, @@ -39,6 +41,7 @@ inline void java_bytecode_convert_method( symbol_table, message_handler, max_array_length, + throw_runtime_exceptions, safe_pointer::create_null()); } diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h index f936d4c55f3..589a76bcc0e 100644 --- a/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/src/java_bytecode/java_bytecode_convert_method_class.h @@ -32,10 +32,12 @@ class java_bytecode_convert_methodt:public messaget symbol_tablet &_symbol_table, message_handlert &_message_handler, size_t _max_array_length, + bool _throw_runtime_exceptions, safe_pointer _lazy_methods): messaget(_message_handler), symbol_table(_symbol_table), max_array_length(_max_array_length), + throw_runtime_exceptions(_throw_runtime_exceptions), lazy_methods(_lazy_methods) { } @@ -54,6 +56,7 @@ class java_bytecode_convert_methodt:public messaget protected: symbol_tablet &symbol_table; const size_t max_array_length; + const bool throw_runtime_exceptions; safe_pointer lazy_methods; irep_idt method_id; diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 69f9f3eb2a4..f408419e27e 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -42,6 +42,7 @@ Function: java_bytecode_languaget::get_language_options void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) { + throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions"); assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null"); string_refinement_enabled=cmd.isset("refine-strings"); if(cmd.isset("java-max-input-array-length")) @@ -551,7 +552,8 @@ bool java_bytecode_languaget::typecheck( *method_sig.second.second, symbol_table, get_message_handler(), - max_user_array_length); + max_user_array_length, + throw_runtime_exceptions); } } // Otherwise our caller is in charge of elaborating methods on demand. @@ -678,6 +680,7 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion( symbol_table, get_message_handler(), max_user_array_length, + throw_runtime_exceptions, safe_pointer::create_non_null(&lazy_methods)); gather_virtual_callsites( symbol_table.lookup(mname).value, @@ -788,7 +791,8 @@ void java_bytecode_languaget::convert_lazy_method( *lazy_method_entry.second, symtab, get_message_handler(), - max_user_array_length); + max_user_array_length, + throw_runtime_exceptions); } /*******************************************************************\ diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index 2da26b71ad6..c380ccbbc3b 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -56,7 +56,8 @@ class java_bytecode_languaget:public languaget virtual ~java_bytecode_languaget(); java_bytecode_languaget(): max_nondet_array_length(MAX_NONDET_ARRAY_LENGTH_DEFAULT), - max_user_array_length(0) + max_user_array_length(0), + throw_runtime_exceptions(false) {} bool from_expr( @@ -96,6 +97,7 @@ class java_bytecode_languaget:public languaget bool assume_inputs_non_null; // assume inputs variables to be non-null size_t max_nondet_array_length; // maximal length for non-det array creation size_t max_user_array_length; // max size for user code created arrays + bool throw_runtime_exceptions; lazy_methodst lazy_methods; lazy_methods_modet lazy_methods_mode; bool string_refinement_enabled; From 17575c552e18b19f56978a62e097f61417d71434 Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 11 May 2017 17:31:47 +0100 Subject: [PATCH 03/13] Add instrumentation for throwing NullPointerException and ClassCastException --- .../java_bytecode_convert_method.cpp | 95 +++++++++++-------- 1 file changed, 57 insertions(+), 38 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 811aa5a0a46..449df11ea6b 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -681,21 +681,20 @@ codet java_bytecode_convert_methodt::get_null_dereference_check( const exprt &expr, const source_locationt &original_sloc) { - symbolt exc_symbol; - if(!symbol_table.has_symbol("ArrayIndexOutOfBoundsException")) + symbolt exc_symbol; + if(!symbol_table.has_symbol("NullPointerException")) { exc_symbol.is_static_lifetime=true; exc_symbol.base_name="NullPointerException"; - exc_symbol.name="NullPointerException"; + exc_symbol.name="NullPointerException"; exc_symbol.mode=ID_java; exc_symbol.type=typet(ID_pointer, empty_typet()); symbol_table.add(exc_symbol); } else exc_symbol=symbol_table.lookup("NullPointerException"); - - const symbol_exprt &exc=exc_symbol.symbol_expr(); - + + const symbol_exprt &exc=exc_symbol.symbol_expr(); side_effect_expr_throwt throw_expr; throw_expr.add_source_location()=original_sloc; throw_expr.copy_to_operands(exc); @@ -707,11 +706,10 @@ codet java_bytecode_convert_methodt::get_null_dereference_check( if_code.add_source_location()=original_sloc; if_code.cond()=equal_expr; if_code.then_case()=code_expressiont(throw_expr); - + return if_code; } - /*******************************************************************\ Function: get_class_cast_check @@ -1563,49 +1561,68 @@ codet java_bytecode_convert_methodt::convert_instructions( { assert(op.size()==1 && results.size()==1); code_blockt block; - // TODO throw NullPointerException instead - const typecast_exprt lhs(op[0], pointer_typet(empty_typet())); - const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type()))); - const exprt not_equal_null( - binary_relation_exprt(lhs, ID_notequal, rhs)); - code_assertt check(not_equal_null); - check.add_source_location() - .set_comment("Throw null"); - check.add_source_location() - .set_property_class("null-pointer-exception"); - block.move_to_operands(check); + if(throw_runtime_exceptions) + { + codet null_dereference_check=get_null_dereference_check( + op[0], + i_it->source_location); + block.move_to_operands(null_dereference_check); + } + else + { + const typecast_exprt lhs(op[0], pointer_typet(empty_typet())); + const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type()))); + const exprt not_equal_null( + binary_relation_exprt(lhs, ID_notequal, rhs)); + code_assertt check(not_equal_null); + check.add_source_location() + .set_comment("Throw null"); + check.add_source_location() + .set_property_class("null-pointer-exception"); + block.move_to_operands(check); + } side_effect_expr_throwt throw_expr; throw_expr.add_source_location()=i_it->source_location; throw_expr.copy_to_operands(op[0]); c=code_expressiont(throw_expr); - results[0]=op[0]; - block.move_to_operands(c); - c=block; + + results[0]=op[0]; + c=std::move(block); } else if(statement=="checkcast") { // checkcast throws an exception in case a cast of object // on stack to given type fails. // The stack isn't modified. - // TODO: convert assertions to exceptions. assert(op.size()==1 && results.size()==1); - binary_predicate_exprt check(op[0], ID_java_instanceof, arg0); - code_assertt assert_class(check); - assert_class.add_source_location().set_comment("Dynamic cast check"); - assert_class.add_source_location().set_property_class("bad-dynamic-cast"); - // checkcast passes when the operand is null. - empty_typet voidt; - pointer_typet voidptr(voidt); - exprt null_check_op=op[0]; - if(null_check_op.type()!=voidptr) - null_check_op.make_typecast(voidptr); - code_ifthenelset conditional_check; - notequal_exprt op_not_null(null_check_op, null_pointer_exprt(voidptr)); - conditional_check.cond()=std::move(op_not_null); - conditional_check.then_case()=std::move(assert_class); - c=std::move(conditional_check); + if(throw_runtime_exceptions) + { + codet conditional_check= + get_class_cast_check(op[0], arg0, i_it->source_location); + c=std::move(conditional_check); + } + else + { + binary_predicate_exprt check(op[0], ID_java_instanceof, arg0); + code_assertt assert_class(check); + assert_class.add_source_location(). + set_comment("Dynamic cast check"); + assert_class.add_source_location(). + set_property_class("bad-dynamic-cast"); + // checkcast passes when the operand is null. + empty_typet voidt; + pointer_typet voidptr(voidt); + exprt null_check_op=op[0]; + if(null_check_op.type()!=voidptr) + null_check_op.make_typecast(voidptr); + code_ifthenelset conditional_check; + notequal_exprt op_not_null(null_check_op, null_pointer_exprt(voidptr)); + conditional_check.cond()=std::move(op_not_null); + conditional_check.then_case()=std::move(assert_class); + c=std::move(conditional_check); + } results[0]=op[0]; } else if(statement=="invokedynamic") @@ -2970,6 +2987,7 @@ void java_bytecode_convert_method( symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, + bool throw_runtime_exceptions, safe_pointer lazy_methods) { static const std::unordered_set methods_to_ignore @@ -2999,6 +3017,7 @@ void java_bytecode_convert_method( symbol_table, message_handler, max_array_length, + throw_runtime_exceptions, lazy_methods); java_bytecode_convert_method(class_symbol, method); From adb3b18dcfae8dd530be4349646cd15709fd1d3b Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 11 May 2017 18:36:57 +0100 Subject: [PATCH 04/13] Add instrumentation for NegativeArraySizeException --- .../java_bytecode_convert_method.cpp | 45 +++++++++++-------- 1 file changed, 27 insertions(+), 18 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 449df11ea6b..246c3183d5d 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -724,26 +724,25 @@ Function: get_class_cast_check codet java_bytecode_convert_methodt::get_class_cast_check( const exprt &class1, - const exprt &class2, + const exprt &class2, const source_locationt &original_sloc) { // TODO: use std::move - - symbolt exc_symbol; + symbolt exc_symbol; if(!symbol_table.has_symbol("ClassCastException")) { exc_symbol.is_static_lifetime=true; exc_symbol.base_name="ClassCastException"; - exc_symbol.name="ClassCastException"; + exc_symbol.name="ClassCastException"; exc_symbol.mode=ID_java; exc_symbol.type=typet(ID_pointer, empty_typet()); symbol_table.add(exc_symbol); } else exc_symbol=symbol_table.lookup("ClassCastException"); - - const symbol_exprt &exc=exc_symbol.symbol_expr(); - + + const symbol_exprt &exc=exc_symbol.symbol_expr(); + side_effect_expr_throwt throw_expr; throw_expr.add_source_location()=original_sloc; throw_expr.copy_to_operands(exc); @@ -758,14 +757,14 @@ codet java_bytecode_convert_methodt::get_class_cast_check( null_check_op.make_typecast(voidptr); notequal_exprt op_not_null(null_check_op, null_pointer_exprt(voidptr)); - // checkcast passes when the operand is null + // checkcast passes when the operand is null and_exprt and_expr(op_not_null, class_cast_check); - + code_ifthenelset if_code; if_code.add_source_location()=original_sloc; if_code.cond()=and_expr; if_code.then_case()=code_expressiont(throw_expr); - + return if_code; } @@ -2453,14 +2452,24 @@ codet java_bytecode_convert_methodt::convert_instructions( java_new_array.add_source_location()=i_it->source_location; c=code_blockt(); - // TODO make this throw NegativeArrayIndexException instead. - constant_exprt intzero=from_integer(0, java_int_type()); - binary_relation_exprt gezero(op[0], ID_ge, intzero); - code_assertt check(gezero); - check.add_source_location().set_comment("Array size < 0"); - check.add_source_location() - .set_property_class("array-create-negative-size"); - c.move_to_operands(check); + + if(throw_runtime_exceptions) + { + codet array_length_check=get_array_length_check( + op[0], + i_it->source_location); + c.move_to_operands(array_length_check); + } + else + { + constant_exprt intzero=from_integer(0, java_int_type()); + binary_relation_exprt gezero(op[0], ID_ge, intzero); + code_assertt check(gezero); + check.add_source_location().set_comment("Array size < 0"); + check.add_source_location() + .set_property_class("array-create-negative-size"); + c.move_to_operands(check); + } if(max_array_length!=0) { From 58e2ca36bcb2466c1870234d4cf00351882c7ea1 Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 11 May 2017 20:08:14 +0100 Subject: [PATCH 05/13] Add instrumentation for NegativeArraySizeException --- .../java_bytecode_convert_method.cpp | 45 +++++++++++-------- 1 file changed, 27 insertions(+), 18 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 246c3183d5d..0446e942e58 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -587,12 +587,12 @@ codet java_bytecode_convert_methodt::get_array_access_check( const exprt &idx, const source_locationt &original_sloc) { - symbolt exc_symbol; + symbolt exc_symbol; if(!symbol_table.has_symbol("ArrayIndexOutOfBoundsException")) { exc_symbol.is_static_lifetime=true; exc_symbol.base_name="ArrayIndexOutOfBoundsException"; - exc_symbol.name="ArrayIndexOutOfBoundsException"; + exc_symbol.name="ArrayIndexOutOfBoundsException"; exc_symbol.mode=ID_java; exc_symbol.type=typet(ID_pointer, empty_typet()); symbol_table.add(exc_symbol); @@ -600,7 +600,7 @@ codet java_bytecode_convert_methodt::get_array_access_check( else exc_symbol=symbol_table.lookup("ArrayIndexOutOfBoundsException"); - const symbol_exprt &exc=exc_symbol.symbol_expr(); + const symbol_exprt &exc=exc_symbol.symbol_expr(); side_effect_expr_throwt throw_expr; throw_expr.add_source_location()=original_sloc; throw_expr.copy_to_operands(exc); @@ -615,7 +615,7 @@ codet java_bytecode_convert_methodt::get_array_access_check( if_code.add_source_location()=original_sloc; if_code.cond()=and_expr; if_code.then_case()=code_expressiont(throw_expr); - + return if_code; } @@ -635,12 +635,12 @@ codet java_bytecode_convert_methodt::get_array_length_check( const exprt &length, const source_locationt &original_sloc) { - symbolt exc_symbol; + symbolt exc_symbol; if(!symbol_table.has_symbol("NegativeArraySizeException")) { exc_symbol.is_static_lifetime=true; exc_symbol.base_name="NegativeArraySizeException"; - exc_symbol.name="NegativeArraySizeException"; + exc_symbol.name="NegativeArraySizeException"; exc_symbol.mode=ID_java; exc_symbol.type=typet(ID_pointer, empty_typet()); symbol_table.add(exc_symbol); @@ -648,7 +648,7 @@ codet java_bytecode_convert_methodt::get_array_length_check( else exc_symbol=symbol_table.lookup("NegativeArraySizeException"); - const symbol_exprt &exc=exc_symbol.symbol_expr(); + const symbol_exprt &exc=exc_symbol.symbol_expr(); side_effect_expr_throwt throw_expr; throw_expr.add_source_location()=original_sloc; throw_expr.copy_to_operands(exc); @@ -2501,15 +2501,24 @@ codet java_bytecode_convert_methodt::convert_instructions( if(!i_it->source_location.get_line().empty()) java_new_array.add_source_location()=i_it->source_location; - code_blockt checkandcreate; - // TODO make this throw NegativeArrayIndexException instead. - constant_exprt intzero=from_integer(0, java_int_type()); - binary_relation_exprt gezero(op[0], ID_ge, intzero); - code_assertt check(gezero); - check.add_source_location().set_comment("Array size < 0"); - check.add_source_location() - .set_property_class("array-create-negative-size"); - checkandcreate.move_to_operands(check); + c=code_blockt(); + if(throw_runtime_exceptions) + { + codet array_length_check=get_array_length_check( + op[0], + i_it->source_location); + c.move_to_operands(array_length_check); + } + else + { + constant_exprt intzero=from_integer(0, java_int_type()); + binary_relation_exprt gezero(op[0], ID_ge, intzero); + code_assertt check(gezero); + check.add_source_location().set_comment("Array size < 0"); + check.add_source_location() + .set_property_class("array-create-negative-size"); + c.move_to_operands(check); + } if(max_array_length!=0) { @@ -2517,11 +2526,11 @@ codet java_bytecode_convert_methodt::convert_instructions( from_integer(max_array_length, java_int_type()); binary_relation_exprt le_max_size(op[0], ID_le, size_limit); code_assumet assume_le_max_size(le_max_size); - checkandcreate.move_to_operands(assume_le_max_size); + c.move_to_operands(assume_le_max_size); } const exprt tmp=tmp_variable("newarray", ref_type); - c=code_assignt(tmp, java_new_array); + c.copy_to_operands(code_assignt(tmp, java_new_array)); results[0]=tmp; } else if(statement=="arraylength") From 7894cbbec6387d88a65c8813b6b246f223f9f77f Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 11 May 2017 20:12:41 +0100 Subject: [PATCH 06/13] Add instrumentation for ArrayIndexOutOfBoundsException --- src/java_bytecode/java_bytecode_convert_method.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 0446e942e58..f20971248a5 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -564,7 +564,6 @@ codet java_bytecode_convert_methodt::get_array_bounds_check( bounds_checks.operands().back().add_source_location() .set_property_class("array-index-out-of-bounds-high"); - // TODO make this throw ArrayIndexOutOfBoundsException instead of asserting. return bounds_checks; } @@ -1845,8 +1844,14 @@ codet java_bytecode_convert_methodt::convert_instructions( const dereference_exprt element(data_plus_offset, element_type); c=code_blockt(); - codet bounds_check= - get_array_bounds_check(deref, op[1], i_it->source_location); + codet bounds_check; + if(throw_runtime_exceptions) + bounds_check= + get_array_access_check(deref, op[1], i_it->source_location); + else + bounds_check= + get_array_bounds_check(deref, op[1], i_it->source_location); + bounds_check.add_source_location()=i_it->source_location; c.move_to_operands(bounds_check); code_assignt array_put(element, op[2]); From 9f9b22df75d50bb360255ce39d6e455bb7b36d2d Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 11 May 2017 20:20:26 +0100 Subject: [PATCH 07/13] Add regression test for NegativeArraySizeException --- .../NegativeArraySizeException.class | Bin 0 -> 448 bytes .../NegativeArraySizeException.java | 5 +++++ .../NegativeArraySizeException/test.desc | 8 ++++++++ 3 files changed, 13 insertions(+) create mode 100644 regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeException.class create mode 100644 regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeException.java create mode 100644 regression/cbmc-java/NegativeArraySizeException/test.desc diff --git a/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeException.class b/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeException.class new file mode 100644 index 0000000000000000000000000000000000000000..d64c39e8f14e084ae564506895d169db5892e6df GIT binary patch literal 448 zcmZ`#O-sW-5Ph@xva#CQY7QcZx9Y)Oyj2Ae1tHW!q?evHafw^fMAo#Z|H_jf;t%jg ziIY_5#qMEd-kUe`hW-Be_yTZ(z=wsdhiwl#1ou?ux;!UXy~7c~zAWw)p%v;}4QJC> znL8P0%yhyck=aNZUEx2{E+6z0VJ{r2RF-YN~801P8UF>>6un=Jbn=H0@sD(C1!WLtJ&Mzr5TYLZj literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeException.java b/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeException.java new file mode 100644 index 00000000000..08ef396b4cd --- /dev/null +++ b/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeException.java @@ -0,0 +1,5 @@ +public class NegativeArraySizeException { + public static void main(String args[]) { + int a[]=new int[-1]; + } +} diff --git a/regression/cbmc-java/NegativeArraySizeException/test.desc b/regression/cbmc-java/NegativeArraySizeException/test.desc new file mode 100644 index 00000000000..ef482f26dcb --- /dev/null +++ b/regression/cbmc-java/NegativeArraySizeException/test.desc @@ -0,0 +1,8 @@ +CORE +NegativeArraySizeException.class +--java-throw-runtime-exceptions +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring From 3ac8e40d0def810c9b790e70cd9948676a3be97c Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 11 May 2017 20:21:28 +0100 Subject: [PATCH 08/13] Add regression test for ArrayIndexOutOfBoundsException --- .../ArrayIndexOutOfBoundsException.class | Bin 0 -> 468 bytes .../ArrayIndexOutOfBoundsException.java | 6 ++++++ .../ArrayIndexOutOfBoundsException/test.desc | 8 ++++++++ 3 files changed, 14 insertions(+) create mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsException.class create mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsException.java create mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException/test.desc diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsException.class b/regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsException.class new file mode 100644 index 0000000000000000000000000000000000000000..d0368b140e8e545c6eda5608cf9ba1d335b74911 GIT binary patch literal 468 zcmaJ-O;5r=6r9%&Dir}iIU0=@)I=`cFeYj+A!+OZ!-dmQR$NlHW@!!nEKerJ_yhb= z#@AxP#juC>c4pt3ne6w^#}|MLw0ziTdf4-@Pbgg~tMG>V^L Date: Fri, 12 May 2017 10:39:09 +0100 Subject: [PATCH 09/13] Use better function names --- .../java_bytecode_convert_method.cpp | 65 +++++++++---------- .../java_bytecode_convert_method_class.h | 16 ++--- src/java_bytecode/java_bytecode_language.cpp | 2 +- src/java_bytecode/java_bytecode_language.h | 4 +- 4 files changed, 42 insertions(+), 45 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index f20971248a5..a6b2cacf24a 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -569,7 +569,7 @@ codet java_bytecode_convert_methodt::get_array_bounds_check( /*******************************************************************\ -Function: get_array_access_check +Function: throw_array_access_exception Inputs: @@ -581,10 +581,10 @@ Function: get_array_access_check \*******************************************************************/ -codet java_bytecode_convert_methodt::get_array_access_check( +codet java_bytecode_convert_methodt::throw_array_access_exception( const exprt &array_struct, const exprt &idx, - const source_locationt &original_sloc) + const source_locationt &original_loc) { symbolt exc_symbol; if(!symbol_table.has_symbol("ArrayIndexOutOfBoundsException")) @@ -601,7 +601,7 @@ codet java_bytecode_convert_methodt::get_array_access_check( const symbol_exprt &exc=exc_symbol.symbol_expr(); side_effect_expr_throwt throw_expr; - throw_expr.add_source_location()=original_sloc; + throw_expr.add_source_location()=original_loc; throw_expr.copy_to_operands(exc); const constant_exprt &zero=from_integer(0, java_int_type()); @@ -611,7 +611,7 @@ codet java_bytecode_convert_methodt::get_array_access_check( const and_exprt and_expr(lt_zero, ge_length); code_ifthenelset if_code; - if_code.add_source_location()=original_sloc; + if_code.add_source_location()=original_loc; if_code.cond()=and_expr; if_code.then_case()=code_expressiont(throw_expr); @@ -620,7 +620,7 @@ codet java_bytecode_convert_methodt::get_array_access_check( /*******************************************************************\ -Function: get_array_length_check +Function: throw_array_length_exception Inputs: @@ -630,9 +630,9 @@ Function: get_array_length_check \*******************************************************************/ -codet java_bytecode_convert_methodt::get_array_length_check( +codet java_bytecode_convert_methodt::throw_array_length_exception( const exprt &length, - const source_locationt &original_sloc) + const source_locationt &original_loc) { symbolt exc_symbol; if(!symbol_table.has_symbol("NegativeArraySizeException")) @@ -649,23 +649,23 @@ codet java_bytecode_convert_methodt::get_array_length_check( const symbol_exprt &exc=exc_symbol.symbol_expr(); side_effect_expr_throwt throw_expr; - throw_expr.add_source_location()=original_sloc; + throw_expr.add_source_location()=original_loc; throw_expr.copy_to_operands(exc); const constant_exprt &zero=from_integer(0, java_int_type()); const binary_relation_exprt ge_zero(length, ID_ge, zero); code_ifthenelset if_code; - if_code.add_source_location()=original_sloc; + if_code.add_source_location()=original_loc; if_code.cond()=ge_zero; if_code.then_case()=code_expressiont(throw_expr); - + return if_code; } /*******************************************************************\ -Function: get_null_dereference_check +Function: throw_null_dereference_exception Inputs: @@ -676,9 +676,9 @@ Function: get_null_dereference_check \*******************************************************************/ -codet java_bytecode_convert_methodt::get_null_dereference_check( +codet java_bytecode_convert_methodt::throw_null_dereference_exception( const exprt &expr, - const source_locationt &original_sloc) + const source_locationt &original_loc) { symbolt exc_symbol; if(!symbol_table.has_symbol("NullPointerException")) @@ -695,14 +695,14 @@ codet java_bytecode_convert_methodt::get_null_dereference_check( const symbol_exprt &exc=exc_symbol.symbol_expr(); side_effect_expr_throwt throw_expr; - throw_expr.add_source_location()=original_sloc; + throw_expr.add_source_location()=original_loc; throw_expr.copy_to_operands(exc); const equal_exprt equal_expr( expr, null_pointer_exprt(pointer_typet(empty_typet()))); code_ifthenelset if_code; - if_code.add_source_location()=original_sloc; + if_code.add_source_location()=original_loc; if_code.cond()=equal_expr; if_code.then_case()=code_expressiont(throw_expr); @@ -711,7 +711,7 @@ codet java_bytecode_convert_methodt::get_null_dereference_check( /*******************************************************************\ -Function: get_class_cast_check +Function: throw_class_cast_exception Inputs: @@ -721,10 +721,10 @@ Function: get_class_cast_check \*******************************************************************/ -codet java_bytecode_convert_methodt::get_class_cast_check( +codet java_bytecode_convert_methodt::throw_class_cast_exception( const exprt &class1, const exprt &class2, - const source_locationt &original_sloc) + const source_locationt &original_loc) { // TODO: use std::move symbolt exc_symbol; @@ -743,7 +743,7 @@ codet java_bytecode_convert_methodt::get_class_cast_check( const symbol_exprt &exc=exc_symbol.symbol_expr(); side_effect_expr_throwt throw_expr; - throw_expr.add_source_location()=original_sloc; + throw_expr.add_source_location()=original_loc; throw_expr.copy_to_operands(exc); binary_predicate_exprt class_cast_check( @@ -760,7 +760,7 @@ codet java_bytecode_convert_methodt::get_class_cast_check( and_exprt and_expr(op_not_null, class_cast_check); code_ifthenelset if_code; - if_code.add_source_location()=original_sloc; + if_code.add_source_location()=original_loc; if_code.cond()=and_expr; if_code.then_case()=code_expressiont(throw_expr); @@ -1561,9 +1561,10 @@ codet java_bytecode_convert_methodt::convert_instructions( code_blockt block; if(throw_runtime_exceptions) { - codet null_dereference_check=get_null_dereference_check( - op[0], - i_it->source_location); + codet null_dereference_check= + throw_null_dereference_exception( + op[0], + i_it->source_location); block.move_to_operands(null_dereference_check); } else @@ -1598,7 +1599,7 @@ codet java_bytecode_convert_methodt::convert_instructions( if(throw_runtime_exceptions) { codet conditional_check= - get_class_cast_check(op[0], arg0, i_it->source_location); + throw_class_cast_exception(op[0], arg0, i_it->source_location); c=std::move(conditional_check); } else @@ -1844,13 +1845,9 @@ codet java_bytecode_convert_methodt::convert_instructions( const dereference_exprt element(data_plus_offset, element_type); c=code_blockt(); - codet bounds_check; - if(throw_runtime_exceptions) - bounds_check= - get_array_access_check(deref, op[1], i_it->source_location); - else - bounds_check= - get_array_bounds_check(deref, op[1], i_it->source_location); + codet bounds_check=throw_runtime_exceptions? + throw_array_access_exception(deref, op[1], i_it->source_location): + get_array_bounds_check(deref, op[1], i_it->source_location); bounds_check.add_source_location()=i_it->source_location; c.move_to_operands(bounds_check); @@ -2460,7 +2457,7 @@ codet java_bytecode_convert_methodt::convert_instructions( if(throw_runtime_exceptions) { - codet array_length_check=get_array_length_check( + codet array_length_check=throw_array_length_exception( op[0], i_it->source_location); c.move_to_operands(array_length_check); @@ -2509,7 +2506,7 @@ codet java_bytecode_convert_methodt::convert_instructions( c=code_blockt(); if(throw_runtime_exceptions) { - codet array_length_check=get_array_length_check( + codet array_length_check=throw_array_length_exception( op[0], i_it->source_location); c.move_to_operands(array_length_check); diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h index 589a76bcc0e..263d50a95c5 100644 --- a/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/src/java_bytecode/java_bytecode_convert_method_class.h @@ -109,25 +109,25 @@ class java_bytecode_convert_methodt:public messaget const exprt &idx, const source_locationt &original_sloc); - codet get_array_access_check( + codet throw_array_access_exception( const exprt &arraystruct, const exprt &idx, const source_locationt &original_sloc); - codet get_array_length_check( + codet throw_array_length_exception( const exprt &length, const source_locationt &original_sloc); - - codet get_null_dereference_check( + + codet throw_null_dereference_exception( const exprt &expr, const source_locationt &original_sloc); - codet get_class_cast_check( + codet throw_class_cast_exception( const exprt &class1, - const exprt &class2, + const exprt &class2, const source_locationt &original_sloc); - - // return corresponding reference of variable + +// return corresponding reference of variable const variablet &find_variable_for_slot( size_t address, variablest &var_list); diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index f408419e27e..9945d78278b 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -42,7 +42,7 @@ Function: java_bytecode_languaget::get_language_options void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) { - throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions"); + throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions"); assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null"); string_refinement_enabled=cmd.isset("refine-strings"); if(cmd.isset("java-max-input-array-length")) diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index c380ccbbc3b..3b6ef4b05e5 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -57,8 +57,8 @@ class java_bytecode_languaget:public languaget java_bytecode_languaget(): max_nondet_array_length(MAX_NONDET_ARRAY_LENGTH_DEFAULT), max_user_array_length(0), - throw_runtime_exceptions(false) - {} + throw_runtime_exceptions(false) + {} bool from_expr( const exprt &expr, From 60c7c8c9a17bb078da2d6c710e9dd09ddb971c3a Mon Sep 17 00:00:00 2001 From: Cristina Date: Tue, 30 May 2017 09:35:22 +0100 Subject: [PATCH 10/13] Address reviewers comments --- .../ArrayIndexOutOfBoundsException.class | Bin 468 -> 0 bytes .../ArrayIndexOutOfBoundsException.java | 6 - .../ArrayIndexOutOfBoundsExceptionTest.class | Bin 0 -> 918 bytes .../ArrayIndexOutOfBoundsExceptionTest.java | 14 ++ .../ArrayIndexOutOfBoundsException/test.desc | 7 +- .../NegativeArraySizeException.class | Bin 448 -> 0 bytes .../NegativeArraySizeException.java | 5 - .../NegativeArraySizeExceptionTest.class | Bin 0 -> 889 bytes .../NegativeArraySizeExceptionTest.java | 11 + .../NegativeArraySizeException/test.desc | 7 +- src/cbmc/cbmc_parse_options.cpp | 1 + .../java_bytecode_convert_method.cpp | 213 ++++++++++-------- .../java_bytecode_convert_method_class.h | 9 +- 13 files changed, 155 insertions(+), 118 deletions(-) delete mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsException.class delete mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsException.java create mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.class create mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.java delete mode 100644 regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeException.class delete mode 100644 regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeException.java create mode 100644 regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.class create mode 100644 regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.java diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsException.class b/regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsException.class deleted file mode 100644 index d0368b140e8e545c6eda5608cf9ba1d335b74911..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 468 zcmaJ-O;5r=6r9%&Dir}iIU0=@)I=`cFeYj+A!+OZ!-dmQR$NlHW@!!nEKerJ_yhb= z#@AxP#juC>c4pt3ne6w^#}|MLw0ziTdf4-@Pbgg~tMG>V^LJ?bB_+@_1@h9jR)|uHRLKxQs!Fs^8+!>`61!U4DEtB6 z&>!HrAW?}T`p!ooW<%Rl0_DNpnc10h&dkoQ-`{@%SiwUZHtH4@Y#92yn?n{23-@ef zw13~mBAOPK7%B}OMMA|g45DW;;=O_J8Q3mEW=#e%e$0?+F6}Uw8=)^4W?dPGm&vdv z)V5A$D7&G@2RmFz?VknB_??Ux8t%GM{Nq;Oi%}H|=4PD1*xMp0V&pNjE@e%}*VtV3NlE2D&r=vQ^ z!(pgi%0GXtO{GG`urM7!%d*gNu#5)`#R*QQw=cYy-g6S#7|<%vEBGRkO8D#NOf;i7 zp$poBUDRolY+5o_tZHp!r9g8;f&R1PwdrJZrd!8gM`Rc%(myi}GL*=6{wAP|3VAtP z!BvXr;!gx-&{?;B*zR&Mlj@wncyo-@srv=#L*!48A=f%R8bg!_&ZH7eFi#X9&qSIa zvvgw znL8P0%yhyck=aNZUEx2{E+6z0VJ{r2RF-YN~801P8UF>>6un=Jbn=H0@sD(C1!WLtJ&Mzr5TYLZj diff --git a/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeException.java b/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeException.java deleted file mode 100644 index 08ef396b4cd..00000000000 --- a/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeException.java +++ /dev/null @@ -1,5 +0,0 @@ -public class NegativeArraySizeException { - public static void main(String args[]) { - int a[]=new int[-1]; - } -} diff --git a/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.class b/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.class new file mode 100644 index 0000000000000000000000000000000000000000..a3fe5e30e607670c9a8436ab1a49d073c4106f84 GIT binary patch literal 889 zcmZ`%-%k@k5dP+R*K3cXlvZm+#3B_7{^$#D5Fy? z{sEuSL=rLb?jL2Gt;m^ZbGeAr2W@mr={Q4ch3LbgzFz@272g}%nJaVYJxaT2j z{6!D<(QvUuDAz?COP#1e6hBk3X!m4?KzoGjnu=8Ngpg@0?Go&bK}Qm%0u{-vVZSZ) zjsX)&!5|d9U7?lnFN1dSM#Y3$uqC@9QAcuJYw@n7-pkG7P#&6cJ2FmInYS-gM5r|O zg9C9SnmrM9o2^8vsJm+Fk|0?7FIa{=4hf5Yp~iC?UZK0Jp!^?N!elEE;oFzua3q&6 zh>%+gdzTG+t-(--^0_kYEsU>XI(TeE`;VZA;><|6n6=L8ey$g=BRoQ|@6X0f@n;jX~p)#lIPsLNt%UCMny{sgZ55q9P?oPWDA91bl1 Msp @@ -569,53 +571,105 @@ codet java_bytecode_convert_methodt::get_array_bounds_check( /*******************************************************************\ -Function: throw_array_access_exception +Function: throw_exception Inputs: Outputs: - Purpose: Checks whether the array access array_struct[idx] - is out-of-bounds, and throws ArrayIndexOutofBoundsException - if necessary + Purpose: Creates a class stub for exc_name and generates a + conditional GOTO such that exc_name is thrown when + cond is met \*******************************************************************/ -codet java_bytecode_convert_methodt::throw_array_access_exception( - const exprt &array_struct, - const exprt &idx, - const source_locationt &original_loc) +codet java_bytecode_convert_methodt::throw_exception( + const exprt &cond, + const source_locationt &original_loc, + const irep_idt &exc_name) { - symbolt exc_symbol; - if(!symbol_table.has_symbol("ArrayIndexOutOfBoundsException")) + exprt exc; + code_blockt init_code; + const irep_idt &exc_obj_name=id2string(goto_functionst::entry_point())+ + "::"+id2string(exc_name); + + if(!symbol_table.has_symbol(exc_obj_name)) { - exc_symbol.is_static_lifetime=true; - exc_symbol.base_name="ArrayIndexOutOfBoundsException"; - exc_symbol.name="ArrayIndexOutOfBoundsException"; + // for now, create a class stub + // TODO: model exceptions and use that model + class_typet class_type; + class_type.set_tag(exc_name); + class_type.set(ID_base_name, exc_name); + class_type.set(ID_incomplete_class, true); + + // produce class symbol + symbolt exc_symbol; + exc_symbol.base_name=exc_name; + exc_symbol.pretty_name=exc_name; + exc_symbol.name="java::"+id2string(exc_name); + class_type.set(ID_name, exc_symbol.name); + exc_symbol.type=class_type; exc_symbol.mode=ID_java; - exc_symbol.type=typet(ID_pointer, empty_typet()); + exc_symbol.is_type=true; symbol_table.add(exc_symbol); + // create the class identifier + java_root_class(exc_symbol); + + // create the exception object + exc=object_factory( + pointer_typet(exc_symbol.type), + exc_name, + init_code, + false, + symbol_table, + max_array_length, + original_loc); } else - exc_symbol=symbol_table.lookup("ArrayIndexOutOfBoundsException"); + exc=symbol_table.lookup(exc_obj_name).symbol_expr(); - const symbol_exprt &exc=exc_symbol.symbol_expr(); side_effect_expr_throwt throw_expr; throw_expr.add_source_location()=original_loc; - throw_expr.copy_to_operands(exc); + throw_expr.move_to_operands(exc); + + code_ifthenelset if_code; + if_code.add_source_location()=original_loc; + if_code.cond()=cond; + if_code.then_case()=code_expressiont(throw_expr); + + init_code.move_to_operands(if_code); + + return init_code; +} + +/*******************************************************************\ + +Function: throw_array_access_exception + + Inputs: + + Outputs: + Purpose: Checks whether the array access array_struct[idx] + is out-of-bounds, and throws ArrayIndexOutofBoundsException + if necessary + +\*******************************************************************/ + +codet java_bytecode_convert_methodt::throw_array_access_exception( + const exprt &array_struct, + const exprt &idx, + const source_locationt &original_loc) +{ const constant_exprt &zero=from_integer(0, java_int_type()); const binary_relation_exprt lt_zero(idx, ID_lt, zero); const member_exprt length_field(array_struct, "length", java_int_type()); const binary_relation_exprt ge_length(idx, ID_ge, length_field); - const and_exprt and_expr(lt_zero, ge_length); + const or_exprt or_expr(lt_zero, ge_length); - code_ifthenelset if_code; - if_code.add_source_location()=original_loc; - if_code.cond()=and_expr; - if_code.then_case()=code_expressiont(throw_expr); - - return if_code; + return throw_exception( + or_expr, + original_loc, "java.lang.ArrayIndexOutOfBoundsException"); } /*******************************************************************\ @@ -634,33 +688,12 @@ codet java_bytecode_convert_methodt::throw_array_length_exception( const exprt &length, const source_locationt &original_loc) { - symbolt exc_symbol; - if(!symbol_table.has_symbol("NegativeArraySizeException")) - { - exc_symbol.is_static_lifetime=true; - exc_symbol.base_name="NegativeArraySizeException"; - exc_symbol.name="NegativeArraySizeException"; - exc_symbol.mode=ID_java; - exc_symbol.type=typet(ID_pointer, empty_typet()); - symbol_table.add(exc_symbol); - } - else - exc_symbol=symbol_table.lookup("NegativeArraySizeException"); - - const symbol_exprt &exc=exc_symbol.symbol_expr(); - side_effect_expr_throwt throw_expr; - throw_expr.add_source_location()=original_loc; - throw_expr.copy_to_operands(exc); - const constant_exprt &zero=from_integer(0, java_int_type()); - const binary_relation_exprt ge_zero(length, ID_ge, zero); - - code_ifthenelset if_code; - if_code.add_source_location()=original_loc; - if_code.cond()=ge_zero; - if_code.then_case()=code_expressiont(throw_expr); + const binary_relation_exprt less_zero(length, ID_lt, zero); - return if_code; + return throw_exception( + less_zero, + original_loc, "java.lang.NegativeArraySizeException"); } /*******************************************************************\ @@ -677,36 +710,22 @@ Function: throw_null_dereference_exception \*******************************************************************/ codet java_bytecode_convert_methodt::throw_null_dereference_exception( - const exprt &expr, + exprt &expr, const source_locationt &original_loc) { - symbolt exc_symbol; - if(!symbol_table.has_symbol("NullPointerException")) - { - exc_symbol.is_static_lifetime=true; - exc_symbol.base_name="NullPointerException"; - exc_symbol.name="NullPointerException"; - exc_symbol.mode=ID_java; - exc_symbol.type=typet(ID_pointer, empty_typet()); - symbol_table.add(exc_symbol); - } - else - exc_symbol=symbol_table.lookup("NullPointerException"); + empty_typet voidt; + pointer_typet voidptr(voidt); - const symbol_exprt &exc=exc_symbol.symbol_expr(); - side_effect_expr_throwt throw_expr; - throw_expr.add_source_location()=original_loc; - throw_expr.copy_to_operands(exc); + if(expr.type()!=voidptr) + expr.make_typecast(voidptr); const equal_exprt equal_expr( expr, - null_pointer_exprt(pointer_typet(empty_typet()))); - code_ifthenelset if_code; - if_code.add_source_location()=original_loc; - if_code.cond()=equal_expr; - if_code.then_case()=code_expressiont(throw_expr); + null_pointer_exprt(voidptr)); - return if_code; + return throw_exception( + equal_expr, + original_loc, "java.lang.NullPointerException"); } /*******************************************************************\ @@ -726,26 +745,6 @@ codet java_bytecode_convert_methodt::throw_class_cast_exception( const exprt &class2, const source_locationt &original_loc) { - // TODO: use std::move - symbolt exc_symbol; - if(!symbol_table.has_symbol("ClassCastException")) - { - exc_symbol.is_static_lifetime=true; - exc_symbol.base_name="ClassCastException"; - exc_symbol.name="ClassCastException"; - exc_symbol.mode=ID_java; - exc_symbol.type=typet(ID_pointer, empty_typet()); - symbol_table.add(exc_symbol); - } - else - exc_symbol=symbol_table.lookup("ClassCastException"); - - const symbol_exprt &exc=exc_symbol.symbol_expr(); - - side_effect_expr_throwt throw_expr; - throw_expr.add_source_location()=original_loc; - throw_expr.copy_to_operands(exc); - binary_predicate_exprt class_cast_check( class1, ID_java_instanceof, class2); @@ -757,14 +756,12 @@ codet java_bytecode_convert_methodt::throw_class_cast_exception( notequal_exprt op_not_null(null_check_op, null_pointer_exprt(voidptr)); // checkcast passes when the operand is null - and_exprt and_expr(op_not_null, class_cast_check); - - code_ifthenelset if_code; - if_code.add_source_location()=original_loc; - if_code.cond()=and_expr; - if_code.then_case()=code_expressiont(throw_expr); + and_exprt and_expr(op_not_null, not_exprt(class_cast_check)); - return if_code; + return throw_exception( + and_expr, + original_loc, + "ClassCastException"); } /*******************************************************************\ @@ -1596,6 +1593,7 @@ codet java_bytecode_convert_methodt::convert_instructions( // on stack to given type fails. // The stack isn't modified. assert(op.size()==1 && results.size()==1); + if(throw_runtime_exceptions) { codet conditional_check= @@ -1845,6 +1843,7 @@ codet java_bytecode_convert_methodt::convert_instructions( const dereference_exprt element(data_plus_offset, element_type); c=code_blockt(); + codet bounds_check=throw_runtime_exceptions? throw_array_access_exception(deref, op[1], i_it->source_location): get_array_bounds_check(deref, op[1], i_it->source_location); @@ -2333,6 +2332,14 @@ codet java_bytecode_convert_methodt::convert_instructions( else if(statement=="getfield") { assert(op.size()==1 && results.size()==1); + if(throw_runtime_exceptions) + { + codet null_dereference_check= + throw_null_dereference_exception( + op[0], + i_it->source_location); + c=null_dereference_check; + } results[0]=java_bytecode_promotion(to_member(op[0], arg0)); } else if(statement=="getstatic") @@ -2360,6 +2367,14 @@ codet java_bytecode_convert_methodt::convert_instructions( else if(statement=="putfield") { assert(op.size()==2 && results.size()==0); + if(throw_runtime_exceptions) + { + codet null_dereference_check= + throw_null_dereference_exception( + op[0], + i_it->source_location); + c=null_dereference_check; + } c=code_assignt(to_member(op[0], arg0), op[1]); } else if(statement=="putstatic") diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h index 263d50a95c5..6327be105bd 100644 --- a/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/src/java_bytecode/java_bytecode_convert_method_class.h @@ -37,7 +37,7 @@ class java_bytecode_convert_methodt:public messaget messaget(_message_handler), symbol_table(_symbol_table), max_array_length(_max_array_length), - throw_runtime_exceptions(_throw_runtime_exceptions), + throw_runtime_exceptions(_throw_runtime_exceptions), lazy_methods(_lazy_methods) { } @@ -109,6 +109,11 @@ class java_bytecode_convert_methodt:public messaget const exprt &idx, const source_locationt &original_sloc); + codet throw_exception( + const exprt &cond, + const source_locationt &original_loc, + const irep_idt &exc_name); + codet throw_array_access_exception( const exprt &arraystruct, const exprt &idx, @@ -119,7 +124,7 @@ class java_bytecode_convert_methodt:public messaget const source_locationt &original_sloc); codet throw_null_dereference_exception( - const exprt &expr, + exprt &expr, const source_locationt &original_sloc); codet throw_class_cast_exception( From 30e7349124455a4de7e0b8dfa8778a50fa0e9d6c Mon Sep 17 00:00:00 2001 From: Cristina Date: Tue, 30 May 2017 10:29:55 +0100 Subject: [PATCH 11/13] Added regression test for throwing NullPointerException --- .../cbmc-java/NullPointerException2/A.class | Bin 0 -> 247 bytes .../cbmc-java/NullPointerException2/B.class | Bin 0 -> 241 bytes .../NullPointerException2/Test.class | Bin 0 -> 835 bytes .../cbmc-java/NullPointerException2/Test.java | 18 ++++++++++++++++++ .../cbmc-java/NullPointerException2/test.desc | 9 +++++++++ 5 files changed, 27 insertions(+) create mode 100644 regression/cbmc-java/NullPointerException2/A.class create mode 100644 regression/cbmc-java/NullPointerException2/B.class create mode 100644 regression/cbmc-java/NullPointerException2/Test.class create mode 100644 regression/cbmc-java/NullPointerException2/Test.java create mode 100644 regression/cbmc-java/NullPointerException2/test.desc diff --git a/regression/cbmc-java/NullPointerException2/A.class b/regression/cbmc-java/NullPointerException2/A.class new file mode 100644 index 0000000000000000000000000000000000000000..19526643bf25706bad6f178a660ab3f724c8920b GIT binary patch literal 247 zcmXX=%MQU%5Iv*SQjg*bEV0my9g#E=iKJmc>~HIaE7c}d{>w^Y;RAe>m|I=U%sFSy zJU-vo8^8oT2L@al9UEN&DUKDvnyEzPbAmA#?g{21JxGEZs6?)Bmr!Oq5yq_af;1BG zUSvx1QZ)0Ey7Fk?PYKR8y=9SHDs8Xt literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NullPointerException2/B.class b/regression/cbmc-java/NullPointerException2/B.class new file mode 100644 index 0000000000000000000000000000000000000000..f29cbafef50e97fe2936695afa091c7f9c847cd4 GIT binary patch literal 241 zcmXX=Jx_!{5Pid^a45#o%2F+k#!h2_(TZ5y5&8u;x)<2Jz+(JcRwfqy0DqKm7M*0~ zedN7lzJETy09@fXg^$A+M=^3jbfdJgw*>$Eq9Fu#=1CIrN@@8x53L+)(e~_|RHhSs zBSz))zZuvUHF32nuLf9vGl tDx+}*kKb}byj)?7m=%o92`@iD?@T literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NullPointerException2/Test.class b/regression/cbmc-java/NullPointerException2/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..cd8ba9d445765df26cec3cd8ac74d3e3317cd1b5 GIT binary patch literal 835 zcmZuuT~8B16g{*3n0C9+(kfO(Kt(J?sUP(TG**PfWI>Y>67gxfoz%f)OLn)0-$H!% z88wnfBJchv^$egjk#0J7?wxbbJ@?)pKfiqk(8MDf13=E!1O<$^+6E4>gzC3(aN5$c8yX)=tVsisGP$`CXY;Ri?ES);`#5^yxkLB z5)%^lIS+x{k{_J)XSe%<$XBb{bdxuN7mP*+qbL&Y;1a6jd?qkC)P9~U2M$IAszX%k z&umwss2@?aVV8K|;31j10=W!{}r04lgZFOQ2DXT&6bAUZ`m zCEWQhupS>F_4*L$ Date: Tue, 30 May 2017 12:01:36 +0100 Subject: [PATCH 12/13] Added more comments --- src/java_bytecode/java_bytecode_convert_method.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 37943612e8a..8f7a3f42e50 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1558,6 +1558,7 @@ codet java_bytecode_convert_methodt::convert_instructions( code_blockt block; if(throw_runtime_exceptions) { + // throw NullPointerException if necessary codet null_dereference_check= throw_null_dereference_exception( op[0], @@ -1566,6 +1567,7 @@ codet java_bytecode_convert_methodt::convert_instructions( } else { + // add assertion const typecast_exprt lhs(op[0], pointer_typet(empty_typet())); const exprt rhs(null_pointer_exprt(to_pointer_type(lhs.type()))); const exprt not_equal_null( @@ -1596,12 +1598,14 @@ codet java_bytecode_convert_methodt::convert_instructions( if(throw_runtime_exceptions) { + // throw ClassCastException codet conditional_check= throw_class_cast_exception(op[0], arg0, i_it->source_location); c=std::move(conditional_check); } else { + // add assertion binary_predicate_exprt check(op[0], ID_java_instanceof, arg0); code_assertt assert_class(check); assert_class.add_source_location(). @@ -2334,6 +2338,7 @@ codet java_bytecode_convert_methodt::convert_instructions( assert(op.size()==1 && results.size()==1); if(throw_runtime_exceptions) { + // throw NullPointerException if necessary codet null_dereference_check= throw_null_dereference_exception( op[0], @@ -2369,6 +2374,7 @@ codet java_bytecode_convert_methodt::convert_instructions( assert(op.size()==2 && results.size()==0); if(throw_runtime_exceptions) { + // throw NullPointerException if necessary codet null_dereference_check= throw_null_dereference_exception( op[0], From 20f87911be2f4b94d633e3eb5935d083c2bd3566 Mon Sep 17 00:00:00 2001 From: Cristina Date: Wed, 31 May 2017 10:28:32 +0100 Subject: [PATCH 13/13] Added more regression tests for runtime exceptions --- .../ArrayIndexOutOfBoundsExceptionTest.java | 20 ++++++++--------- .../cbmc-java/ClassCastException1/A.class | Bin 0 -> 265 bytes .../cbmc-java/ClassCastException1/B.class | Bin 0 -> 265 bytes .../ClassCastExceptionTest.class | Bin 0 -> 976 bytes .../ClassCastExceptionTest.java | 21 ++++++++++++++++++ .../cbmc-java/ClassCastException1/test.desc | 9 ++++++++ .../cbmc-java/ClassCastException2/A.class | Bin 0 -> 265 bytes .../cbmc-java/ClassCastException2/B.class | Bin 0 -> 265 bytes .../ClassCastExceptionTest.class | Bin 0 -> 976 bytes .../ClassCastExceptionTest.java | 21 ++++++++++++++++++ .../cbmc-java/ClassCastException2/test.desc | 9 ++++++++ .../NegativeArraySizeExceptionTest.java | 6 ++--- .../cbmc-java/NullPointerException2/Test.java | 16 ++++++------- .../cbmc-java/NullPointerException3/A.class | Bin 0 -> 247 bytes .../cbmc-java/NullPointerException3/B.class | Bin 0 -> 241 bytes .../NullPointerException3/Test.class | Bin 0 -> 835 bytes .../cbmc-java/NullPointerException3/Test.java | 18 +++++++++++++++ .../cbmc-java/NullPointerException3/test.desc | 9 ++++++++ 18 files changed, 108 insertions(+), 21 deletions(-) create mode 100644 regression/cbmc-java/ClassCastException1/A.class create mode 100644 regression/cbmc-java/ClassCastException1/B.class create mode 100644 regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.class create mode 100644 regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java create mode 100644 regression/cbmc-java/ClassCastException1/test.desc create mode 100644 regression/cbmc-java/ClassCastException2/A.class create mode 100644 regression/cbmc-java/ClassCastException2/B.class create mode 100644 regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.class create mode 100644 regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.java create mode 100644 regression/cbmc-java/ClassCastException2/test.desc create mode 100644 regression/cbmc-java/NullPointerException3/A.class create mode 100644 regression/cbmc-java/NullPointerException3/B.class create mode 100644 regression/cbmc-java/NullPointerException3/Test.class create mode 100644 regression/cbmc-java/NullPointerException3/Test.java create mode 100644 regression/cbmc-java/NullPointerException3/test.desc diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.java b/regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.java index 68b3b948032..385ca761881 100644 --- a/regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.java +++ b/regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.java @@ -1,14 +1,14 @@ public class ArrayIndexOutOfBoundsExceptionTest { public static void main(String args[]) { - try { - int[] a=new int[4]; - a[6]=0; - // TODO: fix the bytecode convertion such that there is no need for - // an explicit throw in order to convert the handler - throw new RuntimeException(); - } - catch(ArrayIndexOutOfBoundsException exc) { - assert false; - } + try { + int[] a=new int[4]; + a[6]=0; + // TODO: fix the bytecode convertion such that there is no need for + // an explicit throw in order to convert the handler + throw new RuntimeException(); + } + catch(ArrayIndexOutOfBoundsException exc) { + assert false; + } } } diff --git a/regression/cbmc-java/ClassCastException1/A.class b/regression/cbmc-java/ClassCastException1/A.class new file mode 100644 index 0000000000000000000000000000000000000000..3618c09b4ef59667a868d72a16f83c799dc86ff5 GIT binary patch literal 265 zcmXX=yKcfj5S#@+2$+{!nv@9zZqfxIAuC8o7Aa!UpPf^3$gv~ef%q*dq!fGr9~H3& z6uUb!JNr2Q|D6E5AZ(+FzK?;AA%PUflHg5MsmzSfe0p9JoVfawgnpt*x!V3@vQ9-- zuo5O!E{e6NmF0KQG2cq_Xfl5#v_GnCoy&!?_EB62tz)6h+dh}SMpb1hwV7RkZP`Y-nY literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ClassCastException1/B.class b/regression/cbmc-java/ClassCastException1/B.class new file mode 100644 index 0000000000000000000000000000000000000000..e9257dc442776837ad9e9e3e5f111a6f8a1718aa GIT binary patch literal 265 zcmXYrziz@n48}i0NNCERl(kDo+JP)=AO<3kDn;!8V!xy(dQqC7+<|y4CZrBL01t)m zwHa*xzR&iZueaX|fH4L>n&^87JUkI7<9H{yQ&lK4BQ%Gv8-f#+Uy{&|RUtq2KZ&f? zBFWhq#APb-ji{8>wdt5|rFk`;PYC|1+*hewDm(rh literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.class b/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.class new file mode 100644 index 0000000000000000000000000000000000000000..766a42a9a45c1eb061f31dc294acb0e2ffc7736e GIT binary patch literal 976 zcmZuvZEw<06n<`7C@p2YDd0Az(+wHZ;mh>P7NfzLEa^0ng=F(nDL2>&Woe7SUt+R9 z;OA)~i6qX?{wU+Q1*r?BY41Jvobx=-d3t~S{{92NHlFB6p{(ML4ha<%8!Dz7+3ydm({K)Qjv=vYcc)J1jsC#1`AbL4y)=(5M%xmS4P=mI$VT$_-GFzv zClU`CGErh8pJ6dNdNXhXr^jcGF)T;Pc~%1pNR!u5&GWy%bkFnp9+^DfB&4c%WYEQV zd`Zv5XR@iXFMdNhLJdI(tj&GLi~YFFu1AvIOp5{0*C6K;oPKsJ~B2ICB>@)?T!6^Z$21x5^#@l1HK IMuCL&Klr}V+W-In literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java b/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java new file mode 100644 index 00000000000..79fc69b76f8 --- /dev/null +++ b/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java @@ -0,0 +1,21 @@ +class A { + int i; +} + +class B { + int j; +} + +public class ClassCastExceptionTest { + public static void main(String args[]) { + try { + Object x = new Integer(0); + String y=(String)x; + throw new RuntimeException(); + } + catch (ClassCastException exc) { + assert false; + } + + } +} diff --git a/regression/cbmc-java/ClassCastException1/test.desc b/regression/cbmc-java/ClassCastException1/test.desc new file mode 100644 index 00000000000..c2a2d4a8498 --- /dev/null +++ b/regression/cbmc-java/ClassCastException1/test.desc @@ -0,0 +1,9 @@ +CORE +ClassCastExceptionTest.class +--java-throw-runtime-exceptions +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file ClassCastExceptionTest.java line 17 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/ClassCastException2/A.class b/regression/cbmc-java/ClassCastException2/A.class new file mode 100644 index 0000000000000000000000000000000000000000..3618c09b4ef59667a868d72a16f83c799dc86ff5 GIT binary patch literal 265 zcmXX=yKcfj5S#@+2$+{!nv@9zZqfxIAuC8o7Aa!UpPf^3$gv~ef%q*dq!fGr9~H3& z6uUb!JNr2Q|D6E5AZ(+FzK?;AA%PUflHg5MsmzSfe0p9JoVfawgnpt*x!V3@vQ9-- zuo5O!E{e6NmF0KQG2cq_Xfl5#v_GnCoy&!?_EB62tz)6h+dh}SMpb1hwV7RkZP`Y-nY literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ClassCastException2/B.class b/regression/cbmc-java/ClassCastException2/B.class new file mode 100644 index 0000000000000000000000000000000000000000..e9257dc442776837ad9e9e3e5f111a6f8a1718aa GIT binary patch literal 265 zcmXYrziz@n48}i0NNCERl(kDo+JP)=AO<3kDn;!8V!xy(dQqC7+<|y4CZrBL01t)m zwHa*xzR&iZueaX|fH4L>n&^87JUkI7<9H{yQ&lK4BQ%Gv8-f#+Uy{&|RUtq2KZ&f? zBFWhq#APb-ji{8>wdt5|rFk`;PYC|1+*hewDm(rh literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.class b/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.class new file mode 100644 index 0000000000000000000000000000000000000000..766a42a9a45c1eb061f31dc294acb0e2ffc7736e GIT binary patch literal 976 zcmZuvZEw<06n<`7C@p2YDd0Az(+wHZ;mh>P7NfzLEa^0ng=F(nDL2>&Woe7SUt+R9 z;OA)~i6qX?{wU+Q1*r?BY41Jvobx=-d3t~S{{92NHlFB6p{(ML4ha<%8!Dz7+3ydm({K)Qjv=vYcc)J1jsC#1`AbL4y)=(5M%xmS4P=mI$VT$_-GFzv zClU`CGErh8pJ6dNdNXhXr^jcGF)T;Pc~%1pNR!u5&GWy%bkFnp9+^DfB&4c%WYEQV zd`Zv5XR@iXFMdNhLJdI(tj&GLi~YFFu1AvIOp5{0*C6K;oPKsJ~B2ICB>@)?T!6^Z$21x5^#@l1HK IMuCL&Klr}V+W-In literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.java b/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.java new file mode 100644 index 00000000000..79fc69b76f8 --- /dev/null +++ b/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.java @@ -0,0 +1,21 @@ +class A { + int i; +} + +class B { + int j; +} + +public class ClassCastExceptionTest { + public static void main(String args[]) { + try { + Object x = new Integer(0); + String y=(String)x; + throw new RuntimeException(); + } + catch (ClassCastException exc) { + assert false; + } + + } +} diff --git a/regression/cbmc-java/ClassCastException2/test.desc b/regression/cbmc-java/ClassCastException2/test.desc new file mode 100644 index 00000000000..6985d0e0f8d --- /dev/null +++ b/regression/cbmc-java/ClassCastException2/test.desc @@ -0,0 +1,9 @@ +CORE +ClassCastExceptionTest.class + +^EXIT=10$ +^SIGNAL=0$ +^.*Dynamic cast check: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.java b/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.java index 120b6856adb..47aac3d378e 100644 --- a/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.java +++ b/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.java @@ -1,11 +1,11 @@ public class NegativeArraySizeExceptionTest { public static void main(String args[]) { try { - int a[]=new int[-1]; - throw new RuntimeException(); + int a[]=new int[-1]; + throw new RuntimeException(); } catch (NegativeArraySizeException exc) { - assert false; + assert false; } } } diff --git a/regression/cbmc-java/NullPointerException2/Test.java b/regression/cbmc-java/NullPointerException2/Test.java index b40f0c8555e..067ad18b70f 100644 --- a/regression/cbmc-java/NullPointerException2/Test.java +++ b/regression/cbmc-java/NullPointerException2/Test.java @@ -6,13 +6,13 @@ class A { public class Test { public static void main(String args[]) { - A a=null; - try { - int i=a.i; - throw new B(); - } - catch (NullPointerException exc) { - assert false; - } + A a=null; + try { + int i=a.i; + throw new B(); + } + catch (NullPointerException exc) { + assert false; + } } } diff --git a/regression/cbmc-java/NullPointerException3/A.class b/regression/cbmc-java/NullPointerException3/A.class new file mode 100644 index 0000000000000000000000000000000000000000..19526643bf25706bad6f178a660ab3f724c8920b GIT binary patch literal 247 zcmXX=%MQU%5Iv*SQjg*bEV0my9g#E=iKJmc>~HIaE7c}d{>w^Y;RAe>m|I=U%sFSy zJU-vo8^8oT2L@al9UEN&DUKDvnyEzPbAmA#?g{21JxGEZs6?)Bmr!Oq5yq_af;1BG zUSvx1QZ)0Ey7Fk?PYKR8y=9SHDs8Xt literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NullPointerException3/B.class b/regression/cbmc-java/NullPointerException3/B.class new file mode 100644 index 0000000000000000000000000000000000000000..f29cbafef50e97fe2936695afa091c7f9c847cd4 GIT binary patch literal 241 zcmXX=Jx_!{5Pid^a45#o%2F+k#!h2_(TZ5y5&8u;x)<2Jz+(JcRwfqy0DqKm7M*0~ zedN7lzJETy09@fXg^$A+M=^3jbfdJgw*>$Eq9Fu#=1CIrN@@8x53L+)(e~_|RHhSs zBSz))zZuvUHF32nuLf9vGl tDx+}*kKb}byj)?7m=%o92`@iD?@T literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NullPointerException3/Test.class b/regression/cbmc-java/NullPointerException3/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..cd8ba9d445765df26cec3cd8ac74d3e3317cd1b5 GIT binary patch literal 835 zcmZuuT~8B16g{*3n0C9+(kfO(Kt(J?sUP(TG**PfWI>Y>67gxfoz%f)OLn)0-$H!% z88wnfBJchv^$egjk#0J7?wxbbJ@?)pKfiqk(8MDf13=E!1O<$^+6E4>gzC3(aN5$c8yX)=tVsisGP$`CXY;Ri?ES);`#5^yxkLB z5)%^lIS+x{k{_J)XSe%<$XBb{bdxuN7mP*+qbL&Y;1a6jd?qkC)P9~U2M$IAszX%k z&umwss2@?aVV8K|;31j10=W!{}r04lgZFOQ2DXT&6bAUZ`m zCEWQhupS>F_4*L$