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 
26 
27 #include "renaming_level.h"
28 #include "ssa_step.h"
29 #include "symex_target.h"
30 
32 class namespacet;
35 struct solver_hardnesst;
36 
41 {
42 public:
43  explicit symex_target_equationt(message_handlert &message_handler)
44  : log(message_handler)
45  {
46  }
47 
48  virtual ~symex_target_equationt() = default;
49 
51  virtual void shared_read(
52  const exprt &guard,
53  const ssa_exprt &ssa_object,
54  unsigned atomic_section_id,
55  const sourcet &source);
56 
58  virtual void shared_write(
59  const exprt &guard,
60  const ssa_exprt &ssa_object,
61  unsigned atomic_section_id,
62  const sourcet &source);
63 
65  virtual void assignment(
66  const exprt &guard,
67  const ssa_exprt &ssa_lhs,
68  const exprt &ssa_full_lhs,
69  const exprt &original_full_lhs,
70  const exprt &ssa_rhs,
71  const sourcet &source,
72  assignment_typet assignment_type);
73 
75  virtual void decl(
76  const exprt &guard,
77  const ssa_exprt &ssa_lhs,
78  const exprt &initializer,
79  const sourcet &source,
80  assignment_typet assignment_type);
81 
83  virtual void dead(
84  const exprt &guard,
85  const ssa_exprt &ssa_lhs,
86  const sourcet &source);
87 
89  virtual void function_call(
90  const exprt &guard,
91  const irep_idt &function_id,
92  const std::vector<renamedt<exprt, L2>> &ssa_function_arguments,
93  const sourcet &source,
94  bool hidden);
95 
97  virtual void function_return(
98  const exprt &guard,
99  const irep_idt &function_id,
100  const sourcet &source,
101  bool hidden);
102 
104  virtual void location(
105  const exprt &guard,
106  const sourcet &source);
107 
109  virtual void output(
110  const exprt &guard,
111  const sourcet &source,
112  const irep_idt &output_id,
113  const std::list<renamedt<exprt, L2>> &args);
114 
116  virtual void output_fmt(
117  const exprt &guard,
118  const sourcet &source,
119  const irep_idt &output_id,
120  const irep_idt &fmt,
121  const std::list<exprt> &args);
122 
124  virtual void input(
125  const exprt &guard,
126  const sourcet &source,
127  const irep_idt &input_id,
128  const std::list<exprt> &args);
129 
131  virtual void assumption(
132  const exprt &guard,
133  const exprt &cond,
134  const sourcet &source);
135 
137  virtual void assertion(
138  const exprt &guard,
139  const exprt &cond,
140  const std::string &msg,
141  const sourcet &source);
142 
144  virtual void goto_instruction(
145  const exprt &guard,
146  const renamedt<exprt, L2> &cond,
147  const sourcet &source);
148 
150  virtual void constraint(
151  const exprt &cond,
152  const std::string &msg,
153  const sourcet &source);
154 
156  virtual void spawn(
157  const exprt &guard,
158  const sourcet &source);
159 
161  virtual void memory_barrier(
162  const exprt &guard,
163  const sourcet &source);
164 
166  virtual void atomic_begin(
167  const exprt &guard,
168  unsigned atomic_section_id,
169  const sourcet &source);
170 
172  virtual void atomic_end(
173  const exprt &guard,
174  unsigned atomic_section_id,
175  const sourcet &source);
176 
181  void convert(decision_proceduret &decision_procedure);
182 
190  void convert_without_assertions(decision_proceduret &decision_procedure);
191 
195  void convert_assignments(decision_proceduret &decision_procedure);
196 
201  void convert_decls(decision_proceduret &decision_procedure);
202 
205  void convert_assumptions(decision_proceduret &decision_procedure);
206 
211  void convert_assertions(
212  decision_proceduret &decision_procedure,
213  bool optimized_for_single_assertions = true);
214 
217  void convert_constraints(decision_proceduret &decision_procedure);
218 
222  void convert_goto_instructions(decision_proceduret &decision_procedure);
223 
226  void convert_guards(decision_proceduret &decision_procedure);
227 
231  void convert_function_calls(decision_proceduret &decision_procedure);
232 
236  void convert_io(decision_proceduret &decision_procedure);
237 
238  exprt make_expression() const;
239 
240  std::size_t count_assertions() const
241  {
242  return narrow_cast<std::size_t>(std::count_if(
243  SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
244  return step.is_assert() && !step.ignore && !step.converted;
245  }));
246  }
247 
248  std::size_t count_ignored_SSA_steps() const
249  {
250  return narrow_cast<std::size_t>(std::count_if(
251  SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
252  return step.ignore;
253  }));
254  }
255 
256  typedef std::list<SSA_stept> SSA_stepst;
258 
259  SSA_stepst::iterator get_SSA_step(std::size_t s)
260  {
261  SSA_stepst::iterator it=SSA_steps.begin();
262  for(; s!=0; s--)
263  {
264  PRECONDITION(it != SSA_steps.end());
265  it++;
266  }
267  return it;
268  }
269 
270  void output(std::ostream &out) const;
271 
272  void clear()
273  {
274  SSA_steps.clear();
275  }
276 
277  bool has_threads() const
278  {
279  return std::any_of(
280  SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
281  return step.source.thread_nr != 0;
282  });
283  }
284 
285  void validate(const namespacet &ns, const validation_modet vm) const
286  {
287  for(const SSA_stept &step : SSA_steps)
288  step.validate(ns, vm);
289  }
290 
291 protected:
293 
294  // for enforcing sharing in the expressions stored
296  void merge_ireps(SSA_stept &SSA_step);
297 
298  // for unique I/O identifiers
299  std::size_t io_count = 0;
300 
301  // for unique function call argument identifiers
302  std::size_t argument_count = 0;
303 };
304 
305 inline bool operator<(
306  const symex_target_equationt::SSA_stepst::const_iterator a,
307  const symex_target_equationt::SSA_stepst::const_iterator b)
308 {
309  return &(*a)<&(*b);
310 }
311 
312 #endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
symex_targett::assignment_typet
assignment_typet
Definition: symex_target.h:69
symex_target_equationt::get_SSA_step
SSA_stepst::iterator get_SSA_step(std::size_t s)
Definition: symex_target_equation.h:259
symex_target_equationt::SSA_stepst
std::list< SSA_stept > SSA_stepst
Definition: symex_target_equation.h:256
symex_target_equationt::assumption
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
Record an assumption.
Definition: symex_target_equation.cpp:270
merge_irep.h
symex_target_equationt::function_return
virtual void function_return(const exprt &guard, const irep_idt &function_id, const sourcet &source, bool hidden)
Record return from a function.
Definition: symex_target_equation.cpp:202
symex_target_equationt::memory_barrier
virtual void memory_barrier(const exprt &guard, const sourcet &source)
Record creating a memory barrier.
Definition: symex_target_equation.cpp:76
SSA_stept
Single SSA step in the equation.
Definition: ssa_step.h:44
decision_proceduret
Definition: decision_procedure.h:20
symex_target_equationt::convert_goto_instructions
void convert_goto_instructions(decision_proceduret &decision_procedure)
Converts goto instructions: convert the expression representing the condition of this goto.
Definition: symex_target_equation.cpp:445
symex_target_equationt::symex_target_equationt
symex_target_equationt(message_handlert &message_handler)
Definition: symex_target_equation.h:43
symex_target_equationt::merge_irep
merge_irept merge_irep
Definition: symex_target_equation.h:295
invariant.h
exprt
Base class for all expressions.
Definition: expr.h:52
symex_target_equationt::argument_count
std::size_t argument_count
Definition: symex_target_equation.h:302
symex_target_equationt::convert_decls
void convert_decls(decision_proceduret &decision_procedure)
Converts declarations: these are effectively ignored by the decision procedure.
Definition: symex_target_equation.cpp:375
ssa_step.h
narrow.h
goto_trace.h
symex_target_equationt::location
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
Definition: symex_target_equation.cpp:171
symex_target_equationt::convert_assignments
void convert_assignments(decision_proceduret &decision_procedure)
Converts assignments: set the equality lhs==rhs to True.
Definition: symex_target_equation.cpp:353
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:16
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
symex_target_equationt::atomic_end
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record ending an atomic section.
Definition: symex_target_equation.cpp:102
symex_target_equationt::count_assertions
std::size_t count_assertions() const
Definition: symex_target_equation.h:240
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
renaming_level.h
operator<
bool operator<(const symex_target_equationt::SSA_stepst::const_iterator a, const symex_target_equationt::SSA_stepst::const_iterator b)
Definition: symex_target_equation.h:305
symex_target_equationt::dead
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
Remove a variable from the scope.
Definition: symex_target_equation.cpp:163
symex_target_equationt::convert_io
void convert_io(decision_proceduret &decision_procedure)
Converts I/O: for each argument build an equality between its symbol and the argument itself.
Definition: symex_target_equation.cpp:647
validation_modet
validation_modet
Definition: validation_mode.h:12
message_handlert
Definition: message.h:27
symex_target_equationt::convert_constraints
void convert_constraints(decision_proceduret &decision_procedure)
Converts constraints: set the represented condition to True.
Definition: symex_target_equation.cpp:472
symex_target_equationt::io_count
std::size_t io_count
Definition: symex_target_equation.h:299
symex_target_equationt::spawn
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
Definition: symex_target_equation.cpp:65
symex_target_equationt::convert_guards
void convert_guards(decision_proceduret &decision_procedure)
Converts guards: convert the expression the guard represents.
Definition: symex_target_equation.cpp:394
symex_target_equationt::shared_write
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...
Definition: symex_target_equation.cpp:48
symex_target_equationt::merge_ireps
void merge_ireps(SSA_stept &SSA_step)
Merging causes identical ireps to be shared.
Definition: symex_target_equation.cpp:688
symex_target_equationt::has_threads
bool has_threads() const
Definition: symex_target_equation.h:277
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:40
goto_program.h
symex_target_equationt::atomic_begin
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record a beginning of an atomic section.
Definition: symex_target_equation.cpp:88
symex_target_equationt::convert_assertions
void convert_assertions(decision_proceduret &decision_procedure, bool optimized_for_single_assertions=true)
Converts assertions: build a disjunction of negated assertions.
Definition: symex_target_equation.cpp:495
symex_target_equationt::count_ignored_SSA_steps
std::size_t count_ignored_SSA_steps() const
Definition: symex_target_equation.h:248
symex_target_equationt::assertion
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
Record an assertion.
Definition: symex_target_equation.cpp:284
symex_target_equationt::output_fmt
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.
Definition: symex_target_equation.cpp:235
merge_irept
Definition: merge_irep.h:105
symex_target_equationt::goto_instruction
virtual void goto_instruction(const exprt &guard, const renamedt< exprt, L2 > &cond, const sourcet &source)
Record a goto instruction.
Definition: symex_target_equation.cpp:300
solver_hardnesst
A structure that facilitates collecting the complexity statistics from a decision procedure.
Definition: solver_hardness.h:44
symex_target_equationt::function_call
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.
Definition: symex_target_equation.cpp:183
symex_target_equationt::convert_function_calls
void convert_function_calls(decision_proceduret &decision_procedure)
Converts function calls: for each argument build an equality between its symbol and the argument itse...
Definition: symex_target_equation.cpp:607
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:257
symex_target_equationt::convert
void convert(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
Definition: symex_target_equation.cpp:347
symex_target_equationt::validate
void validate(const namespacet &ns, const validation_modet vm) const
Definition: symex_target_equation.h:285
symex_target_equationt::shared_read
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...
Definition: symex_target_equation.cpp:32
symex_target_equationt::convert_without_assertions
void convert_without_assertions(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
Definition: symex_target_equation.cpp:330
symex_target_equationt::constraint
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
Record a global constraint: there is no guard limiting its scope.
Definition: symex_target_equation.cpp:314
symex_target_equationt::make_expression
exprt make_expression() const
hardness_collectort
Definition: hardness_collector.h:22
symex_target_equationt::clear
void clear()
Definition: symex_target_equation.h:272
symex_target_equationt::convert_assumptions
void convert_assumptions(decision_proceduret &decision_procedure)
Converts assumptions: convert the expression the assumption represents.
Definition: symex_target_equation.cpp:417
symex_target_equationt::~symex_target_equationt
virtual ~symex_target_equationt()=default
message.h
symex_target_equationt::decl
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.
Definition: symex_target_equation.cpp:137
symex_target.h
symex_targett
The interface of the target container for symbolic execution to record its symbolic steps into.
Definition: symex_target.h:25
renamedt
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:26
symex_target_equationt::input
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
Record an input.
Definition: symex_target_equation.cpp:254
symex_target_equationt::output
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< renamedt< exprt, L2 >> &args)
Record an output.
Definition: symex_target_equation.cpp:218
symex_target_equationt::log
messaget log
Definition: symex_target_equation.h:292
symex_target_equationt::assignment
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.
Definition: symex_target_equation.cpp:115