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;
34 
39 {
40 public:
41  explicit symex_target_equationt(message_handlert &message_handler)
42  : log(message_handler)
43  {
44  }
45 
46  virtual ~symex_target_equationt() = default;
47 
49  virtual void shared_read(
50  const exprt &guard,
51  const ssa_exprt &ssa_object,
52  unsigned atomic_section_id,
53  const sourcet &source);
54 
56  virtual void shared_write(
57  const exprt &guard,
58  const ssa_exprt &ssa_object,
59  unsigned atomic_section_id,
60  const sourcet &source);
61 
63  virtual void assignment(
64  const exprt &guard,
65  const ssa_exprt &ssa_lhs,
66  const exprt &ssa_full_lhs,
67  const exprt &original_full_lhs,
68  const exprt &ssa_rhs,
69  const sourcet &source,
70  assignment_typet assignment_type);
71 
73  virtual void decl(
74  const exprt &guard,
75  const ssa_exprt &ssa_lhs,
76  const exprt &initializer,
77  const sourcet &source,
78  assignment_typet assignment_type);
79 
81  virtual void dead(
82  const exprt &guard,
83  const ssa_exprt &ssa_lhs,
84  const sourcet &source);
85 
87  virtual void function_call(
88  const exprt &guard,
89  const irep_idt &function_id,
90  const std::vector<renamedt<exprt, L2>> &ssa_function_arguments,
91  const sourcet &source,
92  bool hidden);
93 
95  virtual void function_return(
96  const exprt &guard,
97  const irep_idt &function_id,
98  const sourcet &source,
99  bool hidden);
100 
102  virtual void location(
103  const exprt &guard,
104  const sourcet &source);
105 
107  virtual void output(
108  const exprt &guard,
109  const sourcet &source,
110  const irep_idt &output_id,
111  const std::list<renamedt<exprt, L2>> &args);
112 
114  virtual void output_fmt(
115  const exprt &guard,
116  const sourcet &source,
117  const irep_idt &output_id,
118  const irep_idt &fmt,
119  const std::list<exprt> &args);
120 
122  virtual void input(
123  const exprt &guard,
124  const sourcet &source,
125  const irep_idt &input_id,
126  const std::list<exprt> &args);
127 
129  virtual void assumption(
130  const exprt &guard,
131  const exprt &cond,
132  const sourcet &source);
133 
135  virtual void assertion(
136  const exprt &guard,
137  const exprt &cond,
138  const std::string &msg,
139  const sourcet &source);
140 
142  virtual void goto_instruction(
143  const exprt &guard,
144  const renamedt<exprt, L2> &cond,
145  const sourcet &source);
146 
148  virtual void constraint(
149  const exprt &cond,
150  const std::string &msg,
151  const sourcet &source);
152 
154  virtual void spawn(
155  const exprt &guard,
156  const sourcet &source);
157 
159  virtual void memory_barrier(
160  const exprt &guard,
161  const sourcet &source);
162 
164  virtual void atomic_begin(
165  const exprt &guard,
166  unsigned atomic_section_id,
167  const sourcet &source);
168 
170  virtual void atomic_end(
171  const exprt &guard,
172  unsigned atomic_section_id,
173  const sourcet &source);
174 
179  void convert(decision_proceduret &decision_procedure);
180 
188  void convert_without_assertions(decision_proceduret &decision_procedure);
189 
193  void convert_assignments(decision_proceduret &decision_procedure);
194 
199  void convert_decls(decision_proceduret &decision_procedure);
200 
203  void convert_assumptions(decision_proceduret &decision_procedure);
204 
209  void convert_assertions(
210  decision_proceduret &decision_procedure,
211  bool optimized_for_single_assertions = true);
212 
215  void convert_constraints(decision_proceduret &decision_procedure);
216 
220  void convert_goto_instructions(decision_proceduret &decision_procedure);
221 
224  void convert_guards(decision_proceduret &decision_procedure);
225 
229  void convert_function_calls(decision_proceduret &decision_procedure);
230 
234  void convert_io(decision_proceduret &decision_procedure);
235 
237 
238  std::size_t count_assertions() const
239  {
240  return narrow_cast<std::size_t>(std::count_if(
241  SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
242  return step.is_assert() && !step.ignore && !step.converted;
243  }));
244  }
245 
246  std::size_t count_ignored_SSA_steps() const
247  {
248  return narrow_cast<std::size_t>(std::count_if(
249  SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
250  return step.ignore;
251  }));
252  }
253 
254  typedef std::list<SSA_stept> SSA_stepst;
256 
257  SSA_stepst::iterator get_SSA_step(std::size_t s)
258  {
259  SSA_stepst::iterator it=SSA_steps.begin();
260  for(; s!=0; s--)
261  {
262  PRECONDITION(it != SSA_steps.end());
263  it++;
264  }
265  return it;
266  }
267 
268  void output(std::ostream &out) const;
269 
270  void clear()
271  {
272  SSA_steps.clear();
273  }
274 
275  bool has_threads() const
276  {
277  return std::any_of(
278  SSA_steps.begin(), SSA_steps.end(), [](const SSA_stept &step) {
279  return step.source.thread_nr != 0;
280  });
281  }
282 
283  void validate(const namespacet &ns, const validation_modet vm) const
284  {
285  for(const SSA_stept &step : SSA_steps)
286  step.validate(ns, vm);
287  }
288 
289 protected:
291 
292  // for enforcing sharing in the expressions stored
294  void merge_ireps(SSA_stept &SSA_step);
295 
296  // for unique I/O identifiers
297  std::size_t io_count = 0;
298 
299  // for unique function call argument identifiers
300  std::size_t argument_count = 0;
301 };
302 
303 inline bool operator<(
304  const symex_target_equationt::SSA_stepst::const_iterator a,
305  const symex_target_equationt::SSA_stepst::const_iterator b)
306 {
307  return &(*a)<&(*b);
308 }
309 
310 #endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:152
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symex_targett::assignment_typet
assignment_typet
Definition: symex_target.h:70
symex_target_equationt::get_SSA_step
SSA_stepst::iterator get_SSA_step(std::size_t s)
Definition: symex_target_equation.h:257
symex_target_equationt::SSA_stepst
std::list< SSA_stept > SSA_stepst
Definition: symex_target_equation.h:254
symex_target_equationt::assumption
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
Record an assumption.
Definition: symex_target_equation.cpp:261
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:193
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:67
SSA_stept
Single SSA step in the equation.
Definition: ssa_step.h:45
decision_proceduret
Definition: decision_procedure.h:21
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:415
symex_target_equationt::symex_target_equationt
symex_target_equationt(message_handlert &message_handler)
Definition: symex_target_equation.h:41
symex_target_equationt::merge_irep
merge_irept merge_irep
Definition: symex_target_equation.h:293
invariant.h
exprt
Base class for all expressions.
Definition: expr.h:53
symex_target_equationt::argument_count
std::size_t argument_count
Definition: symex_target_equation.h:300
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:358
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:162
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:340
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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:93
symex_target_equationt::count_assertions
std::size_t count_assertions() const
Definition: symex_target_equation.h:238
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:303
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:154
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:565
validation_modet
validation_modet
Definition: validation_mode.h:13
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:438
symex_target_equationt::io_count
std::size_t io_count
Definition: symex_target_equation.h:297
symex_target_equationt::spawn
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
Definition: symex_target_equation.cpp:56
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:373
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:39
symex_target_equationt::merge_ireps
void merge_ireps(SSA_stept &SSA_step)
Merging causes identical ireps to be shared.
Definition: symex_target_equation.cpp:595
symex_target_equationt::has_threads
bool has_threads() const
Definition: symex_target_equation.h:275
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:39
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:79
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:456
symex_target_equationt::count_ignored_SSA_steps
std::size_t count_ignored_SSA_steps() const
Definition: symex_target_equation.h:246
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:275
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:226
merge_irept
Definition: merge_irep.h:106
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:291
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:174
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:537
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:255
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:334
symex_target_equationt::validate
void validate(const namespacet &ns, const validation_modet vm) const
Definition: symex_target_equation.h:283
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:23
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:321
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:305
symex_target_equationt::make_expression
exprt make_expression() const
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:38
symex_target_equationt::clear
void clear()
Definition: symex_target_equation.h:270
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:392
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:128
symex_target.h
symex_targett
The interface of the target container for symbolic execution to record its symbolic steps into.
Definition: symex_target.h:26
renamedt
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:27
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:245
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:209
symex_target_equationt::log
messaget log
Definition: symex_target_equation.h:290
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:106