cprover
interpretert Class Reference

#include <interpreter_class.h>

+ Inheritance diagram for interpretert:
+ Collaboration diagram for interpretert:

Classes

struct  function_assignments_contextt
 
struct  function_assignmentt
 
class  memory_cellt
 
class  stack_framet
 

Public Types

typedef std::vector< function_assignmenttfunction_assignmentst
 
typedef std::vector< mp_integermp_vectort
 
typedef std::pair< irep_idt, irep_idtassignment_idt
 
typedef std::pair< exprt, exprtdiff_pairt
 
typedef std::map< assignment_idt, diff_pairtside_effects_differencet
 
typedef std::pair< irep_idt, exprtinput_entryt
 
typedef std::map< irep_idt, exprtinput_valuest
 
typedef std::map< irep_idt, typetdynamic_typest
 
typedef std::map< irep_idt, function_assignmentstoutput_valuest
 
typedef std::list< function_assignments_contexttfunction_assignments_contextst
 
typedef std::map< irep_idt, std::list< function_assignments_contextt > > list_input_varst
 
- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 

Public Member Functions

 interpretert (const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, message_handlert &_message_handler)
 
void operator() ()
 
void print_memory (bool input_flags)
 Prints the current state of the memory map Since messaget mdofifies class members, print functions are nonconst. More...
 
const dynamic_typestget_dynamic_types ()
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. More...
 

Public Attributes

output_valuest output_values
 

Protected Types

typedef std::unordered_map< irep_idt, mp_integermemory_mapt
 
using inverse_memory_mapt = std::map< mp_integer, optionalt< symbol_exprt > >
 
typedef sparse_vectort< memory_celltmemoryt
 
typedef std::map< std::string, const irep_idt & > parameter_sett
 
typedef std::pair< const irep_idt, const irep_idtstruct_member_idt
 
typedef std::map< struct_member_idt, const exprtstruct_valuest
 
typedef std::stack< stack_frametcall_stackt
 

Protected Member Functions

const inverse_memory_mapt::value_type & address_to_object_record (const mp_integer &address) const
 
symbol_exprt address_to_symbol (const mp_integer &address) const
 
mp_integer address_to_offset (const mp_integer &address) const
 
mp_integer base_address_to_alloc_size (const mp_integer &address) const
 
mp_integer base_address_to_actual_size (const mp_integer &address) const
 
void build_memory_map ()
 Creates a memory map of all static symbols in the program. More...
 
void build_memory_map (const symbolt &symbol)
 
mp_integer build_memory_map (const symbol_exprt &symbol_expr)
 Populates dynamic entries of the memory map. More...
 
typet concretize_type (const typet &type)
 turns a variable length array type into a fixed array type More...
 
bool unbounded_size (const typet &)
 
mp_integer get_size (const typet &type)
 Retrieves the actual size of the provided structured type. More...
 
struct_typet::componentt get_component (const irep_idt &object, const mp_integer &offset)
 retrieves the member at offset More...
 
struct_typet::componentt get_component (const typet &object_type, const mp_integer &offset)
 Retrieves the member at offset of an object of type object_type. More...
 
typet get_type (const irep_idt &id) const
 returns the type object corresponding to id More...
 
exprt get_value (const typet &type, const mp_integer &offset=0, bool use_non_det=false)
 retrives the constant value at memory location offset as an object of type type More...
 
exprt get_value (const typet &type, mp_vectort &rhs, const mp_integer &offset=0)
 returns the value at offset in the form of type given a memory buffer rhs which is typically a structured type More...
 
exprt get_value (const irep_idt &id)
 
void step ()
 executes a single step and updates the program counter More...
 
void execute_assert ()
 
void execute_assume ()
 
void execute_assign ()
 executes the assign statement at the current pc value More...
 
void execute_goto ()
 executes a goto instruction More...
 
void execute_function_call ()
 
void execute_other ()
 executes side effects of 'other' instructions More...
 
void execute_decl ()
 
void clear_input_flags ()
 Clears memoy r/w flag initialization. More...
 
void allocate (const mp_integer &address, const mp_integer &size)
 reserves memory block of size at address More...
 
void assign (const mp_integer &address, const mp_vectort &rhs)
 sets the memory at address with the given rhs value (up to sizeof(rhs)) More...
 
void read (const mp_integer &address, mp_vectort &dest) const
 Reads a memory address and loads it into the dest variable. More...
 
void read_unbounded (const mp_integer &address, mp_vectort &dest) const
 
