Merge pull request #1947 from romainbrenguier/dependency-graph/stop-adding-unecessary-constraints#TG-2608

[TG-2608] Use string dependencies to reduce the number of constraints

Author: romainbrenguier

regression/jbmc-strings/StringDependencies/Test.class

@@ -0,0 +1,22 @@
+class Test {
+    void test(String s) {
+        // Filter
+        if(s == null)
+            return;
+
+        // Act
+
+        // this matters for the final test
+        String t = s.concat("_foo");
+
+        // these should be ignored by the solver as they
+        // do not matter for the final test
+        String u = s.concat("_bar");
+        String v = s.concat("_baz");
+        String w = s.concat("_fiz");
+        String x = s.concat("_buz");
+
+        // Assert
+        assert t.endsWith("foo");
+    }
+}

regression/jbmc-strings/StringDependencies/Test.java

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--refine-strings --string-max-length 1000 --string-max-input-length 100 --verbosity 10 Test.class --function Test.test
+^EXIT=0$
+^SIGNAL=0$
+assertion at file Test.java line 20 .*: SUCCESS
+string_refinement::check_axioms: 3 universal axioms
+--
+--
+We check there are exactly 3 universal formulas considered by the solver (2 for
+`t = s.concat("_foo")` and 1 for `t.endsWith("foo")`).
+The other concatenations should be ignored.

regression/jbmc-strings/StringDependencies/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --string-max-length 1000 --function Test.check
+--refine-strings --string-max-length 40 --function Test.check
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file Test.java line 6 .* SUCCESS

regression/jbmc-strings/StringEquals/test.desc

@@ -18,8 +18,10 @@ static array_string_exprt make_string(
 
 string_transformation_builtin_functiont::
   string_transformation_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() > 2);
   const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
@@ -55,8 +57,10 @@ optionalt<exprt> string_transformation_builtin_functiont::eval(
 }
 
 string_insertion_builtin_functiont::string_insertion_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() > 4);
   const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
@@ -69,8 +73,10 @@ string_insertion_builtin_functiont::string_insertion_builtin_functiont(
 }
 
 string_concatenation_builtin_functiont::string_concatenation_builtin_functiont(
+  const exprt &return_code,
   const std::vector<exprt> &fun_args,
   array_poolt &array_pool)
+  : string_insertion_builtin_functiont(return_code)
 {
   PRECONDITION(fun_args.size() >= 4 && fun_args.size() <= 6);
   const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
@@ -207,3 +213,33 @@ optionalt<exprt> string_insertion_builtin_functiont::eval(
   const array_typet type(result.type().subtype(), length);
   return make_string(result_value, type);
 }
+
+string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt(
+  const exprt &return_code,
+  const function_application_exprt &f,
+  array_poolt &array_pool)
+  : string_builtin_functiont(return_code), function_application(f)
+{
+  const std::vector<exprt> &fun_args = f.arguments();
+  std::size_t i = 0;
+  if(fun_args.size() >= 2 && fun_args[1].type().id() == ID_pointer)
+  {
+    string_res = array_pool.find(fun_args[1], fun_args[0]);
+    i = 2;
+  }
+
+  for(; i < fun_args.size(); ++i)
+  {
+    const auto arg = expr_try_dynamic_cast<struct_exprt>(fun_args[i]);
+    // TODO: use is_refined_string_type ?
+    if(
+      arg && arg->operands().size() == 2 &&
+      arg->op1().type().id() == ID_pointer)
+    {
+      INVARIANT(is_refined_string_type(arg->type()), "should be a string");
+      string_args.push_back(array_pool.find(arg->op1(), arg->op0()));
+    }
+    else
+      args.push_back(fun_args[i]);
+  }
+}

src/solvers/refinement/string_builtin_function.cpp

@@ -7,6 +7,7 @@
 #include <vector>
 #include <util/optional.h>
 #include <util/string_expr.h>
+#include "string_constraint_generator.h"
 
 class array_poolt;
 
@@ -32,8 +33,33 @@ class string_builtin_functiont
 
   virtual std::string name() const = 0;
 
-protected:
+  /// Add constraints ensuring that the value of result expression of the
+  /// builtin function corresponds to the value of the function call.
+  virtual exprt
+  add_constraints(string_constraint_generatort &constraint_generator) const = 0;
+
+  /// Constraint ensuring that the length of the strings are coherent with
+  /// the function call.
+  virtual exprt length_constraint() const = 0;
+
+  exprt return_code;
+
+  /// Tells whether the builtin function can be a testing function, that is a
+  /// function that does not return a string, for instance like `equals`,
+  /// `indexOf` or `compare`.
+  virtual bool maybe_testing_function() const
+  {
+    return true;
+  }
+
+private:
   string_builtin_functiont() = default;
+
+protected:
+  explicit string_builtin_functiont(const exprt &return_code)
+    : return_code(return_code)
+  {
+  }
 };
 
 /// String builtin_function transforming one string into another
@@ -43,14 +69,14 @@ class string_transformation_builtin_functiont : public string_builtin_functiont
   array_string_exprt result;
   array_string_exprt input;
   std::vector<exprt> args;
-  exprt return_code;
 
   /// 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, and potentially some
   /// arguments of primitive types.
   string_transformation_builtin_functiont(
+    const exprt &return_code,
     const std::vector<exprt> &fun_args,
     array_poolt &array_pool);
 
@@ -70,6 +96,11 @@ class string_transformation_builtin_functiont : public string_builtin_functiont
 
   optionalt<exprt>
   eval(const std::function<exprt(const exprt &)> &get_value) const override;
