Add extract_field_name in new shadow_memory_util.h/.cpp

One of the utility functions that we are going
to need in the shadow memory instrumentation implementation.

We put these utility functions into a separate
in order not to bloat the shadow_memory.cpp file.

Author: peterschrammel

src/goto-symex/Makefile

@@ -15,6 +15,7 @@ SRC = auto_objects.cpp \
       precondition.cpp \
       renaming_level.cpp \
       shadow_memory.cpp \
+      shadow_memory_util.cpp \
       show_program.cpp \
       show_vcc.cpp \
       slice.cpp \

src/goto-symex/shadow_memory_util.cpp

@@ -0,0 +1,32 @@
+/*******************************************************************\
+
+Module: Symex Shadow Memory Instrumentation
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Symex Shadow Memory Instrumentation Utilities
+
+#include "shadow_memory_util.h"
+
+#include <util/invariant.h>
+#include <util/pointer_expr.h>
+#include <util/std_expr.h>
+
+irep_idt extract_field_name(const exprt &string_expr)
+{
+  if(string_expr.id() == ID_typecast)
+    return extract_field_name(to_typecast_expr(string_expr).op());
+  else if(string_expr.id() == ID_address_of)
+    return extract_field_name(to_address_of_expr(string_expr).object());
+  else if(string_expr.id() == ID_index)
+    return extract_field_name(to_index_expr(string_expr).array());
+  else if(string_expr.id() == ID_string_constant)
+  {
+    return string_expr.get(ID_value);
+  }
+  else
+    UNREACHABLE;
+}

src/goto-symex/shadow_memory_util.h

@@ -0,0 +1,25 @@
+/*******************************************************************\
+
+Module: Symex Shadow Memory Instrumentation
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Symex Shadow Memory Instrumentation Utilities
+
+#ifndef CPROVER_GOTO_SYMEX_SHADOW_MEMORY_UTIL_H
+#define CPROVER_GOTO_SYMEX_SHADOW_MEMORY_UTIL_H
+
+#include <util/irep.h>
+
+class exprt;
+
+/// 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);
+
+#endif // CPROVER_GOTO_SYMEX_SHADOW_MEMORY_STATE_H