Interface for extracting values from GDB (building on gdb_apit) More...

#include <analyze_symbol.h>

Collaboration diagram for gdb_value_extractort:

Classes
struct	memory_scopet

Public Types
using	pointer_valuet = gdb_apit::pointer_valuet

using	memory_addresst = gdb_apit::memory_addresst

Public Member Functions
	gdb_value_extractort (const symbol_tablet &symbol_table, const std::vector< std::string > &args)

void	analyze_symbols (const std::list< std::string > &symbols)
	For each input symbol in `symbols:` map its value address to its symbol_exprt (via the `values` map) and then call analyze_symbol on it. More...

std::string	get_snapshot_as_c_code ()
	Get memory snapshot as C code. More...

symbol_tablet	get_snapshot_as_symbol_table ()
	Get memory snapshot as symbol table Build a new symbol_tablet and for each `lhs` symbol from collected assignments [lhs:=rhs] store a new symbol (with the `rhs` as value) there. More...

void	create_gdb_process ()

bool	run_gdb_to_breakpoint (const std::string &breakpoint)

void	run_gdb_from_core (const std::string &corefile)

Private Member Functions
bool	has_known_memory_location (const irep_idt &id) const

std::vector< memory_scopet >::iterator	find_dynamic_allocation (irep_idt name)
	Search for a memory scope allocated under `name`. More...

std::vector< memory_scopet >::iterator	find_dynamic_allocation (const memory_addresst &point)
	Search for a memory scope allocated under `name`. More...

mp_integer	get_malloc_size (irep_idt name)
	Search for the size of the allocated memory for `name`. More...

optionalt< std::string >	get_malloc_pointee (const memory_addresst &point, mp_integer member_size)
	Build the pointee string for address `point` assuming it points to a dynamic allocation of ‘n’ elements each of size `member_size`. More...

mp_integer	get_type_size (const typet &type) const
	Wrapper for call get_offset_pointer_bits. More...

void	analyze_symbol (const irep_idt &symbol_name)
	Assign the gdb-extracted value for `symbol_name` to its symbol expression and then process outstanding assignments that this extraction introduced. More...

void	add_assignment (const exprt &lhs, const exprt &value)
	Create assignment `lhs` := `value` (see analyze_symbol) More...

exprt	get_array_value (const exprt &expr, const exprt &array, const source_locationt &location)
	Iterate over `array` and fill its operands with the results of calling get_expr_value on index expressions into `expr`. More...

exprt	get_expr_value (const exprt &expr, const exprt &zero_expr, const source_locationt &location)
	Case analysis on the typet of `expr` 1) For integers, booleans, and enums: call gdb_apit::get_value directly 2) For chars: return the `zero_expr` 3) For structs, arrays, and pointers: call their dedicated functions. More...

exprt	get_struct_value (const exprt &expr, const exprt &zero_expr, const source_locationt &location)
	For each of the members of the struct: call get_expr_value. More...

exprt	get_union_value (const exprt &expr, const exprt &zero_expr, const source_locationt &location)
	For each of the members of the struct: call get_expr_value. More...

exprt	get_pointer_value (const exprt &expr, const exprt &zero_expr, const source_locationt &location)
	Call gdb_apit::get_memory on `expr` then split based on the points-to type being `char` type or not. More...

exprt	get_pointer_to_member_value (const exprt &expr, const pointer_valuet &pointer_value, const source_locationt &location)
	Call get_subexpression_at_offset to get the correct member expression. More...

exprt	get_non_char_pointer_value (const exprt &expr, const pointer_valuet &value, const source_locationt &location)
	Similar to get_char_pointer_value. More...

exprt	get_pointer_to_function_value (const exprt &expr, const pointer_valuet &pointer_value, const source_locationt &location)
	Extract the function name from `pointer_value`, check it has a symbol and return the associated symbol expression. More...

exprt	get_char_pointer_value (const exprt &expr, const memory_addresst &memory_location, const source_locationt &location)
	If `memory_location` is found among values then return the symbol expression associated with it. More...

