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 &ns,
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 }
106 
107 std::string trace_value_binary(
108  const exprt &expr,
109  const namespacet &ns)
110 {
111  const typet &type=ns.follow(expr.type());
112 
113  if(expr.id()==ID_constant)
114  {
115  if(type.id()==ID_unsignedbv ||
116  type.id()==ID_signedbv ||
117  type.id()==ID_bv ||
118  type.id()==ID_fixedbv ||
119  type.id()==ID_floatbv ||
120  type.id()==ID_pointer ||
121  type.id()==ID_c_bit_field ||
122  type.id()==ID_c_bool ||
123  type.id()==ID_c_enum ||
124  type.id()==ID_c_enum_tag)
125  {
126  const std::string & str = expr.get_string(ID_value);
127 
128  std::ostringstream oss;
130  for(const auto c : str)
131  {
132  oss << c;
133  if(++i % 8 == 0 && str.size() != i)
134  oss << ' ';
135  }
136 
137  return oss.str();
138  }
139  else if(type.id()==ID_bool)
140  {
141  return expr.is_true()?"1":"0";
142  }
143  else if(type.id()==ID_integer)
144  {
145  mp_integer i;
146  if(!to_integer(expr, i) && i>=0)
147  return integer2string(i, 2);
148  }
149  }
150  else if(expr.id()==ID_array)
151  {
152  std::string result;
153 
154  forall_operands(it, expr)
155  {
156  if(result=="")
157  result="{ ";
158  else
159  result+=", ";
160  result+=trace_value_binary(*it, ns);
161  }
162 
163  return result+" }";
164  }
165  else if(expr.id()==ID_struct)
166  {
167  std::string result="{ ";
168 
169  forall_operands(it, expr)
170  {
171  if(it!=expr.operands().begin())
172  result+=", ";
173  result+=trace_value_binary(*it, ns);
174  }
175 
176  return result+" }";
177  }
178  else if(expr.id()==ID_union)
179  {
180  assert(expr.operands().size()==1);
181  return trace_value_binary(expr.op0(), ns);
182  }
183 
184  return "?";
185 }
186 
188  std::ostream &out,
189  const namespacet &ns,
190  const ssa_exprt &lhs_object,
191  const exprt &full_lhs,
192  const exprt &value)
193 {
194  irep_idt identifier;
195 
196  if(lhs_object.is_not_nil())
197  identifier=lhs_object.get_object_name();
198 
199  std::string value_string;
200 
201  if(value.is_nil())
202  value_string="(assignment removed)";
203  else
204  {
205  value_string=from_expr(ns, identifier, value);
206 
207  // the binary representation
208  value_string+=" ("+trace_value_binary(value, ns)+")";
209  }
210 
211  out << " "
212  << from_expr(ns, identifier, full_lhs)
213  << "=" << value_string
214  << "\n";
215 }
216 
218  std::ostream &out,
219  const goto_trace_stept &state,
220  const source_locationt &source_location,
221  unsigned step_nr)
222 {
223  out << "\n";
224 
225  if(step_nr==0)
226  out << "Initial State";
227  else
228  out << "State " << step_nr;
229 
230  out << " " << source_location
231  << " thread " << state.thread_nr << "\n";
232  out << "----------------------------------------------------" << "\n";
233 }
234 
236 {
237  if(src.id()==ID_index)
238  return is_index_member_symbol(src.op0());
239  else if(src.id()==ID_member)
240  return is_index_member_symbol(src.op0());
241  else if(src.id()==ID_symbol)
242  return true;
243  else
244  return false;
245 }
246 
248  std::ostream &out,
249  const namespacet &ns,
250  const goto_tracet &goto_trace)
251 {
252  unsigned prev_step_nr=0;
253  bool first_step=true;
254 
255  for(const auto &step : goto_trace.steps)
256  {
257  // hide the hidden ones
258  if(step.hidden)
259  continue;
260 
261  switch(step.type)
262  {
264  if(!step.cond_value)
265  {
266  out << "\n";
267  out << "Violated property:" << "\n";
268  if(!step.pc->source_location.is_nil())
269  out << " " << step.pc->source_location << "\n";
270  out << " " << step.comment << "\n";
271 
272  if(step.pc->is_assert())
273  out << " " << from_expr(ns, step.pc->function, step.pc->guard)
274  << '\n';
275 
276  out << "\n";
277  }
278  break;
279 
281  if(!step.cond_value)
282  {
283  out << "\n";
284  out << "Violated assumption:" << "\n";
285  if(!step.pc->source_location.is_nil())
286  out << " " << step.pc->source_location << "\n";
287 
288  if(step.pc->is_assume())
289  out << " " << from_expr(ns, step.pc->function, step.pc->guard)
290  << '\n';
291 
292  out << "\n";
293  }
294  break;
295 
297  break;
298 
300  break;
301 
303  if(step.pc->is_assign() ||
304  step.pc->is_return() || // returns have a lhs!
305  step.pc->is_function_call() ||
306  (step.pc->is_other() && step.lhs_object.is_not_nil()))
307  {
308  if(prev_step_nr!=step.step_nr || first_step)
309  {
310  first_step=false;
311  prev_step_nr=step.step_nr;
312  show_state_header(out, step, step.pc->source_location, step.step_nr);
313  }
314 
315  // see if the full lhs is something clean
316  if(is_index_member_symbol(step.full_lhs))
317  trace_value(
318  out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value);
319  else
320  trace_value(
321  out, ns, step.lhs_object, step.lhs_object, step.lhs_object_value);
322  }
323  break;
324 
326  if(prev_step_nr!=step.step_nr || first_step)
327  {
328  first_step=false;
329  prev_step_nr=step.step_nr;
330  show_state_header(out, step, step.pc->source_location, step.step_nr);
331  }
332 
333  trace_value(out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value);
334  break;
335 
337  if(step.formatted)
338  {
339  printf_formattert printf_formatter(ns);
340  printf_formatter(id2string(step.format_string), step.io_args);
341  printf_formatter.print(out);
342  out << "\n";
343  }
344  else
345  {
346  show_state_header(out, step, step.pc->source_location, step.step_nr);
347  out << " OUTPUT " << step.io_id << ":";
348 
349  for(std::list<exprt>::const_iterator
350  l_it=step.io_args.begin();
351  l_it!=step.io_args.end();
352  l_it++)
353  {
354  if(l_it!=step.io_args.begin())
355  out << ";";
356  out << " " << from_expr(ns, step.pc->function, *l_it);
357 
358  // the binary representation
359  out << " (" << trace_value_binary(*l_it, ns) << ")";
360  }
361 
362  out << "\n";
363  }
364  break;
365 
367  show_state_header(out, step, step.pc->source_location, step.step_nr);
368  out << " INPUT " << step.io_id << ":";
369 
370  for(std::list<exprt>::const_iterator
371  l_it=step.io_args.begin();
372  l_it!=step.io_args.end();
373  l_it++)
374  {
375  if(l_it!=step.io_args.begin())
376  out << ";";
377  out << " " << from_expr(ns, step.pc->function, *l_it);
378 
379  // the binary representation
380  out << " (" << trace_value_binary(*l_it, ns) << ")";
381  }
382 
383  out << "\n";
384  break;
385 
393  break;
394 
398  default:
399  UNREACHABLE;
400  }
401  }
402 }
403 
404 
The type of an expression.
Definition: type.h:22
BigInt mp_integer
Definition: mp_arith.h:22
bool is_nil() const
Definition: irep.h:102
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
Symbol table entry.
std::string trace_value_binary(const exprt &expr, const namespacet &ns)
Definition: goto_trace.cpp:107
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 from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
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
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
Definition: goto_trace.cpp:247
printf Formatting
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:189
bool is_index_member_symbol(const exprt &src)
Definition: goto_trace.cpp:235
bool is_assume() const
Definition: goto_trace.h:42
unsigned thread_nr
Definition: goto_trace.h:98
TO_BE_DOCUMENTED.
Definition: namespace.h:74
#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 is_function_return() const
Definition: goto_trace.h:47
void trace_value(std::ostream &out, const namespacet &ns, const ssa_exprt &lhs_object, const exprt &full_lhs, const exprt &value)
Definition: goto_trace.cpp:187
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:250
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:202
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:215
void show_state_header(std::ostream &out, const goto_trace_stept &state, const source_locationt &source_location, unsigned step_nr)
Definition: goto_trace.cpp:217
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