30 const exprt &src_original,
33 if(src_ssa.
id()!=src_original.
id())
47 tmp.
index()=index_value;
57 else if(
id==ID_member)
79 else if(tmp.is_false())
84 else if(
id==ID_typecast)
91 else if(
id==ID_byte_extract_little_endian ||
92 id==ID_byte_extract_big_endian)
94 exprt tmp=src_original;
111 if(expr.
id()==ID_symbol)
115 if(!ns.
lookup(
id, symbol))
143 if(SSA_step.
source.pc->source_location.as_string().empty())
160 if(SSA_step.
source.pc->code.get_statement()!=ID_function_call)
176 typedef symex_target_equationt::SSA_stepst::const_iterator ssa_step_iteratort;
177 typedef std::map<mp_integer, std::vector<ssa_step_iteratort>> time_mapt;
182 ssa_step_iteratort last_step_to_keep = target.
SSA_steps.end();
183 bool last_step_was_kept =
false;
188 for(ssa_step_iteratort it = target.
SSA_steps.begin();
193 last_step_to_keep == target.
SSA_steps.end() &&
194 is_last_step_to_keep(it, prop_conv))
196 last_step_to_keep = it;
204 if(it->is_constraint() ||
207 else if(it->is_atomic_begin())
216 else if(it->is_shared_read() || it->is_shared_write() ||
221 if(it->is_shared_read() || it->is_shared_write())
229 else if(it->is_atomic_end() && current_time<0)
232 assert(current_time>=0);
237 time_mapt::const_iterator time_before_steps_it =
238 time_map.find(time_before);
240 if(time_before_steps_it != time_map.end())
242 std::vector<ssa_step_iteratort> ¤t_time_steps =
243 time_map[current_time];
245 current_time_steps.insert(
246 current_time_steps.end(),
247 time_before_steps_it->second.begin(),
248 time_before_steps_it->second.end());
250 time_map.erase(time_before_steps_it);
258 if(it->is_assignment() &&
267 if(it == last_step_to_keep)
269 last_step_was_kept =
true;
272 time_map[current_time].push_back(it);
276 last_step_to_keep == target.
SSA_steps.end() || last_step_was_kept,
277 "last step in SSA trace to keep must not be filtered out as a sync " 278 "instruction, not-taken branch, PHI node, or similar");
283 unsigned step_nr = 0;
285 for(
const auto &time_and_ssa_steps : time_map)
287 for(
const auto ssa_step_it : time_and_ssa_steps.second)
289 const auto &SSA_step = *ssa_step_it;
293 goto_trace_step.
step_nr = ++step_nr;
295 goto_trace_step.
thread_nr = SSA_step.source.thread_nr;
296 goto_trace_step.
pc = SSA_step.source.pc;
297 goto_trace_step.
comment = SSA_step.comment;
298 if(SSA_step.ssa_lhs.is_not_nil())
301 ssa_exprt(SSA_step.ssa_lhs.get_original_expr());
307 goto_trace_step.
type = SSA_step.type;
308 goto_trace_step.
hidden = SSA_step.hidden;
310 goto_trace_step.
io_id = SSA_step.io_id;
311 goto_trace_step.
formatted = SSA_step.formatted;
312 goto_trace_step.
identifier = SSA_step.identifier;
318 (SSA_step.is_assignment() &&
319 (SSA_step.assignment_type ==
321 SSA_step.assignment_type ==
326 if(SSA_step.original_full_lhs.is_not_nil())
329 prop_conv, ns, SSA_step.original_full_lhs, SSA_step.ssa_full_lhs);
332 if(SSA_step.ssa_lhs.is_not_nil())
335 if(SSA_step.ssa_full_lhs.is_not_nil())
341 for(
const auto &j : SSA_step.converted_io_args)
343 if(j.is_constant() || j.id() == ID_string_constant)
345 goto_trace_step.
io_args.push_back(j);
350 goto_trace_step.
io_args.push_back(tmp);
354 if(SSA_step.is_assert() || SSA_step.is_assume() || SSA_step.is_goto())
356 goto_trace_step.
cond_expr = SSA_step.cond_expr;
362 if(ssa_step_it == last_step_to_keep)
370 symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep,
375 const auto is_last_step_to_keep = [last_step_to_keep](
376 symex_target_equationt::SSA_stepst::const_iterator it,
const prop_convt &) {
377 return last_step_to_keep == it;
381 target, is_last_step_to_keep, prop_conv, ns, goto_trace);
385 symex_target_equationt::SSA_stepst::const_iterator step,
388 return step->is_assert() && prop_conv.
l_get(step->cond_literal).
is_false();
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
void build_goto_trace(const symex_target_equationt &target, ssa_step_predicatet is_last_step_to_keep, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
static bool is_failed_assertion_step(symex_target_equationt::SSA_stepst::const_iterator step, const prop_convt &prop_conv)
virtual exprt get(const exprt &expr) const =0
bool is_function_call() const
std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const prop_convt &)> ssa_step_predicatet
The trinary if-then-else operator.
assignment_typet assignment_type
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
bool get_bool(const irep_namet &name) const
goto_programt::const_targett pc
Add constraints to equation encoding partial orders on events.
#define INVARIANT(CONDITION, REASON)
Extract member of struct or union.
static irep_idt rw_clock_id(event_it e, axiomt axiom=AX_PROPAGATION)
const irep_idt & id() const
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const irep_idt get_original_name() const
#define forall_operands(it, expr)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
typet type
Type of symbol.
virtual tvt l_get(literalt a) const =0
static irep_idt entry_point()
Base class for all expressions.
const exprt & struct_op() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
void update_internal_field(const symex_target_equationt::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...
exprt build_full_lhs_rec(const prop_convt &prop_conv, const namespacet &ns, const exprt &src_original, const exprt &src_ssa)
Expression to hold a symbol (variable)
Expression providing an SSA-renamed symbol of expressions.
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.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
bool simplify(exprt &expr, const namespacet &ns)
assignment_typet assignment_type