interpretert Class Reference

#include <interpreter_class.h>

Collaboration diagram for interpretert:

Classes
struct	function_assignments_contextt
struct	function_assignmentt
class	memory_cellt
class	stack_framet

Public Types
typedef std::vector< function_assignmentt >	function_assignmentst
typedef std::vector< mp_integer >	mp_vectort
typedef std::pair< irep_idt, irep_idt >	assignment_idt
typedef std::pair< exprt, exprt >	diff_pairt
typedef std::map< assignment_idt, diff_pairt >	side_effects_differencet
typedef std::pair< irep_idt, exprt >	input_entryt
typedef std::map< irep_idt, exprt >	input_valuest
typedef std::map< irep_idt, typet >	dynamic_typest
typedef std::map< irep_idt, function_assignmentst >	output_valuest
typedef std::list< function_assignments_contextt >	function_assignments_contextst
typedef std::map< irep_idt, std::list< function_assignments_contextt > >	list_input_varst

Public Member Functions
	interpretert (const symbol_table_baset &_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.
const dynamic_typest &	get_dynamic_types ()

Public Attributes
output_valuest	output_values

Protected Types
typedef std::unordered_map< irep_idt, mp_integer >	memory_mapt
using	inverse_memory_mapt = std::map< mp_integer, std::optional< symbol_exprt > >
typedef sparse_vectort< memory_cellt >	memoryt
typedef std::map< std::string, const irep_idt & >	parameter_sett
typedef std::pair< const irep_idt, const irep_idt >	struct_member_idt
typedef std::map< struct_member_idt, const exprt >	struct_valuest
typedef std::stack< stack_framet >	call_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.
void	build_memory_map (const symbolt &symbol)
mp_integer	build_memory_map (const symbol_exprt &symbol_expr)
	Populates dynamic entries of the memory map.
typet	concretize_type (const typet &type)
	turns a variable length array type into a fixed array type
bool	unbounded_size (const typet &)
mp_integer	get_size (const typet &type)
	Retrieves the actual size of the provided structured type.
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.
typet	get_type (const irep_idt &id) const
	returns the type object corresponding to id
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
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
exprt	get_value (const irep_idt &id)
void	step ()
	executes a single step and updates the program counter
void	execute_assert ()
void	execute_assume ()
void	execute_assign ()
	executes the assign statement at the current pc value
void	execute_goto ()
	executes a goto instruction
void	execute_function_call ()
void	execute_other ()
	executes side effects of 'other' instructions
void	execute_decl ()
void	clear_input_flags ()
	Clears memoy r/w flag initialization.
void	allocate (const mp_integer &address, const mp_integer &size)
	reserves memory block of size at address
void	assign (const mp_integer &address, const mp_vectort &rhs)
	sets the memory at address with the given rhs value (up to sizeof(rhs))
void	read (const mp_integer &address, mp_vectort &dest) const
	Reads a memory address and loads it into the dest variable.
void	read_unbounded (const mp_integer &address, mp_vectort &dest) const
virtual void	command ()
	reads a user command and executes it.
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.
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'.
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.
mp_vectort	evaluate (const exprt &)
	Evaluate an expression.
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)
void	show_state ()
	displays the current position of the pc and corresponding code

Protected Attributes
messaget	output
const symbol_table_baset &	symbol_table
const namespacet	ns
const goto_functionst &	goto_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_tracet	steps
bool	done
bool	show
size_t	num_steps
size_t	total_steps
dynamic_typest	dynamic_types
int	num_dynamic_objects
unsigned	thread_id

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

Friends
class	interpreter_testt

Detailed Description

Definition at line 28 of file interpreter_class.h.

Member Typedef Documentation

assignment_idt

typedef std::pair<irep_idt, irep_idt> interpretert::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 257 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

typedef std::map<irep_idt, typet> interpretert::dynamic_typest

Definition at line 77 of file interpreter_class.h.

