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

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.