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 class ssa_exprt;
18 class symbol_exprt;
19 
24 {
25 public:
27  {
28  }
29 
30  virtual ~symex_targett() { }
31 
35  struct sourcet
36  {
37  unsigned thread_nr;
38  irep_idt function;
39  // The program counter is an iterator which indicates where the execution
40  // is in its program sequence
42  bool is_set;
43 
45  {
46  }
47 
49  : thread_nr(0), function(_function), pc(_pc), is_set(true)
50  {
51  }
52 
53  explicit sourcet(
54  const irep_idt &_function,
55  const goto_programt &_goto_program)
56  : thread_nr(0),
57  function(_function),
58  pc(_goto_program.instructions.begin()),
59  is_set(true)
60  {
61  }
62  };
63 
64  enum class assignment_typet
65  {
66  STATE,
67  HIDDEN,
70  PHI,
71  GUARD,
72  };
73 
83  virtual void shared_read(
84  const exprt &guard,
85  const ssa_exprt &ssa_object,
86  unsigned atomic_section_id,
87  const sourcet &source) = 0;
88 
96  virtual void shared_write(
97  const exprt &guard,
98  const ssa_exprt &ssa_object,
99  unsigned atomic_section_id,
100  const sourcet &source) = 0;
101 
113  virtual void assignment(
114  const exprt &guard,
115  const ssa_exprt &ssa_lhs,
116  const exprt &ssa_full_lhs,
117  const exprt &original_full_lhs,
118  const exprt &ssa_rhs,
119  const sourcet &source,
120  assignment_typet assignment_type)=0;
121 
129  virtual void decl(
130  const exprt &guard,
131  const ssa_exprt &ssa_lhs,
132  const sourcet &source,
133  assignment_typet assignment_type)=0;
134 
140  virtual void dead(
141  const exprt &guard,
142  const ssa_exprt &ssa_lhs,
143  const sourcet &source)=0;
144 
152  virtual void function_call(
153  const exprt &guard,
154  const irep_idt &function_identifier,
155  const std::vector<exprt> &ssa_function_arguments,
156  const sourcet &source,
157  bool hidden) = 0;
158 
164  virtual void
165  function_return(const exprt &guard, const sourcet &source, bool hidden) = 0;
166 
171  virtual void location(
172  const exprt &guard,
173  const sourcet &source)=0;
174 
181  virtual void output(
182  const exprt &guard,
183  const sourcet &source,
184  const irep_idt &output_id,
185  const std::list<exprt> &args)=0;
186 
194  virtual void output_fmt(
195  const exprt &guard,
196  const sourcet &source,
197  const irep_idt &output_id,
198  const irep_idt &fmt,
199  const std::list<exprt> &args)=0;
200 
207  virtual void input(
208  const exprt &guard,
209  const sourcet &source,
210  const irep_idt &input_id,
211  const std::list<exprt> &args)=0;
212 
218  virtual void assumption(
219  const exprt &guard,
220  const exprt &cond,
221  const sourcet &source)=0;
222 
229  virtual void assertion(
230  const exprt &guard,
231  const exprt &cond,
232  const std::string &msg,
233  const sourcet &source)=0;
234 
240  virtual void goto_instruction(
241  const exprt &guard,
242  const exprt &cond,
243  const sourcet &source)=0;
244 
250  virtual void constraint(
251  const exprt &cond,
252  const std::string &msg,
253  const sourcet &source)=0;
254 
259  virtual void spawn(
260  const exprt &guard,
261  const sourcet &source)=0;
262 
267  virtual void memory_barrier(
268  const exprt &guard,
269  const sourcet &source)=0;
270 
276  virtual void atomic_begin(
277  const exprt &guard,
278  unsigned atomic_section_id,
279  const sourcet &source)=0;
280 
286  virtual void atomic_end(
287  const exprt &guard,
288  unsigned atomic_section_id,
289  const sourcet &source)=0;
290 };
291 
297 bool operator < (
298  const symex_targett::sourcet &a,
299  const symex_targett::sourcet &b);
300 
301 #endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_H
virtual void location(const exprt &guard, const sourcet &source)=0
Record a location.
goto_programt::const_targett pc
Definition: symex_target.h:41
virtual void function_call(const exprt &guard, const irep_idt &function_identifier, const std::vector< exprt > &ssa_function_arguments, const sourcet &source, bool hidden)=0
Record a function call.
virtual ~symex_targett()
Definition: symex_target.h:30
sourcet(const irep_idt &_function, goto_programt::const_targett _pc)
Definition: symex_target.h:48
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)=0
Remove a variable from the scope.
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 assignme...
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0
Record ending an atomic section.
sourcet(const irep_idt &_function, const goto_programt &_goto_program)
Definition: symex_target.h:53
Identifies source in the context of symbolic execution.
Definition: symex_target.h:35
virtual void spawn(const exprt &guard, const sourcet &source)=0
Record spawning a new thread.
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...
The interface of the target container for symbolic execution to record its symbolic steps into...
Definition: symex_target.h:23
instructionst::const_iterator const_targett
Definition: goto_program.h:415
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)=0
Record an assertion.
bool operator<(const symex_targett::sourcet &a, const symex_targett::sourcet &b)
Base class comparison operator for symbolic execution targets.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
virtual void goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)=0
Record a goto instruction.
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)=0
Record an assumption.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
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 atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0
Record a beginning of an atomic section.
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.
Base class for all expressions.
Definition: expr.h:54
virtual void function_return(const exprt &guard, const sourcet &source, bool hidden)=0
Record return from a function.
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< exprt > &args)=0
Record an output.
Expression to hold a symbol (variable)
Definition: std_expr.h:143
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
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 decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)=0
Declare a fresh variable.
virtual void memory_barrier(const exprt &guard, const sourcet &source)=0
Record creating a memory barrier.
Concrete Goto Program.
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)=0
Record an input.