Merge pull request #7535 from peterschrammel/shadow-memory-basic2

Gather shadow memory fields

regression/cbmc-shadow-memory/declarations1/bad1.c

@@ -0,0 +1,4 @@
+void bad_declaration1()
+{
+  __CPROVER_field_decl_local("field1", (int)0);
+}

regression/cbmc-shadow-memory/declarations1/bad2.c

@@ -0,0 +1,8 @@
+void bad_declaration2()
+{
+  struct STRUCT
+  {
+    char x;
+  } s;
+  __CPROVER_field_decl_global("field2", s);
+}

regression/cbmc-shadow-memory/declarations1/good.c

@@ -0,0 +1,5 @@
+void good_declarations()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)0);
+  __CPROVER_field_decl_global("field2", (unsigned __CPROVER_bitvector[6])0);
+}

regression/cbmc-shadow-memory/declarations1/test_bad1.desc

@@ -0,0 +1,9 @@
+CORE
+bad1.c
+--function bad_declaration1 --verbosity 10
+^EXIT=6$
+^SIGNAL=0$
+^A shadow memory field must not be larger than 8 bits.
+--
+--
+Test that a shadow memory declaration of a too large type is rejected.

regression/cbmc-shadow-memory/declarations1/test_bad2.desc

@@ -0,0 +1,9 @@
+CORE
+bad2.c
+--function bad_declaration2 --verbosity 10
+^EXIT=6$
+^SIGNAL=0$
+^A shadow memory field must be of a bitvector type.
+--
+--
+Test that a shadow memory declaration of a non-bitvector type is rejected.

regression/cbmc-shadow-memory/declarations1/test_good.desc

@@ -0,0 +1,12 @@
+CORE
+good.c
+--function good_declarations --verbosity 10
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+^Shadow memory: declare local field field1 of type c_bool\[8\]
+^Shadow memory: declare global field field2 of type unsignedbv\[6\]
+--
+^A shadow memory field must
+--
+Test that shadow memory declarations are correctly gathered.

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.cpp

@@ -11,11 +11,14 @@ Author: Peter Schrammel
 
 #include "shadow_memory.h"
 
+#include <util/bitvector_types.h>
+#include <util/format_type.h>
 #include <util/fresh_symbol.h>
 
 #include <langapi/language_util.h>
 
 #include "goto_symex_state.h"
+#include "shadow_memory_util.h"
 
 void shadow_memoryt::initialize_shadow_memory(
   goto_symex_statet &state,
@@ -95,17 +98,83 @@ void shadow_memoryt::symex_field_dynamic_init(
 }
 
 shadow_memory_field_definitionst shadow_memoryt::gather_field_declarations(
-  abstract_goto_modelt &goto_model,
+  const abstract_goto_modelt &goto_model,
   message_handlert &message_handler)
 {
-  // To be implemented
-
-  return shadow_memory_field_definitionst();
+  shadow_memory_field_definitionst field_definitions;
+
+  // Gather shadow memory declarations from goto model
+  for(const auto &goto_function : goto_model.get_goto_functions().function_map)
+  {
+    const auto &goto_program = goto_function.second.body;
+    forall_goto_program_instructions(target, goto_program)
+    {
+      if(!target->is_function_call())
+        continue;
+
+      const auto &code_function_call = to_code_function_call(target->code());
+      const exprt &function = code_function_call.function();
+
+      if(function.id() != ID_symbol)
+        continue;
+
+      const irep_idt &identifier = to_symbol_expr(function).get_identifier();
+
+      if(
+        identifier ==
+        CPROVER_PREFIX SHADOW_MEMORY_FIELD_DECL SHADOW_MEMORY_GLOBAL_SCOPE)
+      {
+        convert_field_declaration(
+          code_function_call,
+          field_definitions.global_fields,
+          true,
+          message_handler);
+      }
+      else if(
+        identifier ==
+        CPROVER_PREFIX SHADOW_MEMORY_FIELD_DECL SHADOW_MEMORY_LOCAL_SCOPE)
+      {
+        convert_field_declaration(
+          code_function_call,
+          field_definitions.local_fields,
+          false,
+          message_handler);
+      }
+    }
+  }
+  return field_definitions;
 }
 
 void shadow_memoryt::convert_field_declaration(
   const code_function_callt &code_function_call,
-  shadow_memory_field_definitionst::field_definitiont &fields)
+  shadow_memory_field_definitionst::field_definitiont &fields,
+  bool is_global,
+  message_handlert &message_handler)
 {
-  // To be implemented
+  INVARIANT(
+    code_function_call.arguments().size() == 2,
+    std::string(CPROVER_PREFIX) + SHADOW_MEMORY_FIELD_DECL +
+      (is_global ? SHADOW_MEMORY_GLOBAL_SCOPE : SHADOW_MEMORY_LOCAL_SCOPE) +
+      " requires 2 arguments");
+  irep_idt field_name = extract_field_name(code_function_call.arguments()[0]);
+
+  exprt expr = code_function_call.arguments()[1];
+
+  messaget log(message_handler);
+  log.debug() << "Shadow memory: declare " << (is_global ? "global " : "local ")
+              << "field " << id2string(field_name) << " of type "
+              << format(expr.type()) << messaget::eom;
+  if(!can_cast_type<bitvector_typet>(expr.type()))
+  {
+    throw unsupported_operation_exceptiont(
+      "A shadow memory field must be of a bitvector type.");
+  }
+  if(to_bitvector_type(expr.type()).get_width() > 8)
+  {
+    throw unsupported_operation_exceptiont(
+      "A shadow memory field must not be larger than 8 bits.");
+  }
+
+  // record the field's initial value (and type)
+  fields[field_name] = expr;
 }

src/goto-symex/shadow_memory.h

@@ -50,7 +50,7 @@ class shadow_memoryt
   /// \param message_handler For logging
   /// \return The field definitions
   static shadow_memory_field_definitionst gather_field_declarations(
-    abstract_goto_modelt &goto_model,
+    const abstract_goto_modelt &goto_model,
     message_handlert &message_handler);
 
   /// Initialize global-scope shadow memory for global/static variables.
@@ -100,9 +100,13 @@ class shadow_memoryt
   /// Converts a field declaration
   /// \param code_function_call The __CPROVER_field_decl_* call
   /// \param fields The field declaration to be extended
-  void convert_field_declaration(
+  /// \param is_global True if the declaration is global
+  /// \param message_handler For logging
+  static void convert_field_declaration(
     const code_function_callt &code_function_call,
-    shadow_memory_field_definitionst::field_definitiont &fields);
+    shadow_memory_field_definitionst::field_definitiont &fields,
+    bool is_global,
+    message_handlert &message_handler);
 
   /// Allocates and initializes a shadow memory field for the given original
   /// memory.

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