[TG-2892] Add builtin function class for string_of_int

jbmc/regression/jbmc-strings/StringValueOfInt/Test.java

@@ -0,0 +1,68 @@
+public class Test
+{
+    public static String checkDet()
+    {
+        String tmp = String.valueOf(1000000);
+        tmp = String.valueOf(1000001);
+        tmp = String.valueOf(1000002);
+        tmp = String.valueOf(1000003);
+        tmp = String.valueOf(1000004);
+        tmp = String.valueOf(1000005);
+        tmp = String.valueOf(-1000001);
+        tmp = String.valueOf(-1000002);
+        tmp = String.valueOf(-1000003);
+        tmp = String.valueOf(1000004);
+        tmp = String.valueOf(1000005);
+        tmp = String.valueOf(-1000001);
+        tmp = String.valueOf(-1000002);
+        tmp = String.valueOf(1000003);
+        tmp = String.valueOf(1000004);
+        tmp = String.valueOf(1000005);
+        tmp = String.valueOf(1000001);
+        tmp = String.valueOf(-1000002);
+        tmp = String.valueOf(-1000003);
+        tmp = String.valueOf(1000004);
+        tmp = String.valueOf(1000005);
+        return tmp;
+    }
+
+    public static String checkNonDet(int i)
+    {
+        String tmp = String.valueOf(1000000);
+        tmp = String.valueOf(i + 1);
+        tmp = String.valueOf(i + 2);
+        tmp = String.valueOf(i + 3);
+        tmp = String.valueOf(i + 4);
+        tmp = String.valueOf(i + 5);
+        tmp = String.valueOf(i - 1);
+        tmp = String.valueOf(i - 2);
+        tmp = String.valueOf(i - 3);
+        tmp = String.valueOf(i - 4);
+        tmp = String.valueOf(i - 5);
+        tmp += " ";
+        tmp += String.valueOf(i);
+        tmp += " ";
+        tmp += String.valueOf(i + 2);
+        tmp += " ";
+        tmp += String.valueOf(i + 3);
+        tmp += " ";
+        tmp += String.valueOf(-i);
+        tmp += " ";
+        tmp += String.valueOf(-i + 1);
+        tmp += " ";
+        tmp += String.valueOf(-i - 2);
+        return tmp;
+    }
+
+    public static void checkWithDependency(boolean b)
+    {
+        String s = String.valueOf(12);
+        if (b) {
+            assert(s.startsWith("12"));
+        }
+        else {
+            assert(!s.startsWith("12"));
+        }
+    }
+
+}

jbmc/regression/jbmc-strings/StringValueOfInt/test_dependency.desc

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.checkWithDependency --depth 10000
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 61 .*: SUCCESS
+assertion at file Test.java line 64 .*: FAILURE
+--
+--
+Check that when a dependency is present, the correct constraints are added

jbmc/regression/jbmc-strings/StringValueOfInt/test_det.desc

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.checkDet --verbosity 10 --cover location
+^EXIT=0$
+^SIGNAL=0$
+coverage.* file Test.java line 25 .*: SATISFIED
+--
+adding lemma .*nondet_infinite_array
+--
+Check that using the string dependence informations, no lemma involving arrays is added

jbmc/regression/jbmc-strings/StringValueOfInt/test_nondet.desc

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.checkNonDet --verbosity 10 --cover location
+^EXIT=0$
+^SIGNAL=0$
+coverage.* file Test.java line 53 .*: SATISFIED
+--
+adding lemma .*nondet_infinite_array
+--
+Check that using the string dependence informations, no lemma involving arrays is added

src/solvers/README.md

@@ -281,7 +281,7 @@ allocates a new string before calling a primitive.
     \link string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f) More... \endlink
   * `cprover_string_of_int` :
     \copybrief string_constraint_generatort::add_axioms_from_int(const function_application_exprt &f)
