31 const exprt &src_original,
34 if(src_ssa.
id()!=src_original.
id())
48 tmp.
index()=index_value;
53 return std::move(tmp);
58 else if(
id==ID_member)
83 return std::move(tmp2);
85 else if(
id==ID_typecast)
90 return std::move(tmp);
92 else if(
id==ID_byte_extract_little_endian ||
93 id==ID_byte_extract_big_endian)
112 if(expr.
id()==ID_symbol)
116 if(!ns.
lookup(
id, symbol))
144 if(SSA_step.
source.
pc->source_location.as_string().empty())
161 if(SSA_step.
source.
pc->code.get_statement()!=ID_function_call)
177 typedef symex_target_equationt::SSA_stepst::const_iterator ssa_step_iteratort;
178 typedef std::map<mp_integer, std::vector<ssa_step_iteratort>> time_mapt;
183 ssa_step_iteratort last_step_to_keep = target.
SSA_steps.end();
184 bool last_step_was_kept =
false;
189 for(ssa_step_iteratort it = target.
SSA_steps.begin();
194 last_step_to_keep == target.
SSA_steps.end() &&
195 is_last_step_to_keep(it, prop_conv))
197 last_step_to_keep = it;
205 if(it->is_constraint() ||
208 else if(it->is_atomic_begin())
217 else if(it->is_shared_read() || it->is_shared_write() ||
222 if(it->is_shared_read() || it->is_shared_write())
228 const auto cv = numeric_cast<mp_integer>(clock_value);
234 else if(it->is_atomic_end() && current_time<0)
237 INVARIANT(current_time >= 0,
"time keeping inconsistency");
242 time_mapt::const_iterator time_before_steps_it =
243 time_map.find(time_before);
245 if(time_before_steps_it != time_map.end())
247 std::vector<ssa_step_iteratort> ¤t_time_steps =
248 time_map[current_time];
250 current_time_steps.insert(
251 current_time_steps.end(),
252 time_before_steps_it->second.begin(),
253 time_before_steps_it->second.end());
255 time_map.erase(time_before_steps_it);
263 if(it->is_assignment() &&
272 if(it == last_step_to_keep)
274 last_step_was_kept =
true;
277 time_map[current_time].push_back(it);
281 last_step_to_keep == target.
SSA_steps.end() || last_step_was_kept,
282 "last step in SSA trace to keep must not be filtered out as a sync "
283 "instruction, not-taken branch, PHI node, or similar");
288 unsigned step_nr = 0;
290 for(
const auto &time_and_ssa_steps : time_map)
292 for(
const auto ssa_step_it : time_and_ssa_steps.second)
294 const auto &SSA_step = *ssa_step_it;
298 goto_trace_step.
step_nr = ++step_nr;
300 goto_trace_step.
thread_nr = SSA_step.source.thread_nr;
301 goto_trace_step.
pc = SSA_step.source.pc;
302 goto_trace_step.
function = SSA_step.source.function;
303 goto_trace_step.
comment = SSA_step.comment;
304 goto_trace_step.
type = SSA_step.type;
305 goto_trace_step.
hidden = SSA_step.hidden;
307 goto_trace_step.
io_id = SSA_step.io_id;
308 goto_trace_step.
formatted = SSA_step.formatted;
313 arg = prop_conv.
get(arg);
319 (SSA_step.is_assignment() &&
320 (SSA_step.assignment_type ==
322 SSA_step.assignment_type ==
327 if(SSA_step.original_full_lhs.is_not_nil())
330 prop_conv, ns, SSA_step.original_full_lhs, SSA_step.ssa_full_lhs);
333 if(SSA_step.ssa_full_lhs.is_not_nil())
339 for(
const auto &j : SSA_step.converted_io_args)
341 if(j.is_constant() || j.id() == ID_string_constant)
343 goto_trace_step.
io_args.push_back(j);
348 goto_trace_step.
io_args.push_back(tmp);
352 if(SSA_step.is_assert() || SSA_step.is_assume() || SSA_step.is_goto())
354 goto_trace_step.
cond_expr = SSA_step.cond_expr;
360 if(ssa_step_it == last_step_to_keep)
368 symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep,
373 const auto is_last_step_to_keep = [last_step_to_keep](
374 symex_target_equationt::SSA_stepst::const_iterator it,
const prop_convt &) {
375 return last_step_to_keep == it;
379 target, is_last_step_to_keep, prop_conv, ns, goto_trace);
383 symex_target_equationt::SSA_stepst::const_iterator step,
386 return step->is_assert() && prop_conv.
l_get(step->cond_literal).
is_false();