function_assignments_contextst

typedef std::list<function_assignments_contextt> interpretert::function_assignments_contextst

Definition at line 94 of file interpreter_class.h.

function_assignmentst

typedef std::vector<function_assignmentt> interpretert::function_assignmentst

Definition at line 57 of file interpreter_class.h.

input_entryt

typedef std::pair<irep_idt, exprt> interpretert::input_entryt

Definition at line 71 of file interpreter_class.h.

input_valuest

typedef std::map<irep_idt, exprt> interpretert::input_valuest

Definition at line 74 of file interpreter_class.h.

inverse_memory_mapt

using interpretert::inverse_memory_mapt = std::map<mp_integer, std::optional<symbol_exprt> >

protected

Definition at line 110 of file interpreter_class.h.

list_input_varst

typedef std::map<irep_idt, std::list<function_assignments_contextt> > interpretert::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 109 of file interpreter_class.h.

memoryt

typedef sparse_vectort<memory_cellt> interpretert::memoryt

protected

Definition at line 181 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

typedef std::map<irep_idt, function_assignmentst> interpretert::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 182 of file interpreter_class.h.

side_effects_differencet

typedef std::map<assignment_idt, diff_pairt> interpretert::side_effects_differencet

Definition at line 68 of file interpreter_class.h.

struct_member_idt

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

protected

Definition at line 184 of file interpreter_class.h.

struct_valuest

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

protected

Definition at line 185 of file interpreter_class.h.

Constructor & Destructor Documentation

interpretert()

interpretert::interpretert ( const symbol_table_baset &  _symbol_table, const goto_functionst &  _goto_functions, message_handlert &  _message_handler  )

inline

Definition at line 31 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 114 of file interpreter_class.h.

address_to_offset()

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

inlineprotected

Definition at line 131 of file interpreter_class.h.

address_to_symbol()

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

inlineprotected

Definition at line 126 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 85 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 693 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 147 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 136 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 842 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 909 of file interpreter.cpp.

build_memory_map() [3/3]

void interpretert::build_memory_map ( const symbolt &  symbol )

protected

Definition at line 860 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 160 of file interpreter_evaluate.cpp.

clear_input_flags()

void interpretert::clear_input_flags ( )

protected

Clears memoy r/w flag initialization.

Definition at line 102 of file interpreter_evaluate.cpp.

command()

void interpretert::command ( )

protectedvirtual

reads a user command and executes it.

Definition at line 129 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 883 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

	ty	a type
[out]	result	Number of leaf primitive types in ty

Returns

returns true on error

Definition at line 118 of file interpreter_evaluate.cpp.

evaluate()

interpretert::mp_vectort interpretert::evaluate ( const exprt &  expr )

protected

Evaluate an expression.

Parameters

expr	expression to evaluate

Returns

vector in which the result of the evaluation is stored

Definition at line 312 of file interpreter_evaluate.cpp.

evaluate_address()

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

protected

Definition at line 995 of file interpreter_evaluate.cpp.

evaluate_boolean()

bool interpretert::evaluate_boolean ( const exprt &  expr )

inlineprotected

Definition at line 276 of file interpreter_class.h.

execute_assert()

void interpretert::execute_assert ( )

protected

Definition at line 724 of file interpreter.cpp.

execute_assign()

void interpretert::execute_assign ( )

protected

executes the assign statement at the current pc value

Definition at line 649 of file interpreter.cpp.

execute_assume()

void interpretert::execute_assume ( )

protected

Definition at line 718 of file interpreter.cpp.

execute_decl()

void interpretert::execute_decl ( )

protected

Definition at line 418 of file interpreter.cpp.

execute_function_call()

void interpretert::execute_function_call ( )

protected

Definition at line 734 of file interpreter.cpp.

execute_goto()

void interpretert::execute_goto ( )

protected

executes a goto instruction

Definition at line 369 of file interpreter.cpp.

