Generates a harness which first assigns global variables with values from a given memory snapshot and then calls a specified function. More...

#include <memory_snapshot_harness_generator.h>

Inheritance diagram for memory_snapshot_harness_generatort:

Collaboration diagram for memory_snapshot_harness_generatort:

Classes
struct	entry_goto_locationt
	User provided goto location: function name and (maybe) location number; the structure wraps this option with a parser. More...

struct	entry_locationt
	Wraps the information needed to identify the entry point. More...

struct	entry_source_locationt
	User provided source location: file name and line number; the structure wraps this option with a parser. More...

struct	preordert
	Simple structure for linearising posets. More...

struct	source_location_matcht
	Wraps the information for source location match candidates. More...

Public Member Functions
	memory_snapshot_harness_generatort (message_handlert &message_handler)

void	generate (goto_modelt &goto_model, const irep_idt &harness_function_name) override
	The main function of this harness, consists of the following: More...

Public Member Functions inherited from goto_harness_generatort
virtual	~goto_harness_generatort ()=default

Protected Member Functions
entry_goto_locationt	parse_goto_location (const std::string &cmdl_option)
	Parse a command line option to extract the user specified entry goto location. More...

entry_source_locationt	parse_source_location (const std::string &cmdl_option)
	Parse a command line option to extract the user specified entry source location. More...

entry_locationt	initialize_entry_via_goto (const entry_goto_locationt &entry_goto_location, const goto_functionst &goto_functions)
	Find and return the entry instruction (requested by the user as goto location: function name + location number) More...

entry_locationt	initialize_entry_via_source (const entry_source_locationt &entry_source_location, const goto_functionst &goto_functions)
	Find and return the entry instruction (requested by the user as source location: file name + line number) More...

void	handle_option (const std::string &option, const std::list< std::string > &values) override
	Collect the memory-snapshot specific cmdline options (one at a time) More...

void	validate_options (const goto_modelt &goto_model) override
	Check that user options make sense: On their own, e.g. More...

void	get_memory_snapshot (const std::string &file, symbol_table_baset &snapshot) const
	Parse the snapshot JSON file and initialise the symbol table. More...

void	add_init_section (const symbol_exprt &func_init_done_var, goto_modelt &goto_model) const
	Modify the entry-point function to start from the user-specified initial location. More...

const symbolt &	fresh_symbol_copy (const symbolt &snapshot_symbol, symbol_table_baset &symbol_table) const
	Introduce a new symbol into `symbol_table` with the same name and type as `snapshot_symbol`. More...

code_blockt	add_assignments_to_globals (const symbol_table_baset &snapshot, goto_modelt &goto_model) const
	For each global symbol in the `snapshot` symbol table either: 1) add code_assignt assigning a value from the `snapshot` to the symbol or 2) recursively initialise the symbol to a non-deterministic value of the right type. More...

void	add_call_with_nondet_arguments (const symbolt &called_function_symbol, code_blockt &code) const
	Create as many non-deterministic arguments as there are arguments of the `called_function_symbol` and add a function call with those arguments. More...

void	insert_harness_function_into_goto_model (goto_modelt &goto_model, const symbolt &function) const
	Insert the `function` into the symbol table (and the goto functions map) of the `goto_model`. More...

size_t	pointer_depth (const typet &t) const
	Recursively compute the pointer depth. More...

template<typename Adder >
void	collect_references (const exprt &expr, Adder &&add_reference) const

Protected Attributes
std::string	memory_snapshot_file
	data to store the command-line options More...

std::string	initial_goto_location_line

std::string	initial_source_location_line

std::unordered_set< irep_idt >	variables_to_havoc

entry_locationt	entry_location
	data to initialize the entry function More...

message_handlert &	message_handler

recursive_initialization_configt	recursive_initialization_config

Detailed Description

Generates a harness which first assigns global variables with values from a given memory snapshot and then calls a specified function.

The called function is also modified such that it appears to start executing at the given location number on the first invocation.

Definition at line 28 of file memory_snapshot_harness_generator.h.

Constructor & Destructor Documentation

◆ memory_snapshot_harness_generatort()

memory_snapshot_harness_generatort::memory_snapshot_harness_generatort ( message_handlert & message_handler )

inlineexplicit

Definition at line 31 of file memory_snapshot_harness_generator.h.

Member Function Documentation

◆ add_assignments_to_globals()

code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals	(	const symbol_table_baset &	snapshot,
		goto_modelt &	goto_model
	)		const

protected

For each global symbol in the snapshot symbol table either: 1) add code_assignt assigning a value from the snapshot to the symbol or 2) recursively initialise the symbol to a non-deterministic value of the right type.

