From 54a4d7db47ae2cb1342c37ca2de27e391ba73c37 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 15 Mar 2018 08:47:24 +0000
Subject: [PATCH 01/28] Add class for builtin function with no eval

This is for builtin functions supported by string_constraint_generatort
but not string_builtin_functiont.
---
 .../refinement/string_builtin_function.h      | 31 +++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/src/solvers/refinement/string_builtin_function.h b/src/solvers/refinement/string_builtin_function.h
index 3ebdd6dc8f3..4a528b4b2f2 100644
--- a/src/solvers/refinement/string_builtin_function.h
+++ b/src/solvers/refinement/string_builtin_function.h
@@ -197,4 +197,35 @@ 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;
+  std::string name() const override
+  {
+    return id2string(function_application.id());
+  }
+  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 {};
+  }
+};
+
 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H

From c26b83df078c5b156b1035f2971865f327cecd81 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 15 Mar 2018 09:17:43 +0000
Subject: [PATCH 02/28] Constructor for builtin function with no eval

---
 .../refinement/string_builtin_function.cpp    | 29 +++++++++++++++++++
 .../refinement/string_builtin_function.h      |  5 ++++
 .../refinement/string_refinement_util.cpp     |  4 +--
 3 files changed, 36 insertions(+), 2 deletions(-)

diff --git a/src/solvers/refinement/string_builtin_function.cpp b/src/solvers/refinement/string_builtin_function.cpp
index 045a85a1c8e..8ad963c3034 100644
--- a/src/solvers/refinement/string_builtin_function.cpp
+++ b/src/solvers/refinement/string_builtin_function.cpp
@@ -207,3 +207,32 @@ 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 function_application_exprt &f,
+  array_poolt &array_pool)
+  : 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]);
+  }
+}
diff --git a/src/solvers/refinement/string_builtin_function.h b/src/solvers/refinement/string_builtin_function.h
index 4a528b4b2f2..512ee512e6c 100644
--- a/src/solvers/refinement/string_builtin_function.h
+++ b/src/solvers/refinement/string_builtin_function.h
@@ -208,6 +208,11 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont
   optionalt<array_string_exprt> string_res;
   std::vector<array_string_exprt> string_args;
   std::vector<exprt> args;
+
+  string_builtin_function_with_no_evalt(
+    const function_application_exprt &f,
+    array_poolt &array_pool);
+
   std::string name() const override
   {
     return id2string(function_application.id());
diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index 7da97d672c7..5f2b19732d7 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -176,8 +176,8 @@ static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
                                          : name.get_identifier();
 
   if(id == ID_cprover_string_insert_func)
-    return std::unique_ptr<string_builtin_functiont>(
-      new string_insertion_builtin_functiont(fun_app.arguments(), array_pool));
+    return util_make_unique<string_insertion_builtin_functiont>(
+      fun_app.arguments(), array_pool);
 
   if(id == ID_cprover_string_concat_func)
     return util_make_unique<string_concatenation_builtin_functiont>(

From 408adbe682c480d5ac18f40d71fe67b2f906c7d7 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 15 Mar 2018 09:28:23 +0000
Subject: [PATCH 03/28] never return nullptr in to_string_builtin_function

The default is now to return a function with no eval.
This also change add a use of util_make_unique in the insert case.
---
 src/solvers/refinement/string_refinement_util.cpp | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index 5f2b19732d7..f7bae747110 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -164,9 +164,7 @@ equation_symbol_mappingt::find_equations(const exprt &expr)
 }
 
 /// Construct a string_builtin_functiont object from a function application
-/// \return a unique pointer to the created object, this unique pointer is empty
-///   if the function does not correspond to one of the supported
-///   builtin_functions.
+/// \return a unique pointer to the created object
 static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
   const function_application_exprt &fun_app,
   array_poolt &array_pool)
@@ -187,7 +185,8 @@ static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
     return util_make_unique<string_concat_char_builtin_functiont>(
       fun_app.arguments(), array_pool);
 
-  return {};
+  return util_make_unique<string_builtin_function_with_no_evalt>(
+    fun_app.arguments(), array_pool);
 }
 
 string_dependenciest::string_nodet &

From 2e7057a7e48c6d267fe24b13dbc31f5be5fe0bc0 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 15 Mar 2018 09:32:53 +0000
Subject: [PATCH 04/28] Remove use of unknown_dependency

unknown dependencies on a builtin function are now using
string_builtin_function_with_no_evalt.
---
 .../refinement/string_refinement_util.cpp     | 48 +------------------
 .../refinement/string_refinement_util.h       |  5 --
 2 files changed, 2 insertions(+), 51 deletions(-)

diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index f7bae747110..57de2469c5f 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -250,41 +250,6 @@ void string_dependenciest::add_dependency(
   string_node.dependencies.push_back(builtin_function_node);
 }
 
-void string_dependenciest::add_unknown_dependency(const array_string_exprt &e)
-{
-  if(e.id() == ID_if)
-  {
-    const auto if_expr = to_if_expr(e);
-    const auto &true_case = to_array_string_expr(if_expr.true_case());
-    const auto &false_case = to_array_string_expr(if_expr.false_case());
-    add_unknown_dependency(true_case);
-    add_unknown_dependency(false_case);
-    return;
-  }
-  string_nodet &string_node = get_node(e);
-  string_node.depends_on_unknown_builtin_function = true;
-}
-
-static void add_unknown_dependency_to_string_subexprs(
-  string_dependenciest &dependencies,
-  const function_application_exprt &fun_app,
-  array_poolt &array_pool)
-{
-  for(const auto &expr : fun_app.arguments())
-  {
-    std::for_each(
-      expr.depth_begin(), expr.depth_end(), [&](const exprt &e) { // NOLINT
-        if(is_refined_string_type(e.type()))
-        {
-          const auto &string_struct = expr_checked_cast<struct_exprt>(e);
-          const array_string_exprt string =
-            array_pool.find(string_struct.op1(), string_struct.op0());
-          dependencies.add_unknown_dependency(string);
-        }
-      });
-  }
-}
-
 static void add_dependency_to_string_subexprs(
   string_dependenciest &dependencies,
   const function_application_exprt &fun_app,
@@ -331,9 +296,7 @@ optionalt<exprt> string_dependenciest::eval(
 
   const auto node = string_nodes[it->second];
   const auto &f = node.result_from;
-  if(
-    f && node.dependencies.size() == 1 &&
-    !node.depends_on_unknown_builtin_function)
+  if(f && node.dependencies.size() == 1)
   {
     const auto value_opt = get_builtin_function(*f).eval(get_value);
     eval_string_cache[it->second] = value_opt;
@@ -360,14 +323,7 @@ bool add_node(
     return false;
 
   auto builtin_function = to_string_builtin_function(*fun_app, array_pool);
-
-  if(!builtin_function)
-  {
-    add_unknown_dependency_to_string_subexprs(
-      dependencies, *fun_app, array_pool);
-    return true;
-  }
-
+  CHECK_RETURN(builtin_function != nullptr);
   const auto &builtin_function_node = dependencies.make_node(builtin_function);
   // Warning: `builtin_function` has been emptied and should not be used anymore
 
diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h
index f4a0e219adb..e766859b633 100644
--- a/src/solvers/refinement/string_refinement_util.h
+++ b/src/solvers/refinement/string_refinement_util.h
@@ -172,8 +172,6 @@ class string_dependenciest
     std::vector<builtin_function_nodet> dependencies;
     // builtin function of which it is the result
     optionalt<builtin_function_nodet> result_from;
-    // In case it depends on a builtin_function we don't support yet
-    bool depends_on_unknown_builtin_function = false;
 
     explicit string_nodet(array_string_exprt e, const std::size_t index)
       : expr(std::move(e)), index(index)
@@ -201,9 +199,6 @@ class string_dependenciest
     const array_string_exprt &e,
     const builtin_function_nodet &builtin_function);
 
-  /// Mark node for `e` as depending on unknown builtin_function
-  void add_unknown_dependency(const array_string_exprt &e);
-
   /// Attempt to evaluate the given string from the dependencies and valuation
   /// of strings on which it depends
   /// Warning: eval uses a cache which must be cleaned everytime the valuations

From 82f552c9b9cc38a59a52bca1c84f710fff28dfa5 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 15 Mar 2018 10:04:45 +0000
Subject: [PATCH 05/28] Add and add_constraint method to builtin functions

This will be used to directly add constraints by traversing the string
dependency graph.
---
 .../refinement/string_builtin_function.h      | 35 +++++++++++++++++
 .../refinement/string_constraint_generator.h  | 39 ++++++++++---------
 2 files changed, 55 insertions(+), 19 deletions(-)

diff --git a/src/solvers/refinement/string_builtin_function.h b/src/solvers/refinement/string_builtin_function.h
index 512ee512e6c..6e38113bc18 100644
--- a/src/solvers/refinement/string_builtin_function.h
+++ b/src/solvers/refinement/string_builtin_function.h
@@ -7,6 +7,7 @@
 #include <vector>
 #include <util/optional.h>
 #include <util/string_expr.h>
+#include "string_constraint_generator.h"
 
 class array_poolt;
 
@@ -32,6 +33,11 @@ class string_builtin_functiont
 
   virtual std::string name() const = 0;
 
+  /// 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;
+
 protected:
   string_builtin_functiont() = default;
 };
@@ -96,6 +102,11 @@ 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]);
+  };
 };
 
 /// String inserting a string into another one
