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