Class for generating initialisation code for compound structures. More...

#include <recursive_initialization.h>

Collaboration diagram for recursive_initializationt:

Classes
struct	constructor_keyt

Public Types
using	recursion_sett = std::set< irep_idt >

using	equal_cluster_idt = std::size_t

using	type_constructor_namest = std::map< constructor_keyt, irep_idt >

Public Member Functions
	recursive_initializationt (recursive_initialization_configt initialization_config, goto_modelt &goto_model)

void	initialize (const exprt &lhs, const exprt &depth, code_blockt &body)
	Generate initialisation code for lhs into body.

bool	needs_freeing (const exprt &expr) const

void	free_if_possible (const exprt &expr, code_blockt &body)

void	free_cluster_origins (code_blockt &body)

Static Public Member Functions
static bool	is_initialization_allowed (const symbolt &symbol)

Private Member Functions
bool	should_be_treated_as_array (const irep_idt &pointer_name) const

std::optional< equal_cluster_idt >	find_equal_cluster (const irep_idt &name) const

bool	is_array_size_parameter (const irep_idt &cmdline_arg) const

std::optional< irep_idt >	get_associated_size_variable (const irep_idt &array_name) const

bool	should_be_treated_as_cstring (const irep_idt &pointer_name) const

irep_idt	get_fresh_global_name (const std::string &symbol_name, const exprt &initial_value) const
	Construct a new global symbol of type `int` and set it's value to `initial_value`.

symbol_exprt	get_fresh_global_symexpr (const std::string &symbol_name) const
	Construct a new global symbol of type `int` initialised to 0.

symbol_exprt	get_fresh_local_symexpr (const std::string &symbol_name) const
	Construct a new local symbol of type `int` initialised to 0.

symbol_exprt	get_fresh_local_typed_symexpr (const std::string &symbol_name, const typet &type) const
	Construct a new local symbol of type `type` initialised to `init_value`.

const symbolt &	get_fresh_fun_symbol (const std::string &fun_name, const typet &fun_type)
	Construct a new function symbol of type `fun_type`.

symbolt &	get_fresh_param_symbol (const std::string &param_name, const typet &param_type)
	Construct a new parameter symbol of type `param_type`.

symbol_exprt	get_symbol_expr (const irep_idt &symbol_name) const
	Recover the symbol expression from symbol table.

std::string	type2id (const typet &type) const
	Simple pretty-printer for typet.

code_blockt	build_constructor_body (const exprt &depth_symbol, const symbol_exprt &result_symbol, const std::optional< exprt > &size_symbol, const std::optional< irep_idt > &lhs_name, const bool is_nullable)
	Case analysis for which constructor should be used.

irep_idt	build_constructor (const exprt &expr)
	Check if a constructor for the type of `expr` already exists and create it if not.

code_blockt	build_function_pointer_constructor (const symbol_exprt &result, bool is_nullable)
	Constructor for function pointers.

code_blockt	build_pointer_constructor (const exprt &depth, const symbol_exprt &result)
	Generic constructor for all pointers: only builds one pointee (not an array) but may recourse in case the pointee contains more pointers, e.g.

code_blockt	build_struct_constructor (const exprt &depth, const symbol_exprt &result)
	Constructor for structures: simply iterates over members and initialise each one.

code_blockt	build_nondet_constructor (const symbol_exprt &result) const
	Default constructor: assigns non-deterministic value of the right type.

code_blockt	build_array_constructor (const exprt &depth, const symbol_exprt &result)
	Constructor for arrays: simply iterates over elements and initialise each one.

code_blockt	build_dynamic_array_constructor (const exprt &depth, const symbol_exprt &result, const exprt &size, const std::optional< irep_idt > &lhs_name)
	Constructor for dynamic arrays: allocate memory for `n` elements (`n` is random but bounded) and initialise each one.

void	initialize_selected_member (const exprt &lhs, const exprt &depth, code_blockt &body, const std::vector< irep_idt > &selection_spec)
	Select the specified struct-member to be non-deterministically initialized.

