Class for string builtin functions and dependences

String builtin functions can be initialized from
function_application_exprt for some function names, for now only
cprover_string_concat_func and cprover_string_insert_func are supported
but this could be extended to all builtin functoins supported by the
solver.

We use information of string argument and return values of the
functions for creating a dependency graph between the strings, stored
in the string dependences structure.

We also define indexes in the dependency graph so that we can reuse
generic algorithms of util/graph.

Author: romainbrenguier

src/solvers/refinement/string_refinement.cpp

@@ -287,6 +287,23 @@ static void substitute_function_applications_in_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(
+  string_constraint_generatort &generator,
+  std::vector<equal_exprt> &equations)
+{
+  for(equal_exprt &eq : equations)
+  {
+    if(
+      const auto fun_app =
+        expr_try_dynamic_cast<function_application_exprt>(eq.rhs()))
+    {
+      if(const auto result = generator.make_array_pointer_association(*fun_app))
+        eq.rhs() = *result;
+    }
+  }
+}
 
 void replace_symbols_in_equations(
   const union_find_replacet &symbol_resolve,
@@ -658,8 +675,17 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       string_id_symbol_resolve.replace_expr(eq.rhs());
   }
 
+  make_char_array_pointer_associations(generator, equations);
+
 #ifdef DEBUG
   output_equations(debug(), equations, ns);
+
+  string_dependencest dependences;
+  for(const equal_exprt &eq : equations)
+    add_node(dependences, eq, generator.array_pool);
+
+  debug() << "dec_solve: dependence graph:" << eom;
+  dependences.output_dot(debug());
 #endif
 
   debug() << "dec_solve: Replace function applications" << eom;
@@ -671,8 +697,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 
 #ifdef DEBUG
   debug() << "dec_solve: arrays_of_pointers:" << eom;
