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  INVARIANT(
112  it != assign.rhs().operands().end(), "expression must have operands");
113 
114  member_exprt member(
115  assign.lhs(),
116  comp.get_name(),
117  it->type());
118  if(!result.empty())
119  result+=' ';
120  result+=convert_assign_rec(identifier, code_assignt(member, *it));
121  ++it;
122 
123  // for unions just assign to the first member
124  if(assign.rhs().id()==ID_union)
125  break;
126  }
127  }
128  else
129  {
130  exprt clean_rhs=assign.rhs();
131  remove_l0_l1(clean_rhs);
132 
133  std::string lhs=from_expr(ns, identifier, assign.lhs());
134  if(lhs.find('$')!=std::string::npos)
135  lhs="\\result";
136 
137  result=lhs+" = "+from_expr(ns, identifier, clean_rhs)+";";
138  }
139 
140  return result;
141 }
142 
143 static bool filter_out(
144  const goto_tracet &goto_trace,
145  const goto_tracet::stepst::const_iterator &prev_it,
146  goto_tracet::stepst::const_iterator &it)
147 {
148  if(it->hidden &&
149  (!it->pc->is_assign() ||
150  to_code_assign(it->pc->code).rhs().id()!=ID_side_effect ||
151  to_code_assign(it->pc->code).rhs().get(ID_statement)!=ID_nondet))
152  return true;
153 
154  if(!it->is_assignment() && !it->is_goto() && !it->is_assert())
155  return true;
156 
157  // we filter out steps with the same source location
158  // TODO: if these are assignments we should accumulate them into
159  // a single edge
160  if(prev_it!=goto_trace.steps.end() &&
161  prev_it->pc->source_location==it->pc->source_location)
162  return true;
163 
164  if(it->is_goto() && it->pc->guard.is_true())
165  return true;
166 
167  const source_locationt &source_location=it->pc->source_location;
168 
169  if(source_location.is_nil() ||
170  source_location.get_file().empty() ||
171  source_location.is_built_in() ||
172  source_location.get_line().empty())
173  return true;
174 
175  return false;
176 }
177 
180 {
181  graphml.key_values["sourcecodelang"]="C";
182 
184  graphml[sink].node_name="sink";
185  graphml[sink].thread_nr=0;
186  graphml[sink].is_violation=false;
187  graphml[sink].has_invariant=false;
188 
189  // step numbers start at 1
190  std::vector<std::size_t> step_to_node(goto_trace.steps.size()+1, 0);
191 
192  goto_tracet::stepst::const_iterator prev_it=goto_trace.steps.end();
193  for(goto_tracet::stepst::const_iterator
194  it=goto_trace.steps.begin();
195  it!=goto_trace.steps.end();
196  it++) // we cannot replace this by a ranged for
197  {
198  if(filter_out(goto_trace, prev_it, it))
199  {
200  step_to_node[it->step_nr]=sink;
201 
202  continue;
203  }
204 
205  // skip declarations followed by an immediate assignment
206  goto_tracet::stepst::const_iterator next=it;
207  ++next;
208  if(next!=goto_trace.steps.end() &&
210  it->full_lhs==next->full_lhs &&
211  it->pc->source_location==next->pc->source_location)
212  {
213  step_to_node[it->step_nr]=sink;
214 
215  continue;
216  }
217 
218  prev_it=it;
219 
220  const source_locationt &source_location=it->pc->source_location;
221 
223  graphml[node].node_name=
224  std::to_string(it->pc->location_number)+"."+std::to_string(it->step_nr);
225  graphml[node].file=source_location.get_file();
226  graphml[node].line=source_location.get_line();
227  graphml[node].thread_nr=it->thread_nr;
228  graphml[node].is_violation=
229  it->type==goto_trace_stept::typet::ASSERT && !it->cond_value;
230  graphml[node].has_invariant=false;
231 
232  step_to_node[it->step_nr]=node;
233  }
234 
235  // build edges
236  for(goto_tracet::stepst::const_iterator
237  it=goto_trace.steps.begin();
238  it!=goto_trace.steps.end();
239  ) // no ++it
240  {
241  const std::size_t from=step_to_node[it->step_nr];
242 
243  if(from==sink)
244  {
245  ++it;
246  continue;
247  }
248 
249  auto next = std::next(it);
250  for(; next != goto_trace.steps.end() &&
251  (step_to_node[next->step_nr] == sink ||
252  pointee_address_equalt{}(it->pc, next->pc)); // NOLINT
253  ++next)
254  {
255  // advance
256  }
257  const std::size_t to=
258  next==goto_trace.steps.end()?
259  sink:step_to_node[next->step_nr];
260 
261  switch(it->type)
262  {
266  {
267  xmlt edge("edge");
268  edge.set_attribute("source", graphml[from].node_name);
269  edge.set_attribute("target", graphml[to].node_name);
270 
271  {
272  xmlt &data_f=edge.new_element("data");
273  data_f.set_attribute("key", "originfile");
274  data_f.data=id2string(graphml[from].file);
275 
276  xmlt &data_l=edge.new_element("data");
277  data_l.set_attribute("key", "startline");
278  data_l.data=id2string(graphml[from].line);
279  }
280 
282  it->full_lhs_value.is_not_nil() &&
283  it->full_lhs.is_not_nil())
284  {
285  xmlt &val=edge.new_element("data");
286  val.set_attribute("key", "assumption");
287  val.data = from_expr(ns, it->function, it->full_lhs) + " = " +
288  from_expr(ns, it->function, it->full_lhs_value) + ";";
289 
290  xmlt &val_s=edge.new_element("data");
291  val_s.set_attribute("key", "assumption.scope");
292  val_s.data=id2string(it->pc->source_location.get_function());
293  }
294  else if(it->type==goto_trace_stept::typet::GOTO &&
295  it->pc->is_goto())
296  {
297  xmlt &val=edge.new_element("data");
298  val.set_attribute("key", "sourcecode");
299  const std::string cond = from_expr(ns, it->function, it->cond_expr);
300  const std::string neg_cond =
301  from_expr(ns, it->function, not_exprt(it->cond_expr));
302  val.data="["+(it->cond_value ? cond : neg_cond)+"]";
303 
304  #if 0
305  xmlt edge2("edge");
306  edge2.set_attribute("source", graphml[from].node_name);
307  edge2.set_attribute("target", graphml[sink].node_name);
308 
309  xmlt &data_f2=edge2.new_element("data");
310  data_f2.set_attribute("key", "originfile");
311  data_f2.data=id2string(graphml[from].file);
312 
313  xmlt &data_l2=edge2.new_element("data");
314  data_l2.set_attribute("key", "startline");
315  data_l2.data=id2string(graphml[from].line);
316 
317  xmlt &val2=edge2.new_element("data");
318  val2.set_attribute("key", "sourcecode");
319  val2.data="["+(it->cond_value ? neg_cond : cond)+"]";
320 
321  graphml[sink].in[from].xml_node=edge2;
322  graphml[from].out[sink].xml_node=edge2;
323  #endif
324  }
325 
326  graphml[to].in[from].xml_node=edge;
327  graphml[from].out[to].xml_node=edge;
328  }
329  break;
330 
347  // ignore
348  break;
349  }
350 
351  it=next;
352  }
353 }
354 
357 {
358  graphml.key_values["sourcecodelang"]="C";
359 
361  graphml[sink].node_name="sink";
362  graphml[sink].thread_nr=0;
363  graphml[sink].is_violation=false;
364  graphml[sink].has_invariant=false;
365 
366  // step numbers start at 1
367  std::vector<std::size_t> step_to_node(equation.SSA_steps.size()+1, 0);
368 
369  std::size_t step_nr=1;
370  for(symex_target_equationt::SSA_stepst::const_iterator
371  it=equation.SSA_steps.begin();
372  it!=equation.SSA_steps.end();
373  it++, step_nr++) // we cannot replace this by a ranged for
374  {
375  const source_locationt &source_location=it->source.pc->source_location;
376 
377  if(it->hidden ||
378  (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
379  (it->is_goto() && it->source.pc->guard.is_true()) ||
380  source_location.is_nil() ||
381  source_location.is_built_in() ||
382  source_location.get_line().empty())
383  {
384  step_to_node[step_nr]=sink;
385 
386  continue;
387  }
388 
389  // skip declarations followed by an immediate assignment
390  symex_target_equationt::SSA_stepst::const_iterator next=it;
391  ++next;
392  if(next!=equation.SSA_steps.end() &&
393  next->is_assignment() &&
394  it->ssa_full_lhs==next->ssa_full_lhs &&
395  it->source.pc->source_location==next->source.pc->source_location)
396  {
397  step_to_node[step_nr]=sink;
398 
399  continue;
400  }
401 
403  graphml[node].node_name=
404  std::to_string(it->source.pc->location_number)+"."+
405  std::to_string(step_nr);
406  graphml[node].file=source_location.get_file();
407  graphml[node].line=source_location.get_line();
408  graphml[node].thread_nr=it->source.thread_nr;
409  graphml[node].is_violation=false;
410  graphml[node].has_invariant=false;
411 
412  step_to_node[step_nr]=node;
413  }
414 
415  // build edges
416  step_nr=1;
417  for(symex_target_equationt::SSA_stepst::const_iterator
418  it=equation.SSA_steps.begin();
419  it!=equation.SSA_steps.end();
420  ) // no ++it
421  {
422  const std::size_t from=step_to_node[step_nr];
423 
424  if(from==sink)
425  {
426  ++it;
427  ++step_nr;
428  continue;
429  }
430 
431  symex_target_equationt::SSA_stepst::const_iterator next=it;
432  std::size_t next_step_nr=step_nr;
433  for(++next, ++next_step_nr;
434  next!=equation.SSA_steps.end() &&
435  (step_to_node[next_step_nr]==sink || it->source.pc==next->source.pc);
436  ++next, ++next_step_nr)
437  {
438  // advance
439  }
440  const std::size_t to=
441  next==equation.SSA_steps.end()?
442  sink:step_to_node[next_step_nr];
443 
444  switch(it->type)
445  {
449  {
450  xmlt edge("edge");
451  edge.set_attribute("source", graphml[from].node_name);
452  edge.set_attribute("target", graphml[to].node_name);
453 
454  {
455  xmlt &data_f=edge.new_element("data");
456  data_f.set_attribute("key", "originfile");
457  data_f.data=id2string(graphml[from].file);
458 
459  xmlt &data_l=edge.new_element("data");
460  data_l.set_attribute("key", "startline");
461  data_l.data=id2string(graphml[from].line);
462  }
463 
464  if((it->is_assignment() ||
465  it->is_decl()) &&
466  it->ssa_rhs.is_not_nil() &&
467  it->ssa_full_lhs.is_not_nil())
468  {
469  irep_idt identifier=it->ssa_lhs.get_object_name();
470 
471  graphml[to].has_invariant=true;
472  code_assignt assign(it->ssa_full_lhs, it->ssa_rhs);
473  graphml[to].invariant=convert_assign_rec(identifier, assign);
474  graphml[to].invariant_scope=
475  id2string(it->source.pc->source_location.get_function());
476  }
477  else if(it->is_goto() &&
478  it->source.pc->is_goto())
479  {
480  xmlt &val=edge.new_element("data");
481  val.set_attribute("key", "sourcecode");
482  const std::string cond =
483  from_expr(ns, it->source.function, it->cond_expr);
484  val.data="["+cond+"]";
485  }
486 
487  graphml[to].in[from].xml_node=edge;
488  graphml[from].out[to].xml_node=edge;
489  }
490  break;
491 
508  // ignore
509  break;
510  }
511 
512  it=next;
513  step_nr=next_step_nr;
514  }
515 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
goto_trace_stept::typet::LOCATION
@ LOCATION
typet::subtype
const typet & subtype() const
Definition: type.h:38
goto_trace_stept::typet::ASSUME
@ ASSUME
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:26
graphmlt::key_values
key_valuest key_values
Definition: graphml.h:66
arith_tools.h
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:260
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:274
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:53
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:114
grapht::add_node
node_indext add_node()
Definition: graph.h:180
prefix.h
file
Definition: kdev_t.h:19
goto_tracet::steps
stepst steps
Definition: goto_trace.h:154
exprt
Base class for all expressions.
Definition: expr.h:54
pointee_address_equalt
Functor to check whether iterators from different collections point at the same object.
Definition: goto_program.h:795
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:203
graphml_witnesst::remove_l0_l1
void remove_l0_l1(exprt &expr)
Definition: graphml_witness.cpp:25
source_locationt::is_built_in
static bool is_built_in(const std::string &s)
Definition: source_location.h:168
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
source_locationt::get_line
const irep_idt & get_line() const
Definition: source_location.h:47
grapht< xml_graph_nodet >::node_indext
nodet::node_indext node_indext
Definition: graph.h:174
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
grapht::in
const edgest & in(node_indext n) const
Definition: graph.h:222
byte_operators.h
Expression classes for byte-level operators.
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:179
goto_trace_stept::typet::OUTPUT
@ OUTPUT
goto_trace_stept::typet::FUNCTION_RETURN
@ FUNCTION_RETURN
filter_out
static bool filter_out(const goto_tracet &goto_trace, const goto_tracet::stepst::const_iterator &prev_it, goto_tracet::stepst::const_iterator &it)
Definition: graphml_witness.cpp:143
base_type.h
goto_trace_stept::typet::DECL
@ DECL
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:160
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_trace_stept::typet::ASSERT
@ ASSERT
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:46
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
language_util.h
goto_trace_stept::typet::NONE
@ NONE
base_type_eq
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3931
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:269
goto_trace_stept::typet::ASSIGNMENT
@ ASSIGNMENT
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
graphml_witnesst::graphml
graphmlt graphml
Definition: graphml_witness.h:39
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
dstringt::empty
bool empty() const
Definition: dstring.h:75
goto_trace_stept::typet::INPUT
@ INPUT
goto_trace_stept::typet::ATOMIC_END
@ ATOMIC_END
graphml_witness.h
xmlt
Definition: xml.h:18
goto_trace_stept::typet::SPAWN
@ SPAWN
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:35
goto_program.h
source_locationt
Definition: source_location.h:20
goto_trace_stept::typet::MEMORY_BARRIER
@ MEMORY_BARRIER
goto_trace_stept::typet::SHARED_WRITE
@ SHARED_WRITE
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3890
grapht::out
const edgest & out(node_indext n) const
Definition: graph.h:227
ssa_expr.h
goto_trace_stept::typet::GOTO
@ GOTO
graphml_witnesst::operator()
void operator()(const goto_tracet &goto_trace)
counterexample witness
Definition: graphml_witness.cpp:179
array_typet
Arrays with given size.
Definition: std_types.h:1000
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:175
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:369
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
goto_trace_stept::typet::ATOMIC_BEGIN
@ ATOMIC_BEGIN
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
goto_tracet
TO_BE_DOCUMENTED.
Definition: goto_trace.h:150
graphml_witnesst::convert_assign_rec
std::string convert_assign_rec(const irep_idt &identifier, const code_assignt &assign)
Definition: graphml_witness.cpp:51
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:37
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
graphml_witnesst::ns
const namespacet & ns
Definition: graphml_witness.h:38
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
exprt::operands
operandst & operands()
Definition: expr.h:78
goto_trace_stept::typet::SHARED_READ
@ SHARED_READ
index_exprt
Array index operator.
Definition: std_expr.h:1595
goto_trace_stept::typet::FUNCTION_CALL
@ FUNCTION_CALL
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
xmlt::data
std::string data
Definition: xml.h:30
c_types.h
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:171
validation_modet::INVARIANT
@ INVARIANT
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:86
goto_trace_stept::typet::DEAD
@ DEAD
goto_trace_stept::typet::CONSTRAINT
@ CONSTRAINT
not_exprt
Boolean negation.
Definition: std_expr.h:3308