diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index f21b0bb1ce2..0330794a8e7 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -27,14 +27,12 @@ class java_bytecode_convert_classt:public messaget java_bytecode_convert_classt( symbol_tablet &_symbol_table, message_handlert &_message_handler, - bool _disable_runtime_checks, size_t _max_array_length, lazy_methodst& _lazy_methods, lazy_methods_modet _lazy_methods_mode, bool _string_refinement_enabled): messaget(_message_handler), symbol_table(_symbol_table), - disable_runtime_checks(_disable_runtime_checks), max_array_length(_max_array_length), lazy_methods(_lazy_methods), lazy_methods_mode(_lazy_methods_mode), @@ -60,7 +58,6 @@ class java_bytecode_convert_classt:public messaget protected: symbol_tablet &symbol_table; - const bool disable_runtime_checks; const size_t max_array_length; lazy_methodst &lazy_methods; lazy_methods_modet lazy_methods_mode; @@ -169,7 +166,6 @@ void java_bytecode_convert_classt::convert(const classt &c) method, symbol_table, get_message_handler(), - disable_runtime_checks, max_array_length); } else @@ -364,7 +360,6 @@ bool java_bytecode_convert_class( const java_bytecode_parse_treet &parse_tree, symbol_tablet &symbol_table, message_handlert &message_handler, - bool disable_runtime_checks, size_t max_array_length, lazy_methodst &lazy_methods, lazy_methods_modet lazy_methods_mode, @@ -373,7 +368,6 @@ bool java_bytecode_convert_class( java_bytecode_convert_classt java_bytecode_convert_class( symbol_table, message_handler, - disable_runtime_checks, max_array_length, lazy_methods, lazy_methods_mode, diff --git a/src/java_bytecode/java_bytecode_convert_class.h b/src/java_bytecode/java_bytecode_convert_class.h index 0d2be3d8202..9ce5cc8c7cc 100644 --- a/src/java_bytecode/java_bytecode_convert_class.h +++ b/src/java_bytecode/java_bytecode_convert_class.h @@ -19,7 +19,6 @@ bool java_bytecode_convert_class( const java_bytecode_parse_treet &parse_tree, symbol_tablet &symbol_table, message_handlert &message_handler, - bool disable_runtime_checks, size_t max_array_length, lazy_methodst &, lazy_methods_modet, diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 0912ec8b22a..e479423ed9b 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1084,20 +1084,17 @@ codet java_bytecode_convert_methodt::convert_instructions( { assert(op.size()==1 && results.size()==1); code_blockt block; - if(!disable_runtime_checks) - { - // 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); - } + // 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); side_effect_expr_throwt throw_expr; throw_expr.add_source_location()=i_it->source_location; @@ -1110,20 +1107,15 @@ codet java_bytecode_convert_methodt::convert_instructions( } else if(statement=="checkcast") { - if(!disable_runtime_checks) - { - // 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); - c=code_assertt(check); - c.add_source_location().set_comment("Dynamic cast check"); - c.add_source_location().set_property_class("bad-dynamic-cast"); - } - else - c=code_skipt(); + // 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); + c=code_assertt(check); + c.add_source_location().set_comment("Dynamic cast check"); + c.add_source_location().set_property_class("bad-dynamic-cast"); results[0]=op[0]; } @@ -1308,13 +1300,10 @@ codet java_bytecode_convert_methodt::convert_instructions( const dereference_exprt element(data_plus_offset, element_type); c=code_blockt(); - if(!disable_runtime_checks) - { - codet 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); - } + codet 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]); array_put.add_source_location()=i_it->source_location; c.move_to_operands(array_put); @@ -1354,11 +1343,8 @@ codet java_bytecode_convert_methodt::convert_instructions( typet element_type=data_ptr.type().subtype(); dereference_exprt element(data_plus_offset, element_type); - if(!disable_runtime_checks) - { - c=get_array_bounds_check(deref, op[1], i_it->source_location); - c.add_source_location()=i_it->source_location; - } + c=get_array_bounds_check(deref, op[1], i_it->source_location); + c.add_source_location()=i_it->source_location; results[0]=java_bytecode_promotion(element); } else if(statement==patternt("?load")) @@ -1899,17 +1885,15 @@ codet java_bytecode_convert_methodt::convert_instructions( java_new_array.add_source_location()=i_it->source_location; c=code_blockt(); - if(!disable_runtime_checks) - { - // 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); - } + // 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(max_array_length!=0) { constant_exprt size_limit= @@ -1941,26 +1925,24 @@ codet java_bytecode_convert_methodt::convert_instructions( java_new_array.add_source_location()=i_it->source_location; code_blockt checkandcreate; - if(!disable_runtime_checks) + // 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); + + if(max_array_length!=0) { - // 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); - - if(max_array_length!=0) - { - constant_exprt size_limit= - 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); - } + constant_exprt size_limit= + 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); } + const exprt tmp=tmp_variable("newarray", ref_type); c=code_assignt(tmp, java_new_array); results[0]=tmp; @@ -2428,7 +2410,6 @@ void java_bytecode_convert_method( const java_bytecode_parse_treet::methodt &method, symbol_tablet &symbol_table, message_handlert &message_handler, - bool disable_runtime_checks, size_t max_array_length, safe_pointer > needed_methods, safe_pointer > needed_classes) @@ -2436,7 +2417,6 @@ void java_bytecode_convert_method( java_bytecode_convert_methodt java_bytecode_convert_method( symbol_table, message_handler, - disable_runtime_checks, max_array_length, needed_methods, needed_classes); diff --git a/src/java_bytecode/java_bytecode_convert_method.h b/src/java_bytecode/java_bytecode_convert_method.h index e81881f44e1..bc25eccb0c7 100644 --- a/src/java_bytecode/java_bytecode_convert_method.h +++ b/src/java_bytecode/java_bytecode_convert_method.h @@ -22,7 +22,6 @@ void java_bytecode_convert_method( const java_bytecode_parse_treet::methodt &, symbol_tablet &symbol_table, message_handlert &message_handler, - bool disable_runtime_checks, size_t max_array_length, safe_pointer > needed_methods, safe_pointer > needed_classes); @@ -33,7 +32,6 @@ inline void java_bytecode_convert_method( const java_bytecode_parse_treet::methodt &method, symbol_tablet &symbol_table, message_handlert &message_handler, - bool disable_runtime_checks, size_t max_array_length) { java_bytecode_convert_method( @@ -41,7 +39,6 @@ inline void java_bytecode_convert_method( method, symbol_table, message_handler, - disable_runtime_checks, max_array_length, safe_pointer >::create_null(), 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 4fb24c47b84..60b69a60f34 100644 --- a/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/src/java_bytecode/java_bytecode_convert_method_class.h @@ -30,13 +30,11 @@ class java_bytecode_convert_methodt:public messaget java_bytecode_convert_methodt( symbol_tablet &_symbol_table, message_handlert &_message_handler, - bool _disable_runtime_checks, size_t _max_array_length, safe_pointer > _needed_methods, safe_pointer > _needed_classes): messaget(_message_handler), symbol_table(_symbol_table), - disable_runtime_checks(_disable_runtime_checks), max_array_length(_max_array_length), needed_methods(_needed_methods), needed_classes(_needed_classes) @@ -56,7 +54,6 @@ class java_bytecode_convert_methodt:public messaget protected: symbol_tablet &symbol_table; - const bool disable_runtime_checks; const size_t max_array_length; safe_pointer > needed_methods; safe_pointer > needed_classes; diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 0e2eb25d0ec..ce52cfcece3 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -42,7 +42,6 @@ Function: java_bytecode_languaget::get_language_options void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) { - disable_runtime_checks=cmd.isset("disable-runtime-check"); assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null"); string_refinement_enabled=cmd.isset("string-refine"); if(cmd.isset("java-max-input-array-length")) @@ -518,7 +517,6 @@ bool java_bytecode_languaget::typecheck( c_it->second, symbol_table, get_message_handler(), - disable_runtime_checks, max_user_array_length, lazy_methods, lazy_methods_mode, @@ -639,7 +637,6 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion( *parsed_method.second, symbol_table, get_message_handler(), - disable_runtime_checks, max_user_array_length, safe_pointer >::create_non_null( &method_worklist2), @@ -754,7 +751,6 @@ void java_bytecode_languaget::convert_lazy_method( *lazy_method_entry.second, symtab, get_message_handler(), - disable_runtime_checks, max_user_array_length); } diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index 77689d6e12a..3c889322daf 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -94,12 +94,6 @@ class java_bytecode_languaget:public languaget std::vector main_jar_classes; java_class_loadert java_class_loader; bool assume_inputs_non_null; // assume inputs variables to be non-null - - bool disable_runtime_checks; // disable run-time checks for java, i.e., - // ASSERTS for - // - checkcast / instanceof - // - array bounds check - // - array size for newarray 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 lazy_methodst lazy_methods;