code_blockt	deallocate_code (const exprt &pointer) const
	Generate code mimicking __CPROVER_deallocate (which is what C's free calls) with `pointer` as argument.

Private Attributes
const recursive_initialization_configt	initialization_config

goto_modelt &	goto_model

irep_idt	max_depth_var_name

irep_idt	min_depth_var_name

type_constructor_namest	type_constructor_names

std::vector< std::optional< exprt > >	common_arguments_origins

Detailed Description

Class for generating initialisation code for compound structures.

Definition at line 62 of file recursive_initialization.h.

Member Typedef Documentation

◆ equal_cluster_idt

using recursive_initializationt::equal_cluster_idt = std::size_t

Definition at line 66 of file recursive_initialization.h.

◆ recursion_sett

using recursive_initializationt::recursion_sett = std::set<irep_idt>

Definition at line 65 of file recursive_initialization.h.

◆ type_constructor_namest

using recursive_initializationt::type_constructor_namest = std::map<constructor_keyt, irep_idt>

Definition at line 89 of file recursive_initialization.h.

Constructor & Destructor Documentation

◆ recursive_initializationt()

recursive_initializationt::recursive_initializationt	(	recursive_initialization_configt	initialization_config,
		goto_modelt &	goto_model
	)

Definition at line 118 of file recursive_initialization.cpp.

Member Function Documentation

◆ build_array_constructor()

code_blockt recursive_initializationt::build_array_constructor	(	const exprt &	depth,
		const symbol_exprt &	result
	)

private

Constructor for arrays: simply iterates over elements and initialise each one.

Parameters

depth	symbol of the depth parameter
result	symbol of the result parameter

Returns: the body of the constructor

Definition at line 714 of file recursive_initialization.cpp.

◆ build_constructor()

irep_idt recursive_initializationt::build_constructor ( const exprt & expr )

private

Check if a constructor for the type of expr already exists and create it if not.

Parameters

expr	the expression to be constructed

Returns: name of the constructor function

Definition at line 291 of file recursive_initialization.cpp.

◆ build_constructor_body()

code_blockt recursive_initializationt::build_constructor_body	(	const exprt &	depth_symbol,
		const symbol_exprt &	result_symbol,
		const std::optional< exprt > &	size_symbol,
		const std::optional< irep_idt > &	lhs_name,
		const bool	is_nullable
	)

private

Case analysis for which constructor should be used.

Parameters

depth_symbol	the symbol for `depth` parameter
result_symbol	the symbol for `result` parameter
size_symbol	maybe the symbol for `size` parameter
lhs_name	the name of the original symbol
is_nullable	flag for setting a function pointer nullable

Returns: the body of the constructor

Definition at line 246 of file recursive_initialization.cpp.

◆ build_dynamic_array_constructor()

code_blockt recursive_initializationt::build_dynamic_array_constructor	(	const exprt &	depth,
		const symbol_exprt &	result,
		const exprt &	size,
		const std::optional< irep_idt > &	lhs_name
	)

private

Constructor for dynamic arrays: allocate memory for n elements (n is random but bounded) and initialise each one.

Parameters

depth	symbol of the depth parameter
result	symbol of the result parameter
size	symbol of the size parameter
lhs_name	name of the original symbol

Returns: the body of the constructor

Definition at line 786 of file recursive_initialization.cpp.

◆ build_function_pointer_constructor()

code_blockt recursive_initializationt::build_function_pointer_constructor	(	const symbol_exprt &	result,
		bool	is_nullable
	)

private

Constructor for function pointers.

Parameters

result	symbol of the result parameter
is_nullable	if the function pointer can be null

Returns: the body of the constructor

Definition at line 976 of file recursive_initialization.cpp.

◆ build_nondet_constructor()

code_blockt recursive_initializationt::build_nondet_constructor ( const symbol_exprt & result ) const

private

Default constructor: assigns non-deterministic value of the right type.

Parameters

result symbol of the result parameter

Returns: the body of the constructor

Definition at line 774 of file recursive_initialization.cpp.

◆ build_pointer_constructor()

code_blockt recursive_initializationt::build_pointer_constructor	(	const exprt &	depth,
		const symbol_exprt &	result
	)

private

Generic constructor for all pointers: only builds one pointee (not an array) but may recourse in case the pointee contains more pointers, e.g.

a struct.

Parameters

depth	symbol of the depth parameter
result	symbol of the result parameter

Returns: the body of the constructor

Definition at line 615 of file recursive_initialization.cpp.

◆ build_struct_constructor()

code_blockt recursive_initializationt::build_struct_constructor	(	const exprt &	depth,
		const symbol_exprt &	result
	)

private

Constructor for structures: simply iterates over members and initialise each one.

Parameters

depth	symbol of the depth parameter
result	symbol of the result parameter

Returns: the body of the constructor

Definition at line 736 of file recursive_initialization.cpp.

◆ deallocate_code()

code_blockt recursive_initializationt::deallocate_code ( const exprt & pointer ) const

private

Generate code mimicking __CPROVER_deallocate (which is what C's free calls) with pointer as argument.

Definition at line 919 of file recursive_initialization.cpp.

◆ find_equal_cluster()

std::optional< recursive_initializationt::equal_cluster_idt > recursive_initializationt::find_equal_cluster ( const irep_idt & name ) const

private

Definition at line 383 of file recursive_initialization.cpp.

◆ free_cluster_origins()

void recursive_initializationt::free_cluster_origins ( code_blockt & body )

Definition at line 968 of file recursive_initialization.cpp.

◆ free_if_possible()

void recursive_initializationt::free_if_possible	(	const exprt &	expr,
		code_blockt &	body
	)

Definition at line 936 of file recursive_initialization.cpp.

◆ get_associated_size_variable()

std::optional< irep_idt > recursive_initializationt::get_associated_size_variable ( const irep_idt & array_name ) const

private

Definition at line 403 of file recursive_initialization.cpp.

◆ get_fresh_fun_symbol()

const symbolt & recursive_initializationt::get_fresh_fun_symbol	(	const std::string &	fun_name,
		const typet &	fun_type
	)

private

Construct a new function symbol of type fun_type.

Parameters

fun_name	the base name for the new symbol
fun_type	type for the new symbol

Returns: the new symbol

Definition at line 541 of file recursive_initialization.cpp.

◆ get_fresh_global_name()

irep_idt recursive_initializationt::get_fresh_global_name	(	const std::string &	symbol_name,
		const exprt &	initial_value
	)		const

private

Construct a new global symbol of type int and set it's value to initial_value.

Parameters

symbol_name	the base name for the new symbol
initial_value	the value the symbol should be initialised with

Returns: unique name assigned to the new symbol (may differ from symbol_name)

Definition at line 485 of file recursive_initialization.cpp.

◆ get_fresh_global_symexpr()

symbol_exprt recursive_initializationt::get_fresh_global_symexpr ( const std::string & symbol_name ) const

private

Construct a new global symbol of type int initialised to 0.

Parameters

symbol_name the base name for the new symbol

Returns: the symbol expression associated with the new symbol

Definition at line 498 of file recursive_initialization.cpp.

◆ get_fresh_local_symexpr()

symbol_exprt recursive_initializationt::get_fresh_local_symexpr ( const std::string & symbol_name ) const

private

Construct a new local symbol of type int initialised to 0.

Parameters

symbol_name the base name for the new symbol

Returns: the symbol expression associated with the new symbol

Definition at line 510 of file recursive_initialization.cpp.

◆ get_fresh_local_typed_symexpr()

symbol_exprt recursive_initializationt::get_fresh_local_typed_symexpr	(	const std::string &	symbol_name,
		const typet &	type
	)		const

private

Construct a new local symbol of type type initialised to init_value.

Parameters

symbol_name	the base name for the new symbol
type	type for the new symbol

Returns: the symbol expression associated with the new symbol

Definition at line 525 of file recursive_initialization.cpp.

◆ get_fresh_param_symbol()

symbolt & recursive_initializationt::get_fresh_param_symbol	(	const std::string &	param_name,
		const typet &	param_type
	)

private

Construct a new parameter symbol of type param_type.

Parameters

param_name	the base name for the new parameter
param_type	type for the new symbol

Returns: the new symbol

Definition at line 562 of file recursive_initialization.cpp.

◆ get_symbol_expr()

symbol_exprt recursive_initializationt::get_symbol_expr ( const irep_idt & symbol_name ) const

private

Recover the symbol expression from symbol table.

Parameters

symbol_name the name of the symbol to get

Returns: symbol expression of the symbol with given name

Definition at line 581 of file recursive_initialization.cpp.

◆ initialize()

void recursive_initializationt::initialize	(	const exprt &	lhs,
		const exprt &	depth,
		code_blockt &	body
	)

Generate initialisation code for lhs into body.

Parameters

lhs	The expression to initialise.
depth	The number of pointer follows. Starts at 0.
body	The code block to write initialisation code to.

Definition at line 138 of file recursive_initialization.cpp.

◆ initialize_selected_member()

void recursive_initializationt::initialize_selected_member	(	const exprt &	lhs,
		const exprt &	depth,
		code_blockt &	body,
		const std::vector< irep_idt > &	selection_spec
	)

private

Select the specified struct-member to be non-deterministically initialized.

Parameters

lhs	symbol expression of the top structure
depth	only to be passed
body	code block for the initializing assignment
selection_spec	the user specification of the particular member to havoc

Definition at line 1049 of file recursive_initialization.cpp.

◆ is_array_size_parameter()

bool recursive_initializationt::is_array_size_parameter ( const irep_idt & cmdline_arg ) const

private

Definition at line 395 of file recursive_initialization.cpp.

◆ is_initialization_allowed()

static bool recursive_initializationt::is_initialization_allowed ( const symbolt & symbol )

inlinestatic

Definition at line 101 of file recursive_initialization.h.

◆ needs_freeing()

bool recursive_initializationt::needs_freeing ( const exprt & expr ) const

Definition at line 899 of file recursive_initialization.cpp.

◆ should_be_treated_as_array()

bool recursive_initializationt::should_be_treated_as_array ( const irep_idt & pointer_name ) const

private

Definition at line 375 of file recursive_initialization.cpp.

◆ should_be_treated_as_cstring()

bool recursive_initializationt::should_be_treated_as_cstring ( const irep_idt & pointer_name ) const

private

Definition at line 411 of file recursive_initialization.cpp.

◆ type2id()

std::string recursive_initializationt::type2id ( const typet & type ) const

private

Simple pretty-printer for typet.

Produces strings that can decorate variable names in C.

Parameters

type	type to be pretty-printed

Returns: a string without white characters, quotes, etc.

Definition at line 588 of file recursive_initialization.cpp.

Member Data Documentation

◆ common_arguments_origins

std::vector<std::optional<exprt> > recursive_initializationt::common_arguments_origins

private

Definition at line 121 of file recursive_initialization.h.

◆ goto_model

goto_modelt& recursive_initializationt::goto_model

private

Definition at line 117 of file recursive_initialization.h.

◆ initialization_config

const recursive_initialization_configt recursive_initializationt::initialization_config

private

Definition at line 116 of file recursive_initialization.h.

◆ max_depth_var_name

irep_idt recursive_initializationt::max_depth_var_name

private

Definition at line 118 of file recursive_initialization.h.

◆ min_depth_var_name

irep_idt recursive_initializationt::min_depth_var_name

private

Definition at line 119 of file recursive_initialization.h.

◆ type_constructor_names

type_constructor_namest recursive_initializationt::type_constructor_names

private

Definition at line 120 of file recursive_initialization.h.

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

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

Classes

Public Types

Public Member Functions

Static Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ equal_cluster_idt

◆ recursion_sett

◆ type_constructor_namest

Constructor & Destructor Documentation

◆ recursive_initializationt()

Member Function Documentation

◆ build_array_constructor()

◆ build_constructor()

◆ build_constructor_body()

◆ build_dynamic_array_constructor()

◆ build_function_pointer_constructor()

◆ build_nondet_constructor()

◆ build_pointer_constructor()

◆ build_struct_constructor()

◆ deallocate_code()

◆ find_equal_cluster()

◆ free_cluster_origins()

◆ free_if_possible()

◆ get_associated_size_variable()

◆ get_fresh_fun_symbol()

◆ get_fresh_global_name()

◆ get_fresh_global_symexpr()

◆ get_fresh_local_symexpr()

◆ get_fresh_local_typed_symexpr()

◆ get_fresh_param_symbol()

◆ get_symbol_expr()

◆ initialize()

◆ initialize_selected_member()

◆ is_array_size_parameter()

◆ is_initialization_allowed()

◆ needs_freeing()

◆ should_be_treated_as_array()

◆ should_be_treated_as_cstring()

◆ type2id()

Member Data Documentation

◆ common_arguments_origins

◆ goto_model

◆ initialization_config

◆ max_depth_var_name

◆ min_depth_var_name

◆ type_constructor_names