Merge pull request #4069 from tautschnig/string-solver-simplify

String refinement must not rely on input equations to be simplified

Author: tautschnig

jbmc/regression/strings-smoke-tests/java_starts_with/test-no-simplify.desc

@@ -0,0 +1,14 @@
+CORE
+test_starts_with.class
+--verbosity 10 --max-nondet-string-length 1000 --function test_starts_with.main --unwind 1 --no-simplify
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 8.* SUCCESS$
+^\[.*assertion.2\].* line 9.* FAILURE$
+--
+non equal types
+--
+This test must also pass when not running simplification during goto-symex
+(--no-simplify). Prior to the changes in this commit the test would yield wrong
+results for either line 8, because the string solver was not able to identify
+the string object in a non-simplified expression.

src/solvers/strings/string_constraint_generator_main.cpp

@@ -26,6 +26,7 @@ Author: Romain Brenguier, [email protected]
 #include <util/arith_tools.h>
 #include <util/deprecate.h>
 #include <util/pointer_predicates.h>
+#include <util/simplify_expr.h>
 #include <util/ssa_expr.h>
 #include <util/string_constant.h>
 
@@ -180,7 +181,7 @@ exprt string_constraint_generatort::associate_array_to_pointer(
                                       : f.arguments()[0]);
 
   const exprt &pointer_expr = f.arguments()[1];
-  array_pool.insert(pointer_expr, array_expr);
+  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());
 }

src/solvers/strings/string_refinement.cpp

@@ -339,7 +339,7 @@ static void add_equations_for_symbol_resolution(
 
     if(is_char_pointer_type(rhs.type()))
     {
-      symbol_solver.make_union(lhs, rhs);
+      symbol_solver.make_union(lhs, simplify_expr(rhs, ns));
     }
     else if(rhs.id() == ID_function_application)
     {
@@ -439,7 +439,7 @@ static void add_string_equation_to_symbol_resolution(
 {
   if(eq.rhs().type() == string_typet())
   {
-    symbol_resolve.make_union(eq.lhs(), eq.rhs());
+    symbol_resolve.make_union(eq.lhs(), simplify_expr(eq.rhs(), ns));
   }
   else if(has_subtype(eq.lhs().type(), ID_string, ns))
   {
@@ -646,7 +646,10 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   for(equal_exprt &eq : equations)
   {
     if(can_cast_expr<function_application_exprt>(eq.rhs()))
+    {
+      simplify(eq.rhs(), ns);
       string_id_symbol_resolve.replace_expr(eq.rhs());
+    }
   }
 
   // Generator is also used by get, so we have to use it as a class member