diff --git a/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo$1.class b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo$1.class new file mode 100644 index 00000000000..56f0ef4b05a Binary files /dev/null and b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo$1.class differ diff --git a/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.class b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.class new file mode 100644 index 00000000000..c7dfc05289a Binary files /dev/null and b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.class differ diff --git a/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.java b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.java new file mode 100644 index 00000000000..af6f1bfdcf0 --- /dev/null +++ b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/Foo.java @@ -0,0 +1,16 @@ +package com.diffblue.regression; + +public class Foo { + public int foo(MyEnum e) { + if (e == null) return 0; + switch (e) { + case A: + return 1; + case B: + return 2; + case C: + return 3; + } + return 5; + } +} diff --git a/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/MyEnum.class b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/MyEnum.class new file mode 100644 index 00000000000..c513fb41e02 Binary files /dev/null and b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/MyEnum.class differ diff --git a/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/MyEnum.java b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/MyEnum.java new file mode 100644 index 00000000000..e0adb6f06d0 --- /dev/null +++ b/jbmc/regression/jbmc/enum_switch/com/diffblue/regression/MyEnum.java @@ -0,0 +1,5 @@ +package com.diffblue.regression; + +enum MyEnum { + A, B, C, D; +} diff --git a/jbmc/regression/jbmc/enum_switch/test.desc b/jbmc/regression/jbmc/enum_switch/test.desc new file mode 100644 index 00000000000..f525e3e15d4 --- /dev/null +++ b/jbmc/regression/jbmc/enum_switch/test.desc @@ -0,0 +1,10 @@ +CORE symex-driven-lazy-loading-expected-failure +com/diffblue/regression/Foo.class +--trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 10 --function "com.diffblue.regression.Foo.foo" --java-unwind-enum-static +line 8.*SATISFIED +line 10.*SATISFIED +line 12.*SATISFIED +line 14.*SATISFIED +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.class b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.class new file mode 100644 index 00000000000..e977adcf00c Binary files /dev/null and b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.class differ diff --git a/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.java b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.java new file mode 100644 index 00000000000..bc5d1f617b6 --- /dev/null +++ b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/EnumIter.java @@ -0,0 +1,8 @@ +package com.diffblue.regression; +public class EnumIter { + int f() { + MyEnum[] a = MyEnum.values(); + int num = a[2].ordinal() + a[3].ordinal(); + return num ; + } +} diff --git a/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/MyEnum.class b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/MyEnum.class new file mode 100644 index 00000000000..c513fb41e02 Binary files /dev/null and b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/MyEnum.class differ diff --git a/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/MyEnum.java b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/MyEnum.java new file mode 100644 index 00000000000..e0adb6f06d0 --- /dev/null +++ b/jbmc/regression/jbmc/enum_values_clone/com/diffblue/regression/MyEnum.java @@ -0,0 +1,5 @@ +package com.diffblue.regression; + +enum MyEnum { + A, B, C, D; +} diff --git a/jbmc/regression/jbmc/enum_values_clone/test.desc b/jbmc/regression/jbmc/enum_values_clone/test.desc new file mode 100644 index 00000000000..7009afb0ed1 --- /dev/null +++ b/jbmc/regression/jbmc/enum_values_clone/test.desc @@ -0,0 +1,7 @@ +CORE symex-driven-lazy-loading-expected-failure +com/diffblue/regression/EnumIter.class +--trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static +\d+ of \d+ covered \(100\.0%\) +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.class b/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.class new file mode 100644 index 00000000000..3c7ca188bc9 Binary files /dev/null and b/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.class differ diff --git a/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.java b/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.java new file mode 100644 index 00000000000..4dcfdfca3d2 --- /dev/null +++ b/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/EnumIter.java @@ -0,0 +1,7 @@ +package com.diffblue.regression; +public class EnumIter { + String f() { + MyEnum[] a = MyEnum.values(); + return a[2].name() + a[3].name(); + } +} diff --git a/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/MyEnum.class b/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/MyEnum.class new file mode 100644 index 00000000000..c513fb41e02 Binary files /dev/null and b/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/MyEnum.class differ diff --git a/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/MyEnum.java b/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/MyEnum.java new file mode 100644 index 00000000000..e0adb6f06d0 --- /dev/null +++ b/jbmc/regression/jbmc/enum_values_clone_name/com/diffblue/regression/MyEnum.java @@ -0,0 +1,5 @@ +package com.diffblue.regression; + +enum MyEnum { + A, B, C, D; +} diff --git a/jbmc/regression/jbmc/enum_values_clone_name/test.desc b/jbmc/regression/jbmc/enum_values_clone_name/test.desc new file mode 100644 index 00000000000..66031ef1e9d --- /dev/null +++ b/jbmc/regression/jbmc/enum_values_clone_name/test.desc @@ -0,0 +1,7 @@ +CORE symex-driven-lazy-loading-expected-failure +com/diffblue/regression/EnumIter.class +--trace --cover location --depth 1024 --java-max-vla-length 16 --refine-strings --max-nondet-string-length 20 --string-printable --unwind 2 --function "com.diffblue.regression.EnumIter.f" --java-unwind-enum-static +\d+ of \d+ covered \(100\.0%\) +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/jbmc/src/java_bytecode/Makefile b/jbmc/src/java_bytecode/Makefile index c3964a40375..f3336d20659 100644 --- a/jbmc/src/java_bytecode/Makefile +++ b/jbmc/src/java_bytecode/Makefile @@ -20,6 +20,7 @@ SRC = bytecode_info.cpp \ java_bytecode_typecheck_type.cpp \ java_class_loader.cpp \ java_class_loader_limit.cpp \ + java_enum_array_clone_unwind_handler.cpp \ java_enum_static_init_unwind_handler.cpp \ java_entry_point.cpp \ java_local_variable_table.cpp \ diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 36ad3bff30d..d20cbd13dee 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -115,9 +115,6 @@ class java_bytecode_convert_classt:public messaget void convert(const classt &c, const overlay_classest &overlay_classes); void convert(symbolt &class_symbol, const fieldt &f); - // see definition below for more info - static void add_array_types(symbol_tablet &symbol_table); - static bool is_overlay_method(const methodt &method) { return method.has_annotation(ID_overlay_method); @@ -717,182 +714,6 @@ void java_bytecode_convert_classt::convert( } } -/// Register in the \p symbol_table new symbols for the objects -/// java::array[X] where X is byte, float, int, char... -void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table) -{ - const std::string letters="ijsbcfdza"; - - for(const char l : letters) - { - symbol_typet symbol_type= - to_symbol_type(java_array_type(l).subtype()); - - const irep_idt &symbol_type_identifier=symbol_type.get_identifier(); - if(symbol_table.has_symbol(symbol_type_identifier)) - return; - - java_class_typet class_type; - // we have the base class, java.lang.Object, length and data - // of appropriate type - class_type.set_tag(symbol_type_identifier); - // Note that non-array types don't have "java::" at the beginning of their - // tag, and their name is "java::" + their tag. Since arrays do have - // "java::" at the beginning of their tag we set the name to be the same as - // the tag. - class_type.set_name(symbol_type_identifier); - - class_type.components().reserve(3); - class_typet::componentt base_class_component( - "@java.lang.Object", symbol_typet("java::java.lang.Object")); - base_class_component.set_pretty_name("@java.lang.Object"); - base_class_component.set_base_name("@java.lang.Object"); - class_type.components().push_back(base_class_component); - - class_typet::componentt length_component("length", java_int_type()); - length_component.set_pretty_name("length"); - length_component.set_base_name("length"); - class_type.components().push_back(length_component); - - class_typet::componentt data_component( - "data", java_reference_type(java_type_from_char(l))); - data_component.set_pretty_name("data"); - data_component.set_base_name("data"); - class_type.components().push_back(data_component); - - class_type.add_base(symbol_typet("java::java.lang.Object")); - - INVARIANT( - is_valid_java_array(class_type), - "Constructed a new type representing a Java Array " - "object that doesn't match expectations"); - - symbolt symbol; - symbol.name=symbol_type_identifier; - symbol.base_name=symbol_type.get(ID_C_base_name); - symbol.is_type=true; - symbol.type = class_type; - symbol.mode = ID_java; - symbol_table.add(symbol); - - // Also provide a clone method: - // ---------------------------- - - const irep_idt clone_name= - id2string(symbol_type_identifier)+".clone:()Ljava/lang/Object;"; - code_typet::parametert this_param; - this_param.set_identifier(id2string(clone_name)+"::this"); - this_param.set_base_name("this"); - this_param.set_this(); - this_param.type()=java_reference_type(symbol_type); - const code_typet clone_type({this_param}, java_lang_object_type()); - - parameter_symbolt this_symbol; - this_symbol.name=this_param.get_identifier(); - this_symbol.base_name=this_param.get_base_name(); - this_symbol.pretty_name=this_symbol.base_name; - this_symbol.type=this_param.type(); - this_symbol.mode=ID_java; - symbol_table.add(this_symbol); - - const irep_idt local_name= - id2string(clone_name)+"::cloned_array"; - auxiliary_symbolt local_symbol; - local_symbol.name=local_name; - local_symbol.base_name="cloned_array"; - local_symbol.pretty_name=local_symbol.base_name; - local_symbol.type=java_reference_type(symbol_type); - local_symbol.mode=ID_java; - symbol_table.add(local_symbol); - const auto &local_symexpr=local_symbol.symbol_expr(); - - code_blockt clone_body; - - code_declt declare_cloned(local_symexpr); - clone_body.move_to_operands(declare_cloned); - - side_effect_exprt java_new_array( - ID_java_new_array, - java_reference_type(symbol_type)); - dereference_exprt old_array(this_symbol.symbol_expr(), symbol_type); - dereference_exprt new_array(local_symexpr, symbol_type); - member_exprt old_length( - old_array, length_component.get_name(), length_component.type()); - java_new_array.copy_to_operands(old_length); - code_assignt create_blank(local_symexpr, java_new_array); - clone_body.move_to_operands(create_blank); - - member_exprt old_data( - old_array, data_component.get_name(), data_component.type()); - member_exprt new_data( - new_array, data_component.get_name(), data_component.type()); - - /* - // TODO use this instead of a loop. - codet array_copy; - array_copy.set_statement(ID_array_copy); - array_copy.move_to_operands(new_data); - array_copy.move_to_operands(old_data); - clone_body.move_to_operands(array_copy); - */ - - // Begin for-loop to replace: - - const irep_idt index_name= - id2string(clone_name)+"::index"; - auxiliary_symbolt index_symbol; - index_symbol.name=index_name; - index_symbol.base_name="index"; - index_symbol.pretty_name=index_symbol.base_name; - index_symbol.type = length_component.type(); - index_symbol.mode=ID_java; - symbol_table.add(index_symbol); - const auto &index_symexpr=index_symbol.symbol_expr(); - - code_declt declare_index(index_symexpr); - clone_body.move_to_operands(declare_index); - - code_fort copy_loop; - - copy_loop.init()= - code_assignt(index_symexpr, from_integer(0, index_symexpr.type())); - copy_loop.cond()= - binary_relation_exprt(index_symexpr, ID_lt, old_length); - - side_effect_exprt inc(ID_assign); - inc.operands().resize(2); - inc.op0()=index_symexpr; - inc.op1()=plus_exprt(index_symexpr, from_integer(1, index_symexpr.type())); - copy_loop.iter()=inc; - - dereference_exprt old_cell( - plus_exprt(old_data, index_symexpr), old_data.type().subtype()); - dereference_exprt new_cell( - plus_exprt(new_data, index_symexpr), new_data.type().subtype()); - code_assignt copy_cell(new_cell, old_cell); - copy_loop.body()=copy_cell; - - // End for-loop - clone_body.move_to_operands(copy_loop); - - member_exprt new_base_class( - new_array, base_class_component.get_name(), base_class_component.type()); - address_of_exprt retval(new_base_class); - code_returnt return_inst(retval); - clone_body.move_to_operands(return_inst); - - symbolt clone_symbol; - clone_symbol.name=clone_name; - clone_symbol.pretty_name= - id2string(symbol_type_identifier)+".clone:()"; - clone_symbol.base_name="clone"; - clone_symbol.type=clone_type; - clone_symbol.value=clone_body; - clone_symbol.mode=ID_java; - symbol_table.add(clone_symbol); - } -} - bool java_bytecode_convert_class( const java_class_loadert::parse_tree_with_overlayst &parse_trees, symbol_tablet &symbol_table, diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 330f90ef019..d85824fbdec 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1957,9 +1957,12 @@ codet java_bytecode_convert_methodt::convert_switch( mp_integer number; bool ret = to_integer(to_constant_expr(*a_it), number); DATA_INVARIANT(!ret, "case label expected to be integer"); + // The switch case does not contain any code, it just branches via a GOTO + // to the jump target of the tableswitch/lookupswitch case at + // hand. Therefore we consider this code to belong to the source bytecode + // instruction and not the target instruction. code_case.code() = code_gotot(label(integer2string(number))); - code_case.code().add_source_location() = - address_map.at(integer2unsigned(number)).source->source_location; + code_case.code().add_source_location() = location; if(a_it == args.begin()) code_case.set_default(); @@ -2096,7 +2099,7 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const( void java_bytecode_convert_methodt::convert_invoke( source_locationt location, const irep_idt &statement, - exprt &arg0, + exprt &invoke_statement, codet &c, exprt::operandst &results) { @@ -2104,20 +2107,31 @@ void java_bytecode_convert_methodt::convert_invoke( const bool is_virtual( statement == "invokevirtual" || statement == "invokeinterface"); - code_typet &code_type = to_code_type(arg0.type()); + code_typet &code_type = to_code_type(invoke_statement.type()); code_typet::parameterst ¶meters(code_type.parameters()); + const std::string full_method_name = id2string(method_id); + const size_t method_separator = id2string(method_id).rfind(':'); + const std::string method_name = full_method_name.substr(0, method_separator); + + const size_t class_separator = method_name.rfind('.'); + const std::string calling_class_name = method_name.substr(0, class_separator); + + std::string class_type_name = calling_class_name.substr(6); + std::replace(class_type_name.begin(), class_type_name.end(), '.', '/'); + const auto &enum_clone_symbol = symbol_table.lookup_ref(calling_class_name); + if(use_this) { if(parameters.empty() || !parameters[0].get_this()) { - irep_idt classname = arg0.get(ID_C_class); + irep_idt classname = invoke_statement.get(ID_C_class); typet thistype = symbol_typet(classname); // Note invokespecial is used for super-method calls as well as // constructors. if(statement == "invokespecial") { - if(is_constructor(arg0.get(ID_identifier))) + if(is_constructor(invoke_statement.get(ID_identifier))) { if(needed_lazy_methods) needed_lazy_methods->add_needed_class(classname); @@ -2180,7 +2194,9 @@ void java_bytecode_convert_methodt::convert_invoke( results[0] = promoted; } - assert(arg0.id() == ID_virtual_function); + DATA_INVARIANT( + invoke_statement.id() == ID_virtual_function, + "argument to invoke bytecode must be virtual function here"); // If we don't have a definition for the called symbol, and we won't // inherit a definition from a super-class, we create a new symbol and @@ -2198,18 +2214,19 @@ void java_bytecode_convert_methodt::convert_invoke( // generate code that may wrongly assume that such a method is // accessible if we assume that its access attribute is "more // accessible" than it actually is. - irep_idt id = arg0.get(ID_identifier); + const irep_idt &id = invoke_statement.get(ID_identifier); if( symbol_table.symbols.find(id) == symbol_table.symbols.end() && - !(is_virtual && - is_method_inherited(arg0.get(ID_C_class), arg0.get(ID_component_name)))) + !(is_virtual && is_method_inherited( + invoke_statement.get(ID_C_class), + invoke_statement.get(ID_component_name)))) { symbolt symbol; symbol.name = id; - symbol.base_name = arg0.get(ID_C_base_name); - symbol.pretty_name = id2string(arg0.get(ID_C_class)).substr(6) + "." + - id2string(symbol.base_name) + "()"; - symbol.type = arg0.type(); + symbol.base_name = invoke_statement.get(ID_C_base_name); + symbol.pretty_name = id2string(invoke_statement.get(ID_C_class)).substr(6) + + "." + id2string(symbol.base_name) + "()"; + symbol.type = invoke_statement.type(); symbol.type.set(ID_access, ID_public); symbol.value.make_nil(); symbol.mode = ID_java; @@ -2221,24 +2238,37 @@ void java_bytecode_convert_methodt::convert_invoke( symbol_table.add(symbol); } - if(is_virtual) + const bool is_enum_values_clone_call = + enum_clone_symbol.type.get_bool(ID_enumeration) && + (full_method_name == + (calling_class_name + ".values:()[L" + class_type_name + ";")); + + if(is_enum_values_clone_call) + { + const irep_idt clone_name = + "java::array[" + class_type_name + "].clone:()Ljava/lang/Object;"; + call.function() = symbol_exprt(clone_name, invoke_statement.type()); + } + else if(is_virtual) { // dynamic binding assert(use_this); assert(!call.arguments().empty()); - call.function() = arg0; + call.function() = invoke_statement; // Populate needed methods later, // once we know what object types can exist. } else { // static binding - call.function() = symbol_exprt(arg0.get(ID_identifier), arg0.type()); + call.function() = symbol_exprt( + invoke_statement.get(ID_identifier), invoke_statement.type()); if(needed_lazy_methods) { - needed_lazy_methods->add_needed_method(arg0.get(ID_identifier)); + needed_lazy_methods->add_needed_method( + invoke_statement.get(ID_identifier)); // Calling a static method causes static initialization: - needed_lazy_methods->add_needed_class(arg0.get(ID_C_class)); + needed_lazy_methods->add_needed_class(invoke_statement.get(ID_C_class)); } } @@ -2250,7 +2280,7 @@ void java_bytecode_convert_methodt::convert_invoke( if(!use_this) { - codet clinit_call = get_clinit_call(arg0.get(ID_C_class)); + codet clinit_call = get_clinit_call(invoke_statement.get(ID_C_class)); if(clinit_call.get_statement() != ID_skip) { code_blockt ret_block; diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 663eab78563..9bbf0b7c4c0 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -653,6 +653,9 @@ bool java_bytecode_languaget::typecheck( } } + // Add array type clone specializations for enumerations + add_java_enum_arrays(symbol_table); + // Now that all classes have been created in the symbol table we can populate // the class hierarchy: class_hierarchy(symbol_table); diff --git a/jbmc/src/java_bytecode/java_enum_array_clone_unwind_handler.cpp b/jbmc/src/java_bytecode/java_enum_array_clone_unwind_handler.cpp new file mode 100644 index 00000000000..277f01980c9 --- /dev/null +++ b/jbmc/src/java_bytecode/java_enum_array_clone_unwind_handler.cpp @@ -0,0 +1,65 @@ +/*******************************************************************\ + +Module: Unwind loops in array clone for enums + +Author: Diffblue + +\*******************************************************************/ + +/// \file +/// Unwind loops in array.clone for enums +#include "java_enum_array_clone_unwind_handler.h" + +#include +#include + +#include + +/// Unwind handler that specializes the clone functions of arrays of enumeration +/// classes. This forces unwinding of the copy loop in the clone method with as +/// many iterations as enum elements exist. +/// \param function_id: function the loop is in +/// \param loop_number: ordinal number of the loop (ignored) +/// \param unwind_count: iteration count that is about to begin +/// \param [out] unwind_max: may be set to an advisory (unenforced) maximum when +/// we know the total iteration count +/// \param symbol_table: global symbol table +/// \return false if loop_id belongs to an enumeration's array clone method and +/// unwind_count is <= the enumeration size, or unknown (defer / no decision) +/// otherwise. +tvt java_enum_array_clone_unwind_handler( + const irep_idt &function_id, + unsigned loop_number, + unsigned unwind_count, + unsigned &unwind_max, + const symbol_tablet &symbol_table) +{ + const std::string method_name = id2string(function_id); + const std::string java_array_prefix = "java::array["; + const size_t java_array_prefix_start = method_name.find(java_array_prefix); + const size_t java_array_prefix_end = + method_name.find("].clone:()Ljava/lang/Object;"); + if(java_array_prefix_end == std::string::npos || java_array_prefix_start != 0) + return tvt::unknown(); + + const java_enum_elements_mapt java_enum_elements = + get_java_enum_elements_map(symbol_table); + + std::string enum_name = "java::" + + method_name.substr( + java_array_prefix.size(), + java_array_prefix_end - java_array_prefix.size()); + std::replace(enum_name.begin(), enum_name.end(), '/', '.'); + const auto entry = java_enum_elements.find(enum_name); + + if(entry != java_enum_elements.end()) + { + const size_t bound = entry->second; + if(unwind_count < bound) + { + unwind_max = bound; + return tvt(false); + } + } + return tvt::unknown(); +} diff --git a/jbmc/src/java_bytecode/java_enum_array_clone_unwind_handler.h b/jbmc/src/java_bytecode/java_enum_array_clone_unwind_handler.h new file mode 100644 index 00000000000..3c8c29e2774 --- /dev/null +++ b/jbmc/src/java_bytecode/java_enum_array_clone_unwind_handler.h @@ -0,0 +1,25 @@ +/*******************************************************************\ + +Module: Unwind loops in array clone for enums + +Author: Diffblue + +\*******************************************************************/ + +/// \file +/// Unwind loops in array.clone for enums + +#ifndef CPROVER_JAVA_BYTECODE_JAVA_ENUM_ARRAY_CLONE_UNWIND_HANDLER_H +#define CPROVER_JAVA_BYTECODE_JAVA_ENUM_ARRAY_CLONE_UNWIND_HANDLER_H + +#include +#include + +tvt java_enum_array_clone_unwind_handler( + const irep_idt &function_id, + unsigned loop_number, + unsigned unwind_count, + unsigned &unwind_max, + const symbol_tablet &symbol_table); + +#endif // CPROVER_JAVA_BYTECODE_JAVA_ENUM_ARRAY_CLONE_UNWIND_HANDLER_H diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index 5d49710d02b..1ebec3d247f 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -445,3 +445,223 @@ const std::unordered_set cprover_methods_to_ignore "endThread", "getCurrentThreadID" }; + +/// Register in the \p symbol_table a new symbol type +/// java::array[X] where X is byte, float, int, char... +void add_array_type( + const char l, + symbol_tablet &symbol_table, + const optionalt enum_name) +{ + symbol_typet symbol_type = to_symbol_type(java_array_type(l).subtype()); + + const irep_idt identifier = enum_name + ? "java::array[" + *enum_name + "]" + : id2string(symbol_type.get_identifier()); + const irep_idt &symbol_type_identifier = identifier; + if(symbol_table.has_symbol(symbol_type_identifier)) + return; + + java_class_typet class_type; + // we have the base class, java.lang.Object, length and data + // of appropriate type + class_type.set_tag(symbol_type.get_identifier()); + // Note that non-array types don't have "java::" at the beginning of their + // tag, and their name is "java::" + their tag. Since arrays do have + // "java::" at the beginning of their tag we set the name to be the same as + // the tag. + class_type.set_name(symbol_type.get_identifier()); + + class_type.components().reserve(3); + class_typet::componentt base_class_component( + "@java.lang.Object", symbol_typet("java::java.lang.Object")); + base_class_component.set_pretty_name("@java.lang.Object"); + base_class_component.set_base_name("@java.lang.Object"); + class_type.components().push_back(base_class_component); + + class_typet::componentt length_component("length", java_int_type()); + length_component.set_pretty_name("length"); + length_component.set_base_name("length"); + class_type.components().push_back(length_component); + + class_typet::componentt data_component( + "data", java_reference_type(java_type_from_char(l))); + data_component.set_pretty_name("data"); + data_component.set_base_name("data"); + class_type.components().push_back(data_component); + + class_type.add_base(symbol_typet("java::java.lang.Object")); + + INVARIANT( + is_valid_java_array(class_type), + "Constructed a new type representing a Java Array " + "object that doesn't match expectations"); + + symbolt symbol; + symbol.name = symbol_type_identifier; + symbol.base_name = symbol_type.get(ID_C_base_name); + symbol.is_type = true; + symbol.type = class_type; + symbol.mode = ID_java; + symbol_table.add(symbol); + + // Also provide a clone method: + // ---------------------------- + + const irep_idt clone_name = + id2string(identifier) + ".clone:()Ljava/lang/Object;"; + code_typet::parametert this_param; + this_param.set_identifier(id2string(clone_name) + "::this"); + this_param.set_base_name("this"); + this_param.set_this(); + this_param.type() = java_reference_type(symbol_type); + const code_typet clone_type({this_param}, java_lang_object_type()); + + parameter_symbolt this_symbol; + this_symbol.name = this_param.get_identifier(); + this_symbol.base_name = this_param.get_base_name(); + this_symbol.pretty_name = this_symbol.base_name; + this_symbol.type = this_param.type(); + this_symbol.mode = ID_java; + symbol_table.add(this_symbol); + + const irep_idt local_name = id2string(clone_name) + "::cloned_array"; + auxiliary_symbolt local_symbol; + local_symbol.name = local_name; + local_symbol.base_name = "cloned_array"; + local_symbol.pretty_name = local_symbol.base_name; + local_symbol.type = java_reference_type(symbol_type); + local_symbol.mode = ID_java; + symbol_table.add(local_symbol); + const auto &local_symexpr = local_symbol.symbol_expr(); + + code_blockt clone_body; + + code_declt declare_cloned(local_symexpr); + clone_body.move(declare_cloned); + + side_effect_exprt java_new_array( + ID_java_new_array, java_reference_type(symbol_type)); + dereference_exprt old_array(this_symbol.symbol_expr(), symbol_type); + dereference_exprt new_array(local_symexpr, symbol_type); + member_exprt old_length( + old_array, length_component.get_name(), length_component.type()); + java_new_array.copy_to_operands(old_length); + code_assignt create_blank(local_symexpr, java_new_array); + clone_body.move_to_operands(create_blank); + + member_exprt old_data( + old_array, data_component.get_name(), data_component.type()); + member_exprt new_data( + new_array, data_component.get_name(), data_component.type()); + + // Begin for-loop to replace: + + const irep_idt index_name = id2string(clone_name) + "::index"; + auxiliary_symbolt index_symbol; + index_symbol.name = index_name; + index_symbol.base_name = "index"; + index_symbol.pretty_name = index_symbol.base_name; + index_symbol.type = length_component.type(); + index_symbol.mode = ID_java; + symbol_table.add(index_symbol); + const auto &index_symexpr = index_symbol.symbol_expr(); + + clone_body.add(code_declt(index_symexpr)); + + code_fort copy_loop; + + copy_loop.init() = + code_assignt(index_symexpr, from_integer(0, index_symexpr.type())); + copy_loop.cond() = binary_relation_exprt(index_symexpr, ID_lt, old_length); + + side_effect_exprt inc(ID_assign); + inc.operands().resize(2); + inc.op0() = index_symexpr; + inc.op1() = plus_exprt(index_symexpr, from_integer(1, index_symexpr.type())); + copy_loop.iter() = inc; + + const dereference_exprt old_cell( + plus_exprt(old_data, index_symexpr), old_data.type().subtype()); + const dereference_exprt new_cell( + plus_exprt(new_data, index_symexpr), new_data.type().subtype()); + const code_assignt copy_cell(new_cell, old_cell); + copy_loop.body() = copy_cell; + + // End for-loop + clone_body.move_to_operands(copy_loop); + + member_exprt new_base_class( + new_array, base_class_component.get_name(), base_class_component.type()); + const address_of_exprt retval(new_base_class); + code_returnt return_inst(retval); + clone_body.move_to_operands(return_inst); + + symbolt clone_symbol; + clone_symbol.name = clone_name; + clone_symbol.pretty_name = id2string(identifier) + ".clone:()"; + clone_symbol.base_name = "clone"; + clone_symbol.type = clone_type; + clone_symbol.value = clone_body; + clone_symbol.mode = ID_java; + symbol_table.add(clone_symbol); +} + +/// Register in the \p symbol_table a new symbol for an enum type +/// \param enum_type_name: Name of the enum type, including the "java::" prefix. +/// \param symbol_table: The symbol table the new symbol is added to. +void add_array_type_enum( + const std::string &enum_type_name, + symbol_tablet &symbol_table) +{ + std::string enum_type = enum_type_name.substr(6); + std::replace(enum_type.begin(), enum_type.end(), '.', '/'); + + add_array_type('a', symbol_table, enum_type); +} + +/// Register in the \p symbol_table new symbols for the objects +/// java::array[X] where X is byte, float, int, char... +void add_array_types(symbol_tablet &symbol_table) +{ + const std::string letters = "ijsbcfdza"; + + for(const char l : letters) + { + add_array_type(l, symbol_table, {}); + } +} + +java_enum_elements_mapt +get_java_enum_elements_map(const symbol_tablet &symbol_table) +{ + java_enum_elements_mapt enum_types; + size_t max_enum_size = 0; + for(const auto &entry : symbol_table.symbols) + { + if( + const auto java_class_type = + type_try_dynamic_cast(entry.second.type)) + { + const size_t enum_size = + java_class_type->get_size_t(ID_java_enum_static_unwind); + if(enum_size > 0) + { + if(enum_size > max_enum_size) + max_enum_size = enum_size; + enum_types[entry.first] = enum_size; + } + } + } + return enum_types; +} + +void add_java_enum_arrays(symbol_tablet &symbol_table) +{ + const java_enum_elements_mapt java_enum_elements = + get_java_enum_elements_map(symbol_table); + for(const auto &entry : java_enum_elements) + { + add_array_type_enum(id2string(entry.first), symbol_table); + } +} diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h index 1cc5c7727d4..25142a0cbeb 100644 --- a/jbmc/src/java_bytecode/java_utils.h +++ b/jbmc/src/java_bytecode/java_utils.h @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include #include @@ -110,6 +111,16 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component( bool is_non_null_library_global(const irep_idt &); +void add_array_types(symbol_tablet &symbol_table); +void add_array_type_enum( + const std::string &enum_type_name, + symbol_tablet &symbol_table); + +typedef std::unordered_map java_enum_elements_mapt; +java_enum_elements_mapt +get_java_enum_elements_map(const symbol_tablet &symbol_table); +void add_java_enum_arrays(symbol_tablet &symbol_table); + extern const std::unordered_set cprover_methods_to_ignore; #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 100d28b660f..5a7082e2c93 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -54,6 +54,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -491,6 +492,16 @@ int jbmc_parse_optionst::doit() max_unwind, symbol_table); }); + // unwind Enum.values() loop to correctly enable enum array cloning + bmc.add_loop_unwind_handler( + [&symbol_table]( + const irep_idt &function_id, + unsigned loop_num, + unsigned unwind_count, + unsigned &max_unwind) { + return java_enum_array_clone_unwind_handler( + function_id, loop_num, unwind_count, max_unwind, symbol_table); + }); }; } diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index 8a1941af60f..b53af16a95f 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -894,52 +895,38 @@ void interpretert::evaluate( mp_integer address=evaluate_address( expr, true); // fail quietly - if(address.is_zero() && expr.id()==ID_index) + if(address.is_zero()) { - // Try reading from a constant array: - mp_vectort idx; - evaluate(expr.op1(), idx); - if(idx.size()==1) + exprt simplified; + // In case of being an indexed access, try to evaluate the index, then + // simplify. + if(expr.id() == ID_index) { - mp_integer read_from_index=idx[0]; - if(expr.op0().id()==ID_array) + exprt evaluated_index = expr; + mp_vectort idx; + evaluate(expr.op1(), idx); + if(idx.size() == 1) { - const auto &ops=expr.op0().operands(); - DATA_INVARIANT(read_from_index.is_long(), "index is too large"); - if(read_from_index>=0 && read_from_index