void	process_outstanding_assignments ()
	Call add_assignment for each pair in outstanding_assignments. More...

std::string	get_gdb_value (const exprt &expr)
	Extract a stringified value from and c-converted `expr`. More...

bool	points_to_member (pointer_valuet &pointer_value, const pointer_typet &expected_type)
	Analyzes the `pointer_value` to decide if it point to a struct or a union (or array) More...

Private Attributes
gdb_apit	gdb_api

symbol_tablet	symbol_table
	External symbol table – extracted from read_goto_binary We only expect to analyse symbols located there. More...

const namespacet	ns

expr2ct	c_converter

allocate_objectst	allocate_objects

std::map< exprt, exprt >	assignments
	Sequence of assignments collected during analyze_symbols. More...

std::map< exprt, memory_addresst >	outstanding_assignments
	Mapping pointer expression for which get_non_char_pointer_value returned nil expression to memory location (from gdb_apit). More...

std::map< memory_addresst, exprt >	values
	Storing pairs <address, symbol> such that at `address` is stored the value of `symbol`. More...

std::vector< memory_scopet >	dynamically_allocated
	Keep track of the dynamically allocated memory. More...

std::map< irep_idt, pointer_valuet >	memory_map
	Keep track of the memory location for the analyzed symbols. More...

Detailed Description

Interface for extracting values from GDB (building on gdb_apit)

Definition at line 36 of file analyze_symbol.h.

Member Typedef Documentation

◆ memory_addresst

using gdb_value_extractort::memory_addresst = gdb_apit::memory_addresst

Definition at line 62 of file analyze_symbol.h.

◆ pointer_valuet

using gdb_value_extractort::pointer_valuet = gdb_apit::pointer_valuet

Definition at line 61 of file analyze_symbol.h.

Constructor & Destructor Documentation

◆ gdb_value_extractort()

gdb_value_extractort::gdb_value_extractort	(	const symbol_tablet &	symbol_table,
		const std::vector< std::string > &	args
	)

Definition at line 24 of file analyze_symbol.cpp.

Member Function Documentation

◆ add_assignment()

void gdb_value_extractort::add_assignment	(	const exprt &	lhs,
		const exprt &	value
	)

private

Create assignment lhs := value (see analyze_symbol)

Parameters

lhs	the left-hand side of the assignment; expected to be a symbol_exprt
value	the value to be assigned; the result of get_expr_value

Definition at line 222 of file analyze_symbol.cpp.

◆ analyze_symbol()

void gdb_value_extractort::analyze_symbol ( const irep_idt & symbol_name )

private

Assign the gdb-extracted value for symbol_name to its symbol expression and then process outstanding assignments that this extraction introduced.

Parameters

symbol_name symbol table name to be analysed

Definition at line 148 of file analyze_symbol.cpp.

◆ analyze_symbols()

void gdb_value_extractort::analyze_symbols ( const std::list< std::string > & symbols )

For each input symbol in symbols: map its value address to its symbol_exprt (via the values map) and then call analyze_symbol on it.

Parameters

symbols names of symbols to be analysed

Definition at line 109 of file analyze_symbol.cpp.

◆ create_gdb_process()

void gdb_value_extractort::create_gdb_process ( )

inline

Definition at line 64 of file analyze_symbol.h.

◆ find_dynamic_allocation() [1/2]

std::vector< gdb_value_extractort::memory_scopet >::iterator gdb_value_extractort::find_dynamic_allocation ( const memory_addresst & point )

private

Search for a memory scope allocated under name.

Parameters

point potentially dynamically allocated memory address

Returns: iterator to the right memory scope

Definition at line 70 of file analyze_symbol.cpp.

◆ find_dynamic_allocation() [2/2]

std::vector< gdb_value_extractort::memory_scopet >::iterator gdb_value_extractort::find_dynamic_allocation ( irep_idt name )

