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)
80 else if(tmp.is_false())
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();
const if_exprt & to_if_expr(const exprt &expr)
Cast an 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)
Semantic type conversion.
std::vector< exprt > function_arguments
goto_programt::const_targett pc
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
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
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
bool get_bool(const irep_namet &name) const
goto_programt::const_targett pc
Add constraints to equation encoding partial orders on events.
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.
Expression classes for byte-level operators.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const member_exprt & to_member_expr(const exprt &expr)
Cast an 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()
Get the identifier of the entry point to a goto model.
Single SSA step in the equation.
Base class for all expressions.
const exprt & struct_op() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an 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)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
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 an exprt to an index_exprt.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
bool simplify(exprt &expr, const namespacet &ns)
assignment_typet assignment_type