shadow_memory.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Symex Shadow Memory Instrumentation
 
Author: Peter Schrammel
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_SYMEX_SHADOW_MEMORY_H
#define CPROVER_GOTO_SYMEX_SHADOW_MEMORY_H
 
#include <util/expr.h>
#include <util/message.h>
 
#include "shadow_memory_field_definitions.h"
 
#define SHADOW_MEMORY_PREFIX "SM__"
#define SHADOW_MEMORY_FIELD_DECL "field_decl"
#define SHADOW_MEMORY_GLOBAL_SCOPE "_global"
#define SHADOW_MEMORY_LOCAL_SCOPE "_local"
#define SHADOW_MEMORY_GET_FIELD "get_field"
#define SHADOW_MEMORY_SET_FIELD "set_field"
#define SHADOW_MEMORY_SYMBOL_PREFIX "__SM"
 
class code_function_callt;
class abstract_goto_modelt;
class goto_symex_statet;
class side_effect_exprt;
class ssa_exprt;
class symbol_exprt;
 
class shadow_memoryt
{
public:
  shadow_memoryt(
    const std::function<void(goto_symex_statet &, const exprt &, const exprt &)>
      symex_assign,
    const namespacet &ns,
    message_handlert &message_handler)
    : symex_assign(symex_assign), ns(ns), log(message_handler)
  {
  }
 
  static shadow_memory_field_definitionst gather_field_declarations(
    const abstract_goto_modelt &goto_model,
    message_handlert &message_handler);
 
  void symex_field_static_init(goto_symex_statet &state, const ssa_exprt &lhs);
 
  void symex_field_static_init_string_constant(
    goto_symex_statet &state,
    const ssa_exprt &expr,
    const exprt &rhs);
 
  void symex_field_local_init(goto_symex_statet &state, const ssa_exprt &expr);
 
  void symex_field_dynamic_init(
    goto_symex_statet &state,
    const exprt &expr,
    const side_effect_exprt &code);
 
  void symex_get_field(
    goto_symex_statet &state,
    const exprt &lhs,
    const exprt::operandst &arguments);
 
  void
  symex_set_field(goto_symex_statet &state, const exprt::operandst &arguments);
 
private:
  static void convert_field_declaration(
    const code_function_callt &code_function_call,
    shadow_memory_field_definitionst::field_definitiont &fields,
    bool is_global,
    message_handlert &message_handler);
 
  void initialize_shadow_memory(
    goto_symex_statet &state,
    exprt expr,
    const shadow_memory_field_definitionst::field_definitiont &fields);
 
  const symbol_exprt &add_field(
    goto_symex_statet &state,
    const exprt &expr,
    const irep_idt &field_name,
    const typet &field_type);
 
private:
  const std::function<void(goto_symex_statet &, const exprt &, const exprt)>
    symex_assign;
  const namespacet &ns;
  messaget log;
};
 
#endif // CPROVER_GOTO_SYMEX_SHADOW_MEMORY_H