recursive_initializationt Class Reference

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. More...
symbol_exprt	get_free_function ()
	Get the free function as symbol expression, and inserts it into the goto-model if it doesn't exist already. More...
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
symbol_exprt	get_malloc_function ()
	Get the malloc function as symbol exprt, and inserts it into the goto-model if it doesn't exist already. More...
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. More...
symbol_exprt	get_fresh_global_symexpr (const std::string &symbol_name) const
	Construct a new global symbol of type int initialised to 0. More...
symbol_exprt	get_fresh_local_symexpr (const std::string &symbol_name) const
	Construct a new local symbol of type int initialised to 0. More...
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. More...
const symbolt &	get_fresh_fun_symbol (const std::string &fun_name, const typet &fun_type)
	Construct a new function symbol of type fun_type. More...
symbolt &	get_fresh_param_symbol (const std::string &param_name, const typet &param_type)
	Construct a new parameter symbol of type param_type. More...
symbol_exprt	get_symbol_expr (const irep_idt &symbol_name) const
	Recover the symbol expression from symbol table. More...
std::string	type2id (const typet &type) const
	Simple pretty-printer for typet. More...
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. More...
irep_idt	build_constructor (const exprt &expr)
	Check if a constructor for the type of expr already exists and create it if not. More...
code_blockt	build_function_pointer_constructor (const symbol_exprt &result, bool is_nullable)
	Constructor for function pointers. More...
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. More...
code_blockt	build_struct_constructor (const exprt &depth, const symbol_exprt &result)
	Constructor for structures: simply iterates over members and initialise each one. More...
code_blockt	build_nondet_constructor (const symbol_exprt &result) const
	Default constructor: assigns non-deterministic value of the right type. More...
code_blockt	build_array_constructor (const exprt &depth, const symbol_exprt &result)
	Constructor for arrays: simply iterates over elements and initialise each one. More...
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. More...
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. More...

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 747 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 819 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 986 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 807 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 651 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 769 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 401 of file recursive_initialization.cpp.

free_cluster_origins()

void recursive_initializationt::free_cluster_origins

(

code_blockt &

body

)

Definition at line 978 of file recursive_initialization.cpp.

free_if_possible()

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

Definition at line 945 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 421 of file recursive_initialization.cpp.

get_free_function()

symbol_exprt recursive_initializationt::get_free_function

(

)

Get the free function as symbol expression, and inserts it into the goto-model if it doesn't exist already.

Returns

the symbol expression for the free function

Definition at line 633 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 559 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 503 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 516 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 528 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 543 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 580 of file recursive_initialization.cpp.

get_malloc_function()

symbol_exprt recursive_initializationt::get_malloc_function ( )

private

Get the malloc function as symbol exprt, and inserts it into the goto-model if it doesn't exist already.

Definition at line 375 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 599 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 1059 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 413 of file recursive_initialization.cpp.

is_initialization_allowed()

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

inlinestatic

Definition at line 106 of file recursive_initialization.h.

needs_freeing()

bool recursive_initializationt::needs_freeing

(

const exprt &

expr

)

const

Definition at line 926 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 393 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 429 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 606 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 126 of file recursive_initialization.h.

goto_model

goto_modelt& recursive_initializationt::goto_model

private

Definition at line 122 of file recursive_initialization.h.

initialization_config

const recursive_initialization_configt recursive_initializationt::initialization_config

private

Definition at line 121 of file recursive_initialization.h.

max_depth_var_name

irep_idt recursive_initializationt::max_depth_var_name

private

Definition at line 123 of file recursive_initialization.h.

min_depth_var_name

irep_idt recursive_initializationt::min_depth_var_name

private

Definition at line 124 of file recursive_initialization.h.

type_constructor_names

type_constructor_namest recursive_initializationt::type_constructor_names

private

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