CBMC
Loading...
Searching...
No Matches
Public Member Functions | Static Public Member Functions | Private Member Functions | Static Private Member Functions | Private Attributes | List of all members
shadow_memoryt Class Reference

The shadow memory instrumentation performed during symbolic execution. More...

#include <shadow_memory.h>

+ Collaboration diagram for shadow_memoryt:
[フレーム]
[legend]

Public Member Functions

  shadow_memoryt (const std::function< void(goto_symex_statet &, const exprt &, const exprt &)> symex_assign, const namespacet &ns, message_handlert &message_handler)
 
void  symex_field_static_init (goto_symex_statet &state, const ssa_exprt &lhs)
  Initialize global-scope shadow memory for global/static variables.
 
void  symex_field_static_init_string_constant (goto_symex_statet &state, const ssa_exprt &expr, const exprt &rhs)
  Initialize global-scope shadow memory for string constants.
 
void  symex_field_local_init (goto_symex_statet &state, const ssa_exprt &expr)
  Initialize local-scope shadow memory for local variables and parameters.
 
void  symex_field_dynamic_init (goto_symex_statet &state, const exprt &expr, const side_effect_exprt &code)
  Initialize global-scope shadow memory for dynamically allocated memory.
 
void  symex_get_field (goto_symex_statet &state, const exprt &lhs, const exprt::operandst &arguments)
  Symbolically executes a __CPROVER_get_field call.
 
void  symex_set_field (goto_symex_statet &state, const exprt::operandst &arguments)
  Symbolically executes a __CPROVER_set_field call.
 

Static Public Member Functions

static shadow_memory_field_definitionst  gather_field_declarations (const abstract_goto_modelt &goto_model, message_handlert &message_handler)
  Gathers the available shadow memory field definitions (__CPROVER_field_decl calls) from the goto model.
 

Private Member Functions

void  initialize_shadow_memory (goto_symex_statet &state, exprt expr, const shadow_memory_field_definitionst::field_definitiont &fields)
  Allocates and initializes a shadow memory field for the given original memory.
 
const symbol_exprt &  add_field (goto_symex_statet &state, const exprt &expr, const irep_idt &field_name, const typet &field_type)
  Registers a shadow memory field for the given original memory.
 

Static Private Member Functions

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)
  Converts a field declaration.
 

Private Attributes

const std::function< void(goto_symex_statet &, const exprt &, const exprt)>  symex_assign
 
const namespacet &  ns
 
messaget  log
 

Detailed Description

The shadow memory instrumentation performed during symbolic execution.

Definition at line 36 of file shadow_memory.h.

Constructor & Destructor Documentation

◆  shadow_memoryt()

shadow_memoryt::shadow_memoryt ( const std::function< void(goto_symex_statet &, const exprt &, const exprt &)>  symex_assign,
const namespacet &  ns,
message_handlert &  message_handler 
)
inline

Definition at line 39 of file shadow_memory.h.

Member Function Documentation

◆  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 
)
private

Registers a shadow memory field for the given original memory.

Parameters
state The symex state
expr The expression for which shadow memory should be allocated
field_name The field name
field_type The field type
Returns
The resulting shadow memory symbol expression

Definition at line 67 of file shadow_memory.cpp.

◆  convert_field_declaration()

void shadow_memoryt::convert_field_declaration ( const code_function_callt &  code_function_call,
shadow_memory_field_definitionst::field_definitiont &  fields,
bool  is_global,
message_handlert &  message_handler 
)
staticprivate

Converts a field declaration.

Parameters
code_function_call The __CPROVER_field_decl_* call
fields The field declaration to be extended
is_global True if the declaration is global
message_handler For logging

Definition at line 509 of file shadow_memory.cpp.

◆  gather_field_declarations()

shadow_memory_field_definitionst shadow_memoryt::gather_field_declarations ( const abstract_goto_modelt &  goto_model,
message_handlert &  message_handler 
)
static

Gathers the available shadow memory field definitions (__CPROVER_field_decl calls) from the goto model.

Parameters
goto_model The goto model
message_handler For logging
Returns
The field definitions

Definition at line 461 of file shadow_memory.cpp.

◆  initialize_shadow_memory()

void shadow_memoryt::initialize_shadow_memory ( goto_symex_statet &  state,
exprt  expr,
const shadow_memory_field_definitionst::field_definitiont &  fields 
)
private

Allocates and initializes a shadow memory field for the given original memory.

Parameters
state The symex state
expr The expression for which shadow memory should be allocated
fields The field definition to be used

Definition at line 28 of file shadow_memory.cpp.

◆  symex_field_dynamic_init()

void shadow_memoryt::symex_field_dynamic_init ( goto_symex_statet &  state,
const exprt &  expr,
const side_effect_exprt &  code 
)

Initialize global-scope shadow memory for dynamically allocated memory.

Parameters
state The symex state
expr The dynamic object symbol expression
code The allocation side effect code

Definition at line 449 of file shadow_memory.cpp.

◆  symex_field_local_init()

void shadow_memoryt::symex_field_local_init ( goto_symex_statet &  state,
const ssa_exprt &  expr 
)

Initialize local-scope shadow memory for local variables and parameters.

Parameters
state The symex state
expr The declared symbol expression

Definition at line 406 of file shadow_memory.cpp.

◆  symex_field_static_init()

void shadow_memoryt::symex_field_static_init ( goto_symex_statet &  state,
const ssa_exprt &  lhs 
)

Initialize global-scope shadow memory for global/static variables.

Parameters
state The symex state
lhs The LHS expression of the initializer assignment

Definition at line 343 of file shadow_memory.cpp.

◆  symex_field_static_init_string_constant()

void shadow_memoryt::symex_field_static_init_string_constant ( goto_symex_statet &  state,
const ssa_exprt &  expr,
const exprt &  rhs 
)

Initialize global-scope shadow memory for string constants.

Parameters
state The symex state
expr The defined symbol expression
rhs The RHS expression of the initializer assignment

Definition at line 381 of file shadow_memory.cpp.

◆  symex_get_field()

void shadow_memoryt::symex_get_field ( goto_symex_statet &  state,
const exprt &  lhs,
const exprt::operandst &  arguments 
)

Symbolically executes a __CPROVER_get_field call.

Parameters
state The symex state
lhs The LHS of the call
arguments The call arguments

Definition at line 194 of file shadow_memory.cpp.

◆  symex_set_field()

void shadow_memoryt::symex_set_field ( goto_symex_statet &  state,
const exprt::operandst &  arguments 
)

Symbolically executes a __CPROVER_set_field call.

Parameters
state The symex state
arguments The call arguments

Definition at line 91 of file shadow_memory.cpp.

Member Data Documentation

◆  log

messaget shadow_memoryt::log
private

Definition at line 138 of file shadow_memory.h.

◆  ns

const namespacet& shadow_memoryt::ns
private

Definition at line 137 of file shadow_memory.h.

◆  symex_assign

const std::function<void(goto_symex_statet &, const exprt &, const exprt)> shadow_memoryt::symex_assign
private

Definition at line 136 of file shadow_memory.h.

The documentation for this class was generated from the following files:

AltStyle によって変換されたページ (->オリジナル) /