@@ -141,6 +152,15 @@ 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;
+  };
+
 protected:
   string_insertion_builtin_functiont() = default;
 };
@@ -168,6 +188,16 @@ 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;
+  };
 };
 
 /// String creation from other types
@@ -231,6 +261,11 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont
   {
     return {};
   }
+
+  exprt add_constraints(string_constraint_generatort &generator) const override
+  {
+    return generator.add_axioms_for_function_application(function_application);
+  };
 };
 
 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index b7a3397acb9..c33be47ae78 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -148,6 +148,26 @@ class string_constraint_generatort final
     return signedbv_typet(32);
   }
 
+  exprt add_axioms_for_concat_char(
+    const array_string_exprt &res,
+    const array_string_exprt &s1,
+    const exprt &c);
+  exprt add_axioms_for_concat(
+    const array_string_exprt &res,
+    const array_string_exprt &s1,
+    const array_string_exprt &s2);
+  exprt add_axioms_for_concat_substr(
+    const array_string_exprt &res,
+    const array_string_exprt &s1,
+    const array_string_exprt &s2,
+    const exprt &start_index,
+    const exprt &end_index);
+  exprt add_axioms_for_insert(
+    const array_string_exprt &res,
+    const array_string_exprt &s1,
+    const array_string_exprt &s2,
+    const exprt &offset);
+
 private:
   symbol_exprt fresh_boolean(const irep_idt &prefix);
   array_string_exprt
@@ -203,21 +223,7 @@ class string_constraint_generatort final
   exprt add_axioms_for_empty_string(const function_application_exprt &f);
   exprt add_axioms_for_char_set(const function_application_exprt &f);
   exprt add_axioms_for_copy(const function_application_exprt &f);
-  exprt add_axioms_for_concat(
-    const array_string_exprt &res,
-    const array_string_exprt &s1,
-    const array_string_exprt &s2);
-  exprt add_axioms_for_concat_char(
-    const array_string_exprt &res,
-    const array_string_exprt &s1,
-    const exprt &c);
   exprt add_axioms_for_concat_char(const function_application_exprt &f);
-  exprt add_axioms_for_concat_substr(
-    const array_string_exprt &res,
-    const array_string_exprt &s1,
-    const array_string_exprt &s2,
-    const exprt &start_index,
-    const exprt &end_index);
   exprt add_axioms_for_concat(const function_application_exprt &f);
   exprt add_axioms_for_concat_code_point(const function_application_exprt &f);
   exprt add_axioms_for_constant(
@@ -244,11 +250,6 @@ class string_constraint_generatort final
     const typet &index_type,
     const typet &char_type);
 
-  exprt add_axioms_for_insert(
-    const array_string_exprt &res,
-    const array_string_exprt &s1,
-    const array_string_exprt &s2,
-    const exprt &offset);
   exprt add_axioms_for_insert(const function_application_exprt &f);
   exprt add_axioms_for_insert_int(const function_application_exprt &f);
   exprt add_axioms_for_insert_bool(const function_application_exprt &f);

From b8df2b3b233fefb62d097f6782f58ca52caf6894 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 15 Mar 2018 16:35:31 +0000
Subject: [PATCH 06/28] Initialize return_code for all builtin_functions

---
 .../refinement/string_builtin_function.cpp    |  9 ++++++-
 .../refinement/string_builtin_function.h      | 24 +++++++++++++++----
 .../refinement/string_refinement_util.cpp     | 13 ++++++----
 3 files changed, 35 insertions(+), 11 deletions(-)

diff --git a/src/solvers/refinement/string_builtin_function.cpp b/src/solvers/refinement/string_builtin_function.cpp
index 8ad963c3034..6776bb026e9 100644
--- a/src/solvers/refinement/string_builtin_function.cpp
+++ b/src/solvers/refinement/string_builtin_function.cpp
@@ -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]);
@@ -209,9 +215,10 @@ optionalt<exprt> string_insertion_builtin_functiont::eval(
 }
 
 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)
-  : function_application(f)
+  : string_builtin_functiont(return_code), function_application(f)
 {
   const std::vector<exprt> &fun_args = f.arguments();
   std::size_t i = 0;
diff --git a/src/solvers/refinement/string_builtin_function.h b/src/solvers/refinement/string_builtin_function.h
index 6e38113bc18..55ada98f353 100644
--- a/src/solvers/refinement/string_builtin_function.h
+++ b/src/solvers/refinement/string_builtin_function.h
@@ -38,8 +38,16 @@ class string_builtin_functiont
   virtual exprt
   add_constraints(string_constraint_generatort &constraint_generator) const = 0;
 
-protected:
+  exprt return_code;
+
+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
@@ -49,7 +57,6 @@ 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:
@@ -57,6 +64,7 @@ class string_transformation_builtin_functiont : public string_builtin_functiont
   /// 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);
 
@@ -88,9 +96,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)
   {
   }
 
@@ -117,7 +126,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:
@@ -126,6 +134,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);
 
@@ -162,7 +171,10 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
   };
 
 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
@@ -176,6 +188,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);
 
@@ -240,6 +253,7 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont
   std::vector<exprt> args;
 
   string_builtin_function_with_no_evalt(
+    const exprt &return_code,
     const function_application_exprt &f,
     array_poolt &array_pool);
 
diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index 57de2469c5f..b38a139089d 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -167,6 +167,7 @@ equation_symbol_mappingt::find_equations(const exprt &expr)
 /// \return a unique pointer to the created object
 static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
   const function_application_exprt &fun_app,
+  const exprt &return_code,
   array_poolt &array_pool)
 {
   const auto name = expr_checked_cast<symbol_exprt>(fun_app.function());
@@ -175,18 +176,18 @@ static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
 
   if(id == ID_cprover_string_insert_func)
     return util_make_unique<string_insertion_builtin_functiont>(
-      fun_app.arguments(), array_pool);
+      return_code, fun_app.arguments(), array_pool);
 
   if(id == ID_cprover_string_concat_func)
     return util_make_unique<string_concatenation_builtin_functiont>(
-      fun_app.arguments(), array_pool);
+      return_code, fun_app.arguments(), array_pool);
 
   if(id == ID_cprover_string_concat_char_func)
     return util_make_unique<string_concat_char_builtin_functiont>(
-      fun_app.arguments(), array_pool);
+      return_code, fun_app.arguments(), array_pool);
 
   return util_make_unique<string_builtin_function_with_no_evalt>(
-    fun_app.arguments(), array_pool);
+    return_code, fun_app, array_pool);
 }
 
 string_dependenciest::string_nodet &
@@ -322,7 +323,9 @@ bool add_node(
   if(!fun_app)
     return false;
 
-  auto builtin_function = to_string_builtin_function(*fun_app, array_pool);
+  auto builtin_function =
+    to_string_builtin_function(*fun_app, equation.lhs(), array_pool);
+
   CHECK_RETURN(builtin_function != nullptr);
   const auto &builtin_function_node = dependencies.make_node(builtin_function);
   // Warning: `builtin_function` has been emptied and should not be used anymore

From 8a7d1943a543e680f05a3b2dbaba9237968b9cf2 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 15 Mar 2018 16:05:39 +0000
Subject: [PATCH 07/28] add_constraints method in string_dependencies

---
 src/solvers/refinement/string_refinement_util.cpp | 7 +++++++
 src/solvers/refinement/string_refinement_util.h   | 2 ++
 2 files changed, 9 insertions(+)

diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index b38a139089d..7ab96ec8c96 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -414,3 +414,10 @@ void string_dependenciest::output_dot(std::ostream &stream) const
   output_dot_generic<nodet>(stream, for_each, for_each_succ, node_to_string);
   stream << '}' << std::endl;
 }
+
+void string_dependenciest::add_constraints(
+  string_constraint_generatort &generator)
+{
+  for(const auto &builtin : builtin_function_nodes)
+    builtin->add_constraints(generator);
+}
diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h
index e766859b633..519b89c9f11 100644
--- a/src/solvers/refinement/string_refinement_util.h
+++ b/src/solvers/refinement/string_refinement_util.h
@@ -212,6 +212,8 @@ class string_dependenciest
 
   void output_dot(std::ostream &stream) const;
 
+  void add_constraints(string_constraint_generatort &generatort);
+
 private:
   /// Set of nodes representing builtin_functions
   std::vector<std::unique_ptr<string_builtin_functiont>> builtin_function_nodes;

From 41c029444e9a0b9c808e173e7c7ea1e52bb3811a Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 15 Mar 2018 16:06:03 +0000
Subject: [PATCH 08/28] Add constraints from the string dependencies

We add constraints directly from the constructed graph instead of going
through all the equations.
---
 .../refinement/string_constraint_generator.h  |  1 +
 .../string_constraint_generator_main.cpp      |  5 ++
 src/solvers/refinement/string_refinement.cpp  | 50 ++++---------------
 .../refinement/string_refinement_util.cpp     |  5 +-
 4 files changed, 20 insertions(+), 41 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index c33be47ae78..52d02ac9d6f 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -105,6 +105,7 @@ class string_constraint_generatort final
   /// Axioms are of three kinds: universally quantified string constraint,
   /// not contains string constraints and simple formulas.
   const std::vector<exprt> &get_lemmas() const;
