The main class for the forward symbolic simulator. More...

#include <goto_symex.h>

Inheritance diagram for goto_symext:

Collaboration diagram for goto_symext:

Public Types
typedef goto_symex_statet	statet
	A type abbreviation for goto_symex_statet. More...

typedef std::function< const goto_functionst::goto_functiont &(const irep_idt &)>	get_goto_functiont
	The type of delegate functions that retrieve a goto_functiont for a particular function identifier. More...

Public Member Functions
	goto_symext (message_handlert &mh, const symbol_table_baset &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage, guard_managert &guard_manager)
	Construct a goto_symext to execute a particular program. More...

virtual	~goto_symext ()=default
	A virtual destructor allowing derived classes to be cleaned up correctly. More...

virtual symbol_tablet	symex_from_entry_point_of (const get_goto_functiont &get_goto_function, const shadow_memory_field_definitionst &fields)
	Symbolically execute the entire program starting from entry point. More...

virtual void	initialize_path_storage_from_entry_point_of (const get_goto_functiont &get_goto_function, symbol_table_baset &new_symbol_table, const shadow_memory_field_definitionst &fields)
	Puts the initial state of the entry point function into the path storage. More...

virtual symbol_tablet	resume_symex_from_saved_state (const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *saved_equation)
	Performs symbolic execution using a state and equation that have already been used to symbolically execute part of the program. More...

virtual symbol_tablet	symex_with_state (statet &state, const get_goto_functiont &get_goto_functions)
	Symbolically execute the entire program starting from entry point. More...

virtual bool	check_break (const irep_idt &loop_id, unsigned unwind)
	Defines condition for interrupting symbolic execution for a specific loop. More...

unsigned	get_total_vccs () const

unsigned	get_remaining_vccs () const

void	validate (const validation_modet vm) const

Static Public Member Functions
static get_goto_functiont	get_goto_function (abstract_goto_modelt &goto_model)
	Return a function to get/load a goto function from the given goto model Create a default delegate to retrieve function bodies from a goto_functionst. More...

Public Attributes
bool	should_pause_symex
	Set when states are pushed onto the workqueue If this flag is set at the end of a symbolic execution run, it means that symbolic execution has been paused because we encountered a GOTO instruction while doing path exploration, and thus pushed the successor states of the GOTO onto path_storage. More...

bool	ignore_assertions = false
	If this flag is set to true then assertions will be temporarily ignored by the symbolic executions. More...

irep_idt	language_mode
	language_mode: ID_java, ID_C or another language identifier if we know the source language in use, irep_idt() otherwise. More...

std::size_t	path_segment_vccs
	Number of VCCs generated during the run of this goto_symext object. More...

Protected Types
typedef symex_targett::assignment_typet	assignment_typet

Protected Member Functions
std::unique_ptr< statet >	initialize_entry_point_state (const get_goto_functiont &get_goto_function)
	Initialize the symbolic execution and the given state with the beginning of the entry point function. More...

void	symex_threaded_step (statet &state, const get_goto_functiont &get_goto_function)
	Invokes symex_step and verifies whether additional threads can be executed. More...

virtual void	symex_step (const get_goto_functiont &get_goto_function, statet &state)
	Called for each step in the symbolic execution This calls print_symex_step to print symex's current instruction if required, then execute_next_instruction to execute the actual instruction body. More...

void	execute_next_instruction (const get_goto_functiont &get_goto_function, statet &state)
	Executes the instruction `state.source.pc` Case-switches over the type of the instruction being executed and calls another function appropriate to the instruction type, for example symex_function_call if the current instruction is a function call, symex_goto if the current instruction is a goto, etc. More...

void	kill_instruction_local_symbols (statet &state)
	Kills any variables in instruction_local_symbols (these are currently always let-bound variables defined in the course of executing the current instruction), then clears instruction_local_symbols. More...

void	print_symex_step (statet &state)
	Prints the route of symex as it walks through the code. More...

messaget::mstreamt &	print_callstack_entry (const symex_targett::sourcet &target)

exprt	clean_expr (exprt expr, statet &state, bool write)
	Clean up an expression. More...

void	trigger_auto_object (const exprt &, statet &)

void	initialize_auto_object (const exprt &, statet &)

void	process_array_expr (statet &, exprt &)
	Given an expression, find the root object and the offset into it. More...

exprt	make_auto_object (const typet &, statet &)

virtual void	dereference (exprt &, statet &, bool write)
	Replace all dereference operations within `expr` with explicit references to the objects they may refer to. More...

symbol_exprt	cache_dereference (exprt &dereference_result, statet &state)

void	dereference_rec (exprt &expr, statet &state, bool write, bool is_in_quantifier)
	If `expr` is a dereference_exprt, replace it with explicit references to the objects it may point to. More...

exprt	address_arithmetic (const exprt &, statet &, bool keep_array)
	Transforms an lvalue expression by replacing any dereference operations it contains with explicit references to the objects they may point to (using goto_symext::dereference_rec), and translates `byte_extract,` `member` and `index` operations into integer offsets from a root symbol (if any). More...

virtual void	symex_goto (statet &state)
	Symbolically execute a GOTO instruction. More...

void	symex_unreachable_goto (statet &state)
	Symbolically execute a GOTO instruction in the context of unreachable code. More...

void	symex_set_return_value (statet &state, const exprt &return_value)
	Symbolically execute a SET_RETURN_VALUE instruction. More...

virtual void	symex_start_thread (statet &state)
	Symbolically execute a START_THREAD instruction. More...

virtual void	symex_atomic_begin (statet &state)
	Symbolically execute an ATOMIC_BEGIN instruction. More...

virtual void	symex_atomic_end (statet &state)
	Symbolically execute an ATOMIC_END instruction. More...

virtual void	symex_decl (statet &state)
	Symbolically execute a DECL instruction. More...

virtual void	symex_decl (statet &state, const symbol_exprt &expr)
	Symbolically execute a DECL instruction for the given symbol or simulate such an execution for a synthetic symbol. More...

virtual void	symex_dead (statet &state)
	Symbolically execute a DEAD instruction. More...

void	symex_dead (statet &state, const symbol_exprt &symbol_expr)
	Kill a symbol, as if it had been the subject of a DEAD instruction. More...

virtual void	symex_other (statet &state)
	Symbolically execute an OTHER instruction. More...

void	symex_assert (const goto_programt::instructiont &, statet &)

void	apply_goto_condition (goto_symex_statet &current_state, goto_statet &jump_taken_state, goto_statet &jump_not_taken_state, const exprt &original_guard, const exprt &new_guard, const namespacet &ns)
	Propagate constants and points-to information implied by a GOTO condition. More...

void	try_filter_value_sets (goto_symex_statet &state, exprt condition, const value_sett &original_value_set, value_sett jump_taken_value_set, value_sett jump_not_taken_value_set, const namespacet &ns)
	Try to filter value sets based on whether possible values of a pointer-typed symbol make the condition true or false. More...

virtual void	vcc (const exprt &cond, const irep_idt &property_id, const std::string &msg, statet &state)
	Symbolically execute a verification condition (assertion). More...

virtual void	symex_assume (statet &state, const exprt &cond)
	Symbolically execute an ASSUME instruction or simulate such an execution for a synthetic assumption. More...

void	symex_assume_l2 (statet &, const exprt &cond)

void	merge_gotos (statet &state)
	Merge all branches joining at the current program point. More...

virtual void	merge_goto (const symex_targett::sourcet &source, goto_statet &&goto_state, statet &state)
	Merge a single branch, the symbolic state of which is held in `goto_state`, into the current overall symbolic state. More...

