diff --git a/regression/strings-smoke-tests/java_value_of_float/test.class b/regression/strings-smoke-tests/java_value_of_float/test.class new file mode 100644 index 00000000000..ddb0cfbdc0b Binary files /dev/null and b/regression/strings-smoke-tests/java_value_of_float/test.class differ diff --git a/regression/strings-smoke-tests/java_value_of_float/test.desc b/regression/strings-smoke-tests/java_value_of_float/test.desc new file mode 100644 index 00000000000..d1cc84bd13a --- /dev/null +++ b/regression/strings-smoke-tests/java_value_of_float/test.desc @@ -0,0 +1,8 @@ +CORE +test.class +--refine-strings --function test.check +^EXIT=10$ +^SIGNAL=0$ +assertion.* file test.java line 7 .* SUCCESS$ +assertion.* file test.java line 9 .* FAILURE$ +-- diff --git a/regression/strings-smoke-tests/java_value_of_float/test.java b/regression/strings-smoke-tests/java_value_of_float/test.java new file mode 100644 index 00000000000..ff05337b112 --- /dev/null +++ b/regression/strings-smoke-tests/java_value_of_float/test.java @@ -0,0 +1,11 @@ +public class test +{ + public static void check(int i) + { + String s = String.valueOf(123.456f); + if(i == 1) + assert(s.equals("123.456")); + else + assert(!s.equals("123.456")); + } +} \ No newline at end of file diff --git a/regression/strings-smoke-tests/java_value_of_float_2/test.class b/regression/strings-smoke-tests/java_value_of_float_2/test.class new file mode 100644 index 00000000000..7e8016e0b84 Binary files /dev/null and b/regression/strings-smoke-tests/java_value_of_float_2/test.class differ diff --git a/regression/strings-smoke-tests/java_value_of_float_2/test.desc b/regression/strings-smoke-tests/java_value_of_float_2/test.desc new file mode 100644 index 00000000000..8a2a2bc6207 --- /dev/null +++ b/regression/strings-smoke-tests/java_value_of_float_2/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +test.class +--refine-strings --function test.check +^EXIT=10$ +^SIGNAL=0$ +assertion.* file test.java line 6 .* SUCCESS$ +assertion.* file test.java line 7 .* FAILURE$ +-- diff --git a/regression/strings-smoke-tests/java_value_of_float_2/test.java b/regression/strings-smoke-tests/java_value_of_float_2/test.java new file mode 100644 index 00000000000..7967e6f3668 --- /dev/null +++ b/regression/strings-smoke-tests/java_value_of_float_2/test.java @@ -0,0 +1,9 @@ +public class test +{ + public static void check() + { + String s3=String.valueOf(7.89e12f); + assert(s3.equals("7.89E12")); + assert(!s3.equals("7.89E12")); + } +} diff --git a/regression/strings-smoke-tests/java_value_of_float_3/test.class b/regression/strings-smoke-tests/java_value_of_float_3/test.class new file mode 100644 index 00000000000..3572c20abb1 Binary files /dev/null and b/regression/strings-smoke-tests/java_value_of_float_3/test.class differ diff --git a/regression/strings-smoke-tests/java_value_of_float_3/test.desc b/regression/strings-smoke-tests/java_value_of_float_3/test.desc new file mode 100644 index 00000000000..771fdebe7cc --- /dev/null +++ b/regression/strings-smoke-tests/java_value_of_float_3/test.desc @@ -0,0 +1,9 @@ +KNOWNBUG +test.class +--refine-strings --function test.check +^EXIT=10$ +^SIGNAL=0$ +assertion.* file test.java line 7 .* SUCCESS$ +assertion.* file test.java line 8 .* FAILURE$ + +-- diff --git a/regression/strings-smoke-tests/java_value_of_float_3/test.java b/regression/strings-smoke-tests/java_value_of_float_3/test.java new file mode 100644 index 00000000000..47bfa2b43cf --- /dev/null +++ b/regression/strings-smoke-tests/java_value_of_float_3/test.java @@ -0,0 +1,10 @@ +public class test +{ + public static void check() + { + String s5=String.valueOf(5.67e-9f); + // The result may not be exactly 5.67E-9 as 5.66999...E-9 is also valid + assert(s5.startsWith("5.6") && s5.endsWith("E-9")); + assert(!s5.startsWith("5.6") || !s5.endsWith("E-9")); + } + } diff --git a/regression/strings-smoke-tests/java_value_of_float_4/test.class b/regression/strings-smoke-tests/java_value_of_float_4/test.class new file mode 100644 index 00000000000..b9330858ee9 Binary files /dev/null and b/regression/strings-smoke-tests/java_value_of_float_4/test.class differ diff --git a/regression/strings-smoke-tests/java_value_of_float_4/test.desc b/regression/strings-smoke-tests/java_value_of_float_4/test.desc new file mode 100644 index 00000000000..7f1e0f8819a --- /dev/null +++ b/regression/strings-smoke-tests/java_value_of_float_4/test.desc @@ -0,0 +1,10 @@ +THOROUGH +test.class +--refine-strings --function test.check +^EXIT=10$ +^SIGNAL=0$ +assertion.* test.java line 8 .* SUCCESS$ +assertion.* test.java line 9 .* SUCCESS$ +assertion.* test.java line 10 .* SUCCESS$ +assertion.* test.java line 11 .* FAILURE$ +-- diff --git a/regression/strings-smoke-tests/java_value_of_float_4/test.java b/regression/strings-smoke-tests/java_value_of_float_4/test.java new file mode 100644 index 00000000000..13c1151eb7b --- /dev/null +++ b/regression/strings-smoke-tests/java_value_of_float_4/test.java @@ -0,0 +1,13 @@ +public class test +{ + public static void check() + { + String s7=String.valueOf(java.lang.Float.POSITIVE_INFINITY); + String s8=String.valueOf(java.lang.Float.NEGATIVE_INFINITY); + String s9=String.valueOf(java.lang.Float.NaN); + assert(s7.equals("Infinity")); + assert(s8.equals("-Infinity")); + assert(s9.equals("NaN")); + assert(!s7.equals("Infinity") || !s8.equals("-Infinity") || !s9.equals("NaN")); + } +} diff --git a/regression/strings-smoke-tests/java_value_of_float_5/test.class b/regression/strings-smoke-tests/java_value_of_float_5/test.class new file mode 100644 index 00000000000..576229eef26 Binary files /dev/null and b/regression/strings-smoke-tests/java_value_of_float_5/test.class differ diff --git a/regression/strings-smoke-tests/java_value_of_float_5/test.desc b/regression/strings-smoke-tests/java_value_of_float_5/test.desc new file mode 100644 index 00000000000..7a279ade453 --- /dev/null +++ b/regression/strings-smoke-tests/java_value_of_float_5/test.desc @@ -0,0 +1,8 @@ +THOROUGH +test.class +--refine-strings --function test.check +^EXIT=10$ +^SIGNAL=0$ +assertion.* file test.java line 6 .* SUCCESS$ +assertion.* file test.java line 7 .* FAILURE$ +-- diff --git a/regression/strings-smoke-tests/java_value_of_float_5/test.java b/regression/strings-smoke-tests/java_value_of_float_5/test.java new file mode 100644 index 00000000000..d64f033c86c --- /dev/null +++ b/regression/strings-smoke-tests/java_value_of_float_5/test.java @@ -0,0 +1,9 @@ +public class test +{ + public static void check() + { + String s1=String.valueOf(-123.456f); + assert(s1.equals("-123.456")); + assert(!s1.equals("-123.456")); + } +} diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index d19b649908a..5a1fedf65a9 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -29,6 +29,8 @@ Date: April 2017 /// \param type: a type /// \param tag: a string +/// \return Boolean telling whether the type is a struct with the given tag or a +/// symbolic type with the tag prefixed by "java::" bool java_string_library_preprocesst::java_type_matches_tag( const typet &type, const std::string &tag) { @@ -45,7 +47,8 @@ bool java_string_library_preprocesst::java_type_matches_tag( return false; } -/// \par parameters: a type +/// \param type: a type +/// \return Boolean telling whether the type is that of java string pointer bool java_string_library_preprocesst::is_java_string_pointer_type( const typet &type) { @@ -58,21 +61,25 @@ bool java_string_library_preprocesst::is_java_string_pointer_type( return false; } -/// \par parameters: a type +/// \param type: a type +/// \return Boolean telling whether the type is that of java string bool java_string_library_preprocesst::is_java_string_type( const typet &type) { return java_type_matches_tag(type, "java.lang.String"); } -/// \par parameters: a type +/// \param type: a type +/// \return Boolean telling whether the type is that of java StringBuilder bool java_string_library_preprocesst::is_java_string_builder_type( const typet &type) { return java_type_matches_tag(type, "java.lang.StringBuilder"); } -/// \par parameters: a type +/// \param type: a type +/// \return Boolean telling whether the type is that of java StringBuilder +/// pointers bool java_string_library_preprocesst::is_java_string_builder_pointer_type( const typet &type) { @@ -85,14 +92,17 @@ bool java_string_library_preprocesst::is_java_string_builder_pointer_type( return false; } -/// \par parameters: a type +/// \param type: a type +/// \return Boolean telling whether the type is that of java StringBuffer bool java_string_library_preprocesst::is_java_string_buffer_type( const typet &type) { return java_type_matches_tag(type, "java.lang.StringBuffer"); } -/// \par parameters: a type +/// \param type: a type +/// \return Boolean telling whether the type is that of java StringBuffer +/// pointers bool java_string_library_preprocesst::is_java_string_buffer_pointer_type( const typet &type) { @@ -105,14 +115,17 @@ bool java_string_library_preprocesst::is_java_string_buffer_pointer_type( return false; } -/// \par parameters: a type +/// \param type: a type +/// \return Boolean telling whether the type is that of java char sequence bool java_string_library_preprocesst::is_java_char_sequence_type( const typet &type) { return java_type_matches_tag(type, "java.lang.CharSequence"); } -/// \par parameters: a type +/// \param type: a type +/// \return Boolean telling whether the type is that of a pointer to a java char +/// sequence bool java_string_library_preprocesst::is_java_char_sequence_pointer_type( const typet &type) { @@ -125,7 +138,8 @@ bool java_string_library_preprocesst::is_java_char_sequence_pointer_type( return false; } -/// \par parameters: a type +/// \param type: a type +/// \return Boolean telling whether the type is that of java char array bool java_string_library_preprocesst::is_java_char_array_type( const typet &type) { @@ -148,6 +162,7 @@ bool java_string_library_preprocesst::is_java_char_array_pointer_type( } /// \param symbol_table: a symbol_table containing an entry for java Strings +/// \return the type of data fields in java Strings. typet string_data_type(symbol_tablet symbol_table) { symbolt sym=symbol_table.lookup("java::java.lang.String"); @@ -242,6 +257,7 @@ void java_string_library_preprocesst::declare_function( /// \param symbol_table: symbol table /// \param init_code: code block, in which declaration of some arguments may be /// added +/// \return a list of expressions exprt::operandst java_string_library_preprocesst::process_parameters( const code_typet::parameterst ¶ms, const source_locationt &loc, @@ -295,6 +311,7 @@ void java_string_library_preprocesst::process_single_operand( /// \param symbol_table: symbol table /// \param init_code: code block, in which declaration of some arguments may be /// added +/// \return a list of expressions exprt::operandst java_string_library_preprocesst::process_operands( const exprt::operandst &operands, const source_locationt &loc, @@ -329,6 +346,7 @@ exprt::operandst java_string_library_preprocesst::process_operands( /// \param symbol_table: symbol table /// \param init_code: code block, in which declaration of some arguments may be /// added +/// \return a list of expressions exprt::operandst java_string_library_preprocesst::process_equals_function_operands( const exprt::operandst &operands, @@ -357,6 +375,7 @@ exprt::operandst /// Finds the type of the data component /// \param type: a type containing a "data" component /// \param symbol_table: symbol table +/// \return type of the "data" component typet java_string_library_preprocesst::get_data_type( const typet &type, const symbol_tablet &symbol_table) { @@ -380,6 +399,7 @@ typet java_string_library_preprocesst::get_data_type( /// Finds the type of the length component /// \param type: a type containing a "length" component /// \param symbol_table: symbol table +/// \return type of the "length" component typet java_string_library_preprocesst::get_length_type( const typet &type, const symbol_tablet &symbol_table) { @@ -403,6 +423,7 @@ typet java_string_library_preprocesst::get_length_type( /// access length member /// \param expr: an expression of structured type with length component /// \param symbol_table: symbol table +/// \return expression representing the "length" member exprt java_string_library_preprocesst::get_length( const exprt &expr, const symbol_tablet &symbol_table) { @@ -413,6 +434,7 @@ exprt java_string_library_preprocesst::get_length( /// access data member /// \param expr: an expression of structured type with length component /// \param symbol_table: symbol table +/// \return expression representing the "data" member exprt java_string_library_preprocesst::get_data( const exprt &expr, const symbol_tablet &symbol_table) { @@ -425,6 +447,7 @@ exprt java_string_library_preprocesst::get_data( /// \param loc: location in the source /// \param symbol_table: symbol table /// \param code: code block, in which some assignments will be added +/// \return a string expression string_exprt java_string_library_preprocesst::replace_char_array( const exprt &array_pointer, const source_locationt &loc, @@ -464,6 +487,7 @@ string_exprt java_string_library_preprocesst::replace_char_array( /// \param type: a type for refined strings /// \param loc: a location in the program /// \param symbol_table: symbol table +/// \return a new symbol symbol_exprt java_string_library_preprocesst::fresh_string( const typet &type, const source_locationt &loc, symbol_tablet &symbol_table) { @@ -478,6 +502,7 @@ symbol_exprt java_string_library_preprocesst::fresh_string( /// \param loc: a location in the program /// \param symbol_table: symbol table /// \param code: code block to which allocation instruction will be added +/// \return a new string_expr string_exprt java_string_library_preprocesst::fresh_string_expr( const source_locationt &loc, symbol_tablet &symbol_table, code_blockt &code) { @@ -503,6 +528,7 @@ string_exprt java_string_library_preprocesst::fresh_string_expr( /// \param loc: a location in the program /// \param symbol_table: symbol table /// \param code: code block to which allocation instruction will be added +/// \return a new expression of refined string type exprt java_string_library_preprocesst::fresh_string_expr_symbol( const source_locationt &loc, symbol_tablet &symbol_table, code_blockt &code) { @@ -522,6 +548,7 @@ exprt java_string_library_preprocesst::fresh_string_expr_symbol( /// \param loc: a location in the program /// \param symbol_table: symbol table /// \param code: code block to which allocation instruction will be added +/// \return a new string exprt java_string_library_preprocesst::allocate_fresh_string( const typet &type, const source_locationt &loc, @@ -540,6 +567,7 @@ exprt java_string_library_preprocesst::allocate_fresh_string( /// \param loc: a location in the program /// \param symbol_table: symbol table /// \param code: code block to which allocation instruction will be added +/// \return a new array exprt java_string_library_preprocesst::allocate_fresh_array( const typet &type, const source_locationt &loc, @@ -557,6 +585,7 @@ exprt java_string_library_preprocesst::allocate_fresh_array( /// \param arguments: a list of arguments /// \param type: return type of the function /// \param symbol_table: a symbol table +/// \return a function application representing: `function_name(arguments)` exprt java_string_library_preprocesst::make_function_application( const irep_idt &function_name, const exprt::operandst &arguments, @@ -580,6 +609,10 @@ exprt java_string_library_preprocesst::make_function_application( /// \param function_name: the name of the function /// \param arguments: a list of arguments /// \param symbol_table: a symbol table +/// \return the following code: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// lhs = (arguments) +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::code_assign_function_application( const exprt &lhs, const irep_idt &function_name, @@ -596,6 +629,10 @@ codet java_string_library_preprocesst::code_assign_function_application( /// \param arguments: a list of arguments /// \param type: the return type /// \param symbol_table: a symbol table +/// \return the following code: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// return (arguments) +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::code_return_function_application( const irep_idt &function_name, const exprt::operandst &arguments, @@ -611,6 +648,11 @@ codet java_string_library_preprocesst::code_return_function_application( /// \param function_name: the name of the function /// \param arguments: arguments of the function /// \param symbol_table: symbol table +/// \return return the following code: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// str.length = _length(arguments) +/// str.data = _data(arguments) +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::code_assign_function_to_string_expr( const string_exprt &string_expr, const irep_idt &function_name, @@ -635,6 +677,12 @@ codet java_string_library_preprocesst::code_assign_function_to_string_expr( /// \param loc: a location in the program /// \param symbol_table: symbol table /// \param code: code block in which we add instructions +/// \return return a string expr str and add the following code: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// array = str.data +/// str.length = _length(arguments) +/// str.data = _data(arguments) +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ string_exprt java_string_library_preprocesst:: string_expr_of_function_application( const irep_idt &function_name, @@ -654,6 +702,10 @@ string_exprt java_string_library_preprocesst:: /// \param rhs_array: pointer to the array to assign /// \param rhs_length: length of the array to assign /// \param symbol_table: symbol table +/// \return return the following code: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// lhs = { {Object}, length=rhs_length, data=rhs_array } +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::code_assign_components_to_java_string( const exprt &lhs, const exprt &rhs_array, @@ -687,6 +739,10 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string( /// \param lhs: an expression representing a java string /// \param rhs: a string expression /// \param symbol_table: symbol table +/// \return return the following code: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// lhs = { {Object}, length=rhs.length, data=rhs.data } +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::code_assign_string_expr_to_java_string( const exprt &lhs, const string_exprt &rhs, @@ -701,6 +757,12 @@ codet java_string_library_preprocesst::code_assign_string_expr_to_java_string( /// \param rhs: a string expression /// \param loc: a location in the program /// \param symbol_table: symbol table +/// \return return the following code: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// data = new array[]; +/// *data = rhs.data; +/// lhs = { {Object} , length=rhs.length, data=data} +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst:: code_assign_string_expr_to_new_java_string( const exprt &lhs, @@ -726,6 +788,11 @@ codet java_string_library_preprocesst:: /// \param lhs: a string expression /// \param rhs: an expression representing a java string /// \param symbol_table: symbol table +/// \return return the following code: +/// ~~~~~~~~~~~~~~~~~~~~~~ +/// lhs.length=rhs->length +/// lhs.data=*(rhs->data) +/// ~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::code_assign_java_string_to_string_expr( const string_exprt &lhs, const exprt &rhs, symbol_tablet &symbol_table) { @@ -753,30 +820,34 @@ codet java_string_library_preprocesst::code_assign_java_string_to_string_expr( } /// \param lhs: an expression representing a java string -/// \param tmp_string: a temporary string to hold the literal /// \param s: the literal to be assigned /// \param symbol_table: symbol table +/// \return return the following code: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// tmp_string = "" +/// lhs = (string_expr) tmp_string +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst:: code_assign_string_literal_to_string_expr( const string_exprt &lhs, - const exprt &tmp_string, const std::string &s, symbol_tablet &symbol_table) { - code_blockt code; - code.add(code_assignt(tmp_string, string_literal(s))); - code.add(code_assign_java_string_to_string_expr( - lhs, tmp_string, symbol_table)); - return code; + constant_exprt expr(s, string_typet()); + return code_assign_function_to_string_expr( + lhs, ID_cprover_string_literal_func, {expr}, symbol_table); } /// Used to provide code for the Java String.equals(Object) function. /// \param type: type of the function call /// \param loc: location in the program_invocation_name /// \param symbol_table: symbol table -/// \return Code corresponding to: > string_expr1 = {this->length; *this->data} -/// > string_expr2 = {arg->length; *arg->data} > return -/// cprover_string_equal(string_expr1, string_expr2) +/// \return Code corresponding to: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// string_expr1 = {this->length; *this->data} +/// string_expr2 = {arg->length; *arg->data} +/// return cprover_string_equal(string_expr1, string_expr2) +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_equals_function_code( const code_typet &type, const source_locationt &loc, @@ -797,31 +868,23 @@ codet java_string_library_preprocesst::make_equals_function_code( return code; } -/// construct a Java string literal from a constant string value +/// construct a string_exprt from a constant string value /// \param s: a string -/// \return an expression representing a Java string literal with the given -/// content. -exprt java_string_library_preprocesst::string_literal(const std::string &s) +/// \param symbol_table: a symbol table +/// \return an expression representing a string expr with the given content +exprt java_string_library_preprocesst::string_literal( + const std::string &s, symbol_tablet &symbol_table) { - exprt string_literal(ID_java_string_literal); - string_literal.set(ID_value, s); - return string_literal; + constant_exprt expr(s, string_typet()); + return make_function_application( + ID_cprover_string_literal_func, {expr}, refined_string_type, symbol_table); } -/// Provide code for the Float.toString(F) function. +/// Provide code for the String.valueOf(F) function. /// \param type: type of the function call /// \param loc: location in the program_invocation_name /// \param symbol_table: symbol table -/// \return Code corresponding to: > String * str; > str = MALLOC(String); > -/// String * tmp_string; > int string_expr_length; > char[] -/// string_expr_content; > CPROVER_string string_expr_sym; > if -/// arguments[1]==NaN > then {tmp_string="NaN"; -/// string_expr=(string_expr)tmp_string} > if arguments[1]==Infinity > then -/// {tmp_string="Infinity"; string_expr=(string_expr)tmp_string} > if -/// 1e-3 then -/// string_expr=cprover_float_to_string(arguments[1]) > else -/// string_expr=cprover_float_to_scientific_notation_string(arg[1]) > -/// string_expr_sym=string_expr; > str=(String*) string_expr; > return str; +/// \return Code corresponding to the Java conversion of floats to strings. codet java_string_library_preprocesst::make_float_to_string_code( const code_typet &type, const source_locationt &loc, @@ -837,83 +900,122 @@ codet java_string_library_preprocesst::make_float_to_string_code( // Declaring and allocating String * str exprt str=allocate_fresh_string(type.return_type(), loc, symbol_table, code); - exprt tmp_string=fresh_string(type.return_type(), loc, symbol_table); - // Declaring CPROVER_string string_expr - string_exprt string_expr=fresh_string_expr(loc, symbol_table, code); - exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, code); - - // List of the different cases - std::vector case_list; - - // First case in the list is the default - code_ifthenelset case_sci_notation; + // Expression representing 0.0 ieee_float_spect float_spec=ieee_float_spect::single_precision(); - // Subcase of 0.0 - // TODO: case of -0.0 ieee_floatt zero_float(float_spec); zero_float.from_float(0.0); constant_exprt zero=zero_float.to_expr(); - case_sci_notation.cond()=ieee_float_equal_exprt(arg, zero); - case_sci_notation.then_case()=code_assign_string_literal_to_string_expr( - string_expr, tmp_string, "0.0", symbol_table); - // Subcase of computerized scientific notation - case_sci_notation.else_case()=code_assign_function_to_string_expr( - string_expr, ID_cprover_string_of_float_func, {arg}, symbol_table); - case_list.push_back(case_sci_notation); + // For each possible case with have a condition and a string_exprt + std::vector condition_list; + std::vector string_expr_list; + + // Case of computerized scientific notation + condition_list.push_back(binary_relation_exprt(arg, ID_ge, zero)); + string_exprt sci_notation=fresh_string_expr(loc, symbol_table, code); + exprt sci_notation_sym=fresh_string_expr_symbol(loc, symbol_table, code); + code.add(code_assign_function_to_string_expr( + sci_notation, + ID_cprover_string_of_float_scientific_notation_func, + {arg}, + symbol_table)); + // Assign string_expr_sym = { string_expr_length, string_expr_content } + code.add(code_assignt(sci_notation_sym, sci_notation)); + string_expr_list.push_back(sci_notation); + + // Subcase of negative scientific notation + condition_list.push_back(binary_relation_exprt(arg, ID_lt, zero)); + string_exprt neg_sci_notation=fresh_string_expr(loc, symbol_table, code); + exprt neg_sci_notation_sym=fresh_string_expr_symbol(loc, symbol_table, code); + string_exprt minus_sign=fresh_string_expr(loc, symbol_table, code); + code.add(code_assign_string_literal_to_string_expr( + minus_sign, "-", symbol_table)); + code.add(code_assign_function_to_string_expr( + neg_sci_notation, + ID_cprover_string_concat_func, + {minus_sign, sci_notation}, + symbol_table)); + code.add(code_assignt(neg_sci_notation_sym, neg_sci_notation)); + string_expr_list.push_back(neg_sci_notation); // Case of NaN - code_ifthenelset case_nan; - case_nan.cond()=isnan_exprt(arg); - case_nan.then_case()=code_assign_string_literal_to_string_expr( - string_expr, tmp_string, "NaN", symbol_table); - case_list.push_back(case_nan); + condition_list.push_back(isnan_exprt(arg)); + string_exprt nan=fresh_string_expr(loc, symbol_table, code); + code.add(code_assign_string_literal_to_string_expr( + nan, "NaN", symbol_table)); + string_expr_list.push_back(nan); // Case of Infinity - code_ifthenelset case_infinity; - code_ifthenelset case_minus_infinity; + extractbit_exprt is_neg(arg, float_spec.width()-1); + condition_list.push_back(and_exprt(isinf_exprt(arg), not_exprt(is_neg))); + string_exprt infinity=fresh_string_expr(loc, symbol_table, code); + code.add(code_assign_string_literal_to_string_expr( + infinity, "Infinity", symbol_table)); + string_expr_list.push_back(infinity); - case_infinity.cond()=isinf_exprt(arg); // Case -Infinity - exprt isneg=extractbit_exprt(arg, float_spec.width()-1); - case_minus_infinity.cond()=isneg; - case_minus_infinity.then_case()=code_assign_string_literal_to_string_expr( - string_expr, tmp_string, "-Infinity", symbol_table); - case_minus_infinity.else_case()=code_assign_string_literal_to_string_expr( - string_expr, tmp_string, "Infinity", symbol_table); - case_infinity.then_case()=case_minus_infinity; - case_list.push_back(case_infinity); + string_exprt minus_infinity=fresh_string_expr(loc, symbol_table, code); + condition_list.push_back(and_exprt(isinf_exprt(arg), is_neg)); + code.add(code_assign_string_literal_to_string_expr( + minus_infinity, "-Infinity", symbol_table)); + string_expr_list.push_back(minus_infinity); // Case of simple notation - code_ifthenelset case_simple_notation; - ieee_floatt bound_inf_float(float_spec); ieee_floatt bound_sup_float(float_spec); bound_inf_float.from_float(1e-3); bound_sup_float.from_float(1e7); + bound_inf_float.change_spec(float_spec); + bound_sup_float.change_spec(float_spec); constant_exprt bound_inf=bound_inf_float.to_expr(); constant_exprt bound_sup=bound_sup_float.to_expr(); and_exprt is_simple_float( binary_relation_exprt(arg, ID_ge, bound_inf), binary_relation_exprt(arg, ID_lt, bound_sup)); - case_simple_notation.cond()=is_simple_float; - case_simple_notation.then_case()=code_assign_function_to_string_expr( - string_expr, ID_cprover_string_of_float_func, {arg}, symbol_table); - case_list.push_back(case_simple_notation); - - // Combining all cases - for(std::size_t i=1; i(args) function: > cprover_string_length = -/// fun(arg).length; > cprover_string_array = fun(arg).data; > this->length = -/// cprover_string_length; > this->data = cprover_string_array; > -/// cprover_string = {.=cprover_string_length, .=cprover_string_array}; +/// \return code for the String.(args) function: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// cprover_string_length = fun(arg).length; +/// cprover_string_array = fun(arg).data; +/// this->length = cprover_string_length; +/// this->data = cprover_string_array; +/// cprover_string = {.=cprover_string_length, .=cprover_string_array}; +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_init_function_from_call( const irep_idt &function_name, const code_typet &type, @@ -1080,9 +1186,13 @@ codet java_string_library_preprocesst::make_string_to_char_array_code( /// \param type: type of the function called /// \param loc: location in the source /// \param symbol_table: the symbol table -/// \return Code corresponding to > Class class1; > string_expr1 = -/// substr(this->@class_identifier, 6) > class1=Class.forName(string_expr1) > -/// return class1 +/// \return Code corresponding to +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// Class class1; +/// string_expr1 = substr(this->@class_identifier, 6) +/// class1=Class.forName(string_expr1) +/// return class1 +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_object_get_class_code( const code_typet &type, const source_locationt &loc, @@ -1160,7 +1270,10 @@ codet java_string_library_preprocesst::make_object_get_class_code( /// \param type: type of the function /// \param loc: location in the source /// \param symbol_table: symbol table -/// \return Code corresponding to: > return function_name(args); +/// \return Code corresponding to: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// return function_name(args) +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_function_from_call( const irep_idt &function_name, const code_typet &type, @@ -1181,8 +1294,13 @@ codet java_string_library_preprocesst::make_function_from_call( /// \param type: type of the function /// \param loc: location in the source /// \param symbol_table: symbol table -/// \return Code corresponding to: > string_expr = function_name(args) > string -/// = new String > string = string_expr_to_string(string) > return string +/// \return Code corresponding to: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// string_expr = function_name(args) +/// string = new String +/// string = string_expr_to_string(string) +/// return string +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst:: make_string_returning_function_from_call( const irep_idt &function_name, @@ -1220,9 +1338,14 @@ codet java_string_library_preprocesst:: /// \param type: type of the function /// \param loc: location in the source /// \param symbol_table: symbol table -/// \return 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 +/// \return 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 +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_copy_string_code( const code_typet &type, const source_locationt &loc, @@ -1259,9 +1382,12 @@ codet java_string_library_preprocesst::make_copy_string_code( /// \param type: type of the function /// \param loc: location in the source /// \param symbol_table: symbol table -/// \return 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) +/// \return 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) +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_copy_constructor_code( const code_typet &type, const source_locationt &loc, @@ -1295,8 +1421,12 @@ codet java_string_library_preprocesst::make_copy_constructor_code( /// \param type: type of the function /// \param loc: location in the source /// \param symbol_table: symbol table -/// \return Code corresponding to: > str_expr = java_string_to_string_expr(this) -/// > str_expr_sym = str_expr > return this->length +/// \return Code corresponding to: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// str_expr = java_string_to_string_expr(this) +/// str_expr_sym = str_expr +/// return this->length +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_string_length_code( const code_typet &type, const source_locationt &loc, @@ -1555,12 +1685,22 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_string_returning_function ["java::java.lang.String.valueOf:([CII)Ljava/lang/String;"]= ID_cprover_string_copy_func; - cprover_equivalent_to_java_string_returning_function + conversion_table ["java::java.lang.String.valueOf:(D)Ljava/lang/String;"]= - ID_cprover_string_of_double_func; - cprover_equivalent_to_java_string_returning_function + std::bind( + &java_string_library_preprocesst::make_float_to_string_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3); + conversion_table ["java::java.lang.String.valueOf:(F)Ljava/lang/String;"]= - ID_cprover_string_of_float_func; + std::bind( + &java_string_library_preprocesst::make_float_to_string_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3); cprover_equivalent_to_java_string_returning_function ["java::java.lang.String.valueOf:(I)Ljava/lang/String;"]= ID_cprover_string_of_int_func; @@ -1786,7 +1926,7 @@ void java_string_library_preprocesst::initialize_conversion_table() std::placeholders::_2, std::placeholders::_3); - // CharSequence library + // CharSequence library cprover_equivalent_to_java_function ["java::java.lang.CharSequence.charAt:(I)C"]= ID_cprover_string_char_at_func; diff --git a/src/java_bytecode/java_string_library_preprocess.h b/src/java_bytecode/java_string_library_preprocess.h index 81c98614fbd..ff3a7142fbc 100644 --- a/src/java_bytecode/java_string_library_preprocess.h +++ b/src/java_bytecode/java_string_library_preprocess.h @@ -283,11 +283,10 @@ class java_string_library_preprocesst:public messaget codet code_assign_string_literal_to_string_expr( const string_exprt &lhs, - const exprt &tmp_string, const std::string &s, symbol_tablet &symbol_table); - exprt string_literal(const std::string &s); + exprt string_literal(const std::string &s, symbol_tablet &symbol_table); codet make_function_from_call( const irep_idt &function_name, diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 3f3465277a3..5c994aefc14 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -165,6 +165,7 @@ SRC = $(BOOLEFORCE_SRC) \ refinement/string_constraint_generator_constants.cpp \ refinement/string_constraint_generator_indexof.cpp \ refinement/string_constraint_generator_insert.cpp \ + refinement/string_constraint_generator_float.cpp \ refinement/string_constraint_generator_main.cpp \ refinement/string_constraint_generator_testing.cpp \ refinement/string_constraint_generator_transformation.cpp \ diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 447bfd5f6f0..ca8bf17b5f0 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -155,6 +155,8 @@ class string_constraint_generatort string_exprt add_axioms_for_concat_long(const function_application_exprt &f); string_exprt add_axioms_for_concat_bool(const function_application_exprt &f); string_exprt add_axioms_for_concat_char(const function_application_exprt &f); + string_exprt add_axioms_for_concat_char( + const string_exprt &string_expr, const exprt &char_expr); string_exprt add_axioms_for_concat_double( const function_application_exprt &f); string_exprt add_axioms_for_concat_float(const function_application_exprt &f); @@ -234,11 +236,17 @@ class string_constraint_generatort // and minus infinity the string are "Infinity" and "-Infinity respectively // otherwise the string contains only characters in [0123456789.] and '-' at // the start for negative number - string_exprt add_axioms_from_float(const function_application_exprt &f); - string_exprt add_axioms_from_float( - const exprt &f, - const refined_string_typet &ref_type, - bool double_precision); + string_exprt add_axioms_for_string_of_float( + const function_application_exprt &f); + string_exprt add_axioms_for_string_of_float( + const exprt &f, const refined_string_typet &ref_type); + + string_exprt add_axioms_for_fractional_part( + const exprt &i, size_t max_size, const refined_string_typet &ref_type); + string_exprt add_axioms_from_float_scientific_notation( + const exprt &f, const refined_string_typet &ref_type); + string_exprt add_axioms_from_float_scientific_notation( + const function_application_exprt &f); // Add axioms corresponding to the String.valueOf(D) java function // TODO: the specifications is only partial diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp index b2c9a418055..1a157bbd859 100644 --- a/src/solvers/refinement/string_constraint_generator_concat.cpp +++ b/src/solvers/refinement/string_constraint_generator_concat.cpp @@ -13,7 +13,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include -/// Add axioms to say that the returned string expression is equal to the +/// Add axioms enforcing that the returned string expression is equal to the /// concatenation of s1 with the substring of s2 starting at index start_index /// and ending at index end_index. /// @@ -77,7 +77,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat( return add_axioms_for_concat_substr(s1, s2, index_zero, s2.length()); } -/// Add axioms to say that the returned string expression is equal to the +/// Add axioms enforcing that the returned string expression is equal to the /// concatenation of the two string arguments of the function application. /// /// In case 4 arguments instead of 2 are given the last two arguments are @@ -85,7 +85,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat( /// of the second argument: this is similar to the Java /// StringBuilder.append(CharSequence s, int start, int end) method. /// -/// \param f: function application with two arguments which are strings +/// \param f: function application with two string arguments /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_for_concat( const function_application_exprt &f) @@ -148,9 +148,21 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_char( const function_application_exprt &f) { string_exprt s1=get_string_expr(args(f, 2)[0]); - const refined_string_typet &ref_type=to_refined_string_type(s1.type()); - string_exprt s2=add_axioms_from_char(args(f, 2)[1], ref_type); - return add_axioms_for_concat(s1, s2); + return add_axioms_for_concat_char(s1, args(f, 2)[1]); +} + +/// Add axioms corresponding to adding the character char at the end of +/// string_expr. +/// \param string_expr: a string expression +/// \param char' a character expression +/// \return a new string expression +string_exprt string_constraint_generatort::add_axioms_for_concat_char( + const string_exprt &string_expr, const exprt &char_expr) +{ + const refined_string_typet &ref_type= + to_refined_string_type(string_expr.type()); + string_exprt s2=add_axioms_from_char(char_expr, ref_type); + return add_axioms_for_concat(string_expr, s2); } /// Add axioms corresponding to the StringBuilder.append(D) java function @@ -162,7 +174,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_double( string_exprt s1=get_string_expr(args(f, 2)[0]); PRECONDITION(refined_string_typet::is_refined_string_type(f.type())); refined_string_typet ref_type=to_refined_string_type(f.type()); - string_exprt s2=add_axioms_from_float(args(f, 2)[1], ref_type, true); + string_exprt s2=add_axioms_for_string_of_float(args(f, 2)[1], ref_type); return add_axioms_for_concat(s1, s2); } @@ -175,7 +187,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_float( string_exprt s1=get_string_expr(args(f, 2)[0]); PRECONDITION(refined_string_typet::is_refined_string_type(f.type())); refined_string_typet ref_type=to_refined_string_type(f.type()); - string_exprt s2=add_axioms_from_float(args(f, 2)[1], ref_type, false); + string_exprt s2=add_axioms_for_string_of_float(args(f, 2)[1], ref_type); return add_axioms_for_concat(s1, s2); } diff --git a/src/solvers/refinement/string_constraint_generator_float.cpp b/src/solvers/refinement/string_constraint_generator_float.cpp new file mode 100644 index 00000000000..0bbb9ae6efa --- /dev/null +++ b/src/solvers/refinement/string_constraint_generator_float.cpp @@ -0,0 +1,457 @@ +/*******************************************************************\ + +Module: Generates string constraints for functions generating strings + from other types, in particular int, long, float, double, char, bool + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +/// \file +/// Generates string constraints for functions generating strings from other +/// types, in particular int, long, float, double, char, bool + +#include + +#include "string_constraint_generator.h" + + +/// Gets the unbiased exponent in a floating-point bit-vector +/// +/// TODO: factorize with float_bv.cpp float_utils.h +/// \param src: a floating point expression +/// \param spec: specification for floating points +/// \return A new 32 bit integer expression representing the exponent. +/// Note that 32 bits are sufficient for the exponent even +/// in octuple precision. +exprt get_exponent( + const exprt &src, const ieee_float_spect &spec) +{ + exprt exp_bits=extractbits_exprt( + src, spec.f+spec.e-1, spec.f, unsignedbv_typet(spec.e)); + + // Exponent is in biased form (numbers from -128 to 127 are encoded with + // integer from 0 to 255) we have to remove the bias. + return minus_exprt( + typecast_exprt(exp_bits, signedbv_typet(32)), + from_integer(spec.bias(), signedbv_typet(32))); +} + +/// Gets the fraction without hidden bit +/// \param src: a floating point expression +/// \param spec: specification for floating points +/// \return An unsigned value representing the fractional part. +exprt get_fraction(const exprt &src, const ieee_float_spect &spec) +{ + return extractbits_exprt(src, spec.f-1, 0, unsignedbv_typet(spec.f)); +} + +/// Gets the significand as a java integer, looking for the hidden bit. +/// Since the most significant bit is 1 for normalized number, it is not part +/// of the encoding of the significand and is 0 only if all the bits of the +/// exponent are 0, that is why it is called the hidden bit. +/// \param src: a floating point expression +/// \param spec: specification for floating points +/// \param type: type of the output, should be unsigned with width greater than +/// the width of the significand in the given spec +/// \return An integer expression of the given type representing the +/// significand. +exprt get_significand( + const exprt &src, const ieee_float_spect &spec, const typet &type) +{ + PRECONDITION(type.id()==ID_unsignedbv); + PRECONDITION(to_unsignedbv_type(type).get_width()>spec.f); + typecast_exprt fraction(get_fraction(src, spec), type); + exprt exponent=get_exponent(src, spec); + equal_exprt all_zeros(exponent, from_integer(0, exponent.type())); + exprt hidden_bit=from_integer((1 << spec.f), type); + bitor_exprt with_hidden_bit(fraction, hidden_bit); + return if_exprt(all_zeros, fraction, with_hidden_bit); +} + +/// Create an expression to represent a float or double value. +/// \param f: a floating point value in double precision +/// \return an expression representing this floating point +exprt constant_float(const double f, const ieee_float_spect &float_spec) +{ + ieee_floatt fl(float_spec); + if(float_spec==ieee_float_spect::single_precision()) + fl.from_float(f); + else if(float_spec==ieee_float_spect::double_precision()) + fl.from_double(f); + else + UNREACHABLE; + return fl.to_expr(); +} + +/// Round a float expression to an integer closer to 0 +/// \param f: expression representing a float +/// \return expression representing a 32 bit integer +exprt round_expr_to_zero(const exprt &f) +{ + exprt rounding=from_integer(ieee_floatt::ROUND_TO_ZERO, unsignedbv_typet(32)); + return floatbv_typecast_exprt(f, rounding, signedbv_typet(32)); +} + +/// Multiplication of expressions representing floating points. +/// Note that the rounding mode is set to ROUND_TO_EVEN. +/// \param f: a floating point expression +/// \param g: a floating point expression +/// \param rounding: rounding mode +/// \return An expression representing floating point multiplication. +exprt floatbv_mult(const exprt &f, const exprt &g) +{ + PRECONDITION(f.type()==g.type()); + ieee_floatt::rounding_modet rounding=ieee_floatt::ROUND_TO_EVEN; + exprt mult(ID_floatbv_mult, f.type()); + mult.copy_to_operands(f); + mult.copy_to_operands(g); + mult.copy_to_operands(from_integer(rounding, unsignedbv_typet(32))); + return mult; +} + +/// Convert integers to floating point to be used in operations with +/// other values that are in floating point representation. +/// \param i: an expression representing an integer +/// \param spec: specification for floating point numbers +/// \return An expression representing the value of the input +/// integer as a float. +exprt floatbv_of_int_expr(const exprt &i, const ieee_float_spect &spec) +{ + exprt rounding=from_integer(ieee_floatt::ROUND_TO_ZERO, unsignedbv_typet(32)); + return floatbv_typecast_exprt(i, rounding, spec.to_type()); +} + +/// Estimate the decimal exponent that should be used to represent a given +/// floating point value in decimal. +/// We are looking for d such that n * 10^d = m * 2^e, so: +/// d = log_10(m) + log_10(2) * e - log_10(n) +/// m -- the fraction -- should be between 1 and 2 so log_10(m) +/// in [0,log_10(2)]. +/// n -- the fraction in base 10 -- should be between 1 and 10 so +/// log_10(n) in [0, 1]. +/// So the estimate is given by: +/// d ~=~ floor(log_10(2) * e) +/// \param f: a floating point expression +/// \param spec: specification for floating point +exprt estimate_decimal_exponent(const exprt &f, const ieee_float_spect &spec) +{ + exprt log_10_of_2=constant_float(0.30102999566398119521373889472449302, spec); + exprt bin_exp=get_exponent(f, spec); + exprt float_bin_exp=floatbv_of_int_expr(bin_exp, spec); + exprt dec_exp=floatbv_mult(float_bin_exp, log_10_of_2); + binary_relation_exprt negative_exp(dec_exp, ID_lt, constant_float(0.0, spec)); + // Rounding to zero is not correct for negative numbers, so we substract 1. + minus_exprt dec_minus_one(dec_exp, constant_float(1.0, spec)); + if_exprt adjust_for_neg(negative_exp, dec_minus_one, dec_exp); + return round_expr_to_zero(adjust_for_neg); +} + +/// Add axioms corresponding to the String.valueOf(F) java function +/// \param f: function application with one float argument +/// \return a new string expression +string_exprt string_constraint_generatort::add_axioms_for_string_of_float( + const function_application_exprt &f) +{ + return add_axioms_for_string_of_float( + args(f, 1)[0], to_refined_string_type(f.type())); +} + +/// Add axioms corresponding to the String.valueOf(D) java function +/// \param f: function application with one double argument +/// \return a new string expression +string_exprt string_constraint_generatort::add_axioms_from_double( + const function_application_exprt &f) +{ + return add_axioms_for_string_of_float( + args(f, 1)[0], to_refined_string_type(f.type())); +} + +/// Add axioms corresponding to the integer part of m, in decimal form with no +/// leading zeroes, followed by '.' ('\u002E'), followed by one or more decimal +/// digits representing the fractional part of m. This specification is correct +/// for inputs that do not exceed 100000 and the function is unspecified for +/// other values. +/// +/// TODO: this specification is not correct for negative numbers and +/// double precision +/// \param f: expression representing a float +/// \param ref_type: refined type for strings +/// \return a new string expression +string_exprt string_constraint_generatort::add_axioms_for_string_of_float( + const exprt &f, const refined_string_typet &ref_type) +{ + const floatbv_typet &type=to_floatbv_type(f.type()); + ieee_float_spect float_spec(type); + + // We will look at the first 5 digits of the fractional part. + // shifted is floor(f * 1e5) + exprt shifting=constant_float(1e5, float_spec); + exprt shifted=round_expr_to_zero(floatbv_mult(f, shifting)); + // Numbers with greater or equal value to the following, should use + // the exponent notation. + exprt max_non_exponent_notation=from_integer(100000, shifted.type()); + // fractional_part is floor(f * 100000) % 100000 + mod_exprt fractional_part(shifted, max_non_exponent_notation); + string_exprt fractional_part_str= + add_axioms_for_fractional_part(fractional_part, 6, ref_type); + + // The axiom added to convert to integer should always be satisfiable even + // when the preconditions are not satisfied. + mod_exprt integer_part(round_expr_to_zero(f), max_non_exponent_notation); + // We should not need more than 8 characters to represent the integer + // part of the float. + string_exprt integer_part_str=add_axioms_from_int(integer_part, 8, ref_type); + + return add_axioms_for_concat(integer_part_str, fractional_part_str); +} + +/// Add axioms for representing the fractional part of a floating point starting +/// with a dot +/// \param int_expr: an integer expression +/// \param max_size: a maximal size for the string, this includes the +/// potential minus sign and therefore should be greater than 2 +/// \param ref_type: a type for refined strings +/// \return a string expression +string_exprt string_constraint_generatort::add_axioms_for_fractional_part( + const exprt &int_expr, size_t max_size, const refined_string_typet &ref_type) +{ + PRECONDITION(int_expr.type().id()==ID_signedbv); + PRECONDITION(max_size>=2); + const typet &type=int_expr.type(); + string_exprt res=fresh_string(ref_type); + exprt ten=from_integer(10, type); + const typet &char_type=ref_type.get_char_type(); + const typet &index_type=ref_type.get_index_type(); + exprt zero_char=constant_char('0', char_type); + exprt nine_char=constant_char('9', char_type); + exprt max=from_integer(max_size, index_type); + + // We add axioms: + // a1 : 2 <= |res| <= max_size + // a2 : starts_with_dot && no_trailing_zero && is_number + // starts_with_dot: res[0] = '.' + // is_number: forall i:[1, max_size[. '0' < res[i] < '9' + // no_trailing_zero: forall j:[2, max_size[. !(|res| = j+1 && res[j] = '0') + // a3 : int_expr = sum_j 10^j (j < |res| ? res[j] - '0' : 0) + + and_exprt a1(res.axiom_for_is_strictly_longer_than(1), + res.axiom_for_is_shorter_than(max)); + axioms.push_back(a1); + + equal_exprt starts_with_dot(res[0], from_integer('.', char_type)); + + exprt::operandst digit_constraints; + digit_constraints.push_back(starts_with_dot); + exprt sum=from_integer(0, type); + + for(size_t j=1; j1) + { + not_exprt no_trailing_zero(and_exprt( + equal_exprt(res.length(), from_integer(j+1, res.length().type())), + equal_exprt(res[j], zero_char))); + digit_constraints.push_back(no_trailing_zero); + } + } + + exprt a2=conjunction(digit_constraints); + axioms.push_back(a2); + + equal_exprt a3(int_expr, sum); + axioms.push_back(a3); + + return res; +} + +/// Add axioms to write the float in scientific notation. +/// +/// A float is represented as $f = m * 2^e$ where $0 <= m < 2$ is the +/// significand and $-126 <= e <= 127$ is the exponent. +/// We want an alternate representation by finding $n$ and +/// $d$ such that $f=n*10^d$. We can estimate $d$ the following way: +/// $d ~= log_10(f/n) ~= log_10(m) + log_10(2) * e - log_10(n)$ +/// $d = floor(log_10(2) * e)$ +/// Then $n$ can be expressed by the equation: +/// $log_10(n) = log_10(m) + log_10(2) * e - d$ +/// $n = f / 10^d = m * 2^e / 10^d = m * 2^e / 10^(floor(log_10(2) * e))$ +/// TODO: For now we only consider single precision. +/// \param f: a float expression, which is positive +/// \param max_size: a maximal size for the string +/// \param ref_type: a type for refined strings +/// \return a string expression representing the float in scientific notation +string_exprt string_constraint_generatort:: + add_axioms_from_float_scientific_notation( + const exprt &f, const refined_string_typet &ref_type) +{ + ieee_float_spect float_spec=ieee_float_spect::single_precision(); + typet float_type=float_spec.to_type(); + signedbv_typet int_type(32); + + // This is used for rounding float to integers. + exprt round_to_zero_expr=from_integer(ieee_floatt::ROUND_TO_ZERO, int_type); + + // `bin_exponent` is $e$ in the formulas + exprt bin_exponent=get_exponent(f, float_spec); + + // $m$ from the formula is a value between 0.0 and 2.0 represented + // with values in the range 0x000000 0xFFFFFF so 1 corresponds to 0x800000. + // `bin_significand_int` represents $m * 0x800000$ + exprt bin_significand_int= + get_significand(f, float_spec, unsignedbv_typet(32)); + // `bin_significand` represents $m$ and is obtained + // by multiplying `binary_significand_as_int` by + // 1/0x800000 = 2^-23 = 1.1920928955078125 * 10^-7 + exprt bin_significand=floatbv_mult( + floatbv_typecast_exprt(bin_significand_int, round_to_zero_expr, float_type), + constant_float(1.1920928955078125e-7, float_spec)); + + // This is a first approximation of the exponent that will adjust + // if the fraction we get is greater than 10 + exprt dec_exponent_estimate=estimate_decimal_exponent(f, float_spec); + + // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[0,128] + std::vector two_power_e_over_ten_power_d_table( + { 1, 2, 4, 8, 1.6, 3.2, 6.4, 1.28, 2.56, + 5.12, 1.024, 2.048, 4.096, 8.192, 1.6384, 3.2768, 6.5536, + 1.31072, 2.62144, 5.24288, 1.04858, 2.09715, 4.19430, 8.38861, 1.67772, + 3.35544, 6.71089, 1.34218, 2.68435, 5.36871, 1.07374, 2.14748, 4.29497, + 8.58993, 1.71799, 3.43597, 6.87195, 1.37439, 2.74878, 5.49756, 1.09951, + 2.19902, 4.39805, 8.79609, 1.75922, 3.51844, 7.03687, 1.40737, 2.81475, + 5.62950, 1.12590, 2.25180, 4.50360, 9.00720, 1.80144, 3.60288, 7.20576, + 1.44115, 2.88230, 5.76461, 1.15292, 2.30584, 4.61169, 9.22337, 1.84467, + 3.68935, 7.37870, 1.47574, 2.95148, 5.90296, 1.18059, 2.36118, 4.72237, + 9.44473, 1.88895, 3.77789, 7.55579, 1.51116, 3.02231, 6.04463, 1.20893, + 2.41785, 4.83570, 9.67141, 1.93428, 3.86856, 7.73713, 1.54743, 3.09485, + 6.18970, 1.23794, 2.47588, 4.95176, 9.90352, 1.98070, 3.96141, 7.92282, + 1.58456, 3.16913, 6.33825, 1.26765, 2.53530, 5.07060, 1.01412, 2.02824, + 4.05648, 8.11296, 1.62259, 3.24519, 6.49037, 1.29807, 2.59615, 5.1923, + 1.03846, 2.07692, 4.15384, 8.30767, 1.66153, 3.32307, 6.64614, 1.32923, + 2.65846, 5.31691, 1.06338, 2.12676, 4.25353, 8.50706, 1.70141}); + + // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[-128,-1] + std::vector two_power_e_over_ten_power_d_table_negatives( + { 2.93874, 5.87747, 1.17549, 2.35099, 4.70198, 9.40395, 1.88079, 3.76158, + 7.52316, 1.50463, 3.00927, 6.01853, 1.20371, 2.40741, 4.81482, 9.62965, + 1.92593, 3.85186, 7.70372, 1.54074, 3.08149, 6.16298, 1.23260, 2.46519, + 4.93038, 9.86076, 1.97215, 3.94430, 7.88861, 1.57772, 3.15544, 6.31089, + 1.26218, 2.52435, 5.04871, 1.00974, 2.01948, 4.03897, 8.07794, 1.61559, + 3.23117, 6.46235, 1.29247, 2.58494, 5.16988, 1.03398, 2.06795, 4.13590, + 8.27181, 1.65436, 3.30872, 6.61744, 1.32349, 2.64698, 5.29396, 1.05879, + 2.11758, 4.23516, 8.47033, 1.69407, 3.38813, 6.77626, 1.35525, 2.71051, + 5.42101, 1.08420, 2.16840, 4.33681, 8.67362, 1.73472, 3.46945, 6.93889, + 1.38778, 2.77556, 5.55112, 1.11022, 2.22045, 4.44089, 8.88178, 1.77636, + 3.55271, 7.10543, 1.42109, 2.84217, 5.68434, 1.13687, 2.27374, 4.54747, + 9.09495, 1.81899, 3.63798, 7.27596, 1.45519, 2.91038, 5.82077, 1.16415, + 2.32831, 4.65661, 9.31323, 1.86265, 3.72529, 7.45058, 1.49012, 2.98023, + 5.96046, 1.19209, 2.38419, 4.76837, 9.53674, 1.90735, 3.81470, 7.62939, + 1.52588, 3.05176, 6.10352, 1.22070, 2.44141, 4.88281, 9.76563, 1.95313, + 3.90625, 7.81250, 1.56250, 3.12500, 6.25000, 1.25000, 2.50000, 5}); + + // bias_table used to find the bias factor + exprt conversion_factor_table_size=from_integer( + two_power_e_over_ten_power_d_table_negatives.size()+ + two_power_e_over_ten_power_d_table.size(), + int_type); + array_exprt conversion_factor_table( + array_typet(float_type, conversion_factor_table_size)); + for(const auto &f : two_power_e_over_ten_power_d_table_negatives) + conversion_factor_table.copy_to_operands(constant_float(f, float_spec)); + for(const auto &f : two_power_e_over_ten_power_d_table) + conversion_factor_table.copy_to_operands(constant_float(f, float_spec)); + + // The index in the table, corresponding to exponent e is e+128 + plus_exprt shifted_index(bin_exponent, from_integer(128, int_type)); + + // bias_factor is $2^e / 10^(floor(log_10(2)*e))$ that is $2^e/10^d$ + index_exprt conversion_factor( + conversion_factor_table, shifted_index, float_type); + + // `dec_significand` is $n = m * bias_factor$ + exprt dec_significand=floatbv_mult(conversion_factor, bin_significand); + exprt dec_significand_int=round_expr_to_zero(dec_significand); + + // `dec_exponent` is $d$ in the formulas + // it is obtained from the approximation, checking whether it is not too small + binary_relation_exprt estimate_too_small( + dec_significand_int, ID_ge, from_integer(10, int_type)); + if_exprt decimal_exponent( + estimate_too_small, + plus_exprt(dec_exponent_estimate, from_integer(1, int_type)), + dec_exponent_estimate); + + // `dec_significand` is divided by 10 if it exceeds 10 + dec_significand=if_exprt( + estimate_too_small, + floatbv_mult(dec_significand, constant_float(0.1, float_spec)), + dec_significand); + dec_significand_int=round_expr_to_zero(dec_significand); + + string_exprt string_expr_integer_part= + add_axioms_from_int(dec_significand_int, 3, ref_type); + minus_exprt fractional_part( + dec_significand, floatbv_of_int_expr(dec_significand_int, float_spec)); + + // shifted_float is floor(f * 1e5) + exprt shifting=constant_float(1e5, float_spec); + exprt shifted_float= + round_expr_to_zero(floatbv_mult(fractional_part, shifting)); + + // Numbers with greater or equal value to the following, should use + // the exponent notation. + exprt max_non_exponent_notation=from_integer(100000, shifted_float.type()); + + // fractional_part_shifted is floor(f * 100000) % 100000 + mod_exprt fractional_part_shifted(shifted_float, max_non_exponent_notation); + + string_exprt string_fractional_part=add_axioms_for_fractional_part( + fractional_part_shifted, 6, ref_type); + + // string_expr_with_fractional_part = + // concat(string_with_do, string_fractional_part) + string_exprt string_expr_with_fractional_part=add_axioms_for_concat( + string_expr_integer_part, string_fractional_part); + + // string_expr_with_E = concat(string_fraction, string_lit_E) + string_exprt string_expr_with_E=add_axioms_for_concat_char( + string_expr_with_fractional_part, + from_integer('E', ref_type.get_char_type())); + + // exponent_string = string_of_int(decimal_exponent) + string_exprt exponent_string=add_axioms_from_int( + decimal_exponent, 3, ref_type); + + // string_expr = concat(string_expr_with_E, exponent_string) + return add_axioms_for_concat(string_expr_with_E, exponent_string); +} + +/// Add axioms corresponding to the scientific representation of floating point +/// values +/// \param f: a function application expression +/// \return a new string expression +string_exprt string_constraint_generatort:: + add_axioms_from_float_scientific_notation( + const function_application_exprt &f) +{ + const refined_string_typet &ref_type=to_refined_string_type(f.type()); + return add_axioms_from_float_scientific_notation(args(f, 1)[0], ref_type); +} diff --git a/src/solvers/refinement/string_constraint_generator_insert.cpp b/src/solvers/refinement/string_constraint_generator_insert.cpp index 0fb39e8a658..b7a0a381bad 100644 --- a/src/solvers/refinement/string_constraint_generator_insert.cpp +++ b/src/solvers/refinement/string_constraint_generator_insert.cpp @@ -119,7 +119,7 @@ string_exprt string_constraint_generatort::add_axioms_for_insert_double( { string_exprt s1=get_string_expr(args(f, 3)[0]); const refined_string_typet &ref_type=to_refined_string_type(s1.type()); - string_exprt s2=add_axioms_from_float(args(f, 3)[2], ref_type, true); + string_exprt s2=add_axioms_for_string_of_float(args(f, 3)[2], ref_type); return add_axioms_for_insert(s1, s2, args(f, 3)[1]); } @@ -133,7 +133,7 @@ string_exprt string_constraint_generatort::add_axioms_for_insert_float( { string_exprt s1=get_string_expr(args(f, 3)[0]); const refined_string_typet &ref_type=to_refined_string_type(s1.type()); - string_exprt s2=add_axioms_from_float(args(f, 3)[2], ref_type, false); + string_exprt s2=add_axioms_for_string_of_float(args(f, 3)[2], ref_type); return add_axioms_for_insert(s1, s2, args(f, 3)[1]); } diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index df7589529be..8ac4f30f26c 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -453,7 +453,9 @@ exprt string_constraint_generatort::add_axioms_for_function_application( else if(id==ID_cprover_string_of_int_hex_func) res=add_axioms_from_int_hex(expr); else if(id==ID_cprover_string_of_float_func) - res=add_axioms_from_float(expr); + res=add_axioms_for_string_of_float(expr); + else if(id==ID_cprover_string_of_float_scientific_notation_func) + res=add_axioms_from_float_scientific_notation(expr); else if(id==ID_cprover_string_of_double_func) res=add_axioms_from_double(expr); else if(id==ID_cprover_string_of_long_func) diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index 7416bc1a341..c009dd6e412 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -12,10 +12,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// types, in particular int, long, float, double, char, bool #include -#include -/// add axioms corresponding to the String.valueOf(I) java function -/// \par parameters: function application with one integer argument +/// Add axioms corresponding to the String.valueOf(I) java function. +/// \param expr: function application with one integer argument /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_from_int( const function_application_exprt &expr) @@ -24,8 +23,8 @@ string_exprt string_constraint_generatort::add_axioms_from_int( return add_axioms_from_int(args(expr, 1)[0], MAX_INTEGER_LENGTH, ref_type); } -/// add axioms corresponding to the String.valueOf(J) java function -/// \par parameters: function application with one long argument +/// Add axioms corresponding to the String.valueOf(J) java function. +/// \param expr: function application with one long argument /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_from_long( const function_application_exprt &expr) @@ -34,125 +33,8 @@ string_exprt string_constraint_generatort::add_axioms_from_long( return add_axioms_from_int(args(expr, 1)[0], MAX_LONG_LENGTH, ref_type); } -/// add axioms corresponding to the String.valueOf(F) java function -/// \par parameters: function application with one float argument -/// \return a new string expression -string_exprt string_constraint_generatort::add_axioms_from_float( - const function_application_exprt &f) -{ - const refined_string_typet &ref_type=to_refined_string_type(f.type()); - return add_axioms_from_float(args(f, 1)[0], ref_type, false); -} - -/// add axioms corresponding to the String.valueOf(D) java function -/// \par parameters: function application with one double argument -/// \return a new string expression -string_exprt string_constraint_generatort::add_axioms_from_double( - const function_application_exprt &f) -{ - const refined_string_typet &ref_type=to_refined_string_type(f.type()); - return add_axioms_from_float(args(f, 1)[0], ref_type, true); -} - -/// add axioms corresponding to the String.valueOf(F) java function Warning: we -/// currently only have partial specification -/// \par parameters: float expression and Boolean signaling that the argument -/// has -/// double precision -/// \return a new string expression -string_exprt string_constraint_generatort::add_axioms_from_float( - const exprt &f, const refined_string_typet &ref_type, bool double_precision) -{ - string_exprt res=fresh_string(ref_type); - const typet &index_type=ref_type.get_index_type(); - const typet &char_type=ref_type.get_char_type(); - const exprt &index24=from_integer(24, index_type); - axioms.push_back(res.axiom_for_is_shorter_than(index24)); - - string_exprt magnitude=fresh_string(ref_type); - string_exprt sign_string=fresh_string(ref_type); - string_exprt nan_string=add_axioms_for_constant("NaN", ref_type); - - // We add the axioms: - // a1 : If the argument is NaN, the result length is that of "NaN". - // a2 : If the argument is NaN, the result content is the string "NaN". - // a3 : f<0 => |sign_string|=1 - // a4 : f>=0 => |sign_string|=0 - // a5 : f<0 => sign_string[0]='-' - // a6 : f infinite => |magnitude|=|"Infinity"| - // a7 : forall i<|"Infinity"|, f infinite => magnitude[i]="Infinity"[i] - // a8 : f=0 => |magnitude|=|"0.0"| - // a9 : forall i<|"0.0"|, f=0 => f[i]="0.0"[i] - - ieee_float_spect fspec= - double_precision?ieee_float_spect::double_precision() - :ieee_float_spect::single_precision(); - - exprt isnan=float_bvt().isnan(f, fspec); - implies_exprt a1(isnan, magnitude.axiom_for_has_same_length_as(nan_string)); - axioms.push_back(a1); - - symbol_exprt qvar=fresh_univ_index("QA_equal_nan", index_type); - string_constraintt a2( - qvar, - nan_string.length(), - isnan, - equal_exprt(magnitude[qvar], nan_string[qvar])); - axioms.push_back(a2); - - // If the argument is not NaN, the result is a string that represents - // the sign and magnitude (absolute value) of the argument. - // If the sign is negative, the first character of the result is '-'; - // if the sign is positive, no sign character appears in the result. - - bitvector_typet bv_type=to_bitvector_type(f.type()); - unsigned width=bv_type.get_width(); - exprt isneg=extractbit_exprt(f, width-1); - - implies_exprt a3(isneg, sign_string.axiom_for_has_length(1)); - axioms.push_back(a3); - - implies_exprt a4(not_exprt(isneg), sign_string.axiom_for_has_length(0)); - axioms.push_back(a4); - - implies_exprt a5( - isneg, equal_exprt(sign_string[0], constant_char('-', char_type))); - axioms.push_back(a5); - - // If m is infinity, it is represented by the characters "Infinity"; - // thus, positive infinity produces the result "Infinity" and negative - // infinity produces the result "-Infinity". - - string_exprt infinity_string=add_axioms_for_constant("Infinity", ref_type); - exprt isinf=float_bvt().isinf(f, fspec); - implies_exprt a6( - isinf, magnitude.axiom_for_has_same_length_as(infinity_string)); - axioms.push_back(a6); - - symbol_exprt qvar_inf=fresh_univ_index("QA_equal_infinity", index_type); - equal_exprt meq(magnitude[qvar_inf], infinity_string[qvar_inf]); - string_constraintt a7(qvar_inf, infinity_string.length(), isinf, meq); - axioms.push_back(a7); - - // If m is zero, it is represented by the characters "0.0"; thus, negative - // zero produces the result "-0.0" and positive zero produces "0.0". - - string_exprt zero_string=add_axioms_for_constant("0.0", ref_type); - exprt iszero=float_bvt().is_zero(f, fspec); - implies_exprt a8(iszero, magnitude.axiom_for_has_same_length_as(zero_string)); - axioms.push_back(a8); - - symbol_exprt qvar_zero=fresh_univ_index("QA_equal_zero", index_type); - equal_exprt eq_zero(magnitude[qvar_zero], zero_string[qvar_zero]); - string_constraintt a9(qvar_zero, zero_string.length(), iszero, eq_zero); - axioms.push_back(a9); - - return add_axioms_for_concat(sign_string, magnitude); -} - - -/// add axioms corresponding to the String.valueOf(Z) java function -/// \par parameters: function application with on Boolean argument +/// Add axioms corresponding to the String.valueOf(Z) java function. +/// \param f: function application with a Boolean argument /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_from_bool( const function_application_exprt &f) @@ -161,10 +43,10 @@ string_exprt string_constraint_generatort::add_axioms_from_bool( return add_axioms_from_bool(args(f, 1)[0], ref_type); } - -/// add axioms stating that the returned string equals "true" when the Boolean -/// expression is true and "false" when it is false -/// \par parameters: Boolean expression +/// Add axioms stating that the returned string equals "true" when the Boolean +/// expression is true and "false" when it is false. +/// \param b: Boolean expression +/// \param ref_type: type of refined string expressions /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_from_bool( const exprt &b, const refined_string_typet &ref_type) @@ -207,8 +89,9 @@ string_exprt string_constraint_generatort::add_axioms_from_bool( return res; } -/// add axioms to say the string corresponds to the result of String.valueOf(I) -/// or String.valueOf(J) java functions applied on the integer expression +/// Add axioms enforcing that the string corresponds to the result +/// of String.valueOf(I) or String.valueOf(J) Java functions applied +/// on the integer expression. /// \param i: a signed integer expression /// \param max_size: a maximal size for the string representation /// \param ref_type: type for refined strings @@ -329,8 +212,8 @@ string_exprt string_constraint_generatort::add_axioms_from_int( return res; } -/// returns the value represented by the character -/// \par parameters: a character expression in the following set: +/// Returns the integer value represented by the character. +/// \param chr: a character expression in the following set: /// 0123456789abcdef /// \return an integer expression exprt string_constraint_generatort::int_of_hex_char(const exprt &chr) const @@ -344,9 +227,10 @@ exprt string_constraint_generatort::int_of_hex_char(const exprt &chr) const minus_exprt(chr, zero_char)); } -/// add axioms stating that the returned string corresponds to the integer -/// argument written in hexadecimal -/// \par parameters: one integer argument +/// Add axioms stating that the returned string corresponds to the integer +/// argument written in hexadecimal. +/// \param i: an integer argument +/// \param ref_type: type of refined string expressions /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_from_int_hex( const exprt &i, const refined_string_typet &ref_type) @@ -402,7 +286,7 @@ string_exprt string_constraint_generatort::add_axioms_from_int_hex( } /// add axioms corresponding to the Integer.toHexString(I) java function -/// \par parameters: function application with integer argument +/// \param f: function application with an integer argument /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_from_int_hex( const function_application_exprt &f) @@ -411,8 +295,8 @@ string_exprt string_constraint_generatort::add_axioms_from_int_hex( return add_axioms_from_int_hex(args(f, 1)[0], ref_type); } -/// add axioms corresponding to the String.valueOf(C) java function -/// \par parameters: function application one char argument +/// Add axioms corresponding to the String.valueOf(C) java function. +/// \param f: function application one char argument /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_from_char( const function_application_exprt &f) @@ -421,9 +305,10 @@ string_exprt string_constraint_generatort::add_axioms_from_char( return add_axioms_from_char(args(f, 1)[0], ref_type); } -/// add axioms stating that the returned string has length 1 and the character -/// it contains correspond to the input expression -/// \par parameters: one expression of type char +/// Add axioms stating that the returned string has length 1 and the character +/// it contains corresponds to the input expression. +/// \param c: one expression of type char +/// \param ref_type: type of refined string expressions /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_from_char( const exprt &c, const refined_string_typet &ref_type) @@ -434,9 +319,9 @@ string_exprt string_constraint_generatort::add_axioms_from_char( return res; } -/// add axioms corresponding to the String.valueOf([C) and String.valueOf([CII) -/// functions -/// \par parameters: function application with one or three arguments +/// Add axioms corresponding to the String.valueOf([C) and String.valueOf([CII) +/// functions. +/// \param f: function application with one or three arguments /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_for_value_of( const function_application_exprt &f) @@ -471,9 +356,9 @@ string_exprt string_constraint_generatort::add_axioms_for_value_of( } } -/// add axioms making the return value true if the given string is a correct -/// number -/// \par parameters: function application with one string expression +/// Add axioms making the return value true if the given string is a correct +/// number. +/// \param f: function application with one string expression /// \return an boolean expression exprt string_constraint_generatort::add_axioms_for_correct_number_format( const string_exprt &str, std::size_t max_size) @@ -527,7 +412,7 @@ exprt string_constraint_generatort::add_axioms_for_correct_number_format( } /// add axioms corresponding to the Integer.parseInt java function -/// \par parameters: function application with one string expression +/// \param f: function application with one string expression /// \return an integer expression exprt string_constraint_generatort::add_axioms_for_parse_int( const function_application_exprt &f) diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 38b8783ee8e..8a22f226fc0 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -797,6 +797,7 @@ IREP_ID_ONE(cprover_string_of_int_hex_func) IREP_ID_ONE(cprover_string_of_long_func) IREP_ID_ONE(cprover_string_of_bool_func) IREP_ID_ONE(cprover_string_of_float_func) +IREP_ID_ONE(cprover_string_of_float_scientific_notation_func) IREP_ID_ONE(cprover_string_of_double_func) IREP_ID_ONE(cprover_string_of_char_func) IREP_ID_ONE(cprover_string_of_char_array_func) diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 69a03bdfa9c..0d64ede33c6 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -1790,9 +1790,8 @@ class floatbv_typecast_exprt:public binary_exprt floatbv_typecast_exprt( const exprt &op, const exprt &rounding, - const typet &_type):binary_exprt(ID_floatbv_typecast, _type) + const typet &_type):binary_exprt(op, ID_floatbv_typecast, rounding, _type) { - copy_to_operands(op, rounding); } exprt &op()