Merge pull request #3248 from romainbrenguier/bugfix/char-array-in-string-solver

Bugfix/char array in string solver

Author: romainbrenguier

jbmc/src/java_bytecode/java_string_library_preprocess.h

@@ -37,7 +37,7 @@ class java_string_library_preprocesst:public messaget
   java_string_library_preprocesst()
     : char_type(java_char_type()),
       index_type(java_int_type()),
-      refined_string_type(index_type, char_type)
+      refined_string_type(index_type, pointer_type(char_type))
   {
   }
 

jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -36,7 +36,7 @@ class tt
   }
   refined_string_typet string_type() const
   {
-    return refined_string_typet(length_type(), char_type());
+    return refined_string_typet(length_type(), pointer_type(char_type()));
   }
   array_typet witness_type() const
   {

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

@@ -48,7 +48,8 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
   GIVEN("dependency graph")
   {
     string_dependenciest dependencies;
-    refined_string_typet string_type(java_char_type(), java_int_type());
+    const typet string_type =
+      refined_string_typet(java_int_type(), pointer_type(java_char_type()));
     const exprt string1 = make_string_argument("string1");
     const exprt string2 = make_string_argument("string2");
     const exprt string3 = make_string_argument("string3");

src/solvers/refinement/string_refinement.cpp

@@ -270,12 +270,15 @@ static void make_char_array_pointer_associations(
   }
 }
 
-void replace_symbols_in_equations(
-  const union_find_replacet &symbol_resolve,
-  std::vector<equal_exprt> &equations)
+/// Substitute sub-expressions in equation by representative elements of
+/// `symbol_resolve` whenever possible.
+/// Similar to `symbol_resolve.replace_expr` but doesn't mutate the expression
+/// and returns the transformed expression instead.
+static exprt
+replace_expr_copy(const union_find_replacet &symbol_resolve, exprt expr)
 {
-  for(equal_exprt &eq : equations)
-    symbol_resolve.replace_expr(eq);
+  symbol_resolve.replace_expr(expr);
+  return expr;
 }
 
 /// Record the constraints to ensure that the expression is true when
@@ -301,20 +304,22 @@ void string_refinementt::set_to(const exprt &expr, bool value)
 }
 
 /// Add association for each char pointer in the equation
+/// \param symbol_solver: a union_find_replacet object to keep track of
+///   char pointer equations
 /// \param equations: vector of equations
 /// \param ns: namespace
 /// \param stream: output stream
 /// \return union_find_replacet where char pointer that have been set equal
 ///         by an equation are associated to the same element
-static union_find_replacet generate_symbol_resolution_from_equations(
+static void add_equations_for_symbol_resolution(
+  union_find_replacet &symbol_solver,
   const std::vector<equal_exprt> &equations,
   const namespacet &ns,
   messaget::mstreamt &stream)
 {
   const auto eom = messaget::eom;
   const std::string log_message =
     "WARNING string_refinement.cpp generate_symbol_resolution_from_equations:";
-  union_find_replacet solver;
   for(const equal_exprt &eq : equations)
   {
     const exprt &lhs = eq.lhs();
@@ -335,7 +340,7 @@ static union_find_replacet generate_symbol_resolution_from_equations(
 
     if(is_char_pointer_type(rhs.type()))
     {
-      solver.make_union(lhs, rhs);
+      symbol_solver.make_union(lhs, rhs);
     }
     else if(rhs.id() == ID_function_application)
     {
@@ -355,7 +360,7 @@ static union_find_replacet generate_symbol_resolution_from_equations(
             const member_exprt lhs_data(lhs, comp.get_name(), comp.type());
             const exprt rhs_data = simplify_expr(
               member_exprt(rhs, comp.get_name(), comp.type()), ns);
-            solver.make_union(lhs_data, rhs_data);
+            symbol_solver.make_union(lhs_data, rhs_data);
           }
         }
       }
@@ -366,7 +371,6 @@ static union_find_replacet generate_symbol_resolution_from_equations(
       }
     }
   }
-  return solver;
 }
 
 /// This is meant to be used on the lhs of an equation with string subtype.
@@ -613,9 +617,9 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 #endif
 
   debug() << "dec_solve: Build symbol solver from equations" << eom;
-  // This is used by get, that's why we use a class member here
-  symbol_resolve =
-    generate_symbol_resolution_from_equations(equations, ns, debug());
+  // symbol_resolve is used by get and is kept between calls to dec_solve,
+  // that's why we use a class member here
+  add_equations_for_symbol_resolution(symbol_resolve, equations, ns, debug());
 #ifdef DEBUG
   debug() << "symbol resolve:" << eom;
   for(const auto &pair : symbol_resolve.to_vector())
@@ -632,9 +636,6 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   }
 #endif
 
-  debug() << "dec_solve: Replacing char pointer symbols" << eom;
-  replace_symbols_in_equations(symbol_resolve, equations);
-
   debug() << "dec_solve: Replacing string ids in function applications" << eom;
   for(equal_exprt &eq : equations)
   {
@@ -653,10 +654,18 @@ decision_proceduret::resultt string_refinementt::dec_solve()
 
   debug() << "dec_solve: compute dependency graph and remove function "
           << "applications captured by the dependencies:" << eom;
-  std::vector<exprt> local_equations;
+  std::vector<equal_exprt> local_equations;
   for(const equal_exprt &eq : equations)
   {
-    if(!add_node(dependencies, eq, generator.array_pool))
+    // 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(
+      dependencies,
+      eq_with_char_array_replaced_with_representative_elements,
+      generator.array_pool);
+    if(!node_added)
       local_equations.push_back(eq);
   }
   equations.clear();

src/util/refined_string_type.cpp

@@ -21,10 +21,10 @@ Author: Romain Brenguier, [email protected]
 #include "std_expr.h"
 
 refined_string_typet::refined_string_typet(
-  const typet &index_type, const typet &char_type)
+  const typet &index_type,
+  const pointer_typet &content_type)
 {
-  array_typet char_array(char_type, infinity_exprt(index_type));
   components().emplace_back("length", index_type);
-  components().emplace_back("content", char_array);
+  components().emplace_back("content", content_type);
   set_tag(CPROVER_PREFIX"refined_string_type");
 }

src/util/refined_string_type.h

@@ -26,7 +26,9 @@ Author: Romain Brenguier, [email protected]
 class refined_string_typet: public struct_typet
 {
 public:
-  refined_string_typet(const typet &index_type, const typet &char_type);
+  refined_string_typet(
+    const typet &index_type,
+    const pointer_typet &content_type);
 
   // Type for the content (list of characters) of a string
   const array_typet &get_content_type() const

src/util/string_expr.h

@@ -198,7 +198,7 @@ class refined_string_exprt : public struct_exprt,
     : refined_string_exprt(
         _length,
         _content,
-        refined_string_typet(_length.type(), _content.type()))
+        refined_string_typet(_length.type(), to_pointer_type(_content.type())))
   {
   }