cprover
symex_target.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Generate Equation using Symbolic Execution
4 
5 Author: 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 "renaming_level.h"
18 
19 class ssa_exprt;
20 class symbol_exprt;
21 
26 {
27 public:
29  {
30  }
31 
32  virtual ~symex_targett() { }
33 
37  struct sourcet
38  {
39  unsigned thread_nr;
41  // The program counter is an iterator which indicates where the execution
42  // is in its program sequence
44 
45  sourcet(const irep_idt &_function_id, goto_programt::const_targett _pc)
46  : thread_nr(0), function_id(_function_id), pc(_pc)
47  {
48  }
49 
50  explicit sourcet(
51  const irep_idt &_function_id,
52  const goto_programt &_goto_program)
53  : thread_nr(0),
54  function_id(_function_id),
55  pc(_goto_program.instructions.begin())
56  {
57  }
58 
59  sourcet(sourcet &&other) noexcept
60  : thread_nr(other.thread_nr), function_id(other.function_id), pc(other.pc)
61  {
62  }
63 
64  sourcet(const sourcet &other) = default;
65  sourcet &operator=(const sourcet &other) = default;
66  sourcet &operator=(sourcet &&other) = default;
67  };
68 
69  enum class assignment_typet
70  {
71  STATE,
72  HIDDEN,
75  PHI,
76  GUARD,
77  };
78 
88  virtual void shared_read(
89  const exprt &guard,
90  const ssa_exprt &ssa_object,
91  unsigned atomic_section_id,
92  const sourcet &source) = 0;
93 
101  virtual void shared_write(
102  const exprt &guard,
103  const ssa_exprt &ssa_object,
104  unsigned atomic_section_id,
105  const sourcet &source) = 0;
106 
118  virtual void assignment(
119  const exprt &guard,
120  const ssa_exprt &ssa_lhs,
121  const exprt &ssa_full_lhs,
122  const exprt &original_full_lhs,
123  const exprt &ssa_rhs,
124  const sourcet &source,
125  assignment_typet assignment_type)=0;
126 
135  virtual void decl(
136  const exprt &guard,
137  const ssa_exprt &ssa_lhs,
138  const exprt &initializer,
139  const sourcet &source,
140  assignment_typet assignment_type) = 0;
141 
147  virtual void dead(
148  const exprt &guard,
149  const ssa_exprt &ssa_lhs,
150  const sourcet &source)=0;
151 
159  virtual void function_call(
160  const exprt &guard,
161  const irep_idt &function_id,
162  const std::vector<renamedt<exprt, L2>> &ssa_function_arguments,
163  const sourcet &source,
164  bool hidden) = 0;
165 
172  virtual void function_return(
173  const exprt &guard,
174  const irep_idt &function_id,
175  const sourcet &source,
176  bool hidden) = 0;
177 
182  virtual void location(
183  const exprt &guard,
184  const sourcet &source)=0;
185 
192  virtual void output(
193  const exprt &guard,
194  const sourcet &source,
195  const irep_idt &output_id,
196  const std::list<renamedt<exprt, L2>> &args) = 0;
197 
205  virtual void output_fmt(
206  const exprt &guard,
207  const sourcet &source,
208  const irep_idt &output_id,
209  const irep_idt &fmt,
210  const std::list<exprt> &args)=0;
211 
218  virtual void input(
219  const exprt &guard,
220  const sourcet &source,
221  const irep_idt &input_id,
222  const std::list<exprt> &args)=0;
223 
229  virtual void assumption(
230  const exprt &guard,
231  const exprt &cond,
232  const sourcet &source)=0;
233 
240  virtual void assertion(
241  const exprt &guard,
242  const exprt &cond,
243  const std::string &msg,
244  const sourcet &source)=0;
245 
251  virtual void goto_instruction(
252  const exprt &guard,
253  const renamedt<exprt, L2> &cond,
254  const sourcet &source) = 0;
255 
261  virtual void constraint(
262  const exprt &cond,
263  const std::string &msg,
264  const sourcet &source)=0;
265 
270  virtual void spawn(
271  const exprt &guard,
272  const sourcet &source)=0;
273 
278  virtual void memory_barrier(
279  const exprt &guard,
280  const sourcet &source)=0;
281 
287  virtual void atomic_begin(
288  const exprt &guard,
289  unsigned atomic_section_id,
290  const sourcet &source)=0;
291 
297  virtual void atomic_end(
298  const exprt &guard,
299  unsigned atomic_section_id,
300  const sourcet &source)=0;
301 };
302 
308 bool operator < (
309  const symex_targett::sourcet &a,
310  const symex_targett::sourcet &b);
311 
312 #endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_H
symex_targett::atomic_end
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0
Record ending an atomic section.
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
symex_targett::assignment_typet
assignment_typet
Definition: symex_target.h:69
symex_targett::constraint
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.
symex_targett::sourcet::sourcet
sourcet(const irep_idt &_function_id, const goto_programt &_goto_program)
Definition: symex_target.h:50
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:43
symex_targett::assertion
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)=0
Record an assertion.
symex_targett::dead
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)=0
Remove a variable from the scope.
symex_targett::sourcet::thread_nr
unsigned thread_nr
Definition: symex_target.h:39
symex_targett::function_return
virtual void function_return(const exprt &guard, const irep_idt &function_id, const sourcet &source, bool hidden)=0
Record return from a function.
exprt
Base class for all expressions.
Definition: expr.h:52
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
symex_targett::shared_write
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...
symex_targett::assignment_typet::STATE
symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER
symex_targett::decl
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.
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:16
symex_targett::assignment
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.
symex_targett::assignment_typet::HIDDEN_ACTUAL_PARAMETER
operator<
bool operator<(const symex_targett::sourcet &a, const symex_targett::sourcet &b)
Base class comparison operator for symbolic execution targets.
Definition: symex_target.cpp:14
renaming_level.h
symex_targett::sourcet::operator=
sourcet & operator=(const sourcet &other)=default
symex_targett::function_call
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.
symex_targett::shared_read
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...
symex_targett::assumption
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)=0
Record an assumption.
goto_program.h
symex_targett::assignment_typet::PHI
symex_targett::input
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)=0
Record an input.
symex_targett::output_fmt
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.
symex_targett::goto_instruction
virtual void goto_instruction(const exprt &guard, const renamedt< exprt, L2 > &cond, const sourcet &source)=0
Record a goto instruction.
symex_targett::output
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.
symex_targett::spawn
virtual void spawn(const exprt &guard, const sourcet &source)=0
Record spawning a new thread.
symex_targett::sourcet::sourcet
sourcet(const irep_idt &_function_id, goto_programt::const_targett _pc)
Definition: symex_target.h:45
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
symex_targett::assignment_typet::GUARD
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
symex_targett::assignment_typet::HIDDEN
symex_targett::atomic_begin
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0
Record a beginning of an atomic section.
symex_targett::~symex_targett
virtual ~symex_targett()
Definition: symex_target.h:32
symex_targett::sourcet::function_id
irep_idt function_id
Definition: symex_target.h:40
symex_targett::sourcet::sourcet
sourcet(sourcet &&other) noexcept
Definition: symex_target.h:59
symex_targett::location
virtual void location(const exprt &guard, const sourcet &source)=0
Record a location.
symex_targett::symex_targett
symex_targett()
Definition: symex_target.h:28
symex_targett
The interface of the target container for symbolic execution to record its symbolic steps into.
Definition: symex_target.h:25
renamedt
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:26
symex_targett::memory_barrier
virtual void memory_barrier(const exprt &guard, const sourcet &source)=0
Record creating a memory barrier.