CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
121
122 // for assert
124 std::string comment;
125
126 // the full, original lhs expression, after dereferencing
128
129 // the object being assigned
130 std::optional<symbol_exprt> get_lhs_object() const;
131
132 // A constant with the new value of the lhs
134
135 // for INPUT/OUTPUT
137 typedef std::list<exprt> io_argst;
140
141 // for function calls
143
144 // for function call
145 std::vector<exprt> function_arguments;
146
148 void output(
149 const class namespacet &ns,
150 std::ostream &out) const;
151
167
170 void merge_ireps(merge_irept &dest);
171};
172
177{
178public:
179 typedef std::list<goto_trace_stept> stepst;
181
182 void clear()
183 {
184 steps.clear();
185 }
186
188 void output(
189 const class namespacet &ns,
190 std::ostream &out) const;
191
192 void swap(goto_tracet &other)
193 {
194 other.steps.swap(steps);
195 }
196
198 void add_step(const goto_trace_stept &step)
199 {
200 steps.push_back(step);
201 }
202
206 {
207 return steps.back();
208 }
209
211 {
212 return steps.back();
213 }
214
216 std::set<irep_idt> get_failed_property_ids() const;
217};
218
221{
237
239
240 explicit trace_optionst(const optionst &options)
241 {
242 json_full_lhs = options.get_bool_option("trace-json-extended");
243 hex_representation = options.get_bool_option("trace-hex");
245 show_function_calls = options.get_bool_option("trace-show-function-calls");
246 show_code = options.get_bool_option("trace-show-code");
247 compact_trace = options.get_bool_option("compact-trace");
248 stack_trace = options.get_bool_option("stack-trace");
249 };
250
251private:
253 {
254 json_full_lhs = false;
255 hex_representation = false;
256 base_prefix = false;
257 show_function_calls = false;
258 show_code = false;
259 compact_trace = false;
260 stack_trace = false;
261 };
262};
263
265void show_goto_trace(
267 const namespacet &ns,
268 const goto_tracet &goto_trace,
270
271#define OPT_GOTO_TRACE \
272 "(trace-json-extended)" \
273 "(trace-show-function-calls)" \
274 "(trace-show-code)" \
275 "(trace-hex)" \
276 "(compact-trace)" \
277 "(stack-trace)"
278
279#define HELP_GOTO_TRACE \
280 " {y--trace-json-extended} \t add rawLhs property to trace\n" \
281 " {y--trace-show-function-calls} \t show function calls in plain trace\n" \
282 " {y--trace-show-code} \t show original code in plain trace\n" \
283 " {y--trace-hex} \t represent plain trace values in hex\n" \
284 " {y--compact-trace} \t give a compact trace\n" \
285 " {y--stack-trace} \t give a stack trace only\n"
286
287#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options) \
288 if(cmdline.isset("trace-json-extended")) \
289 options.set_option("trace-json-extended", true); \
290 if(cmdline.isset("trace-show-function-calls")) \
291 options.set_option("trace-show-function-calls", true); \
292 if(cmdline.isset("trace-show-code")) \
293 options.set_option("trace-show-code", true); \
294 if(cmdline.isset("trace-hex")) \
295 options.set_option("trace-hex", true); \
296 if(cmdline.isset("compact-trace")) \
297 options.set_option("compact-trace", true); \
298 if(cmdline.isset("stack-trace")) \
299 options.set_option("stack-trace", true);
300
301#endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
instructionst::const_iterator const_targett
Step of the trace of a GOTO program.
Definition goto_trace.h:50
std::vector< exprt > function_arguments
Definition goto_trace.h:145
irep_idt format_string
Definition goto_trace.h:136
bool is_function_call() const
Definition goto_trace.h:60
exprt original_condition
Definition goto_trace.h:120
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:137
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:124
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:123
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:142
assignment_typet assignment_type
Definition goto_trace.h:107
std::optional< symbol_exprt > get_lhs_object() const
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:177
void swap(goto_tracet &other)
Definition goto_trace.h:192
stepst steps
Definition goto_trace.h:180
const goto_trace_stept & get_last_step() const
Definition goto_trace.h:210
void clear()
Definition goto_trace.h:182
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:198
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:179
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:205
void make_nil()
Definition irep.h:446
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.
Options.
Options for printing the trace using show_goto_trace.
Definition goto_trace.h:221
static const trace_optionst default_options
Definition goto_trace.h:238
bool json_full_lhs
Add rawLhs property to trace.
Definition goto_trace.h:223
trace_optionst(const optionst &options)
Definition goto_trace.h:240
bool hex_representation
Represent plain trace values in hex.
Definition goto_trace.h:225
bool base_prefix
Use prefix (0b or 0x) for distinguishing the base of the representation.
Definition goto_trace.h:228
bool show_code
Show original code in plain text trace.
Definition goto_trace.h:232
bool compact_trace
Give a compact trace.
Definition goto_trace.h:234
bool show_function_calls
Show function calls in plain text trace.
Definition goto_trace.h:230
bool stack_trace
Give a stack trace only.
Definition goto_trace.h:236