Merge pull request #4995 from romainbrenguier/clean-up/string-constraint-generator

Clean up string constraint generator class

Author: romainbrenguier

src/solvers/strings/string_constraint_generator.h

@@ -37,9 +37,6 @@ struct string_constraintst final
   std::vector<exprt> existential;
   std::vector<string_constraintt> universal;
   std::vector<string_not_contains_constraintt> not_contains;
-
-  /// Clear all constraints
-  void clear();
 };
 
 void merge(string_constraintst &result, string_constraintst other);
@@ -60,23 +57,23 @@ class string_constraint_generatort final
 
   array_poolt array_pool;
 
-  string_constraintst constraints;
-
   const namespacet ns;
 
   /// Associate array to pointer, and array to length
   /// \return an expression if the given function application is one of
   ///   associate pointer and associate length
-  optionalt<exprt>
-  make_array_pointer_association(const function_application_exprt &expr);
+  optionalt<exprt> make_array_pointer_association(
+    const exprt &return_code,
+    const function_application_exprt &expr);
 
 private:
-  exprt associate_array_to_pointer(const function_application_exprt &f);
-
-  exprt associate_length_to_array(const function_application_exprt &f);
+  exprt associate_array_to_pointer(
+    const exprt &return_code,
+    const function_application_exprt &f);
 
-  // MEMBERS
-  const messaget message;
+  exprt associate_length_to_array(
+    const exprt &return_code,
+    const function_application_exprt &f);
 };
 
 // Type used by primitives to signal errors

src/solvers/strings/string_constraint_generator_main.cpp

@@ -55,9 +55,12 @@ exprt sum_overflows(const plus_exprt &sum)
 /// Insert in `array_pool` a binding from `ptr` to `arr`. If the length of `arr`
 /// is infinite, a new integer symbol is created and stored in `array_pool`.
 /// This also adds the default axioms for `arr`.
+/// \param return_code: expression which is assigned the result of the function
 /// \param f: a function application with argument a character array `arr` and
 ///   a character pointer `ptr`.
+/// \return a constraint
 exprt string_constraint_generatort::associate_array_to_pointer(
+  const exprt &return_code,
   const function_application_exprt &f)
 {
   PRECONDITION(f.arguments().size() == 2);
@@ -71,31 +74,26 @@ exprt string_constraint_generatort::associate_array_to_pointer(
   const exprt &pointer_expr = f.arguments()[1];
   array_pool.insert(simplify_expr(pointer_expr, ns), array_expr);
   // created_strings.emplace(to_array_string_expr(array_expr));
-  return from_integer(0, f.type());
+  return equal_exprt{return_code, from_integer(0, f.type())};
 }
 
 /// Associate an integer length to a char array.
 /// This adds an axiom ensuring that `arr.length` and `length` are equal.
+/// \param return_code: expression which is assigned the result of the function
 /// \param f: a function application with argument a character array `arr` and
 ///   an integer `length`.
-/// \return integer expression equal to 0
+/// \return a constraint
 exprt string_constraint_generatort::associate_length_to_array(
+  const exprt &return_code,
   const function_application_exprt &f)
 {
   PRECONDITION(f.arguments().size() == 2);
   array_string_exprt array_expr = to_array_string_expr(f.arguments()[0]);
   const exprt &new_length = f.arguments()[1];
 
   const auto &length = array_pool.get_or_create_length(array_expr);
-  constraints.existential.push_back(equal_exprt(length, new_length));
-  return from_integer(0, f.type());
-}
-
-void string_constraintst::clear()
-{
-  existential.clear();
-  universal.clear();
-  not_contains.clear();
+  return and_exprt{equal_exprt{return_code, from_integer(0, f.type())},
+                   equal_exprt(length, new_length)};
 }
 
 /// Merge two sets of constraints by appending to the first one
@@ -200,13 +198,14 @@ static irep_idt get_function_name(const function_application_exprt &expr)
 }
 
 optionalt<exprt> string_constraint_generatort::make_array_pointer_association(
+  const exprt &return_code,
   const function_application_exprt &expr)
 {
   const irep_idt &id = get_function_name(expr);
   if(id == ID_cprover_associate_array_to_pointer_func)
-    return associate_array_to_pointer(expr);
+    return associate_array_to_pointer(return_code, expr);
   else if(id == ID_cprover_associate_length_to_array_func)
-    return associate_length_to_array(expr);
+    return associate_length_to_array(return_code, expr);
   return {};
 }
 