virtual void command ()
 reads a user command and executes it. More...
 
bool evaluate_boolean (const exprt &expr)
 
bool count_type_leaves (const typet &source_type, mp_integer &result)
 Count the number of leaf subtypes of ty, a leaf type is a type that is not an array or a struct. More...
 
bool byte_offset_to_memory_offset (const typet &source_type, const mp_integer &byte_offset, mp_integer &result)
 Supposing the caller has an mp_vector representing a value with type 'source_type', this yields the offset into that vector at which to find a value at byte address 'offset'. More...
 
bool memory_offset_to_byte_offset (const typet &source_type, const mp_integer &cell_offset, mp_integer &result)
 Similarly to the above, the interpreter's memory objects contain mp_integers that represent variable-sized struct members. More...
 
void evaluate (const exprt &expr, mp_vectort &dest)
 Evaluate an expression. More...
 
mp_integer evaluate_address (const exprt &expr, bool fail_quietly=false)
 
void initialize (bool init)
 Initializes the memory map of the interpreter and [optionally] runs up to the entry point (thus doing the cprover initialization) More...
 
void show_state ()
 displays the current position of the pc and corresponding code More...
 

Protected Attributes

const symbol_tabletsymbol_table
 
const namespacet ns
 
const goto_functionstgoto_functions
 
memory_mapt memory_map
 
inverse_memory_mapt inverse_memory_map
 
memoryt memory
 
mp_integer stack_pointer
 
call_stackt call_stack
 
input_valuest input_vars
 
list_input_varst function_input_vars
 
goto_functionst::function_mapt::const_iterator function
 
goto_programt::const_targett pc
 
goto_programt::const_targett next_pc
 
goto_programt::const_targett target_assert
 
goto_tracet steps
 
bool done
 
bool show
 
bool stop_on_assertion
 
size_t num_steps
 
size_t total_steps
 
dynamic_typest dynamic_types
 
int num_dynamic_objects
 
mp_integer stack_depth
 
unsigned thread_id
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Static Protected Attributes

static const size_t npos =std::numeric_limits<size_t>::max()
 

Friends

class interpreter_testt
 

Additional Inherited Members

- Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
 
- Static Public Attributes inherited from messaget
static eomt eom
 
static const commandt reset
 return to default formatting, as defined by the terminal More...
 
static const commandt red
 render text with red foreground color More...
 
static const commandt green
 render text with green foreground color More...
 
static const commandt yellow
 render text with yellow foreground color More...
 
static const commandt blue
 render text with blue foreground color More...
 
static const commandt magenta
 render text with magenta foreground color More...
 
static const commandt cyan
 render text with cyan foreground color More...
 
static const commandt bright_red
 render text with bright red foreground color More...
 
static const commandt bright_green
 render text with bright green foreground color More...
 
static const commandt bright_yellow
 render text with bright yellow foreground color More...
 
static const commandt bright_blue
 render text with bright blue foreground color More...
 
static const commandt bright_magenta
 render text with bright magenta foreground color More...
 
static const commandt bright_cyan
 render text with bright cyan foreground color More...
 
static const commandt bold
 render text with bold font More...
 
static const commandt faint
 render text with faint font More...
 
static const commandt italic
 render italic text More...
 
static const commandt underline
 render underlined text More...
 

Detailed Description

Definition at line 27 of file interpreter_class.h.

Member Typedef Documentation

◆ assignment_idt

Definition at line 62 of file interpreter_class.h.

◆ call_stackt

typedef std::stack<stack_framet> interpretert::call_stackt
protected

Definition at line 261 of file interpreter_class.h.

◆ diff_pairt

typedef std::pair<exprt, exprt> interpretert::diff_pairt

Definition at line 65 of file interpreter_class.h.

◆ dynamic_typest

Definition at line 77 of file interpreter_class.h.

◆ function_assignments_contextst

◆ function_assignmentst

Definition at line 57 of file interpreter_class.h.

◆ input_entryt

Definition at line 71 of file interpreter_class.h.

◆ input_valuest

Definition at line 74 of file interpreter_class.h.

◆ inverse_memory_mapt

Definition at line 109 of file interpreter_class.h.

◆ list_input_varst

Definition at line 96 of file interpreter_class.h.

◆ memory_mapt

typedef std::unordered_map<irep_idt, mp_integer> interpretert::memory_mapt
protected

Definition at line 108 of file interpreter_class.h.

◆ memoryt

Definition at line 180 of file interpreter_class.h.

◆ mp_vectort

