symex_goto.cpp File Reference

Symbolic Execution. More...

#include <util/exception_utils.h>
#include <util/expr_util.h>
#include <util/invariant.h>
#include <util/pointer_expr.h>
#include <util/pointer_offset_size.h>
#include <util/simplify_expr.h>
#include <util/std_expr.h>
#include <langapi/language_util.h>
#include <pointer-analysis/add_failed_symbols.h>
#include <pointer-analysis/value_set_dereference.h>
#include "goto_symex.h"
#include "goto_symex_can_forward_propagate.h"
#include "path_storage.h"
#include <algorithm>

Include dependency graph for symex_goto.cpp:

Go to the source code of this file.

Functions
static std::optional< renamedt< exprt, L2 > >	try_evaluate_pointer_comparison (const irep_idt &operation, const symbol_exprt &symbol_expr, const exprt &other_operand, const value_sett &value_set, const irep_idt language_mode, const namespacet &ns)
	Try to evaluate a simple pointer comparison.
static std::optional< renamedt< exprt, L2 > >	try_evaluate_pointer_comparison (const renamedt< exprt, L2 > &renamed_expr, const value_sett &value_set, const irep_idt &language_mode, const namespacet &ns)
	Check if we have a simple pointer comparison, and if so try to evaluate it.
renamedt< exprt, L2 >	try_evaluate_pointer_comparisons (renamedt< exprt, L2 > condition, const value_sett &value_set, const irep_idt &language_mode, const namespacet &ns)
	Try to evaluate pointer comparisons where they can be trivially determined using the value-set.
static guardt	merge_state_guards (goto_statet &goto_state, goto_symex_statet &state)
static void	merge_names (const goto_statet &goto_state, goto_symext::statet &dest_state, const namespacet &ns, const guardt &diff_guard, messaget &log, const bool do_simplify, symex_target_equationt &target, const incremental_dirtyt &dirty, const ssa_exprt &ssa, const unsigned goto_count, const unsigned dest_count)
	Helper function for phi_function which merges the names of an identifier for two different states.

Detailed Description

Symbolic Execution.

Definition in file symex_goto.cpp.

Function Documentation

merge_names()

static void merge_names ( const goto_statet & goto_state, goto_symext::statet & dest_state, const namespacet & ns, const guardt & diff_guard, messaget & log, const bool do_simplify, symex_target_equationt & target, const incremental_dirtyt & dirty, const ssa_exprt & ssa, const unsigned goto_count, const unsigned dest_count )

static

Helper function for phi_function which merges the names of an identifier for two different states.

Parameters

	goto_state	first state
[in,out]	dest_state	second state
	ns	namespace
	diff_guard	difference between the guards of the two states
[out]	log	logger for debug messages
	do_simplify	should the right-hand-side of the assignment that is added to the target be simplified
[out]	target	equation that will receive the resulting assignment
	dirty	dirty-object analysis
	ssa	SSA expression to merge
	goto_count	current level 2 count in goto_state of l1_identifier
	dest_count	level 2 count in dest_state of l1_identifier

Definition at line 735 of file symex_goto.cpp.

merge_state_guards()

static guardt merge_state_guards ( goto_statet & goto_state, goto_symex_statet & state )

static

Definition at line 647 of file symex_goto.cpp.

try_evaluate_pointer_comparison() [1/2]

static std::optional< renamedt< exprt, L2 > > try_evaluate_pointer_comparison ( const irep_idt & operation, const symbol_exprt & symbol_expr, const exprt & other_operand, const value_sett & value_set, const irep_idt language_mode, const namespacet & ns )

static

Try to evaluate a simple pointer comparison.

Parameters

operation	ID_equal or ID_not_equal
symbol_expr	The symbol expression in the condition
other_operand	The other expression in the condition; we only support an address of expression, a typecast of an address of expression or a null pointer, and return an empty std::optional in all other cases
value_set	The value-set for looking up what the symbol can point to
language_mode	The language mode
ns	A namespace

Returns

If we were able to evaluate the condition as true or false then we return that, otherwise we return an empty std::optional

Definition at line 81 of file symex_goto.cpp.

try_evaluate_pointer_comparison() [2/2]

static std::optional< renamedt< exprt, L2 > > try_evaluate_pointer_comparison ( const renamedt< exprt, L2 > & renamed_expr, const value_sett & value_set, const irep_idt & language_mode, const namespacet & ns )

static

Check if we have a simple pointer comparison, and if so try to evaluate it.

Parameters

renamed_expr	The L2-renamed expression to check
value_set	The value-set for looking up what the symbol can point to
language_mode	The language mode
ns	A namespace

Returns

If we were able to evaluate the condition as true or false then we return that, otherwise we return an empty std::optional

Definition at line 183 of file symex_goto.cpp.

try_evaluate_pointer_comparisons()

renamedt< exprt, L2 > try_evaluate_pointer_comparisons	(	renamedt< exprt, L2 >	condition,
		const value_sett &	value_set,
		const irep_idt &	language_mode,
		const namespacet &	ns )

Try to evaluate pointer comparisons where they can be trivially determined using the value-set.

This is optional as all it does is allow symex to resolve some comparisons itself and therefore create a simpler formula for the SAT solver.

Parameters

[in,out]	condition	An L2-renamed expression with boolean type
	value_set	The value-set for determining what pointer-typed symbols might possibly point to
	language_mode	The language mode
	ns	A namespace

Returns

The possibly modified condition

Definition at line 214 of file symex_goto.cpp.