CBMC
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 irep_idt &property_id,
134  const std::string &msg,
135  const sourcet &source);
136 
138  virtual void goto_instruction(
139  const exprt &guard,
140  const renamedt<exprt, L2> &cond,
141  const sourcet &source);
142 
144  virtual void constraint(
145  const exprt &cond,
146  const std::string &msg,
147  const sourcet &source);
148 
150  virtual void spawn(
151  const exprt &guard,
152  const sourcet &source);
153 
155  virtual void memory_barrier(
156  const exprt &guard,
157  const sourcet &source);
158 
160  virtual void atomic_begin(
161  const exprt &guard,
162  unsigned atomic_section_id,
163  const sourcet &source);
164 
166  virtual void atomic_end(
167  const exprt &guard,
168  unsigned atomic_section_id,
169  const sourcet &source);
170 
175  void convert(decision_proceduret &decision_procedure);
176 
184  void convert_without_assertions(decision_proceduret &decision_procedure);
185 
189  void convert_assignments(decision_proceduret &decision_procedure);
190 
195  void convert_decls(decision_proceduret &decision_procedure);
196 
199  void convert_assumptions(decision_proceduret &decision_procedure);
200 
205  void convert_assertions(
206  decision_proceduret &decision_procedure,
207  bool optimized_for_single_assertions = true);
208 
211  void convert_constraints(decision_proceduret &decision_procedure);
212 
216  void convert_goto_instructions(decision_proceduret &decision_procedure);
217 
220  void convert_guards(decision_proceduret &decision_procedure);
221 
225  void convert_function_calls(decision_proceduret &decision_procedure);
226 
230  void convert_io(decision_proceduret &decision_procedure);
231 
233 
234  std::size_t count_assertions() const
235  {
236  return narrow_cast<std::size_t>(std::count_if(
237  SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
238  return step.is_assert() && !step.ignore && !step.converted;
239  }));
240  }
241 
242  std::size_t count_ignored_SSA_steps() const
243  {
244  return narrow_cast<std::size_t>(std::count_if(
245  SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
246  return step.ignore;
247  }));
248  }
249 
250  typedef std::list<SSA_stept> SSA_stepst;
252 
253  SSA_stepst::iterator get_SSA_step(std::size_t s)
254  {
255  SSA_stepst::iterator it=SSA_steps.begin();
256  for(; s!=0; s--)
257  {
258  PRECONDITION(it != SSA_steps.end());
259  it++;
260  }
261  return it;
262  }
263 
264  void output(std::ostream &out) const;
265 
266  void clear()
267  {
268  SSA_steps.clear();
269  }
270 
271  bool has_threads() const
272  {
273  return std::any_of(
274  SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
275  return step.source.thread_nr != 0;
276  });
277  }
278 
279  void validate(const namespacet &ns, const validation_modet vm) const
280  {
281  for(const SSA_stept &step : SSA_steps)
282  step.validate(ns, vm);
283  }
284 
285 protected:
287 
288  // for enforcing sharing in the expressions stored
290  void merge_ireps(SSA_stept &SSA_step);
291 
292  // for unique I/O identifiers
293  std::size_t io_count = 0;
294 
295  // for unique function call argument identifiers
296  std::size_t argument_count = 0;
297 };
298 
299 inline bool operator<(
300  const symex_target_equationt::SSA_stepst::const_iterator a,
301  const symex_target_equationt::SSA_stepst::const_iterator b)
302 {
303  return &(*a)<&(*b);
304 }
305 
306 #endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
static exprt guard(const exprt::operandst &guards, exprt cond)
Single SSA step in the equation.
Definition: ssa_step.h:47
An interface for a decision procedure for satisfiability problems.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
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 assertion(const exprt &guard, const exprt &cond, const irep_idt &property_id, const std::string &msg, const sourcet &source)
Record an assertion.
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.
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