Conversion between string and float moved into a new file

We remove the add_axioms_from_float that was defined in
string_constraint_generator_valueof.cpp and use the new one from
string_constraint_generator_float.cpp instead.

We add string_constraint_generator_float.cpp to Makefile

We also define an helper method for concatenation of char which can be
used in float conversion.

Improved documentation in string_constraint_generator_valueof
and in string_constraint_generator_concat.

Author: romainbrenguier

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 \

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);
@@ -236,9 +238,14 @@ class string_constraint_generatort
   // 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);
+    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

src/solvers/refinement/string_constraint_generator_concat.cpp

@@ -148,9 +148,22 @@ 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 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

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_from_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_from_float(args(f, 3)[2], ref_type);
   return add_axioms_for_insert(s1, s2, args(f, 3)[1]);
 }
 

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -454,6 +454,8 @@ exprt string_constraint_generatort::add_axioms_for_function_application(
     res=add_axioms_from_int_hex(expr);
   else if(id==ID_cprover_string_of_float_func)
     res=add_axioms_from_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)

src/solvers/refinement/string_constraint_generator_valueof.cpp

@@ -12,10 +12,9 @@ Author: Romain Brenguier, [email protected]
 ///   types, in particular int, long, float, double, char, bool
 
 #include <solvers/refinement/string_constraint_generator.h>
-#include <solvers/floatbv/float_bv.h>
 
-/// 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)
@@ -329,8 +211,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 +226,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 +285,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 +294,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 +304,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 correspond 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 +318,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 +355,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 +411,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)