Merge pull request #2664 from romainbrenguier/feature/extend-builtin-functions-part2

Extend builtin functions for string_set_char

Author: Daniel Kroening

jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.class

@@ -0,0 +1,62 @@
+public class Test {
+    public String det()
+    {
+        StringBuilder builder = new StringBuilder("abcdefghijklmnopqrstuvwxyz");
+        builder.setCharAt(3, '!');
+        builder.setCharAt(5, '!');
+        builder.setCharAt(7, '!');
+        builder.setCharAt(9, '!');
+        builder.setCharAt(13, '!');
+        builder.setCharAt(15, '!');
+        builder.setCharAt(17, '!');
+        builder.setCharAt(19, '!');
+        builder.setCharAt(4, ':');
+        builder.setCharAt(5, ':');
+        builder.setCharAt(6, ':');
+        builder.setCharAt(9, ':');
+        builder.setCharAt(10, ':');
+        builder.setCharAt(11, ':');
+        builder.setCharAt(16, ':');
+        builder.setCharAt(18, ':');
+        return builder.toString();
+    }
+
+    public String nonDet(String s, char c, int i)
+    {
+        StringBuilder builder = new StringBuilder(s);
+        if(i + 5 >= s.length() || 19 >= s.length() || i < 0)
+            return "Out of bounds";
+        builder.setCharAt(i, c);
+        builder.setCharAt(i+5, 'x');
+        builder.setCharAt(7, '!');
+        builder.setCharAt(9, '!');
+        builder.setCharAt(13, '!');
+        builder.setCharAt(15, '!');
+        builder.setCharAt(17, '!');
+        builder.setCharAt(19, '!');
+        builder.setCharAt(4, ':');
+        builder.setCharAt(5, ':');
+        builder.setCharAt(6, c);
+        builder.setCharAt(9, ':');
+        builder.setCharAt(10, ':');
+        builder.setCharAt(11, ':');
+        builder.setCharAt(16, ':');
+        builder.setCharAt(18, ':');
+        return builder.toString();
+    }
+
+    public String withDependency(boolean b)
+    {
+        StringBuilder builder = new StringBuilder("abcdefghijklmnopqrstuvwxyz");
+        builder.setCharAt(3, '!');
+        builder.setCharAt(5, '!');
+
+        if(b) {
+            assert builder.toString().startsWith("abc!");
+        } else {
+            assert !builder.toString().startsWith("abc!");
+        }
+        return builder.toString();
+    }
+
+}

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

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.withDependency --max-nondet-string-length 1000
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 55 .*: SUCCESS
+assertion at file Test.java line 57 .*: FAILURE
+--
+--
+Check that when a dependency is present, the correct constraints are added
+
+

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

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

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

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

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

@@ -29,33 +29,6 @@ string_transformation_builtin_functiont::
   const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
   input = array_pool.find(arg1.op1(), arg1.op0());
   result = array_pool.find(fun_args[1], fun_args[0]);
