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.

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.

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

Search for a memory scope allocated under name.

mp_integer get_malloc_size (irep_idt name)

Search for the size of the allocated memory for name.

std::optional< 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.

mp_integer get_type_size (const typet &type) const

Wrapper for call get_offset_pointer_bits.

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.

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

Create assignment lhs := value (see analyze_symbol)

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.

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.

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.

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.

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.

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.

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

Similar to get_char_pointer_value.

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.

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.

void process_outstanding_assignments ()

Call add_assignment for each pair in outstanding_assignments.

std::string get_gdb_value (const exprt &expr)

Extract a stringified value from and c-converted expr.

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)

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.

const namespacet ns

expr2ct c_converter

allocate_objectst allocate_objects

std::map< exprt, exprt > assignments

Sequence of assignments collected during analyze_symbols.

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).

std::map< memory_addresst, exprt > values

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

std::vector< memory_scopet > dynamically_allocated

Keep track of the dynamically allocated memory.

std::map< irep_idt, pointer_valuet > memory_map

Keep track of the memory location for the analyzed symbols.

Detailed Description

Interface for extracting values from GDB (building on gdb_apit)

Definition at line 32 of file analyze_symbol.h.

Member Typedef Documentation

◆ memory_addresst

using gdb_value_extractort::memory_addresst = gdb_apit::memory_addresst

Definition at line 58 of file analyze_symbol.h.

◆ pointer_valuet

using gdb_value_extractort::pointer_valuet = gdb_apit::pointer_valuet

Definition at line 57 of file analyze_symbol.h.

Constructor & Destructor Documentation

◆ gdb_value_extractort()

gdb_value_extractort::gdb_value_extractort ( const symbol_table_baset & 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 228 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 154 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 115 of file analyze_symbol.cpp.

◆ create_gdb_process()

void gdb_value_extractort::create_gdb_process ( )

inline

Definition at line 60 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 76 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 67 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 586 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 234 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 610 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 760 of file analyze_symbol.cpp.

◆ get_malloc_pointee()

std::optional< 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 95 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 86 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 367 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 346 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 280 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 497 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 180 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 195 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 693 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 108 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 729 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 156 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 471 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 751 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 68 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 64 of file analyze_symbol.h.

Member Data Documentation

◆ allocate_objects

allocate_objectst gdb_value_extractort::allocate_objects

private

Definition at line 81 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 84 of file analyze_symbol.h.

◆ c_converter

expr2ct gdb_value_extractort::c_converter

private

Definition at line 80 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 151 of file analyze_symbol.h.

◆ gdb_api

gdb_apit gdb_value_extractort::gdb_api

private

Definition at line 74 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 154 of file analyze_symbol.h.

◆ ns

const namespacet gdb_value_extractort::ns

private

Definition at line 79 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 88 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 78 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 92 of file analyze_symbol.h.

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

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