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 
27 class merge_irept;
28 
52 {
53 public:
55  std::size_t step_nr;
56 
57  bool is_assignment() const { return type==typet::ASSIGNMENT; }
58  bool is_assume() const { return type==typet::ASSUME; }
59  bool is_assert() const { return type==typet::ASSERT; }
60  bool is_goto() const { return type==typet::GOTO; }
61  bool is_constraint() const { return type==typet::CONSTRAINT; }
62  bool is_function_call() const { return type==typet::FUNCTION_CALL; }
64  bool is_location() const { return type==typet::LOCATION; }
65  bool is_output() const { return type==typet::OUTPUT; }
66  bool is_input() const { return type==typet::INPUT; }
67  bool is_decl() const { return type==typet::DECL; }
68  bool is_dead() const { return type==typet::DEAD; }
69  bool is_shared_read() const { return type==typet::SHARED_READ; }
70  bool is_shared_write() const { return type==typet::SHARED_WRITE; }
71  bool is_spawn() const { return type==typet::SPAWN; }
72  bool is_memory_barrier() const { return type==typet::MEMORY_BARRIER; }
73  bool is_atomic_begin() const { return type==typet::ATOMIC_BEGIN; }
74  bool is_atomic_end() const { return type==typet::ATOMIC_END; }
75 
76  enum class typet
77  {
78  NONE,
79  ASSIGNMENT,
80  ASSUME,
81  ASSERT,
82  GOTO,
83  LOCATION,
84  INPUT,
85  OUTPUT,
86  DECL,
87  DEAD,
90  CONSTRAINT,
93  SPAWN,
97  };
98 
100 
101  // we may choose to hide a step
102  bool hidden;
103 
104  // this is related to an internal expression
105  bool internal;
106 
107  // we categorize
110 
111  // The instruction that created this step
112  // (function calls are in the caller, function returns are in the callee)
115 
116  // this transition done by given thread number
117  unsigned thread_nr;
118 
119  // for assume, assert, goto
122 
123  // for assert
125  std::string comment;
126 
127  // the full, original lhs expression, after dereferencing
129 
130  // the object being assigned
132 
133  // A constant with the new value of the lhs
135 
136  // for INPUT/OUTPUT
138  typedef std::list<exprt> io_argst;
140  bool formatted;
141 
142  // for function calls
144 
145  // for function call
146  std::vector<exprt> function_arguments;
147 
149  void output(
150  const class namespacet &ns,
151  std::ostream &out) const;
152 
154  step_nr(0),
155  type(typet::NONE),
156  hidden(false),
157  internal(false),
159  thread_nr(0),
160  cond_value(false),
161  formatted(false)
162  {
163  full_lhs.make_nil();
166  }
167 
170  void merge_ireps(merge_irept &dest);
171 };
172 
177 {
178 public:
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 {
232  bool show_code;
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 
251 private:
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 
265 void show_goto_trace(
266  messaget::mstreamt &out,
267  const namespacet &ns,
268  const goto_tracet &goto_trace,
269  const trace_optionst &trace_options = trace_optionst::default_options);
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  " --trace-json-extended add rawLhs property to trace\n" \
281  " --trace-show-function-calls show function calls in plain trace\n" \
282  " --trace-show-code show original code in plain trace\n" \
283  " --trace-hex represent plain trace values in hex\n" \
284  " --compact-trace give a compact trace\n" \
285  " --stack-trace 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 
308 {
309 public:
310  const exprt &symbolic_pointer() const
311  {
312  return static_cast<const exprt &>(operands()[0]);
313  }
314 };
315 
316 template <>
318 {
319  return can_cast_expr<constant_exprt>(base) && base.operands().size() == 1;
320 }
321 
324 {
326  return static_cast<const goto_trace_constant_pointer_exprt &>(expr);
327 }
328 
329 #endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H
can_cast_expr< goto_trace_constant_pointer_exprt >
bool can_cast_expr< goto_trace_constant_pointer_exprt >(const exprt &base)
Definition: goto_trace.h:317
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
trace_optionst::compact_trace
bool compact_trace
Give a compact trace.
Definition: goto_trace.h:234
goto_tracet::get_failed_property_ids
std::set< irep_idt > get_failed_property_ids() const
Returns the property IDs of all failed assertions in the trace.
Definition: goto_trace.cpp:799
goto_trace_stept::typet::LOCATION
@ LOCATION
goto_trace_stept::full_lhs_value
exprt full_lhs_value
Definition: goto_trace.h:134
goto_trace_stept::formatted
bool formatted
Definition: goto_trace.h:140
goto_trace_stept::get_lhs_object
optionalt< symbol_exprt > get_lhs_object() const
Definition: goto_trace.cpp:51
goto_trace_stept::comment
std::string comment
Definition: goto_trace.h:125
goto_trace_stept::typet::ASSUME
@ ASSUME
goto_trace_stept::is_memory_barrier
bool is_memory_barrier() const
Definition: goto_trace.h:72
optionst
Definition: options.h:23
irept::make_nil
void make_nil()
Definition: irep.h:465
trace_optionst::base_prefix
bool base_prefix
Use prefix (0b or 0x) for distinguishing the base of the representation.
Definition: goto_trace.h:228
typet
The type of an expression, extends irept.
Definition: type.h:28
goto_trace_stept::assignment_typet::STATE
@ STATE
goto_trace_stept::internal
bool internal
Definition: goto_trace.h:105
goto_trace_stept::is_shared_write
bool is_shared_write() const
Definition: goto_trace.h:70
trace_optionst::show_code
bool show_code
Show original code in plain text trace.
Definition: goto_trace.h:232
show_goto_trace
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:783
trace_optionst::trace_optionst
trace_optionst()
Definition: goto_trace.h:252
goto_trace_stept::is_assert
bool is_assert() const
Definition: goto_trace.h:59
goto_trace_constant_pointer_exprt
Variety of constant expression only used in the context of a GOTO trace, to give both the numeric val...
Definition: goto_trace.h:308
goto_trace_stept::type
typet type
Definition: goto_trace.h:99
goto_trace_stept::is_spawn
bool is_spawn() const
Definition: goto_trace.h:71
goto_tracet::steps
stepst steps
Definition: goto_trace.h:180
exprt
Base class for all expressions.
Definition: expr.h:54
goto_tracet::clear
void clear()
Definition: goto_trace.h:182
goto_trace_stept::is_atomic_begin
bool is_atomic_begin() const
Definition: goto_trace.h:73
goto_trace_constant_pointer_exprt::symbolic_pointer
const exprt & symbolic_pointer() const
Definition: goto_trace.h:310
options.h
Options.
goto_trace_stept::is_input
bool is_input() const
Definition: goto_trace.h:66
goto_trace_stept
Step of the trace of a GOTO program.
Definition: goto_trace.h:52
goto_trace_stept::is_function_call
bool is_function_call() const
Definition: goto_trace.h:62
namespace.h
goto_trace_stept::called_function
irep_idt called_function
Definition: goto_trace.h:143
goto_trace_stept::is_decl
bool is_decl() const
Definition: goto_trace.h:67
goto_trace_stept::is_assignment
bool is_assignment() const
Definition: goto_trace.h:57
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
goto_trace_stept::typet::OUTPUT
@ OUTPUT
goto_trace_stept::typet::FUNCTION_RETURN
@ FUNCTION_RETURN
goto_trace_stept::assignment_typet
assignment_typet
Definition: goto_trace.h:108
goto_trace_stept::is_function_return
bool is_function_return() const
Definition: goto_trace.h:63
goto_trace_stept::typet::DECL
@ DECL
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:64
goto_trace_stept::typet::ASSERT
@ ASSERT
goto_trace_stept::cond_expr
exprt cond_expr
Definition: goto_trace.h:121
goto_trace_stept::typet::NONE
@ NONE
goto_trace_stept::step_nr
std::size_t step_nr
Number of the step in the trace.
Definition: goto_trace.h:55
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
goto_trace_stept::full_lhs
exprt full_lhs
Definition: goto_trace.h:128
goto_trace_stept::function_arguments
std::vector< exprt > function_arguments
Definition: goto_trace.h:146
goto_trace_stept::pc
goto_programt::const_targett pc
Definition: goto_trace.h:114
goto_trace_stept::io_argst
std::list< exprt > io_argst
Definition: goto_trace.h:138
goto_trace_stept::is_shared_read
bool is_shared_read() const
Definition: goto_trace.h:69
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:56
goto_trace_stept::is_atomic_end
bool is_atomic_end() const
Definition: goto_trace.h:74
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:117
goto_trace_stept::typet::SPAWN
@ SPAWN
goto_program.h
Concrete Goto Program.
goto_trace_stept::typet::MEMORY_BARRIER
@ MEMORY_BARRIER
goto_trace_stept::typet::SHARED_WRITE
@ SHARED_WRITE
goto_trace_stept::merge_ireps
void merge_ireps(merge_irept &dest)
Use dest to establish sharing among ireps.
Definition: goto_trace.cpp:139
goto_trace_stept::property_id
irep_idt property_id
Definition: goto_trace.h:124
goto_trace_stept::cond_value
bool cond_value
Definition: goto_trace.h:120
ssa_expr.h
trace_optionst::hex_representation
bool hex_representation
Represent plain trace values in hex.
Definition: goto_trace.h:225
trace_optionst::stack_trace
bool stack_trace
Give a stack trace only.
Definition: goto_trace.h:236
goto_trace_stept::typet::GOTO
@ GOTO
trace_optionst::trace_optionst
trace_optionst(const optionst &options)
Definition: goto_trace.h:240
merge_irept
Definition: merge_irep.h:106
goto_trace_stept::is_location
bool is_location() const
Definition: goto_trace.h:64
goto_trace_stept::goto_trace_stept
goto_trace_stept()
Definition: goto_trace.h:153
trace_optionst
Options for printing the trace using show_goto_trace.
Definition: goto_trace.h:221
trace_optionst::show_function_calls
bool show_function_calls
Show function calls in plain text trace.
Definition: goto_trace.h:230
goto_trace_stept::assignment_type
assignment_typet assignment_type
Definition: goto_trace.h:109
trace_optionst::default_options
static const trace_optionst default_options
Definition: goto_trace.h:238
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
goto_trace_stept::typet::ATOMIC_BEGIN
@ ATOMIC_BEGIN
goto_trace_stept::hidden
bool hidden
Definition: goto_trace.h:102
goto_trace_stept::format_string
irep_idt format_string
Definition: goto_trace.h:137
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:177
trace_optionst::json_full_lhs
bool json_full_lhs
Add rawLhs property to trace.
Definition: goto_trace.h:223
to_goto_trace_constant_pointer_expr
const goto_trace_constant_pointer_exprt & to_goto_trace_constant_pointer_expr(const exprt &expr)
Definition: goto_trace.h:323
messaget::mstreamt
Definition: message.h:224
goto_trace_stept::is_assume
bool is_assume() const
Definition: goto_trace.h:58
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:564
goto_trace_stept::is_dead
bool is_dead() const
Definition: goto_trace.h:68
can_cast_expr< constant_exprt >
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:2689
exprt::operands
operandst & operands()
Definition: expr.h:96
goto_trace_stept::typet::SHARED_READ
@ SHARED_READ
goto_tracet::swap
void swap(goto_tracet &other)
Definition: goto_trace.h:192
goto_tracet::get_last_step
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
goto_trace_stept::is_goto
bool is_goto() const
Definition: goto_trace.h:60
goto_trace_stept::is_constraint
bool is_constraint() const
Definition: goto_trace.h:61
goto_trace_stept::io_id
irep_idt io_id
Definition: goto_trace.h:137
goto_trace_stept::typet::FUNCTION_CALL
@ FUNCTION_CALL
goto_trace_stept::is_output
bool is_output() const
Definition: goto_trace.h:65
goto_tracet::stepst
std::list< goto_trace_stept > stepst
Definition: goto_trace.h:179
message.h
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
goto_trace_stept::io_args
io_argst io_args
Definition: goto_trace.h:139
goto_trace_stept::function_id
irep_idt function_id
Definition: goto_trace.h:113
goto_tracet::add_step
void add_step(const goto_trace_stept &step)
Add a step at the end of the trace.
Definition: goto_trace.h:198
goto_trace_stept::typet::DEAD
@ DEAD
goto_trace_stept::typet::CONSTRAINT
@ CONSTRAINT
goto_tracet::get_last_step
const goto_trace_stept & get_last_step() const
Definition: goto_trace.h:210