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 <ostream>
17 
18 #include <util/arith_tools.h>
19 #include <util/format_expr.h>
20 #include <util/symbol.h>
21 
22 #include <langapi/language_util.h>
23 
24 #include "printf_formatter.h"
25 
27 {
28  if(src.id()==ID_symbol)
29  return to_symbol_expr(src);
30  else if(src.id()==ID_member)
32  else if(src.id()==ID_index)
33  return get_object_rec(to_index_expr(src).array());
34  else if(src.id()==ID_typecast)
35  return get_object_rec(to_typecast_expr(src).op());
36  else
37  return {}; // give up
38 }
39 
41 {
42  return get_object_rec(full_lhs);
43 }
44 
46  const class namespacet &ns,
47  std::ostream &out) const
48 {
49  for(const auto &step : steps)
50  step.output(ns, out);
51 }
52 
54  const namespacet &,
55  std::ostream &out) const
56 {
57  out << "*** ";
58 
59  switch(type)
60  {
61  case goto_trace_stept::typet::ASSERT: out << "ASSERT"; break;
62  case goto_trace_stept::typet::ASSUME: out << "ASSUME"; break;
63  case goto_trace_stept::typet::LOCATION: out << "LOCATION"; break;
64  case goto_trace_stept::typet::ASSIGNMENT: out << "ASSIGNMENT"; break;
65  case goto_trace_stept::typet::GOTO: out << "GOTO"; break;
66  case goto_trace_stept::typet::DECL: out << "DECL"; break;
67  case goto_trace_stept::typet::DEAD: out << "DEAD"; break;
68  case goto_trace_stept::typet::OUTPUT: out << "OUTPUT"; break;
69  case goto_trace_stept::typet::INPUT: out << "INPUT"; break;
71  out << "ATOMIC_BEGIN";
72  break;
73  case goto_trace_stept::typet::ATOMIC_END: out << "ATOMIC_END"; break;
74  case goto_trace_stept::typet::SHARED_READ: out << "SHARED_READ"; break;
75  case goto_trace_stept::typet::SHARED_WRITE: out << "SHARED WRITE"; break;
76  case goto_trace_stept::typet::FUNCTION_CALL: out << "FUNCTION CALL"; break;
78  out << "FUNCTION RETURN"; break;
79  default:
80  out << "unknown type: " << static_cast<int>(type) << std::endl;
82  }
83 
84  if(is_assert() || is_assume() || is_goto())
85  out << " (" << cond_value << ')';
86  else if(is_function_call())
87  out << ' ' << called_function;
88 
89  if(hidden)
90  out << " hidden";
91 
92  out << '\n';
93 
94  if(is_assignment())
95  {
96  out << " " << format(full_lhs)
97  << " = " << format(full_lhs_value)
98  << '\n';
99  }
100 
101  if(!pc->source_location.is_nil())
102  out << pc->source_location << '\n';
103 
104  out << pc->type << '\n';
105 
106  if(pc->is_assert())
107  {
108  if(!cond_value)
109  {
110  out << "Violated property:" << '\n';
111  if(pc->source_location.is_nil())
112  out << " " << pc->source_location << '\n';
113 
114  if(!comment.empty())
115  out << " " << comment << '\n';
116 
117  out << " " << format(pc->guard) << '\n';
118  out << '\n';
119  }
120  }
121 
122  out << '\n';
123 }
133 static std::string numeric_representation(
134  const constant_exprt &expr,
135  const namespacet &ns,
136  const trace_optionst &options)
137 {
138  std::string result;
139  std::string prefix;
140 
141  const typet &expr_type = expr.type();
142 
143  const typet &underlying_type =
144  expr_type.id() == ID_c_enum_tag
145  ? ns.follow_tag(to_c_enum_tag_type(expr_type)).subtype()
146  : expr_type;
147 
148  const irep_idt &value = expr.get_value();
149 
150  const auto width = to_bitvector_type(underlying_type).get_width();
151 
152  const mp_integer value_int = bvrep2integer(id2string(value), width, false);
153 
154  if(options.hex_representation)
155  {
156  result = integer2string(value_int, 16);
157  prefix = "0x";
158  }
159  else
160  {
161  result = integer2binary(value_int, width);
162  prefix = "0b";
163  }
164 
165  std::ostringstream oss;
167  for(const auto c : result)
168  {
169  oss << c;
170  if(++i % 8 == 0 && result.size() != i)
171  oss << ' ';
172  }
173  if(options.base_prefix)
174  return prefix + oss.str();
175  else
176  return oss.str();
177 }
178 
180  const exprt &expr,
181  const namespacet &ns,
182  const trace_optionst &options)
183 {
184  const typet &type=ns.follow(expr.type());
185 
186  if(expr.id()==ID_constant)
187  {
188  if(type.id()==ID_unsignedbv ||
189  type.id()==ID_signedbv ||
190  type.id()==ID_bv ||
191  type.id()==ID_fixedbv ||
192  type.id()==ID_floatbv ||
193  type.id()==ID_pointer ||
194  type.id()==ID_c_bit_field ||
195  type.id()==ID_c_bool ||
196  type.id()==ID_c_enum ||
197  type.id()==ID_c_enum_tag)
198  {
199  return numeric_representation(to_constant_expr(expr), ns, options);
200  }
201  else if(type.id()==ID_bool)
202  {
203  return expr.is_true()?"1":"0";
204  }
205  else if(type.id()==ID_integer)
206  {
207  const auto i = numeric_cast<mp_integer>(expr);
208  if(i.has_value() && *i >= 0)
209  {
210  if(options.hex_representation)
211  return "0x" + integer2string(*i, 16);
212  else
213  return "0b" + integer2string(*i, 2);
214  }
215  }
216  }
217  else if(expr.id()==ID_array)
218  {
219  std::string result;
220 
221  forall_operands(it, expr)
222  {
223  if(result=="")
224  result="{ ";
225  else
226  result+=", ";
227  result+=trace_numeric_value(*it, ns, options);
228  }
229 
230  return result+" }";
231  }
232  else if(expr.id()==ID_struct)
233  {
234  std::string result="{ ";
235 
236  forall_operands(it, expr)
237  {
238  if(it!=expr.operands().begin())
239  result+=", ";
240  result+=trace_numeric_value(*it, ns, options);
241  }
242 
243  return result+" }";
244  }
245  else if(expr.id()==ID_union)
246  {
247  PRECONDITION(expr.operands().size()==1);
248  return trace_numeric_value(expr.op0(), ns, options);
249  }
250 
251  return "?";
252 }
253 
255  messaget::mstreamt &out,
256  const namespacet &ns,
257  const optionalt<symbol_exprt> &lhs_object,
258  const exprt &full_lhs,
259  const exprt &value,
260  const trace_optionst &options)
261 {
262  irep_idt identifier;
263 
264  if(lhs_object.has_value())
265  identifier=lhs_object->get_identifier();
266 
267  out << " " << from_expr(ns, identifier, full_lhs) << '=';
268 
269  if(value.is_nil())
270  out << "(assignment removed)";
271  else
272  {
273  out << from_expr(ns, identifier, value);
274 
275  // the binary representation
276  out << ' ' << messaget::faint << '('
277  << trace_numeric_value(value, ns, options) << ')' << messaget::reset;
278  }
279 
280  out << '\n';
281 }
282 
283 static std::string
285 {
286  std::string result;
287 
288  const auto &source_location = state.pc->source_location;
289 
290  if(!source_location.get_file().empty())
291  result += "file " + id2string(source_location.get_file());
292 
293  if(!state.function.empty())
294  {
295  const symbolt &symbol = ns.lookup(state.function);
296  if(!result.empty())
297  result += ' ';
298  result += "function " + id2string(symbol.display_name());
299  }
300 
301  if(!source_location.get_line().empty())
302  {
303  if(!result.empty())
304  result += ' ';
305  result += "line " + id2string(source_location.get_line());
306  }
307 
308  if(!result.empty())
309  result += ' ';
310  result += "thread " + std::to_string(state.thread_nr);
311 
312  return result;
313 }
314 
316  messaget::mstreamt &out,
317  const namespacet &ns,
318  const goto_trace_stept &state,
319  unsigned step_nr,
320  const trace_optionst &options)
321 {
322  out << '\n';
323 
324  if(step_nr == 0)
325  out << "Initial State";
326  else
327  out << "State " << step_nr;
328 
329  out << ' ' << state_location(state, ns) << '\n';
330  out << "----------------------------------------------------" << '\n';
331 
332  if(options.show_code)
333  {
334  out << as_string(ns, *state.pc) << '\n';
335  out << "----------------------------------------------------" << '\n';
336  }
337 }
338 
340 {
341  if(src.id()==ID_index)
342  return is_index_member_symbol(src.op0());
343  else if(src.id()==ID_member)
344  return is_index_member_symbol(src.op0());
345  else if(src.id()==ID_symbol)
346  return true;
347  else
348  return false;
349 }
350 
352  messaget::mstreamt &out,
353  const namespacet &ns,
354  const goto_tracet &goto_trace,
355  const trace_optionst &options)
356 {
357  unsigned prev_step_nr=0;
358  bool first_step=true;
359  std::size_t function_depth=0;
360 
361  for(const auto &step : goto_trace.steps)
362  {
363  // hide the hidden ones
364  if(step.hidden)
365  continue;
366 
367  switch(step.type)
368  {
370  if(!step.cond_value)
371  {
372  out << '\n';
373  out << messaget::red << "Violated property:" << messaget::reset << '\n';
374  if(!step.pc->source_location.is_nil())
375  {
376  out << " " << state_location(step, ns) << '\n';
377  }
378 
379  out << " " << messaget::red << step.comment << messaget::reset << '\n';
380 
381  if(step.pc->is_assert())
382  out << " " << from_expr(ns, step.function, step.pc->guard) << '\n';
383 
384  out << '\n';
385  }
386  break;
387 
389  if(!step.cond_value)
390  {
391  out << '\n';
392  out << "Violated assumption:" << '\n';
393  if(!step.pc->source_location.is_nil())
394  out << " " << step.pc->source_location << '\n';
395 
396  if(step.pc->is_assume())
397  out << " " << from_expr(ns, step.function, step.pc->guard) << '\n';
398 
399  out << '\n';
400  }
401  break;
402 
404  break;
405 
407  break;
408 
410  if(step.pc->is_assign() ||
411  step.pc->is_return() || // returns have a lhs!
412  step.pc->is_function_call() ||
413  (step.pc->is_other() && step.full_lhs.is_not_nil()))
414  {
415  if(prev_step_nr!=step.step_nr || first_step)
416  {
417  first_step=false;
418  prev_step_nr=step.step_nr;
419  show_state_header(out, ns, step, step.step_nr, options);
420  }
421 
422  trace_value(
423  out,
424  ns,
425  step.get_lhs_object(),
426  step.full_lhs,
427  step.full_lhs_value,
428  options);
429  }
430  break;
431 
433  if(prev_step_nr!=step.step_nr || first_step)
434  {
435  first_step=false;
436  prev_step_nr=step.step_nr;
437  show_state_header(out, ns, step, step.step_nr, options);
438  }
439 
440  trace_value(
441  out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
442  break;
443 
445  if(step.formatted)
446  {
447  printf_formattert printf_formatter(ns);
448  printf_formatter(id2string(step.format_string), step.io_args);
449  printf_formatter.print(out);
450  out << '\n';
451  }
452  else
453  {
454  show_state_header(out, ns, step, step.step_nr, options);
455  out << " OUTPUT " << step.io_id << ':';
456 
457  for(std::list<exprt>::const_iterator
458  l_it=step.io_args.begin();
459  l_it!=step.io_args.end();
460  l_it++)
461  {
462  if(l_it!=step.io_args.begin())
463  out << ';';
464 
465  out << ' ' << from_expr(ns, step.function, *l_it);
466 
467  // the binary representation
468  out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
469  }
470 
471  out << '\n';
472  }
473  break;
474 
476  show_state_header(out, ns, step, step.step_nr, options);
477  out << " INPUT " << step.io_id << ':';
478 
479  for(std::list<exprt>::const_iterator
480  l_it=step.io_args.begin();
481  l_it!=step.io_args.end();
482  l_it++)
483  {
484  if(l_it!=step.io_args.begin())
485  out << ';';
486 
487  out << ' ' << from_expr(ns, step.function, *l_it);
488 
489  // the binary representation
490  out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
491  }
492 
493  out << '\n';
494  break;
495 
497  function_depth++;
498  if(options.show_function_calls)
499  {
500  out << "\n#### Function call: " << step.called_function;
501  out << '(';
502 
503  bool first = true;
504  for(auto &arg : step.function_arguments)
505  {
506  if(first)
507  first = false;
508  else
509  out << ", ";
510 
511  out << from_expr(ns, step.function, arg);
512  }
513 
514  out << ") (depth " << function_depth << ") ####\n";
515  }
516  break;
517 
519  function_depth--;
520  if(options.show_function_calls)
521  {
522  out << "\n#### Function return from " << step.function << " (depth "
523  << function_depth << ") ####\n";
524  }
525  break;
526 
532  break;
533 
537  default:
538  UNREACHABLE;
539  }
540  }
541 }
542 
544  messaget::mstreamt &out,
545  const namespacet &ns,
546  const goto_tracet &goto_trace)
547 {
548  // map from thread number to a call stack
549  std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
550  call_stacks;
551 
552  // by default, we show thread 0
553  unsigned thread_to_show = 0;
554 
555  for(auto s_it = goto_trace.steps.begin(); s_it != goto_trace.steps.end();
556  s_it++)
557  {
558  const auto &step = *s_it;
559  auto &stack = call_stacks[step.thread_nr];
560 
561  if(step.is_assert())
562  {
563  if(!step.cond_value)
564  {
565  stack.push_back(s_it);
566  thread_to_show = step.thread_nr;
567  }
568  }
569  else if(step.is_function_call())
570  {
571  stack.push_back(s_it);
572  }
573  else if(step.is_function_return())
574  {
575  stack.pop_back();
576  }
577  }
578 
579  const auto &stack = call_stacks[thread_to_show];
580 
581  // print in reverse order
582  for(auto s_it = stack.rbegin(); s_it != stack.rend(); s_it++)
583  {
584  const auto &step = **s_it;
585  if(step.is_assert())
586  {
587  out << " assertion failure";
588  if(!step.pc->source_location.is_nil())
589  out << ' ' << step.pc->source_location;
590  out << '\n';
591  }
592  else if(step.is_function_call())
593  {
594  out << " " << step.called_function;
595  out << '(';
596 
597  bool first = true;
598  for(auto &arg : step.function_arguments)
599  {
600  if(first)
601  first = false;
602  else
603  out << ", ";
604 
605  out << from_expr(ns, step.function, arg);
606  }
607 
608  out << ')';
609 
610  if(!step.pc->source_location.is_nil())
611  out << ' ' << step.pc->source_location;
612 
613  out << '\n';
614  }
615  }
616 }
617 
619  messaget::mstreamt &out,
620  const namespacet &ns,
621  const goto_tracet &goto_trace,
622  const trace_optionst &options)
623 {
624  if(options.stack_trace)
625  show_goto_stack_trace(out, ns, goto_trace);
626  else
627  show_full_goto_trace(out, ns, goto_trace, options);
628 }
629 
631  messaget::mstreamt &out,
632  const namespacet &ns,
633  const goto_tracet &goto_trace)
634 {
635  show_goto_trace(out, ns, goto_trace, trace_optionst::default_options);
636 }
637 
The type of an expression, extends irept.
Definition: type.h:27
BigInt mp_integer
Definition: mp_arith.h:22
void show_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Definition: goto_trace.cpp:618
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
Symbol table entry.
bool show_function_calls
Definition: goto_trace.h:201
bool is_goto() const
Definition: goto_trace.h:38
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
exprt & op0()
Definition: expr.h:84
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1178
const exprt & op() const
Definition: std_expr.h:370
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::string trace_numeric_value(const exprt &expr, const namespacet &ns, const trace_optionst &options)
Definition: goto_trace.cpp:179
void show_state_header(messaget::mstreamt &out, const namespacet &ns, const goto_trace_stept &state, unsigned step_nr, const trace_optionst &options)
Definition: goto_trace.cpp:315
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const irep_idt & get_value() const
Definition: std_expr.h:4362
Traces of GOTO Programs.
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:122
typet & type()
Return the type of the expression.
Definition: expr.h:68
unsignedbv_typet size_type()
Definition: c_types.cpp:58
Symbol table entry.
Definition: symbol.h:27
printf Formatting
A constant literal expression.
Definition: std_expr.h:4343
std::string as_string(const class namespacet &ns, const goto_programt::instructiont &i)
TO_BE_DOCUMENTED.
Definition: goto_trace.h:30
stepst steps
Definition: goto_trace.h:154
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:330
goto_programt::const_targett pc
Definition: goto_trace.h:92
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:108
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace in ASCII to a given stream
Definition: goto_trace.cpp:45
irep_idt called_function
Definition: goto_trace.h:120
irep_idt function
Definition: goto_trace.h:91
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace step in ASCII to a given stream
Definition: goto_trace.cpp:53
bool is_function_call() const
Definition: goto_trace.h:40
const irep_idt & id() const
Definition: irep.h:259
bool is_index_member_symbol(const exprt &src)
Definition: goto_trace.cpp:339
bool is_assume() const
Definition: goto_trace.h:36
static std::string state_location(const goto_trace_stept &state, const namespacet &ns)
Definition: goto_trace.cpp:284
source_locationt source_location
Definition: message.h:236
nonstd::optional< T > optionalt
Definition: optional.h:35
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Definition: arith_tools.h:123
unsigned thread_nr
Definition: goto_trace.h:95
static const commandt red
render text with red foreground color
Definition: message.h:333
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
#define PRECONDITION(CONDITION)
Definition: invariant.h:427
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3926
optionalt< symbol_exprt > get_lhs_object() const
Definition: goto_trace.cpp:40
#define forall_operands(it, expr)
Definition: expr.h:20
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:80
bool hex_representation
Definition: goto_trace.h:199
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4382
std::size_t get_width() const
Definition: std_types.h:1138
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:758
void trace_value(messaget::mstreamt &out, const namespacet &ns, const optionalt< symbol_exprt > &lhs_object, const exprt &full_lhs, const exprt &value, const trace_optionst &options)
Definition: goto_trace.cpp:254
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
static const commandt faint
render text with faint font
Definition: message.h:372
void show_full_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Definition: goto_trace.cpp:351
static std::string numeric_representation(const constant_exprt &expr, const namespacet &ns, const trace_optionst &options)
Returns the numeric representation of an expression, based on options.
Definition: goto_trace.cpp:133
Base class for all expressions.
Definition: expr.h:54
const exprt & struct_op() const
Definition: std_expr.h:3898
exprt full_lhs_value
Definition: goto_trace.h:111
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:67
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:467
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2281
void print(std::ostream &out)
std::string comment
Definition: goto_trace.h:102
bool is_assert() const
Definition: goto_trace.h:37
bool is_assignment() const
Definition: goto_trace.h:35
static void show_goto_stack_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace)
Definition: goto_trace.cpp:543
TO_BE_DOCUMENTED.
Definition: goto_trace.h:150
static optionalt< symbol_exprt > get_object_rec(const exprt &src)
Definition: goto_trace.cpp:26
static const trace_optionst default_options
Definition: goto_trace.h:205
const typet & subtype() const
Definition: type.h:38
operandst & operands()
Definition: expr.h:78
#define stack(x)
Definition: parser.h:144
bool empty() const
Definition: dstring.h:75
exprt & array()
Definition: std_expr.h:1598
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1625
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:184
static format_containert< T > format(const T &o)
Definition: format.h:35