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/symbol.h>
21 
23 #include <langapi/language_util.h>
24 
26  const class namespacet &ns,
27  std::ostream &out) const
28 {
29  for(const auto &step : steps)
30  step.output(ns, out);
31 }
32 
34  const namespacet &ns,
35  std::ostream &out) const
36 {
37  out << "*** ";
38 
39  switch(type)
40  {
41  case goto_trace_stept::typet::ASSERT: out << "ASSERT"; break;
42  case goto_trace_stept::typet::ASSUME: out << "ASSUME"; break;
43  case goto_trace_stept::typet::LOCATION: out << "LOCATION"; break;
44  case goto_trace_stept::typet::ASSIGNMENT: out << "ASSIGNMENT"; break;
45  case goto_trace_stept::typet::GOTO: out << "GOTO"; break;
46  case goto_trace_stept::typet::DECL: out << "DECL"; break;
47  case goto_trace_stept::typet::OUTPUT: out << "OUTPUT"; break;
48  case goto_trace_stept::typet::INPUT: out << "INPUT"; break;
49  case goto_trace_stept::typet::ATOMIC_BEGIN: out << "ATOMC_BEGIN"; break;
50  case goto_trace_stept::typet::ATOMIC_END: out << "ATOMIC_END"; break;
51  case goto_trace_stept::typet::SHARED_READ: out << "SHARED_READ"; break;
52  case goto_trace_stept::typet::SHARED_WRITE: out << "SHARED WRITE"; break;
53  case goto_trace_stept::typet::FUNCTION_CALL: out << "FUNCTION CALL"; break;
55  out << "FUNCTION RETURN"; break;
56  default: assert(false);
57  }
58 
60  out << " (" << cond_value << ")";
61 
62  if(hidden)
63  out << " hidden";
64 
65  out << "\n";
66 
67  if(!pc->source_location.is_nil())
68  out << pc->source_location << "\n";
69 
70  if(pc->is_goto())
71  out << "GOTO ";
72  else if(pc->is_assume())
73  out << "ASSUME ";
74  else if(pc->is_assert())
75  out << "ASSERT ";
76  else if(pc->is_dead())
77  out << "DEAD ";
78  else if(pc->is_other())
79  out << "OTHER ";
80  else if(pc->is_assign())
81  out << "ASSIGN ";
82  else if(pc->is_decl())
83  out << "DECL ";
84  else if(pc->is_function_call())
85  out << "CALL ";
86  else
87  out << "(?) ";
88 
89  out << "\n";
90 
91  if(pc->is_other() || pc->is_assign())
92  {
94  out << " " << from_expr(ns, identifier, lhs_object.get_original_expr())
95  << " = " << from_expr(ns, identifier, lhs_object_value)
96  << "\n";
97  }
98  else if(pc->is_assert())
99  {
100  if(!cond_value)
101  {
102  out << "Violated property:" << "\n";
103  if(pc->source_location.is_nil())
104  out << " " << pc->source_location << "\n";
105 
106  if(comment!="")
107  out << " " << comment << "\n";
108  out << " " << from_expr(ns, "", pc->guard) << "\n";
109  out << "\n";
110  }
111  }
112 
113  out << "\n";
114 }
115 
116 std::string trace_value_binary(
117  const exprt &expr,
118  const namespacet &ns)
119 {
120  const typet &type=ns.follow(expr.type());
121 
122  if(expr.id()==ID_constant)
123  {
124  if(type.id()==ID_unsignedbv ||
125  type.id()==ID_signedbv ||
126  type.id()==ID_bv ||
127  type.id()==ID_fixedbv ||
128  type.id()==ID_floatbv ||
129  type.id()==ID_pointer ||
130  type.id()==ID_c_bit_field ||
131  type.id()==ID_c_bool ||
132  type.id()==ID_c_enum ||
133  type.id()==ID_c_enum_tag)
134  {
135  return expr.get_string(ID_value);
136  }
137  else if(type.id()==ID_bool)
138  {
139  return expr.is_true()?"1":"0";
140  }
141  }
142  else if(expr.id()==ID_array)
143  {
144  std::string result;
145 
146  forall_operands(it, expr)
147  {
148  if(result=="")
149  result="{ ";
150  else
151  result+=", ";
152  result+=trace_value_binary(*it, ns);
153  }
154 
155  return result+" }";
156  }
157  else if(expr.id()==ID_struct)
158  {
159  std::string result="{ ";
160 
161  forall_operands(it, expr)
162  {
163  if(it!=expr.operands().begin())
164  result+=", ";
165  result+=trace_value_binary(*it, ns);
166  }
167 
168  return result+" }";
169  }
170  else if(expr.id()==ID_union)
171  {
172  assert(expr.operands().size()==1);
173  return trace_value_binary(expr.op0(), ns);
174  }
175 
176  return "?";
177 }
178 
180  std::ostream &out,
181  const namespacet &ns,
182  const ssa_exprt &lhs_object,
183  const exprt &full_lhs,
184  const exprt &value)
185 {
186  irep_idt identifier;
187 
188  if(lhs_object.is_not_nil())
189  identifier=lhs_object.get_object_name();
190 
191  std::string value_string;
192 
193  if(value.is_nil())
194  value_string="(assignment removed)";
195  else
196  {
197  value_string=from_expr(ns, identifier, value);
198 
199  // the binary representation
200  value_string+=" ("+trace_value_binary(value, ns)+")";
201  }
202 
203  out << " "
204  << from_expr(ns, identifier, full_lhs)
205  << "=" << value_string
206  << "\n";
207 }
208 
210  std::ostream &out,
211  const goto_trace_stept &state,
212  const source_locationt &source_location,
213  unsigned step_nr)
214 {
215  out << "\n";
216 
217  if(step_nr==0)
218  out << "Initial State";
219  else
220  out << "State " << step_nr;
221 
222  out << " " << source_location
223  << " thread " << state.thread_nr << "\n";
224  out << "----------------------------------------------------" << "\n";
225 }
226 
228 {
229  if(src.id()==ID_index)
230  return is_index_member_symbol(src.op0());
231  else if(src.id()==ID_member)
232  return is_index_member_symbol(src.op0());
233  else if(src.id()==ID_symbol)
234  return true;
235  else
236  return false;
237 }
238 
240  std::ostream &out,
241  const namespacet &ns,
242  const goto_tracet &goto_trace)
243 {
244  unsigned prev_step_nr=0;
245  bool first_step=true;
246 
247  for(const auto &step : goto_trace.steps)
248  {
249  // hide the hidden ones
250  if(step.hidden)
251  continue;
252 
253  switch(step.type)
254  {
256  if(!step.cond_value)
257  {
258  out << "\n";
259  out << "Violated property:" << "\n";
260  if(!step.pc->source_location.is_nil())
261  out << " " << step.pc->source_location << "\n";
262  out << " " << step.comment << "\n";
263 
264  if(step.pc->is_assert())
265  out << " " << from_expr(ns, "", step.pc->guard) << "\n";
266 
267  out << "\n";
268  }
269  break;
270 
272  if(!step.cond_value)
273  {
274  out << "\n";
275  out << "Violated assumption:" << "\n";
276  if(!step.pc->source_location.is_nil())
277  out << " " << step.pc->source_location << "\n";
278 
279  if(step.pc->is_assume())
280  out << " " << from_expr(ns, "", step.pc->guard) << "\n";
281 
282  out << "\n";
283  }
284  break;
285 
287  break;
288 
290  break;
291 
293  if(step.pc->is_assign() ||
294  step.pc->is_return() || // returns have a lhs!
295  step.pc->is_function_call() ||
296  (step.pc->is_other() && step.lhs_object.is_not_nil()))
297  {
298  if(prev_step_nr!=step.step_nr || first_step)
299  {
300  first_step=false;
301  prev_step_nr=step.step_nr;
302  show_state_header(out, step, step.pc->source_location, step.step_nr);
303  }
304 
305  // see if the full lhs is something clean
306  if(is_index_member_symbol(step.full_lhs))
307  trace_value(
308  out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value);
309  else
310  trace_value(
311  out, ns, step.lhs_object, step.lhs_object, step.lhs_object_value);
312  }
313  break;
314 
316  if(prev_step_nr!=step.step_nr || first_step)
317  {
318  first_step=false;
319  prev_step_nr=step.step_nr;
320  show_state_header(out, step, step.pc->source_location, step.step_nr);
321  }
322 
323  trace_value(out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value);
324  break;
325 
327  if(step.formatted)
328  {
329  printf_formattert printf_formatter(ns);
330  printf_formatter(id2string(step.format_string), step.io_args);
331  printf_formatter.print(out);
332  out << "\n";
333  }
334  else
335  {
336  show_state_header(out, step, step.pc->source_location, step.step_nr);
337  out << " OUTPUT " << step.io_id << ":";
338 
339  for(std::list<exprt>::const_iterator
340  l_it=step.io_args.begin();
341  l_it!=step.io_args.end();
342  l_it++)
343  {
344  if(l_it!=step.io_args.begin())
345  out << ";";
346  out << " " << from_expr(ns, "", *l_it);
347 
348  // the binary representation
349  out << " (" << trace_value_binary(*l_it, ns) << ")";
350  }
351 
352  out << "\n";
353  }
354  break;
355 
357  show_state_header(out, step, step.pc->source_location, step.step_nr);
358  out << " INPUT " << step.io_id << ":";
359 
360  for(std::list<exprt>::const_iterator
361  l_it=step.io_args.begin();
362  l_it!=step.io_args.end();
363  l_it++)
364  {
365  if(l_it!=step.io_args.begin())
366  out << ";";
367  out << " " << from_expr(ns, "", *l_it);
368 
369  // the binary representation
370  out << " (" << trace_value_binary(*l_it, ns) << ")";
371  }
372 
373  out << "\n";
374  break;
375 
383  break;
384 
386  assert(false);
387  break;
388 
391  assert(false);
392  break;
393 
394  default:
395  assert(false);
396  }
397  }
398 }
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
Symbol table entry.
std::string trace_value_binary(const exprt &expr, const namespacet &ns)
Definition: goto_trace.cpp:116
exprt & op0()
Definition: expr.h:84
exprt lhs_object_value
Definition: goto_trace.h:109
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:133
typet & type()
Definition: expr.h:60
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
Definition: goto_trace.cpp:239
printf Formatting
TO_BE_DOCUMENTED.
Definition: goto_trace.h:34
stepst steps
Definition: goto_trace.h:150
goto_programt::const_targett pc
Definition: goto_trace.h:90
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace in ASCII to a given stream
Definition: goto_trace.cpp:25
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace step in ASCII to a given stream
Definition: goto_trace.cpp:33
const irep_idt & id() const
Definition: irep.h:189
bool is_index_member_symbol(const exprt &src)
Definition: goto_trace.cpp:227
unsigned thread_nr
Definition: goto_trace.h:93
TO_BE_DOCUMENTED.
Definition: namespace.h:62
#define forall_operands(it, expr)
Definition: expr.h:17
irep_idt identifier
Definition: goto_trace.h:118
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:179
Base class for all expressions.
Definition: expr.h:46
ssa_exprt lhs_object
Definition: goto_trace.h:103
irep_idt get_object_name() const
Definition: ssa_expr.h:46
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
void print(std::ostream &out)
std::string comment
Definition: goto_trace.h:100
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146
void show_state_header(std::ostream &out, const goto_trace_stept &state, const source_locationt &source_location, unsigned step_nr)
Definition: goto_trace.cpp:209
operandst & operands()
Definition: expr.h:70
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17