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 
21 {
22 public:
24  {
25  }
26 
27  virtual ~symex_targett() { }
28 
29  struct sourcet
30  {
31  unsigned thread_nr;
33  bool is_set;
34 
36  thread_nr(0),
37  is_set(false)
38  {
39  }
40 
41  explicit sourcet(
43  thread_nr(0),
44  pc(_pc),
45  is_set(true)
46  {
47  }
48 
49  explicit sourcet(const goto_programt &_goto_program):
50  thread_nr(0),
51  pc(_goto_program.instructions.begin()),
52  is_set(true)
53  {
54  }
55  };
56 
57  enum class assignment_typet
58  {
59  STATE,
60  HIDDEN,
63  PHI,
64  GUARD,
65  };
66 
67  // read event
68  virtual void shared_read(
69  const exprt &guard,
70  const ssa_exprt &ssa_rhs,
71  unsigned atomic_section_id,
72  const sourcet &source)=0;
73 
74  // write event
75  virtual void shared_write(
76  const exprt &guard,
77  const ssa_exprt &ssa_rhs,
78  unsigned atomic_section_id,
79  const sourcet &source)=0;
80 
81  // write event - lhs must be symbol
82  virtual void assignment(
83  const exprt &guard,
84  const ssa_exprt &ssa_lhs,
85  const exprt &ssa_full_lhs,
86  const exprt &original_full_lhs,
87  const exprt &ssa_rhs,
88  const sourcet &source,
89  assignment_typet assignment_type)=0;
90 
91  // declare fresh variable - lhs must be symbol
92  virtual void decl(
93  const exprt &guard,
94  const ssa_exprt &ssa_lhs,
95  const sourcet &source,
96  assignment_typet assignment_type)=0;
97 
98  // note the death of a variable - lhs must be symbol
99  virtual void dead(
100  const exprt &guard,
101  const ssa_exprt &ssa_lhs,
102  const sourcet &source)=0;
103 
104  // record a function call
105  virtual void function_call(
106  const exprt &guard,
107  const irep_idt &identifier,
108  const sourcet &source)=0;
109 
110  // record return from a function
111  virtual void function_return(
112  const exprt &guard,
113  const irep_idt &identifier,
114  const sourcet &source)=0;
115 
116  // just record a location
117  virtual void location(
118  const exprt &guard,
119  const sourcet &source)=0;
120 
121  // record output
122  virtual void output(
123  const exprt &guard,
124  const sourcet &source,
125  const irep_idt &output_id,
126  const std::list<exprt> &args)=0;
127 
128  // record formatted output
129  virtual void output_fmt(
130  const exprt &guard,
131  const sourcet &source,
132  const irep_idt &output_id,
133  const irep_idt &fmt,
134  const std::list<exprt> &args)=0;
135 
136  // record input
137  virtual void input(
138  const exprt &guard,
139  const sourcet &source,
140  const irep_idt &input_id,
141  const std::list<exprt> &args)=0;
142 
143  // record an assumption
144  virtual void assumption(
145  const exprt &guard,
146  const exprt &cond,
147  const sourcet &source)=0;
148 
149  // record an assertion
150  virtual void assertion(
151  const exprt &guard,
152  const exprt &cond,
153  const std::string &msg,
154  const sourcet &source)=0;
155 
156  // record a goto
157  virtual void goto_instruction(
158  const exprt &guard,
159  const exprt &cond,
160  const sourcet &source)=0;
161 
162  // record a constraint
163  virtual void constraint(
164  const exprt &cond,
165  const std::string &msg,
166  const sourcet &source)=0;
167 
168  // record thread spawn
169  virtual void spawn(
170  const exprt &guard,
171  const sourcet &source)=0;
172 
173  // record memory barrier
174  virtual void memory_barrier(
175  const exprt &guard,
176  const sourcet &source)=0;
177 
178  // record atomic section
179  virtual void atomic_begin(
180  const exprt &guard,
181  unsigned atomic_section_id,
182  const sourcet &source)=0;
183  virtual void atomic_end(
184  const exprt &guard,
185  unsigned atomic_section_id,
186  const sourcet &source)=0;
187 };
188 
189 bool operator < (
190  const symex_targett::sourcet &a,
191  const symex_targett::sourcet &b);
192 
193 #endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_H
sourcet(goto_programt::const_targett _pc)
Definition: symex_target.h:41
virtual void location(const exprt &guard, const sourcet &source)=0
goto_programt::const_targett pc
Definition: symex_target.h:32
virtual ~symex_targett()
Definition: symex_target.h:27
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)=0
sourcet(const goto_programt &_goto_program)
Definition: symex_target.h:49
virtual void function_call(const exprt &guard, const irep_idt &identifier, const sourcet &source)=0
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0
instructionst::const_iterator const_targett
virtual void spawn(const exprt &guard, const sourcet &source)=0
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)=0
bool operator<(const symex_targett::sourcet &a, const symex_targett::sourcet &b)
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_rhs, unsigned atomic_section_id, const sourcet &source)=0
virtual void goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)=0
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)=0
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
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
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0
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
Base class for all expressions.
Definition: expr.h:46
virtual void function_return(const exprt &guard, const irep_idt &identifier, const sourcet &source)=0
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< exprt > &args)=0
Expression to hold a symbol (variable)
Definition: std_expr.h:82
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_rhs, unsigned atomic_section_id, const sourcet &source)=0
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
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)=0
virtual void memory_barrier(const exprt &guard, const sourcet &source)=0
Concrete Goto Program.
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)=0