Shadow memory initialization functions

src/goto-symex/shadow_memory.cpp

@@ -12,44 +12,80 @@
 #include "shadow_memory.h"
 
 #include <util/bitvector_types.h>
+#include <util/expr_initializer.h>
+#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"
 
 void shadow_memoryt::initialize_shadow_memory(
   goto_symex_statet &state,
-  const exprt &expr,
+  exprt expr,
   const shadow_memory_field_definitionst::field_definitiont &fields)
 {
-  // To be implemented
+  typet type = ns.follow(expr.type());
+  clean_pointer_expr(expr, type);
+  for(const auto &field_pair : fields)
+  {
+    const symbol_exprt &shadow = add_field(state, expr, field_pair.first, type);
+
+    if(
+      field_pair.second.id() == ID_typecast &&
+      to_typecast_expr(field_pair.second).op().is_zero())
+    {
+      const auto zero_value =
+        zero_initializer(type, expr.source_location(), ns);
+      CHECK_RETURN(zero_value.has_value());
+
+      symex_assign(state, shadow, *zero_value);
+    }
+    else
+    {
+      exprt init_expr = field_pair.second;
+      if(init_expr.id() == ID_typecast)
+        init_expr = to_typecast_expr(field_pair.second).op();
+      const auto init_value =
+        expr_initializer(type, expr.source_location(), ns, init_expr);
+      CHECK_RETURN(init_value.has_value());
+
+      symex_assign(state, shadow, *init_value);
+    }
+
+    log.debug() << "Shadow memory: initialize field "
+                << id2string(shadow.get_identifier()) << " for " << format(expr)
+                << " with initial value " << format(field_pair.second)
+                << messaget::eom;
+  }
 }
 
-symbol_exprt shadow_memoryt::add_field(
+const symbol_exprt &shadow_memoryt::add_field(
   goto_symex_statet &state,
   const exprt &expr,
   const irep_idt &field_name,
   const typet &field_type)
 {
-  // To be completed
-
   const auto &function_symbol = ns.lookup(state.source.function_id);
-
-  symbolt &new_symbol = get_fresh_aux_symbol(
+  const symbolt &new_symbol = get_fresh_aux_symbol(
     field_type,
     id2string(state.source.function_id),
     SHADOW_MEMORY_PREFIX + from_expr(expr) + "__" + id2string(field_name),
     state.source.pc->source_location(),
     function_symbol.mode,
     state.symbol_table);
 
-  // Call some function on ns to silence the compiler in the meanwhile.
-  ns.get_symbol_table();
+  auto &addresses = state.shadow_memory.address_fields[field_name];
+  addresses.push_back(
+    shadow_memory_statet::shadowed_addresst{expr, new_symbol.symbol_expr()});
 
-  return new_symbol.symbol_expr();
+  return addresses.back().shadow;
 }
 
 void shadow_memoryt::symex_set_field(
@@ -67,34 +103,132 @@
   // 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(

src/goto-symex/shadow_memory.h

@@ -14,7 +14,6 @@ Author: Peter Schrammel
 
 #include <util/expr.h>
 #include <util/message.h>
-#include <util/std_expr.h>
 
 #include "shadow_memory_field_definitions.h"
 
@@ -30,6 +29,7 @@ class abstract_goto_modelt;
 class goto_symex_statet;
 class side_effect_exprt;
 class ssa_exprt;
+class symbol_exprt;
 
 /// \brief The shadow memory instrumentation performed during symbolic execution
 class shadow_memoryt
@@ -115,7 +115,7 @@ class shadow_memoryt
   /// \param fields The field definition to be used
   void initialize_shadow_memory(
     goto_symex_statet &state,
-    const exprt &expr,
+    exprt expr,
     const shadow_memory_field_definitionst::field_definitiont &fields);
 
   /// Registers a shadow memory field for the given original memory
@@ -124,7 +124,7 @@ class shadow_memoryt
   /// \param field_name The field name
   /// \param field_type The field type
   /// \return The resulting shadow memory symbol expression
-  symbol_exprt add_field(
+  const symbol_exprt &add_field(
     goto_symex_statet &state,
     const exprt &expr,
     const irep_idt &field_name,

src/goto-symex/shadow_memory_util.cpp

@@ -11,8 +11,10 @@
 
 #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 @@
   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