From 2a22a2e61c18348049b6e21e7e5c2b6582ae2554 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 22 Nov 2017 15:25:51 +0000 Subject: [PATCH 1/4] Fix allocation of infinite char arrays Infinite char arrays used in string need to be dynamically allocated instead of being on the stack as it used to be. --- src/java_bytecode/java_object_factory.cpp | 53 +++++++++++++++---- .../java_string_library_preprocess.cpp | 1 + 2 files changed, 45 insertions(+), 9 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 5c05b26c295..18fe7238fba 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -511,6 +511,19 @@ 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); + alloc.copy_to_operands(size); + alloc.copy_to_operands(false_exprt()); + alloc.type() = lhs.type(); + return code_assignt(lhs, alloc); +} + /// Initialize a nondeterministic String structure /// \param obj: struct to initialize, must have been declared using /// code of the form: @@ -527,15 +540,19 @@ static mp_integer max_value(const typet &type) /// tmp_object_factory$1 = NONDET(int); /// __CPROVER_assume(tmp_object_factory$1 >= 0); /// __CPROVER_assume(tmp_object_factory$1 <= max_nondet_string_length); +/// char (*string_data_pointer)[INFINITY()]; +/// string_data_pointer = ALLOCATE(char [INFINITY()], INFINITY(), false); /// char nondet_infinite_array$2[INFINITY()]; /// nondet_infinite_array$2 = NONDET(char [INFINITY()]); -/// cprover_associate_array_to_pointer_func -/// (nondet_infinite_array$2, &nondet_infinite_array$2[0]); -/// prover_associate_length_to_array_func -/// (nondet_infinite_array$2, tmp_object_factory$1); -/// arg = { .\@java.lang.Object={ .\@class_identifier="java.lang.String", -/// .\@lock=false }, .length=tmp_object_factory$1, -/// .data=nondet_infinite_array$2 }; +/// *string_data_pointer = nondet_infinite_array$2; +/// cprover_associate_array_to_pointer_func( +/// *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\", .@lock=false }, +/// .length=tmp_object_factory, +/// .data=*string_data_pointer }; /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ /// Unit tests in `unit/java_bytecode/java_object_factory/` ensure /// it is the case. @@ -570,6 +587,7 @@ codet initialize_nondet_string_struct( // 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 = new_tmp_symbol(symbol_table, loc, java_int_type()); @@ -593,14 +611,29 @@ codet initialize_nondet_string_struct( 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 - exprt data_expr = make_nondet_infinite_char_array(symbol_table, loc, code); + const dereference_exprt data_expr(data_pointer); + const exprt nondet_array = + make_nondet_infinite_char_array(symbol_table, loc, code); + code.add(code_assignt(data_expr, nondet_array)); struct_expr.copy_to_operands(length_expr); const address_of_exprt array_pointer( index_exprt(data_expr, from_integer(0, java_int_type()))); - struct_expr.copy_to_operands(array_pointer); add_pointer_to_array_association( array_pointer, data_expr, symbol_table, loc, code); @@ -608,6 +641,8 @@ codet initialize_nondet_string_struct( add_array_to_length_association( data_expr, length_expr, symbol_table, loc, code); + struct_expr.copy_to_operands(array_pointer); + // Printable ASCII characters are between ' ' and '~'. if(printable) { diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 6c040a5a759..2c6df028b9d 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -519,6 +519,7 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr( symbol_table_baset &symbol_table, code_blockt &code) { + /// \todo refactor with initialize_nonddet_string_struct const refined_string_exprt str = decl_string_expr(loc, symbol_table, code); side_effect_expr_nondett nondet_length(str.length().type()); From 2e760b35e1edfaddb0be1208c51daa743eb4c0d1 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 23 Nov 2017 07:29:18 +0000 Subject: [PATCH 2/4] Add invariant on array to pointer association In the string solver each char array should be associated to a pointer which is unique for each array. This invariant ensures we don't make mistake there. --- src/solvers/refinement/string_constraint_generator_main.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 97b034e78a0..c73e450fdbd 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -270,7 +270,10 @@ exprt string_constraint_generatort::associate_array_to_pointer( /// \todo We should use a function for inserting the correspondance /// between array and pointers. - arrays_of_pointers_.insert(std::make_pair(pointer_expr, array_expr)); + const auto it_bool = + arrays_of_pointers_.insert(std::make_pair(pointer_expr, array_expr)); + INVARIANT( + it_bool.second, "should not associate two arrays to the same pointer"); add_default_axioms(to_array_string_expr(array_expr)); return from_integer(0, f.type()); } From 89c123e1359998123c95e9ff36ec7e943fbaf4f3 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 23 Nov 2017 08:00:22 +0000 Subject: [PATCH 3/4] Adapt unit test for allocation of string data --- .../java_object_factory/gen_nondet_string_init.cpp | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp index b410805e488..6ae8472ff44 100644 --- a/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp +++ b/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp @@ -70,18 +70,22 @@ SCENARIO( "tmp_object_factory = NONDET(int);", "__CPROVER_assume(tmp_object_factory >= 0);", "__CPROVER_assume(tmp_object_factory <= 20);", + "char (*string_data_pointer)[INFINITY()];", + "string_data_pointer = " + "ALLOCATE(char [INFINITY()], INFINITY(), false);", "char nondet_infinite_array[INFINITY()];", "nondet_infinite_array = NONDET(char [INFINITY()]);", + "*string_data_pointer = nondet_infinite_array;", "int return_array;", "return_array = cprover_associate_array_to_pointer_func" - "(nondet_infinite_array, nondet_infinite_array);", + "(*string_data_pointer, *string_data_pointer);", "int return_array;", "return_array = cprover_associate_length_to_array_func" - "(nondet_infinite_array, tmp_object_factory);", + "(*string_data_pointer, tmp_object_factory);", "arg = { .@java.lang.Object={ .@class_identifier" - "=\"java::java.lang.String\", .@lock=false }," - " .length=tmp_object_factory, " - ".data=nondet_infinite_array };"}; + "=\"java::java.lang.String\", .@lock=false }," + " .length=tmp_object_factory, " + ".data=*string_data_pointer };"}; for(std::size_t i = 0; i < code_string.size() && i < reference_code.size(); From ea0c70ac2493de857763c8910dbf785285ff0cc2 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 23 Nov 2017 11:53:07 +0000 Subject: [PATCH 4/4] Remove redundant pointer to array association This redundant step which is already done in process_parameters, was detected in string constraint generation as an attempt to access two array to the same pointers. Although the array are in fact the same here, the second call to add_pointer_to_array_association is unecessary. --- src/java_bytecode/java_string_library_preprocess.cpp | 8 -------- 1 file changed, 8 deletions(-) diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 2c6df028b9d..452c59e0ddb 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -1696,14 +1696,6 @@ codet java_string_library_preprocesst::make_init_from_array_code( /// \todo this assumes the array to be constant between all calls to /// string primitives, which may not be true in general. refined_string_exprt string_arg = to_string_expr(args[1]); - add_pointer_to_array_association( - string_arg.content(), - dereference_exprt( - string_arg.content(), - array_typet(java_char_type(), infinity_exprt(java_int_type()))), - symbol_table, - loc, - code); // The third argument is `count`, whereas the third argument of substring // is `end` which corresponds to `offset+count`