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;
exprt guard
Guard for gotos, assume, assert.
irep_idt name
The unique identifier.
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
goto_programt::const_targett pc
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.
virtual void symex_goto(statet &)
std::set< targett > incoming_edges
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Variables whose address is taken.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Deprecated expression utility functions.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
const irep_idt & get_identifier() const
std::map< irep_idt, exprt > propagation
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.
virtual void goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)
Record a goto instruction.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual void merge_goto(const statet::goto_statet &goto_state, statet &)
The trinary if-then-else operator.
goto_state_mapt goto_state_map
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
void set_level_2(unsigned i)
virtual void do_simplify(exprt &)
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
std::map< irep_idt, exprt > propagation
targetst targets
The list of successor instructions.
unsigned depth
distance from entry
This class represents an instruction in the GOTO intermediate representation.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
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',...
const irep_idt & id() const
unsigned atomic_section_id
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
The Boolean constant true.
Identifies source in the context of symbolic execution.
bool doing_path_exploration
source_locationt source_location
virtual void symex_assume(statet &, const exprt &cond)
API to expression classes.
symex_target_equationt & target
void merge_value_sets(const statet::goto_statet &goto_state, statet &dest)
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static irep_idt loop_id(const instructiont &instruction)
Human-readable loop name.
void symex_transition(goto_symext::statet &state)
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.
std::vector< threadt > threads
const irep_idt get_level_0() const
path_storaget & path_storage
current_namest current_names
std::unordered_map< irep_idt, loop_infot > loop_iterations
Class that provides messages with a built-in verbosity 'level'.
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.
virtual bool should_stop_unwind(const symex_targett::sourcet &source, const goto_symex_statet::call_stackt &context, unsigned unwind)
unsigned atomic_section_id
virtual void loop_bound_exceeded(statet &, const exprt &guard)
The Boolean constant false.
void phi_function(const statet::goto_statet &goto_state, statet &)
virtual void vcc(const exprt &, const std::string &msg, statet &)
std::vector< framet > call_stackt
bool self_loops_to_assumptions
symex_level2t::current_namest level2_current_names
void clean_expr(exprt &, statet &, bool write)
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
goto_programt::const_targett saved_target
bool should_pause_symex
Have states been pushed onto the workqueue?
const symex_configt symex_config
Base class for all expressions.
call_stackt & call_stack()
irep_idt get_object_name() const
const exprt & get_original_expr() const
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 not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
Information saved at a conditional goto to resume execution.
const irep_idt guard_identifier
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
void merge_gotos(statet &)
Expression to hold a symbol (variable)
bool unwinding_assertions
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
virtual void push(const patht &next_instruction, const patht &jump_target)=0
Add paths to resume to the storage.
std::list< goto_statet > goto_state_listt
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Expression providing an SSA-renamed symbol of expressions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void add(const exprt &expr)
bool simplify(exprt &expr, const namespacet &ns)
symex_targett::sourcet source