Handle more formulas than just equations in string solver

jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp

@@ -89,12 +89,15 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
       symbol_generatort generator;
       array_poolt array_pool(generator);
 
-      bool success = add_node(dependencies, equation1, array_pool);
-      REQUIRE(success);
-      success = add_node(dependencies, equation2, array_pool);
-      REQUIRE(success);
-      success = add_node(dependencies, equation3, array_pool);
-      REQUIRE(success);
+      optionalt<exprt> new_equation1 =
+        add_node(dependencies, equation1, array_pool, generator);
+      REQUIRE(new_equation1.has_value());
+      optionalt<exprt> new_equation2 =
+        add_node(dependencies, equation2, array_pool, generator);
+      REQUIRE(new_equation2.has_value());
+      optionalt<exprt> new_equation3 =
+        add_node(dependencies, equation3, array_pool, generator);
+      REQUIRE(new_equation3.has_value());
 
 #ifdef DEBUG // useful output for visualizing the graph
       {

src/solvers/strings/string_dependencies.cpp

@@ -90,7 +90,7 @@ string_dependenciest::node_at(const array_string_exprt &e) const
 }
 
 string_dependenciest::builtin_function_nodet &string_dependenciest::make_node(
-  std::unique_ptr<string_builtin_functiont> &builtin_function)
+  std::unique_ptr<string_builtin_functiont> builtin_function)
 {
   builtin_function_nodes.emplace_back(
     std::move(builtin_function), builtin_function_nodes.size());
@@ -195,22 +195,39 @@ void string_dependenciest::clean_cache()
     e.reset();
 }
 