typedef std::vector<mp_integer> interpretert::mp_vectort

Definition at line 59 of file interpreter_class.h.

◆ output_valuest

Definition at line 79 of file interpreter_class.h.

◆ parameter_sett

typedef std::map<std::string, const irep_idt &> interpretert::parameter_sett
protected

Definition at line 181 of file interpreter_class.h.

◆ side_effects_differencet

◆ struct_member_idt

typedef std::pair<const irep_idt, const irep_idt> interpretert::struct_member_idt
protected

Definition at line 183 of file interpreter_class.h.

◆ struct_valuest

typedef std::map<struct_member_idt, const exprt> interpretert::struct_valuest
protected

Definition at line 184 of file interpreter_class.h.

Constructor & Destructor Documentation

◆ interpretert()

interpretert::interpretert ( const symbol_tablet _symbol_table,
const goto_functionst _goto_functions,
message_handlert _message_handler 
)
inline

Definition at line 30 of file interpreter_class.h.

Member Function Documentation

◆ address_to_object_record()

const inverse_memory_mapt::value_type& interpretert::address_to_object_record ( const mp_integer address) const
inlineprotected

Definition at line 113 of file interpreter_class.h.

◆ address_to_offset()

mp_integer interpretert::address_to_offset ( const mp_integer address) const
inlineprotected

Definition at line 130 of file interpreter_class.h.

◆ address_to_symbol()

symbol_exprt interpretert::address_to_symbol ( const mp_integer address) const
inlineprotected

Definition at line 125 of file interpreter_class.h.

◆ allocate()

void interpretert::allocate ( const mp_integer address,
const mp_integer size 
)
protected

reserves memory block of size at address

Definition at line 80 of file interpreter_evaluate.cpp.

◆ assign()

void interpretert::assign ( const mp_integer address,
const mp_vectort rhs 
)
protected

sets the memory at address with the given rhs value (up to sizeof(rhs))

Definition at line 710 of file interpreter.cpp.

◆ base_address_to_actual_size()

mp_integer interpretert::base_address_to_actual_size ( const mp_integer address) const
inlineprotected

Definition at line 146 of file interpreter_class.h.

◆ base_address_to_alloc_size()

mp_integer interpretert::base_address_to_alloc_size ( const mp_integer address) const
inlineprotected

Definition at line 135 of file interpreter_class.h.

◆ build_memory_map() [1/3]

void interpretert::build_memory_map ( )
protected

Creates a memory map of all static symbols in the program.

Definition at line 860 of file interpreter.cpp.

◆ build_memory_map() [2/3]

mp_integer interpretert::build_memory_map ( const symbol_exprt symbol_expr)
protected

Populates dynamic entries of the memory map.

Returns
Updates the memory map to include variable id if it does not exist

Definition at line 927 of file interpreter.cpp.

◆ build_memory_map() [3/3]

void interpretert::build_memory_map ( const symbolt symbol)
protected

Definition at line 877 of file interpreter.cpp.

◆ byte_offset_to_memory_offset()

bool interpretert::byte_offset_to_memory_offset ( const typet source_type,
const mp_integer offset,
mp_integer result 
)
protected

Supposing the caller has an mp_vector representing a value with type 'source_type', this yields the offset into that vector at which to find a value at byte address 'offset'.

We need this because the interpreter's memory map uses unlabelled variable-width values – for example, a C value { { 1, 2 }, 3, 4 } of type struct { int x[2]; char y; unsigned long z; } would be represented [1,2,3,4], with the source type needed alongside to figure out which member is targeted by a byte-extract operation.

parameters: 'source_type', 'offset' (unit: bytes),
Returns
Offset into a vector of interpreter values; returns true on error

Definition at line 156 of file interpreter_evaluate.cpp.

◆ clear_input_flags()

void interpretert::clear_input_flags ( )
protected

Clears memoy r/w flag initialization.

Definition at line 97 of file interpreter_evaluate.cpp.

◆ command()

void interpretert::command ( )
protectedvirtual

reads a user command and executes it.

Definition at line 128 of file interpreter.cpp.

◆ concretize_type()

typet interpretert::concretize_type ( const typet type)
protected

turns a variable length array type into a fixed array type

Definition at line 900 of file interpreter.cpp.

◆ count_type_leaves()

bool interpretert::count_type_leaves ( const typet ty,
mp_integer result 
)
protected

Count the number of leaf subtypes of ty, a leaf type is a type that is not an array or a struct.

