Go to the documentation of this file.
40 exprt new_guard=old_guard;
56 !instruction.
targets.empty(),
"goto should have at least one target");
60 instruction.
targets.size() == 1,
"no support for non-deterministic gotos");
116 (simpl_state_guard.
is_true() ||
122 instruction.
targets.size() > 0,
123 "Instruction is an unconditional goto with no target: " +
134 new_state_pc=goto_target;
140 while(state_pc!=goto_target && !state_pc->is_target())
143 if(state_pc==goto_target)
153 state_pc=goto_target;
164 "Tried to explore the other path of a branch, but the next "
165 "instruction along that path is not the same as the instruction "
166 "that we saved at the branch point. Saved instruction is " +
168 "\nwe were intending "
170 new_state_pc->code.pretty() +
172 "instruction we think we saw on a previous path exploration is " +
173 state_pc->code.pretty());
175 new_state_pc = state_pc;
183 log.
debug() <<
"Resuming from next instruction '"
202 log.
debug() <<
"Saving next instruction '"
205 log.
debug() <<
"Saving jump target '"
236 new_guard.
id() == ID_symbol ||
237 (new_guard.
id() == ID_not &&
240 guard_expr=new_guard;
264 new_lhs, new_lhs, guard_symbol_expr,
302 statet::goto_state_mapt::iterator state_map_it=
311 for(statet::goto_state_listt::reverse_iterator
312 list_it=state_list.rbegin();
313 list_it!=state_list.rend();
328 "atomic sections differ across branches",
360 const std::map<
irep_idt, std::pair<ssa_exprt, unsigned>> &first_map,
361 const std::map<
irep_idt, std::pair<ssa_exprt, unsigned>> &second_map,
362 const std::function<
void(
const ssa_exprt &,
unsigned,
unsigned)> &f)
364 auto second_it = second_map.begin();
365 for(
const auto &first_pair : first_map)
367 while(second_it != second_map.end() && second_it->first < first_pair.first)
369 f(second_it->second.first, 0, second_it->second.second);
372 const ssa_exprt &ssa = first_pair.second.first;
373 const unsigned count = first_pair.second.second;
374 if(second_it != second_map.end() && second_it->first == first_pair.first)
376 f(ssa, count, second_it->second.second);
382 while(second_it != second_map.end())
384 f(second_it->second.first, 0, second_it->second.second);
411 const bool do_simplify,
414 const unsigned goto_count,
415 const unsigned dest_count)
420 if(obj_identifier == guard_identifier)
423 if(goto_count == dest_count)
446 exprt goto_state_rhs = ssa, dest_state_rhs = ssa;
449 const auto p_it = goto_state.
propagation.find(l1_identifier);
452 goto_state_rhs = p_it->second;
458 const auto p_it = dest_state.
propagation.find(l1_identifier);
461 dest_state_rhs = p_it->second;
473 rhs = goto_state_rhs;
475 rhs = dest_state_rhs;
476 else if(goto_count == 0)
478 rhs = dest_state_rhs;
480 else if(dest_count == 0)
482 rhs = goto_state_rhs;
494 dest_state.
assignment(new_lhs, rhs, ns,
true,
true);
525 diff_guard -= dest_state.
guard;
530 [&](
const ssa_exprt &ssa,
unsigned goto_count,
unsigned dest_count) {
538 symex_config.simplify_opt,
550 const unsigned loop_number=state.
source.
pc->loop_number;
Class that provides messages with a built-in verbosity 'level'.
virtual bool should_stop_unwind(const symex_targett::sourcet &source, const goto_symex_statet::call_stackt &context, unsigned unwind)
void merge_value_sets(const statet::goto_statet &goto_state, statet &dest)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
goto_state_mapt goto_state_map
static void merge_names(const goto_symext::statet::goto_statet &goto_state, goto_symext::statet &dest_state, const namespacet &ns, const guardt &diff_guard, const irep_idt &guard_identifier, messaget &log, const bool do_simplify, symex_target_equationt &target, 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.
bool self_loops_to_assumptions
const irep_idt get_level_0() const
void merge_gotos(statet &)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
goto_programt::const_targett pc
symex_target_equationt & target
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
path_storaget & path_storage
void add(const exprt &expr)
The trinary if-then-else operator.
const irep_idt guard_identifier
void clean_expr(exprt &, statet &, bool write)
std::map< irep_idt, exprt > propagation
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
Base class for all expressions.
irep_idt get_object_name() const
symex_targett::sourcet source
symex_level2t::current_namest level2_current_names
virtual void do_simplify(exprt &)
virtual void goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)
Record a goto instruction.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
targetst targets
The list of successor instructions.
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
bool is_true() const
Return whether the expression is a constant representing true.
std::unordered_map< irep_idt, loop_infot > loop_iterations
Expression to hold a symbol (variable)
const exprt & get_original_expr() const
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
bool is_false() const
Return whether the expression is a constant representing false.
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
Expression providing an SSA-renamed symbol of expressions.
std::map< irep_idt, exprt > propagation
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
std::list< goto_statet > goto_state_listt
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
unsigned depth
distance from entry
std::vector< threadt > threads
call_stackt & call_stack()
static void for_each2(const std::map< irep_idt, std::pair< ssa_exprt, unsigned >> &first_map, const std::map< irep_idt, std::pair< ssa_exprt, unsigned >> &second_map, const std::function< void(const ssa_exprt &, unsigned, unsigned)> &f)
Applies f to (k, ssa, i, j) if the first map maps k to (ssa, i) and the second to (ssa',...
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
source_locationt source_location
unsigned atomic_section_id
const irep_idt & get_identifier() const
bool doing_path_exploration
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
bool unwinding_assertions
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
bool simplify(exprt &expr, const namespacet &ns)
static irep_idt loop_id(const instructiont &instruction)
Human-readable loop name.
virtual void symex_goto(statet &)
const irep_idt & id() const
The Boolean constant false.
Information saved at a conditional goto to resume execution.
std::vector< framet > call_stackt
void symex_transition(goto_symext::statet &state)
unsigned atomic_section_id
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual void loop_bound_exceeded(statet &, const exprt &guard)
virtual void symex_assume(statet &, const exprt &cond)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Deprecated expression utility functions.
std::set< targett > incoming_edges
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
void phi_function(const statet::goto_statet &goto_state, statet &)
virtual void vcc(const exprt &, const std::string &msg, statet &)
exprt guard
Guard for gotos, assume, assert.
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
const symex_configt symex_config
void set_level_2(unsigned i)
instructionst::const_iterator const_targett
virtual void push(const patht &next_instruction, const patht &jump_target)=0
Add paths to resume to the storage.
virtual void merge_goto(const statet::goto_statet &goto_state, statet &)
goto_programt::const_targett saved_target
Identifies source in the context of symbolic execution.
The Boolean constant true.
This class represents an instruction in the GOTO intermediate representation.
current_namest current_names
irep_idt name
The unique identifier.
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
bool should_pause_symex
Have states been pushed onto the workqueue?
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)
Write to a local variable.