Handle the c-specific cases in string refinement

extracting string arrays from byte-expressions and string constants, hiding the
`symex::args` renaming, etc.

Author: petr-bauch

src/solvers/strings/array_pool.cpp

@@ -7,6 +7,8 @@ Author: Romain Brenguier, [email protected]
 \*******************************************************************/
 
 #include "array_pool.h"
+#include "string_refinement_util.h"
+#include <util/pointer_predicates.h>
 
 symbol_exprt symbol_generatort::
 operator()(const irep_idt &prefix, const typet &type)
@@ -102,13 +104,15 @@ array_string_exprt array_poolt::make_char_array_for_char_pointer(
   const bool is_constant_array =
     char_pointer.id() == ID_address_of &&
     to_address_of_expr(char_pointer).object().id() == ID_index &&
-    to_index_expr(to_address_of_expr(char_pointer).object()).array().id() ==
-      ID_array;
+    (to_index_expr(to_address_of_expr(char_pointer).object()).array().id() ==
+       ID_array ||
+     to_index_expr(to_address_of_expr(char_pointer).object()).array().id() ==
+       ID_string_constant);
 
   if(is_constant_array)
   {
-    return to_array_string_expr(
-      to_index_expr(to_address_of_expr(char_pointer).object()).array());
+    return to_array_string_expr(massage_weird_arrays_into_non_weird_arrays(
+      to_index_expr(to_address_of_expr(char_pointer).object()).array()));
   }
   const std::string symbol_name = "char_array_" + id2string(char_pointer.id());
   const auto array_sym =
@@ -135,12 +139,19 @@ static void attempt_assign_length_from_type(
   std::unordered_map<array_string_exprt, exprt, irep_hash> &length_of_array,
   symbol_generatort &symbol_generator)
 {
-  DATA_INVARIANT(
-    array_expr.id() != ID_if,
-    "attempt_assign_length_from_type does not handle if exprts");
-  // This invariant seems always true, but I don't know why.
-  // If we find a case where this is violated, try calling
-  // attempt_assign_length_from_type on the true and false cases.
+  if(array_expr.id() == ID_if)
+  {
+    const auto &if_expr = to_if_expr(array_expr);
+    attempt_assign_length_from_type(
+      to_array_string_expr(if_expr.true_case()),
+      length_of_array,
+      symbol_generator);
+    attempt_assign_length_from_type(
+      to_array_string_expr(if_expr.false_case()),
+      length_of_array,
+      symbol_generator);
+    return;
+  }
   const exprt &size_from_type = to_array_type(array_expr.type()).size();
   const exprt &size_to_assign =
     size_from_type != infinity_exprt(size_from_type.type())
@@ -151,19 +162,25 @@ static void attempt_assign_length_from_type(
     length_of_array.emplace(array_expr, size_to_assign);
   INVARIANT(
     emplace_result.second,
-    "attempt_assign_length_from_type should only be called when no entry"
+    "attempt_assign_length_from_type should only be called when no entry "
     "for the array_string_exprt exists in the length_of_array map");
 }
 
 void array_poolt::insert(
   const exprt &pointer_expr,
   const array_string_exprt &array_expr)
 {
-  const auto it_bool =
+  const auto association_it = arrays_of_pointers.find(pointer_expr);
+  if(association_it != arrays_of_pointers.end())
+  {
+    INVARIANT(
+      association_it->second == array_expr,
+      "should not associate two different arrays to the same pointer");
+  }
+  else
+  {
     arrays_of_pointers.insert(std::make_pair(pointer_expr, array_expr));
-
-  INVARIANT(
-    it_bool.second, "should not associate two arrays to the same pointer");
+  }
 
   if(length_of_array.find(array_expr) == length_of_array.end())
   {

src/solvers/strings/string_constraint_generator_main.cpp

@@ -19,6 +19,7 @@ Author: Romain Brenguier, [email protected]
 
 #include "string_constraint_generator.h"
 #include "string_refinement_invariant.h"
+#include "string_refinement_util.h"
 
 #include <iterator>
 #include <limits>
@@ -68,8 +69,9 @@ exprt string_constraint_generatort::associate_array_to_pointer(
   /// \todo: we allow expression of the form of `arr[0]` instead of `arr` as
   ///        the array argument but this could go away.
   array_string_exprt array_expr = to_array_string_expr(
-    f.arguments()[0].id() == ID_index ? to_index_expr(f.arguments()[0]).array()
-                                      : f.arguments()[0]);
+    f.arguments()[0].id() == ID_index
+      ? to_index_expr(f.arguments()[0]).array()
+      : massage_weird_arrays_into_non_weird_arrays(f.arguments()[0]));
 
   const exprt &pointer_expr = f.arguments()[1];
   array_pool.insert(simplify_expr(pointer_expr, ns), array_expr);

src/solvers/strings/string_refinement.cpp

@@ -24,9 +24,11 @@ Author: Alberto Griggio, [email protected]
 #include <solvers/sat/satcheck.h>
 #include <stack>
 #include <unordered_set>
+#include <util/c_types.h>
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
 #include <util/magic.h>
+#include <util/prefix.h>
 #include <util/range.h>
 #include <util/simplify_expr.h>
 
@@ -327,6 +329,16 @@ static void add_equations_for_symbol_resolution(
       continue;
     }
 
+    if(
+      rhs.id() == ID_symbol &&
+      has_prefix(
+        id2string(to_symbol_expr(rhs).get_identifier()), "symex::args::"))
+    {
+      // Symex introduces a new name for non-constant arguments that it uses in
+      // trace building, we do not need it here for symbol resolve.
+      continue;
+    }
+
     if(is_char_pointer_type(rhs.type()))
     {
       symbol_solver.make_union(lhs, simplify_expr(rhs, ns));
@@ -1066,7 +1078,7 @@ static exprt get_char_array_and_concretize(
   const namespacet &ns,
   messaget::mstreamt &stream,
   const array_string_exprt &arr,
-  array_poolt &array_pool)
+  const array_poolt &array_pool)
 {
   stream << "- " << format(arr) << ":\n";
   stream << std::string(4, ' ') << "- type: " << format(arr.type())
@@ -1115,7 +1127,7 @@ void debug_model(
   const namespacet &ns,
   const std::function<exprt(const exprt &)> &super_get,
   const std::vector<symbol_exprt> &symbols,
-  array_poolt &array_pool)
+  const array_poolt &array_pool)
 {
   stream << "debug_model:" << '\n';
   for(const auto &pointer_array : generator.array_pool.get_arrays_of_pointers())
@@ -1201,7 +1213,8 @@ static optionalt<exprt> substitute_array_access(
   symbol_generatort &symbol_generator,
   const bool left_propagate)
 {
-  const exprt &array = index_expr.array();
+  const auto array =
+    massage_weird_arrays_into_non_weird_arrays(index_expr.array());
   if(auto array_of = expr_try_dynamic_cast<array_of_exprt>(array))
     return array_of->op();
   if(auto array_with = expr_try_dynamic_cast<with_exprt>(array))
@@ -1617,8 +1630,20 @@ static void initial_index_set(
   }
   if(auto ite = expr_try_dynamic_cast<if_exprt>(s))
   {
-    initial_index_set(index_set, ns, qvar, upper_bound, ite->true_case(), i);
-    initial_index_set(index_set, ns, qvar, upper_bound, ite->false_case(), i);
+    initial_index_set(
+      index_set,
+      ns,
+      qvar,
+      upper_bound,
+      massage_weird_arrays_into_non_weird_arrays(ite->true_case()),
+      i);
+    initial_index_set(
+      index_set,
+      ns,
+      qvar,
+      upper_bound,
+      massage_weird_arrays_into_non_weird_arrays(ite->false_case()),
+      i);
     return;
   }
   const minus_exprt u_minus_1(upper_bound, from_integer(1, upper_bound.type()));
@@ -1641,7 +1666,8 @@ static void initial_index_set(
     if(it->id() == ID_index && is_char_type(it->type()))
     {
       const auto &index_expr = to_index_expr(*it);
-      const auto &s = index_expr.array();
+      const auto s =
+        massage_weird_arrays_into_non_weird_arrays(index_expr.array());
       initial_index_set(index_set, ns, qvar, bound, s, index_expr.index());
       it.next_sibling_or_parent();
     }
@@ -1835,7 +1861,9 @@ exprt string_refinementt::get(const exprt &expr) const
       else
         UNREACHABLE;
     }
-    const auto array = supert::get(current.get());
+    const auto array =
+      massage_weird_arrays_into_non_weird_arrays(supert::get(current.get()));
+
     const auto index = get(index_expr->index());
 
     // If the underlying solver does not know about the existence of an array,

src/solvers/strings/string_refinement.h

@@ -56,6 +56,7 @@ Author: Alberto Griggio, [email protected]
 // it is not turned on by default and not all options are available.
 #define OPT_STRING_REFINEMENT_CBMC \
   "(refine-strings)" \
+  "(max-nondet-string-length):" \
   "(string-printable)"
 
 #define HELP_STRING_REFINEMENT_CBMC \

src/util/string_constant.h

@@ -50,4 +50,10 @@ inline string_constantt &to_string_constant(typet &type)
   return to_string_constant((exprt &)type);
 }
 
+template <>
+inline bool can_cast_expr<string_constantt>(const exprt &base)
+{
+  return base.id() == ID_string_constant;
+}
+
 #endif // CPROVER_ANSI_C_STRING_CONSTANT_H