#include <symex_bmc_incremental_one_loop.h>

Inheritance diagram for symex_bmc_incremental_one_loopt:

Collaboration diagram for symex_bmc_incremental_one_loopt:

Public Member Functions
	symex_bmc_incremental_one_loopt (message_handlert &, const symbol_tablet &outer_symbol_table, symex_target_equationt &, const optionst &, path_storaget &, guard_managert &, unwindsett &, ui_message_handlert::uit output_ui)

bool	from_entry_point_of (const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)
	Return true if symex can be resumed.

bool	resume (const get_goto_functiont &get_goto_function)
	Return true if symex can be resumed.

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

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

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

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.

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

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.

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.

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.

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

unsigned	get_total_vccs () const

unsigned	get_remaining_vccs () const

void	validate (const validation_modet vm) const

Protected Member Functions
bool	check_break (const irep_idt &loop_id, unsigned unwind) override
	Defines condition for interrupting symbolic execution for incremental BMC.

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

void	log_unwinding (unsigned unwind)

Protected Member Functions inherited from symex_bmct
void	symex_step (const get_goto_functiont &get_goto_function, statet &state) override
	show progress

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.

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

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.

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

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.

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.

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

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

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

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.

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.

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.

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

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

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

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

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

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

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

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

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.

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

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

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

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.

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.

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

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

void	symex_assume_l2 (statet &, const exprt &cond)

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

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

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.

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.

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

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.

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.

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

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

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

virtual void	do_simplify (exprt &expr, const value_sett &value_set)

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.

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)

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

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

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.

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.

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.

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.

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.

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.

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

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.

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

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.

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.

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.

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.

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

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.

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

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.

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

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

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

void	rewrite_quantifiers (exprt &, statet &)

Protected Attributes
const irep_idt	incr_loop_id

const unsigned	incr_max_unwind

const unsigned	incr_min_unwind

std::unique_ptr< goto_symext::statet >	state

ui_message_handlert::uit	output_ui

Protected Attributes inherited from symex_bmct
unwindsett &	unwindset

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

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

symex_coveraget	symex_coverage

Protected Attributes inherited from goto_symext
const symex_configt	symex_config
	The configuration to use for this symbolic execution.

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

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.

guard_managert &	guard_manager
	Used to create guards.

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

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

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

messaget	log
	The messaget to write log messages to.

path_storaget &	path_storage
	Symbolic execution paths to be resumed later.

complexity_limitert	complexity_module

shadow_memoryt	shadow_memory
	Shadow memory instrumentation API.

unsigned	_total_vccs

unsigned	_remaining_vccs

Additional Inherited Members
Public Types inherited from symex_bmct
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.

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.

Public Types inherited from goto_symext
typedef goto_symex_statet	statet
	A type abbreviation for goto_symex_statet.

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.

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.

Public Attributes inherited from symex_bmct
source_locationt	last_source_location

const bool	record_coverage

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.

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

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.

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

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 15 of file symex_bmc_incremental_one_loop.h.

Constructor & Destructor Documentation

◆ symex_bmc_incremental_one_loopt()

symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt	(	message_handlert &	message_handler,
		const symbol_tablet &	outer_symbol_table,
		symex_target_equationt &	target,
		const optionst &	options,
		path_storaget &	path_storage,
		guard_managert &	guard_manager,
		unwindsett &	unwindset,
		ui_message_handlert::uit	output_ui
	)