+
+  bool maybe_testing_function() const override
+  {
+    return false;
+  }
 };
 
 /// Adding a character at the end of a string
@@ -82,9 +113,10 @@ class string_concat_char_builtin_functiont
   /// an integer `result.length`, a character pointer `&result[0]`,
   /// a string `arg1` of type refined_string_typet, and a character.
   string_concat_char_builtin_functiont(
+    const exprt &return_code,
     const std::vector<exprt> &fun_args,
     array_poolt &array_pool)
-    : string_transformation_builtin_functiont(fun_args, array_pool)
+    : string_transformation_builtin_functiont(return_code, fun_args, array_pool)
   {
   }
 
@@ -96,6 +128,16 @@ class string_concat_char_builtin_functiont
   {
     return "concat_char";
   }
+
+  exprt add_constraints(string_constraint_generatort &generator) const override
+  {
+    return generator.add_axioms_for_concat_char(result, input, args[0]);
+  }
+
+  exprt length_constraint() const override
+  {
+    return length_constraint_for_concat_char(result, input);
+  }
 };
 
 /// String inserting a string into another one
@@ -106,7 +148,6 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
   array_string_exprt input1;
   array_string_exprt input2;
   std::vector<exprt> args;
-  exprt return_code;
 
   /// Constructor from arguments of a function application.
   /// The arguments in `fun_args` should be in order:
@@ -115,6 +156,7 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
   /// a string `arg2` of type refined_string_typet,
   /// and potentially some arguments of primitive types.
   string_insertion_builtin_functiont(
+    const exprt &return_code,
     const std::vector<exprt> &fun_args,
     array_poolt &array_pool);
 
@@ -141,8 +183,34 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
     return "insert";
   }
 
+  exprt add_constraints(string_constraint_generatort &generator) const override
+  {
+    if(args.size() == 1)
+      return generator.add_axioms_for_insert(result, input1, input2, args[0]);
+    if(args.size() == 3)
+      UNIMPLEMENTED;
+    UNREACHABLE;
+  };
+
+  exprt length_constraint() const override
+  {
+    if(args.size() == 1)
+      return length_constraint_for_insert(result, input1, input2, args[0]);
+    if(args.size() == 3)
+      UNIMPLEMENTED;
+    UNREACHABLE;
+  };
+
+  bool maybe_testing_function() const override
+  {
+    return false;
+  }
+
 protected:
-  string_insertion_builtin_functiont() = default;
+  explicit string_insertion_builtin_functiont(const exprt &return_code)
+    : string_builtin_functiont(return_code)
+  {
+  }
 };
 
 class string_concatenation_builtin_functiont final
@@ -156,6 +224,7 @@ class string_concatenation_builtin_functiont final
   /// a string `arg2` of type refined_string_typet,
   /// optionally followed by an integer `start` and an integer `end`.
   string_concatenation_builtin_functiont(
+    const exprt &return_code,
     const std::vector<exprt> &fun_args,
     array_poolt &array_pool);
 
@@ -168,6 +237,26 @@ class string_concatenation_builtin_functiont final
   {
     return "concat";
   }
+
+  exprt add_constraints(string_constraint_generatort &generator) const override
+  {
+    if(args.size() == 0)
+      return generator.add_axioms_for_concat(result, input1, input2);
+    if(args.size() == 2)
+      return generator.add_axioms_for_concat_substr(
+        result, input1, input2, args[0], args[1]);
+    UNREACHABLE;
+  };
+
+  exprt length_constraint() const override
+  {
+    if(args.size() == 0)
+      return length_constraint_for_concat(result, input1, input2);
+    if(args.size() == 2)
+      return length_constraint_for_concat_substr(
+        result, input1, input2, args[0], args[1]);
+    UNREACHABLE;
+  }
 };
 
 /// String creation from other types
@@ -182,6 +271,11 @@ class string_creation_builtin_functiont : public string_builtin_functiont
   {
     return result;
   }
+
+  bool maybe_testing_function() const override
+  {
+    return false;
+  }
 };
 
 /// String test
@@ -197,4 +291,53 @@ class string_test_builtin_functiont : public string_builtin_functiont
   }
 };
 
+/// Functions that are not yet supported in this class but are supported by
+/// string_constraint_generatort.
+/// \note Ultimately this should be disappear, once all builtin function have
+///       a corresponding string_builtin_functiont class.
+class string_builtin_function_with_no_evalt : public string_builtin_functiont
+{
+public:
+  function_application_exprt function_application;
+  optionalt<array_string_exprt> string_res;
+  std::vector<array_string_exprt> string_args;
+  std::vector<exprt> args;
+
+  string_builtin_function_with_no_evalt(
+    const exprt &return_code,
+    const function_application_exprt &f,
+    array_poolt &array_pool);
+
+  std::string name() const override
+  {
+    return id2string(function_application.function().get_identifier());
+  }
+  std::vector<array_string_exprt> string_arguments() const override
+  {
+    return std::vector<array_string_exprt>(string_args);
+  }
+  optionalt<array_string_exprt> string_result() const override
+  {
+    return string_res;
+  }
+
+  optionalt<exprt>
+  eval(const std::function<exprt(const exprt &)> &get_value) const override
+  {
+    return {};
+  }
+
+  exprt add_constraints(string_constraint_generatort &generator) const override
+  {
+    return generator.add_axioms_for_function_application(function_application);
+  };
+
+  exprt length_constraint() const override
+  {
+    // For now, there is no need for implementing that as `add_constraints`
+    // should always be called on these functions
+    UNIMPLEMENTED;
+  }
+};
+
 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H