src/solvers/strings/string_dependencies.cpp

@@ -328,8 +328,8 @@ void string_dependenciest::output_dot(std::ostream &stream) const
   stream << '}' << std::endl;
 }
 
-void string_dependenciest::add_constraints(
-  string_constraint_generatort &generator)
+string_constraintst
+string_dependenciest::add_constraints(string_constraint_generatort &generator)
 {
   std::unordered_set<nodet, node_hash> test_dependencies;
   for(const auto &builtin : builtin_function_nodes)
@@ -346,16 +346,16 @@ void string_dependenciest::add_constraints(
       for_each_successor(n, f);
     });
 
+  string_constraintst constraints;
   for(const auto &node : builtin_function_nodes)
   {
     if(test_dependencies.count(nodet(node)))
     {
       const auto &builtin = builtin_function_nodes[node.index];
-      string_constraintst constraints = builtin.data->constraints(generator);
-      merge(generator.constraints, std::move(constraints));
+      merge(constraints, builtin.data->constraints(generator));
     }
     else
-      generator.constraints.existential.push_back(
-        node.data->length_constraint());
+      constraints.existential.push_back(node.data->length_constraint());
   }
+  return constraints;
 }

src/solvers/strings/string_dependencies.h

@@ -14,6 +14,8 @@ Author: Diffblue Ltd.
 
 #include <memory>
 
+#include <util/nodiscard.h>
+
 #include "string_builtin_function.h"
 
 /// Keep track of dependencies between strings.
@@ -114,7 +116,8 @@ class string_dependenciest
   /// 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);
+  NODISCARD string_constraintst
+  add_constraints(string_constraint_generatort &generatort);
 
   /// Clear the content of the dependency graph
   void clear();

src/solvers/strings/string_refinement.cpp

@@ -251,8 +251,13 @@ static void make_char_array_pointer_associations(
       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;
+      const auto new_equation =
+        generator.make_array_pointer_association(eq.lhs(), *fun_app);
+      if(new_equation)
+      {
+        eq =
+          equal_exprt{from_integer(true, new_equation->type()), *new_equation};
+      }
     }
   }
 }
@@ -645,9 +650,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
     }
   }
 
-  // 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.constraints.clear();
+  // Constraints start clear at each `dec_solve` call.
+  string_constraintst constraints;
   make_char_array_pointer_associations(generator, equations);
 
 #ifdef DEBUG
@@ -677,7 +681,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 #endif
 
   log.debug() << "dec_solve: add constraints" << messaget::eom;
-  dependencies.add_constraints(generator);
+  merge(constraints, dependencies.add_constraints(generator));
 
 #ifdef DEBUG
   output_equations(log.debug(), equations);
@@ -702,8 +706,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   }
 
   std::transform(
-    generator.constraints.universal.begin(),
-    generator.constraints.universal.end(),
+    constraints.universal.begin(),
+    constraints.universal.end(),
     std::back_inserter(axioms.universal),
     [&](string_constraintt constraint) {
       constraint.replace_expr(symbol_resolve);
@@ -715,8 +719,8 @@ decision_proceduret::resultt string_refinementt::dec_solve()
     });
 
   std::transform(
-    generator.constraints.not_contains.begin(),
-    generator.constraints.not_contains.end(),
+    constraints.not_contains.begin(),
+    constraints.not_contains.end(),
     std::back_inserter(axioms.not_contains),
     [&](string_not_contains_constraintt axiom) {
       replace(symbol_resolve, axiom);
@@ -737,7 +741,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       nc_axiom, generator.fresh_symbol("not_contains_witness", witness_type));
   }
 
-  for(const exprt &lemma : generator.constraints.existential)
+  for(const exprt &lemma : constraints.existential)
   {
     add_lemma(substitute_array_access(lemma, generator.fresh_symbol, true));
   }