From c61d0951a32c5fa09d7452b83529a6c96535004f Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 26 May 2017 18:03:12 +0100 Subject: [PATCH] Improve constructor and copy of strings We now assign strings in one step instead of field by field. This makes constant propagation work better in later step of the analysis. This is necessary for the implementation of String.replace(). --- .../java_string_library_preprocess.cpp | 284 +++++++++++++++--- .../java_string_library_preprocess.h | 16 + 2 files changed, 252 insertions(+), 48 deletions(-) diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 199d472ea0e..067812974e0 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -1013,41 +1013,80 @@ string_exprt java_string_library_preprocesst:: /*******************************************************************\ Function: java_string_library_preprocesst:: - code_assign_string_expr_to_java_string + code_assign_components_to_java_string Inputs: - lhs - an expression representing a java string - rhs - a string expression + lhs - expression representing the java string to assign to + rhs_array - pointer to the array to assign + rhs_length - length of the array to assign symbol_table - symbol table Output: return the following code: - > lhs->length=rhs.length - > lhs->data=&rhs.data + > lhs = { {Object}, length=rhs_length, data=rhs_array } + + Purpose: Produce code for an assignemnrt of a string expr to a + Java string, component-wise. \*******************************************************************/ -codet java_string_library_preprocesst::code_assign_string_expr_to_java_string( +codet java_string_library_preprocesst::code_assign_components_to_java_string( const exprt &lhs, - const string_exprt &rhs, + const exprt &rhs_array, + const exprt &rhs_length, symbol_tablet &symbol_table) { assert(implements_java_char_sequence(lhs.type())); dereference_exprt deref(lhs, lhs.type().subtype()); - // Fields of the string object - exprt lhs_length=get_length(deref, symbol_table); - exprt lhs_data=get_data(deref, symbol_table); - - // Assignments code_blockt code; - code.add(code_assignt(lhs_length, rhs.length())); - code.add( - code_assignt(lhs_data, address_of_exprt(rhs.content()))); + + // A String has a field Object with @clsid = String and @lock = false: + const symbolt &jlo_symbol=symbol_table.lookup("java::java.lang.Object"); + const struct_typet &jlo_struct=to_struct_type(jlo_symbol.type); + struct_exprt jlo_init(jlo_struct); + jlo_init.copy_to_operands(constant_exprt( + "java::java.lang.String", jlo_struct.components()[0].type())); + jlo_init.copy_to_operands(from_integer(0, jlo_struct.components()[1].type())); + + struct_exprt struct_rhs(deref.type()); + struct_rhs.copy_to_operands(jlo_init); + struct_rhs.copy_to_operands(rhs_length); + struct_rhs.copy_to_operands(rhs_array); + code.add(code_assignt( + dereference_exprt(lhs, lhs.type().subtype()), struct_rhs)); + return code; } /*******************************************************************\ +Function: java_string_library_preprocesst:: + code_assign_string_expr_to_java_string + + Inputs: + lhs - an expression representing a java string + rhs - a string expression + symbol_table - symbol table + + Output: return the following code: + > lhs = { {Object}, length=rhs.length, data=rhs.data } + + Purpose: Produce code for an assignemnt of a string expr to a Java + string. + +\*******************************************************************/ + +codet java_string_library_preprocesst::code_assign_string_expr_to_java_string( + const exprt &lhs, + const string_exprt &rhs, + symbol_tablet &symbol_table) +{ + return code_assign_components_to_java_string( + lhs, address_of_exprt(rhs.content()), rhs.length(), symbol_table); +} + +/*******************************************************************\ + Function: java_string_library_preprocesst:: code_assign_string_expr_to_new_java_string @@ -1058,8 +1097,11 @@ Function: java_string_library_preprocesst:: symbol_table - symbol table Output: return the following code: - > lhs->length=rhs.length - > lhs->data=&rhs.data + > data = new array[]; + > *data = rhs.data; + > lhs = { {Object} , length=rhs.length, data=data} + + Purpose: Produce code for an assignment of a string from a string expr. \*******************************************************************/ @@ -1073,19 +1115,15 @@ codet java_string_library_preprocesst:: assert(implements_java_char_sequence(lhs.type())); dereference_exprt deref(lhs, lhs.type().subtype()); - // Fields of the string object - exprt lhs_length=get_length(deref, symbol_table); - exprt lhs_data=get_data(deref, symbol_table); - - // Assignments code_blockt code; - // new array <- malloc(char[]) exprt new_array=allocate_fresh_array( get_data_type(deref.type(), symbol_table), loc, symbol_table, code); code.add(code_assignt( dereference_exprt(new_array, new_array.type().subtype()), rhs.content())); - code.add(code_assignt(lhs_length, rhs.length())); - code.add(code_assignt(lhs_data, new_array)); + + code.add(code_assign_components_to_java_string( + lhs, new_array, rhs.length(), symbol_table)); + return code; } @@ -1730,6 +1768,7 @@ codet java_string_library_preprocesst::make_function_from_call( Outputs: Code corresponding to: > string_expr = function_name(args) + > string = new String > string = string_expr_to_string(string) > return string @@ -1756,11 +1795,11 @@ codet java_string_library_preprocesst:: string_exprt string_expr=string_expr_of_function_application( function_name, arguments, loc, symbol_table, code); - // Assigning string_expr to symbol for keeping track of it + // Assign string_expr to symbol to keep track of it exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, code); code.add(code_assignt(string_expr_sym, string_expr)); - // Assigning to string + // Assign to string exprt str=allocate_fresh_string(type.return_type(), loc, symbol_table, code); code.add(code_assign_string_expr_to_new_java_string( str, string_expr, loc, symbol_table)); @@ -1772,6 +1811,108 @@ codet java_string_library_preprocesst:: /*******************************************************************\ +Function: + java_string_library_preprocesst::make_copy_string_code + + Inputs: + type - type of the function + loc - location in the source + symbol_table - symbol table + + Outputs: Code corresponding to: + > string_expr = string_to_string_expr(arg0) + > string_expr_sym = { string_expr.length; string_expr.content } + > str = new String + > str = string_expr_to_string(string_expr) + > return str + + Purpose: Generates code for a function which copies a string object to a new + string object. + +\*******************************************************************/ + +codet java_string_library_preprocesst::make_copy_string_code( + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table) +{ + // Code for the output + code_blockt code; + + // String expression that will hold the result + string_exprt string_expr=fresh_string_expr(loc, symbol_table, code); + + // Assign the argument to string_expr + code_typet::parametert op=type.parameters()[0]; + symbol_exprt arg0(op.get_identifier(), op.type()); + code.add(code_assign_java_string_to_string_expr( + string_expr, arg0, symbol_table)); + + // Assign string_expr to string_expr_sym + exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, code); + code.add(code_assignt(string_expr_sym, string_expr)); + + // Allocate and assign the string + exprt str=allocate_fresh_string(type.return_type(), loc, symbol_table, code); + code.add(code_assign_string_expr_to_new_java_string( + str, string_expr, loc, symbol_table)); + + // Return value + code.add(code_returnt(str)); + return code; +} + +/*******************************************************************\ + +Function: + java_string_library_preprocesst::make_copy_constructor_code + + Inputs: + type - type of the function + loc - location in the source + symbol_table - symbol table + + Outputs: Code corresponding to: + > string_expr = java_string_to_string_expr(arg1) + > string_expr_sym = { string_expr.length; string_expr.content } + > this = string_expr_to_java_string(string_expr) + + Purpose: Generates code for a constructor of a string object from another + string object. + +\*******************************************************************/ + +codet java_string_library_preprocesst::make_copy_constructor_code( + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table) +{ + // Code for the output + code_blockt code; + + // String expression that will hold the result + string_exprt string_expr=fresh_string_expr(loc, symbol_table, code); + + // Assign argument to a string_expr + code_typet::parameterst params=type.parameters(); + symbol_exprt arg1(params[1].get_identifier(), params[1].type()); + code.add(code_assign_java_string_to_string_expr( + string_expr, arg1, symbol_table)); + + // Assign string_expr to symbol to keep track of it + exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, code); + code.add(code_assignt(string_expr_sym, string_expr)); + + // Assign string_expr to `this` object + symbol_exprt arg_this(params[0].get_identifier(), params[0].type()); + code.add(code_assign_string_expr_to_new_java_string( + arg_this, string_expr, loc, symbol_table)); + + return code; +} + +/*******************************************************************\ + Function: java_string_library_preprocesst::code_for_function Inputs: @@ -1866,12 +2007,22 @@ void java_string_library_preprocesst::initialize_conversion_table() "java.lang.StringBuffer"}; // String library - cprover_equivalent_to_java_constructor + conversion_table ["java::java.lang.String.:(Ljava/lang/String;)V"]= - ID_cprover_string_copy_func; - cprover_equivalent_to_java_constructor + std::bind( + &java_string_library_preprocesst::make_copy_constructor_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3); + conversion_table ["java::java.lang.String.:(Ljava/lang/StringBuilder;)V"]= - ID_cprover_string_copy_func; + std::bind( + &java_string_library_preprocesst::make_copy_constructor_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3); cprover_equivalent_to_java_constructor ["java::java.lang.String.:([C)V"]= ID_cprover_string_copy_func; @@ -2038,9 +2189,14 @@ void java_string_library_preprocesst::initialize_conversion_table() // Not supported "java.lang.String.valueOf:(LObject;)" // StringBuilder library - cprover_equivalent_to_java_constructor + conversion_table ["java::java.lang.StringBuilder.:(Ljava/lang/String;)V"]= - ID_cprover_string_copy_func; + std::bind( + &java_string_library_preprocesst::make_copy_constructor_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3); cprover_equivalent_to_java_constructor ["java::java.lang.StringBuilder.:()V"]= ID_cprover_string_empty_string_func; @@ -2056,18 +2212,27 @@ void java_string_library_preprocesst::initialize_conversion_table() "Ljava/lang/StringBuilder;"]= ID_cprover_string_concat_func; // Not supported: "java.lang.StringBuilder.append:([CII)" - // Not supported: "java.lang.StringBuilder.append:(LCharSequence;)" + + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;II)" + "Ljava/lang/StringBuilder;"]= + ID_cprover_string_concat_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)" + "Ljava/lang/StringBuilder;"]= + ID_cprover_string_concat_func; + cprover_equivalent_to_java_assign_and_return_function ["java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"]= ID_cprover_string_concat_double_func; - conversion_table["java::java.lang.StringBuilder.append:" - "(F)Ljava/lang/StringBuilder;"]= - std::bind( - &java_string_library_preprocesst::make_string_builder_append_float_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3); + conversion_table + ["java::java.lang.StringBuilder.append:(F)Ljava/lang/StringBuilder;"]= + std::bind( + &java_string_library_preprocesst::make_string_builder_append_float_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3); cprover_equivalent_to_java_assign_and_return_function ["java::java.lang.StringBuilder.append:(I)Ljava/lang/StringBuilder;"]= ID_cprover_string_concat_int_func; @@ -2161,16 +2326,26 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_string_returning_function ["java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]= ID_cprover_string_substring_func; - cprover_equivalent_to_java_string_returning_function + conversion_table ["java::java.lang.StringBuilder.toString:()Ljava/lang/String;"]= - ID_cprover_string_copy_func; + std::bind( + &java_string_library_preprocesst::make_copy_string_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3); // Not supported "java.lang.StringBuilder.trimToSize" // TODO clean irep ids from insert_char_array etc... // StringBuffer library - cprover_equivalent_to_java_constructor + conversion_table ["java::java.lang.StringBuffer.:(Ljava/lang/String;)V"]= - ID_cprover_string_copy_func; + std::bind( + &java_string_library_preprocesst::make_copy_constructor_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3); cprover_equivalent_to_java_constructor ["java::java.lang.StringBuffer.:()V"]= ID_cprover_string_empty_string_func; @@ -2278,15 +2453,28 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_string_returning_function ["java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]= ID_cprover_string_substring_func; - cprover_equivalent_to_java_string_returning_function + conversion_table ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"]= - ID_cprover_string_copy_func; + std::bind( + &java_string_library_preprocesst::make_copy_string_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3); // Not supported "java.lang.StringBuffer.trimToSize" // Other libraries cprover_equivalent_to_java_function ["java::java.lang.CharSequence.charAt:(I)C"]= ID_cprover_string_char_at_func; + conversion_table + ["java::java.lang.CharSequence.toString:()Ljava/lang/String;"]= + std::bind( + &java_string_library_preprocesst::make_copy_string_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3); conversion_table ["java::java.lang.Float.toString:(F)Ljava/lang/String;"]= std::bind( diff --git a/src/java_bytecode/java_string_library_preprocess.h b/src/java_bytecode/java_string_library_preprocess.h index f9bfb8cffc6..16ab5cfc6a9 100644 --- a/src/java_bytecode/java_string_library_preprocess.h +++ b/src/java_bytecode/java_string_library_preprocess.h @@ -136,6 +136,16 @@ class java_string_library_preprocesst:public messaget const source_locationt &loc, symbol_tablet &symbol_table); + codet make_copy_string_code( + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table); + + codet make_copy_constructor_code( + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table); + // Auxiliary functions codet code_for_scientific_notation( const exprt &arg, @@ -251,6 +261,12 @@ class java_string_library_preprocesst:public messaget symbol_tablet &symbol_table, code_blockt &code); + codet code_assign_components_to_java_string( + const exprt &lhs, + const exprt &rhs_array, + const exprt &rhs_length, + symbol_tablet &symbol_table); + codet code_assign_string_expr_to_java_string( const exprt &lhs, const string_exprt &rhs, symbol_tablet &symbol_table);