Implement shadow_memoryt::gather_field_declarations

Gathers the available shadow memory field definitions
(__CPROVER_field_decl calls) from the goto model
and stores them in a shadow_memory_field_definitionst.

Author: peterschrammel

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,84 @@ 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->get_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.