diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 852d5bf1eb4..44b9af5935d 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -526,18 +526,6 @@ static mp_integer max_value(const typet &type) UNREACHABLE; } -/// Create code allocating object of size `size` and assigning it to `lhs` -/// \param lhs : pointer which will be allocated -/// \param size : size of the object -/// \return code allocation object and assigning `lhs` -static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size) -{ - side_effect_exprt alloc(ID_allocate, lhs.type(), lhs.source_location()); - alloc.copy_to_operands(size); - alloc.copy_to_operands(false_exprt()); - return code_assignt(lhs, alloc); -} - /// 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 @@ -648,25 +636,8 @@ bool initialize_nondet_string_fields( 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()))); - - 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()))); - - // `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 = + const exprt data_expr = make_nondet_infinite_char_array(symbol_table, loc, function_id, code); - code.add(code_assignt(data_expr, nondet_array)); - struct_expr.operands()[struct_type.component_number("length")] = length_expr; const address_of_exprt array_pointer( diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 41f25256320..aa22e28d1de 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -617,6 +617,18 @@ codet java_string_library_preprocesst::code_return_function_application( return code_returnt(fun_app); } +/// Create code allocating object of size `size` and assigning it to `lhs` +/// \param lhs : pointer which will be allocated +/// \param size : size of the object +/// \return code allocation object and assigning `lhs` +static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size) +{ + side_effect_exprt alloc(ID_allocate, lhs.type(), lhs.source_location()); + alloc.add_to_operands(size); + alloc.add_to_operands(false_exprt()); + return code_assignt(lhs, alloc); +} + /// Declare a fresh symbol of type array of character with infinite size. /// \param symbol_table: the symbol table /// \param loc: source location @@ -632,17 +644,20 @@ exprt make_nondet_infinite_char_array( const array_typet array_type( java_char_type(), infinity_exprt(java_int_type())); const symbolt data_sym = get_fresh_aux_symbol( - array_type, + pointer_type(array_type), id2string(function_id), - "nondet_infinite_array", + "nondet_infinite_array_pointer", loc, ID_java, symbol_table); - const symbol_exprt data_expr = data_sym.symbol_expr(); - code.add(code_declt(data_expr), loc); - const side_effect_expr_nondett nondet_data(data_expr.type(), loc); - code.add(code_assignt(data_expr, nondet_data), loc); - return data_expr; + + const symbol_exprt data_pointer = data_sym.symbol_expr(); + code.add(code_declt(data_pointer)); + code.add(make_allocate_code(data_pointer, array_type.size())); + const exprt nondet_data = side_effect_expr_nondett(array_type, loc); + const exprt data = dereference_exprt(data_pointer, array_type); + code.add(code_assignt(data, nondet_data), loc); + return data; } /// Add a call to a primitive of the string solver, letting it know that 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 67d26161375..d224e36c65b 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 @@ -84,22 +84,20 @@ SCENARIO( "tmp_object_factory = NONDET(int);", CPROVER_PREFIX "assume(tmp_object_factory >= 0);", CPROVER_PREFIX "assume(tmp_object_factory <= 20);", - "char (*string_data_pointer)[INFINITY()];", - "string_data_pointer = " + "char (*nondet_infinite_array_pointer)[INFINITY()];", + "nondet_infinite_array_pointer = " "ALLOCATE(char [INFINITY()], INFINITY(), false);", - "char nondet_infinite_array[INFINITY()];", - "nondet_infinite_array = NONDET(char [INFINITY()]);", - "*string_data_pointer = nondet_infinite_array;", + "*nondet_infinite_array_pointer = NONDET(char [INFINITY()]);", "int return_array;", "return_array = cprover_associate_array_to_pointer_func" - "(*string_data_pointer, *string_data_pointer);", + "(*nondet_infinite_array_pointer, *nondet_infinite_array_pointer);", "int return_array;", "return_array = cprover_associate_length_to_array_func" - "(*string_data_pointer, tmp_object_factory);", + "(*nondet_infinite_array_pointer, tmp_object_factory);", "arg = { .@java.lang.Object={ .@class_identifier" "=\"java::java.lang.String\" }," " .length=tmp_object_factory, " - ".data=*string_data_pointer };"}; + ".data=*nondet_infinite_array_pointer };"}; // clang-format on for(std::size_t i = 0;