For instance the count for a type such as struct { (int[3])[5]; int } would be 16 = (3 * 5 + 1).

Parameters
tya type
[out]resultNumber of leaf primitive types in ty
Returns
returns true on error

Definition at line 113 of file interpreter_evaluate.cpp.

◆ evaluate()

void interpretert::evaluate ( const exprt expr,
mp_vectort dest 
)
protected

Evaluate an expression.

Parameters
exprexpression to evaluate
[out]destvector in which the result of the evaluation is stored

Definition at line 313 of file interpreter_evaluate.cpp.

◆ evaluate_address()

mp_integer interpretert::evaluate_address ( const exprt expr,
bool  fail_quietly = false 
)
protected

Definition at line 1055 of file interpreter_evaluate.cpp.

◆ evaluate_boolean()

bool interpretert::evaluate_boolean ( const exprt expr)
inlineprotected

Definition at line 282 of file interpreter_class.h.

◆ execute_assert()

void interpretert::execute_assert ( )
protected

Definition at line 741 of file interpreter.cpp.

◆ execute_assign()

void interpretert::execute_assign ( )
protected

executes the assign statement at the current pc value

Definition at line 663 of file interpreter.cpp.

◆ execute_assume()

void interpretert::execute_assume ( )
protected

Definition at line 735 of file interpreter.cpp.

◆ execute_decl()

void interpretert::execute_decl ( )
protected

Definition at line 419 of file interpreter.cpp.

◆ execute_function_call()

void interpretert::execute_function_call ( )
protected

Definition at line 753 of file interpreter.cpp.

◆ execute_goto()

void interpretert::execute_goto ( )
protected

executes a goto instruction

Definition at line 370 of file interpreter.cpp.

◆ execute_other()

void interpretert::execute_other ( )
protected

executes side effects of 'other' instructions

Definition at line 385 of file interpreter.cpp.

◆ get_component() [1/2]

struct_typet::componentt interpretert::get_component ( const irep_idt object,
const mp_integer offset 
)
protected

retrieves the member at offset

Deprecated:
"use the object_type version instead"
parameters: an object and a memory offset

Definition at line 426 of file interpreter.cpp.

◆ get_component() [2/2]

struct_typet::componentt interpretert::get_component ( const typet object_type,
const mp_integer offset 
)
protected

Retrieves the member at offset of an object of type object_type.

Definition at line 436 of file interpreter.cpp.

◆ get_dynamic_types()

const dynamic_typest& interpretert::get_dynamic_types ( )
inline

Definition at line 98 of file interpreter_class.h.

◆ get_size()

mp_integer interpretert::get_size ( const typet type)
protected

Retrieves the actual size of the provided structured type.

Unbounded objects get allocated 2^32 address space each (of a 2^64 sized space).

Parameters
typea structured type
Returns
Size of the given type

Definition at line 981 of file interpreter.cpp.

◆ get_type()

typet interpretert::get_type ( const irep_idt id) const
protected

returns the type object corresponding to id

Definition at line 459 of file interpreter.cpp.

◆ get_value() [1/3]

exprt interpretert::get_value ( const irep_idt id)
protected

Definition at line 1046 of file interpreter.cpp.

◆ get_value() [2/3]

exprt interpretert::get_value ( const typet type,
const mp_integer offset = 0,
bool  use_non_det = false 
)
protected

retrives the constant value at memory location offset as an object of type type

Definition at line 469 of file interpreter.cpp.

◆ get_value() [3/3]

exprt interpretert::get_value ( const typet type,
mp_vectort rhs,
const mp_integer offset = 0 
)
protected

returns the value at offset in the form of type given a memory buffer rhs which is typically a structured type

Definition at line 536 of file interpreter.cpp.

◆ initialize()

void interpretert::initialize ( bool  init)
protected

Initializes the memory map of the interpreter and [optionally] runs up to the entry point (thus doing the cprover initialization)

Definition at line 64 of file interpreter.cpp.

◆ memory_offset_to_byte_offset()

bool interpretert::memory_offset_to_byte_offset ( const typet source_type,
const mp_integer full_cell_offset,
mp_integer result 
)
protected

Similarly to the above, the interpreter's memory objects contain mp_integers that represent variable-sized struct members.

This counts the size of type leaves to determine the byte offset corresponding to a memory offset.

parameters: An interpreter memory offset and the type to interpret that
memory
Returns
The corresponding byte offset. Returns true on error

Definition at line 238 of file interpreter_evaluate.cpp.

◆ operator()()

void interpretert::operator() ( void  )

