Add c-specific refinement utils

For handling byte-extract expression, string-constants etc., in places that
expect string arrays. Also slightly extend the definition of char-type.

Author: hannes-steffenhagen-diffblue

src/solvers/strings/string_refinement_util.cpp

@@ -14,19 +14,27 @@ Author: Diffblue Ltd.
 #include <numeric>
 #include <unordered_set>
 #include <util/arith_tools.h>
+#include <util/expr_cast.h>
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
 #include <util/graph.h>
 #include <util/magic.h>
 #include <util/make_unique.h>
 #include <util/ssa_expr.h>
-#include <util/std_expr.h>
+#include <util/string2int.h>
+#include <util/string_constant.h>
 #include <util/unicode.h>
 
 bool is_char_type(const typet &type)
 {
-  return type.id() == ID_unsignedbv && to_unsignedbv_type(type).get_width() <=
-                                         STRING_REFINEMENT_MAX_CHAR_WIDTH;
+  if(type.id() == ID_unsignedbv)
+    return to_unsignedbv_type(type).get_width() <=
+           STRING_REFINEMENT_MAX_CHAR_WIDTH;
+
+  if(type.id() == ID_signedbv)
+    return to_signedbv_type(type).get_width() <= 8;
+
+  return false;
 }
 
 bool is_char_array_type(const typet &type, const namespacet &ns)
@@ -192,3 +200,68 @@ array_exprt interval_sparse_arrayt::concretize(
     size, it == entries.end() ? default_value : it->second);
   return array;
 }
+
+exprt maybe_byte_extract_expr(const exprt &expr)
+{
+  if(!can_cast_expr<byte_extract_exprt>(expr))
+    return expr;
+
+  const auto &byte_extract_expr = to_byte_extract_expr(expr);
+  const auto &offset = byte_extract_expr.offset();
+  PRECONDITION(offset.id() == ID_constant);
+  if(offset.id() != ID_constant)
+  {
+    return expr;
+  }
+  const auto &constant_offset = to_constant_expr(offset);
+  const auto &op = byte_extract_expr.op();
+  auto numeric_offset =
+    string2optional_int(id2string(constant_offset.get_value()));
+  PRECONDITION(numeric_offset.has_value());
+  if(*numeric_offset == 0)
+  {
+    return op;
+  }
+
+  array_exprt::operandst offset_operands;
+  offset_operands.insert(
+    offset_operands.end(),
+    op.operands().begin() + *numeric_offset,
+    op.operands().end());
+  const auto extracted_array_suffix =
+    array_exprt{offset_operands, to_array_type(op.type())};
+
+  return extracted_array_suffix;
+}
+
+exprt maybe_remove_string_exprs(const exprt &expr)
+{
+  return [&]() {
+    if(
+      auto const &maybe_string_constant =
+        expr_try_dynamic_cast<string_constantt>(expr))
+    {
+      return static_cast<const exprt &>(maybe_string_constant->to_array_expr());
+    }
+    else
+    {
+      return expr;
+    }
+  }();
+}
+
+exprt massage_weird_arrays_into_non_weird_arrays(const exprt &expr)
+{
+  auto const byte_extracted = maybe_byte_extract_expr(expr);
+  auto const string_removed = maybe_remove_string_exprs(byte_extracted);
+  PRECONDITION(string_removed.type().id() == ID_array);
+  if(string_removed.id() == ID_if)
+  {
+    return if_exprt{
+      string_removed.op0(),
+      massage_weird_arrays_into_non_weird_arrays(string_removed.op1()),
+      massage_weird_arrays_into_non_weird_arrays(string_removed.op2()),
+      string_removed.type()};
+  }
+  return string_removed;
+}

src/solvers/strings/string_refinement_util.h

@@ -140,4 +140,9 @@ class interval_sparse_arrayt final : public sparse_arrayt
   }
 };
 
+exprt maybe_remove_string_exprs(const exprt &expr);
+
+exprt maybe_byte_extract_expr(const exprt &expr);
+
+exprt massage_weird_arrays_into_non_weird_arrays(const exprt &expr);
 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H