-    \link string_constraint_generatort::add_axioms_from_int(const function_application_exprt &f) More... \endlink
+    \link string_constraint_generatort::add_axioms_for_string_of_int(const function_application_exprt &f) More... \endlink
   * `cprover_string_of_float` :
     \copybrief string_constraint_generatort::add_axioms_for_string_of_float(const function_application_exprt &f)
     \link string_constraint_generatort::add_axioms_for_string_of_float(const function_application_exprt &f) More... \endlink

src/solvers/refinement/string_builtin_function.cpp

@@ -122,19 +122,25 @@ optionalt<std::vector<mp_integer>> eval_string(
   return result;
 }
 
-array_string_exprt
-make_string(const std::vector<mp_integer> &array, const array_typet &array_type)
+template <typename Iter>
+static array_string_exprt
+make_string(Iter begin, Iter end, const array_typet &array_type)
 {
   const typet &char_type = array_type.subtype();
   array_exprt array_expr(array_type);
   const auto &insert = std::back_inserter(array_expr.operands());
-  std::transform(
-    array.begin(), array.end(), insert, [&](const mp_integer &i) { // NOLINT
-      return from_integer(i, char_type);
-    });
+  std::transform(begin, end, insert, [&](const mp_integer &i) {
+    return from_integer(i, char_type);
+  });
   return to_array_string_expr(array_expr);
 }
 