+  void add_lemma(const exprt &);
   const std::vector<string_constraintt> &get_constraints() const;
   const std::vector<string_not_contains_constraintt> &
   get_not_contains_constraints() const;
diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
index efd85c8165b..ec29a940a0c 100644
--- a/src/solvers/refinement/string_constraint_generator_main.cpp
+++ b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -39,6 +39,11 @@ const std::vector<exprt> &string_constraint_generatort::get_lemmas() const
   return lemmas;
 }
 
+void string_constraint_generatort::add_lemma(const exprt &expr)
+{
+  lemmas.push_back(expr);
+}
+
 const std::vector<string_constraintt> &
 string_constraint_generatort::get_constraints() const
 {
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 53da9d1cbb6..52c7e8d7675 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -251,41 +251,6 @@ static std::vector<exprt> generate_instantiations(
   return lemmas;
 }
 
-/// Remove functions applications and create the necessary axioms.
-/// \param expr: an expression possibly containing function applications
-/// \param generator: generator for the string constraints
-/// \return an expression containing no function application
-static void substitute_function_applications(
-  exprt &expr,
-  string_constraint_generatort &generator)
-{
-  for(auto it = expr.depth_begin(), itend = expr.depth_end();
-      it != itend;) // No ++it
-  {
-    if(it->id() == ID_function_application)
-    {
-      it.mutate() =
-        generator.add_axioms_for_function_application(
-          to_function_application_expr(expr));
-      it.next_sibling_or_parent();
-    }
-    else
-      ++it;
-  }
-}
-
-/// Remove functions applications and create the necessary axioms.
-/// \param equations: vector of equations
-/// \param generator: generator for the string constraints
-/// \return vector of equations where function application have been replaced
-static void substitute_function_applications_in_equations(
-  std::vector<equal_exprt> &equations,
-  string_constraint_generatort &generator)
-{
-  for(auto &eq : equations)
-    substitute_function_applications(eq.rhs(), generator);
-}
-
 /// Fill the array_pointer correspondence and replace the right hand sides of
 /// the corresponding equations
 static void make_char_array_pointer_associations(
@@ -680,17 +645,22 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   output_equations(debug(), equations, ns);
 #endif
 
-  debug() << "dec_solve: compute dependency graph:" << eom;
-  for(const equal_exprt &eq : equations)
-    add_node(dependencies, eq, generator.array_pool);
+  debug() << "dec_solve: compute dependency graph and remove function "
+          << "applications captured by the dependencies:" << eom;
+  const auto new_equation_end = std::remove_if(
+    equations.begin(), equations.end(), [&](const equal_exprt &eq) { // NOLINT
+      return add_node(dependencies, eq, generator.array_pool);
+    });
+  equations.erase(new_equation_end, equations.end());
 
 #ifdef DEBUG
   dependencies.output_dot(debug());
 #endif
 
-  debug() << "dec_solve: Replace function applications" << eom;
+  debug() << "dec_solve: add constraints" << eom;
   // Generator is also used by get, that's why we use a class member
-  substitute_function_applications_in_equations(equations, generator);
+  dependencies.add_constraints(generator);
+
 #ifdef DEBUG
   output_equations(debug(), equations, ns);
 #endif
diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index 7ab96ec8c96..f148393504a 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -419,5 +419,8 @@ void string_dependenciest::add_constraints(
   string_constraint_generatort &generator)
 {
   for(const auto &builtin : builtin_function_nodes)
-    builtin->add_constraints(generator);
+  {
+    const exprt return_value = builtin->add_constraints(generator);
+    generator.add_lemma(equal_exprt(return_value, builtin->return_code));
+  }
 }

From 97ee2d6c4769f5c6c679e41afe139162f70fc125 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 16 Mar 2018 17:47:00 +0000
Subject: [PATCH 09/28] Store builtin function pointer inside builtin node

This is more natural than always having to refer to the
builtin_function_nodes array.
---
 .../refinement/string_refinement_util.cpp     | 40 ++++++++-----------
 .../refinement/string_refinement_util.h       | 26 +++++++-----
 2 files changed, 32 insertions(+), 34 deletions(-)

diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index f148393504a..ad071aa3f58 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -210,28 +210,18 @@ string_dependenciest::node_at(const array_string_exprt &e) const
   return {};
 }
 
-string_dependenciest::builtin_function_nodet string_dependenciest::make_node(
+string_dependenciest::builtin_function_nodet &string_dependenciest::make_node(
   std::unique_ptr<string_builtin_functiont> &builtin_function)
 {
-  const builtin_function_nodet builtin_function_node(
-    builtin_function_nodes.size());
-  builtin_function_nodes.emplace_back();
-  builtin_function_nodes.back().swap(builtin_function);
-  return builtin_function_node;
+  builtin_function_nodes.emplace_back(
+    std::move(builtin_function), builtin_function_nodes.size());
+  return builtin_function_nodes.back();
 }
 
 const string_builtin_functiont &string_dependenciest::get_builtin_function(
   const builtin_function_nodet &node) const
 {
-  PRECONDITION(node.index < builtin_function_nodes.size());
-  return *(builtin_function_nodes[node.index]);
-}
-
-const std::vector<string_dependenciest::builtin_function_nodet> &
-string_dependenciest::dependencies(
-  const string_dependenciest::string_nodet &node) const
-{
-  return node.dependencies;
+  return *node.data;
 }
 
 void string_dependenciest::add_dependency(
@@ -248,7 +238,7 @@ void string_dependenciest::add_dependency(
     return;
   }
   string_nodet &string_node = get_node(e);
-  string_node.dependencies.push_back(builtin_function_node);
+  string_node.dependencies.push_back(builtin_function_node.index);
 }
 
 static void add_dependency_to_string_subexprs(
@@ -299,7 +289,7 @@ optionalt<exprt> string_dependenciest::eval(
   const auto &f = node.result_from;
   if(f && node.dependencies.size() == 1)
   {
-    const auto value_opt = get_builtin_function(*f).eval(get_value);
+    const auto value_opt = builtin_function_nodes[*f].data->eval(get_value);
     eval_string_cache[it->second] = value_opt;
     return value_opt;
   }
@@ -336,7 +326,7 @@ bool add_node(
   {
     dependencies.add_dependency(*string_result, builtin_function_node);
     auto &node = dependencies.get_node(*string_result);
-    node.result_from = builtin_function_node;
+    node.result_from = builtin_function_node.index;
   }
   else
     add_dependency_to_string_subexprs(
@@ -352,7 +342,7 @@ void string_dependenciest::for_each_successor(
   if(node.kind == nodet::BUILTIN)
   {
     const auto &builtin = builtin_function_nodes[node.index];
-    for(const auto &s : builtin->string_arguments())
+    for(const auto &s : builtin.data->string_arguments())
     {
       std::vector<std::reference_wrapper<const exprt>> stack({s});
       while(!stack.empty())
@@ -377,7 +367,9 @@ void string_dependenciest::for_each_successor(
     std::for_each(
       s_node.dependencies.begin(),
       s_node.dependencies.end(),
-      [&](const builtin_function_nodet &p) { f(nodet(p)); });
+      [&](const std::size_t &index) { // NOLINT
+        f(nodet(builtin_function_nodes[index]));
+      });
   }
   else
     UNREACHABLE;
@@ -389,7 +381,7 @@ void string_dependenciest::for_each_node(
   for(const auto string_node : string_nodes)
     f(nodet(string_node));
   for(std::size_t i = 0; i < builtin_function_nodes.size(); ++i)
-    f(nodet(builtin_function_nodet(i)));
+    f(nodet(builtin_function_nodes[i]));
 }
 
 void string_dependenciest::output_dot(std::ostream &stream) const
@@ -405,7 +397,7 @@ void string_dependenciest::output_dot(std::ostream &stream) const
   const auto node_to_string = [&](const nodet &n) { // NOLINT
     std::stringstream ostream;
     if(n.kind == nodet::BUILTIN)
-      ostream << builtin_function_nodes[n.index]->name() << n.index;
+      ostream << builtin_function_nodes[n.index].data->name() << n.index;
     else
       ostream << '"' << format(string_nodes[n.index].expr) << '"';
     return ostream.str();
@@ -420,7 +412,7 @@ void string_dependenciest::add_constraints(
 {
   for(const auto &builtin : builtin_function_nodes)
   {
-    const exprt return_value = builtin->add_constraints(generator);
-    generator.add_lemma(equal_exprt(return_value, builtin->return_code));
+    const exprt return_value = builtin.data->add_constraints(generator);
+    generator.add_lemma(equal_exprt(return_value, builtin.data->return_code));
   }
 }
diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h
index 519b89c9f11..fa6473fd05d 100644
--- a/src/solvers/refinement/string_refinement_util.h
+++ b/src/solvers/refinement/string_refinement_util.h
@@ -149,13 +149,19 @@ class equation_symbol_mappingt
 class string_dependenciest
 {
 public:
-  /// A builtin_function node is just an index in the `builtin_function_nodes`
-  /// vector.
+  /// A builtin function node contains a builtin function call
   class builtin_function_nodet
   {
   public:
+    // index in the `builtin_function_nodes` vector
     std::size_t index;
-    explicit builtin_function_nodet(std::size_t i) : index(i)
+    // pointer to the builtin function
+    std::unique_ptr<string_builtin_functiont> data;
+
+    explicit builtin_function_nodet(
+      std::unique_ptr<string_builtin_functiont> d,
+      std::size_t i)
+      : index(i), data(std::move(d))
     {
     }
   };
@@ -168,10 +174,12 @@ class string_dependenciest
     array_string_exprt expr;
     // index in the string_nodes vector
     std::size_t index;
-    // builtin functions on which it depends
-    std::vector<builtin_function_nodet> dependencies;
+    // builtin functions on which it depends, refered by there index in
+    // builtin_function node vector.
+    // \todo should these we shared pointers?
+    std::vector<std::size_t> dependencies;
     // builtin function of which it is the result
-    optionalt<builtin_function_nodet> result_from;
+    optionalt<std::size_t> result_from;
 
     explicit string_nodet(array_string_exprt e, const std::size_t index)
       : expr(std::move(e)), index(index)
@@ -185,10 +193,8 @@ class string_dependenciest
   node_at(const array_string_exprt &e) const;
 
   /// `builtin_function` is reset to an empty pointer after the node is created
-  builtin_function_nodet
+  builtin_function_nodet &
   make_node(std::unique_ptr<string_builtin_functiont> &builtin_function);
-  const std::vector<builtin_function_nodet> &
-  dependencies(const string_nodet &node) const;
   const string_builtin_functiont &
   get_builtin_function(const builtin_function_nodet &node) const;
 
@@ -216,7 +222,7 @@ class string_dependenciest
 
 private:
   /// Set of nodes representing builtin_functions
-  std::vector<std::unique_ptr<string_builtin_functiont>> builtin_function_nodes;
+  std::vector<builtin_function_nodet> builtin_function_nodes;
 
   /// Set of nodes representing strings
   std::vector<string_nodet> string_nodes;

From 66092474535401ff36d18a6f2ad77c45dcb2b9ae Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 16 Mar 2018 17:52:09 +0000
Subject: [PATCH 10/28] Add a maybe_testing_function to builtin functions

This is to know whether the result of a function can be used outside of
string operations.
---
 .../refinement/string_builtin_function.h      | 23 +++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/src/solvers/refinement/string_builtin_function.h b/src/solvers/refinement/string_builtin_function.h
index 55ada98f353..282810c6775 100644
--- a/src/solvers/refinement/string_builtin_function.h
+++ b/src/solvers/refinement/string_builtin_function.h
@@ -40,6 +40,14 @@ class string_builtin_functiont
 
   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;
 
@@ -84,6 +92,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
@@ -170,6 +183,11 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
     UNREACHABLE;
   };
 
+  bool maybe_testing_function() const override
+  {
+    return false;
+  }
+
 protected:
   explicit string_insertion_builtin_functiont(const exprt &return_code)
     : string_builtin_functiont(return_code)
@@ -225,6 +243,11 @@ class string_creation_builtin_functiont : public string_builtin_functiont
   {
     return result;
   }
+
+  bool maybe_testing_function() const override
+  {
+    return false;
+  }
 };
 
 /// String test

From 46d25072aab08f8134f96005b83b034e02567f50 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Tue, 20 Mar 2018 12:23:23 +0000
Subject: [PATCH 11/28] Add move constructors to builtin_function_nodet

Because of some issues with Visual Studio these need to be defined.
---
 src/solvers/refinement/string_refinement_util.h | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h
index fa6473fd05d..a15d91fecaa 100644
--- a/src/solvers/refinement/string_refinement_util.h
+++ b/src/solvers/refinement/string_refinement_util.h
@@ -164,6 +164,18 @@ class string_dependenciest
       : index(i), data(std::move(d))
     {
     }
+
+    builtin_function_nodet(builtin_function_nodet &&other)
+      : index(other.index), data(std::move(other.data))
+    {
+    }
+
+    builtin_function_nodet &operator=(builtin_function_nodet &&other)
+    {
+      index = other.index;
+      data = std::move(other.data);
+      return *this;
+    }
   };
 
   /// A string node points to builtin_function on which it depends

From c487c4b9dced830f276e06299812a5fa71e53243 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 19 Mar 2018 14:52:21 +0000
Subject: [PATCH 12/28] Generic get_reachable function

This takes as argument a set and a for_each_successor function.
This can be used even by classes that do not inherit from grapht.
---
 src/util/graph.h | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/src/util/graph.h b/src/util/graph.h
index ed67703cf9d..13c0db26bc0 100644
--- a/src/util/graph.h
+++ b/src/util/graph.h
@@ -461,6 +461,38 @@ void grapht<N>::visit_reachable(node_indext src)
     nodes[index].visited = true;
 }
 
+/// Add to `set`, nodes that are reachable from `set`.
+///
+/// This implements a depth first search using a stack: at each step we pop a
+/// node, and push on the stack all its successors that have not yet been
+/// visited.
+/// \param set: set of source nodes, must be a container with an
+///   `insert(const value_type&)` method.
+/// \param for_each_successor: function which given a node `n` and a function
+///   `f`, applies `f` on all successors of `n`.
+template <class Container, typename nodet = typename Container::value_type>
+void get_reachable(
+  Container &set,
+  const std::function<void(
+    const typename Container::value_type &,
+    const std::function<void(const typename Container::value_type &)> &)>
+    &for_each_successor)
+{
+  std::vector<nodet> stack;
+  for(const auto &elt : set)
+    stack.push_back(elt);
+
+  while(!stack.empty())
+  {
+    auto n = stack.back();
+    stack.pop_back();
+    for_each_successor(n, [&](const nodet &node) { // NOLINT
+      if(set.insert(node).second)
+        stack.push_back(node);
+    });
+  }
+}
+
 /// Run depth-first search on the graph, starting from a single source
 /// node.
 /// \param src The node to start the search from.

From 23f8cd47503199c0f3f4b212738c19af93271816 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 22 Mar 2018 11:14:16 +0000
Subject: [PATCH 13/28] Correct name of builtin function with no eval

---
 src/solvers/refinement/string_builtin_function.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solvers/refinement/string_builtin_function.h b/src/solvers/refinement/string_builtin_function.h
index 282810c6775..4c2642e88f3 100644
--- a/src/solvers/refinement/string_builtin_function.h
+++ b/src/solvers/refinement/string_builtin_function.h
@@ -282,7 +282,7 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont
 
   std::string name() const override
   {
-    return id2string(function_application.id());
+    return id2string(function_application.function().get_identifier());
   }
   std::vector<array_string_exprt> string_arguments() const override
   {

From 3c61cf2d096e9eb29b60b41699f1ef601e91dc0a Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 19 Mar 2018 16:48:13 +0000
Subject: [PATCH 14/28] Add a hash function for nodes

This is to be able to use containers such as unordered_set/unordered_map
---
 src/solvers/refinement/string_refinement_util.h | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h
index a15d91fecaa..808bd512e8d 100644
--- a/src/solvers/refinement/string_refinement_util.h
+++ b/src/solvers/refinement/string_refinement_util.h
@@ -263,6 +263,23 @@ class string_dependenciest
       : kind(STRING), index(string_node.index)
     {
     }
+
+    bool operator==(const nodet &n) const
+    {
+      return n.kind == kind && n.index == index;
+    }
+  };
+
+  /// Hash function for nodes
+  // NOLINTNEXTLINE(readability/identifiers)
+  struct node_hash
+  {
+    size_t
+    operator()(const string_dependenciest::nodet &node) const optional_noexcept
+    {
+      return 2 * node.index +
+             (node.kind == string_dependenciest::nodet::STRING ? 0 : 1);
+    }
   };
 
   mutable std::vector<optionalt<exprt>> eval_string_cache;

From 4b342f75d7e8cff6bacb5751f61c6b09a4f75b6f Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 19 Mar 2018 08:29:02 +0000
Subject: [PATCH 15/28] Only add constraints on test function dependencies

Instead of adding all constraints corresponding to a string function
call, we look at which strings may be used in a testing function (such
as endsWith, equals, compare, etc...). We only add constraints for these
function calls, since the other operations cannot matter for the
satisfiability problem.
---
 .../refinement/string_refinement_util.cpp     | 24 +++++++++++++++++--
 1 file changed, 22 insertions(+), 2 deletions(-)

diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index ad071aa3f58..f7aa5c06903 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -17,6 +17,7 @@
 #include <util/graph.h>
 #include <util/magic.h>
 #include <util/make_unique.h>
+#include <unordered_set>
 #include "string_refinement_util.h"
 
 bool is_char_type(const typet &type)
@@ -410,9 +411,28 @@ void string_dependenciest::output_dot(std::ostream &stream) const
 void string_dependenciest::add_constraints(
   string_constraint_generatort &generator)
 {
+  std::unordered_set<nodet, node_hash> test_dependencies;
   for(const auto &builtin : builtin_function_nodes)
   {
-    const exprt return_value = builtin.data->add_constraints(generator);
-    generator.add_lemma(equal_exprt(return_value, builtin.data->return_code));
+    if(builtin.data->maybe_testing_function())
+      test_dependencies.insert(nodet(builtin));
+  }
+
+  get_reachable(
+    test_dependencies,
+    [&](
+      const nodet &n,
+      const std::function<void(const nodet &)> &f) { // NOLINT
+      for_each_successor(n, f);
+    });
+
+  for(const auto &node : test_dependencies)
+  {
+    if(node.kind == node.BUILTIN)
+    {
+      const auto &builtin = builtin_function_nodes[node.index];
+      const exprt return_value = builtin.data->add_constraints(generator);
+      generator.add_lemma(equal_exprt(return_value, builtin.data->return_code));
+    }
   }
 }

From be5f194fea4c23681d5b8b1320732def81901145 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 23 Mar 2018 10:52:19 +0000
Subject: [PATCH 16/28] Add double quotes to output_dot

---
 src/solvers/refinement/string_refinement_util.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index f7aa5c06903..7c5c6c815c4 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -398,7 +398,8 @@ void string_dependenciest::output_dot(std::ostream &stream) const
   const auto node_to_string = [&](const nodet &n) { // NOLINT
     std::stringstream ostream;
     if(n.kind == nodet::BUILTIN)
-      ostream << builtin_function_nodes[n.index].data->name() << n.index;
+      ostream << '"' << builtin_function_nodes[n.index].data->name() << '_'
+              << n.index << '"';
     else
       ostream << '"' << format(string_nodes[n.index].expr) << '"';
     return ostream.str();

From 2655a9b0c4c6f740fe6937ce9d5c30b766cecc90 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 22 Mar 2018 09:06:26 +0000
Subject: [PATCH 17/28] Rewrite axioms for insert

This reduces the number of universal formulas added (from 6 to 3), and
avoid introducing new strings. Ideally the add_axioms_-function should
not introduce new strings, that would make it easier to refactor and add
new functionalities.
---
 .../string_constraint_generator_insert.cpp    | 58 ++++++++++++-------
 1 file changed, 38 insertions(+), 20 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator_insert.cpp b/src/solvers/refinement/string_constraint_generator_insert.cpp
index c5c975ffbff..34a57515ff4 100644
--- a/src/solvers/refinement/string_constraint_generator_insert.cpp
+++ b/src/solvers/refinement/string_constraint_generator_insert.cpp
@@ -14,8 +14,14 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 
 /// Add axioms ensuring the result `res` corresponds to `s1` where we
 /// inserted `s2` at position `offset`.
+/// We write offset' for `max(0, min(res.length, offset))`.
+/// These axioms are:
+/// 1. res.length = s1.length + s2.length
+/// 2. forall i < offset' . res[i] = s1[i]
+/// 3. forall i < s2.length. res[i + offset'] = s2[i]
+/// 4. forall i in [offset', s1.length). res[i + s2.length] = s1[i]
 /// This is equivalent to
-/// `res=concat(substring(s1, 0, offset), concat(s2, substring(s1, offset)))`.
+/// `res=concat(substring(s1, 0, offset'), concat(s2, substring(s1, offset')))`.
 /// \param res: array of characters expression
 /// \param s1: array of characters expression
 /// \param s2: array of characters expression
@@ -30,25 +36,37 @@ exprt string_constraint_generatort::add_axioms_for_insert(
 {
   PRECONDITION(offset.type()==s1.length().type());
   const typet &index_type = s1.length().type();
-  const typet &char_type = s1.content().type().subtype();
-  array_string_exprt pref = fresh_string(index_type, char_type);
-  exprt return_code1 =
-    add_axioms_for_substring(pref, s1, from_integer(0, offset.type()), offset);
-  array_string_exprt suf = fresh_string(index_type, char_type);
-  exprt return_code2 = add_axioms_for_substring(suf, s1, offset, s1.length());
-  array_string_exprt concat1 = fresh_string(index_type, char_type);
-  exprt return_code3 = add_axioms_for_concat(concat1, pref, s2);
-  exprt return_code4 = add_axioms_for_concat(res, concat1, suf);
-  return if_exprt(
-    equal_exprt(return_code1, from_integer(0, return_code1.type())),
-    if_exprt(
-      equal_exprt(return_code2, from_integer(0, return_code1.type())),
-      if_exprt(
-        equal_exprt(return_code3, from_integer(0, return_code1.type())),
-        return_code4,
-        return_code3),
-      return_code2),
-    return_code1);
+  const exprt offset1 =
+    maximum(from_integer(0, index_type), minimum(s1.length(), offset));
+
+  // Axiom 1.
+  lemmas.push_back(
+    equal_exprt(res.length(), plus_exprt(s1.length(), s2.length())));
+
+  // Axiom 2.
+  constraints.push_back([&] { // NOLINT
+    const symbol_exprt i = fresh_symbol("QA_insert1", index_type);
+    return string_constraintt(i, offset1, equal_exprt(res[i], s1[i]));
+  }());
+
+  // Axiom 3.
+  constraints.push_back([&] { // NOLINT
+    const symbol_exprt i = fresh_symbol("QA_insert2", index_type);
+    return string_constraintt(
+      i, s2.length(), equal_exprt(res[plus_exprt(i, offset1)], s2[i]));
+  }());
+
+  // Axiom 4.
+  constraints.push_back([&] { // NOLINT
+    const symbol_exprt i = fresh_symbol("QA_insert3", index_type);
+    return string_constraintt(
+      i,
+      offset1,
+      s1.length(),
+      equal_exprt(res[plus_exprt(i, s2.length())], s1[i]));
+  }());
+
+  return from_integer(0, get_return_code_type());
 }
 
 /// Insertion of a string in another at a specific index

From e3da98c20dd24a19dfcf2fd436a941e86dc09443 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 23 Mar 2018 10:59:38 +0000
Subject: [PATCH 18/28] Deactivating invariant

---
 src/solvers/refinement/string_refinement_util.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index 7c5c6c815c4..bcaf5d1b61a 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -358,7 +358,10 @@ void string_dependenciest::for_each_successor(
         else if(const auto node = node_at(to_array_string_expr(current)))
           f(nodet(*node));
         else
-          UNREACHABLE;
+        {
+          std::cout << "Warning no node for " << format(current) << std::endl;
+          //UNREACHABLE;
+        }
       }
     }
   }

From a45c64f5edc6d151a4b37c017e217ef8cd74873e Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 19 Mar 2018 16:54:00 +0000
Subject: [PATCH 19/28] Add tests for the use of string dependencies

This tests, check that only constraints for the string operation that
matters are added to the list of axioms of the string solver.
In the example added here, the solver would previously consider 11
constraints, but now only 3, and still finds the correct result.
---
 .../StringDependencies/Test.class             | Bin 0 -> 783 bytes
 .../jbmc-strings/StringDependencies/Test.java |  22 ++++++++++++++++++
 .../jbmc-strings/StringDependencies/test.desc |  12 ++++++++++
 3 files changed, 34 insertions(+)
 create mode 100644 regression/jbmc-strings/StringDependencies/Test.class
 create mode 100644 regression/jbmc-strings/StringDependencies/Test.java
 create mode 100644 regression/jbmc-strings/StringDependencies/test.desc

diff --git a/regression/jbmc-strings/StringDependencies/Test.class b/regression/jbmc-strings/StringDependencies/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..c06ccc8b8df9b7204a44bc1063b8a5e236e16395
GIT binary patch
literal 783
zcmZ`$O>fgc6r6SJtmC>(ntl)nrG>U3ZA!zTCx{Rb;M9*pDiFOO$JrK_U?bb%$K=F~
zb3sZakl={Kj{;`Xv_X7mZO_|%Z{NHbfB*663xF-$cHp9H<En!NT(hy5gM%d-*Y*B}
z#Ige$Wr-CBtEfoa6qs4@l0?O65QWL3Ao1E=)e#T}0@+3o2I)P4Om*$4fZ2>XN+7=-
zglf0<x~<}UUCczPl2l->x_#`u_3B+OJgT?SI0%pK>U)!|)bn5McyET~<d&!k*bTos
zYVWk7UhJzUfo_)DXR}S+$VDCnc7M_KVqS5vhIPF?j3O74nBrW_xTs-6pfsj_a4zR@
z97i#4=#CP%Tx_B)P#9P4wU3q0$$vXKo15DGDD*w%D*saTw@?aFVJCSOq%Z&D1P#rP
zsheH8E->FwNf4{f#mw|7?J+^i53t0a=kmXbLP-l|l;KNPATZ5nfhdU9`YFT-1A!vH
z+2Ns1%wU$WE`0|BlGv<$gLzUb8Uti@YDJT<dj@yR5n3b6et^}->_#y=fb3)9GwkQ5
z$bHpB#*nCj9AlHq;?lEDkur}mCtN0Njr0#O#|13HuzsQeDKRf`>5qp6HcA)5wuTCT
h>7p~hL?6<84>R)-)|mTTr0#9OaPMm?E^}kx$}cG!ln4L-

literal 0
HcmV?d00001

diff --git a/regression/jbmc-strings/StringDependencies/Test.java b/regression/jbmc-strings/StringDependencies/Test.java
new file mode 100644
index 00000000000..80fabe62f0b
--- /dev/null
+++ b/regression/jbmc-strings/StringDependencies/Test.java
@@ -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");
+    }
+}
diff --git a/regression/jbmc-strings/StringDependencies/test.desc b/regression/jbmc-strings/StringDependencies/test.desc
new file mode 100644
index 00000000000..8368650a1cf
--- /dev/null
+++ b/regression/jbmc-strings/StringDependencies/test.desc
@@ -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.

From c3aed8541c4fb240584472bbd20725f4cf4e4fd2 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 23 Mar 2018 06:38:08 +0000
Subject: [PATCH 20/28] Define two helper functions for for_each_successor

These two functions deal with one type of node.
Type safety ensures we don't mix the two kinds of node, so these two
functions can be made public.
---
 .../refinement/string_refinement_util.cpp     | 76 +++++++++++--------
 .../refinement/string_refinement_util.h       |  8 ++
 2 files changed, 52 insertions(+), 32 deletions(-)

diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index bcaf5d1b61a..ed8a5894b3a 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -336,47 +336,59 @@ bool add_node(
   return true;
 }
 
-void string_dependenciest::for_each_successor(
-  const nodet &node,
-  const std::function<void(const nodet &)> &f) const
+void string_dependenciest::for_each_dependency(
+  const builtin_function_nodet &node,
+  const std::function<void(const string_nodet &)> &f) const
 {
-  if(node.kind == nodet::BUILTIN)
+  for(const auto &s : node.data->string_arguments())
   {
-    const auto &builtin = builtin_function_nodes[node.index];
-    for(const auto &s : builtin.data->string_arguments())
+    std::vector<std::reference_wrapper<const exprt>> stack({s});
+    while(!stack.empty())
     {
-      std::vector<std::reference_wrapper<const exprt>> stack({s});
-      while(!stack.empty())
+      const auto current = stack.back();
+      stack.pop_back();
+      if(const auto if_expr = expr_try_dynamic_cast<if_exprt>(current.get()))
       {
-        const auto current = stack.back();
-        stack.pop_back();
-        if(const auto if_expr = expr_try_dynamic_cast<if_exprt>(current.get()))
-        {
-          stack.emplace_back(if_expr->true_case());
-          stack.emplace_back(if_expr->false_case());
-        }
-        else if(const auto node = node_at(to_array_string_expr(current)))
-          f(nodet(*node));
-        else
-        {
-          std::cout << "Warning no node for " << format(current) << std::endl;
-          //UNREACHABLE;
-        }
+        stack.emplace_back(if_expr->true_case());
+        stack.emplace_back(if_expr->false_case());
+      }
+      else if(const auto string_node = node_at(to_array_string_expr(current)))
+        f(*string_node);
+      else
+      {
+        std::cout << "Warning no node for " << format(current) << std::endl;
+        //UNREACHABLE;
       }
     }
   }
-  else if(node.kind == nodet::STRING)
+}
+
+void string_dependenciest::for_each_dependency(
+  const string_nodet &node,
+  const std::function<void(const builtin_function_nodet &)> &f) const
+{
+  for(const std::size_t &index : node.dependencies)
+    f(builtin_function_nodes[index]);
+}
+
+void string_dependenciest::for_each_successor(
+  const nodet &node,
+  const std::function<void(const nodet &)> &f) const
+{
+  switch(node.kind)
   {
-    const auto &s_node = string_nodes[node.index];
-    std::for_each(
-      s_node.dependencies.begin(),
-      s_node.dependencies.end(),
-      [&](const std::size_t &index) { // NOLINT
-        f(nodet(builtin_function_nodes[index]));
-      });
+  case nodet::BUILTIN:
+    for_each_dependency(
+      builtin_function_nodes[node.index],
+      [&](const string_nodet &n) { return f(nodet(n)); });
+    break;
+
+  case nodet::STRING:
+    for_each_dependency(
+      string_nodes[node.index],
+      [&](const builtin_function_nodet &n) { return f(nodet(n)); });
+    break;
   }
-  else
-    UNREACHABLE;
 }
 
 void string_dependenciest::for_each_node(
diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h
index 808bd512e8d..1014f14d2b2 100644
--- a/src/solvers/refinement/string_refinement_util.h
+++ b/src/solvers/refinement/string_refinement_util.h
@@ -217,6 +217,14 @@ class string_dependenciest
     const array_string_exprt &e,
     const builtin_function_nodet &builtin_function);
 
+  /// Applies `f` to each node on which `node` depends
+  void for_each_dependency(
+    const string_nodet &node,
+    const std::function<void(const builtin_function_nodet &)> &f) const;
+  void for_each_dependency(
+    const builtin_function_nodet &node,
+    const std::function<void(const string_nodet &)> &f) const;
+
   /// Attempt to evaluate the given string from the dependencies and valuation
   /// of strings on which it depends
   /// Warning: eval uses a cache which must be cleaned everytime the valuations

From 8a982462ae798d78c76d7b87b91d73443e95a49d Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 22 Mar 2018 15:54:06 +0000
Subject: [PATCH 21/28] Adapt unit tests for the new interface

The interface for string dependencies has changed so these need to be adapted.
---
 .../string_refinement/dependency_graph.cpp    | 98 ++++++++++---------
 1 file changed, 51 insertions(+), 47 deletions(-)

diff --git a/unit/solvers/refinement/string_refinement/dependency_graph.cpp b/unit/solvers/refinement/string_refinement/dependency_graph.cpp
index 09c4b075fb0..3a0b6e16b62 100644
--- a/unit/solvers/refinement/string_refinement/dependency_graph.cpp
+++ b/unit/solvers/refinement/string_refinement/dependency_graph.cpp
@@ -3,7 +3,7 @@
  Module: Unit tests for dependency graph
    solvers/refinement/string_refinement.cpp
 
- Author: DiffBlue Limited. All rights reserved.
+ Author: DiffBlue Ltd.
 
 \*******************************************************************/
 
@@ -47,7 +47,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
 {
   GIVEN("dependency graph")
   {
-    string_dependenciest dependences;
+    string_dependenciest dependencies;
     refined_string_typet string_type(java_char_type(), java_int_type());
     const exprt string1 = make_string_argument("string1");
     const exprt string2 = make_string_argument("string2");
@@ -93,11 +93,11 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
       symbol_generatort generator;
       array_poolt array_pool(generator);
 
-      bool success = add_node(dependences, equation1, array_pool);
+      bool success = add_node(dependencies, equation1, array_pool);
       REQUIRE(success);
-      success = add_node(dependences, equation2, array_pool);
+      success = add_node(dependencies, equation2, array_pool);
       REQUIRE(success);
-      success = add_node(dependences, equation3, array_pool);
+      success = add_node(dependencies, equation3, array_pool);
       REQUIRE(success);
 
 #ifdef DEBUG // useful output for visualizing the graph
@@ -105,9 +105,7 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
         register_language(new_java_bytecode_language);
         symbol_tablet symbol_table;
         namespacet ns(symbol_table);
-        dependencies.output_dot(std::cerr, [&](const exprt &expr) { // NOLINT
-          return from_expr(ns, "", expr);
-        });
+        dependencies.output_dot(std::cerr);
       }
 #endif
 
@@ -141,53 +139,59 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
 
       THEN("string3 depends on primitive0")
       {
-        const auto &node = dependences.get_node(char_array3);
-        const std::vector<string_dependenciest::builtin_function_nodet>
-          &depends = dependences.dependencies(node);
-        REQUIRE(depends.size() == 1);
-        const auto &primitive0 = dependences.get_builtin_function(depends[0]);
-
-        THEN("primitive0 depends on string1 and string2")
-        {
-          const auto &depends2 = primitive0.string_arguments();
-          REQUIRE(depends2.size() == 2);
-          REQUIRE(depends2[0] == char_array1);
-          REQUIRE(depends2[1] == char_array2);
-        }
+        const auto &node = dependencies.get_node(char_array3);
+        std::size_t nb_dependencies = 0;
+        dependencies.for_each_dependency(
+          node,
+          [&](const string_dependenciest::builtin_function_nodet &n) { // NOLINT
+            nb_dependencies++;
+            THEN("primitive0 depends on string1 and string2")
+            {
+              const auto &depends2 = n.data->string_arguments();
+              REQUIRE(depends2.size() == 2);
+              REQUIRE(depends2[0] == char_array1);
+              REQUIRE(depends2[1] == char_array2);
+            }
+          });
+        REQUIRE(nb_dependencies == 1);
       }
 
       THEN("string5 depends on primitive1")
       {
-        const auto &node = dependences.get_node(char_array5);
-        const std::vector<string_dependenciest::builtin_function_nodet>
-          &depends = dependences.dependencies(node);
-        REQUIRE(depends.size() == 1);
-        const auto &primitive1 = dependences.get_builtin_function(depends[0]);
-
-        THEN("primitive1 depends on string3 and string4")
-        {
-          const auto &depends2 = primitive1.string_arguments();
-          REQUIRE(depends2.size() == 2);
-          REQUIRE(depends2[0] == char_array3);
-          REQUIRE(depends2[1] == char_array4);
-        }
+        const auto &node = dependencies.get_node(char_array5);
+        std::size_t nb_dependencies = 0;
+        dependencies.for_each_dependency(
+          node,
+          [&](const string_dependenciest::builtin_function_nodet &n) { // NOLINT
+            nb_dependencies++;
+            THEN("primitive1 depends on string3 and string4")
+            {
+              const auto &depends2 = n.data->string_arguments();
+              REQUIRE(depends2.size() == 2);
+              REQUIRE(depends2[0] == char_array3);
+              REQUIRE(depends2[1] == char_array4);
+            }
+          });
+        REQUIRE(nb_dependencies == 1);
       }
 
       THEN("string6 depends on primitive2")
       {
-        const auto &node = dependences.get_node(char_array6);
-        const std::vector<string_dependenciest::builtin_function_nodet>
-          &depends = dependences.dependencies(node);
-        REQUIRE(depends.size() == 1);
-        const auto &primitive2 = dependences.get_builtin_function(depends[0]);
-
-        THEN("primitive2 depends on string5 and string2")
-        {
-          const auto &depends2 = primitive2.string_arguments();
-          REQUIRE(depends2.size() == 2);
-          REQUIRE(depends2[0] == char_array5);
-          REQUIRE(depends2[1] == char_array2);
-        }
+        const auto &node = dependencies.get_node(char_array6);
+        std::size_t nb_dependencies = 0;
+        dependencies.for_each_dependency(
+          node,
+          [&](const string_dependenciest::builtin_function_nodet &n) { // NOLINT
+            nb_dependencies++;
+            THEN("primitive2 depends on string5 and string2")
+            {
+              const auto &depends2 = n.data->string_arguments();
+              REQUIRE(depends2.size() == 2);
+              REQUIRE(depends2[0] == char_array5);
+              REQUIRE(depends2[1] == char_array2);
+            }
+          });
+        REQUIRE(nb_dependencies == 1);
       }
     }
   }

