diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class b/regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class new file mode 100644 index 00000000000..4aeaf643291 Binary files /dev/null and b/regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class differ diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.java b/regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.java new file mode 100644 index 00000000000..265b89ec489 --- /dev/null +++ b/regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.java @@ -0,0 +1,12 @@ +public class ArrayIndexOutOfBoundsExceptionTest { + public static void main(String args[]) { + try { + int[] a=new int[4]; + a[4]=0; + throw new RuntimeException(); + } + catch (ArrayIndexOutOfBoundsException exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException1/test.desc b/regression/cbmc-java/ArrayIndexOutOfBoundsException1/test.desc new file mode 100644 index 00000000000..092cbf0b1f4 --- /dev/null +++ b/regression/cbmc-java/ArrayIndexOutOfBoundsException1/test.desc @@ -0,0 +1,9 @@ +CORE +ArrayIndexOutOfBoundsExceptionTest.class +--java-throw-runtime-exceptions +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 9 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/ClassCastException1/A.class b/regression/cbmc-java/ClassCastException1/A.class new file mode 100644 index 00000000000..3618c09b4ef Binary files /dev/null and b/regression/cbmc-java/ClassCastException1/A.class differ diff --git a/regression/cbmc-java/ClassCastException1/B.class b/regression/cbmc-java/ClassCastException1/B.class new file mode 100644 index 00000000000..e9257dc4427 Binary files /dev/null and b/regression/cbmc-java/ClassCastException1/B.class differ diff --git a/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.class b/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.class new file mode 100644 index 00000000000..de62bd5ca58 Binary files /dev/null and b/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.class differ diff --git a/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java b/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java new file mode 100644 index 00000000000..bb7eacd1647 --- /dev/null +++ b/regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java @@ -0,0 +1,13 @@ +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..983d5f730d8 --- /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 9 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 00000000000..5400c088442 Binary files /dev/null and b/regression/cbmc-java/ClassCastException2/A.class differ diff --git a/regression/cbmc-java/ClassCastException2/B.class b/regression/cbmc-java/ClassCastException2/B.class new file mode 100644 index 00000000000..57c02bfbefd Binary files /dev/null and b/regression/cbmc-java/ClassCastException2/B.class differ diff --git a/regression/cbmc-java/ClassCastException2/C.class b/regression/cbmc-java/ClassCastException2/C.class new file mode 100644 index 00000000000..3bff3313aa1 Binary files /dev/null and b/regression/cbmc-java/ClassCastException2/C.class differ diff --git a/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.class b/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.class new file mode 100644 index 00000000000..503940e149a Binary files /dev/null and b/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.class differ diff --git a/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.java b/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.java new file mode 100644 index 00000000000..d8979415dbc --- /dev/null +++ b/regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.java @@ -0,0 +1,21 @@ +class A {} + +class B extends A {} + +class C extends B {} + +public class ClassCastExceptionTest { + public static void main(String args[]) { + try { + A c = new C(); + B b = (B)c; + // TODO: an explicit throw is currently needed in order + // for CBMC to convert the exception handler + 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..c593280efe5 --- /dev/null +++ b/regression/cbmc-java/ClassCastException2/test.desc @@ -0,0 +1,8 @@ +CORE +ClassCastExceptionTest.class +--java-throw-runtime-exceptions +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NullPointerException2/A.class b/regression/cbmc-java/NullPointerException2/A.class new file mode 100644 index 00000000000..19526643bf2 Binary files /dev/null and b/regression/cbmc-java/NullPointerException2/A.class differ diff --git a/regression/cbmc-java/NullPointerException2/B.class b/regression/cbmc-java/NullPointerException2/B.class new file mode 100644 index 00000000000..f29cbafef50 Binary files /dev/null and b/regression/cbmc-java/NullPointerException2/B.class differ diff --git a/regression/cbmc-java/NullPointerException2/Test.class b/regression/cbmc-java/NullPointerException2/Test.class new file mode 100644 index 00000000000..e49a2d70d61 Binary files /dev/null and b/regression/cbmc-java/NullPointerException2/Test.class differ diff --git a/regression/cbmc-java/NullPointerException2/Test.java b/regression/cbmc-java/NullPointerException2/Test.java new file mode 100644 index 00000000000..cf04d9edefb --- /dev/null +++ b/regression/cbmc-java/NullPointerException2/Test.java @@ -0,0 +1,20 @@ +class B extends RuntimeException {} + +class A { + int i; +} + +public class Test { + public static void main(String args[]) { + A a=null; + try { + a.i=0; + // TODO: an explicit throw is currently needed in order + // for CBMC to convert the exception handler + throw new B(); + } + catch (NullPointerException exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/NullPointerException2/test.desc b/regression/cbmc-java/NullPointerException2/test.desc new file mode 100644 index 00000000000..ed7e923ae16 --- /dev/null +++ b/regression/cbmc-java/NullPointerException2/test.desc @@ -0,0 +1,9 @@ +CORE +Test.class +--java-throw-runtime-exceptions +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file Test.java line 17 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NullPointerException3/A.class b/regression/cbmc-java/NullPointerException3/A.class new file mode 100644 index 00000000000..19526643bf2 Binary files /dev/null and b/regression/cbmc-java/NullPointerException3/A.class differ diff --git a/regression/cbmc-java/NullPointerException3/B.class b/regression/cbmc-java/NullPointerException3/B.class new file mode 100644 index 00000000000..f29cbafef50 Binary files /dev/null and b/regression/cbmc-java/NullPointerException3/B.class differ diff --git a/regression/cbmc-java/NullPointerException3/Test.class b/regression/cbmc-java/NullPointerException3/Test.class new file mode 100644 index 00000000000..77c124a4b86 Binary files /dev/null and b/regression/cbmc-java/NullPointerException3/Test.class differ diff --git a/regression/cbmc-java/NullPointerException3/Test.java b/regression/cbmc-java/NullPointerException3/Test.java new file mode 100644 index 00000000000..35df442dd61 --- /dev/null +++ b/regression/cbmc-java/NullPointerException3/Test.java @@ -0,0 +1,20 @@ +class B extends RuntimeException {} + +class A { + int i; +} + +public class Test { + public static void main(String args[]) { + A a=null; + try { + int i=a.i; + // TODO: an explicit throw is currently needed in order + // for CBMC to convert the exception handler + throw new B(); + } + catch (NullPointerException exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/NullPointerException3/test.desc b/regression/cbmc-java/NullPointerException3/test.desc new file mode 100644 index 00000000000..ed7e923ae16 --- /dev/null +++ b/regression/cbmc-java/NullPointerException3/test.desc @@ -0,0 +1,9 @@ +CORE +Test.class +--java-throw-runtime-exceptions +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file Test.java line 17 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index eac3893130d..d1dd4947e17 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -1070,6 +1070,7 @@ void cbmc_parse_optionst::help() // NOLINTNEXTLINE(whitespace/line_length) " --java-max-vla-length limit the length of user-code-created arrays\n" // NOLINTNEXTLINE(whitespace/line_length) + " --java-throw-runtime-exceptions Make implicit runtime exceptions explicit" " --java-cp-include-files regexp or JSON list of files to load (with '@' prefix)\n" " --java-unwind-enum-static try to unwind loops in static initialization of enums\n" "\n" diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 4f43637234a..145ff8e6e77 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -65,6 +65,7 @@ class optionst; "(graphml-witness):" \ "(java-max-vla-length):(java-unwind-enum-static)" \ "(java-cp-include-files):" \ + "(java-throw-runtime-exceptions)" \ "(localize-faults)(localize-faults-method):" \ "(lazy-methods)" \ "(test-invariant-failure)" \ diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index 0334b20595f..5125f2f6664 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -5,6 +5,7 @@ SRC = bytecode_info.cpp \ jar_file.cpp \ java_bytecode_convert_class.cpp \ java_bytecode_convert_method.cpp \ + java_bytecode_instrument.cpp \ java_bytecode_internal_additions.cpp \ java_bytecode_language.cpp \ java_bytecode_parse_tree.cpp \ diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index ada2468e924..9b6d53841e3 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_types.h" #include "java_bytecode_convert_method.h" #include "java_bytecode_language.h" +#include "java_utils.h" #include #include @@ -56,7 +57,10 @@ class java_bytecode_convert_classt:public messaget string_preprocess.add_string_type( parse_tree.parsed_class.name, symbol_table); else if(!loading_success) - generate_class_stub(parse_tree.parsed_class.name); + generate_class_stub( + parse_tree.parsed_class.name, + symbol_table, + get_message_handler()); } typedef java_bytecode_parse_treet::classt classt; @@ -73,7 +77,6 @@ class java_bytecode_convert_classt:public messaget void convert(const classt &c); void convert(symbolt &class_symbol, const fieldt &f); - void generate_class_stub(const irep_idt &class_name); void add_array_types(); }; @@ -171,40 +174,6 @@ void java_bytecode_convert_classt::convert(const classt &c) java_root_class(*class_symbol); } -void java_bytecode_convert_classt::generate_class_stub( - const irep_idt &class_name) -{ - class_typet class_type; - - class_type.set_tag(class_name); - class_type.set(ID_base_name, class_name); - - class_type.set(ID_incomplete_class, true); - - // produce class symbol - symbolt new_symbol; - new_symbol.base_name=class_name; - new_symbol.pretty_name=class_name; - new_symbol.name="java::"+id2string(class_name); - class_type.set(ID_name, new_symbol.name); - new_symbol.type=class_type; - new_symbol.mode=ID_java; - new_symbol.is_type=true; - - symbolt *class_symbol; - - if(symbol_table.move(new_symbol, class_symbol)) - { - warning() << "stub class symbol " << new_symbol.name - << " already exists" << eom; - } - else - { - // create the class identifier etc - java_root_class(*class_symbol); - } -} - void java_bytecode_convert_classt::convert( symbolt &class_symbol, const fieldt &f) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 14b67ba330f..ef6b1dd1bb3 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -509,39 +509,14 @@ static member_exprt to_member(const exprt &pointer, const exprt &fieldref) const dereference_exprt obj_deref(pointer2, class_type); - return member_exprt( + member_exprt member_expr( obj_deref, fieldref.get(ID_component_name), fieldref.type()); -} -codet java_bytecode_convert_methodt::get_array_bounds_check( - const exprt &arraystruct, - const exprt &idx, - const source_locationt &original_sloc) -{ - constant_exprt intzero=from_integer(0, java_int_type()); - binary_relation_exprt gezero(idx, ID_ge, intzero); - const member_exprt length_field(arraystruct, "length", java_int_type()); - binary_relation_exprt ltlength(idx, ID_lt, length_field); - code_blockt bounds_checks; - - bounds_checks.add(code_assertt(gezero)); - bounds_checks.operands().back().add_source_location()=original_sloc; - bounds_checks.operands().back().add_source_location() - .set_comment("Array index < 0"); - bounds_checks.operands().back().add_source_location() - .set_property_class("array-index-out-of-bounds-low"); - bounds_checks.add(code_assertt(ltlength)); - - bounds_checks.operands().back().add_source_location()=original_sloc; - bounds_checks.operands().back().add_source_location() - .set_comment("Array index >= length"); - 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; + // tag it so it's easy to identify during instrumentation + member_expr.set(ID_java_member_access, true); + return member_expr; } /// Find all goto statements in 'repl' that target 'old_label' and redirect them @@ -1256,50 +1231,26 @@ codet java_bytecode_convert_methodt::convert_instructions( else if(statement=="athrow") { 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); 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; } 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); + // we add this assert such that we can recognise it + // during the instrumentation phase + c=std::move(assert_class); results[0]=op[0]; } else if(statement=="invokedynamic") @@ -1525,17 +1476,12 @@ codet java_bytecode_convert_methodt::convert_instructions( pointer_typet(java_type_from_char(type_char))); plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type()); + // tag it so it's easy to identify during instrumentation + data_plus_offset.set(ID_java_array_access, true); typet element_type=data_ptr.type().subtype(); 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); - 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); + c=code_assignt(element, op[2]); c.add_source_location()=i_it->source_location; } else if(statement==patternt("?store")) @@ -1569,11 +1515,10 @@ codet java_bytecode_convert_methodt::convert_instructions( pointer_typet(java_type_from_char(type_char))); plus_exprt data_plus_offset(data_ptr, op[1], data_ptr.type()); + // tag it so it's easy to identify during instrumentation + data_plus_offset.set(ID_java_array_access, true); typet element_type=data_ptr.type().subtype(); dereference_exprt element(data_plus_offset, element_type); - - 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")) @@ -2136,14 +2081,6 @@ 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(max_array_length!=0) { @@ -2175,15 +2112,7 @@ 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); + code_blockt create; if(max_array_length!=0) { @@ -2191,11 +2120,12 @@ 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); + create.move_to_operands(assume_le_max_size); } const exprt tmp=tmp_variable("newarray", ref_type); - c=code_assignt(tmp, java_new_array); + create.copy_to_operands(code_assignt(tmp, java_new_array)); + c=std::move(create); results[0]=tmp; } else if(statement=="arraylength") diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h index f44df98be49..85537034894 100644 --- a/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/src/java_bytecode/java_bytecode_convert_method_class.h @@ -123,11 +123,6 @@ class java_bytecode_convert_methodt:public messaget INST_INDEX_CONST=3 }; - codet get_array_bounds_check( - const exprt &arraystruct, - const exprt &idx, - const source_locationt &original_sloc); - // return corresponding reference of variable const variablet &find_variable_for_slot( size_t address, diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp new file mode 100644 index 00000000000..9ec9f3293b2 --- /dev/null +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -0,0 +1,522 @@ +/*******************************************************************\ + +Module: Instrument codet with assertions/runtime exceptions + +Author: Cristina David + +Date: June 2017 + +\*******************************************************************/ + +#include +#include +#include +#include + +#include + +#include "java_bytecode_convert_class.h" +#include "java_bytecode_instrument.h" +#include "java_entry_point.h" +#include "java_object_factory.h" +#include "java_root_class.h" +#include "java_types.h" +#include "java_utils.h" + +class java_bytecode_instrumentt:public messaget +{ +public: + java_bytecode_instrumentt( + symbol_tablet &_symbol_table, + const bool _throw_runtime_exceptions, + message_handlert &_message_handler, + const size_t _max_array_length): + symbol_table(_symbol_table), + throw_runtime_exceptions(_throw_runtime_exceptions), + message_handler(_message_handler), + max_array_length(_max_array_length) + { + } + + void operator()(exprt &expr); + +protected: + symbol_tablet &symbol_table; + const bool throw_runtime_exceptions; + message_handlert &message_handler; + const size_t max_array_length; + + codet throw_exception( + const exprt &cond, + const source_locationt &original_loc, + const irep_idt &exc_name); + + codet check_array_access( + const exprt &array_struct, + const exprt &idx, + const source_locationt &original_loc); + + codet check_null_dereference( + const exprt &expr, + const source_locationt &original_loc, + const bool assertion_enabled); + + codet check_class_cast( + const exprt &class1, + const exprt &class2, + const source_locationt &original_loc); + + codet check_array_length( + const exprt &length, + const source_locationt &original_loc); + + void instrument_code(exprt &expr); + codet instrument_expr(const exprt &expr); +}; + + +/// Creates a class stub for exc_name and generates a +/// conditional GOTO such that exc_name is thrown when +/// cond is met. +/// \par parameters: `cond`: condition to be met in order +/// to throw an exception +/// `original_loc`: source location in the original program +/// `exc_name`: the name of the exception to be thrown +/// \return Returns the code initialising the throwing the +/// exception +codet java_bytecode_instrumentt::throw_exception( + const exprt &cond, + const source_locationt &original_loc, + const irep_idt &exc_name) +{ + 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)) + { + generate_class_stub( + exc_name, + symbol_table, + get_message_handler()); + const symbolt &exc_symbol=symbol_table.lookup( + "java::"+id2string(exc_name)); + + // 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_table.lookup(exc_obj_name).symbol_expr(); + + side_effect_expr_throwt throw_expr; + throw_expr.add_source_location()=original_loc; + 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; +} + +/// Checks whether the array access array_struct[idx] is out-of-bounds, +/// and throws ArrayIndexOutofBoundsException/generates an assertion +/// if necessary; Exceptions are thrown when the `throw_runtime_exceptions` +/// flag is set. Otherwise, assertions are emitted. +/// \par parameters: `array_struct`: the array being accessed +/// `idx`: index into the array +/// `original_loc: source location in the original code +/// \return Based on the value of the flag `throw_runtime_exceptions`, +/// it returns code that either throws an ArrayIndexOutPfBoundsException +/// or emits an assertion checking the array access +codet java_bytecode_instrumentt::check_array_access( + 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 ge_zero(idx, ID_ge, zero); + const member_exprt length_field(array_struct, "length", java_int_type()); + const binary_relation_exprt lt_length(idx, ID_lt, length_field); + const and_exprt cond(ge_zero, lt_length); + + if(throw_runtime_exceptions) + return throw_exception( + not_exprt(cond), + original_loc, + "java.lang.ArrayIndexOutOfBoundsException"); + + code_blockt bounds_checks; + bounds_checks.add(code_assertt(ge_zero)); + bounds_checks.operands().back().add_source_location()=original_loc; + bounds_checks.operands().back().add_source_location() + .set_comment("Array index should be >= 0"); + bounds_checks.operands().back().add_source_location() + .set_property_class("array-index-out-of-bounds-low"); + + bounds_checks.add(code_assertt(lt_length)); + bounds_checks.operands().back().add_source_location()=original_loc; + bounds_checks.operands().back().add_source_location() + .set_comment("Array index should be < length"); + bounds_checks.operands().back().add_source_location() + .set_property_class("array-index-out-of-bounds-high"); + + return bounds_checks; +} + +/// Checks whether `class1` is an instance of `class2` and throws +/// ClassCastException/generates an assertion when necessary; +/// Exceptions are thrown when the `throw_runtime_exceptions` flag is set. +/// Otherwise, assertions are emitted. +/// \par parameters: `class1`: the subclass +/// `class2`: the super class +/// `original_loc: source location in the original code +/// \return Based on the value of the flag `throw_runtime_exceptions`, +/// it returns code that either throws an ClassCastException or emits an +/// assertion checking the subtype relation +codet java_bytecode_instrumentt::check_class_cast( + const exprt &class1, + const exprt &class2, + const source_locationt &original_loc) +{ + 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, not_exprt(class_cast_check)); + + if(throw_runtime_exceptions) + return throw_exception( + and_expr, + original_loc, + "ClassCastException"); + + code_assertt assert_class(class_cast_check); + assert_class.add_source_location(). + set_comment("Dynamic cast check"); + assert_class.add_source_location(). + set_property_class("bad-dynamic-cast"); + + code_ifthenelset conditional_check; + conditional_check.cond()=std::move(op_not_null); + conditional_check.then_case()=std::move(assert_class); + return conditional_check; +} + +/// Checks whether `expr` is null and throws NullPointerException/ +/// generates an assertion when necessary; +/// Exceptions are thrown when the `throw_runtime_exceptions` flag is set. +/// Otherwise, assertions are emitted. +/// \par parameters: `expr`: the checked expression +/// `original_loc: source location in the original code +/// \return Based on the value of the flag `throw_runtime_exceptions`, +/// it returns code that either throws an NullPointerException or emits an +/// assertion checking the subtype relation +codet java_bytecode_instrumentt::check_null_dereference( + const exprt &expr, + const source_locationt &original_loc, + const bool assertion_enabled) +{ + exprt local_expr=expr; + empty_typet voidt; + pointer_typet voidptr(voidt); + + if(local_expr.type()!=voidptr) + local_expr.make_typecast(voidptr); + + const equal_exprt equal_expr( + local_expr, + null_pointer_exprt(voidptr)); + + if(throw_runtime_exceptions) + return throw_exception( + equal_expr, + original_loc, "java.lang.NullPointerException"); + + if(assertion_enabled) + { + code_assertt check((not_exprt(equal_expr))); + check.add_source_location() + .set_comment("Throw null"); + check.add_source_location() + .set_property_class("null-pointer-exception"); + return check; + } + + return code_skipt(); +} + +/// Checks whether `length`>=0 and throws NegativeArraySizeException/ +/// generates an assertion when necessary; +/// Exceptions are thrown when the `throw_runtime_exceptions` flag is set. +/// Otherwise, assertions are emitted. +/// \par parameters: `length`: the checked length +/// `original_loc: source location in the original code +/// \return Based on the value of the flag `throw_runtime_exceptions`, +/// it returns code that either throws an NegativeArraySizeException +/// or emits an assertion checking the subtype relation +codet java_bytecode_instrumentt::check_array_length( + const exprt &length, + const source_locationt &original_loc) +{ + const constant_exprt &zero=from_integer(0, java_int_type()); + const binary_relation_exprt ge_zero(length, ID_ge, zero); + + if(throw_runtime_exceptions) + return throw_exception( + not_exprt(ge_zero), + original_loc, + "java.lang.NegativeArraySizeException"); + + code_assertt check(ge_zero); + check.add_source_location().set_comment("Array size should be >= 0"); + check.add_source_location() + .set_property_class("array-create-negative-size"); + return check; +} + +/// Augments `expr` with instrumentation in the form of either +/// assertions or runtime exceptions +/// \par parameters: `expr`: the expression to be instrumented +void java_bytecode_instrumentt::instrument_code(exprt &expr) +{ + codet &code=to_code(expr); + + const irep_idt &statement=code.get_statement(); + + if(statement==ID_assign) + { + code_assignt code_assign=to_code_assign(code); + + code_blockt block; + block.copy_to_operands(instrument_expr(code_assign.lhs())); + block.copy_to_operands(instrument_expr(code_assign.rhs())); + block.copy_to_operands(code_assign); + + code=block; + } + else if(statement==ID_expression) + { + code_expressiont code_expression= + to_code_expression(code); + + code_blockt block; + block.copy_to_operands( + instrument_expr(code_expression.expression())); + block.copy_to_operands(code_expression); + code=block; + } + else if(statement==ID_assert) + { + code_assertt code_assert=to_code_assert(code); + + // does this correspond to checkcast? + if(code_assert.assertion().id()==ID_java_instanceof) + { + code_blockt block; + + INVARIANT( + code_assert.assertion().operands().size()==2, + "Instanceof should have 2 operands"); + + block.copy_to_operands( + check_class_cast( + code_assert.assertion().op0(), + code_assert.assertion().op1(), + code_assert.source_location())); + block.copy_to_operands(code_assert); + code=block; + } + } + else if(statement==ID_block) + { + Forall_operands(it, code) + instrument_code(to_code(*it)); + } + else if(statement==ID_label) + { + code_labelt &code_label=to_code_label(code); + instrument_code(code_label.code()); + } + else if(statement==ID_ifthenelse) + { + code_blockt block; + code_ifthenelset &code_ifthenelse=to_code_ifthenelse(code); + block.copy_to_operands(instrument_expr(code_ifthenelse.cond())); + instrument_code(code_ifthenelse.then_case()); + if(code_ifthenelse.else_case().is_not_nil()) + instrument_code(code_ifthenelse.else_case()); + block.copy_to_operands(code); + code=block; + } + else if(statement==ID_switch) + { + code_blockt block; + code_switcht &code_switch=to_code_switch(code); + block.copy_to_operands( + instrument_expr(code_switch.value())); + block.copy_to_operands( + instrument_expr(code_switch.body())); + block.copy_to_operands(code); + code=block; + } + else if(statement==ID_return) + { + if(code.operands().size()==1) + { + code_blockt block; + block.copy_to_operands(instrument_expr(code.op0())); + block.copy_to_operands(code); + code=block; + } + } + else if(statement==ID_function_call) + { + code_blockt block; + code_function_callt &code_function_call=to_code_function_call(code); + block.copy_to_operands(instrument_expr(code_function_call.lhs())); + block.copy_to_operands(instrument_expr(code_function_call.function())); + + for(code_function_callt::argumentst::iterator + a_it=code_function_call.arguments().begin(); + a_it!=code_function_call.arguments().end(); + a_it++) + block.copy_to_operands(instrument_expr(*a_it)); + + block.copy_to_operands(code); + code=block; + } +} + +/// Computes the instrumentation for `expr` in the form of +/// either assertions or runtime exceptions. +/// \par parameters: `expr`: the expression for which we compute +/// instrumentation +/// \return: The instrumentation required for `expr` +codet java_bytecode_instrumentt::instrument_expr( + const exprt &expr) +{ + if(expr.id()==ID_plus && + expr.get_bool(ID_java_array_access)) + { + // this corresponds to ?aload and ?astore so + // we check that 0<=index=0 + return check_array_length( + expr.op0(), + expr.source_location()); + } + else if(expr.id()==ID_member && + expr.get_bool(ID_java_member_access)) + { + // this corresponds to either getfield or putfield + // so we must check null pointer dereference + const member_exprt &member_expr=to_member_expr(expr); + if(member_expr.op0().id()==ID_dereference) + { + const dereference_exprt dereference_expr= + to_dereference_expr(member_expr.op0()); + codet null_dereference_check= + check_null_dereference( + dereference_expr.op0(), + dereference_expr.source_location(), + false); + return null_dereference_check; + } + } + + if(!expr.has_operands()) + return code_skipt(); + + code_blockt block; + forall_operands(it, expr) + { + block.copy_to_operands(instrument_expr(*it)); + } + return block; +} + +/// Instruments `expr` +/// \par parameters: `expr`: the expression to be instrumented +void java_bytecode_instrumentt::operator()(exprt &expr) +{ + instrument_code(expr); +} + +/// Instruments all the code in the symbol_table with +/// runtime exceptions or corresponding assertions. +/// Exceptions are thrown when the `throw_runtime_exceptions` flag is set. +/// Otherwise, assertions are emitted. +/// \par parameters: `symbol_table`: the symbol table to instrument +/// `throw_runtime_exceptions`: flag determining whether we instrument the code +/// with runtime exceptions or with assertions. The former applies if this flag +/// is set to true. +/// `max_array_length`: maximum array length; the only reason we need this is +/// in order to be able to call the object factory to create exceptions. +void java_bytecode_instrument( + symbol_tablet &symbol_table, + const bool throw_runtime_exceptions, + message_handlert &message_handler, + const size_t max_array_length) +{ + java_bytecode_instrumentt instrument( + symbol_table, + throw_runtime_exceptions, + message_handler, + max_array_length); + + Forall_symbols(s_it, symbol_table.symbols) + { + if(s_it->second.value.id()==ID_code) + instrument(s_it->second.value); + } +} diff --git a/src/java_bytecode/java_bytecode_instrument.h b/src/java_bytecode/java_bytecode_instrument.h new file mode 100644 index 00000000000..0d987746bce --- /dev/null +++ b/src/java_bytecode/java_bytecode_instrument.h @@ -0,0 +1,19 @@ +/*******************************************************************\ + +Module: Instrument codet with assertions/runtime exceptions + +Author: Cristina David + +Date: June 2017 + +\*******************************************************************/ + +#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H +#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H + +void java_bytecode_instrument( + symbol_tablet &symbol_table, + const bool throw_runtime_exceptions, + message_handlert &_message_handler, + const size_t max_array_length); +#endif diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index e024653bef7..297484ad82d 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_bytecode_convert_class.h" #include "java_bytecode_convert_method.h" #include "java_bytecode_internal_additions.h" +#include "java_bytecode_instrument.h" #include "java_bytecode_typecheck.h" #include "java_entry_point.h" #include "java_bytecode_parser.h" @@ -36,6 +37,7 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) { assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null"); string_refinement_enabled=cmd.isset("refine-strings"); + throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions"); if(cmd.isset("java-max-input-array-length")) max_nondet_array_length= std::stoi(cmd.get_value("java-max-input-array-length")); @@ -438,6 +440,13 @@ bool java_bytecode_languaget::typecheck( } // Otherwise our caller is in charge of elaborating methods on demand. + // now instrument runtime exceptions + java_bytecode_instrument( + symbol_table, + throw_runtime_exceptions, + get_message_handler(), + max_nondet_array_length); + // now typecheck all if(java_bytecode_typecheck( symbol_table, get_message_handler(), string_refinement_enabled)) diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index c107ffd0267..d0c9c0ba0f7 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -103,6 +103,7 @@ class java_bytecode_languaget:public languaget lazy_methodst lazy_methods; lazy_methods_modet lazy_methods_mode; bool string_refinement_enabled; + bool throw_runtime_exceptions; java_string_library_preprocesst string_preprocess; std::string java_cp_include_files; }; diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index 9f8be11e4ad..5643d819a28 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -6,12 +6,13 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ - +#include +#include #include #include -#include #include +#include "java_root_class.h" #include "java_utils.h" #include "java_types.h" @@ -54,7 +55,47 @@ unsigned java_method_parameter_slots(const code_typet &t) return slots; } + const std::string java_class_to_package(const std::string &canonical_classname) { return trim_from_last_delimiter(canonical_classname, '.'); } + +void generate_class_stub( + const irep_idt &class_name, + symbol_tablet &symbol_table, + message_handlert &message_handler) +{ + class_typet class_type; + + class_type.set_tag(class_name); + class_type.set(ID_base_name, class_name); + + class_type.set(ID_incomplete_class, true); + + // produce class symbol + symbolt new_symbol; + new_symbol.base_name=class_name; + new_symbol.pretty_name=class_name; + new_symbol.name="java::"+id2string(class_name); + class_type.set(ID_name, new_symbol.name); + new_symbol.type=class_type; + new_symbol.mode=ID_java; + new_symbol.is_type=true; + + symbolt *class_symbol; + + if(symbol_table.move(new_symbol, class_symbol)) + { + messaget message(message_handler); + message.warning() << + "stub class symbol " << + new_symbol.name << + " already exists" << messaget::eom; + } + else + { + // create the class identifier etc + java_root_class(*class_symbol); + } +} diff --git a/src/java_bytecode/java_utils.h b/src/java_bytecode/java_utils.h index ef64ff9e18e..77cb35825b0 100644 --- a/src/java_bytecode/java_utils.h +++ b/src/java_bytecode/java_utils.h @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include "java_bytecode_parse_tree.h" @@ -16,6 +17,11 @@ Author: Daniel Kroening, kroening@kroening.com bool java_is_array_type(const typet &type); +void generate_class_stub( + const irep_idt &class_name, + symbol_tablet &symbol_table, + message_handlert &message_handler); + /// Returns the number of JVM local variables (slots) taken by a local variable /// that, when translated to goto, has type \p t. unsigned java_local_variable_slots(const typet &t); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 8a22f226fc0..e24d7cd981f 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -815,6 +815,8 @@ IREP_ID_ONE(skip_initialize) IREP_ID_ONE(basic_block_covered_lines) IREP_ID_ONE(is_nondet_nullable) IREP_ID_ONE(array_replace) +IREP_ID_ONE(java_array_access) +IREP_ID_ONE(java_member_access) #undef IREP_ID_ONE #undef IREP_ID_TWO