#include <symex_bmc.h>

Inheritance diagram for symex_bmct:

Collaboration diagram for symex_bmct:

Public Types
typedef std::function< tvt(const call_stackt &, unsigned, unsigned, unsigned &)>	loop_unwind_handlert
	Loop unwind handlers take the call stack, loop number, the unwind count so far, and an out-parameter specifying an advisory maximum, which they may set. More...

typedef std::function< tvt(const irep_idt &, unsigned, unsigned &)>	recursion_unwind_handlert
	Recursion unwind handlers take the function ID, the unwind count so far, and an out-parameter specifying an advisory maximum, which they may set. More...

Public Types inherited from goto_symext
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
	symex_bmct (message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage, guard_managert &guard_manager, unwindsett &unwindset)

void	add_loop_unwind_handler (loop_unwind_handlert handler)
	Add a callback function that will be called to determine whether to unwind loops. More...

void	add_recursion_unwind_handler (recursion_unwind_handlert handler)
	Add a callback function that will be called to determine whether to unwind recursion. More...

bool	output_coverage_report (const goto_functionst &goto_functions, const std::string &path) const

Public Member Functions inherited from 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)
	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

Public Attributes
source_locationt	last_source_location

const bool	record_coverage

unwindsett &	unwindset

Public Attributes inherited from goto_symext
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 Member Functions
void	symex_step (const get_goto_functiont &get_goto_function, statet &state) override
	show progress More...

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

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

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

Protected Member Functions inherited from goto_symext
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...

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

void	phi_function (const goto_statet &goto_state, statet &dest_state)
	Merge the SSA assignments from goto_state into dest_state. 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...

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

Protected Attributes
std::vector< loop_unwind_handlert >	loop_unwind_handlers
	Callbacks that may provide an unwind/do-not-unwind decision for a loop. More...

std::vector< recursion_unwind_handlert >	recursion_unwind_handlers
	Callbacks that may provide an unwind/do-not-unwind decision for a recursive call. More...

symex_coveraget	symex_coverage

Protected Attributes inherited from goto_symext
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...

unsigned	_total_vccs

unsigned	_remaining_vccs

Additional Inherited Members
Static Public Member Functions inherited from goto_symext
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...

Protected Types inherited from goto_symext
typedef symex_targett::assignment_typet	assignment_typet

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

Detailed Description

Definition at line 23 of file symex_bmc.h.

Member Typedef Documentation

◆ loop_unwind_handlert

typedef std::function< tvt(const call_stackt &, unsigned, unsigned, unsigned &)> symex_bmct::loop_unwind_handlert

Loop unwind handlers take the call stack, loop number, the unwind count so far, and an out-parameter specifying an advisory maximum, which they may set.

If set the advisory maximum is set it is only used to print useful information for the user (e.g. "unwinding iteration N, max M"), and is not enforced. They return true to halt unwinding, false to authorise unwinding, or Unknown to indicate they have no opinion.

Definition at line 46 of file symex_bmc.h.

◆ recursion_unwind_handlert

typedef std::function<tvt(const irep_idt &, unsigned, unsigned &)> symex_bmct::recursion_unwind_handlert

Recursion unwind handlers take the function ID, the unwind count so far, and an out-parameter specifying an advisory maximum, which they may set.

If set the advisory maximum is set it is only used to print useful information for the user (e.g. "unwinding iteration N, max M"), and is not enforced. They return true to halt unwinding, false to authorise unwinding, or Unknown to indicate they have no opinion.

Definition at line 55 of file symex_bmc.h.

Constructor & Destructor Documentation

◆ symex_bmct()

symex_bmct::symex_bmct	(	message_handlert &	mh,
		const symbol_tablet &	outer_symbol_table,
		symex_target_equationt &	_target,
		const optionst &	options,
		path_storaget &	path_storage,
		guard_managert &	guard_manager,
		unwindsett &	unwindset
	)

Definition at line 21 of file symex_bmc.cpp.

Member Function Documentation

◆ add_loop_unwind_handler()

void symex_bmct::add_loop_unwind_handler ( loop_unwind_handlert handler )

inline

Add a callback function that will be called to determine whether to unwind loops.

The first function added will get the first chance to answer, and the first authoratitive (true or false) answer is final.

Parameters

handler new callback

Definition at line 61 of file symex_bmc.h.

◆ add_recursion_unwind_handler()

void symex_bmct::add_recursion_unwind_handler ( recursion_unwind_handlert handler )

inline

Add a callback function that will be called to determine whether to unwind recursion.

The first function added will get the first chance to answer, and the first authoratitive (true or false) answer is final.

Parameters

handler new callback

Definition at line 70 of file symex_bmc.h.

◆ get_unwind_recursion()

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

overrideprotectedvirtual

Reimplemented from goto_symext.

Definition at line 164 of file symex_bmc.cpp.

◆ merge_goto()

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

overrideprotectedvirtual

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 from goto_symext.

Definition at line 98 of file symex_bmc.cpp.

◆ output_coverage_report()

bool symex_bmct::output_coverage_report	(	const goto_functionst &	goto_functions,
		const std::string &	path
	)		const

inline

Definition at line 75 of file symex_bmc.h.

◆ should_stop_unwind()

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

overrideprotectedvirtual

Determine whether to unwind a loop.

Parameters

source
context
unwind

Returns: true indicates abort, with false we continue

Reimplemented from goto_symext.

Reimplemented in symex_bmc_incremental_one_loopt.

Definition at line 118 of file symex_bmc.cpp.

◆ symex_step()

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

overrideprotectedvirtual

show progress

Reimplemented from goto_symext.

Definition at line 43 of file symex_bmc.cpp.

Member Data Documentation

◆ last_source_location

source_locationt symex_bmct::last_source_location

Definition at line 36 of file symex_bmc.h.

◆ loop_unwind_handlers

std::vector<loop_unwind_handlert> symex_bmct::loop_unwind_handlers

protected

Callbacks that may provide an unwind/do-not-unwind decision for a loop.

Definition at line 88 of file symex_bmc.h.

◆ record_coverage

const bool symex_bmct::record_coverage

Definition at line 82 of file symex_bmc.h.

◆ recursion_unwind_handlers

std::vector<recursion_unwind_handlert> symex_bmct::recursion_unwind_handlers

protected

Callbacks that may provide an unwind/do-not-unwind decision for a recursive call.

Definition at line 92 of file symex_bmc.h.

◆ symex_coverage

symex_coveraget symex_bmct::symex_coverage

protected

Definition at line 112 of file symex_bmc.h.

◆ unwindset

unwindsett& symex_bmct::unwindset

Definition at line 84 of file symex_bmc.h.

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

/home/runner/work/cbmc/cbmc/src/goto-checker/symex_bmc.h
/home/runner/work/cbmc/cbmc/src/goto-checker/symex_bmc.cpp

Public Types

Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ loop_unwind_handlert

◆ recursion_unwind_handlert

Constructor & Destructor Documentation

◆ symex_bmct()

Member Function Documentation

◆ add_loop_unwind_handler()

◆ add_recursion_unwind_handler()

◆ get_unwind_recursion()

◆ merge_goto()

◆ output_coverage_report()

◆ should_stop_unwind()

◆ symex_step()

Member Data Documentation

◆ last_source_location

◆ loop_unwind_handlers

◆ record_coverage

◆ recursion_unwind_handlers

◆ symex_coverage

◆ unwindset