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 <algorithm>
16 #include <iosfwd>
17 #include <list>
18 
19 #include <util/invariant.h>
20 #include <util/merge_irep.h>
21 #include <util/message.h>
22 #include <util/narrow.h>
23 
24 #include "ssa_step.h"
25 #include "symex_target.h"
26 
28 class namespacet;
29 
34 {
35 public:
36  explicit symex_target_equationt(message_handlert &message_handler)
37  : log(message_handler)
38  {
39  }
40 
41  virtual ~symex_target_equationt() = default;
42 
44  virtual void shared_read(
45  const exprt &guard,
46  const ssa_exprt &ssa_object,
47  unsigned atomic_section_id,
48  const sourcet &source);
49 
51  virtual void shared_write(
52  const exprt &guard,
53  const ssa_exprt &ssa_object,
54  unsigned atomic_section_id,
55  const sourcet &source);
56 
58  virtual void assignment(
59  const exprt &guard,
60  const ssa_exprt &ssa_lhs,
61  const exprt &ssa_full_lhs,
62  const exprt &original_full_lhs,
63  const exprt &ssa_rhs,
64  const sourcet &source,
65  assignment_typet assignment_type);
66 
68  virtual void decl(
69  const exprt &guard,
70  const ssa_exprt &ssa_lhs,
71  const exprt &initializer,
72  const sourcet &source,
73  assignment_typet assignment_type);
74 
76  virtual void dead(
77  const exprt &guard,
78  const ssa_exprt &ssa_lhs,
79  const sourcet &source);
80 
82  virtual void function_call(
83  const exprt &guard,
84  const irep_idt &function_id,
85  const std::vector<renamedt<exprt, L2>> &ssa_function_arguments,
86  const sourcet &source,
87  bool hidden);
88 
90  virtual void function_return(
91  const exprt &guard,
92  const irep_idt &function_id,
93  const sourcet &source,
94  bool hidden);
95 
97  virtual void location(
98  const exprt &guard,
99  const sourcet &source);
100 
102  virtual void output(
103  const exprt &guard,
104  const sourcet &source,
105  const irep_idt &output_id,
106  const std::list<renamedt<exprt, L2>> &args);
107 
109  virtual void output_fmt(
110  const exprt &guard,
111  const sourcet &source,
112  const irep_idt &output_id,
113  const irep_idt &fmt,
114  const std::list<exprt> &args);
115 
117  virtual void input(
118  const exprt &guard,
119  const sourcet &source,
120  const irep_idt &input_id,
121  const std::list<exprt> &args);
122 
124  virtual void assumption(
125  const exprt &guard,
126  const exprt &cond,
127  const sourcet &source);
128 
130  virtual void assertion(
131  const exprt &guard,
132  const exprt &cond,
133  const std::string &msg,
134  const sourcet &source);
135 
137  virtual void goto_instruction(
138  const exprt &guard,
139  const renamedt<exprt, L2> &cond,
140  const sourcet &source);
141 
143  virtual void constraint(
144  const exprt &cond,
145  const std::string &msg,
146  const sourcet &source);
147 
149  virtual void spawn(
150  const exprt &guard,
151  const sourcet &source);
152 
154  virtual void memory_barrier(
155  const exprt &guard,
156  const sourcet &source);
157 
159  virtual void atomic_begin(
160  const exprt &guard,
161  unsigned atomic_section_id,
162  const sourcet &source);
163 
165  virtual void atomic_end(
166  const exprt &guard,
167  unsigned atomic_section_id,
168  const sourcet &source);
169 
174  void convert(decision_proceduret &decision_procedure);
175 
183  void convert_without_assertions(decision_proceduret &decision_procedure);
184 
188  void convert_assignments(decision_proceduret &decision_procedure);
189 
194  void convert_decls(decision_proceduret &decision_procedure);
195 
198  void convert_assumptions(decision_proceduret &decision_procedure);
199 
204  void convert_assertions(
205  decision_proceduret &decision_procedure,
206  bool optimized_for_single_assertions = true);
207 
210  void convert_constraints(decision_proceduret &decision_procedure);
211 
215  void convert_goto_instructions(decision_proceduret &decision_procedure);
216 
219  void convert_guards(decision_proceduret &decision_procedure);
220 
224  void convert_function_calls(decision_proceduret &decision_procedure);
225 
229  void convert_io(decision_proceduret &decision_procedure);
230 
232 
233  std::size_t count_assertions() const
234  {
235  return narrow_cast<std::size_t>(std::count_if(
236  SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
237  return step.is_assert() && !step.ignore && !step.converted;
238  }));
239  }
240 
241  std::size_t count_ignored_SSA_steps() const
242  {
243  return narrow_cast<std::size_t>(std::count_if(
244  SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
245  return step.ignore;
246  }));
247  }
248 
249  typedef std::list<SSA_stept> SSA_stepst;
251 
252  SSA_stepst::iterator get_SSA_step(std::size_t s)
253  {
254  SSA_stepst::iterator it=SSA_steps.begin();
255  for(; s!=0; s--)
256  {
257  PRECONDITION(it != SSA_steps.end());
258  it++;
259  }
260  return it;
261  }
262 
263  void output(std::ostream &out) const;
264 
265  void clear()
266  {
267  SSA_steps.clear();
268  }
269 
270  bool has_threads() const
271  {
272  return std::any_of(
273  SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
274  return step.source.thread_nr != 0;
275  });
276  }
277 
278  void validate(const namespacet &ns, const validation_modet vm) const
279  {
280  for(const SSA_stept &step : SSA_steps)
281  step.validate(ns, vm);
282  }
283 
284 protected:
286 
287  // for enforcing sharing in the expressions stored
289  void merge_ireps(SSA_stept &SSA_step);
290 
291  // for unique I/O identifiers
292  std::size_t io_count = 0;
293 
294  // for unique function call argument identifiers
295  std::size_t argument_count = 0;
296 };
297 
298 inline bool operator<(
299  const symex_target_equationt::SSA_stepst::const_iterator a,
300  const symex_target_equationt::SSA_stepst::const_iterator b)
301 {
302  return &(*a)<&(*b);
303 }
304 
305 #endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
Single SSA step in the equation.
Definition: ssa_step.h:47
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:33
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
Record a global constraint: there is no guard limiting its scope.
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Read from a shared variable ssa_object (which is both the left- and the right–hand side of assignment...
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
Record an input.
exprt make_expression() const
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< renamedt< exprt, L2 >> &args)
Record an output.
std::size_t count_assertions() const
SSA_stepst::iterator get_SSA_step(std::size_t s)
void convert_decls(decision_proceduret &decision_procedure)
Converts declarations: these are effectively ignored by the decision procedure.
void convert_assumptions(decision_proceduret &decision_procedure)
Converts assumptions: convert the expression the assumption represents.
std::size_t count_ignored_SSA_steps() const
void convert_without_assertions(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
Record an assumption.
void validate(const namespacet &ns, const validation_modet vm) const
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record a beginning of an atomic section.
std::list< SSA_stept > SSA_stepst
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Write to a shared variable ssa_object: we effectively assign a value from this thread to be visible b...
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
Record formatted output.
virtual void function_return(const exprt &guard, const irep_idt &function_id, const sourcet &source, bool hidden)
Record return from a function.
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record ending an atomic section.
void convert_assignments(decision_proceduret &decision_procedure)
Converts assignments: set the equality lhs==rhs to True.
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
Record an assertion.
void merge_ireps(SSA_stept &SSA_step)
Merging causes identical ireps to be shared.
void convert_guards(decision_proceduret &decision_procedure)
Converts guards: convert the expression the guard represents.
virtual void goto_instruction(const exprt &guard, const renamedt< exprt, L2 > &cond, const sourcet &source)
Record a goto instruction.
symex_target_equationt(message_handlert &message_handler)
void convert(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
virtual ~symex_target_equationt()=default
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
Remove a variable from the scope.
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
void convert_io(decision_proceduret &decision_procedure)
Converts I/O: for each argument build an equality between its symbol and the argument itself.
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 local variable.
void convert_function_calls(decision_proceduret &decision_procedure)
Converts function calls: for each argument build an equality between its symbol and the argument itse...
void convert_constraints(decision_proceduret &decision_procedure)
Converts constraints: set the represented condition to True.
void convert_goto_instructions(decision_proceduret &decision_procedure)
Converts goto instructions: convert the expression representing the condition of this goto.
virtual void memory_barrier(const exprt &guard, const sourcet &source)
Record creating a memory barrier.
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)
Record a function call.
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &initializer, const sourcet &source, assignment_typet assignment_type)
Declare a fresh variable.
void convert_assertions(decision_proceduret &decision_procedure, bool optimized_for_single_assertions=true)
Converts assertions: build a disjunction of negated assertions.
The interface of the target container for symbolic execution to record its symbolic steps into.
Definition: symex_target.h:25
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
Generate Equation using Symbolic Execution.
bool operator<(const symex_target_equationt::SSA_stepst::const_iterator a, const symex_target_equationt::SSA_stepst::const_iterator b)
validation_modet