void	phi_function (const goto_statet &goto_state, statet &dest_state)
	Merge the SSA assignments from goto_state into dest_state. More...

virtual bool	should_stop_unwind (const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind)
	Determine whether to unwind a loop. More...

virtual void	loop_bound_exceeded (statet &state, const exprt &guard)

virtual void	symex_function_call (const get_goto_functiont &get_goto_function, statet &state, const goto_programt::instructiont &instruction)
	Symbolically execute a FUNCTION_CALL instruction. More...

virtual void	locality (const irep_idt &function_identifier, goto_symext::statet &state, const goto_functionst::goto_functiont &goto_function)
	Preserves locality of parameters of a given function by applying L1 renaming to them. More...

virtual void	symex_end_of_function (statet &)
	Symbolically execute a END_FUNCTION instruction. More...

virtual void	symex_function_call_symbol (const get_goto_functiont &get_goto_function, statet &state, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments)
	Symbolic execution of a call to a function call. More...

virtual void	symex_function_call_post_clean (const get_goto_functiont &get_goto_function, statet &state, const exprt &cleaned_lhs, const symbol_exprt &function, const exprt::operandst &cleaned_arguments)
	Symbolic execution of a function call by inlining. More...

virtual bool	get_unwind_recursion (const irep_idt &identifier, unsigned thread_nr, unsigned unwind)

void	parameter_assignments (const irep_idt &function_identifier, const goto_functionst::goto_functiont &goto_function, statet &state, const exprt::operandst &arguments)
	Iterates over `arguments` and assigns them to the parameters, which are symbols whose name and type are deduced from the type of `goto_function`. More...

void	symex_throw (statet &state)
	Symbolically execute a THROW instruction. More...

void	symex_catch (statet &state)
	Symbolically execute a CATCH instruction. More...

virtual void	do_simplify (exprt &expr)

void	symex_assign (statet &state, const exprt &lhs, const exprt &rhs)
	Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment. More...

bool	constant_propagate_assignment_with_side_effects (statet &state, symex_assignt &symex_assign, const exprt &lhs, const exprt &rhs)
	Attempt to constant propagate side effects of the assignment (if any) More...

