45 if(expr.
id()==ID_symbol)
51 std::string identifier=
55 if(l0_l1!=std::string::npos)
57 identifier.resize(l0_l1);
64 else if(expr.
id() == ID_string_constant)
85 if(cit !=
cache.end())
90 if(assign.
rhs().
id() == ID_array_list)
93 const auto &ops = array_list.
operands();
95 for(std::size_t listidx = 0; listidx != ops.size(); listidx += 2)
104 else if(assign.
rhs().
id() == ID_array)
118 else if(assign.
rhs().
id()==ID_struct ||
119 assign.
rhs().
id()==ID_union)
124 assign.
lhs().
id() == ID_member &&
132 else if(assign.
lhs().
id()==ID_byte_extract_little_endian ||
133 assign.
lhs().
id()==ID_byte_extract_big_endian)
146 exprt::operandst::const_iterator it=
148 for(
const auto &comp : components)
150 if(comp.type().id()==ID_code ||
151 comp.get_is_padding() ||
157 it != assign.
rhs().
operands().end(),
"expression must have operands");
169 if(assign.
rhs().
id()==ID_union)
173 else if(assign.
rhs().
id() == ID_with)
176 const auto &ops = with_expr.
operands();
178 for(std::size_t i = 1; i < ops.size(); i += 2)
183 if(ops[i].
id() == ID_member_name)
186 assign.
lhs(), ops[i].
get(ID_component_name), ops[i + 1].type()};
208 lhs.find(
"#return_value") != std::string::npos ||
209 (lhs.find(
'$') != std::string::npos &&
210 has_prefix(lhs,
"return_value___VERIFIER_nondet_")))
229 const goto_tracet::stepst::const_iterator &prev_it,
230 goto_tracet::stepst::const_iterator &it)
234 (!it->pc->is_assign() || it->pc->assign_rhs().id() != ID_side_effect ||
235 it->pc->assign_rhs().get(ID_statement) != ID_nondet))
238 if(!it->is_assignment() && !it->is_goto() && !it->is_assert())
245 prev_it != goto_trace.
steps.end() &&
246 prev_it->pc->source_location() == it->pc->source_location())
249 if(it->is_goto() && it->pc->get_condition().is_true())
254 if(source_location.
is_nil() ||
273 expr.
id() == ID_symbol &&
290 unsigned int max_thread_idx = 0;
291 bool trace_has_violation =
false;
292 for(goto_tracet::stepst::const_iterator it = goto_trace.
steps.begin();
293 it != goto_trace.
steps.end();
296 if(it->thread_nr > max_thread_idx)
297 max_thread_idx = it->thread_nr;
298 if(it->is_assert() && !it->cond_value)
299 trace_has_violation =
true;
305 graphml[sink].node_name=
"sink";
306 graphml[sink].is_violation=
false;
307 graphml[sink].has_invariant=
false;
309 if(max_thread_idx > 0 && trace_has_violation)
311 std::vector<graphmlt::node_indext> nodes;
313 for(
unsigned int i = 0; i <= max_thread_idx + 1; ++i)
317 graphml[nodes.back()].is_violation = i == max_thread_idx + 1;
318 graphml[nodes.back()].has_invariant =
false;
321 for(
auto it = nodes.cbegin(); std::next(it) != nodes.cend(); ++it)
326 const auto thread_id = std::distance(nodes.cbegin(), it);
328 data.set_attribute(
"key",
"createThread");
333 data.set_attribute(
"key",
"enterFunction");
336 graphml[*std::next(it)].
in[*it].xml_node = edge;
337 graphml[*it].
out[*std::next(it)].xml_node = edge;
346 std::vector<std::size_t> step_to_node(goto_trace.
steps.size()+1, 0);
348 goto_tracet::stepst::const_iterator prev_it=goto_trace.
steps.end();
349 for(goto_tracet::stepst::const_iterator
350 it=goto_trace.
steps.begin();
351 it!=goto_trace.
steps.end();
356 step_to_node[it->step_nr]=sink;
362 goto_tracet::stepst::const_iterator next=it;
365 next != goto_trace.
steps.end() &&
367 it->full_lhs == next->full_lhs &&
368 it->pc->source_location() == next->pc->source_location())
370 step_to_node[it->step_nr]=sink;
386 graphml[node].has_invariant=
false;
388 step_to_node[it->step_nr]=node;
394 for(goto_tracet::stepst::const_iterator
395 it=goto_trace.
steps.begin();
396 it!=goto_trace.
steps.end();
399 const std::size_t from=step_to_node[it->step_nr];
402 if(from == sink ||
graphml[from].is_violation)
408 auto next = std::next(it);
409 for(; next != goto_trace.
steps.end() &&
410 (step_to_node[next->step_nr] == sink ||
416 const std::size_t to=
417 next==goto_trace.
steps.end()?
418 sink:step_to_node[next->step_nr];
429 {{
"source",
graphml[from].node_name},
430 {
"target",
graphml[to].node_name}},
447 const auto lhs_object = it->get_lhs_object();
450 lhs_object.has_value())
452 const std::string &lhs_id =
id2string(lhs_object->get_identifier());
453 if(lhs_id.find(
"pthread_create::thread") != std::string::npos)
464 lhs_id.find(
"thread") == std::string::npos &&
465 lhs_id.find(
"mutex") == std::string::npos &&
466 (!it->full_lhs_value.is_constant() ||
467 !it->full_lhs_value.has_operands() ||
481 irep_idt function_id = it->function_id;
482 const symbolt *symbol_ptr =
nullptr;
485 function_id = lhs_id.substr(0, lhs_id.find(
"::"));
536 graphml[sink].node_name=
"sink";
537 graphml[sink].is_violation=
false;
538 graphml[sink].has_invariant=
false;
541 std::vector<std::size_t> step_to_node(equation.
SSA_steps.size()+1, 0);
543 std::size_t step_nr=1;
544 for(symex_target_equationt::SSA_stepst::const_iterator
553 (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
554 (it->is_goto() && it->source.pc->get_condition().is_true()) ||
558 step_to_node[step_nr]=sink;
564 symex_target_equationt::SSA_stepst::const_iterator next=it;
567 next != equation.
SSA_steps.end() && next->is_assignment() &&
568 it->ssa_full_lhs == next->ssa_full_lhs &&
569 it->source.pc->source_location() == next->source.pc->source_location())
571 step_to_node[step_nr]=sink;
582 graphml[node].is_violation=
false;
583 graphml[node].has_invariant=
false;
585 step_to_node[step_nr]=node;
590 for(symex_target_equationt::SSA_stepst::const_iterator
595 const std::size_t from=step_to_node[step_nr];
604 symex_target_equationt::SSA_stepst::const_iterator next=it;
605 std::size_t next_step_nr=step_nr;
606 for(++next, ++next_step_nr;
608 (step_to_node[next_step_nr]==sink || it->source.pc==next->source.pc);
609 ++next, ++next_step_nr)
613 const std::size_t to=
615 sink:step_to_node[next_step_nr];
626 {{
"source",
graphml[from].node_name},
627 {
"target",
graphml[to].node_name}},
641 (it->is_assignment() || it->is_decl()) && it->ssa_rhs.is_not_nil() &&
642 it->ssa_full_lhs.is_not_nil())
644 irep_idt identifier = it->ssa_lhs.get_object_name();
646 graphml[to].has_invariant =
true;
678 step_nr=next_step_nr;
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
unsignedbv_typet size_type()
bitvector_typet c_index_type()
Array constructor from a list of index-element pairs Operands are index/value pairs,...
const typet & element_type() const
The type of the elements of the array.
A codet representing an assignment in the program.
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.
void operator()(const goto_tracet &goto_trace)
counterexample witness
std::unordered_map< std::pair< unsigned int, const irept::dt * >, std::string, pair_hash< unsigned int, const irept::dt * > > cache
void remove_l0_l1(exprt &expr)
std::string convert_assign_rec(const irep_idt &identifier, const code_assignt &assign)
nodet::node_indext node_indext
const edgest & out(node_indext n) const
node_indext add_node(arguments &&... values)
const edgest & in(node_indext n) const
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
Extract member of struct or union.
const exprt & struct_op() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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().
const irep_idt & get_function() const
const irep_idt & get_file() const
const irep_idt & get_line() const
static bool is_built_in(const std::string &s)
const exprt & get_original_expr() const
array_exprt to_array_expr() const
convert string into array constant
Base type for structs and unions.
const componentst & components() const
std::vector< componentt > componentst
void set_identifier(const irep_idt &identifier)
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Operator to update elements in structs and arrays.
xmlt & new_element(const std::string &key)
void set_attribute(const std::string &attribute, unsigned value)
static bool is_printable_xml(const std::string &s)
Determine whether s does not contain any characters that cannot be escaped in XML 1....
bool has_prefix(const std::string &s, const std::string &prefix)
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
static std::string expr_to_string(const namespacet &ns, const irep_idt &id, const exprt &expr)
static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
static bool filter_out(const goto_tracet &goto_trace, const goto_tracet::stepst::const_iterator &prev_it, goto_tracet::stepst::const_iterator &it)
Witnesses for Traces and Proofs.
const std::string & id2string(const irep_idt &d)
const std::string thread_id
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const irep_idt & get_mode_from_identifier(const namespacet &ns, const irep_idt &identifier)
Get the mode of the given identifier's symbol.
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
bool is_ssa_expr(const exprt &expr)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
const array_list_exprt & to_array_list_expr(const exprt &expr)
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const string_constantt & to_string_constant(const exprt &expr)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
string_containert & get_string_container()
Get a reference to the global string container.
static expr2c_configurationt clean_configuration
This prints compilable C that loses some of the internal details of the GOTO program.
Functor to check whether iterators from different collections point at the same object.
Generate Equation using Symbolic Execution.