private

Search for a memory scope allocated under name.

Parameters

name	name of the pointer used during allocation

Returns: iterator to the right memory scope

Definition at line 61 of file analyze_symbol.cpp.

◆ get_array_value()

exprt gdb_value_extractort::get_array_value	(	const exprt &	expr,
		const exprt &	array,
		const source_locationt &	location
	)

private

Iterate over array and fill its operands with the results of calling get_expr_value on index expressions into expr.

Parameters

expr	the expression to be analysed
array	array with zero-initialised elements
location	the source location return an array of the same type as `expr` filled with values from gdb

Definition at line 580 of file analyze_symbol.cpp.

◆ get_char_pointer_value()

exprt gdb_value_extractort::get_char_pointer_value	(	const exprt &	expr,
		const memory_addresst &	memory_location,
		const source_locationt &	location
	)

private

If memory_location is found among values then return the symbol expression associated with it.

Otherwise we add the appropriate values mapping: 1) call gdb_apit::get_memory on the expr 2) allocate new symbol and assign it with the memory string from 1) 3) fill values (mapping memory_location to the new symbol)

Parameters

expr	the pointer expression to be analysed
memory_location	pointer value from gdb_apit::get_memory
location	the source location

Returns: symbol expression associated with memory_location

Definition at line 228 of file analyze_symbol.cpp.

◆ get_expr_value()

exprt gdb_value_extractort::get_expr_value	(	const exprt &	expr,
		const exprt &	zero_expr,
		const source_locationt &	location
	)

private

Case analysis on the typet of expr 1) For integers, booleans, and enums: call gdb_apit::get_value directly 2) For chars: return the zero_expr 3) For structs, arrays, and pointers: call their dedicated functions.

Parameters

expr	the expression to be analysed
zero_expr	zero of the same type as `expr`
location	the source location

Returns: the value of the expression extracted from gdb_apit

Definition at line 604 of file analyze_symbol.cpp.

◆ get_gdb_value()

std::string gdb_value_extractort::get_gdb_value ( const exprt & expr )

private

Extract a stringified value from and c-converted expr.

Parameters

expr	expression to be extracted

Returns: the value as a string

Definition at line 751 of file analyze_symbol.cpp.

◆ get_malloc_pointee()

optionalt< std::string > gdb_value_extractort::get_malloc_pointee	(	const memory_addresst &	point,
		mp_integer	member_size
	)

private

Build the pointee string for address point assuming it points to a dynamic allocation of ‘n’ elements each of size member_size.

E.g.:

int p = (int)malloc(sizeof(int)*4); int *q = &(p[2]);

get_malloc_pointee(get_memory(q), sizeof(int)) -> "p+8"

Parameters

point	potentially dynamically allocated memory address
member_size	size of each allocated element

Returns: pointee as a string if we have a record of the allocation

Definition at line 89 of file analyze_symbol.cpp.

◆ get_malloc_size()

mp_integer gdb_value_extractort::get_malloc_size ( irep_idt name )

private

Search for the size of the allocated memory for name.

Parameters

name	name of the pointer used during allocation

Returns: the size if have a record of name's allocation (1 otherwise)

Definition at line 80 of file analyze_symbol.cpp.

◆ get_non_char_pointer_value()

exprt gdb_value_extractort::get_non_char_pointer_value	(	const exprt &	expr,
		const pointer_valuet &	value,
		const source_locationt &	location
	)

private

Similar to get_char_pointer_value.

Doesn't re-call gdb_apit::get_memory, calls get_expr_value on dereferenced expr (the result of which is assigned to a new symbol).

Parameters

expr	the pointer expression to be analysed
value	pointer value from gdb_apit::get_memory
location	the source location

Returns: symbol expression associated with memory_location

Definition at line 361 of file analyze_symbol.cpp.

◆ get_pointer_to_function_value()

exprt gdb_value_extractort::get_pointer_to_function_value	(	const exprt &	expr,
		const pointer_valuet &	pointer_value,
		const source_locationt &	location
	)