Malloc(ed) pointers point to temporaries which do not exists in the symbol table: for these we introduce fresh symbols.

Parameters

snapshot	snapshot to load the symbols and their values from
goto_model	model to initialise the havoc-ing

Returns: the block of code where the assignments are added

Definition at line 208 of file memory_snapshot_harness_generator.cpp.

◆ add_call_with_nondet_arguments()

void memory_snapshot_harness_generatort::add_call_with_nondet_arguments	(	const symbolt &	called_function_symbol,
		code_blockt &	code
	)		const

protected

Create as many non-deterministic arguments as there are arguments of the called_function_symbol and add a function call with those arguments.

Parameters

called_function_symbol	the function to be called
code	the block of code where the function call is added

Definition at line 289 of file memory_snapshot_harness_generator.cpp.

◆ add_init_section()

void memory_snapshot_harness_generatort::add_init_section	(	const symbol_exprt &	func_init_done_var,
		goto_modelt &	goto_model
	)		const

protected

Modify the entry-point function to start from the user-specified initial location.

Turn this:

int foo() { ..first_part.. i: //location_number=i ..second_part.. }

Into this:

func_init_done; __CPROVER_initialize() { ... func_init_done = false; } int foo() { if (func_init_done) goto 1; func_init_done = true; goto i; 1: ; ..first_part.. i: //location_number=i ..second_part.. }

Parameters

func_init_done_var	symbol expression for the `func_init_done` variable
goto_model	Model where the modification takes place

Definition at line 152 of file memory_snapshot_harness_generator.cpp.

◆ collect_references()

template<typename Adder >

void memory_snapshot_harness_generatort::collect_references	(	const exprt &	expr,
		Adder &&	add_reference
	)		const

inlineprotected

Definition at line 281 of file memory_snapshot_harness_generator.h.

◆ fresh_symbol_copy()

const symbolt & memory_snapshot_harness_generatort::fresh_symbol_copy	(	const symbolt &	snapshot_symbol,
		symbol_table_baset &	symbol_table
	)		const

protected

Introduce a new symbol into symbol_table with the same name and type as snapshot_symbol.

Parameters

snapshot_symbol	the unknown symbol to be introduced
symbol_table	the symbol table to be updated

Returns: the new symbol

Definition at line 183 of file memory_snapshot_harness_generator.cpp.

◆ generate()

void memory_snapshot_harness_generatort::generate	(	goto_modelt &	goto_model,
		const irep_idt &	harness_function_name
	)

overridevirtual

The main function of this harness, consists of the following:

Load memory table from the snapshot.
Add initial section to the user-specified initial location.
Assign global variables their snapshot values (via the harness function).
Insert call of the initial location (with nondet values) into the harness function.
Build symbol for the harness functions.
Insert harness function into goto_model.
Parameters

goto_model goto model to be modified

harness_function_name name of the resulting harness function

Implements goto_harness_generatort.

Definition at line 369 of file memory_snapshot_harness_generator.cpp.

◆ get_memory_snapshot()

void memory_snapshot_harness_generatort::get_memory_snapshot	(	const std::string &	file,
		symbol_table_baset &	snapshot
	)		const

protected

Parse the snapshot JSON file and initialise the symbol table.

Parameters

file	the snapshot JSON file
snapshot	the resulting symbol table built from the snapshot

Definition at line 327 of file memory_snapshot_harness_generator.cpp.

◆ handle_option()

void memory_snapshot_harness_generatort::handle_option	(	const std::string &	option,
		const std::list< std::string > &	values
	)

overrideprotectedvirtual

Collect the memory-snapshot specific cmdline options (one at a time)

Parameters

option	memory-snapshot \| initial-location \| havoc-variables
values	list of arguments related to a given option

Implements goto_harness_generatort.

Definition at line 29 of file memory_snapshot_harness_generator.cpp.

◆ initialize_entry_via_goto()

memory_snapshot_harness_generatort::entry_locationt memory_snapshot_harness_generatort::initialize_entry_via_goto	(	const entry_goto_locationt &	entry_goto_location,
		const goto_functionst &	goto_functions
	)

protected

Find and return the entry instruction (requested by the user as goto location: function name + location number)

Parameters

entry_goto_location	user specified goto location
goto_functions	goto functions to be searched for the entry instruction

Returns: the correctly constructed entry location

Definition at line 470 of file memory_snapshot_harness_generator.cpp.

◆ initialize_entry_via_source()

memory_snapshot_harness_generatort::entry_locationt memory_snapshot_harness_generatort::initialize_entry_via_source	(	const entry_source_locationt &	entry_source_location,
		const goto_functionst &	goto_functions
	)

protected

Find and return the entry instruction (requested by the user as source location: file name + line number)

Parameters

entry_source_location	user specified goto location
goto_functions	goto functions to be searched for the entry instruction

Returns: the correctly constructed entry location

Definition at line 499 of file memory_snapshot_harness_generator.cpp.

◆ insert_harness_function_into_goto_model()

void memory_snapshot_harness_generatort::insert_harness_function_into_goto_model	(	goto_modelt &	goto_model,
		const symbolt &	function
	)		const

protected

Insert the function into the symbol table (and the goto functions map) of the goto_model.

Parameters

goto_model	goto model where the insertion is to take place
function	symbol of the function to be inserted

Definition at line 307 of file memory_snapshot_harness_generator.cpp.

◆ parse_goto_location()

memory_snapshot_harness_generatort::entry_goto_locationt memory_snapshot_harness_generatort::parse_goto_location ( const std::string & cmdl_option )

protected

Parse a command line option to extract the user specified entry goto location.

Parameters

cmdl_option a string of the format name:number

Returns: correctly constructed entry goto location

Definition at line 424 of file memory_snapshot_harness_generator.cpp.

◆ parse_source_location()

memory_snapshot_harness_generatort::entry_source_locationt memory_snapshot_harness_generatort::parse_source_location ( const std::string & cmdl_option )

protected

Parse a command line option to extract the user specified entry source location.

Parameters

cmdl_option a string of the format name:number

Returns: correctly constructed entry source location

Definition at line 450 of file memory_snapshot_harness_generator.cpp.

◆ pointer_depth()

size_t memory_snapshot_harness_generatort::pointer_depth ( const typet & t ) const

protected

Recursively compute the pointer depth.

Parameters

t	input type

Returns: pointer depth of type t

Definition at line 200 of file memory_snapshot_harness_generator.cpp.

◆ validate_options()

void memory_snapshot_harness_generatort::validate_options ( const goto_modelt & goto_model )

overrideprotectedvirtual

Check that user options make sense: On their own, e.g.

location number cannot be specified without a function. In relation to the input program, e.g. function name must be known via the symbol table.

Parameters

goto_model the model containing the symbol table, goto functions, etc.

Implements goto_harness_generatort.

Definition at line 108 of file memory_snapshot_harness_generator.cpp.

Member Data Documentation

◆ entry_location

entry_locationt memory_snapshot_harness_generatort::entry_location

protected

data to initialize the entry function

Definition at line 377 of file memory_snapshot_harness_generator.h.

◆ initial_goto_location_line

std::string memory_snapshot_harness_generatort::initial_goto_location_line

protected

Definition at line 372 of file memory_snapshot_harness_generator.h.

◆ initial_source_location_line

std::string memory_snapshot_harness_generatort::initial_source_location_line

protected

Definition at line 373 of file memory_snapshot_harness_generator.h.

◆ memory_snapshot_file

std::string memory_snapshot_harness_generatort::memory_snapshot_file

protected

data to store the command-line options

Definition at line 371 of file memory_snapshot_harness_generator.h.

◆ message_handler

message_handlert& memory_snapshot_harness_generatort::message_handler

protected

Definition at line 379 of file memory_snapshot_harness_generator.h.

◆ recursive_initialization_config

recursive_initialization_configt memory_snapshot_harness_generatort::recursive_initialization_config

protected

Definition at line 381 of file memory_snapshot_harness_generator.h.

◆ variables_to_havoc

std::unordered_set<irep_idt> memory_snapshot_harness_generatort::variables_to_havoc

protected

Definition at line 374 of file memory_snapshot_harness_generator.h.

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

/home/runner/work/cbmc/cbmc/src/goto-harness/memory_snapshot_harness_generator.h
/home/runner/work/cbmc/cbmc/src/goto-harness/memory_snapshot_harness_generator.cpp

goto_model	goto model to be modified
harness_function_name	name of the resulting harness function

Classes

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ memory_snapshot_harness_generatort()

Member Function Documentation

◆ add_assignments_to_globals()

◆ add_call_with_nondet_arguments()

◆ add_init_section()

◆ collect_references()

◆ fresh_symbol_copy()

◆ generate()

◆ get_memory_snapshot()

◆ handle_option()

◆ initialize_entry_via_goto()

◆ initialize_entry_via_source()

◆ insert_harness_function_into_goto_model()

◆ parse_goto_location()

◆ parse_source_location()

◆ pointer_depth()

◆ validate_options()

Member Data Documentation

◆ entry_location

◆ initial_goto_location_line

◆ initial_source_location_line

◆ memory_snapshot_file

◆ message_handler

◆ recursive_initialization_config

◆ variables_to_havoc