void	constant_propagate_empty_string (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
	Create an empty string constant. More...

bool	constant_propagate_string_concat (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
	Attempt to constant propagate string concatenation. More...

bool	constant_propagate_string_substring (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
	Attempt to constant propagate getting a substring of a string. More...

bool	constant_propagate_integer_to_string (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
	Attempt to constant propagate converting an integer to a string. More...

bool	constant_propagate_delete_char_at (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
	Attempt to constant propagate deleting a character from a string. More...

bool	constant_propagate_delete (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
	Attempt to constant propagate deleting a substring from a string. More...

bool	constant_propagate_set_length (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
	Attempt to constant propagate setting the length of a string. More...

bool	constant_propagate_set_char_at (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
	Attempt to constant propagate setting the char at the given index. More...

bool	constant_propagate_trim (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
	Attempt to constant propagate trim operations. More...

bool	constant_propagate_case_change (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1, bool to_upper)
	Attempt to constant propagate case changes, both upper and lower. More...

bool	constant_propagate_replace (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)
	Attempt to constant proagate character replacement. More...

void	assign_string_constant (statet &state, symex_assignt &symex_assign, const ssa_exprt &length, const constant_exprt &new_length, const ssa_exprt &char_array, const array_exprt &new_char_array)
	Assign constant string length and string data given by a char array to given ssa variables. More...

const symbolt &	get_new_string_data_symbol (statet &state, symex_assignt &symex_assign, const std::string &aux_symbol_name, const ssa_exprt &char_array, const array_exprt &new_char_array)
	Installs a new symbol in the symbol table to represent the given character array, and assigns the character array to the symbol. More...

void	associate_array_to_pointer (statet &state, symex_assignt &symex_assign, const array_exprt &new_char_array, const address_of_exprt &string_data)
	Generate array to pointer association primitive. More...

std::optional< std::reference_wrapper< const array_exprt > >	try_evaluate_constant_string (const statet &state, const exprt &content)

void	havoc_rec (statet &state, const guardt &guard, const exprt &dest)

void	lift_lets (statet &, exprt &)
	Execute any let expressions in `expr` using symex_assignt::assign_symbol. More...

void	lift_let (statet &state, const let_exprt &let_expr)
	Execute a single let expression, which should not have any nested let expressions (use lift_lets instead if there might be). More...

virtual void	symex_va_start (statet &, const exprt &lhs, const side_effect_exprt &)

virtual void	symex_allocate (statet &state, const exprt &lhs, const side_effect_exprt &code)
	Symbolically execute an assignment instruction that has an `allocate` on the right hand side. More...

virtual void	symex_cpp_delete (statet &state, const codet &code)
	Symbolically execute an OTHER instruction that does a CPP `delete` More...

virtual void	symex_cpp_new (statet &state, const exprt &lhs, const side_effect_exprt &code)
	Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes. More...

virtual void	symex_printf (statet &state, const exprt &rhs)
	Symbolically execute an OTHER instruction that does a CPP `printf` More...

virtual void	symex_input (statet &state, const codet &code)
	Symbolically execute an OTHER instruction that does a CPP input. More...

virtual void	symex_output (statet &state, const codet &code)
	Symbolically execute an OTHER instruction that does a CPP output. More...

void	rewrite_quantifiers (exprt &, statet &)

Static Protected Member Functions
static std::optional< std::reference_wrapper< const constant_exprt > >	try_evaluate_constant (const statet &state, const exprt &expr)

Protected Attributes
const symex_configt	symex_config
	The configuration to use for this symbolic execution. More...

const symbol_table_baset &	outer_symbol_table
	The symbol table associated with the goto-program being executed. More...

namespacet	ns
	Initialized just before symbolic execution begins, to point to both `outer_symbol_table` and the symbol table owned by the `goto_symex_statet` object used during symbolic execution. More...

guard_managert &	guard_manager
	Used to create guards. More...

symex_target_equationt &	target
	The equation that this execution is building up. More...

unsigned	atomic_section_counter
	A monotonically increasing index for each encountered ATOMIC_BEGIN instruction. More...

std::vector< symbol_exprt >	instruction_local_symbols
	Variables that should be killed at the end of the current symex_step invocation. More...

messaget	log
	The messaget to write log messages to. More...

path_storaget &	path_storage
	Symbolic execution paths to be resumed later. More...

complexity_limitert	complexity_module

shadow_memoryt	shadow_memory
	Shadow memory instrumentation API. More...

Statistics
The actual number of total and remaining VCCs should be assigned to the relevant members of goto_symex_statet. The members below are used to cache the values from goto_symex_statet after symbolic execution has ended, so that the user of \ref goto_symext can read those values even after the state has been deallocated.
unsigned	_total_vccs

unsigned	_remaining_vccs

Friends
class	symex_dereference_statet

Detailed Description

The main class for the forward symbolic simulator.

Remarks: Higher-level architectural information on symbolic execution is documented in the Symbolic execution module page.

Definition at line 36 of file goto_symex.h.

Member Typedef Documentation

◆ assignment_typet

typedef symex_targett::assignment_typet goto_symext::assignment_typet

protected

Definition at line 752 of file goto_symex.h.

◆ get_goto_functiont

typedef std::function<const goto_functionst::goto_functiont &(const irep_idt &)> goto_symext::get_goto_functiont

The type of delegate functions that retrieve a goto_functiont for a particular function identifier.

Remarks: This allows goto_symext to be divorced from the particular type of goto_modelt that provides the function bodies

Definition at line 93 of file goto_symex.h.

◆ statet

typedef goto_symex_statet goto_symext::statet

A type abbreviation for goto_symex_statet.

Definition at line 40 of file goto_symex.h.

Constructor & Destructor Documentation

◆ goto_symext()

goto_symext::goto_symext	(	message_handlert &	mh,
		const symbol_table_baset &	outer_symbol_table,
		symex_target_equationt &	_target,
		const optionst &	options,
		path_storaget &	path_storage,
		guard_managert &	guard_manager
	)

inline

Construct a goto_symext to execute a particular program.

Parameters

mh	The message handler to use for log messages
outer_symbol_table	The symbol table for the program to be executed, excluding any symbols added during the symbolic execution
_target	Where to store the equation built up by this execution
options	The options to use to configure this execution
path_storage	Place to storage symbolic execution paths that have been halted and can be resumed later
guard_manager	Manager for creating guards

Definition at line 51 of file goto_symex.h.

◆ ~goto_symext()

virtual goto_symext::~goto_symext ( )

virtualdefault

A virtual destructor allowing derived classes to be cleaned up correctly.

Member Function Documentation

◆ address_arithmetic()

exprt goto_symext::address_arithmetic	(	const exprt &	expr,
		statet &	state,
		bool	keep_array
	)

protected

Transforms an lvalue expression by replacing any dereference operations it contains with explicit references to the objects they may point to (using goto_symext::dereference_rec), and translates byte_extract, member and index operations into integer offsets from a root symbol (if any).

These are ultimately expressed in the form (target_type*)((char*)(&underlying_symbol) + offset).

Parameters

expr	expression to replace with normalised, dereference-free form
state	working state. See goto_symext::dereference for possible side-effects of a dereference operation.
keep_array	if true and an underlying object is an array, return its address (`&array`); otherwise return the address of its first element (`&array[0]).

Returns: the transformed lvalue expression

Definition at line 43 of file symex_dereference.cpp.

◆ apply_goto_condition()

void goto_symext::apply_goto_condition	(	goto_symex_statet &	current_state,
		goto_statet &	jump_taken_state,
		goto_statet &	jump_not_taken_state,
		const exprt &	original_guard,
		const exprt &	new_guard,
		const namespacet &	ns
	)

protected

Propagate constants and points-to information implied by a GOTO condition.

See goto_statet::apply_condition for aspects of this which are common to GOTO and ASSUME instructions.

Parameters

current_state	state prior to the GOTO instruction
jump_taken_state	state following taking the GOTO
jump_not_taken_state	fall-through state
original_guard	the original GOTO condition
new_guard	GOTO condition, L2 renamed and simplified
ns	global namespace

Definition at line 30 of file symex_goto.cpp.

◆ assign_string_constant()

void goto_symext::assign_string_constant	(	statet &	state,
		symex_assignt &	symex_assign,
		const ssa_exprt &	length,
		const constant_exprt &	new_length,
		const ssa_exprt &	char_array,
		const array_exprt &	new_char_array
	)

protected

Assign constant string length and string data given by a char array to given ssa variables.

A new symbol is created (if not yet existing) in the symbol table to hold the string data given by new_char_array. The name of the symbol is derived from the contents of new_char_array (e.g., if the array contains "abc", the symbol will be named "abc_constant_char_array"). Then, the expression &sym[0] is assigned to char_array (assuming sym denotes the symbol holding the string data given by new_char_array. The assignment is preceeded by an assume statement ensuring length before this call was zero, this is to avoid leaving the previous array unconstrained.

Parameters

state	goto symex state
symex_assign	object handling symbol assignments
length	ssa variable to assign the constant string length to
new_length	value to assign to `length`
char_array	ssa variable to assign the constant string data to
new_char_array	constant char array which gives the string data to assign to `char_array`

Definition at line 258 of file goto_symex.cpp.

◆ associate_array_to_pointer()

void goto_symext::associate_array_to_pointer	(	statet &	state,
		symex_assignt &	symex_assign,
		const array_exprt &	new_char_array,
		const address_of_exprt &	string_data
	)

protected

Generate array to pointer association primitive.

Executes an assignment return_value = f(new_char_array, string_data), with new_char_array being the character array to associate with pointer string_data

Parameters

state	goto symex state
symex_assign	object handling symbol assignments
new_char_array	character array to associate with pointer
string_data	pointer to associate with character array

Definition at line 338 of file goto_symex.cpp.

◆ cache_dereference()

symbol_exprt goto_symext::cache_dereference	(	exprt &	dereference_result,
		statet &	state
	)

protected

Definition at line 197 of file symex_dereference.cpp.

◆ check_break()

bool goto_symext::check_break	(	const irep_idt &	loop_id,
		unsigned	unwind
	)

virtual

Defines condition for interrupting symbolic execution for a specific loop.

False constant by default, over-ridden by incremental BMC implementation to allow breaking if the unwinding the user specified loop

Parameters

loop_id	the loop identifier
unwind	current unwinding counter

Returns: true if the symbolic execution is to be interrupted for checking

Reimplemented in symex_bmc_incremental_one_loopt.

Definition at line 617 of file symex_goto.cpp.

◆ clean_expr()

exprt goto_symext::clean_expr	(	exprt	expr,
		statet &	state,
		bool	write
	)

protected

Clean up an expression.

Remarks: this does the following: a) rename non-det choices b) remove pointer dereferencing c) clean up byte_extract on the lhs of an assignment

Parameters

expr	The expression to clean up
state
write

Definition at line 236 of file symex_clean_expr.cpp.

◆ constant_propagate_assignment_with_side_effects()

bool goto_symext::constant_propagate_assignment_with_side_effects	(	statet &	state,
		symex_assignt &	symex_assign,
		const exprt &	lhs,
		const exprt &	rhs
	)

protected

Attempt to constant propagate side effects of the assignment (if any)

Parameters

state	goto symex state
symex_assign	object handling symbol assignments
lhs	lhs of the assignment
rhs	rhs of the assignment

Returns: true if the operation could be evaluated to a constant string, false otherwise

Definition at line 184 of file goto_symex.cpp.

◆ constant_propagate_case_change()

bool goto_symext::constant_propagate_case_change	(	statet &	state,
		symex_assignt &	symex_assign,
		const function_application_exprt &	f_l1,
		bool	to_upper
	)

protected

Attempt to constant propagate case changes, both upper and lower.

Definition at line 970 of file goto_symex.cpp.

◆ constant_propagate_delete()

bool goto_symext::constant_propagate_delete	(	statet &	state,
		symex_assignt &	symex_assign,
		const function_application_exprt &	f_l1
	)

protected

Attempt to constant propagate deleting a substring from a string.

Parameters

state	goto symex state
symex_assign	object handling symbol assignments
f_l1	application of function ID_cprover_string_delete_func with l1 renaming applied

Returns: true if the operation could be evaluated to a constant string, false otherwise

Definition at line 725 of file goto_symex.cpp.

◆ constant_propagate_delete_char_at()

bool goto_symext::constant_propagate_delete_char_at	(	statet &	state,
		symex_assignt &	symex_assign,
		const function_application_exprt &	f_l1
	)

protected

Attempt to constant propagate deleting a character from a string.

Parameters

state	goto symex state
symex_assign	object handling symbol assignments
f_l1	application of function ID_cprover_string_delete_char_at_func with l1 renaming applied

Returns: true if the operation could be evaluated to a constant string, false otherwise

Definition at line 652 of file goto_symex.cpp.

◆ constant_propagate_empty_string()

void goto_symext::constant_propagate_empty_string	(	statet &	state,
		symex_assignt &	symex_assign,
		const function_application_exprt &	f_l1
	)

protected

Create an empty string constant.

Parameters

state	goto symex state
symex_assign	object handling symbol assignments
f_l1	application of function ID_cprover_string_empty_string_func with l1 renaming applied

Definition at line 408 of file goto_symex.cpp.

◆ constant_propagate_integer_to_string()

bool goto_symext::constant_propagate_integer_to_string	(	statet &	state,
		symex_assignt &	symex_assign,
		const function_application_exprt &	f_l1
	)

protected

Attempt to constant propagate converting an integer to a string.

Parameters

state	goto symex state
symex_assign	object handling symbol assignments
f_l1	application of function with ID ID_cprover_string_of_int_func or ID_cprover_string_of_long_func with l1 renaming applied

Returns: true if the operation could be evaluated to a constant string, false otherwise

Definition at line 573 of file goto_symex.cpp.

◆ constant_propagate_replace()

bool goto_symext::constant_propagate_replace	(	statet &	state,
		symex_assignt &	symex_assign,
		const function_application_exprt &	f_l1
	)

protected

Attempt to constant proagate character replacement.

Definition at line 1032 of file goto_symex.cpp.

◆ constant_propagate_set_char_at()

bool goto_symext::constant_propagate_set_char_at	(	statet &	state,
		symex_assignt &	symex_assign,
		const function_application_exprt &	f_l1
	)

protected

Attempt to constant propagate setting the char at the given index.

Parameters

state	goto symex state
symex_assign	object handling symbol assignments
f_l1	application of function ID_cprover_string_char_set_func with l1 renaming applied

Returns: true if the operation could be evaluated to a constant string, false otherwise

Definition at line 900 of file goto_symex.cpp.

◆ constant_propagate_set_length()

bool goto_symext::constant_propagate_set_length	(	statet &	state,
		symex_assignt &	symex_assign,
		const function_application_exprt &	f_l1
	)

protected

Attempt to constant propagate setting the length of a string.

If the new length is less than the current length, characters are stripped from the end to match the new length. If the new length is greater than the current length, null characters '\u0000' are appended to match the new length.

Parameters

state	goto symex state
symex_assign	object handling symbol assignments
f_l1	application of function ID_cprover_string_set_length_func with l1 renaming applied

Returns: true if the operation could be evaluated to a constant string, false otherwise

Definition at line 819 of file goto_symex.cpp.

◆ constant_propagate_string_concat()

bool goto_symext::constant_propagate_string_concat	(	statet &	state,
		symex_assignt &	symex_assign,
		const function_application_exprt &	f_l1
	)

protected

Attempt to constant propagate string concatenation.

Parameters

state	goto symex state
symex_assign	object handling symbol assignments
f_l1	application of function ID_cprover_string_concat_func with l1 renaming applied

Returns: true if the operation could be evaluated to a constant string, false otherwise

Definition at line 436 of file goto_symex.cpp.

◆ constant_propagate_string_substring()

bool goto_symext::constant_propagate_string_substring	(	statet &	state,
		symex_assignt &	symex_assign,
		const function_application_exprt &	f_l1
	)

protected

Attempt to constant propagate getting a substring of a string.

Parameters

state	goto symex state
symex_assign	object handling symbol assignments
f_l1	application of function ID_cprover_string_substring_func with l1 renaming applied

Returns: true if the operation could be evaluated to a constant string, false otherwise

Definition at line 486 of file goto_symex.cpp.

◆ constant_propagate_trim()

bool goto_symext::constant_propagate_trim	(	statet &	state,
		symex_assignt &	symex_assign,
		const function_application_exprt &	f_l1
	)

protected

Attempt to constant propagate trim operations.

Definition at line 1140 of file goto_symex.cpp.

◆ dereference()

void goto_symext::dereference	(	exprt &	expr,
		statet &	state,
		bool	write
	)

protectedvirtual

Replace all dereference operations within expr with explicit references to the objects they may refer to.

For example, the expression *p1 + *p2 might be rewritten to obj1 + (p2 == &obj2 ? obj2 : obj3) in the case where p1 is known to point to obj1 and p2 points to either obj2 or obj3. The expression, and any object references introduced, are renamed to L1 in the process (so in fact we would get obj1!0@3 + (p2!0@1 == .... rather than the exact example given above).

It may have two kinds of side-effect:

When an expression may (or must) point to something which cannot legally be dereferenced, such as a null pointer or an integer cast to a pointer, a "failed object" is created instead, via one of two routes:

a. if the add_failed_symbols pass has been run then a pointer-typed symbol x will have a corresponding failed symbol x$object. This is replicated according to L1 renaming on demand, so for example on the first failed dereference of x!5@10 we will create x$object!5@10 and add that to the symbol table. This addition is made by symex_dereference_statet::get_or_create_failed_symbol

b. if such a failed symbol can't be found then symex will create one of its own, called symex::failed_symbol with some suffix. This is done by value_set_dereferencet::dereference

In either case any newly-created symbol is added to state's symbol table and expr is altered to refer to it. Typically when expr has some legal targets as well this results in an expression like ptr == &real_obj ? real_obj : ptr$object.
Any object whose base-name ends with auto_object is automatically initialised when dereferenced for the first time, creating a tree of pointers leading to fresh objects each time such a pointer is dereferenced. If new objects are created by this mechanism then state will be altered (by symex_assign) to initialise them. See auto_objects.cpp for details.

Definition at line 484 of file symex_dereference.cpp.

◆ dereference_rec()

void goto_symext::dereference_rec	(	exprt &	expr,
		statet &	state,
		bool	write,
		bool	is_in_binding_expression
	)

protected

If expr is a dereference_exprt, replace it with explicit references to the objects it may point to.

Otherwise recursively apply this function to expr's operands, with special cases for address-of (handled by goto_symext::address_arithmetic) and certain common expression patterns such as &struct.flexible_array[0] (see inline comments in code). Note that write is used to alter behaviour when this function is operating on the LHS of an assignment. Similarly is_in_binding_expression indicates when the dereference is inside a binding expression (related to scoping when dereference caching is enabled). For full details of this method's pointer replacement and potential side- effects see goto_symext::dereference

Definition at line 262 of file symex_dereference.cpp.

◆ do_simplify()

void goto_symext::do_simplify ( exprt & expr )

protectedvirtual

Definition at line 32 of file goto_symex.cpp.

◆ execute_next_instruction()

void goto_symext::execute_next_instruction	(	const get_goto_functiont &	get_goto_function,
		statet &	state
	)

protected

Executes the instruction state.source.pc Case-switches over the type of the instruction being executed and calls another function appropriate to the instruction type, for example symex_function_call if the current instruction is a function call, symex_goto if the current instruction is a goto, etc.

Parameters

get_goto_function	The delegate to retrieve function bodies (see get_goto_functiont)
state	Symbolic execution state for current instruction

Definition at line 601 of file symex_main.cpp.

◆ get_goto_function()

goto_symext::get_goto_functiont goto_symext::get_goto_function ( abstract_goto_modelt & goto_model )

static

Return a function to get/load a goto function from the given goto model Create a default delegate to retrieve function bodies from a goto_functionst.

Parameters

goto_model The goto model holding the function map from which to retrieve function bodies

Returns: A delegate to retrieve function bodies from the given goto_functionst

Definition at line 492 of file symex_main.cpp.

◆ get_new_string_data_symbol()

const symbolt & goto_symext::get_new_string_data_symbol	(	statet &	state,
		symex_assignt &	symex_assign,
		const std::string &	aux_symbol_name,
		const ssa_exprt &	char_array,
		const array_exprt &	new_char_array
	)

protected

Installs a new symbol in the symbol table to represent the given character array, and assigns the character array to the symbol.

Parameters

state	goto symex state
symex_assign	object handling symbol assignments
aux_symbol_name	name of the symbol to create
char_array	ssa variable to which to assign a pointer to the symbol
new_char_array	new character array to assign to the symbol

Definition at line 302 of file goto_symex.cpp.

◆ get_remaining_vccs()

unsigned goto_symext::get_remaining_vccs ( ) const

inline

Definition at line 851 of file goto_symex.h.

◆ get_total_vccs()

unsigned goto_symext::get_total_vccs ( ) const

inline

Definition at line 842 of file goto_symex.h.

◆ get_unwind_recursion()

bool goto_symext::get_unwind_recursion	(	const irep_idt &	identifier,
		unsigned	thread_nr,
		unsigned	unwind
	)

protectedvirtual

Reimplemented in symex_bmct.

Definition at line 27 of file symex_function_call.cpp.

◆ havoc_rec()

void goto_symext::havoc_rec	(	statet &	state,
		const guardt &	guard,
		const exprt &	dest
	)

protected

Definition at line 20 of file symex_other.cpp.

◆ initialize_auto_object()

void goto_symext::initialize_auto_object	(	const exprt &	expr,
		statet &	state
	)

protected

Definition at line 35 of file auto_objects.cpp.

◆ initialize_entry_point_state()

std::unique_ptr< goto_symext::statet > goto_symext::initialize_entry_point_state ( const get_goto_functiont & get_goto_function )

protected

Initialize the symbolic execution and the given state with the beginning of the entry point function.

Parameters

get_goto_function producer for GOTO functions

Returns: Initialized symex state.

Definition at line 397 of file symex_main.cpp.

◆ initialize_path_storage_from_entry_point_of()

void goto_symext::initialize_path_storage_from_entry_point_of	(	const get_goto_functiont &	get_goto_function,
		symbol_table_baset &	new_symbol_table,
		const shadow_memory_field_definitionst &	fields
	)

virtual

Puts the initial state of the entry point function into the path storage.

Parameters

get_goto_function	The delegate to retrieve function bodies (see get_goto_functiont)
new_symbol_table	A symbol table to store the symbols added during symbolic execution
fields	The shadow memory field declarations

Definition at line 475 of file symex_main.cpp.

◆ kill_instruction_local_symbols()

void goto_symext::kill_instruction_local_symbols ( statet & state )

protected

Kills any variables in instruction_local_symbols (these are currently always let-bound variables defined in the course of executing the current instruction), then clears instruction_local_symbols.

Definition at line 744 of file symex_main.cpp.

◆ lift_let()

void goto_symext::lift_let	(	statet &	state,
		const let_exprt &	let_expr
	)

protected

Execute a single let expression, which should not have any nested let expressions (use lift_lets instead if there might be).

Records the newly-defined variable in instruction_local_symbols, meaning it will be killed when symex_step concludes.

Definition at line 183 of file symex_clean_expr.cpp.

◆ lift_lets()

void goto_symext::lift_lets	(	statet &	state,
		exprt &	rhs
	)

protected

Execute any let expressions in expr using symex_assignt::assign_symbol.

The assignments will be made in bottom-up topological but otherwise arbitrary order (i.e. in (let x = let y = 0 in x + y) + (let z = 0 in z) we will defineybeforex, butzandx` could come in either order)

Definition at line 207 of file symex_clean_expr.cpp.

◆ locality()

void goto_symext::locality	(	const irep_idt &	function_identifier,
		goto_symext::statet &	state,
		const goto_functionst::goto_functiont &	goto_function
	)

protectedvirtual

Preserves locality of parameters of a given function by applying L1 renaming to them.

Parameters

function_identifier	The parameter identifier
state	The current state
goto_function	The goto function

Definition at line 462 of file symex_function_call.cpp.

◆ loop_bound_exceeded()

void goto_symext::loop_bound_exceeded	(	statet &	state,
		const exprt &	guard
	)

protectedvirtual

Definition at line 926 of file symex_goto.cpp.

◆ make_auto_object()

exprt goto_symext::make_auto_object	(	const typet &	type,
		statet &	state
	)

protected

Definition at line 19 of file auto_objects.cpp.

◆ merge_goto()

void goto_symext::merge_goto	(	const symex_targett::sourcet &	source,
		goto_statet &&	goto_state,
		statet &	state
	)

protectedvirtual

Merge a single branch, the symbolic state of which is held in goto_state, into the current overall symbolic state.

goto_state is no longer expected to be valid afterwards.

Parameters

source	source associated with the incoming `goto_state`
goto_state	A state to be merged into this location
state	Symbolic execution state to be updated

Reimplemented in symex_bmct.

Definition at line 678 of file symex_goto.cpp.

◆ merge_gotos()

void goto_symext::merge_gotos ( statet & state )

protected

Merge all branches joining at the current program point.

Applies merge_goto for each goto state (each of which corresponds to previous branch).

Parameters

state Symbolic execution state to be updated

Definition at line 623 of file symex_goto.cpp.

◆ parameter_assignments()

void goto_symext::parameter_assignments	(	const irep_idt &	function_identifier,
		const goto_functionst::goto_functiont &	goto_function,
		statet &	state,
		const exprt::operandst &	arguments
	)

protected

Iterates over arguments and assigns them to the parameters, which are symbols whose name and type are deduced from the type of goto_function.

Parameters

	function_identifier	name of the function
	goto_function	function whose parameters we want to assign
[out]	state	state of the goto program
	arguments	arguments that are passed to the function

Definition at line 32 of file symex_function_call.cpp.

◆ phi_function()

void goto_symext::phi_function	(	const goto_statet &	goto_state,
		statet &	dest_state
	)

protected

Merge the SSA assignments from goto_state into dest_state.

Parameters

goto_state	A state to be merged into this location
dest_state	Symbolic execution state to be updated

Definition at line 859 of file symex_goto.cpp.

◆ print_callstack_entry()

messaget::mstreamt & goto_symext::print_callstack_entry ( const symex_targett::sourcet & target )

protected

Definition at line 501 of file symex_main.cpp.

◆ print_symex_step()

void goto_symext::print_symex_step ( statet & state )

protected

Prints the route of symex as it walks through the code.

Used for debugging.

Definition at line 509 of file symex_main.cpp.

◆ process_array_expr()

void goto_symext::process_array_expr	(	statet &	state,
		exprt &	expr
	)

protected

Given an expression, find the root object and the offset into it.

The extra complication to be considered here is that the expression may have any number of ternary expressions mixed with type casts.

Definition at line 129 of file symex_clean_expr.cpp.

◆ resume_symex_from_saved_state()

symbol_tablet goto_symext::resume_symex_from_saved_state	(	const get_goto_functiont &	get_goto_function,
		const statet &	saved_state,
		symex_target_equationt *	saved_equation
	)

virtual

Performs symbolic execution using a state and equation that have already been used to symbolically execute part of the program.

The state is not re-initialized; instead, symbolic execution resumes from the program counter of the saved state.

Parameters

get_goto_function	The delegate to retrieve function bodies (see get_goto_functiont)
saved_state	The symbolic execution state to resume from
saved_equation	The equation as previously built up

Returns: A symbol table holding the symbols added during symbolic execution.

Definition at line 379 of file symex_main.cpp.

◆ rewrite_quantifiers()

void goto_symext::rewrite_quantifiers	(	exprt &	expr,
		statet &	state
	)

protected

Definition at line 251 of file symex_main.cpp.

◆ should_stop_unwind()

bool goto_symext::should_stop_unwind	(	const symex_targett::sourcet &	source,
		const call_stackt &	context,
		unsigned	unwind
	)

protectedvirtual

Determine whether to unwind a loop.

Parameters

source
context
unwind

Returns: true indicates abort, with false we continue

Reimplemented in symex_bmc_incremental_one_loopt, and symex_bmct.

Definition at line 954 of file symex_goto.cpp.

◆ symex_allocate()

void goto_symext::symex_allocate	(	statet &	state,
		const exprt &	lhs,
		const side_effect_exprt &	code
	)

protectedvirtual

Symbolically execute an assignment instruction that has an allocate on the right hand side.

Parameters

state	Symbolic execution state for current instruction
lhs	The expression to assign to
code	The `allocate` expression

Definition at line 49 of file symex_builtin_functions.cpp.

◆ symex_assert()

void goto_symext::symex_assert	(	const goto_programt::instructiont &	instruction,
		statet &	state
	)

protected

Definition at line 151 of file symex_main.cpp.

◆ symex_assign()

void goto_symext::symex_assign	(	statet &	state,
		const exprt &	lhs,
		const exprt &	rhs
	)

protected

Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.

Parameters

state	Symbolic execution state for current instruction
lhs	The lhs of the assignment to execute
rhs	The rhs of the assignment to execute

Definition at line 38 of file goto_symex.cpp.

◆ symex_assume()

void goto_symext::symex_assume	(	statet &	state,
		const exprt &	cond
	)

protectedvirtual

Symbolically execute an ASSUME instruction or simulate such an execution for a synthetic assumption.

Parameters

state	Symbolic execution state for current instruction
cond	The guard of the assumption

Definition at line 199 of file symex_main.cpp.

◆ symex_assume_l2()

void goto_symext::symex_assume_l2	(	statet &	state,
		const exprt &	cond
	)

protected

Definition at line 219 of file symex_main.cpp.

◆ symex_atomic_begin()

void goto_symext::symex_atomic_begin ( statet & state )

protectedvirtual

Symbolically execute an ATOMIC_BEGIN instruction.

Parameters

state Symbolic execution state for current instruction

Definition at line 16 of file symex_atomic_section.cpp.

◆ symex_atomic_end()

void goto_symext::symex_atomic_end ( statet & state )

protectedvirtual

Symbolically execute an ATOMIC_END instruction.

Parameters

state Symbolic execution state for current instruction

Definition at line 36 of file symex_atomic_section.cpp.

◆ symex_catch()

void goto_symext::symex_catch ( statet & state )

protected

Symbolically execute a CATCH instruction.

Parameters

state Symbolic execution state for current instruction

Definition at line 14 of file symex_catch.cpp.

◆ symex_cpp_delete()

void goto_symext::symex_cpp_delete	(	statet &	state,
		const codet &	code
	)

protectedvirtual

Symbolically execute an OTHER instruction that does a CPP delete

Parameters

state	Symbolic execution state for current instruction
code	The cleaned up CPP `delete` instruction

Definition at line 534 of file symex_builtin_functions.cpp.

◆ symex_cpp_new()

void goto_symext::symex_cpp_new	(	statet &	state,
		const exprt &	lhs,
		const side_effect_exprt &	code
	)

protectedvirtual

Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes.

Parameters

state	Symex state
lhs	left-hand side of assignment
code	right-hand side containing side effect

Definition at line 472 of file symex_builtin_functions.cpp.

◆ symex_dead() [1/2]

void goto_symext::symex_dead ( statet & state )

protectedvirtual

Symbolically execute a DEAD instruction.

Parameters

state Symbolic execution state for current instruction

Definition at line 16 of file symex_dead.cpp.

◆ symex_dead() [2/2]

void goto_symext::symex_dead	(	statet &	state,
		const symbol_exprt &	symbol_expr
	)

protected

Kill a symbol, as if it had been the subject of a DEAD instruction.

Parameters

state	Symbolic execution state
symbol_expr	Symbol to kill

Definition at line 63 of file symex_dead.cpp.

◆ symex_decl() [1/2]

void goto_symext::symex_decl ( statet & state )

protectedvirtual

Symbolically execute a DECL instruction.

Parameters

state Symbolic execution state for current instruction

Definition at line 18 of file symex_decl.cpp.

◆ symex_decl() [2/2]

void goto_symext::symex_decl	(	statet &	state,
		const symbol_exprt &	expr
	)

protectedvirtual

Symbolically execute a DECL instruction for the given symbol or simulate such an execution for a synthetic symbol.

Parameters

state	Symbolic execution state for current instruction
expr	The symbol being declared

Definition at line 24 of file symex_decl.cpp.

◆ symex_end_of_function()

void goto_symext::symex_end_of_function ( statet & state )

protectedvirtual

Symbolically execute a END_FUNCTION instruction.

do function call by inlining

Parameters

state Symbolic execution state for current instruction

Definition at line 431 of file symex_function_call.cpp.

◆ symex_from_entry_point_of()

symbol_tablet goto_symext::symex_from_entry_point_of	(	const get_goto_functiont &	get_goto_function,
		const shadow_memory_field_definitionst &	fields
	)

virtual

Symbolically execute the entire program starting from entry point.

Remarks: The state that goto_symext maintains uses a lot of memory. This method therefore deallocates the state as soon as symbolic execution has completed. This function is useful to callers that don't care about having the state around afterwards.

Parameters

get_goto_function	The delegate to retrieve function bodies (see get_goto_functiont)
fields	The shadow memory field declarations

Returns: A symbol table holding the symbols added during symbolic execution.

Definition at line 464 of file symex_main.cpp.

◆ symex_function_call()

void goto_symext::symex_function_call	(	const get_goto_functiont &	get_goto_function,
		statet &	state,
		const goto_programt::instructiont &	instruction
	)

protectedvirtual

Symbolically execute a FUNCTION_CALL instruction.

Only functions that are symbols are supported, see goto_symext::symex_function_call_symbol.

Parameters

get_goto_function	The delegate to retrieve function bodies (see get_goto_functiont)
state	Symbolic execution state for current instruction
instruction	The function call instruction

Definition at line 167 of file symex_function_call.cpp.

◆ symex_function_call_post_clean()

void goto_symext::symex_function_call_post_clean	(	const get_goto_functiont &	get_goto_function,
		statet &	state,
		const exprt &	cleaned_lhs,
		const symbol_exprt &	function,
		const exprt::operandst &	cleaned_arguments
	)

protectedvirtual

Symbolic execution of a function call by inlining.

Records the call in target by appending a function call step and:

if the body is available create a new frame, assigns the parameters, and proceed to executing the code of the function.

otherwise assign a nondetministic value to the left-hand-side of the call when there is one

Parameters

get_goto_function	The delegate to retrieve function bodies (see get_goto_functiont)
state	Symbolic execution state for current instruction
cleaned_lhs	nil or the lhs of the function call, cleaned
function	the symbol of the function to call
cleaned_arguments	the arguments of the function call, cleaned

Definition at line 230 of file symex_function_call.cpp.

◆ symex_function_call_symbol()

void goto_symext::symex_function_call_symbol	(	const get_goto_functiont &	get_goto_function,
		statet &	state,
		const exprt &	lhs,
		const symbol_exprt &	function,
		const exprt::operandst &	arguments
	)

protectedvirtual

Symbolic execution of a call to a function call.

Parameters

get_goto_function	The delegate to retrieve function bodies (see get_goto_functiont)
state	Symbolic execution state for current instruction
lhs	nil or the lhs of the function call instruction
function	the symbol of the function to call
arguments	the arguments of the function call

Definition at line 187 of file symex_function_call.cpp.

◆ symex_goto()

void goto_symext::symex_goto ( statet & state )

protectedvirtual

Symbolically execute a GOTO instruction.

Parameters

state Symbolic execution state for current instruction

Definition at line 230 of file symex_goto.cpp.

◆ symex_input()

void goto_symext::symex_input	(	statet &	state,
		const codet &	code
	)

protectedvirtual

Symbolically execute an OTHER instruction that does a CPP input.

Parameters

state	Symbolic execution state for current instruction
code	The cleaned up input instruction

Definition at line 428 of file symex_builtin_functions.cpp.

◆ symex_other()

void goto_symext::symex_other ( statet & state )

protectedvirtual

Symbolically execute an OTHER instruction.

Parameters

state Symbolic execution state for current instruction

Definition at line 79 of file symex_other.cpp.

◆ symex_output()

void goto_symext::symex_output	(	statet &	state,
		const codet &	code
	)

protectedvirtual

Symbolically execute an OTHER instruction that does a CPP output.

Parameters

state	Symbolic execution state for current instruction
code	The cleaned up output instruction

Definition at line 450 of file symex_builtin_functions.cpp.

◆ symex_printf()

void goto_symext::symex_printf	(	statet &	state,
		const exprt &	rhs
	)

protectedvirtual

Symbolically execute an OTHER instruction that does a CPP printf

Parameters

state	Symbolic execution state for current instruction
rhs	The cleaned up CPP `printf` instruction

Definition at line 367 of file symex_builtin_functions.cpp.

◆ symex_set_return_value()

void goto_symext::symex_set_return_value	(	statet &	state,
		const exprt &	return_value
	)

protected

Symbolically execute a SET_RETURN_VALUE instruction.

Parameters

state	Symbolic execution state for current instruction
return_value	The value to be returned

Definition at line 14 of file symex_set_return_value.cpp.

◆ symex_start_thread()

void goto_symext::symex_start_thread ( statet & state )

protectedvirtual

Symbolically execute a START_THREAD instruction.

Parameters

state Symbolic execution state for current instruction

Definition at line 21 of file symex_start_thread.cpp.

◆ symex_step()

void goto_symext::symex_step	(	const get_goto_functiont &	get_goto_function,
		statet &	state
	)

protectedvirtual

Called for each step in the symbolic execution This calls print_symex_step to print symex's current instruction if required, then execute_next_instruction to execute the actual instruction body.

do just one step

Parameters

get_goto_function	The delegate to retrieve function bodies (see get_goto_functiont)
state	Symbolic execution state for current instruction

Reimplemented in symex_bmct.

Definition at line 591 of file symex_main.cpp.

◆ symex_threaded_step()

void goto_symext::symex_threaded_step	(	statet &	state,
		const get_goto_functiont &	get_goto_function
	)

protected

Invokes symex_step and verifies whether additional threads can be executed.

Parameters

state	Symbolic execution state for current instruction
get_goto_function	The delegate to retrieve function bodies (see get_goto_functiont)

Definition at line 299 of file symex_main.cpp.

◆ symex_throw()

void goto_symext::symex_throw ( statet & state )

protected

Symbolically execute a THROW instruction.

Parameters

state Symbolic execution state for current instruction

Definition at line 14 of file symex_throw.cpp.

◆ symex_unreachable_goto()

void goto_symext::symex_unreachable_goto ( statet & state )

protected

Symbolically execute a GOTO instruction in the context of unreachable code.

Parameters

state Symbolic execution state for current instruction

Definition at line 544 of file symex_goto.cpp.

◆ symex_va_start()

void goto_symext::symex_va_start	(	statet &	state,
		const exprt &	lhs,
		const side_effect_exprt &	code
	)

protectedvirtual

Definition at line 247 of file symex_builtin_functions.cpp.

◆ symex_with_state()

symbol_tablet goto_symext::symex_with_state	(	statet &	state,
		const get_goto_functiont &	get_goto_functions
	)

virtual

Symbolically execute the entire program starting from entry point.

This method uses the state argument as the symbolic execution state, which is useful for examining the state after this method returns. The state that goto_symext maintains has a large memory footprint, so if keeping the state around is not necessary, clients should instead call goto_symext::symex_from_entry_point_of().

Parameters

state	The symbolic execution state to use for the execution
get_goto_functions	A functor to retrieve function bodies to execute

Returns: A symbol table holding the symbols added during symbolic execution.

Definition at line 323 of file symex_main.cpp.

◆ trigger_auto_object()

void goto_symext::trigger_auto_object	(	const exprt &	expr,
		statet &	state
	)

protected

Definition at line 76 of file auto_objects.cpp.

◆ try_evaluate_constant()

std::optional< std::reference_wrapper< const constant_exprt > > goto_symext::try_evaluate_constant	(	const statet &	state,
		const exprt &	expr
	)

staticprotected

Definition at line 389 of file goto_symex.cpp.

◆ try_evaluate_constant_string()

std::optional< std::reference_wrapper< const array_exprt > > goto_symext::try_evaluate_constant_string	(	const statet &	state,
		const exprt &	content
	)

protected

Definition at line 368 of file goto_symex.cpp.

◆ try_filter_value_sets()

void goto_symext::try_filter_value_sets	(	goto_symex_statet &	state,
		exprt	condition,
		const value_sett &	original_value_set,
		value_sett *	jump_taken_value_set,
		value_sett *	jump_not_taken_value_set,
		const namespacet &	ns
	)

protected

Try to filter value sets based on whether possible values of a pointer-typed symbol make the condition true or false.

We only do this when there is only one pointer-typed symbol in condition.

Parameters

state	The current state
condition	The condition which is being evaluated, which it expects will not have been cleaned or renamed. In practice, it's fine if it has been cleaned and renamed up to level L1.
original_value_set	The value set we will read from
jump_taken_value_set	The value set that will be used when the condition is true, so we remove any elements which we can tell will make the condition false, or nullptr if this shouldn't be done
jump_not_taken_value_set	The value set that will be used when the condition is false, so we remove any elements which we can tell will make the condition true, or nullptr if this shouldn't be done
ns	A namespace

Definition at line 780 of file symex_main.cpp.

◆ validate()

void goto_symext::validate ( const validation_modet vm ) const

inline

Definition at line 860 of file goto_symex.h.

◆ vcc()

void goto_symext::vcc	(	const exprt &	cond,
		const irep_idt &	property_id,
		const std::string &	msg,
		statet &	state
	)

protectedvirtual

Symbolically execute a verification condition (assertion).

Parameters

cond	The guard of the assumption
property_id	Unique property identifier of this assertion
msg	The message associated with this assertion
state	Symbolic execution state for current instruction

Definition at line 180 of file symex_main.cpp.

Friends And Related Function Documentation

◆ symex_dereference_statet

friend class symex_dereference_statet

friend

Definition at line 280 of file goto_symex.h.

Member Data Documentation

◆ _remaining_vccs

unsigned goto_symext::_remaining_vccs

protected

Definition at line 833 of file goto_symex.h.

◆ _total_vccs

unsigned goto_symext::_total_vccs

protected

Definition at line 833 of file goto_symex.h.

◆ atomic_section_counter

unsigned goto_symext::atomic_section_counter

protected

A monotonically increasing index for each encountered ATOMIC_BEGIN instruction.

Definition at line 270 of file goto_symex.h.

◆ complexity_module

complexity_limitert goto_symext::complexity_module

protected

Definition at line 836 of file goto_symex.h.

◆ guard_manager

guard_managert& goto_symext::guard_manager

protected

Used to create guards.

Guards created with different guard managers cannot be combined together, so guards created by goto-symex should not escape the scope of this manager.

Definition at line 263 of file goto_symex.h.

◆ ignore_assertions

bool goto_symext::ignore_assertions = false

If this flag is set to true then assertions will be temporarily ignored by the symbolic executions.

Definition at line 171 of file goto_symex.h.

◆ instruction_local_symbols

std::vector<symbol_exprt> goto_symext::instruction_local_symbols

protected

Variables that should be killed at the end of the current symex_step invocation.

Currently this is used for let-bound variables executed during symex, whose lifetime is at most one instruction long.

Definition at line 275 of file goto_symex.h.

◆ language_mode

irep_idt goto_symext::language_mode

language_mode: ID_java, ID_C or another language identifier if we know the source language in use, irep_idt() otherwise.

Definition at line 241 of file goto_symex.h.

◆ log

messaget goto_symext::log

mutableprotected

The messaget to write log messages to.

Definition at line 278 of file goto_symex.h.

◆ ns

namespacet goto_symext::ns

protected

Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol table owned by the goto_symex_statet object used during symbolic execution.

That symbol table must be owned by goto_symex_statet rather than passed in, in case the state is saved and resumed. This namespacet is used during symbolic execution to look up names from the original goto-program, and the names of dynamically-created objects.

Definition at line 258 of file goto_symex.h.

◆ outer_symbol_table

const symbol_table_baset& goto_symext::outer_symbol_table

protected

The symbol table associated with the goto-program being executed.

This symbol table will not have objects that are dynamically created as part of symbolic execution added to it; those object are stored in the symbol table passed as the new_symbol_table argument to the symex_* methods.

Definition at line 249 of file goto_symex.h.

◆ path_segment_vccs

std::size_t goto_symext::path_segment_vccs

Number of VCCs generated during the run of this goto_symext object.

This member is always initialized to 0 upon construction of this object. It therefore differs from goto_symex_statet::total_vccs, which persists across the creation of several goto_symext objects. When CBMC is run in path-exploration mode, the meaning of this member is "the number of VCCs generated between the last branch point and the current instruction," while goto_symex_statet::total_vccs records the total number of VCCs generated along the entire path from the beginning of the program.

Definition at line 822 of file goto_symex.h.

◆ path_storage

path_storaget& goto_symext::path_storage

protected

Symbolic execution paths to be resumed later.

Remarks: Partially-executed symbolic execution paths whose execution can be resumed later

Definition at line 810 of file goto_symex.h.

◆ shadow_memory

shadow_memoryt goto_symext::shadow_memory

protected

Shadow memory instrumentation API.

Definition at line 839 of file goto_symex.h.

◆ should_pause_symex

bool goto_symext::should_pause_symex

Set when states are pushed onto the workqueue If this flag is set at the end of a symbolic execution run, it means that symbolic execution has been paused because we encountered a GOTO instruction while doing path exploration, and thus pushed the successor states of the GOTO onto path_storage.

The symbolic execution caller should now choose which successor state to continue executing, and resume symbolic execution from that state.

Definition at line 167 of file goto_symex.h.

◆ symex_config

const symex_configt goto_symext::symex_config

protected

The configuration to use for this symbolic execution.

Definition at line 185 of file goto_symex.h.

◆ target

symex_target_equationt& goto_symext::target

protected

The equation that this execution is building up.

Definition at line 266 of file goto_symex.h.

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

/home/runner/work/cbmc/cbmc/src/goto-symex/goto_symex.h
/home/runner/work/cbmc/cbmc/src/goto-symex/auto_objects.cpp
/home/runner/work/cbmc/cbmc/src/goto-symex/goto_symex.cpp
/home/runner/work/cbmc/cbmc/src/goto-symex/symex_atomic_section.cpp
/home/runner/work/cbmc/cbmc/src/goto-symex/symex_builtin_functions.cpp
/home/runner/work/cbmc/cbmc/src/goto-symex/symex_catch.cpp
/home/runner/work/cbmc/cbmc/src/goto-symex/symex_clean_expr.cpp
/home/runner/work/cbmc/cbmc/src/goto-symex/symex_dead.cpp
/home/runner/work/cbmc/cbmc/src/goto-symex/symex_decl.cpp
/home/runner/work/cbmc/cbmc/src/goto-symex/symex_dereference.cpp
/home/runner/work/cbmc/cbmc/src/goto-symex/symex_function_call.cpp
/home/runner/work/cbmc/cbmc/src/goto-symex/symex_goto.cpp
/home/runner/work/cbmc/cbmc/src/goto-symex/symex_main.cpp
/home/runner/work/cbmc/cbmc/src/goto-symex/symex_other.cpp
/home/runner/work/cbmc/cbmc/src/goto-symex/symex_set_return_value.cpp
/home/runner/work/cbmc/cbmc/src/goto-symex/symex_start_thread.cpp
/home/runner/work/cbmc/cbmc/src/goto-symex/symex_throw.cpp

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Protected Types

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Friends

Detailed Description

Member Typedef Documentation

◆ assignment_typet

◆ get_goto_functiont

◆ statet

Constructor & Destructor Documentation

◆ goto_symext()

◆ ~goto_symext()

Member Function Documentation

◆ address_arithmetic()

◆ apply_goto_condition()

◆ assign_string_constant()

◆ associate_array_to_pointer()

◆ cache_dereference()

◆ check_break()

◆ clean_expr()

◆ constant_propagate_assignment_with_side_effects()

◆ constant_propagate_case_change()

◆ constant_propagate_delete()

◆ constant_propagate_delete_char_at()

◆ constant_propagate_empty_string()

◆ constant_propagate_integer_to_string()

◆ constant_propagate_replace()

◆ constant_propagate_set_char_at()

◆ constant_propagate_set_length()

◆ constant_propagate_string_concat()

◆ constant_propagate_string_substring()

◆ constant_propagate_trim()

◆ dereference()

◆ dereference_rec()

◆ do_simplify()

◆ execute_next_instruction()

◆ get_goto_function()

◆ get_new_string_data_symbol()

◆ get_remaining_vccs()

◆ get_total_vccs()

◆ get_unwind_recursion()

◆ havoc_rec()

◆ initialize_auto_object()

◆ initialize_entry_point_state()

◆ initialize_path_storage_from_entry_point_of()

◆ kill_instruction_local_symbols()

◆ lift_let()

◆ lift_lets()

◆ locality()

◆ loop_bound_exceeded()

◆ make_auto_object()

◆ merge_goto()

◆ merge_gotos()

◆ parameter_assignments()

◆ phi_function()

◆ print_callstack_entry()

◆ print_symex_step()

◆ process_array_expr()

◆ resume_symex_from_saved_state()

◆ rewrite_quantifiers()

◆ should_stop_unwind()

◆ symex_allocate()

◆ symex_assert()

◆ symex_assign()

◆ symex_assume()

◆ symex_assume_l2()

◆ symex_atomic_begin()

◆ symex_atomic_end()

◆ symex_catch()

◆ symex_cpp_delete()

◆ symex_cpp_new()

◆ symex_dead() [1/2]

◆ symex_dead() [2/2]

◆ symex_decl() [1/2]

◆ symex_decl() [2/2]