From 8684e6df77871d8878f2784701fbca85506a42fb Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 23 Mar 2018 15:41:06 +0000
Subject: [PATCH 22/28] Helper functions for length constraints on strings

This defines functions adding constraints on length of strings.
This constraints are used in the add_axioms_* functions and the goal is
to reuse them in string dependencies, to add axioms only about the
length and not the content of the strings.
---
 .../refinement/string_constraint_generator.h  | 19 ++++++++
 .../string_constraint_generator_concat.cpp    | 48 ++++++++++++++++---
 .../string_constraint_generator_insert.cpp    | 14 +++++-
 3 files changed, 72 insertions(+), 9 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index 52d02ac9d6f..d30b7640529 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -444,4 +444,23 @@ exprt minimum(const exprt &a, const exprt &b);
 /// \return expression representing the maximum of two expressions
 exprt maximum(const exprt &a, const exprt &b);
 
+exprt length_constraint_for_concat_char(
+  const array_string_exprt &res,
+  const array_string_exprt &s1);
+exprt length_constraint_for_concat(
+  const array_string_exprt &res,
+  const array_string_exprt &s1,
+  const array_string_exprt &s2);
+exprt length_constraint_for_concat_substr(
+  const array_string_exprt &res,
+  const array_string_exprt &s1,
+  const array_string_exprt &s2,
+  const exprt &start_index,
+  const exprt &end_index);
+exprt length_constraint_for_insert(
+  const array_string_exprt &res,
+  const array_string_exprt &s1,
+  const array_string_exprt &s2,
+  const exprt &offset);
+
 #endif
diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp
index 6c258566351..d1cd743b32d 100644
--- a/src/solvers/refinement/string_constraint_generator_concat.cpp
+++ b/src/solvers/refinement/string_constraint_generator_concat.cpp
@@ -43,10 +43,8 @@ exprt string_constraint_generatort::add_axioms_for_concat_substr(
   const exprt end1 = maximum(minimum(end_index, s2.length()), start1);
 
   // Axiom 1.
-  lemmas.push_back([&] { // NOLINT
-    const plus_exprt res_length(s1.length(), minus_exprt(end1, start1));
-    return equal_exprt(res.length(), res_length);
-  }());
+  lemmas.push_back(
+    length_constraint_for_concat_substr(res, s1, s2, start_index, end_index));
 
   // Axiom 2.
   constraints.push_back([&] { // NOLINT
@@ -67,6 +65,34 @@ exprt string_constraint_generatort::add_axioms_for_concat_substr(
   return from_integer(0, get_return_code_type());
 }
 
+/// Add axioms enforcing that the length of `res` is that of the concatenation
+/// of `s1` with the substring of `s2` starting at index `start'`
+/// and ending at index `end'`.
+/// Where start_index' is max(0, start) and end' is
+/// max(min(end, s2.length), start')
+exprt length_constraint_for_concat_substr(
+  const array_string_exprt &res,
+  const array_string_exprt &s1,
+  const array_string_exprt &s2,
+  const exprt &start,
+  const exprt &end)
+{
+  const exprt start1 = maximum(start, from_integer(0, start.type()));
+  const exprt end1 = maximum(minimum(end, s2.length()), start1);
+  const plus_exprt res_length(s1.length(), minus_exprt(end1, start1));
+  return equal_exprt(res.length(), res_length);
+}
+
+/// Add axioms enforcing that the length of `res` is that of the concatenation
+/// of `s1` with `s2`
+exprt length_constraint_for_concat(
+  const array_string_exprt &res,
+  const array_string_exprt &s1,
+  const array_string_exprt &s2)
+{
+  return equal_exprt(res.length(), plus_exprt(s1.length(), s2.length()));
+}
+
 /// Add axioms enforcing that `res` is the concatenation of `s1` with
 /// character `c`.
 /// These axioms are :
@@ -84,9 +110,7 @@ exprt string_constraint_generatort::add_axioms_for_concat_char(
   const exprt &c)
 {
   const typet &index_type = res.length().type();
-  const equal_exprt a1(
-    res.length(), plus_exprt(s1.length(), from_integer(1, index_type)));
-  lemmas.push_back(a1);
+  lemmas.push_back(length_constraint_for_concat_char(res, s1));
 
   symbol_exprt idx = fresh_univ_index("QA_index_concat_char", index_type);
   string_constraintt a2(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
@@ -99,6 +123,16 @@ exprt string_constraint_generatort::add_axioms_for_concat_char(
   return from_integer(0, get_return_code_type());
 }
 
+/// Add axioms enforcing that the length of `res` is that of the concatenation
+/// of `s1` with
+exprt length_constraint_for_concat_char(
+  const array_string_exprt &res,
+  const array_string_exprt &s1)
+{
+  return equal_exprt(
+    res.length(), plus_exprt(s1.length(), from_integer(1, s1.length().type())));
+}
+
 /// Add axioms enforcing that `res` is equal to the concatenation of `s1` and
 /// `s2`.
 ///
diff --git a/src/solvers/refinement/string_constraint_generator_insert.cpp b/src/solvers/refinement/string_constraint_generator_insert.cpp
index 34a57515ff4..37791fe2932 100644
--- a/src/solvers/refinement/string_constraint_generator_insert.cpp
+++ b/src/solvers/refinement/string_constraint_generator_insert.cpp
@@ -40,8 +40,7 @@ exprt string_constraint_generatort::add_axioms_for_insert(
     maximum(from_integer(0, index_type), minimum(s1.length(), offset));
 
   // Axiom 1.
-  lemmas.push_back(
-    equal_exprt(res.length(), plus_exprt(s1.length(), s2.length())));
+  lemmas.push_back(length_constraint_for_insert(res, s1, s2, offset));
 
   // Axiom 2.
   constraints.push_back([&] { // NOLINT
@@ -69,6 +68,17 @@ exprt string_constraint_generatort::add_axioms_for_insert(
   return from_integer(0, get_return_code_type());
 }
 
+/// Add axioms ensuring the length of `res` corresponds that of `s1` where we
+/// inserted `s2` at position `offset`.
+exprt length_constraint_for_insert(
+  const array_string_exprt &res,
+  const array_string_exprt &s1,
+  const array_string_exprt &s2,
+  const exprt &offset)
+{
+  return equal_exprt(res.length(), plus_exprt(s1.length(), s2.length()));
+}
+
 /// Insertion of a string in another at a specific index
 ///
 /// \copybrief string_constraint_generatort::add_axioms_for_insert(

From 61b39109ab1c128c5ae2e7af4fb6b00a89a7d5f5 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 23 Mar 2018 15:43:07 +0000
Subject: [PATCH 23/28] Add length_constraint method to builtin functions

This give the constraints that ensure the length of the result of a
buitin function is correct. Will be used when we don't need the
constraints about the actual content of the strings.
---
 .../refinement/string_builtin_function.h      | 37 ++++++++++++++++++-
 1 file changed, 36 insertions(+), 1 deletion(-)

diff --git a/src/solvers/refinement/string_builtin_function.h b/src/solvers/refinement/string_builtin_function.h
index 4c2642e88f3..c6fad6b57da 100644
--- a/src/solvers/refinement/string_builtin_function.h
+++ b/src/solvers/refinement/string_builtin_function.h
@@ -38,6 +38,10 @@ class string_builtin_functiont
   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
@@ -128,7 +132,12 @@ 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]);
-  };
+  }
+
+  exprt length_constraint() const override
+  {
+    return length_constraint_for_concat_char(result, input);
+  }
 };
 
 /// String inserting a string into another one
@@ -183,6 +192,15 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
     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;
@@ -229,6 +247,16 @@ class string_concatenation_builtin_functiont final
         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
@@ -303,6 +331,13 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont
   {
     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

From 805f45fc55a067c7367e468f4508c17f3efc533b Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 23 Mar 2018 15:45:02 +0000
Subject: [PATCH 24/28] Correct add_constraints in string_dependencies

When the result of a function is not tested we don't need to add full
constraints, but constraints about the length may still be necessary as
the length field of the string can be accessed directly.
---
 src/solvers/refinement/string_refinement_util.cpp | 6 ++++--
 src/solvers/refinement/string_refinement_util.h   | 3 +++
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index ed8a5894b3a..99f1e2f5c09 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -442,13 +442,15 @@ void string_dependenciest::add_constraints(
       for_each_successor(n, f);
     });
 
-  for(const auto &node : test_dependencies)
+  for(const auto &node : builtin_function_nodes)
   {
-    if(node.kind == node.BUILTIN)
+    if(test_dependencies.count(nodet(node)))
     {
       const auto &builtin = builtin_function_nodes[node.index];
       const exprt return_value = builtin.data->add_constraints(generator);
       generator.add_lemma(equal_exprt(return_value, builtin.data->return_code));
     }
+    else
+      generator.add_lemma(node.data->length_constraint());
   }
 }
diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h
index 1014f14d2b2..e8f7b615e8f 100644
--- a/src/solvers/refinement/string_refinement_util.h
+++ b/src/solvers/refinement/string_refinement_util.h
@@ -238,6 +238,9 @@ class string_dependenciest
 
   void output_dot(std::ostream &stream) const;
 
+  /// For all builtin call on which a test (or an unsupported buitin)
+  /// result depends, add the corresponding constraints. For the other builtin
+  /// only add constraints on the length.
   void add_constraints(string_constraint_generatort &generatort);
 
 private:

From 0bb2fad0409d6414df9077b9e1291f7937082909 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 23 Mar 2018 16:37:53 +0000
Subject: [PATCH 25/28] Define a for_each_atomic_string helper function

This could be used in several places in this file.
---
 .../refinement/string_refinement_util.cpp     | 33 ++++++++++++-------
 1 file changed, 22 insertions(+), 11 deletions(-)

diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index 99f1e2f5c09..d8196620024 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -20,6 +20,12 @@
 #include <unordered_set>
 #include "string_refinement_util.h"
 
+/// Applies `f` on all strings contained in `e` that are not if-expressions.
+/// For instance on input `cond1?s1:cond2?s2:s3` we apply `f` on s1, s2 and s3.
+static void for_each_atomic_string(
+  const array_string_exprt &e,
+  const std::function<void(const array_string_exprt &)> f);
+
 bool is_char_type(const typet &type)
 {
   return type.id() == ID_unsignedbv &&
@@ -225,21 +231,26 @@ const string_builtin_functiont &string_dependenciest::get_builtin_function(
   return *node.data;
 }
 
+static void for_each_atomic_string(
+  const array_string_exprt &e,
+  const std::function<void(const array_string_exprt &)> f)
+{
+  if(e.id() != ID_if)
+    return f(e);
+
+  const auto if_expr = to_if_expr(e);
+  for_each_atomic_string(to_array_string_expr(if_expr.true_case()), f);
+  for_each_atomic_string(to_array_string_expr(if_expr.false_case()), f);
+}
+
 void string_dependenciest::add_dependency(
   const array_string_exprt &e,
   const builtin_function_nodet &builtin_function_node)
 {
-  if(e.id() == ID_if)
-  {
-    const auto if_expr = to_if_expr(e);
-    const auto &true_case = to_array_string_expr(if_expr.true_case());
-    const auto &false_case = to_array_string_expr(if_expr.false_case());
-    add_dependency(true_case, builtin_function_node);
-    add_dependency(false_case, builtin_function_node);
-    return;
-  }
-  string_nodet &string_node = get_node(e);
-  string_node.dependencies.push_back(builtin_function_node.index);
+  for_each_atomic_string(e, [&](const array_string_exprt &s) { //NOLINT
+    string_nodet &string_node = get_node(s);
+    string_node.dependencies.push_back(builtin_function_node.index);
+  });
 }
 
 static void add_dependency_to_string_subexprs(

From 367ca134bc0416dd84069631e925e769669a2f51 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 23 Mar 2018 16:40:49 +0000
Subject: [PATCH 26/28] Ensure all atomic strings in arguments have node

We make sure a node is created for each atomic string in arguments of
builtin functions. This allows us to restablish the check that a node
exists for each dependency of a builtin function.
---
 src/solvers/refinement/string_refinement_util.cpp | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index d8196620024..0175984f4b5 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -339,6 +339,15 @@ bool add_node(
     dependencies.add_dependency(*string_result, builtin_function_node);
     auto &node = dependencies.get_node(*string_result);
     node.result_from = builtin_function_node.index;
+
+    // Ensure all atomic strings in the argument have an associated node
+    for(const auto arg : builtin_function_node.data->string_arguments())
+    {
+      for_each_atomic_string(
+        arg, [&](const array_string_exprt &atomic) { // NOLINT
+          (void)dependencies.get_node(atomic);
+        });
+    }
   }
   else
     add_dependency_to_string_subexprs(
@@ -366,10 +375,7 @@ void string_dependenciest::for_each_dependency(
       else if(const auto string_node = node_at(to_array_string_expr(current)))
         f(*string_node);
       else
-      {
-        std::cout << "Warning no node for " << format(current) << std::endl;
-        //UNREACHABLE;
-      }
+        UNREACHABLE;
     }
   }
 }

From 50cfe345853e4526c102fdbb072b136fe695c0ab Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Sat, 24 Mar 2018 19:22:46 +0000
Subject: [PATCH 27/28] Clear constraints at each call to dec_solve

constraint_generator is kept as a class member because it is used by
get, but we need to make sure it is cleared at each dec_solve call so
that we don't keep unecessary or redundant constraints.
---
 src/solvers/refinement/string_constraint_generator.h       | 3 +++
 .../refinement/string_constraint_generator_main.cpp        | 7 +++++++
 src/solvers/refinement/string_refinement.cpp               | 6 ++++--
 3 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h
index d30b7640529..7fcd2d76574 100644
--- a/src/solvers/refinement/string_constraint_generator.h
+++ b/src/solvers/refinement/string_constraint_generator.h
@@ -110,6 +110,9 @@ class string_constraint_generatort final
   const std::vector<string_not_contains_constraintt> &
   get_not_contains_constraints() const;
 
+  /// Clear all constraints and lemmas
+  void clear_constraints();
+
   /// Boolean symbols for the results of some string functions
   const std::vector<symbol_exprt> &get_boolean_symbols() const;
 
diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
index ec29a940a0c..97c0287eb96 100644
--- a/src/solvers/refinement/string_constraint_generator_main.cpp
+++ b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -323,6 +323,13 @@ string_constraint_generatort::get_string_expr(const exprt &expr)
   return char_array_of_pointer(str.content(), str.length());
 }
 
+void string_constraint_generatort::clear_constraints()
+{
+  lemmas.clear();
+  constraints.clear();
+  not_contains_constraints.clear();
+}
+
 /// adds standard axioms about the length of the string and its content: * its
 /// length should be positive * it should not exceed max_string_length * if
 /// force_printable_characters is true then all characters should belong to the
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 52c7e8d7675..8cec89c46fb 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -639,6 +639,9 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       string_id_symbol_resolve.replace_expr(eq.rhs());
   }
 
+  // Generator is also used by get, so we have to use it as a class member
+  // but we make sure it is cleared at each `dec_solve` call.
+  generator.clear_constraints();
   make_char_array_pointer_associations(generator, equations);
 
 #ifdef DEBUG
@@ -658,8 +661,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 #endif
 
   debug() << "dec_solve: add constraints" << eom;
-  // Generator is also used by get, that's why we use a class member
-  dependencies.add_constraints(generator);
+ dependencies.add_constraints(generator);
 
 #ifdef DEBUG
   output_equations(debug(), equations, ns);

From 60bfbd03065353ae0d01cbba2934c9c4a61e9a85 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Sat, 24 Mar 2018 20:35:35 +0000
Subject: [PATCH 28/28] Reduce string-max-length on String.equals test

Execution time can vary depending on what the sat solver find as a
model at the refinement steps.
Observed execution time go from 0.2s to 7s.
Setting the limit to 100 limit these variations (maximum observed is
0.3s).
---
 regression/jbmc-strings/StringEquals/test.desc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/regression/jbmc-strings/StringEquals/test.desc b/regression/jbmc-strings/StringEquals/test.desc
index b71cf70c218..3e35d340082 100644
--- a/regression/jbmc-strings/StringEquals/test.desc
+++ b/regression/jbmc-strings/StringEquals/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