private

Extract the function name from pointer_value, check it has a symbol and return the associated symbol expression.

Parameters

expr	the pointer-to-function expression
pointer_value	pointer value with the function name as the pointee member
location	the source location

Returns: symbol expression for the function pointed at by pointer_value

Definition at line 340 of file analyze_symbol.cpp.

◆ get_pointer_to_member_value()

exprt gdb_value_extractort::get_pointer_to_member_value	(	const exprt &	expr,
		const pointer_valuet &	pointer_value,
		const source_locationt &	location
	)

private

Call get_subexpression_at_offset to get the correct member expression.

Parameters

expr	the input pointer expression (needed to get the right type)
pointer_value	pointer value with structure name and offset as the pointee member
location	the source location

Returns: member_exprt that the pointer_value points to

Definition at line 274 of file analyze_symbol.cpp.

◆ get_pointer_value()

exprt gdb_value_extractort::get_pointer_value	(	const exprt &	expr,
		const exprt &	zero_expr,
		const source_locationt &	location
	)

private

Call gdb_apit::get_memory on expr then split based on the points-to type being char type or not.

These have dedicated functions.

Parameters

expr	the input pointer expression
zero_expr	null-pointer (or its equivalent)
location	the source location

Returns: symbol expression associated with the gdb-extracted memory location

Definition at line 491 of file analyze_symbol.cpp.

◆ get_snapshot_as_c_code()

std::string gdb_value_extractort::get_snapshot_as_c_code ( )

Get memory snapshot as C code.

Returns: converted block of code with the collected assignments

Definition at line 174 of file analyze_symbol.cpp.

◆ get_snapshot_as_symbol_table()

symbol_tablet gdb_value_extractort::get_snapshot_as_symbol_table ( )

Get memory snapshot as symbol table Build a new symbol_tablet and for each lhs symbol from collected assignments [lhs:=rhs] store a new symbol (with the rhs as value) there.

Get memory snapshot as symbol table.

Also, type symbols are copied from symbol_table.

Returns: a new symbol table with known symbols having their extracted values

Definition at line 189 of file analyze_symbol.cpp.

◆ get_struct_value()

exprt gdb_value_extractort::get_struct_value	(	const exprt &	expr,
		const exprt &	zero_expr,
		const source_locationt &	location
	)

private

For each of the members of the struct: call get_expr_value.

Parameters

expr	struct expression to be analysed
zero_expr	struct with zero-initialised members
location	the source location

Returns: the value of the struct from gdb_apit

Definition at line 687 of file analyze_symbol.cpp.

◆ get_type_size()

mp_integer gdb_value_extractort::get_type_size ( const typet & type ) const

private

Wrapper for call get_offset_pointer_bits.

Parameters

type	type to get the size of

Returns: the size of the type in bytes

Definition at line 102 of file analyze_symbol.cpp.

◆ get_union_value()

exprt gdb_value_extractort::get_union_value	(	const exprt &	expr,
		const exprt &	zero_expr,
		const source_locationt &	location
	)

private

For each of the members of the struct: call get_expr_value.

Parameters

expr	struct expression to be analysed
zero_expr	struct with zero-initialised members
location	the source location

Returns: the value of the struct from gdb_apit

Definition at line 720 of file analyze_symbol.cpp.

◆ has_known_memory_location()

bool gdb_value_extractort::has_known_memory_location ( const irep_idt & id ) const

inlineprivate

Definition at line 160 of file analyze_symbol.h.

◆ points_to_member()

bool gdb_value_extractort::points_to_member	(	pointer_valuet &	pointer_value,
		const pointer_typet &	expected_type
	)

private

Analyzes the pointer_value to decide if it point to a struct or a union (or array)

Parameters

pointer_value	pointer value to be analyzed
expected_type	type of the potential member

Returns: true if pointing to a member

Definition at line 465 of file analyze_symbol.cpp.

