Add implementation to shadow memory init function

This commit adds the implementation to the 4 shadow memory
user-facing initialization functions.
Namely:
 - shadow_memoryt::symex_field_static_init
 - shadow_memoryt::symex_field_static_init_string_constant
 - shadow_memoryt::symex_field_local_init
 - shadow_memoryt::symex_field_dynamic_init

Author: Enrico Steffinlongo

src/goto-symex/shadow_memory.cpp

@@ -16,8 +16,12 @@ Author: Peter Schrammel
 #include <util/format_expr.h>
 #include <util/format_type.h>
 #include <util/fresh_symbol.h>
+#include <util/pointer_expr.h>
+#include <util/prefix.h>
+#include <util/string_constant.h>
 
 #include <langapi/language_util.h>
+#include <linking/static_lifetime_init.h>
 
 #include "goto_symex_state.h"
 #include "shadow_memory_util.h"
@@ -99,34 +103,132 @@ void shadow_memoryt::symex_get_field(
   // To be implemented
 }
 
+// TODO: the following 4 functions (`symex_field_static_init`,
+//                                  `symex_field_static_init_string_constant`,
+//                                  `symex_field_local_init`,
+//                                  `symex_field_dynamic_init`) do filtering on
+//  the input symbol name and then call `initialize_shadow_memory` accordingly.
+//  We want to refactor and improve the way the filtering is done, but given
+//  that we don't have an easy mechanism to validate that we haven't changed the
+//  behaviour, we want to postpone changing this until the full shadow memory
+//  functionalities are integrated and we have good regression/unit testing.
+
 void shadow_memoryt::symex_field_static_init(
   goto_symex_statet &state,
   const ssa_exprt &lhs)
 {
-  // To be implemented
+  if(lhs.get_original_expr().id() != ID_symbol)
+    return;
+
+  const irep_idt &identifier =
+    to_symbol_expr(lhs.get_original_expr()).get_identifier();
+
+  if(state.source.function_id != INITIALIZE_FUNCTION)
+    return;
+
+  if(
+    has_prefix(id2string(identifier), CPROVER_PREFIX) &&
+    !has_prefix(id2string(identifier), CPROVER_PREFIX "errno"))
+  {
+    return;
+  }
+
+  const symbolt &symbol = ns.lookup(identifier);
+
+  if(
+    (id2string(symbol.name).find("::return_value") == std::string::npos &&
+     symbol.is_auxiliary) ||
+    !symbol.is_static_lifetime)
+    return;
+  if(id2string(symbol.name).find("__cs_") != std::string::npos)
+    return;
+
+  const typet &type = symbol.type;
+  log.debug() << "Shadow memory: global memory " << id2string(identifier)
+              << " of type " << from_type(ns, "", type) << messaget::eom;
+
+  initialize_shadow_memory(
+    state, lhs, state.shadow_memory.fields.global_fields);
 }
 
 void shadow_memoryt::symex_field_static_init_string_constant(
   goto_symex_statet &state,
   const ssa_exprt &expr,
   const exprt &rhs)
 {
-  // To be implemented
+  if(
+    expr.get_original_expr().id() == ID_symbol &&
+    has_prefix(
+      id2string(to_symbol_expr(expr.get_original_expr()).get_identifier()),
+      CPROVER_PREFIX))
+  {
+    return;
+  }
+  const index_exprt &index_expr =
+    to_index_expr(to_address_of_expr(rhs).object());
+
+  const typet &type = index_expr.array().type();
+  log.debug() << "Shadow memory: global memory "
+              << id2string(to_string_constant(index_expr.array()).get_value())
+              << " of type " << from_type(ns, "", type) << messaget::eom;
+
+  initialize_shadow_memory(
+    state, index_expr.array(), state.shadow_memory.fields.global_fields);
 }
 
 void shadow_memoryt::symex_field_local_init(
   goto_symex_statet &state,
   const ssa_exprt &expr)
 {
-  // To be implemented
+  const symbolt &symbol =
+    ns.lookup(to_symbol_expr(expr.get_original_expr()).get_identifier());
+
+  const std::string symbol_name = id2string(symbol.name);
+  if(
+    symbol.is_auxiliary &&
+    symbol_name.find("::return_value") == std::string::npos)
+    return;
+  if(
+    symbol_name.find("malloc::") != std::string::npos &&
+    (symbol_name.find("malloc_size") != std::string::npos ||
+     symbol_name.find("malloc_res") != std::string::npos ||
+     symbol_name.find("record_malloc") != std::string::npos ||
+     symbol_name.find("record_may_leak") != std::string::npos))
+  {
+    return;
+  }
+  if(
+    symbol_name.find("__builtin_alloca::") != std::string::npos &&
+    (symbol_name.find("alloca_size") != std::string::npos ||
+     symbol_name.find("record_malloc") != std::string::npos ||
+     symbol_name.find("record_alloca") != std::string::npos ||
+     symbol_name.find("res") != std::string::npos))
+  {
+    return;
+  }
+  if(symbol_name.find("__cs_") != std::string::npos)
+    return;
+
+  const typet &type = expr.type();
+  ssa_exprt expr_l1 = remove_level_2(expr);
+  log.debug() << "Shadow memory: local memory "
+              << id2string(expr_l1.get_identifier()) << " of type "
+              << from_type(ns, "", type) << messaget::eom;
+
+  initialize_shadow_memory(
+    state, expr_l1, state.shadow_memory.fields.local_fields);
 }
 
 void shadow_memoryt::symex_field_dynamic_init(
   goto_symex_statet &state,
   const exprt &expr,
   const side_effect_exprt &code)
 {
-  // To be implemented
+  log.debug() << "Shadow memory: dynamic memory of type "
+              << from_type(ns, "", expr.type()) << messaget::eom;
+
+  initialize_shadow_memory(
+    state, expr, state.shadow_memory.fields.global_fields);
 }
 
 shadow_memory_field_definitionst shadow_memoryt::gather_field_declarations(