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;
205 
207 
208  explicit trace_optionst(const optionst &options)
209  {
210  json_full_lhs = options.get_bool_option("trace-json-extended");
211  hex_representation = options.get_bool_option("trace-hex");
213  show_function_calls = options.get_bool_option("trace-show-function-calls");
214  show_code = options.get_bool_option("trace-show-code");
215  compact_trace = options.get_bool_option("compact-trace");
216  stack_trace = options.get_bool_option("stack-trace");
217  };
218 
219 private:
221  {
222  json_full_lhs = false;
223  hex_representation = false;
224  base_prefix = false;
225  show_function_calls = false;
226  show_code = false;
227  compact_trace = false;
228  stack_trace = false;
229  };
230 };
231 
232 void show_goto_trace(
233  messaget::mstreamt &out,
234  const namespacet &,
235  const goto_tracet &);
236 
237 void show_goto_trace(
238  messaget::mstreamt &out,
239  const namespacet &,
240  const goto_tracet &,
241  const trace_optionst &);
242 
243 void trace_value(
244  messaget::mstreamt &out,
245  const namespacet &,
246  const optionalt<symbol_exprt> &lhs_object,
247  const exprt &full_lhs,
248  const exprt &value,
249  const trace_optionst &);
250 
251 #define OPT_GOTO_TRACE \
252  "(trace-json-extended)" \
253  "(trace-show-function-calls)" \
254  "(trace-show-code)" \
255  "(trace-hex)" \
256  "(compact-trace)" \
257  "(stack-trace)"
258 
259 #define HELP_GOTO_TRACE \
260  " --trace-json-extended add rawLhs property to trace\n" \
261  " --trace-show-function-calls show function calls in plain trace\n" \
262  " --trace-show-code show original code in plain trace\n" \
263  " --trace-hex represent plain trace values in hex\n" \
264  " --compact-trace give a compact trace\n" \
265  " --stack-trace give a stack trace only\n"
266 
267 #define PARSE_OPTIONS_GOTO_TRACE(cmdline, options) \
268  if(cmdline.isset("trace-json-extended")) \
269  options.set_option("trace-json-extended", true); \
270  if(cmdline.isset("trace-show-function-calls")) \
271  options.set_option("trace-show-function-calls", true); \
272  if(cmdline.isset("trace-show-code")) \
273  options.set_option("trace-show-code", true); \
274  if(cmdline.isset("trace-hex")) \
275  options.set_option("trace-hex", true); \
276  if(cmdline.isset("compact-trace")) \
277  options.set_option("compact-trace", true); \
278  if(cmdline.isset("stack-trace")) \
279  options.set_option("stack-trace", true);
280 
281 #endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
trace_optionst::compact_trace
bool compact_trace
Definition: goto_trace.h:203
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
goto_trace_stept::typet::LOCATION
@ LOCATION
goto_trace_stept::full_lhs_value
exprt full_lhs_value
Definition: goto_trace.h:111
goto_trace_stept::formatted
bool formatted
Definition: goto_trace.h:117
goto_trace_stept::get_lhs_object
optionalt< symbol_exprt > get_lhs_object() const
Definition: goto_trace.cpp:42
goto_trace_stept::comment
std::string comment
Definition: goto_trace.h:102
show_goto_trace
void show_goto_trace(messaget::mstreamt &out, const namespacet &, const goto_tracet &)
Definition: goto_trace.cpp:762
goto_trace_stept::typet::ASSUME
@ ASSUME
goto_tracet::trim_after
void trim_after(stepst::iterator s)
Definition: goto_trace.h:189
goto_trace_stept::is_memory_barrier
bool is_memory_barrier() const
Definition: goto_trace.h:50
optionst
Definition: options.h:22
irept::make_nil
void make_nil()
Definition: irep.h:315
trace_optionst::base_prefix
bool base_prefix
Definition: goto_trace.h:200
typet
The type of an expression, extends irept.
Definition: type.h:27
goto_trace_stept::assignment_typet::STATE
@ STATE
goto_trace_stept::internal
bool internal
Definition: goto_trace.h:83
goto_trace_stept::is_shared_write
bool is_shared_write() const
Definition: goto_trace.h:48
trace_optionst::show_code
bool show_code
Definition: goto_trace.h:202
trace_optionst::trace_optionst
trace_optionst()
Definition: goto_trace.h:220
goto_trace_stept::is_assert
bool is_assert() const
Definition: goto_trace.h:37
goto_trace_stept::type
typet type
Definition: goto_trace.h:77
goto_trace_stept::is_spawn
bool is_spawn() const
Definition: goto_trace.h:49
goto_tracet::steps
stepst steps
Definition: goto_trace.h:154
exprt
Base class for all expressions.
Definition: expr.h:54
goto_tracet::clear
void clear()
Definition: goto_trace.h:158
goto_trace_stept::is_atomic_begin
bool is_atomic_begin() const
Definition: goto_trace.h:51
options.h
goto_trace_stept::is_input
bool is_input() const
Definition: goto_trace.h:44
goto_trace_stept
TO_BE_DOCUMENTED.
Definition: goto_trace.h:30
goto_trace_stept::is_function_call
bool is_function_call() const
Definition: goto_trace.h:40
namespace.h
goto_trace_stept::called_function
irep_idt called_function
Definition: goto_trace.h:120
goto_trace_stept::is_decl
bool is_decl() const
Definition: goto_trace.h:45
goto_trace_stept::is_assignment
bool is_assignment() const
Definition: goto_trace.h:35
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
goto_trace_stept::typet::OUTPUT
@ OUTPUT
goto_trace_stept::typet::FUNCTION_RETURN
@ FUNCTION_RETURN
dstringt::swap
void swap(dstringt &b)
Definition: dstring.h:132
goto_trace_stept::assignment_typet
assignment_typet
Definition: goto_trace.h:86
goto_trace_stept::is_function_return
bool is_function_return() const
Definition: goto_trace.h:41
goto_trace_stept::typet::DECL
@ DECL
trace_value
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:256
goto_trace_stept::output
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace step in ASCII to a given stream
Definition: goto_trace.cpp:55
goto_trace_stept::typet::ASSERT
@ ASSERT
goto_trace_stept::cond_expr
exprt cond_expr
Definition: goto_trace.h:99
goto_trace_stept::typet::NONE
@ NONE
goto_trace_stept::step_nr
std::size_t step_nr
Definition: goto_trace.h:33
goto_tracet::mode
irep_idt mode
Definition: goto_trace.h:156
goto_trace_stept::full_lhs
exprt full_lhs
Definition: goto_trace.h:105
goto_trace_stept::function_arguments
std::vector< exprt > function_arguments
Definition: goto_trace.h:123
goto_trace_stept::pc
goto_programt::const_targett pc
Definition: goto_trace.h:92
goto_trace_stept::io_argst
std::list< exprt > io_argst
Definition: goto_trace.h:115
goto_trace_stept::is_shared_read
bool is_shared_read() const
Definition: goto_trace.h:47
goto_trace_stept::typet::ASSIGNMENT
@ ASSIGNMENT
goto_tracet::output
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace in ASCII to a given stream
Definition: goto_trace.cpp:47
goto_trace_stept::is_atomic_end
bool is_atomic_end() const
Definition: goto_trace.h:52
goto_trace_stept::assignment_typet::ACTUAL_PARAMETER
@ ACTUAL_PARAMETER
goto_trace_stept::typet::INPUT
@ INPUT
goto_trace_stept::typet::ATOMIC_END
@ ATOMIC_END
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
goto_trace_stept::thread_nr
unsigned thread_nr
Definition: goto_trace.h:95
goto_trace_stept::typet::SPAWN
@ SPAWN
dstringt::clear
void clear()
Definition: dstring.h:129
goto_program.h
goto_trace_stept::typet::MEMORY_BARRIER
@ MEMORY_BARRIER
goto_trace_stept::typet::SHARED_WRITE
@ SHARED_WRITE
goto_trace_stept::cond_value
bool cond_value
Definition: goto_trace.h:98
ssa_expr.h
trace_optionst::hex_representation
bool hex_representation
Definition: goto_trace.h:199
trace_optionst::stack_trace
bool stack_trace
Definition: goto_trace.h:204
goto_trace_stept::typet::GOTO
@ GOTO
trace_optionst::trace_optionst
trace_optionst(const optionst &options)
Definition: goto_trace.h:208
goto_trace_stept::is_location
bool is_location() const
Definition: goto_trace.h:42
goto_trace_stept::goto_trace_stept
goto_trace_stept()
Definition: goto_trace.h:131
trace_optionst
Definition: goto_trace.h:196
trace_optionst::show_function_calls
bool show_function_calls
Definition: goto_trace.h:201
goto_trace_stept::assignment_type
assignment_typet assignment_type
Definition: goto_trace.h:87
trace_optionst::default_options
static const trace_optionst default_options
Definition: goto_trace.h:206
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
goto_trace_stept::typet::ATOMIC_BEGIN
@ ATOMIC_BEGIN
goto_trace_stept::hidden
bool hidden
Definition: goto_trace.h:80
goto_trace_stept::format_string
irep_idt format_string
Definition: goto_trace.h:114
goto_tracet
TO_BE_DOCUMENTED.
Definition: goto_trace.h:150
trace_optionst::json_full_lhs
bool json_full_lhs
Definition: goto_trace.h:198
messaget::mstreamt
Definition: message.h:212
goto_trace_stept::is_assume
bool is_assume() const
Definition: goto_trace.h:36
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
goto_trace_stept::is_dead
bool is_dead() const
Definition: goto_trace.h:46
goto_trace_stept::typet::SHARED_READ
@ SHARED_READ
goto_tracet::swap
void swap(goto_tracet &other)
Definition: goto_trace.h:170
goto_tracet::get_last_step
goto_trace_stept & get_last_step()
Definition: goto_trace.h:183
goto_trace_stept::is_goto
bool is_goto() const
Definition: goto_trace.h:38
goto_trace_stept::is_constraint
bool is_constraint() const
Definition: goto_trace.h:39
goto_trace_stept::io_id
irep_idt io_id
Definition: goto_trace.h:114
goto_trace_stept::typet::FUNCTION_CALL
@ FUNCTION_CALL
goto_trace_stept::is_output
bool is_output() const
Definition: goto_trace.h:43
goto_tracet::stepst
std::list< goto_trace_stept > stepst
Definition: goto_trace.h:153
message.h
goto_trace_stept::io_args
io_argst io_args
Definition: goto_trace.h:116
goto_tracet::add_step
void add_step(const goto_trace_stept &step)
Definition: goto_trace.h:176
goto_trace_stept::typet::DEAD
@ DEAD
goto_trace_stept::typet::CONSTRAINT
@ CONSTRAINT