cprover
Loading...
Searching...
No Matches
goto_trace.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Traces of GOTO Programs
4
5Author: Daniel Kroening
6
7Date: 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
25class merge_irept;
26
50{
51public:
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; }
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,
78 ASSUME,
79 ASSERT,
80 GOTO,
82 INPUT,
83 OUTPUT,
84 DECL,
85 DEAD,
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
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;
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 {
164 }
165
168 void merge_ireps(merge_irept &dest);
169};
170
175{
176public:
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{
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
249private:
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
263void show_goto_trace(
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{
307public:
308 const exprt &symbolic_pointer() const
309 {
310 return static_cast<const exprt &>(operands()[0]);
311 }
312};
313
314template <>
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:2807
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
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
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
goto_programt::const_targett pc
Definition goto_trace.h:112
irep_idt function_id
Definition goto_trace.h:111
void merge_ireps(merge_irept &dest)
Use dest to establish sharing among ireps.
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.
bool is_constraint() const
Definition goto_trace.h:59
bool is_location() const
Definition goto_trace.h:62
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
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.
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.
std::list< goto_trace_stept > stepst
Definition goto_trace.h:177
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
void make_nil()
Definition irep.h:454
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:29
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.
const goto_trace_constant_pointer_exprt & to_goto_trace_constant_pointer_expr(const exprt &expr)
Definition goto_trace.h:321
bool can_cast_expr< goto_trace_constant_pointer_exprt >(const exprt &base)
Definition goto_trace.h:315
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:2829
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