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/invariant.h>
19 #include <util/merge_irep.h>
20 
23 
24 #include <solvers/prop/literal.h>
25 
26 #include "symex_target.h"
27 
29 class namespacet;
30 class prop_convt;
31 
33 {
34 public:
35  virtual ~symex_target_equationt() = default;
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)
178  // NOLINTNEXTLINE(whitespace/line_length)
180  // NOLINTNEXTLINE(whitespace/line_length)
182  // NOLINTNEXTLINE(whitespace/line_length)
183  bool is_goto() const { return type==goto_trace_stept::typet::GOTO; }
184  // NOLINTNEXTLINE(whitespace/line_length)
186  // NOLINTNEXTLINE(whitespace/line_length)
188  // NOLINTNEXTLINE(whitespace/line_length)
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)
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())),
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())),
251  cond_expr(static_cast<const exprt &>(get_nil_irep())),
252  cond_literal(const_literal(false)),
253  formatted(false),
255  ignore(false)
256  {
257  }
258 
259  DEPRECATED("Use output without ns param")
260  void output(
261  const namespacet &ns,
262  std::ostream &out) const;
263 
264  void output(std::ostream &out) const;
265  };
266 
267  std::size_t count_assertions() const
268  {
269  std::size_t i=0;
270  for(SSA_stepst::const_iterator
271  it=SSA_steps.begin();
272  it!=SSA_steps.end(); it++)
273  if(it->is_assert())
274  i++;
275  return i;
276  }
277 
278  std::size_t count_ignored_SSA_steps() const
279  {
280  std::size_t i=0;
281  for(SSA_stepst::const_iterator
282  it=SSA_steps.begin();
283  it!=SSA_steps.end(); it++)
284  if(it->ignore)
285  i++;
286  return i;
287  }
288 
289  typedef std::list<SSA_stept> SSA_stepst;
291 
292  SSA_stepst::iterator get_SSA_step(std::size_t s)
293  {
294  SSA_stepst::iterator it=SSA_steps.begin();
295  for(; s!=0; s--)
296  {
297  PRECONDITION(it != SSA_steps.end());
298  it++;
299  }
300  return it;
301  }
302 
303  void output(std::ostream &out, const namespacet &ns) const;
304 
305  void clear()
306  {
307  SSA_steps.clear();
308  }
309 
310  bool has_threads() const
311  {
312  for(SSA_stepst::const_iterator it=SSA_steps.begin();
313  it!=SSA_steps.end();
314  it++)
315  if(it->source.thread_nr!=0)
316  return true;
317 
318  return false;
319  }
320 
321 protected:
322  // for enforcing sharing in the expressions stored
324  void merge_ireps(SSA_stept &SSA_step);
325 };
326 
327 inline bool operator<(
328  const symex_target_equationt::SSA_stepst::const_iterator a,
329  const symex_target_equationt::SSA_stepst::const_iterator b)
330 {
331  return &(*a)<&(*b);
332 }
333 
334 #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:22
virtual void spawn(const exprt &guard, const sourcet &source)
spawn a new thread
SSA_stepst::iterator get_SSA_step(std::size_t s)
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.
STL namespace.
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:36
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
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
record a constraint
void convert_constraints(decision_proceduret &decision_procedure) const
converts constraints
DEPRECATED("use instrument_cover_goals(goto_programt &goto_program," "const cover_instrumenterst &instrumenters," "message_handlert &message_handler, const irep_idt mode) instead") void instrument_cover_goals(const symbol_tablet &symbol_table
Instruments goto program for a given coverage criterion.
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)
declare a fresh variable
virtual ~symex_target_equationt()=default
TO_BE_DOCUMENTED.
Definition: namespace.h:74
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
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
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:42
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
std::size_t count_assertions() const
std::size_t count_ignored_SSA_steps() const
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
void merge_ireps(SSA_stept &SSA_step)
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