-  for(auto pair :
-      generator.array_pointer_correspondance.get_arrays_of_pointers())
+  for(auto pair : generator.array_pool.get_arrays_of_pointers())
   {
     debug() << "  * " << format(pair.first) << "\t--> " << format(pair.second)
             << " : " << format(pair.second.type()) << eom;

src/solvers/refinement/string_refinement_util.cpp

@@ -8,9 +8,13 @@
 
 #include <algorithm>
 #include <numeric>
+#include <functional>
+#include <iostream>
 #include <util/arith_tools.h>
+#include <util/ssa_expr.h>
 #include <util/std_expr.h>
 #include <util/expr_iterator.h>
+#include <util/graph.h>
 #include <util/magic.h>
 #include "string_refinement_util.h"
 
@@ -157,3 +161,270 @@ equation_symbol_mappingt::find_equations(const exprt &expr)
 {
   return equations_containing[expr];
 }
+
+string_insertion_builtin_functiont::string_insertion_builtin_functiont(
+  const std::vector<exprt> &fun_args,
+  array_poolt &array_pool)
+{
+  PRECONDITION(fun_args.size() > 3);
+  const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
+  input1 = array_pool.find(arg1.op1(), arg1.op0());
+  const auto arg2 = expr_checked_cast<struct_exprt>(fun_args[3]);
+  input2 = array_pool.find(arg2.op1(), arg2.op0());
+  result = array_pool.find(fun_args[1], fun_args[0]);
+  args.insert(args.end(), fun_args.begin() + 4, fun_args.end());
+}
+
+/// 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.
+static std::unique_ptr<string_builtin_functiont> to_string_builtin_function(
+  const function_application_exprt &fun_app,
+  array_poolt &array_pool)
+{
+  const auto name = expr_checked_cast<symbol_exprt>(fun_app.function());
+  const irep_idt &id = is_ssa_expr(name) ? to_ssa_expr(name).get_object_name()
+                                         : 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));
+
+  if(id == ID_cprover_string_concat_func)
+    return std::unique_ptr<string_builtin_functiont>(
+      new string_insertion_builtin_functiont(fun_app.arguments(), array_pool));
+
+  return {};
+}
+
+string_dependencest::string_nodet &
+string_dependencest::get_node(const array_string_exprt &e)
+{
+  auto entry_inserted = node_index_pool.emplace(e, string_nodes.size());
+  if(!entry_inserted.second)
+    return string_nodes[entry_inserted.first->second];
+
+  string_nodes.emplace_back();
+  return string_nodes.back();
+}
+
+string_dependencest::builtin_function_nodet string_dependencest::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;
+}
+
+const string_builtin_functiont &string_dependencest::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_dependencest::builtin_function_nodet> &
+string_dependencest::dependencies(
+  const string_dependencest::string_nodet &node) const
+{
+  return node.dependencies;
+}
+
+void string_dependencest::add_dependency(
+  const array_string_exprt &e,
+  const builtin_function_nodet &builtin_function_node)
+{
+  string_nodet &string_node = get_node(e);
+  string_node.dependencies.push_back(builtin_function_node);
+}
+
+void string_dependencest::add_unknown_dependency(const array_string_exprt &e)
+{
+  string_nodet &string_node = get_node(e);
+  string_node.depends_on_unknown_builtin_function = true;
+}
+
+static void add_unknown_dependency_to_string_subexprs(
+  string_dependencest &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
+        const auto &string_struct = expr_try_dynamic_cast<struct_exprt>(e);
+        if(string_struct && string_struct->operands().size() == 2)
+        {
+          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_dependencest &dependencies,
+  const function_application_exprt &fun_app,
+  const string_dependencest::builtin_function_nodet &builtin_function_node,
+  array_poolt &array_pool)
+{
+  PRECONDITION(fun_app.arguments()[0].type().id() != ID_pointer);
+  if(
+    fun_app.arguments().size() > 1 &&
+    fun_app.arguments()[1].type().id() == ID_pointer)
+  {
+    // Case where the result is given as a pointer argument
+    const array_string_exprt string =
+      array_pool.find(fun_app.arguments()[1], fun_app.arguments()[0]);
+    dependencies.add_dependency(string, builtin_function_node);
+  }
+
+  for(const auto &expr : fun_app.arguments())
+  {
+    std::for_each(
+      expr.depth_begin(),
+      expr.depth_end(),
+      [&](const exprt &e) { // NOLINT
+        if(const auto structure = expr_try_dynamic_cast<struct_exprt>(e))
+        {
+          const array_string_exprt string = array_pool.of_argument(*structure);
+          dependencies.add_dependency(string, builtin_function_node);
+        }
+      });
+  }
+}
+
+string_dependencest::node_indext string_dependencest::size() const
+{
+  return builtin_function_nodes.size() + string_nodes.size();
+}
+
+/// Convert an index of a string node in `string_nodes` to the node_indext for
+/// the same node
+static std::size_t string_index_to_node_index(const std::size_t string_index)
+{
+  return 2 * string_index + 1;
+}
+
+/// Convert an index of a builtin function node to the node_indext for
+/// the same node
+static std::size_t
+builtin_function_index_to_node_index(const std::size_t builtin_index)
+{
+  return 2 * builtin_index;
+}
+
+string_dependencest::node_indext
+string_dependencest::node_index(const builtin_function_nodet &n) const
+{
+  return builtin_function_index_to_node_index(n.index);
+}
+
+string_dependencest::node_indext
+string_dependencest::node_index(const array_string_exprt &s) const
+{
+  return string_index_to_node_index(node_index_pool.at(s));
+}
+
+optionalt<string_dependencest::builtin_function_nodet>
+string_dependencest::get_builtin_function_node(node_indext i) const
+{
+  if(i % 2 == 0)
+    return builtin_function_nodet(i / 2);
+  return {};
+}
+
+optionalt<string_dependencest::string_nodet>
+string_dependencest::get_string_node(node_indext i) const
+{
+  if(i % 2 == 1 && i / 2 < string_nodes.size())
+    return string_nodes[i / 2];
+  return {};
+}
+
+bool add_node(
+  string_dependencest &dependencies,
+  const equal_exprt &equation,
+  array_poolt &array_pool)
+{
+  const auto fun_app =
+    expr_try_dynamic_cast<function_application_exprt>(equation.rhs());
+  if(!fun_app)
+    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;
+  }
+
+  const auto &builtin_function_node = dependencies.make_node(builtin_function);
+  // Warning: `builtin_function` has been emptied and should not be used anymore
+
+  if(
+    const auto &string_result =
+      dependencies.get_builtin_function(builtin_function_node).string_result())
+    dependencies.add_dependency(*string_result, builtin_function_node);
+  else
+    add_dependency_to_string_subexprs(
+      dependencies, *fun_app, builtin_function_node, array_pool);
+
+  return true;
+}
+
+void string_dependencest::for_each_successor(
+  const std::size_t &i,
+  const std::function<void(const std::size_t &)> &f) const
+{
+  if(const auto &builtin_function_node = get_builtin_function_node(i))
+  {
+    const string_builtin_functiont &p =
+      get_builtin_function(*builtin_function_node);
+    std::for_each(
+      p.string_arguments().begin(),
+      p.string_arguments().end(),
+      [&](const array_string_exprt &s) { f(node_index(s)); });
+  }
+  else if(const auto &s = get_string_node(i))
+  {
+    std::for_each(
+      s->dependencies.begin(),
+      s->dependencies.end(),
+      [&](const builtin_function_nodet &p) { f(node_index(p)); });
+  }
+  else
+    UNREACHABLE;
+}
+
+void string_dependencest::output_dot(std::ostream &stream) const
+{
+  const auto for_each_node =
+    [&](const std::function<void(const std::size_t &)> &f) { // NOLINT
+      for(std::size_t i = 0; i < string_nodes.size(); ++i)
+        f(string_index_to_node_index(i));
+      for(std::size_t i = 0; i < builtin_function_nodes.size(); ++i)
+        f(builtin_function_index_to_node_index(i));
+    };
+
+  const auto for_each_succ = [&](
+    const std::size_t &i,
+    const std::function<void(const std::size_t &)> &f) { // NOLINT
+    for_each_successor(i, f);
+  };
+
+  const auto node_to_string = [&](const std::size_t &i) { // NOLINT
+    return std::to_string(i);
+  };
+  stream << "digraph dependencies {\n";
+  output_dot_generic<std::size_t>(
+    stream, for_each_node, for_each_succ, node_to_string);
+  stream << '}' << std::endl;
+}