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 
24 #include <iosfwd>
25 #include <vector>
26 
27 #include <util/namespace.h>
28 #include <util/options.h>
29 #include <util/ssa_expr.h>
30 
32 
37 {
38 public:
39  std::size_t step_nr;
40 
41  bool is_assignment() const { return type==typet::ASSIGNMENT; }
42  bool is_assume() const { return type==typet::ASSUME; }
43  bool is_assert() const { return type==typet::ASSERT; }
44  bool is_goto() const { return type==typet::GOTO; }
45  bool is_constraint() const { return type==typet::CONSTRAINT; }
46  bool is_function_call() const { return type==typet::FUNCTION_CALL; }
48  bool is_location() const { return type==typet::LOCATION; }
49  bool is_output() const { return type==typet::OUTPUT; }
50  bool is_input() const { return type==typet::INPUT; }
51  bool is_decl() const { return type==typet::DECL; }
52  bool is_dead() const { return type==typet::DEAD; }
53  bool is_shared_read() const { return type==typet::SHARED_READ; }
54  bool is_shared_write() const { return type==typet::SHARED_WRITE; }
55  bool is_spawn() const { return type==typet::SPAWN; }
56  bool is_memory_barrier() const { return type==typet::MEMORY_BARRIER; }
57  bool is_atomic_begin() const { return type==typet::ATOMIC_BEGIN; }
58  bool is_atomic_end() const { return type==typet::ATOMIC_END; }
59 
60  enum class typet
61  {
62  NONE,
63  ASSIGNMENT,
64  ASSUME,
65  ASSERT,
66  GOTO,
67  LOCATION,
68  INPUT,
69  OUTPUT,
70  DECL,
71  DEAD,
74  CONSTRAINT,
77  SPAWN,
81  };
82 
84 
85  // we may choose to hide a step
86  bool hidden;
87 
88  // this is related to an internal expression
89  bool internal;
90 
91  // we categorize
94 
96 
97  // this transition done by given thread number
98  unsigned thread_nr;
99 
100  // for assume, assert, goto
103 
104  // for assert
105  std::string comment;
106 
107  // the object being assigned
109 
110  // the full, original lhs expression
112 
113  // A constant with the new value
115 
116  // for INPUT/OUTPUT
118  typedef std::list<exprt> io_argst;
120  bool formatted;
121 
122  // for function call/return
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  {
143  full_lhs.make_nil();
146  }
147 };
148 
153 {
154 public:
155  typedef std::list<goto_trace_stept> stepst;
157 
159 
160  void clear()
161  {
162  mode.clear();
163  steps.clear();
164  }
165 
168  void output(
169  const class namespacet &ns,
170  std::ostream &out) const;
171 
172  void swap(goto_tracet &other)
173  {
174  other.steps.swap(steps);
175  other.mode.swap(mode);
176  }
177 
178  void add_step(const goto_trace_stept &step)
179  {
180  steps.push_back(step);
181  }
182 
183  // retrieves the final step in the trace for manipulation
184  // (used to fill a trace from code, hence non-const)
186  {
187  return steps.back();
188  }
189 
190  // delete all steps after (not including) s
191  void trim_after(stepst::iterator s)
192  {
193  assert(s!=steps.end());
194  steps.erase(++s, steps.end());
195  }
196 };
197 
198 void show_goto_trace(
199  std::ostream &out,
200  const namespacet &,
201  const goto_tracet &);
202 
203 void trace_value(
204  std::ostream &out,
205  const namespacet &,
206  const ssa_exprt &lhs_object,
207  const exprt &full_lhs,
208  const exprt &value);
209 
210 
212 {
214 
216 
217  explicit trace_optionst(const optionst &options)
218  {
219  json_full_lhs = options.get_bool_option("trace-json-extended");
220  };
221 
222 private:
224  {
225  json_full_lhs = false;
226  };
227 };
228 
229 #define OPT_GOTO_TRACE "(trace-json-extended)"
230 
231 #define HELP_GOTO_TRACE \
232  " --trace-json-extended add rawLhs property to trace\n"
233 
234 #define PARSE_OPTIONS_GOTO_TRACE(cmdline, options) \
235  if(cmdline.isset("trace-json-extended")) \
236  options.set_option("trace-json-extended", true);
237 
238 
239 #endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H
The type of an expression.
Definition: type.h:22
bool is_shared_write() const
Definition: goto_trace.h:54
bool is_location() const
Definition: goto_trace.h:48
bool json_full_lhs
Definition: goto_trace.h:213
bool is_goto() const
Definition: goto_trace.h:44
void trim_after(stepst::iterator s)
Definition: goto_trace.h:191
bool is_input() const
Definition: goto_trace.h:50
exprt lhs_object_value
Definition: goto_trace.h:114
io_argst io_args
Definition: goto_trace.h:119
void clear()
Definition: goto_trace.h:160
std::list< exprt > io_argst
Definition: goto_trace.h:118
std::list< goto_trace_stept > stepst
Definition: goto_trace.h:155
goto_trace_stept & get_last_step()
Definition: goto_trace.h:185
void swap(goto_tracet &other)
Definition: goto_trace.h:172
std::size_t step_nr
Definition: goto_trace.h:39
bool is_shared_read() const
Definition: goto_trace.h:53
TO_BE_DOCUMENTED.
Definition: goto_trace.h:36
stepst steps
Definition: goto_trace.h:156
goto_programt::const_targett pc
Definition: goto_trace.h:95
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace in ASCII to a given stream
Definition: goto_trace.cpp:27
void add_step(const goto_trace_stept &step)
Definition: goto_trace.h:178
irep_idt io_id
Definition: goto_trace.h:117
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace step in ASCII to a given stream
Definition: goto_trace.cpp:35
bool is_function_call() const
Definition: goto_trace.h:46
bool is_output() const
Definition: goto_trace.h:49
bool is_assume() const
Definition: goto_trace.h:42
void show_goto_trace(std::ostream &out, const namespacet &, const goto_tracet &)
Definition: goto_trace.cpp:247
void trace_value(std::ostream &out, const namespacet &, const ssa_exprt &lhs_object, const exprt &full_lhs, const exprt &value)
Definition: goto_trace.cpp:187
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
unsigned thread_nr
Definition: goto_trace.h:98
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
bool is_atomic_end() const
Definition: goto_trace.h:58
irep_idt identifier
Definition: goto_trace.h:123
bool is_function_return() const
Definition: goto_trace.h:47
bool is_atomic_begin() const
Definition: goto_trace.h:57
void swap(dstringt &b)
Definition: dstring.h:118
void clear()
Definition: dstring.h:115
Base class for all expressions.
Definition: expr.h:42
trace_optionst(const optionst &options)
Definition: goto_trace.h:217
ssa_exprt lhs_object
Definition: goto_trace.h:108
exprt full_lhs_value
Definition: goto_trace.h:114
bool is_constraint() const
Definition: goto_trace.h:45
bool is_memory_barrier() const
Definition: goto_trace.h:56
std::string comment
Definition: goto_trace.h:105
void make_nil()
Definition: irep.h:243
bool is_assert() const
Definition: goto_trace.h:43
bool is_decl() const
Definition: goto_trace.h:51
bool is_assignment() const
Definition: goto_trace.h:41
bool is_dead() const
Definition: goto_trace.h:52
Options.
TO_BE_DOCUMENTED.
Definition: goto_trace.h:152
static const trace_optionst default_options
Definition: goto_trace.h:215
irep_idt mode
Definition: goto_trace.h:158
irep_idt format_string
Definition: goto_trace.h:117
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
Concrete Goto Program.
bool is_spawn() const
Definition: goto_trace.h:55
assignment_typet assignment_type
Definition: goto_trace.h:93