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 
31 {
32 public:
33  std::size_t step_nr;
34 
35  bool is_assignment() const { return type==typet::ASSIGNMENT; }
36  bool is_assume() const { return type==typet::ASSUME; }
37  bool is_assert() const { return type==typet::ASSERT; }
38  bool is_goto() const { return type==typet::GOTO; }
39  bool is_constraint() const { return type==typet::CONSTRAINT; }
40  bool is_function_call() const { return type==typet::FUNCTION_CALL; }
42  bool is_location() const { return type==typet::LOCATION; }
43  bool is_output() const { return type==typet::OUTPUT; }
44  bool is_input() const { return type==typet::INPUT; }
45  bool is_decl() const { return type==typet::DECL; }
46  bool is_dead() const { return type==typet::DEAD; }
47  bool is_shared_read() const { return type==typet::SHARED_READ; }
48  bool is_shared_write() const { return type==typet::SHARED_WRITE; }
49  bool is_spawn() const { return type==typet::SPAWN; }
50  bool is_memory_barrier() const { return type==typet::MEMORY_BARRIER; }
51  bool is_atomic_begin() const { return type==typet::ATOMIC_BEGIN; }
52  bool is_atomic_end() const { return type==typet::ATOMIC_END; }
53 
54  enum class typet
55  {
56  NONE,
57  ASSIGNMENT,
58  ASSUME,
59  ASSERT,
60  GOTO,
61  LOCATION,
62  INPUT,
63  OUTPUT,
64  DECL,
65  DEAD,
68  CONSTRAINT,
71  SPAWN,
75  };
76 
78 
79  // we may choose to hide a step
80  bool hidden;
81 
82  // this is related to an internal expression
83  bool internal;
84 
85  // we categorize
88 
89  // The instruction that created this step
90  // (function calls are in the caller, function returns are in the callee)
91  irep_idt function;
93 
94  // this transition done by given thread number
95  unsigned thread_nr;
96 
97  // for assume, assert, goto
98  bool cond_value;
100 
101  // for assert
102  std::string comment;
103 
104  // the full, original lhs expression, after dereferencing
106 
107  // the object being assigned
109 
110  // A constant with the new value of the lhs
112 
113  // for INPUT/OUTPUT
115  typedef std::list<exprt> io_argst;
117  bool formatted;
118 
119  // for function calls
121 
122  // for function call
123  std::vector<exprt> function_arguments;
124 
127  void output(
128  const class namespacet &ns,
129  std::ostream &out) const;
130 
132  step_nr(0),
133  type(typet::NONE),
134  hidden(false),
135  internal(false),
137  thread_nr(0),
138  cond_value(false),
139  formatted(false)
140  {
141  full_lhs.make_nil();
144  }
145 };
146 
151 {
152 public:
153  typedef std::list<goto_trace_stept> stepst;
155 
157 
158  void clear()
159  {
160  mode.clear();
161  steps.clear();
162  }
163 
166  void output(
167  const class namespacet &ns,
168  std::ostream &out) const;
169 
170  void swap(goto_tracet &other)
171  {
172  other.steps.swap(steps);
173  other.mode.swap(mode);
174  }
175 
176  void add_step(const goto_trace_stept &step)
177  {
178  steps.push_back(step);
179  }
180 
181  // retrieves the final step in the trace for manipulation
182  // (used to fill a trace from code, hence non-const)
184  {
185  return steps.back();
186  }
187 
188  // delete all steps after (not including) s
189  void trim_after(stepst::iterator s)
190  {
191  PRECONDITION(s != steps.end());
192  steps.erase(++s, steps.end());
193  }
194 };
195 
197 {
202  bool show_code;
204 
206 
207  explicit trace_optionst(const optionst &options)
208  {
209  json_full_lhs = options.get_bool_option("trace-json-extended");
210  hex_representation = options.get_bool_option("trace-hex");
212  show_function_calls = options.get_bool_option("trace-show-function-calls");
213  show_code = options.get_bool_option("trace-show-code");
214  stack_trace = options.get_bool_option("stack-trace");
215  };
216 
217 private:
219  {
220  json_full_lhs = false;
221  hex_representation = false;
222  base_prefix = false;
223  show_function_calls = false;
224  show_code = false;
225  stack_trace = false;
226  };
227 };
228 
229 void show_goto_trace(
230  messaget::mstreamt &out,
231  const namespacet &,
232  const goto_tracet &);
233 
234 void show_goto_trace(
235  messaget::mstreamt &out,
236  const namespacet &,
237  const goto_tracet &,
238  const trace_optionst &);
239 
240 void trace_value(
241  messaget::mstreamt &out,
242  const namespacet &,
243  const optionalt<symbol_exprt> &lhs_object,
244  const exprt &full_lhs,
245  const exprt &value,
246  const trace_optionst &);
247 
248 #define OPT_GOTO_TRACE \
249  "(trace-json-extended)" \
250  "(trace-show-function-calls)" \
251  "(trace-show-code)" \
252  "(trace-hex)" \
253  "(stack-trace)"
254 
255 #define HELP_GOTO_TRACE \
256  " --trace-json-extended add rawLhs property to trace\n" \
257  " --trace-show-function-calls show function calls in plain trace\n" \
258  " --trace-show-code show original code in plain trace\n" \
259  " --trace-hex represent plain trace values in hex\n" \
260  " --stack-trace give a stack trace only\n"
261 
262 #define PARSE_OPTIONS_GOTO_TRACE(cmdline, options) \
263  if(cmdline.isset("trace-json-extended")) \
264  options.set_option("trace-json-extended", true); \
265  if(cmdline.isset("trace-show-function-calls")) \
266  options.set_option("trace-show-function-calls", true); \
267  if(cmdline.isset("trace-show-code")) \
268  options.set_option("trace-show-code", true); \
269  if(cmdline.isset("trace-hex")) \
270  options.set_option("trace-hex", true); \
271  if(cmdline.isset("stack-trace")) \
272  options.set_option("stack-trace", true);
273 
274 #endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H
The type of an expression, extends irept.
Definition: type.h:27
bool is_shared_write() const
Definition: goto_trace.h:48
std::vector< exprt > function_arguments
Definition: goto_trace.h:123
bool is_location() const
Definition: goto_trace.h:42
bool json_full_lhs
Definition: goto_trace.h:198
bool show_function_calls
Definition: goto_trace.h:201
bool is_goto() const
Definition: goto_trace.h:38
void trim_after(stepst::iterator s)
Definition: goto_trace.h:189
bool is_input() const
Definition: goto_trace.h:44
io_argst io_args
Definition: goto_trace.h:116
void clear()
Definition: goto_trace.h:158
std::list< exprt > io_argst
Definition: goto_trace.h:115
void trace_value(messaget::mstreamt &out, const namespacet &, const optionalt< symbol_exprt > &lhs_object, const exprt &full_lhs, const exprt &value, const trace_optionst &)
Definition: goto_trace.cpp:254
std::list< goto_trace_stept > stepst
Definition: goto_trace.h:153
goto_trace_stept & get_last_step()
Definition: goto_trace.h:183
void swap(goto_tracet &other)
Definition: goto_trace.h:170
std::size_t step_nr
Definition: goto_trace.h:33
bool is_shared_read() const
Definition: goto_trace.h:47
TO_BE_DOCUMENTED.
Definition: goto_trace.h:30
stepst steps
Definition: goto_trace.h:154
goto_programt::const_targett pc
Definition: goto_trace.h:92
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
void add_step(const goto_trace_stept &step)
Definition: goto_trace.h:176
irep_idt io_id
Definition: goto_trace.h:114
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
bool is_output() const
Definition: goto_trace.h:43
bool is_assume() const
Definition: goto_trace.h:36
nonstd::optional< T > optionalt
Definition: optional.h:35
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
unsigned thread_nr
Definition: goto_trace.h:95
instructionst::const_iterator const_targett
Definition: goto_program.h:415
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
bool is_atomic_end() const
Definition: goto_trace.h:52
optionalt< symbol_exprt > get_lhs_object() const
Definition: goto_trace.cpp:40
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
bool is_function_return() const
Definition: goto_trace.h:41
bool is_atomic_begin() const
Definition: goto_trace.h:51
void swap(dstringt &b)
Definition: dstring.h:132
void clear()
Definition: dstring.h:129
Base class for all expressions.
Definition: expr.h:54
trace_optionst(const optionst &options)
Definition: goto_trace.h:207
exprt full_lhs_value
Definition: goto_trace.h:111
bool is_constraint() const
Definition: goto_trace.h:39
bool is_memory_barrier() const
Definition: goto_trace.h:50
std::string comment
Definition: goto_trace.h:102
void make_nil()
Definition: irep.h:315
bool is_assert() const
Definition: goto_trace.h:37
bool is_decl() const
Definition: goto_trace.h:45
bool is_assignment() const
Definition: goto_trace.h:35
bool is_dead() const
Definition: goto_trace.h:46
Options.
TO_BE_DOCUMENTED.
Definition: goto_trace.h:150
static const trace_optionst default_options
Definition: goto_trace.h:205
irep_idt mode
Definition: goto_trace.h:156
irep_idt format_string
Definition: goto_trace.h:114
void show_goto_trace(messaget::mstreamt &out, const namespacet &, const goto_tracet &)
Definition: goto_trace.cpp:630
Concrete Goto Program.
bool is_spawn() const
Definition: goto_trace.h:49
assignment_typet assignment_type
Definition: goto_trace.h:87