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/namespace.h>
22 #include <util/options.h>
23 #include <util/ssa_expr.h>
24 
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 };
166 
171 {
172 public:
173  typedef std::list<goto_trace_stept> stepst;
175 
176  void clear()
177  {
178  steps.clear();
179  }
180 
182  void output(
183  const class namespacet &ns,
184  std::ostream &out) const;
185 
186  void swap(goto_tracet &other)
187  {
188  other.steps.swap(steps);
189  }
190 
192  void add_step(const goto_trace_stept &step)
193  {
194  steps.push_back(step);
195  }
196 
200  {
201  return steps.back();
202  }
203 
205  {
206  return steps.back();
207  }
208 
210  std::set<irep_idt> get_failed_property_ids() const;
211 };
212 
215 {
226  bool show_code;
231 
233 
234  explicit trace_optionst(const optionst &options)
235  {
236  json_full_lhs = options.get_bool_option("trace-json-extended");
237  hex_representation = options.get_bool_option("trace-hex");
239  show_function_calls = options.get_bool_option("trace-show-function-calls");
240  show_code = options.get_bool_option("trace-show-code");
241  compact_trace = options.get_bool_option("compact-trace");
242  stack_trace = options.get_bool_option("stack-trace");
243  };
244 
245 private:
247  {
248  json_full_lhs = false;
249  hex_representation = false;
250  base_prefix = false;
251  show_function_calls = false;
252  show_code = false;
253  compact_trace = false;
254  stack_trace = false;
255  };
256 };
257 
259 void show_goto_trace(
260  messaget::mstreamt &out,
261  const namespacet &ns,
262  const goto_tracet &goto_trace,
263  const trace_optionst &trace_options = trace_optionst::default_options);
264 
265 #define OPT_GOTO_TRACE \
266  "(trace-json-extended)" \
267  "(trace-show-function-calls)" \
268  "(trace-show-code)" \
269  "(trace-hex)" \
270  "(compact-trace)" \
271  "(stack-trace)"
272 
273 #define HELP_GOTO_TRACE \
274  " --trace-json-extended add rawLhs property to trace\n" \
275  " --trace-show-function-calls show function calls in plain trace\n" \
276  " --trace-show-code show original code in plain trace\n" \
277  " --trace-hex represent plain trace values in hex\n" \
278  " --compact-trace give a compact trace\n" \
279  " --stack-trace give a stack trace only\n"
280 
281 #define PARSE_OPTIONS_GOTO_TRACE(cmdline, options) \
282  if(cmdline.isset("trace-json-extended")) \
283  options.set_option("trace-json-extended", true); \
284  if(cmdline.isset("trace-show-function-calls")) \
285  options.set_option("trace-show-function-calls", true); \
286  if(cmdline.isset("trace-show-code")) \
287  options.set_option("trace-show-code", true); \
288  if(cmdline.isset("trace-hex")) \
289  options.set_option("trace-hex", true); \
290  if(cmdline.isset("compact-trace")) \
291  options.set_option("compact-trace", true); \
292  if(cmdline.isset("stack-trace")) \
293  options.set_option("stack-trace", true);
294 
295 #endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H
The type of an expression, extends irept.
Definition: type.h:28
bool is_shared_write() const
Definition: goto_trace.h:68
std::vector< exprt > function_arguments
Definition: goto_trace.h:144
bool is_location() const
Definition: goto_trace.h:62
bool json_full_lhs
Add rawLhs property to trace.
Definition: goto_trace.h:217
bool show_function_calls
Show function calls in plain text trace.
Definition: goto_trace.h:224
bool is_goto() const
Definition: goto_trace.h:58
bool base_prefix
Use prefix (0b or 0x) for distinguishing the base of the representation.
Definition: goto_trace.h:222
bool is_input() const
Definition: goto_trace.h:64
io_argst io_args
Definition: goto_trace.h:137
void clear()
Definition: goto_trace.h:176
std::list< exprt > io_argst
Definition: goto_trace.h:136
std::list< goto_trace_stept > stepst
Definition: goto_trace.h:173
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:199
void swap(goto_tracet &other)
Definition: goto_trace.h:186
std::size_t step_nr
Number of the step in the trace.
Definition: goto_trace.h:53
bool is_shared_read() const
Definition: goto_trace.h:67
Step of the trace of a GOTO program.
Definition: goto_trace.h:49
stepst steps
Definition: goto_trace.h:174
goto_programt::const_targett pc
Definition: goto_trace.h:112
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace in ASCII to a given stream.
Definition: goto_trace.cpp:54
irep_idt called_function
Definition: goto_trace.h:141
void add_step(const goto_trace_stept &step)
Add a step at the end of the trace.
Definition: goto_trace.h:192
std::set< irep_idt > get_failed_property_ids() const
Returns the property IDs of all failed assertions in the trace.
Definition: goto_trace.cpp:784
bool stack_trace
Give a stack trace only.
Definition: goto_trace.h:230
irep_idt io_id
Definition: goto_trace.h:135
Options for printing the trace using show_goto_trace.
Definition: goto_trace.h:214
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace step in ASCII to a given stream.
Definition: goto_trace.cpp:62
bool is_function_call() const
Definition: goto_trace.h:60
bool is_output() const
Definition: goto_trace.h:63
bool is_assume() const
Definition: goto_trace.h:56
bool show_code
Show original code in plain text trace.
Definition: goto_trace.h:226
nonstd::optional< T > optionalt
Definition: optional.h:35
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
unsigned thread_nr
Definition: goto_trace.h:115
instructionst::const_iterator const_targett
Definition: goto_program.h:580
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool is_atomic_end() const
Definition: goto_trace.h:72
optionalt< symbol_exprt > get_lhs_object() const
Definition: goto_trace.cpp:49
irep_idt property_id
Definition: goto_trace.h:122
bool hex_representation
Represent plain trace values in hex.
Definition: goto_trace.h:219
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:36
bool is_function_return() const
Definition: goto_trace.h:61
bool is_atomic_begin() const
Definition: goto_trace.h:71
const goto_trace_stept & get_last_step() const
Definition: goto_trace.h:204
bool compact_trace
Give a compact trace.
Definition: goto_trace.h:228
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:768
Base class for all expressions.
Definition: expr.h:52
trace_optionst(const optionst &options)
Definition: goto_trace.h:234
exprt full_lhs_value
Definition: goto_trace.h:132
bool is_constraint() const
Definition: goto_trace.h:59
bool is_memory_barrier() const
Definition: goto_trace.h:70
std::string comment
Definition: goto_trace.h:123
void make_nil()
Definition: irep.h:475
irep_idt function_id
Definition: goto_trace.h:111
bool is_assert() const
Definition: goto_trace.h:57
bool is_decl() const
Definition: goto_trace.h:65
bool is_assignment() const
Definition: goto_trace.h:55
bool is_dead() const
Definition: goto_trace.h:66
Options.
Trace of a GOTO program.
Definition: goto_trace.h:170
static const trace_optionst default_options
Definition: goto_trace.h:232
irep_idt format_string
Definition: goto_trace.h:135
Concrete Goto Program.
bool is_spawn() const
Definition: goto_trace.h:69
assignment_typet assignment_type
Definition: goto_trace.h:107