cprover
goto_trace.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Traces of GOTO Programs
4 
5 Author: Daniel Kroening
6 
7  Date: July 2005
8 
9 \*******************************************************************/
10 
13 
14 #include "goto_trace.h"
15 
16 #include <cassert>
17 #include <ostream>
18 
19 #include <util/arith_tools.h>
20 #include <util/format_expr.h>
21 #include <util/symbol.h>
22 
23 #include <langapi/language_util.h>
24 
25 #include "printf_formatter.h"
26 
28  const class namespacet &ns,
29  std::ostream &out) const
30 {
31  for(const auto &step : steps)
32  step.output(ns, out);
33 }
34 
36  const namespacet &,
37  std::ostream &out) const
38 {
39  out << "*** ";
40 
41  switch(type)
42  {
43  case goto_trace_stept::typet::ASSERT: out << "ASSERT"; break;
44  case goto_trace_stept::typet::ASSUME: out << "ASSUME"; break;
45  case goto_trace_stept::typet::LOCATION: out << "LOCATION"; break;
46  case goto_trace_stept::typet::ASSIGNMENT: out << "ASSIGNMENT"; break;
47  case goto_trace_stept::typet::GOTO: out << "GOTO"; break;
48  case goto_trace_stept::typet::DECL: out << "DECL"; break;
49  case goto_trace_stept::typet::DEAD: out << "DEAD"; break;
50  case goto_trace_stept::typet::OUTPUT: out << "OUTPUT"; break;
51  case goto_trace_stept::typet::INPUT: out << "INPUT"; break;
53  out << "ATOMIC_BEGIN";
54  break;
55  case goto_trace_stept::typet::ATOMIC_END: out << "ATOMIC_END"; break;
56  case goto_trace_stept::typet::SHARED_READ: out << "SHARED_READ"; break;
57  case goto_trace_stept::typet::SHARED_WRITE: out << "SHARED WRITE"; break;
58  case goto_trace_stept::typet::FUNCTION_CALL: out << "FUNCTION CALL"; break;
60  out << "FUNCTION RETURN"; break;
61  default:
62  out << "unknown type: " << static_cast<int>(type) << std::endl;
64  }
65 
66  if(is_assert() || is_assume() || is_goto())
67  out << " (" << cond_value << ")";
68  else if(is_function_call() || is_function_return())
69  out << ' ' << identifier;
70 
71  if(hidden)
72  out << " hidden";
73 
74  out << '\n';
75 
76  if(is_assignment())
77  {
78  out << " " << format(full_lhs)
79  << " = " << format(full_lhs_value)
80  << '\n';
81  }
82 
83  if(!pc->source_location.is_nil())
84  out << pc->source_location << '\n';
85 
86  out << pc->type << '\n';
87 
88  if(pc->is_assert())
89  {
90  if(!cond_value)
91  {
92  out << "Violated property:" << '\n';
93  if(pc->source_location.is_nil())
94  out << " " << pc->source_location << '\n';
95 
96  if(!comment.empty())
97  out << " " << comment << '\n';
98 
99  out << " " << format(pc->guard) << '\n';
100  out << '\n';
101  }
102  }
103 
104  out << '\n';
105 }
114 static std::string
115 numeric_representation(const exprt &expr, const trace_optionst &options)
116 {
117  std::string result;
118  std::string prefix;
119  if(options.hex_representation)
120  {
121  mp_integer value_int =
122  binary2integer(id2string(to_constant_expr(expr).get_value()), false);
123  result = integer2string(value_int, 16);
124  prefix = "0x";
125  }
126  else
127  {
128  prefix = "0b";
129  result = expr.get_string(ID_value);
130  }
131 
132  std::ostringstream oss;
134  for(const auto c : result)
135  {
136  oss << c;
137  if(++i % 8 == 0 && result.size() != i)
138  oss << ' ';
139  }
140  if(options.base_prefix)
141  return prefix + oss.str();
142  else
143  return oss.str();
144 }
145 
147  const exprt &expr,
148  const namespacet &ns,
149  const trace_optionst &options)
150 {
151  const typet &type=ns.follow(expr.type());
152 
153  if(expr.id()==ID_constant)
154  {
155  if(type.id()==ID_unsignedbv ||
156  type.id()==ID_signedbv ||
157  type.id()==ID_bv ||
158  type.id()==ID_fixedbv ||
159  type.id()==ID_floatbv ||
160  type.id()==ID_pointer ||
161  type.id()==ID_c_bit_field ||
162  type.id()==ID_c_bool ||
163  type.id()==ID_c_enum ||
164  type.id()==ID_c_enum_tag)
165  {
166  const std::string &str = numeric_representation(expr, options);
167  return str;
168  }
169  else if(type.id()==ID_bool)
170  {
171  return expr.is_true()?"1":"0";
172  }
173  else if(type.id()==ID_integer)
174  {
175  mp_integer i;
176  if(!to_integer(expr, i) && i>=0)
177  return integer2string(i, 2);
178  }
179  }
180  else if(expr.id()==ID_array)
181  {
182  std::string result;
183 
184  forall_operands(it, expr)
185  {
186  if(result=="")
187  result="{ ";
188  else
189  result+=", ";
190  result+=trace_numeric_value(*it, ns, options);
191  }
192 
193  return result+" }";
194  }
195  else if(expr.id()==ID_struct)
196  {
197  std::string result="{ ";
198 
199  forall_operands(it, expr)
200  {
201  if(it!=expr.operands().begin())
202  result+=", ";
203  result+=trace_numeric_value(*it, ns, options);
204  }
205 
206  return result+" }";
207  }
208  else if(expr.id()==ID_union)
209  {
210  PRECONDITION(expr.operands().size()==1);
211  return trace_numeric_value(expr.op0(), ns, options);
212  }
213 
214  return "?";
215 }
216 
218  std::ostream &out,
219  const namespacet &ns,
220  const ssa_exprt &lhs_object,
221  const exprt &full_lhs,
222  const exprt &value,
223  const trace_optionst &options)
224 {
225  irep_idt identifier;
226 
227  if(lhs_object.is_not_nil())
228  identifier=lhs_object.get_object_name();
229 
230  std::string value_string;
231 
232  if(value.is_nil())
233  value_string="(assignment removed)";
234  else
235  {
236  value_string=from_expr(ns, identifier, value);
237 
238  // the binary representation
239  value_string += " (" + trace_numeric_value(value, ns, options) + ")";
240  }
241 
242  out << " "
243  << from_expr(ns, identifier, full_lhs)
244  << "=" << value_string
245  << "\n";
246 }
247 
249  std::ostream &out,
250  const namespacet &ns,
251  const goto_trace_stept &state,
252  const source_locationt &source_location,
253  unsigned step_nr,
254  const trace_optionst &options)
255 {
256  out << "\n";
257 
258  if(step_nr == 0)
259  out << "Initial State";
260  else
261  out << "State " << step_nr;
262 
263  out << " " << source_location << " thread " << state.thread_nr << "\n";
264  out << "----------------------------------------------------"
265  << "\n";
266 
267  if(options.show_code)
268  {
269  out << as_string(ns, *state.pc)
270  << "\n";
271  out << "----------------------------------------------------"
272  << "\n";
273  }
274 }
275 
277 {
278  if(src.id()==ID_index)
279  return is_index_member_symbol(src.op0());
280  else if(src.id()==ID_member)
281  return is_index_member_symbol(src.op0());
282  else if(src.id()==ID_symbol)
283  return true;
284  else
285  return false;
286 }
287 
289  std::ostream &out,
290  const namespacet &ns,
291  const goto_tracet &goto_trace,
292  const trace_optionst &options)
293 {
294  unsigned prev_step_nr=0;
295  bool first_step=true;
296  std::size_t function_depth=0;
297 
298  for(const auto &step : goto_trace.steps)
299  {
300  // hide the hidden ones
301  if(step.hidden)
302  continue;
303 
304  switch(step.type)
305  {
307  if(!step.cond_value)
308  {
309  out << "\n";
310  out << "Violated property:" << "\n";
311  if(!step.pc->source_location.is_nil())
312  out << " " << step.pc->source_location << "\n";
313  out << " " << step.comment << "\n";
314 
315  if(step.pc->is_assert())
316  out << " " << from_expr(ns, step.pc->function, step.pc->guard)
317  << '\n';
318 
319  out << "\n";
320  }
321  break;
322 
324  if(!step.cond_value)
325  {
326  out << "\n";
327  out << "Violated assumption:" << "\n";
328  if(!step.pc->source_location.is_nil())
329  out << " " << step.pc->source_location << "\n";
330 
331  if(step.pc->is_assume())
332  out << " " << from_expr(ns, step.pc->function, step.pc->guard)
333  << '\n';
334 
335  out << "\n";
336  }
337  break;
338 
340  break;
341 
343  break;
344 
346  if(step.pc->is_assign() ||
347  step.pc->is_return() || // returns have a lhs!
348  step.pc->is_function_call() ||
349  (step.pc->is_other() && step.lhs_object.is_not_nil()))
350  {
351  if(prev_step_nr!=step.step_nr || first_step)
352  {
353  first_step=false;
354  prev_step_nr=step.step_nr;
356  out, ns, step, step.pc->source_location, step.step_nr, options);
357  }
358 
359  // see if the full lhs is something clean
360  if(is_index_member_symbol(step.full_lhs))
361  trace_value(
362  out,
363  ns,
364  step.lhs_object,
365  step.full_lhs,
366  step.full_lhs_value,
367  options);
368  else
369  trace_value(
370  out,
371  ns,
372  step.lhs_object,
373  step.lhs_object,
374  step.lhs_object_value,
375  options);
376  }
377  break;
378 
380  if(prev_step_nr!=step.step_nr || first_step)
381  {
382  first_step=false;
383  prev_step_nr=step.step_nr;
385  out, ns, step, step.pc->source_location, step.step_nr, options);
386  }
387 
388  trace_value(
389  out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value, options);
390  break;
391 
393  if(step.formatted)
394  {
395  printf_formattert printf_formatter(ns);
396  printf_formatter(id2string(step.format_string), step.io_args);
397  printf_formatter.print(out);
398  out << "\n";
399  }
400  else
401  {
403  out, ns, step, step.pc->source_location, step.step_nr, options);
404  out << " OUTPUT " << step.io_id << ":";
405 
406  for(std::list<exprt>::const_iterator
407  l_it=step.io_args.begin();
408  l_it!=step.io_args.end();
409  l_it++)
410  {
411  if(l_it!=step.io_args.begin())
412  out << ";";
413  out << " " << from_expr(ns, step.pc->function, *l_it);
414 
415  // the binary representation
416  out << " (" << trace_numeric_value(*l_it, ns, options) << ")";
417  }
418 
419  out << "\n";
420  }
421  break;
422 
425  out, ns, step, step.pc->source_location, step.step_nr, options);
426  out << " INPUT " << step.io_id << ":";
427 
428  for(std::list<exprt>::const_iterator
429  l_it=step.io_args.begin();
430  l_it!=step.io_args.end();
431  l_it++)
432  {
433  if(l_it!=step.io_args.begin())
434  out << ";";
435  out << " " << from_expr(ns, step.pc->function, *l_it);
436 
437  // the binary representation
438  out << " (" << trace_numeric_value(*l_it, ns, options) << ")";
439  }
440 
441  out << "\n";
442  break;
443 
445  function_depth++;
446  if(options.show_function_calls)
447  out << "\n#### Function call: " << step.identifier << " (depth "
448  << function_depth << ") ####\n";
449  break;
451  function_depth--;
452  if(options.show_function_calls)
453  out << "\n#### Function return: " << step.identifier << " (depth "
454  << function_depth << ") ####\n";
455  break;
461  break;
462 
466  default:
467  UNREACHABLE;
468  }
469  }
470 }
471 
473  std::ostream &out,
474  const namespacet &ns,
475  const goto_tracet &goto_trace)
476 {
477  show_goto_trace(out, ns, goto_trace, trace_optionst::default_options);
478 }
479 
The type of an expression.
Definition: type.h:22
BigInt mp_integer
Definition: mp_arith.h:22
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
void show_state_header(std::ostream &out, const namespacet &ns, const goto_trace_stept &state, const source_locationt &source_location, unsigned step_nr, const trace_optionst &options)
Definition: goto_trace.cpp:248
Symbol table entry.
bool show_function_calls
Definition: goto_trace.h:203
bool is_goto() const
Definition: goto_trace.h:44
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
exprt & op0()
Definition: expr.h:72
std::string trace_numeric_value(const exprt &expr, const namespacet &ns, const trace_optionst &options)
Definition: goto_trace.cpp:146
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
static std::string numeric_representation(const exprt &expr, const trace_optionst &options)
Returns the numeric representation of an expression, based on options.
Definition: goto_trace.cpp:115
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
Traces of GOTO Programs.
bool is_true() const
Definition: expr.cpp:124
typet & type()
Definition: expr.h:56
unsignedbv_typet size_type()
Definition: c_types.cpp:58
printf Formatting
std::string as_string(const class namespacet &ns, const goto_programt::instructiont &i)
TO_BE_DOCUMENTED.
Definition: goto_trace.h:36
stepst steps
Definition: goto_trace.h:156
goto_programt::const_targett pc
Definition: goto_trace.h:95
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace in ASCII to a given stream
Definition: goto_trace.cpp:27
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace step in ASCII to a given stream
Definition: goto_trace.cpp:35
bool is_function_call() const
Definition: goto_trace.h:46
const irep_idt & id() const
Definition: irep.h:259
bool is_index_member_symbol(const exprt &src)
Definition: goto_trace.cpp:276
bool is_assume() const
Definition: goto_trace.h:42
void trace_value(std::ostream &out, const namespacet &ns, const ssa_exprt &lhs_object, const exprt &full_lhs, const exprt &value, const trace_optionst &options)
Definition: goto_trace.cpp:217
unsigned thread_nr
Definition: goto_trace.h:98
TO_BE_DOCUMENTED.
Definition: namespace.h:74
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
#define forall_operands(it, expr)
Definition: expr.h:17
const typet & follow(const typet &) const
Definition: namespace.cpp:55
irep_idt identifier
Definition: goto_trace.h:123
bool hex_representation
Definition: goto_trace.h:201
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
bool is_function_return() const
Definition: goto_trace.h:47
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4463
Base class for all expressions.
Definition: expr.h:42
exprt full_lhs_value
Definition: goto_trace.h:114
irep_idt get_object_name() const
Definition: ssa_expr.h:46
#define UNREACHABLE
Definition: invariant.h:271
void print(std::ostream &out)
std::string comment
Definition: goto_trace.h:105
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Definition: goto_trace.cpp:288
bool is_assert() const
Definition: goto_trace.h:43
bool is_assignment() const
Definition: goto_trace.h:41
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
TO_BE_DOCUMENTED.
Definition: goto_trace.h:152
static const trace_optionst default_options
Definition: goto_trace.h:206
operandst & operands()
Definition: expr.h:66
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
static format_containert< T > format(const T &o)
Definition: format.h:35