30 const exprt &src_original,
33 if(src_ssa.
id()!=src_original.
id())
47 tmp.
index()=index_value;
53 return std::move(tmp);
58 else if(
id==ID_member)
90 return std::move(tmp2);
92 else if(
id==ID_typecast)
100 return std::move(tmp);
102 else if(
id==ID_byte_extract_little_endian ||
103 id==ID_byte_extract_big_endian)
122 if(expr.
id()==ID_symbol)
124 const auto &type = expr.
type();
125 if(type.id() != ID_code && type.id() != ID_mathematical_function)
129 if(!ns.
lookup(
id, symbol))
158 if(SSA_step.
source.
pc->source_location.as_string().empty())
175 if(SSA_step.
source.
pc->code.get_statement()!=ID_function_call)
185 if(type.
id() == ID_array)
215 typedef symex_target_equationt::SSA_stepst::const_iterator ssa_step_iteratort;
216 typedef std::map<mp_integer, std::vector<ssa_step_iteratort>> time_mapt;
221 ssa_step_iteratort last_step_to_keep = target.
SSA_steps.end();
222 bool last_step_was_kept =
false;
227 for(ssa_step_iteratort it = target.
SSA_steps.begin();
232 last_step_to_keep == target.
SSA_steps.end() &&
233 is_last_step_to_keep(it, decision_procedure))
235 last_step_to_keep = it;
243 if(it->is_constraint() ||
246 else if(it->is_atomic_begin())
255 else if(it->is_shared_read() || it->is_shared_write() ||
260 if(it->is_shared_read() || it->is_shared_write())
265 exprt clock_value = decision_procedure.
get(
268 const auto cv = numeric_cast<mp_integer>(clock_value);
274 else if(it->is_atomic_end() && current_time<0)
277 INVARIANT(current_time >= 0,
"time keeping inconsistency");
282 time_mapt::const_iterator time_before_steps_it =
283 time_map.find(time_before);
285 if(time_before_steps_it != time_map.end())
287 std::vector<ssa_step_iteratort> ¤t_time_steps =
288 time_map[current_time];
290 current_time_steps.insert(
291 current_time_steps.end(),
292 time_before_steps_it->second.begin(),
293 time_before_steps_it->second.end());
295 time_map.erase(time_before_steps_it);
303 if(it->is_assignment() &&
312 if(it == last_step_to_keep)
314 last_step_was_kept =
true;
317 time_map[current_time].push_back(it);
321 last_step_to_keep == target.
SSA_steps.end() || last_step_was_kept,
322 "last step in SSA trace to keep must not be filtered out as a sync "
323 "instruction, not-taken branch, PHI node, or similar");
328 unsigned step_nr = 0;
330 for(
const auto &time_and_ssa_steps : time_map)
332 for(
const auto ssa_step_it : time_and_ssa_steps.second)
334 const auto &SSA_step = *ssa_step_it;
338 goto_trace_step.
step_nr = ++step_nr;
340 goto_trace_step.
thread_nr = SSA_step.source.thread_nr;
341 goto_trace_step.
pc = SSA_step.source.pc;
342 goto_trace_step.
function_id = SSA_step.source.function_id;
343 if(SSA_step.is_assert())
345 goto_trace_step.
comment = SSA_step.comment;
346 goto_trace_step.
property_id = SSA_step.get_property_id();
348 goto_trace_step.
type = SSA_step.type;
349 goto_trace_step.
hidden = SSA_step.hidden;
351 goto_trace_step.
io_id = SSA_step.io_id;
352 goto_trace_step.
formatted = SSA_step.formatted;
357 arg = decision_procedure.
get(arg);
363 (SSA_step.is_assignment() &&
364 (SSA_step.assignment_type ==
366 SSA_step.assignment_type ==
371 if(SSA_step.original_full_lhs.is_not_nil())
377 SSA_step.original_full_lhs,
378 SSA_step.ssa_full_lhs),
383 if(SSA_step.ssa_full_lhs.is_not_nil())
386 decision_procedure.
get(SSA_step.ssa_full_lhs);
392 for(
const auto &j : SSA_step.converted_io_args)
394 if(j.is_constant() || j.id() == ID_string_constant)
396 goto_trace_step.
io_args.push_back(j);
400 exprt tmp = decision_procedure.
get(j);
401 goto_trace_step.
io_args.push_back(tmp);
405 if(SSA_step.is_assert() || SSA_step.is_assume() || SSA_step.is_goto())
407 goto_trace_step.
cond_expr = SSA_step.cond_expr;
410 decision_procedure.
get(SSA_step.cond_handle).
is_true();
413 if(ssa_step_it == last_step_to_keep)
421 symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep,
426 const auto is_last_step_to_keep =
428 symex_target_equationt::SSA_stepst::const_iterator it,
432 target, is_last_step_to_keep, decision_procedure, ns, goto_trace);
436 symex_target_equationt::SSA_stepst::const_iterator step,
439 return step->is_assert() &&
440 decision_procedure.
get(step->cond_handle).
is_false();