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/ssa_expr.h>
28 
30 
35 {
36 public:
37  unsigned step_nr;
38 
39  bool is_assignment() const { return type==typet::ASSIGNMENT; }
40  bool is_assume() const { return type==typet::ASSUME; }
41  bool is_assert() const { return type==typet::ASSERT; }
42  bool is_goto() const { return type==typet::GOTO; }
43  bool is_constraint() const { return type==typet::CONSTRAINT; }
44  bool is_function_call() const { return type==typet::FUNCTION_CALL; }
46  bool is_location() const { return type==typet::LOCATION; }
47  bool is_output() const { return type==typet::OUTPUT; }
48  bool is_input() const { return type==typet::INPUT; }
49  bool is_decl() const { return type==typet::DECL; }
50  bool is_dead() const { return type==typet::DEAD; }
51  bool is_shared_read() const { return type==typet::SHARED_READ; }
52  bool is_shared_write() const { return type==typet::SHARED_WRITE; }
53  bool is_spawn() const { return type==typet::SPAWN; }
54  bool is_memory_barrier() const { return type==typet::MEMORY_BARRIER; }
55  bool is_atomic_begin() const { return type==typet::ATOMIC_BEGIN; }
56  bool is_atomic_end() const { return type==typet::ATOMIC_END; }
57 
58  enum class typet
59  {
60  NONE,
61  ASSIGNMENT,
62  ASSUME,
63  ASSERT,
64  GOTO,
65  LOCATION,
66  INPUT,
67  OUTPUT,
68  DECL,
69  DEAD,
72  CONSTRAINT,
75  SPAWN,
79  };
80 
82 
83  // we may choose to hide a step
84  bool hidden;
85 
86  // we categorize
87  enum class assignment_typet { STATE, ACTUAL_PARAMETER };
89 
91 
92  // this transition done by given thread number
93  unsigned thread_nr;
94 
95  // for assume, assert, goto
96  bool cond_value;
98 
99  // for assert
100  std::string comment;
101 
102  // the object being assigned
104 
105  // the full, original lhs expression
107 
108  // A constant with the new value
110 
111  // for INPUT/OUTPUT
113  typedef std::list<exprt> io_argst;
114  io_argst io_args;
115  bool formatted;
116 
117  // for function call/return
119 
122  void output(
123  const class namespacet &ns,
124  std::ostream &out) const;
125 
127  step_nr(0),
128  type(typet::NONE),
129  hidden(false),
130  assignment_type(assignment_typet::STATE),
131  thread_nr(0),
132  cond_value(false),
133  formatted(false)
134  {
135  lhs_object.make_nil();
136  lhs_object_value.make_nil();
137  full_lhs.make_nil();
138  full_lhs_value.make_nil();
139  cond_expr.make_nil();
140  }
141 };
142 
147 {
148 public:
149  typedef std::list<goto_trace_stept> stepst;
150  stepst steps;
151 
153 
154  void clear()
155  {
156  mode.clear();
157  steps.clear();
158  }
159 
162  void output(
163  const class namespacet &ns,
164  std::ostream &out) const;
165 
166  void swap(goto_tracet &other)
167  {
168  other.steps.swap(steps);
169  other.mode.swap(mode);
170  }
171 
172  void add_step(const goto_trace_stept &step)
173  {
174  steps.push_back(step);
175  }
176 
177  // delete all steps after (not including) s
178  void trim_after(stepst::iterator s)
179  {
180  assert(s!=steps.end());
181  steps.erase(++s, steps.end());
182  }
183 };
184 
185 void show_goto_trace(
186  std::ostream &out,
187  const namespacet &ns,
188  const goto_tracet &goto_trace);
189 
190 void trace_value(
191  std::ostream &out,
192  const namespacet &ns,
193  const ssa_exprt &lhs_object,
194  const exprt &full_lhs,
195  const exprt &value);
196 
197 #endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H
The type of an expression.
Definition: type.h:20
bool is_shared_write() const
Definition: goto_trace.h:52
bool is_location() const
Definition: goto_trace.h:46
bool is_goto() const
Definition: goto_trace.h:42
void trim_after(stepst::iterator s)
Definition: goto_trace.h:178
bool is_input() const
Definition: goto_trace.h:48
exprt lhs_object_value
Definition: goto_trace.h:109
io_argst io_args
Definition: goto_trace.h:114
unsigned step_nr
Definition: goto_trace.h:37
void clear()
Definition: goto_trace.h:154
std::list< exprt > io_argst
Definition: goto_trace.h:113
std::list< goto_trace_stept > stepst
Definition: goto_trace.h:149
void trace_value(std::ostream &out, const namespacet &ns, const ssa_exprt &lhs_object, const exprt &full_lhs, const exprt &value)
Definition: goto_trace.cpp:179
void swap(goto_tracet &other)
Definition: goto_trace.h:166
bool is_shared_read() const
Definition: goto_trace.h:51
TO_BE_DOCUMENTED.
Definition: goto_trace.h:34
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
Definition: goto_trace.cpp:239
stepst steps
Definition: goto_trace.h:150
goto_programt::const_targett pc
Definition: goto_trace.h:90
void add_step(const goto_trace_stept &step)
Definition: goto_trace.h:172
irep_idt io_id
Definition: goto_trace.h:112
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace step in ASCII to a given stream
Definition: goto_trace.cpp:33
bool is_function_call() const
Definition: goto_trace.h:44
bool is_output() const
Definition: goto_trace.h:47
instructionst::const_iterator const_targett
bool is_assume() const
Definition: goto_trace.h:40
unsigned thread_nr
Definition: goto_trace.h:93
TO_BE_DOCUMENTED.
Definition: namespace.h:62
bool is_atomic_end() const
Definition: goto_trace.h:56
irep_idt identifier
Definition: goto_trace.h:118
bool is_function_return() const
Definition: goto_trace.h:45
bool is_atomic_begin() const
Definition: goto_trace.h:55
void swap(dstringt &b)
Definition: dstring.h:118
void clear()
Definition: dstring.h:115
Base class for all expressions.
Definition: expr.h:46
ssa_exprt lhs_object
Definition: goto_trace.h:103
exprt full_lhs_value
Definition: goto_trace.h:109
bool is_constraint() const
Definition: goto_trace.h:43
bool is_memory_barrier() const
Definition: goto_trace.h:54
std::string comment
Definition: goto_trace.h:100
void make_nil()
Definition: irep.h:243
bool is_assert() const
Definition: goto_trace.h:41
bool is_decl() const
Definition: goto_trace.h:49
bool is_assignment() const
Definition: goto_trace.h:39
bool is_dead() const
Definition: goto_trace.h:50
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146
irep_idt mode
Definition: goto_trace.h:152
irep_idt format_string
Definition: goto_trace.h:112
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
Concrete Goto Program.
bool is_spawn() const
Definition: goto_trace.h:53
assignment_typet assignment_type
Definition: goto_trace.h:88