◆ process_outstanding_assignments()

void gdb_value_extractort::process_outstanding_assignments ( )

private

Call add_assignment for each pair in outstanding_assignments.

Definition at line 742 of file analyze_symbol.cpp.

◆ run_gdb_from_core()

void gdb_value_extractort::run_gdb_from_core ( const std::string & corefile )

inline

Definition at line 72 of file analyze_symbol.h.

◆ run_gdb_to_breakpoint()

bool gdb_value_extractort::run_gdb_to_breakpoint ( const std::string & breakpoint )

inline

Definition at line 68 of file analyze_symbol.h.

Member Data Documentation

◆ allocate_objects

allocate_objectst gdb_value_extractort::allocate_objects

private

Definition at line 85 of file analyze_symbol.h.

◆ assignments

std::map<exprt, exprt> gdb_value_extractort::assignments

private

Sequence of assignments collected during analyze_symbols.

Definition at line 88 of file analyze_symbol.h.

◆ c_converter

expr2ct gdb_value_extractort::c_converter

private

Definition at line 84 of file analyze_symbol.h.

◆ dynamically_allocated

std::vector<memory_scopet> gdb_value_extractort::dynamically_allocated

private

Keep track of the dynamically allocated memory.

Definition at line 155 of file analyze_symbol.h.

◆ gdb_api

gdb_apit gdb_value_extractort::gdb_api

private

Definition at line 78 of file analyze_symbol.h.

◆ memory_map

std::map<irep_idt, pointer_valuet> gdb_value_extractort::memory_map

private

Keep track of the memory location for the analyzed symbols.

Definition at line 158 of file analyze_symbol.h.

◆ ns

const namespacet gdb_value_extractort::ns

private

Definition at line 83 of file analyze_symbol.h.

◆ outstanding_assignments

std::map<exprt, memory_addresst> gdb_value_extractort::outstanding_assignments

private

Mapping pointer expression for which get_non_char_pointer_value returned nil expression to memory location (from gdb_apit).

Definition at line 92 of file analyze_symbol.h.

◆ symbol_table

symbol_tablet gdb_value_extractort::symbol_table

private

External symbol table – extracted from read_goto_binary We only expect to analyse symbols located there.

Definition at line 82 of file analyze_symbol.h.

◆ values

std::map<memory_addresst, exprt> gdb_value_extractort::values

private

Storing pairs <address, symbol> such that at address is stored the value of symbol.

Definition at line 96 of file analyze_symbol.h.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/memory-analyzer/analyze_symbol.h
/home/runner/work/cbmc-documentation/cbmc-documentation/src/memory-analyzer/analyze_symbol.cpp

Classes

Public Types

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ memory_addresst

◆ pointer_valuet

Constructor & Destructor Documentation

◆ gdb_value_extractort()

Member Function Documentation

◆ add_assignment()

◆ analyze_symbol()

◆ analyze_symbols()

◆ create_gdb_process()

◆ find_dynamic_allocation() [1/2]

◆ find_dynamic_allocation() [2/2]

◆ get_array_value()

◆ get_char_pointer_value()

◆ get_expr_value()

◆ get_gdb_value()

◆ get_malloc_pointee()

◆ get_malloc_size()

◆ get_non_char_pointer_value()

◆ get_pointer_to_function_value()

◆ get_pointer_to_member_value()

◆ get_pointer_value()

◆ get_snapshot_as_c_code()

◆ get_snapshot_as_symbol_table()

◆ get_struct_value()

◆ get_type_size()

◆ get_union_value()

◆ has_known_memory_location()

◆ points_to_member()

◆ process_outstanding_assignments()

◆ run_gdb_from_core()

◆ run_gdb_to_breakpoint()

Member Data Documentation

◆ allocate_objects

◆ assignments

◆ c_converter

◆ dynamically_allocated

◆ gdb_api

◆ memory_map

◆ ns

◆ outstanding_assignments

◆ symbol_table

◆ values