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_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 "string_refinement_util.h"
 
 bool is_char_type(const typet &type)
@@ -169,3 +173,242 @@ 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
+{
+  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
+        if(const auto &string = get_char_array_of_argument(e))
+          dependencies.add_unknown_dependency(array_pool.find(*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();
+}
+
+string_dependencest::node_indext
+string_dependencest::node_index(const builtin_function_nodet &n) const
+{
+  return 2 * n.index;
+}
+
+string_dependencest::node_indext
+string_dependencest::node_index(const array_string_exprt &s) const
+{
+  return 2 * node_index_pool.at(s) + 1;
+}
+
+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,
+  std::function<std::string(const exprt &)> to_string) const
+{
+  stream << "digraph dependencies {\n";
+
+  output_dot_generic<std::size_t>(
+    stream,
+    (std::size_t)size(),
+    [&](
+      const std::size_t &i,
+      const std::function<void(const std::size_t &)> &f) { // NOLINT
+      for_each_successor(i, f);
+    });
+
+  stream << '}' << std::endl;
+}