27 : max_depth(options.get_unsigned_int_option(
"depth")),
28 doing_path_exploration(options.is_set(
"paths")),
29 allow_pointer_unsoundness(
30 options.get_bool_option(
"allow-pointer-unsoundness")),
31 constant_propagation(options.get_bool_option(
"propagation")),
32 self_loops_to_assumptions(
33 options.get_bool_option(
"self-loops-to-assumptions")),
34 simplify_opt(options.get_bool_option(
"simplify")),
35 unwinding_assertions(options.get_bool_option(
"unwinding-assertions")),
36 partial_loops(options.get_bool_option(
"partial-loops")),
38 run_validation_checks(options.get_bool_option(
"validate-ssa-equation"))
45 bool is_backwards_goto)
57 if(i_e->is_goto() && i_e->is_backwards_goto() &&
58 (!is_backwards_goto ||
59 state.
source.
pc->location_number>i_e->location_number))
74 const exprt &vcc_expr,
75 const std::string &msg,
103 exprt simplified_cond=cond;
112 exprt tmp=simplified_cond;
132 if(expr.
id()==ID_forall)
140 exprt tmp = quant_expr.where();
141 quant_expr.
swap(tmp);
148 const irep_idt &function_identifier,
160 !pc->function.empty(),
"all symexed instructions should have a function");
162 const goto_functiont &entry_point_function = get_goto_function(pc->function);
166 auto emplace_safe_pointers_result =
168 if(emplace_safe_pointers_result.second)
169 emplace_safe_pointers_result.first->second(entry_point_function.body);
211 std::cout <<
"********* Now executing thread " << t <<
'\n';
221 return [&goto_functions](
275 const statet &saved_state,
285 statet state(saved_state, saved_equation);
304 catch(
const std::out_of_range &)
317 start_function->body.instructions.
begin(),
318 prev(start_function->body.instructions.end()));
321 state, get_goto_function, new_symbol_table);
330 std::cout <<
"\ninstruction type is " << state.
source.
pc->type <<
'\n';
331 std::cout <<
"Location: " << state.
source.
pc->source_location <<
'\n';
350 switch(instruction.type)
378 exprt tmp=instruction.guard;
393 exprt tmp(instruction.guard);
395 vcc(tmp, msg, state);
std::string::const_iterator begin() const
void return_assignment(statet &)
const std::string & id2string(const irep_idt &d)
virtual void symex_from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)
symex entire program starting from entry point
goto_programt::const_targett pc
void guard_expr(exprt &dest) const
virtual void symex_goto(statet &)
std::set< targett > incoming_edges
Variables whose address is taken.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
bool run_validation_checks
Should the additional validation checks be run?
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
Record an assumption.
bool is_false() const
Return whether the expression is a constant representing false.
Thrown when we encounter an instruction, parameters to an instruction etc.
symex_target_equationt * symex_target
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
bool is_true() const
Return whether the expression is a constant representing true.
function_mapt function_map
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
virtual void resume_symex_from_saved_state(const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *saved_equation, symbol_tablet &new_symbol_table)
Performs symbolic execution using a state and equation that have already been used to symex part of t...
virtual void do_simplify(exprt &)
goto_programt::const_targett end_of_function
virtual void symex_step(const get_goto_functiont &, statet &)
do just one step
virtual void symex_end_of_function(statet &)
do function call by inlining
unsigned depth
distance from entry
void symex_catch(statet &)
virtual void symex_atomic_end(statet &)
This class represents an instruction in the GOTO intermediate representation.
void initialize_entry_point(statet &state, const get_goto_functiont &get_goto_function, const irep_idt &function_identifier, goto_programt::const_targett pc, goto_programt::const_targett limit)
Initialise the symbolic execution and the given state with pc as entry point.
void symex_throw(statet &)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
virtual void symex_atomic_begin(statet &)
virtual void symex_other(statet &)
Identifies source in the context of symbolic execution.
#define Forall_expr(it, expr)
bool doing_path_exploration
static goto_symext::get_goto_functiont get_function_from_goto_functions(const goto_functionst &goto_functions)
virtual void symex_with_state(statet &, const goto_functionst &, symbol_tablet &)
symex entire program starting from entry point
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program that we're executing.
virtual void symex_assume(statet &, const exprt &cond)
virtual void symex_decl(statet &)
symex_targett::sourcet calling_location
API to expression classes.
symex_target_equationt & target
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
::goto_functiont goto_functiont
std::size_t path_segment_vccs
Number of VCCs generated during the run of this goto_symext object.
static irep_idt loop_id(const instructiont &instruction)
Human-readable loop name.
#define PRECONDITION(CONDITION)
bool run_validation_checks
Should the additional validation checks be run?
std::vector< threadt > threads
codet representation of a function call statement.
static void switch_to_thread(goto_symex_statet &state, const unsigned int thread_nb)
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
std::unordered_map< irep_idt, loop_infot > loop_iterations
void populate_dirty_for_function(const irep_idt &id, const goto_functionst::goto_functiont &function)
Analyse the given function with dirtyt if it hasn't been seen before.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
unsigned atomic_section_id
The Boolean constant false.
A goto function, consisting of function type (see type), function body (see body),...
void rewrite_quantifiers(exprt &, statet &)
void symex_assign(statet &, const code_assignt &)
virtual void vcc(const exprt &, const std::string &msg, statet &)
void symex_threaded_step(statet &, const get_goto_functiont &)
Invokes symex_step and verifies whether additional threads can be executed.
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
Record an assertion.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
void clean_expr(exprt &, statet &, bool write)
bool should_pause_symex
Have states been pushed onto the workqueue?
const symex_configt symex_config
Base class for all expressions.
symex_configt(const optionst &options)
call_stackt & call_stack()
#define UNREACHABLE
This should be used to mark dead code.
virtual void symex_dead(statet &)
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
virtual void symex_start_thread(statet &)
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
void merge_gotos(statet &)
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
Expression to hold a symbol (variable)
void symex_transition(goto_symext::statet &state, goto_programt::const_targett to, bool is_backwards_goto)
virtual void symex_function_call(const get_goto_functiont &, statet &, const code_function_callt &)
int unsafe_string2int(const std::string &str, int base)
void add(const exprt &expr)
const code_function_callt & to_code_function_call(const codet &code)
symex_targett::sourcet source