cprover
symex_target.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Generate Equation using Symbolic Execution
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_SYMEX_SYMEX_TARGET_H
13#define CPROVER_GOTO_SYMEX_SYMEX_TARGET_H
14
16
17#include "renamed.h"
18
19class ssa_exprt;
20
25{
26public:
28 {
29 }
30
31 virtual ~symex_targett() { }
32
36 struct sourcet
37 {
38 unsigned thread_nr;
40 // The program counter is an iterator which indicates where the execution
41 // is in its program sequence
43
45 : thread_nr(0), function_id(_function_id), pc(_pc)
46 {
47 }
48
49 explicit sourcet(
50 const irep_idt &_function_id,
51 const goto_programt &_goto_program)
52 : thread_nr(0),
53 function_id(_function_id),
54 pc(_goto_program.instructions.begin())
55 {
56 }
57
58 sourcet(sourcet &&other) noexcept
59 : thread_nr(other.thread_nr), function_id(other.function_id), pc(other.pc)
60 {
61 }
62
63 sourcet(const sourcet &other) = default;
64 sourcet &operator=(const sourcet &other) = default;
65 sourcet &operator=(sourcet &&other) = default;
66 };
67
69 {
70 STATE,
71 HIDDEN,
72 VISIBLE_ACTUAL_PARAMETER,
73 HIDDEN_ACTUAL_PARAMETER,
74 PHI,
75 GUARD,
76 };
77
87 virtual void shared_read(
88 const exprt &guard,
89 const ssa_exprt &ssa_object,
90 unsigned atomic_section_id,
91 const sourcet &source) = 0;
92
100 virtual void shared_write(
101 const exprt &guard,
102 const ssa_exprt &ssa_object,
103 unsigned atomic_section_id,
104 const sourcet &source) = 0;
105
117 virtual void assignment(
118 const exprt &guard,
119 const ssa_exprt &ssa_lhs,
120 const exprt &ssa_full_lhs,
121 const exprt &original_full_lhs,
122 const exprt &ssa_rhs,
123 const sourcet &source,
124 assignment_typet assignment_type)=0;
125
134 virtual void decl(
135 const exprt &guard,
136 const ssa_exprt &ssa_lhs,
137 const exprt &initializer,
138 const sourcet &source,
139 assignment_typet assignment_type) = 0;
140
146 virtual void dead(
147 const exprt &guard,
148 const ssa_exprt &ssa_lhs,
149 const sourcet &source)=0;
150
158 virtual void function_call(
159 const exprt &guard,
160 const irep_idt &function_id,
161 const std::vector<renamedt<exprt, L2>> &ssa_function_arguments,
162 const sourcet &source,
163 bool hidden) = 0;
164
171 virtual void function_return(
172 const exprt &guard,
173 const irep_idt &function_id,
174 const sourcet &source,
175 bool hidden) = 0;
176
181 virtual void location(
182 const exprt &guard,
183 const sourcet &source)=0;
184
191 virtual void output(
192 const exprt &guard,
193 const sourcet &source,
194 const irep_idt &output_id,
195 const std::list<renamedt<exprt, L2>> &args) = 0;
196
204 virtual void output_fmt(
205 const exprt &guard,
206 const sourcet &source,
207 const irep_idt &output_id,
208 const irep_idt &fmt,
209 const std::list<exprt> &args)=0;
210
217 virtual void input(
218 const exprt &guard,
219 const sourcet &source,
220 const irep_idt &input_id,
221 const std::list<exprt> &args)=0;
222
228 virtual void assumption(
229 const exprt &guard,
230 const exprt &cond,
231 const sourcet &source)=0;
232
239 virtual void assertion(
240 const exprt &guard,
241 const exprt &cond,
242 const std::string &msg,
243 const sourcet &source)=0;
244
250 virtual void goto_instruction(
251 const exprt &guard,
252 const renamedt<exprt, L2> &cond,
253 const sourcet &source) = 0;
254
260 virtual void constraint(
261 const exprt &cond,
262 const std::string &msg,
263 const sourcet &source)=0;
264
269 virtual void spawn(
270 const exprt &guard,
271 const sourcet &source)=0;
272
277 virtual void memory_barrier(
278 const exprt &guard,
279 const sourcet &source)=0;
280
286 virtual void atomic_begin(
287 const exprt &guard,
288 unsigned atomic_section_id,
289 const sourcet &source)=0;
290
296 virtual void atomic_end(
297 const exprt &guard,
298 unsigned atomic_section_id,
299 const sourcet &source)=0;
300};
301
307bool operator < (
308 const symex_targett::sourcet &a,
309 const symex_targett::sourcet &b);
310
311#endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_H
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
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::const_iterator const_targett
Definition: goto_program.h:593
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:33
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
The interface of the target container for symbolic execution to record its symbolic steps into.
Definition: symex_target.h:25
virtual void spawn(const exprt &guard, const sourcet &source)=0
Record spawning a new thread.
virtual void memory_barrier(const exprt &guard, const sourcet &source)=0
Record creating a memory barrier.
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)=0
Record an assertion.
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)=0
Read from a shared variable ssa_object (which is both the left- and the right–hand side of assignment...
virtual void function_call(const exprt &guard, const irep_idt &function_id, const std::vector< renamedt< exprt, L2 > > &ssa_function_arguments, const sourcet &source, bool hidden)=0
Record a function call.
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)=0
Record formatted output.
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &initializer, const sourcet &source, assignment_typet assignment_type)=0
Declare a fresh variable.
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)=0
Write to a shared variable ssa_object: we effectively assign a value from this thread to be visible b...
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)=0
Record a global constraint: there is no guard limiting its scope.
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< renamedt< exprt, L2 > > &args)=0
Record an output.
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0
Record a beginning of an atomic section.
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)=0
Write to a local variable.
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)=0
Record an input.
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)=0
Remove a variable from the scope.
virtual ~symex_targett()
Definition: symex_target.h:31
virtual void function_return(const exprt &guard, const irep_idt &function_id, const sourcet &source, bool hidden)=0
Record return from a function.
virtual void goto_instruction(const exprt &guard, const renamedt< exprt, L2 > &cond, const sourcet &source)=0
Record a goto instruction.
virtual void location(const exprt &guard, const sourcet &source)=0
Record a location.
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)=0
Record an assumption.
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0
Record ending an atomic section.
Concrete Goto Program.
Class for expressions or types renamed up to a given level.
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
sourcet & operator=(sourcet &&other)=default
sourcet(const sourcet &other)=default
sourcet(const irep_idt &_function_id, goto_programt::const_targett _pc)
Definition: symex_target.h:44
sourcet(sourcet &&other) noexcept
Definition: symex_target.h:58
goto_programt::const_targett pc
Definition: symex_target.h:42
sourcet & operator=(const sourcet &other)=default
sourcet(const irep_idt &_function_id, const goto_programt &_goto_program)
Definition: symex_target.h:49
bool operator<(const symex_targett::sourcet &a, const symex_targett::sourcet &b)
Base class comparison operator for symbolic execution targets.