Add util for cleaning pointer argument expr

Clean the given pointer expression so that it has the right
shape for being used for identifying shadow memory.
This handles some quirks regarding array sizes containing
L2 symbols and string constants not having char-pointer type.

Author: peterschrammel

src/goto-symex/shadow_memory_util.cpp

@@ -11,8 +11,10 @@ Author: Peter Schrammel
 
 #include "shadow_memory_util.h"
 
+#include <util/c_types.h>
 #include <util/invariant.h>
 #include <util/pointer_expr.h>
+#include <util/ssa_expr.h>
 #include <util/std_expr.h>
 
 irep_idt extract_field_name(const exprt &string_expr)
@@ -30,3 +32,42 @@ irep_idt extract_field_name(const exprt &string_expr)
   else
     UNREACHABLE;
 }
+
+/// If the given type is an array type, then remove the L2 level
+/// renaming from its size.
+/// \param type Type to be modified
+static void remove_array_type_l2(typet &type)
+{
+  if(to_array_type(type).size().id() != ID_symbol)
+    return;
+
+  ssa_exprt &size = to_ssa_expr(to_array_type(type).size());
+  size.remove_level_2();
+}
+
+void clean_pointer_expr(exprt &expr, const typet &type)
+{
+  if(
+    type.id() == ID_array && expr.id() == ID_symbol &&
+    to_array_type(type).size().get_bool(ID_C_SSA_symbol))
+  {
+    remove_array_type_l2(expr.type());
+    exprt original_expr = to_ssa_expr(expr).get_original_expr();
+    remove_array_type_l2(original_expr.type());
+    to_ssa_expr(expr).set_expression(original_expr);
+  }
+  if(expr.id() == ID_string_constant)
+  {
+    expr = address_of_exprt(expr);
+    expr.type() = pointer_type(char_type());
+  }
+  else if(expr.id() == ID_dereference)
+  {
+    expr = to_dereference_expr(expr).pointer();
+  }
+  else
+  {
+    expr = address_of_exprt(expr);
+  }
+  POSTCONDITION(expr.type().id() == ID_pointer);
+}

src/goto-symex/shadow_memory_util.h

@@ -15,11 +15,21 @@ Author: Peter Schrammel
 #include <util/irep.h>
 
 class exprt;
+class typet;
 
 /// Extracts the field name identifier from a string expression,
 /// e.g. as passed as argument to a __CPROVER_field_decl_local call.
 /// \param string_expr The string argument expression
 /// \return The identifier denoted by the string argument expression
 irep_idt extract_field_name(const exprt &string_expr);
 
+/// Clean the given pointer expression so that it has the right
+/// shape for being used for identifying shadow memory.
+/// This handles some quirks regarding array sizes containing
+/// L2 symbols and string constants not having char-pointer type.
+/// \param expr The pointer to the original memory, e.g. as passed to
+///    __CPROVER_field_get.
+/// \param type The followed type of expr.
+void clean_pointer_expr(exprt &expr, const typet &type);
+
 #endif // CPROVER_GOTO_SYMEX_SHADOW_MEMORY_STATE_H