-  args.insert(args.end(), fun_args.begin() + 3, fun_args.end());
-}
-
-optionalt<exprt> string_transformation_builtin_functiont::eval(
-  const std::function<exprt(const exprt &)> &get_value) const
-{
-  const auto &input_value = eval_string(input, get_value);
-  if(!input_value.has_value())
-    return {};
-
-  std::vector<mp_integer> arg_values;
-  const auto &insert = std::back_inserter(arg_values);
-  const mp_integer unknown('?');
-  std::transform(
-    args.begin(), args.end(), insert, [&](const exprt &e) { // NOLINT
-      if(const auto val = numeric_cast<mp_integer>(get_value(e)))
-        return *val;
-      INVARIANT(
-        get_value(e).id() == ID_unknown,
-        "array valuation should only contain constants and unknown");
-      return unknown;
-    });
-
-  const auto result_value = eval(*input_value, arg_values);
-  const auto length = from_integer(result_value.size(), result.length().type());
-  const array_typet type(result.type().subtype(), length);
-  return make_string(result_value, type);
 }
 
 string_insertion_builtin_functiont::string_insertion_builtin_functiont(
@@ -162,14 +135,56 @@ std::vector<mp_integer> string_concatenation_builtin_functiont::eval(
   return result;
 }
 
-std::vector<mp_integer> string_concat_char_builtin_functiont::eval(
-  const std::vector<mp_integer> &input_value,
-  const std::vector<mp_integer> &args_value) const
+optionalt<exprt> string_concat_char_builtin_functiont::eval(
+  const std::function<exprt(const exprt &)> &get_value) const
 {
-  PRECONDITION(args_value.size() == 1);
-  std::vector<mp_integer> result(input_value);
-  result.push_back(args_value[0]);
-  return result;
+  auto input_opt = eval_string(input, get_value);
+  if(!input_opt.has_value())
+    return {};
+  const mp_integer char_val = [&] {
+    if(const auto val = numeric_cast<mp_integer>(get_value(character)))
+      return *val;
+    INVARIANT(
+      get_value(character).id() == ID_unknown,
+      "character valuation should only contain constants and unknown");
+    return mp_integer(CHARACTER_FOR_UNKNOWN);
+  }();
+  input_opt.value().push_back(char_val);
+  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);
+}
+
+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()[numeric_cast_v<std::size_t>(*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(

src/solvers/refinement/string_builtin_function.cpp

@@ -11,6 +11,8 @@
 
 class array_poolt;
 
+#define CHARACTER_FOR_UNKNOWN '?'
+
 /// Base class for string functions that are built in the solver
 class string_builtin_functiont
 {
@@ -68,7 +70,6 @@ class string_transformation_builtin_functiont : public string_builtin_functiont
 public:
   array_string_exprt result;
   array_string_exprt input;
-  std::vector<exprt> args;
 
   /// Constructor from arguments of a function application.
   /// The arguments in `fun_args` should be in order:
@@ -88,15 +89,6 @@ class string_transformation_builtin_functiont : public string_builtin_functiont
   {
     return {input};
   }
-
-  /// Evaluate the result from a concrete valuation of the arguments
-  virtual std::vector<mp_integer> eval(
-    const std::vector<mp_integer> &input_value,
-    const std::vector<mp_integer> &args_value) const = 0;
-
-  optionalt<exprt>
-  eval(const std::function<exprt(const exprt &)> &get_value) const override;
-
   bool maybe_testing_function() const override
   {
     return false;
@@ -108,6 +100,8 @@ class string_concat_char_builtin_functiont
   : public string_transformation_builtin_functiont
 {
 public:
+  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]`,
@@ -118,11 +112,12 @@ class string_concat_char_builtin_functiont
     array_poolt &array_pool)
     : string_transformation_builtin_functiont(return_code, fun_args, array_pool)
   {
+    PRECONDITION(fun_args.size() == 4);
+    character = fun_args[3];
   }
 
-  std::vector<mp_integer> eval(
-    const std::vector<mp_integer> &input_value,
-    const std::vector<mp_integer> &args_value) const override;
+  optionalt<exprt>
+  eval(const std::function<exprt(const exprt &)> &get_value) const override;
 
   std::string name() const override
   {
@@ -131,7 +126,7 @@ class string_concat_char_builtin_functiont
 
   exprt add_constraints(string_constraint_generatort &generator) const override
   {
-    return generator.add_axioms_for_concat_char(result, input, args[0]);
+    return generator.add_axioms_for_concat_char(result, input, character);
   }
 
   exprt length_constraint() const override
@@ -140,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_builtin_function.h

@@ -170,6 +170,11 @@ class string_constraint_generatort final
     const exprt &input_int,
     const exprt &radix,
     size_t max_size = 0);
+  exprt add_axioms_for_set_char(
+    const array_string_exprt &res,
+    const array_string_exprt &str,
+    const exprt &position,
+    const exprt &character);
 
 private:
   symbol_exprt fresh_boolean(const irep_idt &prefix);