execute_other()

void interpretert::execute_other ( )

protected

executes side effects of 'other' instructions

Definition at line 384 of file interpreter.cpp.

get_component()

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 425 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^(platform bit-width / 2 + 1) address space each.

Parameters

type	a structured type

Returns

Size of the given type

Definition at line 963 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 448 of file interpreter.cpp.

get_value() [1/3]

exprt interpretert::get_value ( const irep_idt &  id )

protected

Definition at line 1025 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 458 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 523 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 62 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 241 of file interpreter_evaluate.cpp.

operator()()

void interpretert::operator()

(

)

Definition at line 38 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 1045 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 31 of file interpreter_evaluate.cpp.

read_unbounded()

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

protected

Definition at line 55 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 110 of file interpreter.cpp.

step()

void interpretert::step ( )

protected

executes a single step and updates the program counter

Definition at line 234 of file interpreter.cpp.

unbounded_size()

bool interpretert::unbounded_size ( const typet &  type )

protected

Definition at line 940 of file interpreter.cpp.

Friends And Related Symbol Documentation

interpreter_testt

friend class interpreter_testt

friend

Definition at line 305 of file interpreter_class.h.

Member Data Documentation

call_stack

call_stackt interpretert::call_stack

protected

Definition at line 259 of file interpreter_class.h.

done

bool interpretert::done

protected

Definition at line 266 of file interpreter_class.h.

dynamic_types

dynamic_typest interpretert::dynamic_types

protected

Definition at line 272 of file interpreter_class.h.

function

goto_functionst::function_mapt::const_iterator interpretert::function

protected

Definition at line 263 of file interpreter_class.h.

function_input_vars

list_input_varst interpretert::function_input_vars

protected

Definition at line 261 of file interpreter_class.h.

goto_functions

const goto_functionst& interpretert::goto_functions

protected

Definition at line 107 of file interpreter_class.h.

input_vars

input_valuest interpretert::input_vars

protected

Definition at line 260 of file interpreter_class.h.

inverse_memory_map

inverse_memory_mapt interpretert::inverse_memory_map

protected

Definition at line 112 of file interpreter_class.h.

memory

memoryt interpretert::memory

mutableprotected

Definition at line 190 of file interpreter_class.h.

memory_map

memory_mapt interpretert::memory_map

protected

Definition at line 111 of file interpreter_class.h.

next_pc

goto_programt::const_targett interpretert::next_pc

protected

Definition at line 264 of file interpreter_class.h.

npos

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

staticprotected

Definition at line 268 of file interpreter_class.h.

ns

const namespacet interpretert::ns

protected

Definition at line 105 of file interpreter_class.h.

num_dynamic_objects

int interpretert::num_dynamic_objects

protected

Definition at line 273 of file interpreter_class.h.

num_steps

size_t interpretert::num_steps

protected

Definition at line 269 of file interpreter_class.h.

output

messaget interpretert::output

protected

Definition at line 101 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 264 of file interpreter_class.h.

show

bool interpretert::show

protected

Definition at line 267 of file interpreter_class.h.

stack_pointer

mp_integer interpretert::stack_pointer

protected

Definition at line 192 of file interpreter_class.h.

steps

goto_tracet interpretert::steps

protected

Definition at line 265 of file interpreter_class.h.

symbol_table

const symbol_table_baset& interpretert::symbol_table

protected

Definition at line 102 of file interpreter_class.h.

thread_id

unsigned interpretert::thread_id

protected

Definition at line 274 of file interpreter_class.h.

total_steps

size_t interpretert::total_steps

protected

Definition at line 270 of file interpreter_class.h.

---

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

• /home/runner/work/cbmc/cbmc/src/goto-programs/interpreter_class.h
• /home/runner/work/cbmc/cbmc/src/goto-programs/interpreter.cpp
• /home/runner/work/cbmc/cbmc/src/goto-programs/interpreter_evaluate.cpp