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);