-bool add_node(
+optionalt<exprt> add_node(
   string_dependenciest &dependencies,
-  const equal_exprt &equation,
-  array_poolt &array_pool)
+  const exprt &expr,
+  array_poolt &array_pool,
+  symbol_generatort &fresh_symbol)
 {
-  const auto fun_app =
-    expr_try_dynamic_cast<function_application_exprt>(equation.rhs());
+  const auto fun_app = expr_try_dynamic_cast<function_application_exprt>(expr);
   if(!fun_app)
-    return false;
+  {
+    exprt copy = expr;
+    bool copy_differs_from_expr = false;
+    for(std::size_t i = 0; i < expr.operands().size(); ++i)
+    {
+      auto new_op =
+        add_node(dependencies, expr.operands()[i], array_pool, fresh_symbol);
+      if(new_op)
+      {
+        copy.operands()[i] = *new_op;
+        copy_differs_from_expr = true;
+      }
+    }
+    if(copy_differs_from_expr)
+      return copy;
+    return {};
+  }
 
+  const exprt return_code = fresh_symbol("string_builtin_return", expr.type());
   auto builtin_function =
-    to_string_builtin_function(*fun_app, equation.lhs(), array_pool);
+    to_string_builtin_function(*fun_app, return_code, 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
+  const auto &builtin_function_node =
+    dependencies.make_node(std::move(builtin_function));
 
   if(
     const auto &string_result =
@@ -233,7 +250,7 @@ bool add_node(
     add_dependency_to_string_subexprs(
       dependencies, *fun_app, builtin_function_node, array_pool);
 
-  return true;
+  return return_code;
 }
 
 void string_dependenciest::for_each_dependency(

src/solvers/strings/string_dependencies.h

@@ -79,9 +79,8 @@ class string_dependenciest
   std::unique_ptr<const string_nodet>
   node_at(const array_string_exprt &e) const;
 
-  /// `builtin_function` is reset to an empty pointer after the node is created
   builtin_function_nodet &
-  make_node(std::unique_ptr<string_builtin_functiont> &builtin_function);
+  make_node(std::unique_ptr<string_builtin_functiont> builtin_function);
   const string_builtin_functiont &
   get_builtin_function(const builtin_function_nodet &node) const;
 
@@ -183,22 +182,27 @@ class string_dependenciest
     const std::function<void(const nodet &)> &f) const;
 };
 
-/// When right hand side of equation is a builtin_function add
+/// When a sub-expression of \p expr is a builtin_function, add
 /// a "string_builtin_function" node to the graph and connect it to the strings
 /// on which it depends and which depends on it.
 /// If the string builtin_function is not a supported one, mark all the string
 /// arguments as depending on an unknown builtin_function.
 /// \param dependencies: graph to which we add the node
-/// \param equation: an equation whose right hand side is possibly a call to a
+/// \param expr: an expression which may contain a call to a
 ///   string builtin_function.
 /// \param array_pool: array pool containing arrays corresponding to the string
 ///   exprt arguments of the builtin_function call
-/// \return true if a node was added, if false is returned it either means that
-///   the right hand side is not a function application
+/// \param fresh_symbol: used to create new symbols for the return values of
+///   builtin functions
+/// \return An expression in which function applications have been replaced
+///   by symbols corresponding to the `return_value` field of the associated
+///   builtin function. Or an empty optional when no function applications has
+///   been encountered
 /// \todo there should be a class with just the three functions we require here
-bool add_node(
+optionalt<exprt> add_node(
   string_dependenciest &dependencies,
-  const equal_exprt &equation,
-  array_poolt &array_pool);
+  const exprt &expr,
+  array_poolt &array_pool,
+  symbol_generatort &fresh_symbol);
 
 #endif // CPROVER_SOLVERS_STRINGS_STRING_DEPENDENCIES_H

src/solvers/strings/string_refinement.cpp

@@ -27,6 +27,7 @@ Author: Alberto Griggio, [email protected]
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
 #include <util/magic.h>
+#include <util/range.h>
 #include <util/simplify_expr.h>
 
 #include "equation_symbol_mapping.h"
@@ -239,23 +240,24 @@ static std::vector<exprt> generate_instantiations(
   return lemmas;
 }
 
-/// Fill the array_pointer correspondence and replace the right hand sides of
-/// the corresponding equations
+/// If \p expr is an equation whose right-hand-side is a
+/// associate_array_to_pointer call, add the correspondence and replace the call
+/// by an expression representing its result.
 static void make_char_array_pointer_associations(
   string_constraint_generatort &generator,
-  std::vector<equal_exprt> &equations)
+  exprt &expr)
 {
-  for(equal_exprt &eq : equations)
+  if(const auto equal_expr = expr_try_dynamic_cast<equal_exprt>(expr))
   {
     if(
-      const auto fun_app =
-        expr_try_dynamic_cast<function_application_exprt>(eq.rhs()))
+      const auto fun_app = expr_try_dynamic_cast<function_application_exprt>(
+        as_const(equal_expr->rhs())))
     {
       const auto new_equation =
-        generator.make_array_pointer_association(eq.lhs(), *fun_app);
+        generator.make_array_pointer_association(equal_expr->lhs(), *fun_app);
       if(new_equation)
       {
-        eq =
+        expr =
           equal_exprt{from_integer(true, new_equation->type()), *new_equation};
       }
     }
@@ -281,18 +283,10 @@ void string_refinementt::set_to(const exprt &expr, bool value)
 {
   PRECONDITION(expr.type().id() == ID_bool);
   PRECONDITION(equality_propagation);
-
-  if(expr.id() == ID_equal && value)
-  {
-    const equal_exprt &eq_expr = to_equal_expr(expr);
-    equations.push_back(eq_expr);
-  }
+  if(!value)
+    equations.push_back(not_exprt{expr});
   else
-  {
-    INVARIANT(
-      !has_char_array_subexpr(expr, ns), "char array only appear in equations");
-    supert::set_to(expr, value);
-  }
+    equations.push_back(expr);
 }
 
 /// Add association for each char pointer in the equation
@@ -305,16 +299,19 @@ void string_refinementt::set_to(const exprt &expr, bool value)
 ///   by an equation are associated to the same element
 static void add_equations_for_symbol_resolution(
   union_find_replacet &symbol_solver,
-  const std::vector<equal_exprt> &equations,
+  const std::vector<exprt> &equations,
   const namespacet &ns,
   messaget::mstreamt &stream)
 {
   const std::string log_message =
     "WARNING string_refinement.cpp generate_symbol_resolution_from_equations:";
-  for(const equal_exprt &eq : equations)
+  auto equalities = make_range(equations).filter(
+    [&](const exprt &e) { return can_cast_expr<equal_exprt>(e); });
+  for(const exprt &e : equalities)
   {
-    const exprt &lhs = eq.lhs();
-    const exprt &rhs = eq.rhs();
+    const equal_exprt &eq = to_equal_expr(e);
+    const exprt &lhs = to_equal_expr(eq).lhs();
+    const exprt &rhs = to_equal_expr(eq).rhs();
     if(lhs.id() != ID_symbol)
     {
       stream << log_message << "non symbol lhs: " << format(lhs)
@@ -463,7 +460,7 @@ static void add_string_equation_to_symbol_resolution(
 /// \param stream: output stream
 /// \return union_find_replacet structure containing the correspondences.
 union_find_replacet string_identifiers_resolution_from_equations(
-  std::vector<equal_exprt> &equations,
+  const std::vector<equal_exprt> &equations,
   const namespacet &ns,
   messaget::mstreamt &stream)
 {
@@ -534,13 +531,11 @@ union_find_replacet string_identifiers_resolution_from_equations(
 
 #ifdef DEBUG
 /// Output a vector of equations to the given stream, used for debugging.
-static void output_equations(
-  std::ostream &output,
-  const std::vector<equal_exprt> &equations)
+static void
+output_equations(std::ostream &output, const std::vector<exprt> &equations)
 {
   for(std::size_t i = 0; i < equations.size(); ++i)
-    output << "  [" << i << "] " << format(equations[i].lhs())
-           << " == " << format(equations[i].rhs()) << std::endl;
+    output << "  [" << i << "] " << format(equations[i]) << std::endl;
 }
 #endif
 
@@ -629,7 +624,18 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 #endif
 
   const union_find_replacet string_id_symbol_resolve =
-    string_identifiers_resolution_from_equations(equations, ns, log.debug());
+    string_identifiers_resolution_from_equations(
+      [&] {
+        std::vector<equal_exprt> equalities;
+        for(const auto &eq : equations)
+        {
+          if(auto equal_expr = expr_try_dynamic_cast<equal_exprt>(eq))
+            equalities.push_back(*equal_expr);
+        }
+        return equalities;
+      }(),
+      ns,
+      log.debug());
 #ifdef DEBUG
   log.debug() << "symbol resolve string:" << messaget::eom;
   for(const auto &pair : string_id_symbol_resolve.to_vector())
@@ -639,39 +645,55 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   }
 #endif
 
-  log.debug() << "dec_solve: Replacing string ids in function applications"
+  log.debug() << "dec_solve: Replacing string ids and simplifying arguments"
+                 " in function applications"
               << messaget::eom;
-  for(equal_exprt &eq : equations)
+  for(exprt &expr : equations)
   {
-    if(can_cast_expr<function_application_exprt>(eq.rhs()))
+    auto it = expr.depth_begin();
+    while(it != expr.depth_end())
     {
-      simplify(eq.rhs(), ns);
-      string_id_symbol_resolve.replace_expr(eq.rhs());
+      if(can_cast_expr<function_application_exprt>(*it))
+      {
+        // Simplification is required because the array pool may not realize
+        // that an expression like
+        // `(unsignedbv[16]*)((signedbv[8]*)&constarray[0] + 0)` is the
+        // same pointer as `&constarray[0]
+        simplify(it.mutate(), ns);
+        string_id_symbol_resolve.replace_expr(it.mutate());
+        it.next_sibling_or_parent();
+      }
+      else
+        ++it;
     }
   }
 
   // Constraints start clear at each `dec_solve` call.
   string_constraintst constraints;
-  make_char_array_pointer_associations(generator, equations);
+  for(auto &expr : equations)
+    make_char_array_pointer_associations(generator, expr);
 
 #ifdef DEBUG
   output_equations(log.debug(), equations);
 #endif
 
   log.debug() << "dec_solve: compute dependency graph and remove function "
               << "applications captured by the dependencies:" << messaget::eom;
-  std::vector<equal_exprt> local_equations;
-  for(const equal_exprt &eq : equations)
+  std::vector<exprt> local_equations;
+  for(const exprt &eq : equations)
   {
     // Ensures that arrays that are equal, are associated to the same nodes
     // in the graph.
-    const equal_exprt eq_with_char_array_replaced_with_representative_elements =
-      to_equal_expr(replace_expr_copy(symbol_resolve, eq));
-    const bool node_added = add_node(
+    const exprt eq_with_char_array_replaced_with_representative_elements =
+      replace_expr_copy(symbol_resolve, eq);
+    const optionalt<exprt> new_equation = add_node(
       dependencies,
       eq_with_char_array_replaced_with_representative_elements,
-      generator.array_pool);
-    if(!node_added)
+      generator.array_pool,
+      generator.fresh_symbol);
+    if(new_equation)
+      local_equations.push_back(*new_equation);
+    else
       local_equations.push_back(eq);
   }
   equations.clear();

src/solvers/strings/string_refinement.h

@@ -111,7 +111,7 @@ class string_refinementt final : public bv_refinementt
   index_set_pairt index_sets;
   union_find_replacet symbol_resolve;
 
-  std::vector<equal_exprt> equations;
+  std::vector<exprt> equations;
 
   string_dependenciest dependencies;
 
@@ -122,7 +122,7 @@ exprt substitute_array_lists(exprt expr, std::size_t string_max_length);
 
 // Declaration required for unit-test:
 union_find_replacet string_identifiers_resolution_from_equations(
-  std::vector<equal_exprt> &equations,
+  const std::vector<equal_exprt> &equations,
   const namespacet &ns,
   messaget::mstreamt &stream);
 

unit/Makefile

@@ -57,6 +57,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/strings/string_format_builtin_function/length_of_decimal_int.cpp \
        solvers/strings/string_refinement/concretize_array.cpp \
        solvers/strings/string_refinement/sparse_array.cpp \
+       solvers/strings/string_refinement/string_refinement.cpp \
        solvers/strings/string_refinement/substitute_array_list.cpp \
        solvers/strings/string_refinement/union_find_replace.cpp \
        util/allocate_objects.cpp \

unit/solvers/strings/string_refinement/module_dependencies.txt

@@ -1,4 +1,5 @@
 solvers/refinement
+solvers/sat
 solvers/strings
 string_refinement
 testing-utils