diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/Test.class b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/Test.class new file mode 100644 index 00000000000..ced41ac19a3 Binary files /dev/null and b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/Test.class differ diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/Test.java b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/Test.java new file mode 100644 index 00000000000..36bef70d308 --- /dev/null +++ b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/Test.java @@ -0,0 +1,7 @@ +public class Test { + + public static void testme(StringBuilder builder, StringBuffer buffer) { + + } + +} diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/AbstractStringBuilder.class b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/AbstractStringBuilder.class new file mode 100644 index 00000000000..63f44f994ce Binary files /dev/null and b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/AbstractStringBuilder.class differ diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/AbstractStringBuilder.java b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/AbstractStringBuilder.java new file mode 100644 index 00000000000..13b25b4c809 --- /dev/null +++ b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/AbstractStringBuilder.java @@ -0,0 +1,5 @@ +package java.lang; + +public class AbstractStringBuilder implements CharSequence { + +} diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/CharSequence.class b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/CharSequence.class new file mode 100644 index 00000000000..9b3497435fd Binary files /dev/null and b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/CharSequence.class differ diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/CharSequence.java b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/CharSequence.java new file mode 100644 index 00000000000..d5a060634aa --- /dev/null +++ b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/CharSequence.java @@ -0,0 +1,5 @@ +package java.lang; + +interface CharSequence { + +} diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/String.class b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/String.class new file mode 100644 index 00000000000..d6945bd07a2 Binary files /dev/null and b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/String.class differ diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/String.java b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/String.java new file mode 100644 index 00000000000..e9d95981d63 --- /dev/null +++ b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/String.java @@ -0,0 +1,5 @@ +package java.lang; + +public class String implements CharSequence { + +} diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuffer.class b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuffer.class new file mode 100644 index 00000000000..1c6cddabe11 Binary files /dev/null and b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuffer.class differ diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuffer.java b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuffer.java new file mode 100644 index 00000000000..5031f40a7c7 --- /dev/null +++ b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuffer.java @@ -0,0 +1,5 @@ +package java.lang; + +public class StringBuffer extends AbstractStringBuilder { + +} diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuilder.class b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuilder.class new file mode 100644 index 00000000000..9830cfebf49 Binary files /dev/null and b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuilder.class differ diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuilder.java b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuilder.java new file mode 100644 index 00000000000..0fd6a6f0160 --- /dev/null +++ b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuilder.java @@ -0,0 +1,5 @@ +package java.lang; + +public class StringBuilder extends AbstractStringBuilder { + +} diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/test.desc b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/test.desc new file mode 100644 index 00000000000..4d82786d6ef --- /dev/null +++ b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/test.desc @@ -0,0 +1,12 @@ +CORE +Test.class +--function Test.testme +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +type mismatch +-- +Before cbmc#2472 this would assume that StringBuilder's direct parent was +java.lang.Object, causing a type mismatch when --refine-strings was not in use +(which at the time would assume that parent-child relationship) diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/Test.class b/jbmc/regression/jbmc-strings/StringModelsWithFields/Test.class new file mode 100644 index 00000000000..ecc310248ef Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringModelsWithFields/Test.class differ diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/Test.java b/jbmc/regression/jbmc-strings/StringModelsWithFields/Test.java new file mode 100644 index 00000000000..7bb9f7676ef --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringModelsWithFields/Test.java @@ -0,0 +1,36 @@ +public class Test { + + public static void testme(StringBuilder builder, StringBuffer buffer, String str) { + + // In this test the versions of String, StringBuilder and + // StringBuffer.class supplied have fields beyond the expected situation + // of either no fields at all (without --refine-strings) or only 'length' + // and 'data' (with --refine-strings). We check they have been nondet- + // initialized as expected by making sure we can reach the final + // 'assert false'. + + if(str != null && + builder != null && + buffer != null && + str.a != null && + builder.i != null && + buffer.i != null && + str.a.x >= 5 && + str.a.y <= -10.0f && + builder.d >= 100.0 && + buffer.b == true) { + + assert builder instanceof StringBuilder; + assert buffer instanceof StringBuffer; + assert str instanceof String; + + assert str.a instanceof A; + assert builder.i instanceof Integer; + assert buffer.i instanceof Integer; + + assert false; + } + + } + +} diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/A.class b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/A.class new file mode 100644 index 00000000000..f620ab4db78 Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/A.class differ diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/A.java b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/A.java new file mode 100644 index 00000000000..7a001f56696 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/A.java @@ -0,0 +1,8 @@ +package java.lang; + +public class A { + + public int x; + public float y; + +} diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/AbstractStringBuilder.class b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/AbstractStringBuilder.class new file mode 100644 index 00000000000..aecd1092a9a Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/AbstractStringBuilder.class differ diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/AbstractStringBuilder.java b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/AbstractStringBuilder.java new file mode 100644 index 00000000000..995fd2ac018 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/AbstractStringBuilder.java @@ -0,0 +1,7 @@ +package java.lang; + +public class AbstractStringBuilder implements CharSequence { + + public Integer i; + +} diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/CharSequence.class b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/CharSequence.class new file mode 100644 index 00000000000..9b3497435fd Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/CharSequence.class differ diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/CharSequence.java b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/CharSequence.java new file mode 100644 index 00000000000..d5a060634aa --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/CharSequence.java @@ -0,0 +1,5 @@ +package java.lang; + +interface CharSequence { + +} diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/String.class b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/String.class new file mode 100644 index 00000000000..0bde10b655f Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/String.class differ diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/String.java b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/String.java new file mode 100644 index 00000000000..5f9cd4b405c --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/String.java @@ -0,0 +1,7 @@ +package java.lang; + +public class String implements CharSequence { + + public A a; + +} diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuffer.class b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuffer.class new file mode 100644 index 00000000000..7d574b934be Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuffer.class differ diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuffer.java b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuffer.java new file mode 100644 index 00000000000..703812fe942 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuffer.java @@ -0,0 +1,7 @@ +package java.lang; + +public class StringBuffer extends AbstractStringBuilder { + + public boolean b; + +} diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuilder.class b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuilder.class new file mode 100644 index 00000000000..616af091291 Binary files /dev/null and b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuilder.class differ diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuilder.java b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuilder.java new file mode 100644 index 00000000000..b9cc96a321b --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuilder.java @@ -0,0 +1,7 @@ +package java.lang; + +public class StringBuilder extends AbstractStringBuilder { + + public double d; + +} diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/test.desc b/jbmc/regression/jbmc-strings/StringModelsWithFields/test.desc new file mode 100644 index 00000000000..caba6e8ac88 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringModelsWithFields/test.desc @@ -0,0 +1,14 @@ +CORE +Test.class +--function Test.testme +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 23 .* SUCCESS +assertion at file Test.java line 24 .* SUCCESS +assertion at file Test.java line 25 .* SUCCESS +assertion at file Test.java line 27 .* SUCCESS +assertion at file Test.java line 28 .* SUCCESS +assertion at file Test.java line 29 .* SUCCESS +assertion at file Test.java line 31 .* FAILURE +-- +type mismatch diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index bba09f713f9..565a4b59f97 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -510,17 +510,22 @@ static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size) return code_assignt(lhs, alloc); } -/// Initialize a nondeterministic String structure -/// \param obj: struct to initialize, must have been declared using -/// code of the form: -/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -/// struct java.lang.String { struct \@java.lang.Object; -/// int length; char *data; } tmp_object_factory$1; -/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// Check if a structure is a nondeterministic String structure, and if it is +/// initialize its length and data fields. +/// \param struct_expr [out]: struct that we may initialize +/// \param code: block to add pre-requisite declarations (e.g. to allocate a +/// data array) /// \param max_nondet_string_length: maximum length of strings to initialize /// \param loc: location in the source +/// \param function_id: function ID to associate with auxiliary variables /// \param symbol_table: the symbol table -/// \return code for initialization of the strings +/// \param printable: if true, the nondet string must consist of printable +/// characters only +/// \return true if struct_expr's length and data fields have been set up, +/// false if we took no action because struct_expr wasn't a CharSequence +/// or didn't have the necessary fields. +/// +/// The code produced is of the form: /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ /// int tmp_object_factory$1; /// tmp_object_factory$1 = NONDET(int); @@ -535,169 +540,125 @@ static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size) /// *string_data_pointer, *string_data_pointer); /// cprover_associate_length_to_array_func( /// *string_data_pointer, tmp_object_factory); -/// arg = { .@java.lang.Object={ -/// .@class_identifier=\"java::java.lang.String\" }, +/// +/// struct_expr is then adjusted to set /// .length=tmp_object_factory, -/// .data=*string_data_pointer }; +/// .data=*string_data_pointer /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ /// Unit tests in `unit/java_bytecode/java_object_factory/` ensure /// it is the case. -codet initialize_nondet_string_struct( - const exprt &obj, +bool initialize_nondet_string_fields( + struct_exprt &struct_expr, + code_blockt &code, const std::size_t &max_nondet_string_length, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, bool printable) { - PRECONDITION( - java_string_library_preprocesst::implements_java_char_sequence(obj.type())); + if(!java_string_library_preprocesst::implements_java_char_sequence( + struct_expr.type())) + { + return false; + } - const namespacet ns(symbol_table); - code_blockt code; + namespacet ns(symbol_table); + + const struct_typet &struct_type = + to_struct_type(ns.follow(struct_expr.type())); + + // In case the type for String was not added to the symbol table, + // (typically when string refinement is not activated), `struct_type` + // just contains the standard Object fields (or may have some other model + // entirely), and in particular has no length and data fields. + if(!struct_type.has_component("length") || !struct_type.has_component("data")) + return false; - // `obj` is `*expr` - const struct_typet &struct_type = to_struct_type(ns.follow(obj.type())); - // @clsid = java::java.lang.String or similar. // We allow type StringBuffer and StringBuilder to be initialized // in the same way has String, because they have the same structure and // are treated in the same way by CBMC. + // Note that CharSequence cannot be used as classid because it's abstract, // so it is replaced by String. // \todo allow StringBuffer and StringBuilder as classid for Charsequence - const irep_idt &class_id = - struct_type.get_tag() == "java.lang.CharSequence" - ? "java::java.lang.String" - : "java::" + id2string(struct_type.get_tag()); + if(struct_type.get_tag() == "java.lang.CharSequence") + { + set_class_identifier( + struct_expr, ns, symbol_typet("java::java.lang.String")); + } - const symbol_typet jlo_symbol("java::java.lang.Object"); - const struct_typet &jlo_type = to_struct_type(ns.follow(jlo_symbol)); - struct_exprt jlo_init(jlo_symbol); - java_root_class_init(jlo_init, jlo_type, class_id); + // OK, this is a String type with the expected fields -- add code to `code` + // to set up pre-requisite variables and assign them in `struct_expr`. - struct_exprt struct_expr(obj.type()); - struct_expr.copy_to_operands(jlo_init); + /// \todo Refactor with make_nondet_string_expr + // length_expr = nondet(int); + const symbolt length_sym = get_fresh_aux_symbol( + java_int_type(), + id2string(function_id), + "tmp_object_factory", + loc, + ID_java, + symbol_table); + const symbol_exprt length_expr = length_sym.symbol_expr(); + const side_effect_expr_nondett nondet_length(length_expr.type()); + code.add(code_declt(length_expr)); + code.add(code_assignt(length_expr, nondet_length)); - // In case the type for string was not added to the symbol table, - // (typically when string refinement is not activated), `struct_type` - // just contains the standard Object field and no length and data fields. - if(struct_type.has_component("length")) - { - /// \todo Refactor with make_nondet_string_expr - // length_expr = nondet(int); - const symbolt length_sym = get_fresh_aux_symbol( - java_int_type(), - id2string(function_id), - "tmp_object_factory", - loc, - ID_java, - symbol_table); - const symbol_exprt length_expr = length_sym.symbol_expr(); - const side_effect_expr_nondett nondet_length(length_expr.type()); - code.add(code_declt(length_expr)); - code.add(code_assignt(length_expr, nondet_length)); + // assume (length_expr >= 0); + code.add( + code_assumet( + binary_relation_exprt( + length_expr, ID_ge, from_integer(0, java_int_type())))); - // assume (length_expr >= 0); + // assume (length_expr <= max_input_length) + if(max_nondet_string_length <= max_value(length_expr.type())) + { + exprt max_length = + from_integer(max_nondet_string_length, length_expr.type()); code.add( - code_assumet( - binary_relation_exprt( - length_expr, ID_ge, from_integer(0, java_int_type())))); - - // assume (length_expr <= max_input_length) - if(max_nondet_string_length <= max_value(length_expr.type())) - { - exprt max_length = - from_integer(max_nondet_string_length, length_expr.type()); - code.add( - code_assumet(binary_relation_exprt(length_expr, ID_le, max_length))); - } + code_assumet(binary_relation_exprt(length_expr, ID_le, max_length))); + } - // char (*array_data_init)[INFINITY]; - const typet data_ptr_type = pointer_type( - array_typet(java_char_type(), infinity_exprt(java_int_type()))); + // char (*array_data_init)[INFINITY]; + const typet data_ptr_type = pointer_type( + array_typet(java_char_type(), infinity_exprt(java_int_type()))); - symbolt &data_pointer_sym = get_fresh_aux_symbol( - data_ptr_type, "", "string_data_pointer", loc, ID_java, symbol_table); - const auto data_pointer = data_pointer_sym.symbol_expr(); - code.add(code_declt(data_pointer)); + symbolt &data_pointer_sym = get_fresh_aux_symbol( + data_ptr_type, "", "string_data_pointer", loc, ID_java, symbol_table); + const auto data_pointer = data_pointer_sym.symbol_expr(); + code.add(code_declt(data_pointer)); - // Dynamic allocation: `data array = allocate char[INFINITY]` - code.add(make_allocate_code(data_pointer, infinity_exprt(java_int_type()))); + // Dynamic allocation: `data array = allocate char[INFINITY]` + code.add(make_allocate_code(data_pointer, infinity_exprt(java_int_type()))); - // `data_expr` is `*data_pointer` - // data_expr = nondet(char[INFINITY]) // we use infinity for variable size - const dereference_exprt data_expr(data_pointer); - const exprt nondet_array = - make_nondet_infinite_char_array(symbol_table, loc, function_id, code); - code.add(code_assignt(data_expr, nondet_array)); + // `data_expr` is `*data_pointer` + // data_expr = nondet(char[INFINITY]) // we use infinity for variable size + const dereference_exprt data_expr(data_pointer); + const exprt nondet_array = + make_nondet_infinite_char_array(symbol_table, loc, function_id, code); + code.add(code_assignt(data_expr, nondet_array)); - struct_expr.copy_to_operands(length_expr); + struct_expr.operands()[struct_type.component_number("length")] = length_expr; - const address_of_exprt array_pointer( - index_exprt(data_expr, from_integer(0, java_int_type()))); + const address_of_exprt array_pointer( + index_exprt(data_expr, from_integer(0, java_int_type()))); - add_pointer_to_array_association( - array_pointer, data_expr, symbol_table, loc, code); + add_pointer_to_array_association( + array_pointer, data_expr, symbol_table, loc, code); - add_array_to_length_association( - data_expr, length_expr, symbol_table, loc, code); + add_array_to_length_association( + data_expr, length_expr, symbol_table, loc, code); - struct_expr.copy_to_operands(array_pointer); + struct_expr.operands()[struct_type.component_number("data")] = array_pointer; - // Printable ASCII characters are between ' ' and '~'. - if(printable) - { - add_character_set_constraint( - array_pointer, length_expr, " -~", symbol_table, loc, code); - } + // Printable ASCII characters are between ' ' and '~'. + if(printable) + { + add_character_set_constraint( + array_pointer, length_expr, " -~", symbol_table, loc, code); } - // tmp_object = struct_expr; - code.add(code_assignt(obj, struct_expr)); - return code; -} - -/// Add code for the initialization of a string using a nondeterministic -/// content and association of its address to the pointer `expr`. -/// \param expr: pointer to be affected -/// \param max_nondet_string_length: maximum length of strings to initialize -/// \param printable: Boolean, true to force content to be printable -/// \param symbol_table: the symbol table -/// \param loc: location in the source -/// \param [out] code: code block in which initialization code is added -/// \return false if code was added, true to signal an error when the given -/// object does not implement CharSequence or does not have data and -/// length fields, in which case it should be initialized another way. -static bool add_nondet_string_pointer_initialization( - const exprt &expr, - const std::size_t &max_nondet_string_length, - bool printable, - symbol_table_baset &symbol_table, - const source_locationt &loc, - const irep_idt &function_id, - code_blockt &code) -{ - const namespacet ns(symbol_table); - const dereference_exprt obj(expr, expr.type().subtype()); - const struct_typet &struct_type = - to_struct_type(ns.follow(to_symbol_type(obj.type()))); - - // if no String model is loaded then we cannot construct a String object - if(struct_type.get_bool(ID_incomplete_class)) - return true; - - const exprt malloc_site = allocate_dynamic_object_with_decl( - expr, symbol_table, loc, function_id, code); - - code.add( - initialize_nondet_string_struct( - dereference_exprt(malloc_site, struct_type), - max_nondet_string_length, - loc, - function_id, - symbol_table, - printable)); - return false; + return true; } /// Initializes a pointer \p expr of type \p pointer_type to a primitive-typed @@ -831,35 +792,13 @@ void java_object_factoryt::gen_nondet_pointer_init( // and asign to `expr` the address of such object code_blockt non_null_inst; - // Note string-type-specific initialization might fail, e.g. if java.lang.CharSequence does not - // have the expected fields (typically this happens if --refine-strings was not passed). In this - // case we fall back to normal pointer target init. - bool string_init_succeeded = false; - - if(java_string_library_preprocesst::implements_java_char_sequence_pointer( - expr.type())) - { - string_init_succeeded = - !add_nondet_string_pointer_initialization( - expr, - object_factory_parameters.max_nondet_string_length, - object_factory_parameters.string_printable, - symbol_table, - loc, - object_factory_parameters.function_id, - assignments); - } - - if(!string_init_succeeded) - { - gen_pointer_target_init( - non_null_inst, - expr, - subtype, - alloc_type, - depth, - update_in_placet::NO_UPDATE_IN_PLACE); - } + gen_pointer_target_init( + non_null_inst, + expr, + subtype, + alloc_type, + depth, + update_in_placet::NO_UPDATE_IN_PLACE); auto set_null_inst=get_null_assignment(expr, pointer_type); @@ -1030,6 +969,8 @@ void java_object_factoryt::gen_nondet_struct_init( // case they will set `skip_classid` // * Not if we're re-initializing an existing object (i.e. update_in_place) + bool skip_special_string_fields = false; + if(!is_sub && !skip_classid && update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE) @@ -1042,15 +983,28 @@ void java_object_factoryt::gen_nondet_struct_init( // This code mirrors the `remove_java_new` pass: null_message_handlert nullout; - exprt zero_object= + exprt initial_object = zero_initializer( struct_type, source_locationt(), ns, nullout); irep_idt qualified_clsid = "java::" + id2string(class_identifier); set_class_identifier( - to_struct_expr(zero_object), ns, symbol_typet(qualified_clsid)); + to_struct_expr(initial_object), ns, symbol_typet(qualified_clsid)); + + // If the initialised type is a special-cased String type (one with length + // and data fields introduced by string-library preprocessing), initialise + // those fields with nondet values: + skip_special_string_fields = + initialize_nondet_string_fields( + to_struct_expr(initial_object), + assignments, + object_factory_parameters.max_nondet_string_length, + loc, + object_factory_parameters.function_id, + symbol_table, + object_factory_parameters.string_printable); assignments.copy_to_operands( - code_assignt(expr, zero_object)); + code_assignt(expr, initial_object)); } for(const auto &component : components) @@ -1076,6 +1030,12 @@ void java_object_factoryt::gen_nondet_struct_init( code.add_source_location() = loc; assignments.copy_to_operands(code); } + else if(skip_special_string_fields && (name == "length" || name == "data")) + { + // In this case these were set up by initialise_nondet_string_fields + // above. + continue; + } else { INVARIANT(!name.empty(), "Each component of a struct must have a name"); diff --git a/jbmc/src/java_bytecode/java_object_factory.h b/jbmc/src/java_bytecode/java_object_factory.h index a1ce6bb51d6..d174d4e4ae2 100644 --- a/jbmc/src/java_bytecode/java_object_factory.h +++ b/jbmc/src/java_bytecode/java_object_factory.h @@ -150,12 +150,4 @@ exprt allocate_dynamic_object_with_decl( const irep_idt &function_id, code_blockt &output_code); -codet initialize_nondet_string_struct( - const exprt &obj, - const std::size_t &max_nondet_string_length, - const source_locationt &loc, - const irep_idt &function_id, - symbol_table_baset &symbol_table, - bool printable); - #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H diff --git a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp index 032348e8ed6..53cc0e7f5ef 100644 --- a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp +++ b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp @@ -46,10 +46,22 @@ SCENARIO( symbol_typet java_string_type("java::java.lang.String"); symbol_exprt expr("arg", java_string_type); + object_factory_parameterst object_factory_parameters; + object_factory_parameters.max_nondet_string_length = 20; + object_factory_parameters.function_id = "test"; + WHEN("Initialisation code for a string is generated") { - const codet code = initialize_nondet_string_struct( - expr, 20, loc, "test", symbol_table, false); + code_blockt code; + gen_nondet_init( + expr, + code, + symbol_table, + loc, + false, + allocation_typet::DYNAMIC, + object_factory_parameters, + update_in_placet::NO_UPDATE_IN_PLACE); THEN("Code is produced") {