symex_goto.cpp File Reference

#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_is_constant.h"
#include "path_storage.h"
#include <algorithm>

Include dependency graph for symex_goto.cpp:

Go to the source code of this file.

Functions
static optionalt< 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 optionalt< 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 optionalt<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 optionalt 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 optionalt

Definition at line 81 of file symex_goto.cpp.

try_evaluate_pointer_comparison() [2/2]

static optionalt<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 optionalt

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.