cprover
graphml_witness.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Witnesses for Traces and Proofs
4 
5 Author: Daniel Kroening
6 
7 \*******************************************************************/
8 
11 
12 #include "graphml_witness.h"
13 
14 #include <util/base_type.h>
15 #include <util/byte_operators.h>
16 #include <util/c_types.h>
17 #include <util/arith_tools.h>
18 #include <util/prefix.h>
19 #include <util/ssa_expr.h>
20 
22 {
23  if(expr.id()==ID_symbol)
24  {
25  if(is_ssa_expr(expr))
26  expr=to_ssa_expr(expr).get_original_expr();
27  else
28  {
29  std::string identifier=
30  id2string(to_symbol_expr(expr).get_identifier());
31 
32  std::string::size_type l0_l1=identifier.find_first_of("!@");
33  if(l0_l1!=std::string::npos)
34  {
35  identifier.resize(l0_l1);
36  to_symbol_expr(expr).set_identifier(identifier);
37  }
38  }
39 
40  return;
41  }
42 
43  Forall_operands(it, expr)
44  remove_l0_l1(*it);
45 }
46 
48  const irep_idt &identifier,
49  const code_assignt &assign)
50 {
51  std::string result;
52 
53  if(assign.rhs().id()==ID_array)
54  {
55  const array_typet &type=
56  to_array_type(ns.follow(assign.rhs().type()));
57 
58  unsigned i=0;
59  forall_operands(it, assign.rhs())
60  {
61  index_exprt index(
62  assign.lhs(),
63  from_integer(i++, index_type()),
64  type.subtype());
65  if(!result.empty())
66  result+=' ';
67  result+=convert_assign_rec(identifier, code_assignt(index, *it));
68  }
69  }
70  else if(assign.rhs().id()==ID_struct ||
71  assign.rhs().id()==ID_union)
72  {
73  // dereferencing may have resulted in an lhs that is the first
74  // struct member; undo this
75  if(assign.lhs().id()==ID_member &&
76  !base_type_eq(assign.lhs().type(), assign.rhs().type(), ns))
77  {
78  code_assignt tmp=assign;
79  tmp.lhs()=to_member_expr(assign.lhs()).struct_op();
80 
81  return convert_assign_rec(identifier, tmp);
82  }
83  else if(assign.lhs().id()==ID_byte_extract_little_endian ||
84  assign.lhs().id()==ID_byte_extract_big_endian)
85  {
86  code_assignt tmp=assign;
87  tmp.lhs()=to_byte_extract_expr(assign.lhs()).op();
88 
89  return convert_assign_rec(identifier, tmp);
90  }
91 
92  const struct_union_typet &type=
93  to_struct_union_type(ns.follow(assign.lhs().type()));
94  const struct_union_typet::componentst &components=
95  type.components();
96 
97  exprt::operandst::const_iterator it=
98  assign.rhs().operands().begin();
99  for(const auto &comp : components)
100  {
101  if(comp.type().id()==ID_code ||
102  comp.get_is_padding() ||
103  // for some reason #is_padding gets lost in *some* cases
104  has_prefix(id2string(comp.get_name()), "$pad"))
105  continue;
106 
107  assert(it!=assign.rhs().operands().end());
108 
109  member_exprt member(
110  assign.lhs(),
111  comp.get_name(),
112  it->type());
113  if(!result.empty())
114  result+=' ';
115  result+=convert_assign_rec(identifier, code_assignt(member, *it));
116  ++it;
117 
118  // for unions just assign to the first member
119  if(assign.rhs().id()==ID_union)
120  break;
121  }
122  }
123  else
124  {
125  exprt clean_rhs=assign.rhs();
126  remove_l0_l1(clean_rhs);
127 
128  std::string lhs=from_expr(ns, identifier, assign.lhs());
129  if(lhs.find('$')!=std::string::npos)
130  lhs="\\result";
131 
132  result=lhs+" = "+from_expr(ns, identifier, clean_rhs)+";";
133  }
134 
135  return result;
136 }
137 
138 static bool filter_out(
139  const goto_tracet &goto_trace,
140  const goto_tracet::stepst::const_iterator &prev_it,
141  goto_tracet::stepst::const_iterator &it)
142 {
143  if(it->hidden &&
144  (!it->is_assignment() ||
145  to_code_assign(it->pc->code).rhs().id()!=ID_side_effect ||
146  to_code_assign(it->pc->code).rhs().get(ID_statement)!=ID_nondet))
147  return true;
148 
149  if(!it->is_assignment() && !it->is_goto() && !it->is_assert())
150  return true;
151 
152  // we filter out steps with the same source location
153  // TODO: if these are assignments we should accumulate them into
154  // a single edge
155  if(prev_it!=goto_trace.steps.end() &&
156  prev_it->pc->source_location==it->pc->source_location)
157  return true;
158 
159  if(it->is_goto() && it->pc->guard.is_true())
160  return true;
161 
162  const source_locationt &source_location=it->pc->source_location;
163 
164  if(source_location.is_nil() ||
165  source_location.get_file().empty() ||
166  source_location.is_built_in() ||
167  source_location.get_line().empty())
168  return true;
169 
170  return false;
171 }
172 
175 {
176  graphml.key_values["sourcecodelang"]="C";
177 
179  graphml[sink].node_name="sink";
180  graphml[sink].thread_nr=0;
181  graphml[sink].is_violation=false;
182  graphml[sink].has_invariant=false;
183 
184  // step numbers start at 1
185  std::vector<std::size_t> step_to_node(goto_trace.steps.size()+1, 0);
186 
187  goto_tracet::stepst::const_iterator prev_it=goto_trace.steps.end();
188  for(goto_tracet::stepst::const_iterator
189  it=goto_trace.steps.begin();
190  it!=goto_trace.steps.end();
191  it++) // we cannot replace this by a ranged for
192  {
193  if(filter_out(goto_trace, prev_it, it))
194  {
195  step_to_node[it->step_nr]=sink;
196 
197  continue;
198  }
199 
200  // skip declarations followed by an immediate assignment
201  goto_tracet::stepst::const_iterator next=it;
202  ++next;
203  if(next!=goto_trace.steps.end() &&
205  it->full_lhs==next->full_lhs &&
206  it->pc->source_location==next->pc->source_location)
207  {
208  step_to_node[it->step_nr]=sink;
209 
210  continue;
211  }
212 
213  prev_it=it;
214 
215  const source_locationt &source_location=it->pc->source_location;
216 
218  graphml[node].node_name=
219  std::to_string(it->pc->location_number)+"."+std::to_string(it->step_nr);
220  graphml[node].file=source_location.get_file();
221  graphml[node].line=source_location.get_line();
222  graphml[node].thread_nr=it->thread_nr;
223  graphml[node].is_violation=
224  it->type==goto_trace_stept::typet::ASSERT && !it->cond_value;
225  graphml[node].has_invariant=false;
226 
227  step_to_node[it->step_nr]=node;
228  }
229 
230  // build edges
231  for(goto_tracet::stepst::const_iterator
232  it=goto_trace.steps.begin();
233  it!=goto_trace.steps.end();
234  ) // no ++it
235  {
236  const std::size_t from=step_to_node[it->step_nr];
237 
238  if(from==sink)
239  {
240  ++it;
241  continue;
242  }
243 
244  goto_tracet::stepst::const_iterator next=it;
245  for(++next;
246  next!=goto_trace.steps.end() &&
247  (step_to_node[next->step_nr]==sink || it->pc==next->pc);
248  ++next)
249  {
250  // advance
251  }
252  const std::size_t to=
253  next==goto_trace.steps.end()?
254  sink:step_to_node[next->step_nr];
255 
256  switch(it->type)
257  {
261  {
262  xmlt edge("edge");
263  edge.set_attribute("source", graphml[from].node_name);
264  edge.set_attribute("target", graphml[to].node_name);
265 
266  {
267  xmlt &data_f=edge.new_element("data");
268  data_f.set_attribute("key", "originfile");
269  data_f.data=id2string(graphml[from].file);
270 
271  xmlt &data_l=edge.new_element("data");
272  data_l.set_attribute("key", "startline");
273  data_l.data=id2string(graphml[from].line);
274  }
275 
277  it->lhs_object_value.is_not_nil() &&
278  it->full_lhs.is_not_nil())
279  {
280  if(!it->lhs_object_value.is_constant() ||
281  !it->lhs_object_value.has_operands() ||
282  !has_prefix(id2string(it->lhs_object_value.op0().get(ID_value)),
283  "INVALID-"))
284  {
285  xmlt &val=edge.new_element("data");
286  val.set_attribute("key", "assumption");
287  code_assignt assign(it->lhs_object, it->lhs_object_value);
288  irep_idt identifier=it->lhs_object.get_identifier();
289  val.data=convert_assign_rec(identifier, assign);
290 
291  xmlt &val_s=edge.new_element("data");
292  val_s.set_attribute("key", "assumption.scope");
293  val_s.data=id2string(it->pc->source_location.get_function());
294  }
295  }
296  else if(it->type==goto_trace_stept::typet::GOTO &&
297  it->pc->is_goto())
298  {
299  xmlt &val=edge.new_element("data");
300  val.set_attribute("key", "sourcecode");
301  const std::string cond=from_expr(ns, "", it->cond_expr);
302  const std::string neg_cond=
303  from_expr(ns, "", not_exprt(it->cond_expr));
304  val.data="["+(it->cond_value ? cond : neg_cond)+"]";
305 
306  #if 0
307  xmlt edge2("edge");
308  edge2.set_attribute("source", graphml[from].node_name);
309  edge2.set_attribute("target", graphml[sink].node_name);
310 
311  xmlt &data_f2=edge2.new_element("data");
312  data_f2.set_attribute("key", "originfile");
313  data_f2.data=id2string(graphml[from].file);
314 
315  xmlt &data_l2=edge2.new_element("data");
316  data_l2.set_attribute("key", "startline");
317  data_l2.data=id2string(graphml[from].line);
318 
319  xmlt &val2=edge2.new_element("data");
320  val2.set_attribute("key", "sourcecode");
321  val2.data="["+(it->cond_value ? neg_cond : cond)+"]";
322 
323  graphml[sink].in[from].xml_node=edge2;
324  graphml[from].out[sink].xml_node=edge2;
325  #endif
326  }
327 
328  graphml[to].in[from].xml_node=edge;
329  graphml[from].out[to].xml_node=edge;
330  }
331  break;
332 
349  // ignore
350  break;
351  }
352 
353  it=next;
354  }
355 }
356 
359 {
360  graphml.key_values["sourcecodelang"]="C";
361 
363  graphml[sink].node_name="sink";
364  graphml[sink].thread_nr=0;
365  graphml[sink].is_violation=false;
366  graphml[sink].has_invariant=false;
367 
368  // step numbers start at 1
369  std::vector<std::size_t> step_to_node(equation.SSA_steps.size()+1, 0);
370 
371  std::size_t step_nr=1;
372  for(symex_target_equationt::SSA_stepst::const_iterator
373  it=equation.SSA_steps.begin();
374  it!=equation.SSA_steps.end();
375  it++, step_nr++) // we cannot replace this by a ranged for
376  {
377  const source_locationt &source_location=it->source.pc->source_location;
378 
379  if(it->hidden ||
380  (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
381  (it->is_goto() && it->source.pc->guard.is_true()) ||
382  source_location.is_nil() ||
383  source_location.is_built_in() ||
384  source_location.get_line().empty())
385  {
386  step_to_node[step_nr]=sink;
387 
388  continue;
389  }
390 
391  // skip declarations followed by an immediate assignment
392  symex_target_equationt::SSA_stepst::const_iterator next=it;
393  ++next;
394  if(next!=equation.SSA_steps.end() &&
395  next->is_assignment() &&
396  it->ssa_full_lhs==next->ssa_full_lhs &&
397  it->source.pc->source_location==next->source.pc->source_location)
398  {
399  step_to_node[step_nr]=sink;
400 
401  continue;
402  }
403 
405  graphml[node].node_name=
406  std::to_string(it->source.pc->location_number)+"."+
407  std::to_string(step_nr);
408  graphml[node].file=source_location.get_file();
409  graphml[node].line=source_location.get_line();
410  graphml[node].thread_nr=it->source.thread_nr;
411  graphml[node].is_violation=false;
412  graphml[node].has_invariant=false;
413 
414  step_to_node[step_nr]=node;
415  }
416 
417  // build edges
418  step_nr=1;
419  for(symex_target_equationt::SSA_stepst::const_iterator
420  it=equation.SSA_steps.begin();
421  it!=equation.SSA_steps.end();
422  ) // no ++it
423  {
424  const std::size_t from=step_to_node[step_nr];
425 
426  if(from==sink)
427  {
428  ++it;
429  ++step_nr;
430  continue;
431  }
432 
433  symex_target_equationt::SSA_stepst::const_iterator next=it;
434  std::size_t next_step_nr=step_nr;
435  for(++next, ++next_step_nr;
436  next!=equation.SSA_steps.end() &&
437  (step_to_node[next_step_nr]==sink || it->source.pc==next->source.pc);
438  ++next, ++next_step_nr)
439  {
440  // advance
441  }
442  const std::size_t to=
443  next==equation.SSA_steps.end()?
444  sink:step_to_node[next_step_nr];
445 
446  switch(it->type)
447  {
451  {
452  xmlt edge("edge");
453  edge.set_attribute("source", graphml[from].node_name);
454  edge.set_attribute("target", graphml[to].node_name);
455 
456  {
457  xmlt &data_f=edge.new_element("data");
458  data_f.set_attribute("key", "originfile");
459  data_f.data=id2string(graphml[from].file);
460 
461  xmlt &data_l=edge.new_element("data");
462  data_l.set_attribute("key", "startline");
463  data_l.data=id2string(graphml[from].line);
464  }
465 
466  if((it->is_assignment() ||
467  it->is_decl()) &&
468  it->ssa_rhs.is_not_nil() &&
469  it->ssa_full_lhs.is_not_nil())
470  {
471  irep_idt identifier=it->ssa_lhs.get_object_name();
472 
473  graphml[to].has_invariant=true;
474  code_assignt assign(it->ssa_full_lhs, it->ssa_rhs);
475  graphml[to].invariant=convert_assign_rec(identifier, assign);
476  graphml[to].invariant_scope=
477  id2string(it->source.pc->source_location.get_function());
478  }
479  else if(it->is_goto() &&
480  it->source.pc->is_goto())
481  {
482  xmlt &val=edge.new_element("data");
483  val.set_attribute("key", "sourcecode");
484  const std::string cond=from_expr(ns, "", it->cond_expr);
485  from_expr(ns, "", not_exprt(it->cond_expr));
486  val.data="["+cond+"]";
487  }
488 
489  graphml[to].in[from].xml_node=edge;
490  graphml[from].out[to].xml_node=edge;
491  }
492  break;
493 
510  // ignore
511  break;
512  }
513 
514  it=next;
515  step_nr=next_step_nr;
516  }
517 }
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
Boolean negation.
Definition: std_expr.h:2648
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::string convert_assign_rec(const irep_idt &identifier, const code_assignt &assign)
const namespacet & ns
static bool is_built_in(const std::string &s)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< componentt > componentst
Definition: std_types.h:240
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
const componentst & components() const
Definition: std_types.h:242
typet & type()
Definition: expr.h:60
unsignedbv_typet size_type()
Definition: c_types.cpp:57
stepst steps
Definition: goto_trace.h:150
Extract member of struct or union.
Definition: std_expr.h:3214
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:277
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
exprt & lhs()
Definition: std_code.h:157
Expression classes for byte-level operators.
const irep_idt & get_line() const
void remove_l0_l1(exprt &expr)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:150
exprt & rhs()
Definition: std_code.h:162
const edgest & out(node_indext n) const
Definition: graph.h:192
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
Definition: xml.h:18
#define forall_operands(it, expr)
Definition: expr.h:17
nodet::node_indext node_indext
Definition: graph.h:139
std::string data
Definition: xml.h:30
bitvector_typet index_type()
Definition: c_types.cpp:15
xmlt & new_element(const std::string &name)
Definition: xml.h:86
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const irep_idt & get_file() const
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:159
node_indext add_node()
Definition: graph.h:145
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:169
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:115
const edgest & in(node_indext n) const
Definition: graph.h:187
#define Forall_operands(it, expr)
Definition: expr.h:23
key_valuest key_values
Definition: graphml.h:67
arrays with given size
Definition: std_types.h:901
void operator()(const goto_tracet &goto_trace)
counterexample witness
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146
static bool filter_out(const goto_tracet &goto_trace, const goto_tracet::stepst::const_iterator &prev_it, goto_tracet::stepst::const_iterator &it)
Base Type Computation.
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bool empty() const
Definition: dstring.h:61
Assignment.
Definition: std_code.h:144
Witnesses for Traces and Proofs.
array index operator
Definition: std_expr.h:1170
Definition: kdev_t.h:19