Definition at line 40 of file interpreter.cpp.

◆ print_memory()

void interpretert::print_memory ( bool  input_flags)

Prints the current state of the memory map Since messaget mdofifies class members, print functions are nonconst.

Definition at line 1066 of file interpreter.cpp.

◆ read()

void interpretert::read ( const mp_integer address,
mp_vectort dest 
) const
protected

Reads a memory address and loads it into the dest variable.

Marks cell as READ_BEFORE_WRITTEN if cell has never been written.

Definition at line 26 of file interpreter_evaluate.cpp.

◆ read_unbounded()

void interpretert::read_unbounded ( const mp_integer address,
mp_vectort dest 
) const
protected

Definition at line 50 of file interpreter_evaluate.cpp.

◆ show_state()

void interpretert::show_state ( )
protected

displays the current position of the pc and corresponding code

Definition at line 105 of file interpreter.cpp.

◆ step()

void interpretert::step ( )
protected

executes a single step and updates the program counter

Definition at line 233 of file interpreter.cpp.

◆ unbounded_size()

bool interpretert::unbounded_size ( const typet type)
protected

Definition at line 958 of file interpreter.cpp.

Friends And Related Function Documentation

◆ interpreter_testt

friend class interpreter_testt
friend

Definition at line 314 of file interpreter_class.h.

Member Data Documentation

◆ call_stack

call_stackt interpretert::call_stack
protected

Definition at line 263 of file interpreter_class.h.

◆ done

bool interpretert::done
protected

Definition at line 270 of file interpreter_class.h.

◆ dynamic_types

dynamic_typest interpretert::dynamic_types
protected

Definition at line 277 of file interpreter_class.h.

◆ function

goto_functionst::function_mapt::const_iterator interpretert::function
protected

Definition at line 267 of file interpreter_class.h.

◆ function_input_vars

list_input_varst interpretert::function_input_vars
protected

Definition at line 265 of file interpreter_class.h.

◆ goto_functions

const goto_functionst& interpretert::goto_functions
protected

Definition at line 106 of file interpreter_class.h.

◆ input_vars

input_valuest interpretert::input_vars
protected

Definition at line 264 of file interpreter_class.h.

◆ inverse_memory_map

inverse_memory_mapt interpretert::inverse_memory_map
protected

Definition at line 111 of file interpreter_class.h.

◆ memory

memoryt interpretert::memory
mutableprotected

Definition at line 189 of file interpreter_class.h.

◆ memory_map

memory_mapt interpretert::memory_map
protected

Definition at line 110 of file interpreter_class.h.

◆ next_pc

goto_programt::const_targett interpretert::next_pc
protected

Definition at line 268 of file interpreter_class.h.

◆ npos

const std::size_t interpretert::npos =std::numeric_limits<size_t>::max()
staticprotected

Definition at line 273 of file interpreter_class.h.

◆ ns

const namespacet interpretert::ns
protected

Definition at line 104 of file interpreter_class.h.

◆ num_dynamic_objects

int interpretert::num_dynamic_objects
protected

Definition at line 278 of file interpreter_class.h.

◆ num_steps

size_t interpretert::num_steps
protected

Definition at line 274 of file interpreter_class.h.

◆ output_values

output_valuest interpretert::output_values

Definition at line 80 of file interpreter_class.h.

◆ pc

goto_programt::const_targett interpretert::pc
protected

Definition at line 268 of file interpreter_class.h.

◆ show

bool interpretert::show
protected

Definition at line 271 of file interpreter_class.h.

◆ stack_depth

mp_integer interpretert::stack_depth
protected

Definition at line 279 of file interpreter_class.h.

◆ stack_pointer

mp_integer interpretert::stack_pointer
protected

Definition at line 191 of file interpreter_class.h.

◆ steps

goto_tracet interpretert::steps
protected

Definition at line 269 of file interpreter_class.h.

◆ stop_on_assertion

bool interpretert::stop_on_assertion
protected

Definition at line 272 of file interpreter_class.h.

◆ symbol_table

const symbol_tablet& interpretert::symbol_table
protected

Definition at line 101 of file interpreter_class.h.

◆ target_assert

goto_programt::const_targett interpretert::target_assert
protected

Definition at line 268 of file interpreter_class.h.

◆ thread_id

unsigned interpretert::thread_id
protected

Definition at line 280 of file interpreter_class.h.

◆ total_steps

size_t interpretert::total_steps
protected

Definition at line 275 of file interpreter_class.h.


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