cprover
symex_target_equation.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_EQUATION_H
13 #define CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
14 
15 #include <list>
16 #include <iosfwd>
17 
18 #include <util/merge_irep.h>
19 
22 
23 #include <solvers/prop/literal.h>
24 
25 #include "symex_target.h"
26 
28 class namespacet;
29 class prop_convt;
30 
32 {
33 public:
34  explicit symex_target_equationt(const namespacet &_ns);
35  virtual ~symex_target_equationt();
36 
37  // read event
38  virtual void shared_read(
39  const exprt &guard,
40  const ssa_exprt &ssa_object,
41  unsigned atomic_section_id,
42  const sourcet &source);
43 
44  // write event
45  virtual void shared_write(
46  const exprt &guard,
47  const ssa_exprt &ssa_object,
48  unsigned atomic_section_id,
49  const sourcet &source);
50 
51  // assignment to a variable - lhs must be symbol
52  virtual void assignment(
53  const exprt &guard,
54  const ssa_exprt &ssa_lhs,
55  const exprt &ssa_full_lhs,
56  const exprt &original_full_lhs,
57  const exprt &ssa_rhs,
58  const sourcet &source,
59  assignment_typet assignment_type);
60 
61  // declare fresh variable - lhs must be symbol
62  virtual void decl(
63  const exprt &guard,
64  const ssa_exprt &ssa_lhs,
65  const sourcet &source,
66  assignment_typet assignment_type);
67 
68  // note the death of a variable - lhs must be symbol
69  virtual void dead(
70  const exprt &guard,
71  const ssa_exprt &ssa_lhs,
72  const sourcet &source);
73 
74  // record a function call
75  virtual void function_call(
76  const exprt &guard,
77  const irep_idt &identifier,
78  const sourcet &source);
79 
80  // record return from a function
81  virtual void function_return(
82  const exprt &guard,
83  const irep_idt &identifier,
84  const sourcet &source);
85 
86  // just record a location
87  virtual void location(
88  const exprt &guard,
89  const sourcet &source);
90 
91  // output
92  virtual void output(
93  const exprt &guard,
94  const sourcet &source,
95  const irep_idt &fmt,
96  const std::list<exprt> &args);
97 
98  // output, formatted
99  virtual void output_fmt(
100  const exprt &guard,
101  const sourcet &source,
102  const irep_idt &output_id,
103  const irep_idt &fmt,
104  const std::list<exprt> &args);
105 
106  // input
107  virtual void input(
108  const exprt &guard,
109  const sourcet &source,
110  const irep_idt &input_id,
111  const std::list<exprt> &args);
112 
113  // record an assumption
114  virtual void assumption(
115  const exprt &guard,
116  const exprt &cond,
117  const sourcet &source);
118 
119  // record an assertion
120  virtual void assertion(
121  const exprt &guard,
122  const exprt &cond,
123  const std::string &msg,
124  const sourcet &source);
125 
126  // record a goto
127  virtual void goto_instruction(
128  const exprt &guard,
129  const exprt &cond,
130  const sourcet &source);
131 
132  // record a (global) constraint
133  virtual void constraint(
134  const exprt &cond,
135  const std::string &msg,
136  const sourcet &source);
137 
138  // record thread spawn
139  virtual void spawn(
140  const exprt &guard,
141  const sourcet &source);
142 
143  // record memory barrier
144  virtual void memory_barrier(
145  const exprt &guard,
146  const sourcet &source);
147 
148  // record atomic section
149  virtual void atomic_begin(
150  const exprt &guard,
151  unsigned atomic_section_id,
152  const sourcet &source);
153  virtual void atomic_end(
154  const exprt &guard,
155  unsigned atomic_section_id,
156  const sourcet &source);
157 
158  void convert(prop_convt &prop_conv);
159  void convert_assignments(decision_proceduret &decision_procedure) const;
160  void convert_decls(prop_convt &prop_conv) const;
161  void convert_assumptions(prop_convt &prop_conv);
162  void convert_assertions(prop_convt &prop_conv);
163  void convert_constraints(decision_proceduret &decision_procedure) const;
164  void convert_goto_instructions(prop_convt &prop_conv);
165  void convert_guards(prop_convt &prop_conv);
166  void convert_io(decision_proceduret &decision_procedure);
167 
168  exprt make_expression() const;
169 
170  class SSA_stept
171  {
172  public:
173  sourcet source;
175 
176  // NOLINTNEXTLINE(whitespace/line_length)
177  bool is_assert() const { return type==goto_trace_stept::typet::ASSERT; }
178  // NOLINTNEXTLINE(whitespace/line_length)
179  bool is_assume() const { return type==goto_trace_stept::typet::ASSUME; }
180  // NOLINTNEXTLINE(whitespace/line_length)
181  bool is_assignment() const { return type==goto_trace_stept::typet::ASSIGNMENT; }
182  // NOLINTNEXTLINE(whitespace/line_length)
183  bool is_goto() const { return type==goto_trace_stept::typet::GOTO; }
184  // NOLINTNEXTLINE(whitespace/line_length)
185  bool is_constraint() const { return type==goto_trace_stept::typet::CONSTRAINT; }
186  // NOLINTNEXTLINE(whitespace/line_length)
187  bool is_location() const { return type==goto_trace_stept::typet::LOCATION; }
188  // NOLINTNEXTLINE(whitespace/line_length)
189  bool is_output() const { return type==goto_trace_stept::typet::OUTPUT; }
190  // NOLINTNEXTLINE(whitespace/line_length)
191  bool is_decl() const { return type==goto_trace_stept::typet::DECL; }
192  // NOLINTNEXTLINE(whitespace/line_length)
194  // NOLINTNEXTLINE(whitespace/line_length)
196  // NOLINTNEXTLINE(whitespace/line_length)
198  // NOLINTNEXTLINE(whitespace/line_length)
200  // NOLINTNEXTLINE(whitespace/line_length)
201  bool is_spawn() const { return type==goto_trace_stept::typet::SPAWN; }
202  // NOLINTNEXTLINE(whitespace/line_length)
204  // NOLINTNEXTLINE(whitespace/line_length)
206  // NOLINTNEXTLINE(whitespace/line_length)
207  bool is_atomic_end() const { return type==goto_trace_stept::typet::ATOMIC_END; }
208 
209  // we may choose to hide
210  bool hidden=false;
211 
214 
215  // for ASSIGNMENT and DECL
220 
221  // for ASSUME/ASSERT/GOTO/CONSTRAINT
224  std::string comment;
225 
226  // for INPUT/OUTPUT
228  bool formatted=false;
229  std::list<exprt> io_args;
230  std::list<exprt> converted_io_args;
231 
232  // for function call/return
234 
235  // for SHARED_READ/SHARED_WRITE and ATOMIC_BEGIN/ATOMIC_END
236  unsigned atomic_section_id=0;
237 
238  // for slicing
239  bool ignore=false;
240 
242  type(goto_trace_stept::typet::NONE),
243  hidden(false),
244  guard(static_cast<const exprt &>(get_nil_irep())),
245  guard_literal(const_literal(false)),
246  ssa_lhs(static_cast<const ssa_exprt &>(get_nil_irep())),
247  ssa_full_lhs(static_cast<const exprt &>(get_nil_irep())),
248  original_full_lhs(static_cast<const exprt &>(get_nil_irep())),
249  ssa_rhs(static_cast<const exprt &>(get_nil_irep())),
250  cond_expr(static_cast<const exprt &>(get_nil_irep())),
251  cond_literal(const_literal(false)),
252  formatted(false),
253  atomic_section_id(0),
254  ignore(false)
255  {
256  }
257 
258  void output(
259  const namespacet &ns,
260  std::ostream &out) const;
261  };
262 
263  unsigned count_assertions() const
264  {
265  unsigned i=0;
266  for(SSA_stepst::const_iterator
267  it=SSA_steps.begin();
268  it!=SSA_steps.end(); it++)
269  if(it->is_assert())
270  i++;
271  return i;
272  }
273 
274  unsigned count_ignored_SSA_steps() const
275  {
276  unsigned i=0;
277  for(SSA_stepst::const_iterator
278  it=SSA_steps.begin();
279  it!=SSA_steps.end(); it++)
280  if(it->ignore)
281  i++;
282  return i;
283  }
284 
285  typedef std::list<SSA_stept> SSA_stepst;
286  SSA_stepst SSA_steps;
287 
288  SSA_stepst::iterator get_SSA_step(unsigned s)
289  {
290  SSA_stepst::iterator it=SSA_steps.begin();
291  for(; s!=0; s--)
292  {
293  assert(it!=SSA_steps.end());
294  it++;
295  }
296  return it;
297  }
298 
299  void output(std::ostream &out) const;
300 
301  void clear()
302  {
303  SSA_steps.clear();
304  }
305 
306  bool has_threads() const
307  {
308  for(SSA_stepst::const_iterator it=SSA_steps.begin();
309  it!=SSA_steps.end();
310  it++)
311  if(it->source.thread_nr!=0)
312  return true;
313 
314  return false;
315  }
316 
317 protected:
318  const namespacet &ns;
319 
320  // for enforcing sharing in the expressions stored
322  void merge_ireps(SSA_stept &SSA_step);
323 };
324 
325 inline bool operator<(
326  const symex_target_equationt::SSA_stepst::const_iterator a,
327  const symex_target_equationt::SSA_stepst::const_iterator b)
328 {
329  return &(*a)<&(*b);
330 }
331 
332 std::ostream &operator<<(
333  std::ostream &out,
335 std::ostream &operator<<(
336  std::ostream &out,
337  const symex_target_equationt &equation);
338 
339 #endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
const irept & get_nil_irep()
Definition: irep.cpp:56
The type of an expression.
Definition: type.h:20
virtual void spawn(const exprt &guard, const sourcet &source)
spawn a new thread
virtual void function_call(const exprt &guard, const irep_idt &identifier, const sourcet &source)
just record a location
virtual void memory_barrier(const exprt &guard, const sourcet &source)
void convert(prop_convt &prop_conv)
exprt make_expression() const
void convert_assumptions(prop_convt &prop_conv)
converts assumptions
Generate Equation using Symbolic Execution.
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
record an assumption
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
just record input
virtual void goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)
record a goto instruction
Traces of GOTO Programs.
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
start an atomic section
TO_BE_DOCUMENTED.
Definition: goto_trace.h:34
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
end an atomic section
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
write to a sharedvariable
unsigned count_ignored_SSA_steps() const
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
record a constraint
symex_target_equationt(const namespacet &_ns)
void convert_constraints(decision_proceduret &decision_procedure) const
converts constraints
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)
declare a fresh variable
TO_BE_DOCUMENTED.
Definition: namespace.h:62
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)
write to a variable
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
just record formatted output
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &fmt, const std::list< exprt > &args)
just record output
SSA_stepst::iterator get_SSA_step(unsigned s)
void convert_goto_instructions(prop_convt &prop_conv)
converts goto instructions
literalt const_literal(bool value)
Definition: literal.h:187
void convert_assignments(decision_proceduret &decision_procedure) const
converts assignments
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
read from a shared variable
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
record an assertion
void convert_assertions(prop_convt &prop_conv)
converts assertions
std::list< SSA_stept > SSA_stepst
void convert_decls(prop_convt &prop_conv) const
converts declarations
Base class for all expressions.
Definition: expr.h:46
virtual void function_return(const exprt &guard, const irep_idt &identifier, const sourcet &source)
just record a location
bool operator<(const symex_target_equationt::SSA_stepst::const_iterator a, const symex_target_equationt::SSA_stepst::const_iterator b)
virtual void location(const exprt &guard, const sourcet &source)
just record a location
void output(const namespacet &ns, std::ostream &out) const
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
declare a fresh variable
std::ostream & operator<<(std::ostream &out, const symex_target_equationt::SSA_stept &step)
void merge_ireps(SSA_stept &SSA_step)
unsigned count_assertions() const
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
void convert_guards(prop_convt &prop_conv)
converts guards
Concrete Goto Program.
void convert_io(decision_proceduret &decision_procedure)
converts I/O