Add builtin support for string_set_char

Author: romainbrenguier

src/solvers/refinement/string_builtin_function.cpp

@@ -156,6 +156,37 @@ optionalt<exprt> string_concat_char_builtin_functiont::eval(
   return make_string(input_opt.value(), type);
 }
 
+optionalt<exprt> string_set_char_builtin_functiont::eval(
+  const std::function<exprt(const exprt &)> &get_value) const
+{
+  auto input_opt = eval_string(input, get_value);
+  const auto char_opt = numeric_cast<mp_integer>(get_value(character));
+  const auto position_opt = numeric_cast<mp_integer>(get_value(position));
+  if(!input_opt || !char_opt || !position_opt)
+    return {};
+  if(0 <= *position_opt && *position_opt < input_opt.value().size())
+    input_opt.value()[*position_opt] = *char_opt;
+  const auto length =
+    from_integer(input_opt.value().size(), result.length().type());
+  const array_typet type(result.type().subtype(), length);
+  return make_string(input_opt.value(), type);
+}
+
+exprt string_set_char_builtin_functiont::length_constraint() const
+{
+  const exprt out_of_bounds = or_exprt(
+    binary_relation_exprt(position, ID_ge, input.length()),
+    binary_relation_exprt(
+      position, ID_le, from_integer(0, input.length().type())));
+  const exprt return_value = if_exprt(
+    out_of_bounds,
+    from_integer(1, return_code.type()),
+    from_integer(0, return_code.type()));
+  return and_exprt(
+    equal_exprt(result.length(), input.length()),
+    equal_exprt(return_code, return_value));
+}
+
 std::vector<mp_integer> string_insertion_builtin_functiont::eval(
   const std::vector<mp_integer> &input1_value,
   const std::vector<mp_integer> &input2_value,

src/solvers/refinement/string_builtin_function.h

@@ -135,6 +135,48 @@ class string_concat_char_builtin_functiont
   }
 };
 
+/// Setting a character at a particular position of a string
+class string_set_char_builtin_functiont
+  : public string_transformation_builtin_functiont
+{
+public:
+  exprt position;
+  exprt character;
+
+  /// 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]`,
+  /// a string `arg1` of type refined_string_typet, a position and a character.
+  string_set_char_builtin_functiont(
+    const exprt &return_code,
+    const std::vector<exprt> &fun_args,
+    array_poolt &array_pool)
+    : string_transformation_builtin_functiont(return_code, fun_args, array_pool)
+  {
+    PRECONDITION(fun_args.size() == 5);
+    position = fun_args[3];
+    character = fun_args[4];
+  }
+
+  optionalt<exprt>
+  eval(const std::function<exprt(const exprt &)> &get_value) const override;
+
+  std::string name() const override
+  {
+    return "set_char";
+  }
+
+  exprt add_constraints(string_constraint_generatort &generator) const override
+  {
+    return generator.add_axioms_for_set_char(
+      result, input, position, character);
+  }
+
+  // \todo: length_constraint is not the best possible name because we also
+  // \todo: add constraint about the return code
+  exprt length_constraint() const override;
+};
+
 /// String inserting a string into another one
 class string_insertion_builtin_functiont : public string_builtin_functiont
 {

src/solvers/refinement/string_refinement_util.cpp

@@ -228,6 +228,10 @@ static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
     return util_make_unique<string_of_int_builtin_functiont>(
       return_code, fun_app.arguments(), array_pool);
 
+  if(id == ID_cprover_string_char_set_func)
+    return util_make_unique<string_set_char_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);
 }