+static array_string_exprt
+make_string(const std::vector<mp_integer> &array, const array_typet &array_type)
+{
+  return make_string(array.begin(), array.end(), array_type);
+}
+
 std::vector<mp_integer> string_concatenation_builtin_functiont::eval(
   const std::vector<mp_integer> &input1_value,
   const std::vector<mp_integer> &input2_value,
@@ -216,6 +222,84 @@ optionalt<exprt> string_insertion_builtin_functiont::eval(
   return make_string(result_value, type);
 }
 
+/// Constructor from arguments of a function application.
+/// The arguments in `fun_args` should be in order:
+/// an integer `result.length`, a character pointer `&result[0]`,
+/// an expression `arg` which is to be converted to a string.
+/// Other arguments are ignored by this constructor.
+string_creation_builtin_functiont::string_creation_builtin_functiont(
+  const exprt &return_code,
+  const std::vector<exprt> &fun_args,
+  array_poolt &array_pool)
+  : string_builtin_functiont(return_code)
+{
+  PRECONDITION(fun_args.size() >= 3);
+  result = array_pool.find(fun_args[1], fun_args[0]);
+  arg = fun_args[2];
+}
+
+optionalt<exprt> string_of_int_builtin_functiont::eval(
+  const std::function<exprt(const exprt &)> &get_value) const
+{
+  const auto arg_value = numeric_cast<mp_integer>(get_value(arg));
+  if(!arg_value)
+    return {};
+  static std::string digits = "0123456789abcdefghijklmnopqrstuvwxyz";
+  const auto radix_value = numeric_cast<mp_integer>(get_value(radix));
+  if(!radix_value || *radix_value > digits.length())
+    return {};
+
+  mp_integer current_value = *arg_value;
+  std::vector<mp_integer> right_to_left_characters;
+  if(current_value < 0)
+    current_value = -current_value;
+  if(current_value == 0)
+    right_to_left_characters.emplace_back('0');
+  while(current_value > 0)
+  {
+    const auto digit_value = (current_value % *radix_value).to_ulong();
+    right_to_left_characters.emplace_back(digits.at(digit_value));
+    current_value /= *radix_value;
+  }
+  if(*arg_value < 0)
+    right_to_left_characters.emplace_back('-');
+
+  const auto length = right_to_left_characters.size();
+  const auto length_expr = from_integer(length, result.length().type());
+  const array_typet type(result.type().subtype(), length_expr);
+  return make_string(
+    right_to_left_characters.rbegin(), right_to_left_characters.rend(), type);
+}
+
+exprt string_of_int_builtin_functiont::length_constraint() const
+{
+  const typet &type = result.length().type();
+  const auto radix_opt = numeric_cast<std::size_t>(radix);
+  const auto radix_value = radix_opt.has_value() ? radix_opt.value() : 2;
+  const std::size_t upper_bound =
+    max_printed_string_length(arg.type(), radix_value);
+  const exprt negative_arg =
+    binary_relation_exprt(arg, ID_le, from_integer(0, type));
+  const exprt absolute_arg =
+    if_exprt(negative_arg, unary_minus_exprt(arg), arg);
+
+  exprt size_expr = from_integer(1, type);
+  exprt min_int_with_current_size = from_integer(1, radix.type());
+  for(std::size_t current_size = 2; current_size <= upper_bound + 1;
+      ++current_size)
+  {
+    min_int_with_current_size = mult_exprt(radix, min_int_with_current_size);
+    const exprt at_least_current_size =
+      binary_relation_exprt(absolute_arg, ID_ge, min_int_with_current_size);
+    size_expr = if_exprt(
+      at_least_current_size, from_integer(current_size, type), size_expr);
+  }
+
+  const exprt size_expr_with_sign = if_exprt(
+    negative_arg, plus_exprt(size_expr, from_integer(1, type)), size_expr);
+  return equal_exprt(result.length(), size_expr_with_sign);
+}
+
 string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt(
   const exprt &return_code,
   const function_application_exprt &f,

src/solvers/refinement/string_builtin_function.h

@@ -264,8 +264,12 @@ class string_creation_builtin_functiont : public string_builtin_functiont
 {
 public:
   array_string_exprt result;
-  std::vector<exprt> args;
-  exprt return_code;
+  exprt arg;
+
+  string_creation_builtin_functiont(
+    const exprt &return_code,
+    const std::vector<exprt> &fun_args,
+    array_poolt &array_pool);
 
   optionalt<array_string_exprt> string_result() const override
   {
@@ -278,6 +282,43 @@ class string_creation_builtin_functiont : public string_builtin_functiont
   }
 };
 
+/// String creation from integer types
+class string_of_int_builtin_functiont : public string_creation_builtin_functiont
+{
+public:
+  string_of_int_builtin_functiont(
+    const exprt &return_code,
+    const std::vector<exprt> &fun_args,
+    array_poolt &array_pool)
+    : string_creation_builtin_functiont(return_code, fun_args, array_pool)
+  {
+    PRECONDITION(fun_args.size() <= 4);
+    if(fun_args.size() == 4)
+      radix = fun_args[3];
+    else
+      radix = from_integer(10, arg.type());
+  };
+
+  optionalt<exprt>
+  eval(const std::function<exprt(const exprt &)> &get_value) const override;
+
+  std::string name() const override
+  {
+    return "string_of_int";
+  }
+
+  exprt add_constraints(string_constraint_generatort &generator) const override
+  {
+    return generator.add_axioms_for_string_of_int_with_radix(
+      result, arg, radix);
+  }
+
+  exprt length_constraint() const override;
+
+private:
+  exprt radix;
+};
+
 /// String test
 class string_test_builtin_functiont : public string_builtin_functiont
 {

src/solvers/refinement/string_constraint_generator.h

@@ -165,6 +165,11 @@ class string_constraint_generatort final
     const array_string_exprt &s1,
     const array_string_exprt &s2,
     const exprt &offset);
+  exprt add_axioms_for_string_of_int_with_radix(
+    const array_string_exprt &res,
+    const exprt &input_int,
+    const exprt &radix,
+    size_t max_size = 0);
 
 private:
   symbol_exprt fresh_boolean(const irep_idt &prefix);
@@ -258,15 +263,10 @@ class string_constraint_generatort final
     const exprt &guard);
   exprt add_axioms_from_literal(const function_application_exprt &f);
   exprt add_axioms_from_int(const function_application_exprt &f);
-  exprt add_axioms_from_int(
+  exprt add_axioms_for_string_of_int(
     const array_string_exprt &res,
     const exprt &input_int,
     size_t max_size = 0);
-  exprt add_axioms_from_int_with_radix(
-    const array_string_exprt &res,
-    const exprt &input_int,
-    const exprt &radix,
-    size_t max_size = 0);
   exprt add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i);
   exprt add_axioms_from_int_hex(const function_application_exprt &f);
   exprt add_axioms_from_long(const function_application_exprt &f);

src/solvers/refinement/string_constraint_generator_float.cpp

@@ -214,7 +214,7 @@ exprt string_constraint_generatort::add_axioms_for_string_of_float(
   const array_string_exprt integer_part_str =
     fresh_string(index_type, char_type);
   const exprt return_code2 =
-    add_axioms_from_int(integer_part_str, integer_part, 8);
+    add_axioms_for_string_of_int(integer_part_str, integer_part, 8);
 
   return add_axioms_for_concat(res, integer_part_str, fractional_part_str);
 }
@@ -423,8 +423,8 @@ exprt string_constraint_generatort::add_axioms_from_float_scientific_notation(
 
   array_string_exprt string_expr_integer_part =
     fresh_string(index_type, char_type);
-  exprt return_code1 =
-    add_axioms_from_int(string_expr_integer_part, dec_significand_int, 3);
+  exprt return_code1 = add_axioms_for_string_of_int(
+    string_expr_integer_part, dec_significand_int, 3);
   minus_exprt fractional_part(
     dec_significand, floatbv_of_int_expr(dec_significand_int, float_spec));
 
@@ -467,7 +467,7 @@ exprt string_constraint_generatort::add_axioms_from_float_scientific_notation(
   const array_string_exprt exponent_string =
     fresh_string(index_type, char_type);
   const exprt return_code6 =
-    add_axioms_from_int(exponent_string, decimal_exponent, 3);
+    add_axioms_for_string_of_int(exponent_string, decimal_exponent, 3);
 
   // string_expr = concat(string_expr_with_E, exponent_string)
   return add_axioms_for_concat(res, string_expr_with_E, exponent_string);

src/solvers/refinement/string_constraint_generator_format.cpp

@@ -269,7 +269,7 @@ string_constraint_generatort::add_axioms_for_format_specifier(
   {
   case format_specifiert::DECIMAL_INTEGER:
     return_code =
-      add_axioms_from_int(res, get_component_in_struct(arg, ID_int));
+      add_axioms_for_string_of_int(res, get_component_in_struct(arg, ID_int));
     return res;
   case format_specifiert::HEXADECIMAL_INTEGER:
     return_code =
@@ -293,8 +293,8 @@ string_constraint_generatort::add_axioms_for_format_specifier(
   case format_specifiert::STRING:
     return get_string_expr(get_component_in_struct(arg, "string_expr"));
   case format_specifiert::HASHCODE:
-    return_code =
-      add_axioms_from_int(res, get_component_in_struct(arg, "hashcode"));
+    return_code = add_axioms_for_string_of_int(
+      res, get_component_in_struct(arg, "hashcode"));
     return res;
   case format_specifiert::LINE_SEPARATOR:
     // TODO: the constant should depend on the system: System.lineSeparator()

src/solvers/refinement/string_constraint_generator_insert.cpp

@@ -144,7 +144,7 @@ exprt string_constraint_generatort::add_axioms_for_insert_int(
   const typet &index_type = s1.length().type();
   const typet &char_type = s1.content().type().subtype();
   array_string_exprt s2 = fresh_string(index_type, char_type);
-  exprt return_code = add_axioms_from_int(s2, f.arguments()[4]);
+  exprt return_code = add_axioms_for_string_of_int(s2, f.arguments()[4]);
   return add_axioms_for_insert(res, s1, s2, offset);
 }