1/*******************************************************************\
3Module: Traces of GOTO Programs
9\*******************************************************************/
42 // get index value from src_ssa
55 return std::move(
tmp);
88 return tmp2.true_case();
90 return tmp2.false_case();
92 return std::move(
tmp2);
102 return std::move(
tmp);
111 // re-write into big case-split
126 const auto &type = expr.
type();
131 if(!ns.
lookup(
id, symbol))
141 for(
const auto &op : expr.
operands())
153 // set internal for dynamic_object in both lhs and rhs expressions
157 // set internal field to CPROVER functions (e.g., __CPROVER_initialize)
160 if(SSA_step.
source.
pc->source_location().as_string().empty())
164 // set internal field to input and output steps
171 // set internal field to _start function-return step
174 // "__CPROVER_*" function calls in __CPROVER_start are already marked as
175 // internal. Don't mark any other function calls (i.e. "main"), function
176 // arguments or any other parts of a code_function_callt as internal.
214 // We need to re-sort the steps according to their clock.
215 // Furthermore, read-events need to occur before write
216 // events with the same clock.
219 typedef std::map<mp_integer, std::vector<ssa_step_iteratort>>
time_mapt;
228 // First sort the SSA steps by time, in the process dropping steps
229 // we definitely don't want to retain in the final trace:
247 if(it->is_constraint() ||
250 else if(it->is_atomic_begin())
252 // for atomic sections the timing can only be determined once we see
253 // a shared read or write (if there is none, the time will be
254 // reverted to the time before entering the atomic section); we thus
255 // use a temporary negative time slot to gather all events
259 else if(it->is_shared_read() || it->is_shared_write() ||
267 if(it->is_shared_read() || it->is_shared_write())
269 // these are just used to get the time stamp -- the clock type is
270 // computed to be of the minimal necessary size, but we don't need to
271 // know it to get the value so just use typeless
285 // move any steps gathered in an atomic section
309 // drop PHI and GUARD assignments altogether
310 if(it->is_assignment() &&
329 "last step in SSA trace to keep must not be filtered out as a sync "
330 "instruction, not-taken branch, PHI node, or similar");
332 // Now build the GOTO trace, ordered by time, then by SSA trace order.
334 // produce the step numbers
335 unsigned step_nr = 0;
350 if(SSA_step.is_assert())
362 for(
const auto &arg : SSA_step.converted_function_arguments)
368 // update internal field for specific variables in the counterexample
372 (SSA_step.is_assignment() &&
373 (SSA_step.assignment_type ==
375 SSA_step.assignment_type ==
380 if(SSA_step.original_full_lhs.is_not_nil())
386 SSA_step.original_full_lhs,
387 SSA_step.ssa_full_lhs),
393 if(SSA_step.ssa_full_lhs.is_not_nil())
396 decision_procedure.
get(SSA_step.ssa_full_lhs);
402 for(
const auto &j : SSA_step.converted_io_args)
408 if(SSA_step.is_assert() || SSA_step.is_assume() || SSA_step.is_goto())
413 decision_procedure.
get(SSA_step.cond_handle) ==
true;
416 if(SSA_step.source.pc->is_assert() || SSA_step.source.pc->is_assume())
437 symex_target_equationt::SSA_stepst::const_iterator it,
445 symex_target_equationt::SSA_stepst::const_iterator step,
448 return step->is_assert() &&
449 decision_procedure.
get(step->cond_handle) ==
false;
static exprt build_full_lhs_rec(const decision_proceduret &decision_procedure, const namespacet &ns, const exprt &src_original, const exprt &src_ssa)
static void set_internal_dynamic_object(const exprt &expr, goto_trace_stept &goto_trace_step, const namespacet &ns)
set internal field for variable assignment related to dynamic_object[0-9] and dynamic_[0-9]_array.
static void update_internal_field(const SSA_stept &SSA_step, goto_trace_stept &goto_trace_step, const namespacet &ns)
set internal for variables assignments related to dynamic_object and CPROVER internal functions (e....
static bool is_failed_assertion_step(symex_target_equationt::SSA_stepst::const_iterator step, const decision_proceduret &decision_procedure)
static void replace_nondet_in_type(typet &type, const decision_proceduret &solver)
Replace nondet values that appear in type by their values as found by solver.
void build_goto_trace(const symex_target_equationt &target, ssa_step_predicatet is_last_step_to_keep, const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace)
Build a trace by going through the steps of target and stopping after the step matching a given condi...
std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const decision_proceduret &)> ssa_step_predicatet
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Single SSA step in the equation.
symex_targett::assignment_typet assignment_type
symex_targett::sourcet source
bool is_function_call() const
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
An interface for a decision procedure for satisfiability problems.
virtual exprt get(const exprt &) const =0
Return expr with variables replaced by values from satisfying assignment if available.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Step of the trace of a GOTO program.
The trinary if-then-else operator.
bool get_bool(const irep_idt &name) const
const irep_idt & id() const
Extract member of struct or union.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
static irep_idt rw_clock_id(event_it e, axiomt axiom=AX_PROPAGATION)
Build identifier for the read/write clock variable.
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
typet type
Type of symbol.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
@ VISIBLE_ACTUAL_PARAMETER
@ HIDDEN_ACTUAL_PARAMETER
Semantic type conversion.
The type of an expression, extends irept.
Decision Procedure Interface.
Goto Programs with Functions.
Add constraints to equation encoding partial orders on events.
void restore_union(exprt &expr, const namespacet &ns)
Undo the union access -> byte_extract replacement that rewrite_union did for the purpose of displayin...
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
void solver(std::vector< framet > &frames, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const solver_optionst &solver_options, const namespacet &ns, std::vector< propertyt > &properties, std::size_t property_index)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
goto_programt::const_targett pc
const type_with_subtypet & to_type_with_subtype(const typet &type)