cprover
goto_trace.h
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 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H
15 #define CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H
16 
17 #include <iosfwd>
18 #include <vector>
19 
20 #include <util/message.h>
21 #include <util/options.h>
22 
24 
25 class merge_irept;
26 
50 {
51 public:
53  std::size_t step_nr;
54 
55  bool is_assignment() const { return type==typet::ASSIGNMENT; }
56  bool is_assume() const { return type==typet::ASSUME; }
57  bool is_assert() const { return type==typet::ASSERT; }
58  bool is_goto() const { return type==typet::GOTO; }
59  bool is_constraint() const { return type==typet::CONSTRAINT; }
60  bool is_function_call() const { return type==typet::FUNCTION_CALL; }
62  bool is_location() const { return type==typet::LOCATION; }
63  bool is_output() const { return type==typet::OUTPUT; }
64  bool is_input() const { return type==typet::INPUT; }
65  bool is_decl() const { return type==typet::DECL; }
66  bool is_dead() const { return type==typet::DEAD; }
67  bool is_shared_read() const { return type==typet::SHARED_READ; }
68  bool is_shared_write() const { return type==typet::SHARED_WRITE; }
69  bool is_spawn() const { return type==typet::SPAWN; }
70  bool is_memory_barrier() const { return type==typet::MEMORY_BARRIER; }
71  bool is_atomic_begin() const { return type==typet::ATOMIC_BEGIN; }
72  bool is_atomic_end() const { return type==typet::ATOMIC_END; }
73 
74  enum class typet
75  {
76  NONE,
77  ASSIGNMENT,
78  ASSUME,
79  ASSERT,
80  GOTO,
81  LOCATION,
82  INPUT,
83  OUTPUT,
84  DECL,
85  DEAD,
88  CONSTRAINT,
91  SPAWN,
95  };
96 
98 
99  // we may choose to hide a step
100  bool hidden;
101 
102  // this is related to an internal expression
103  bool internal;
104 
105  // we categorize
108 
109  // The instruction that created this step
110  // (function calls are in the caller, function returns are in the callee)
113 
114  // this transition done by given thread number
115  unsigned thread_nr;
116 
117  // for assume, assert, goto
120 
121  // for assert
123  std::string comment;
124 
125  // the full, original lhs expression, after dereferencing
127 
128  // the object being assigned
130 
131  // A constant with the new value of the lhs
133 
134  // for INPUT/OUTPUT
136  typedef std::list<exprt> io_argst;
138  bool formatted;
139 
140  // for function calls
142 
143  // for function call
144  std::vector<exprt> function_arguments;
145 
147  void output(
148  const class namespacet &ns,
149  std::ostream &out) const;
150 
152  step_nr(0),
153  type(typet::NONE),
154  hidden(false),
155  internal(false),
157  thread_nr(0),
158  cond_value(false),
159  formatted(false)
160  {
161  full_lhs.make_nil();
164  }
165 
168  void merge_ireps(merge_irept &dest);
169 };
170 
175 {
176 public:
177  typedef std::list<goto_trace_stept> stepst;
179 
180  void clear()
181  {
182  steps.clear();
183  }
184 
186  void output(
187  const class namespacet &ns,
188  std::ostream &out) const;
189 
190  void swap(goto_tracet &other)
191  {
192  other.steps.swap(steps);
193  }
194 
196  void add_step(const goto_trace_stept &step)
197  {
198  steps.push_back(step);
199  }
200 
204  {
205  return steps.back();
206  }
207 
209  {
210  return steps.back();
211  }
212 
214  std::set<irep_idt> get_failed_property_ids() const;
215 };
216 
219 {
230  bool show_code;
235 
237 
238  explicit trace_optionst(const optionst &options)
239  {
240  json_full_lhs = options.get_bool_option("trace-json-extended");
241  hex_representation = options.get_bool_option("trace-hex");
243  show_function_calls = options.get_bool_option("trace-show-function-calls");
244  show_code = options.get_bool_option("trace-show-code");
245  compact_trace = options.get_bool_option("compact-trace");
246  stack_trace = options.get_bool_option("stack-trace");
247  };
248 
249 private:
251  {
252  json_full_lhs = false;
253  hex_representation = false;
254  base_prefix = false;
255  show_function_calls = false;
256  show_code = false;
257  compact_trace = false;
258  stack_trace = false;
259  };
260 };
261 
263 void show_goto_trace(
264  messaget::mstreamt &out,
265  const namespacet &ns,
266  const goto_tracet &goto_trace,
267  const trace_optionst &trace_options = trace_optionst::default_options);
268 
269 #define OPT_GOTO_TRACE \
270  "(trace-json-extended)" \
271  "(trace-show-function-calls)" \
272  "(trace-show-code)" \
273  "(trace-hex)" \
274  "(compact-trace)" \
275  "(stack-trace)"
276 
277 #define HELP_GOTO_TRACE \
278  " --trace-json-extended add rawLhs property to trace\n" \
279  " --trace-show-function-calls show function calls in plain trace\n" \
280  " --trace-show-code show original code in plain trace\n" \
281  " --trace-hex represent plain trace values in hex\n" \
282  " --compact-trace give a compact trace\n" \
283  " --stack-trace give a stack trace only\n"
284 
285 #define PARSE_OPTIONS_GOTO_TRACE(cmdline, options) \
286  if(cmdline.isset("trace-json-extended")) \
287  options.set_option("trace-json-extended", true); \
288  if(cmdline.isset("trace-show-function-calls")) \
289  options.set_option("trace-show-function-calls", true); \
290  if(cmdline.isset("trace-show-code")) \
291  options.set_option("trace-show-code", true); \
292  if(cmdline.isset("trace-hex")) \
293  options.set_option("trace-hex", true); \
294  if(cmdline.isset("compact-trace")) \
295  options.set_option("compact-trace", true); \
296  if(cmdline.isset("stack-trace")) \
297  options.set_option("stack-trace", true);
298 
306 {
307 public:
308  const exprt &symbolic_pointer() const
309  {
310  return static_cast<const exprt &>(operands()[0]);
311  }
312 };
313 
314 template <>
316 {
317  return can_cast_expr<constant_exprt>(base) && base.operands().size() == 1;
318 }
319 
322 {
324  return static_cast<const goto_trace_constant_pointer_exprt &>(expr);
325 }
326 
327 #endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H
A constant literal expression.
Definition: std_expr.h:2753
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
operandst & operands()
Definition: expr.h:92
instructionst::const_iterator const_targett
Definition: goto_program.h:647
Variety of constant expression only used in the context of a GOTO trace, to give both the numeric val...
Definition: goto_trace.h:306
const exprt & symbolic_pointer() const
Definition: goto_trace.h:308
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
std::vector< exprt > function_arguments
Definition: goto_trace.h:144
irep_idt format_string
Definition: goto_trace.h:135
bool is_function_call() const
Definition: goto_trace.h:60
optionalt< symbol_exprt > get_lhs_object() const
Definition: goto_trace.cpp:51
bool is_spawn() const
Definition: goto_trace.h:69
bool is_memory_barrier() const
Definition: goto_trace.h:70
std::list< exprt > io_argst
Definition: goto_trace.h:136
bool is_assignment() const
Definition: goto_trace.h:55
bool is_atomic_begin() const
Definition: goto_trace.h:71
bool is_function_return() const
Definition: goto_trace.h:61
std::string comment
Definition: goto_trace.h:123
exprt full_lhs_value
Definition: goto_trace.h:132
goto_programt::const_targett pc
Definition: goto_trace.h:112
irep_idt function_id
Definition: goto_trace.h:111
io_argst io_args
Definition: goto_trace.h:137
void merge_ireps(merge_irept &dest)
Use dest to establish sharing among ireps.
Definition: goto_trace.cpp:139
unsigned thread_nr
Definition: goto_trace.h:115
bool is_goto() const
Definition: goto_trace.h:58
bool is_shared_write() const
Definition: goto_trace.h:68
irep_idt property_id
Definition: goto_trace.h:122
bool is_assume() const
Definition: goto_trace.h:56
bool is_atomic_end() const
Definition: goto_trace.h:72
bool is_assert() const
Definition: goto_trace.h:57
bool is_shared_read() const
Definition: goto_trace.h:67
irep_idt called_function
Definition: goto_trace.h:141
assignment_typet assignment_type
Definition: goto_trace.h:107
bool is_decl() const
Definition: goto_trace.h:65
bool is_dead() const
Definition: goto_trace.h:66
std::size_t step_nr
Number of the step in the trace.
Definition: goto_trace.h:53
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace step in ASCII to a given stream.
Definition: goto_trace.cpp:64
bool is_constraint() const
Definition: goto_trace.h:59
bool is_location() const
Definition: goto_trace.h:62
irep_idt io_id
Definition: goto_trace.h:135
bool is_output() const
Definition: goto_trace.h:63
bool is_input() const
Definition: goto_trace.h:64
Trace of a GOTO program.
Definition: goto_trace.h:175
void swap(goto_tracet &other)
Definition: goto_trace.h:190
goto_trace_stept & get_last_step()
Retrieves the final step in the trace for manipulation (used to fill a trace from code,...
Definition: goto_trace.h:203
stepst steps
Definition: goto_trace.h:178
const goto_trace_stept & get_last_step() const
Definition: goto_trace.h:208
void clear()
Definition: goto_trace.h:180
std::set< irep_idt > get_failed_property_ids() const
Returns the property IDs of all failed assertions in the trace.
Definition: goto_trace.cpp:800
void add_step(const goto_trace_stept &step)
Add a step at the end of the trace.
Definition: goto_trace.h:196
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace in ASCII to a given stream.
Definition: goto_trace.cpp:56
std::list< goto_trace_stept > stepst
Definition: goto_trace.h:177
void make_nil()
Definition: irep.h:465
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
The type of an expression, extends irept.
Definition: type.h:28
Concrete Goto Program.
void show_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &trace_options=trace_optionst::default_options)
Output the trace on the given stream out.
Definition: goto_trace.cpp:784
bool can_cast_expr< goto_trace_constant_pointer_exprt >(const exprt &base)
Definition: goto_trace.h:315
const goto_trace_constant_pointer_exprt & to_goto_trace_constant_pointer_expr(const exprt &expr)
Definition: goto_trace.h:321
nonstd::optional< T > optionalt
Definition: optional.h:35
Options.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:2775
Options for printing the trace using show_goto_trace.
Definition: goto_trace.h:219
static const trace_optionst default_options
Definition: goto_trace.h:236
bool json_full_lhs
Add rawLhs property to trace.
Definition: goto_trace.h:221
trace_optionst(const optionst &options)
Definition: goto_trace.h:238
bool hex_representation
Represent plain trace values in hex.
Definition: goto_trace.h:223
bool base_prefix
Use prefix (0b or 0x) for distinguishing the base of the representation.
Definition: goto_trace.h:226
bool show_code
Show original code in plain text trace.
Definition: goto_trace.h:230
bool compact_trace
Give a compact trace.
Definition: goto_trace.h:232
bool show_function_calls
Show function calls in plain text trace.
Definition: goto_trace.h:228
bool stack_trace
Give a stack trace only.
Definition: goto_trace.h:234