Add builtin support for string_of_int

Author: romainbrenguier

src/solvers/refinement/string_builtin_function.cpp

@@ -222,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_refinement_util.cpp

@@ -224,6 +224,10 @@ static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
     return util_make_unique<string_concat_char_builtin_functiont>(
       return_code, fun_app.arguments(), array_pool);
 
+  if(id == ID_cprover_string_of_int_func)
+    return util_make_unique<string_of_int_builtin_functiont>(
+      return_code, fun_app.arguments(), array_pool);
+
   return util_make_unique<string_builtin_function_with_no_evalt>(
     return_code, fun_app, array_pool);
 }