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 
36 {
37 public:
38  virtual ~symex_target_equationt() = default;
39 
41  virtual void shared_read(
42  const exprt &guard,
43  const ssa_exprt &ssa_object,
44  unsigned atomic_section_id,
45  const sourcet &source);
46 
48  virtual void shared_write(
49  const exprt &guard,
50  const ssa_exprt &ssa_object,
51  unsigned atomic_section_id,
52  const sourcet &source);
53 
55  virtual void assignment(
56  const exprt &guard,
57  const ssa_exprt &ssa_lhs,
58  const exprt &ssa_full_lhs,
59  const exprt &original_full_lhs,
60  const exprt &ssa_rhs,
61  const sourcet &source,
62  assignment_typet assignment_type);
63 
65  virtual void decl(
66  const exprt &guard,
67  const ssa_exprt &ssa_lhs,
68  const sourcet &source,
69  assignment_typet assignment_type);
70 
72  virtual void dead(
73  const exprt &guard,
74  const ssa_exprt &ssa_lhs,
75  const sourcet &source);
76 
78  virtual void function_call(
79  const exprt &guard,
80  const irep_idt &function_identifier,
81  const std::vector<exprt> &ssa_function_arguments,
82  const sourcet &source,
83  bool hidden);
84 
86  virtual void
87  function_return(const exprt &guard, const sourcet &source, bool hidden);
88 
90  virtual void location(
91  const exprt &guard,
92  const sourcet &source);
93 
95  virtual void output(
96  const exprt &guard,
97  const sourcet &source,
98  const irep_idt &output_id,
99  const std::list<exprt> &args);
100 
102  virtual void output_fmt(
103  const exprt &guard,
104  const sourcet &source,
105  const irep_idt &output_id,
106  const irep_idt &fmt,
107  const std::list<exprt> &args);
108 
110  virtual void input(
111  const exprt &guard,
112  const sourcet &source,
113  const irep_idt &input_id,
114  const std::list<exprt> &args);
115 
117  virtual void assumption(
118  const exprt &guard,
119  const exprt &cond,
120  const sourcet &source);
121 
123  virtual void assertion(
124  const exprt &guard,
125  const exprt &cond,
126  const std::string &msg,
127  const sourcet &source);
128 
130  virtual void goto_instruction(
131  const exprt &guard,
132  const exprt &cond,
133  const sourcet &source);
134 
136  virtual void constraint(
137  const exprt &cond,
138  const std::string &msg,
139  const sourcet &source);
140 
142  virtual void spawn(
143  const exprt &guard,
144  const sourcet &source);
145 
147  virtual void memory_barrier(
148  const exprt &guard,
149  const sourcet &source);
150 
152  virtual void atomic_begin(
153  const exprt &guard,
154  unsigned atomic_section_id,
155  const sourcet &source);
156 
158  virtual void atomic_end(
159  const exprt &guard,
160  unsigned atomic_section_id,
161  const sourcet &source);
162 
167  void convert(prop_convt &prop_conv);
168 
172  void convert_assignments(decision_proceduret &decision_procedure) const;
173 
177  void convert_decls(prop_convt &prop_conv) const;
178 
181  void convert_assumptions(prop_convt &prop_conv);
182 
185  void convert_assertions(prop_convt &prop_conv);
186 
190  void convert_constraints(decision_proceduret &decision_procedure) const;
191 
195  void convert_goto_instructions(prop_convt &prop_conv);
196 
199  void convert_guards(prop_convt &prop_conv);
200 
205  void convert_function_calls(decision_proceduret &decision_procedure);
206 
211  void convert_io(decision_proceduret &decision_procedure);
212 
213  exprt make_expression() const;
214 
243  class SSA_stept
244  {
245  public:
246  sourcet source;
248 
249  // NOLINTNEXTLINE(whitespace/line_length)
251  // NOLINTNEXTLINE(whitespace/line_length)
253  // NOLINTNEXTLINE(whitespace/line_length)
255  // NOLINTNEXTLINE(whitespace/line_length)
256  bool is_goto() const { return type==goto_trace_stept::typet::GOTO; }
257  // NOLINTNEXTLINE(whitespace/line_length)
259  // NOLINTNEXTLINE(whitespace/line_length)
261  // NOLINTNEXTLINE(whitespace/line_length)
263  // NOLINTNEXTLINE(whitespace/line_length)
264  bool is_decl() const { return type==goto_trace_stept::typet::DECL; }
265  // NOLINTNEXTLINE(whitespace/line_length)
267  // NOLINTNEXTLINE(whitespace/line_length)
269  // NOLINTNEXTLINE(whitespace/line_length)
271  // NOLINTNEXTLINE(whitespace/line_length)
273  // NOLINTNEXTLINE(whitespace/line_length)
274  bool is_spawn() const { return type==goto_trace_stept::typet::SPAWN; }
275  // NOLINTNEXTLINE(whitespace/line_length)
277  // NOLINTNEXTLINE(whitespace/line_length)
279  // NOLINTNEXTLINE(whitespace/line_length)
281 
282  // we may choose to hide
283  bool hidden=false;
284 
287 
288  // for ASSIGNMENT and DECL
293 
294  // for ASSUME/ASSERT/GOTO/CONSTRAINT
297  std::string comment;
298 
299  // for INPUT/OUTPUT
301  bool formatted=false;
302  std::list<exprt> io_args;
303  std::list<exprt> converted_io_args;
304 
305  // for function calls: the function that is called
307 
308  // for function calls
309  std::vector<exprt> ssa_function_arguments,
311 
312  // for SHARED_READ/SHARED_WRITE and ATOMIC_BEGIN/ATOMIC_END
313  unsigned atomic_section_id=0;
314 
315  // for slicing
316  bool ignore=false;
317 
319  type(goto_trace_stept::typet::NONE),
320  hidden(false),
321  guard(static_cast<const exprt &>(get_nil_irep())),
323  ssa_lhs(static_cast<const ssa_exprt &>(get_nil_irep())),
324  ssa_full_lhs(static_cast<const exprt &>(get_nil_irep())),
325  original_full_lhs(static_cast<const exprt &>(get_nil_irep())),
326  ssa_rhs(static_cast<const exprt &>(get_nil_irep())),
328  cond_expr(static_cast<const exprt &>(get_nil_irep())),
329  cond_literal(const_literal(false)),
330  formatted(false),
332  ignore(false)
333  {
334  }
335 
336  DEPRECATED("Use output without ns param")
337  void output(
338  const namespacet &ns,
339  std::ostream &out) const;
340 
341  void output(std::ostream &out) const;
342 
343  void validate(const namespacet &ns, const validation_modet vm) const;
344  };
345 
346  std::size_t count_assertions() const
347  {
348  std::size_t i=0;
349  for(SSA_stepst::const_iterator
350  it=SSA_steps.begin();
351  it!=SSA_steps.end(); it++)
352  if(it->is_assert())
353  i++;
354  return i;
355  }
356 
357  std::size_t count_ignored_SSA_steps() const
358  {
359  std::size_t i=0;
360  for(SSA_stepst::const_iterator
361  it=SSA_steps.begin();
362  it!=SSA_steps.end(); it++)
363  if(it->ignore)
364  i++;
365  return i;
366  }
367 
368  typedef std::list<SSA_stept> SSA_stepst;
370 
371  SSA_stepst::iterator get_SSA_step(std::size_t s)
372  {
373  SSA_stepst::iterator it=SSA_steps.begin();
374  for(; s!=0; s--)
375  {
376  PRECONDITION(it != SSA_steps.end());
377  it++;
378  }
379  return it;
380  }
381 
382  void output(std::ostream &out, const namespacet &ns) const;
383 
384  void clear()
385  {
386  SSA_steps.clear();
387  }
388 
389  bool has_threads() const
390  {
391  for(SSA_stepst::const_iterator it=SSA_steps.begin();
392  it!=SSA_steps.end();
393  it++)
394  if(it->source.thread_nr!=0)
395  return true;
396 
397  return false;
398  }
399 
400  void validate(const namespacet &ns, const validation_modet vm) const
401  {
402  for(const SSA_stept &step : SSA_steps)
403  step.validate(ns, vm);
404  }
405 
406 protected:
407  // for enforcing sharing in the expressions stored
409  void merge_ireps(SSA_stept &SSA_step);
410 };
411 
412 inline bool operator<(
413  const symex_target_equationt::SSA_stepst::const_iterator a,
414  const symex_target_equationt::SSA_stepst::const_iterator b)
415 {
416  return &(*a)<&(*b);
417 }
418 
419 #endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
const irept & get_nil_irep()
Definition: irep.cpp:55
The type of an expression, extends irept.
Definition: type.h:27
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
SSA_stepst::iterator get_SSA_step(std::size_t s)
virtual void memory_barrier(const exprt &guard, const sourcet &source)
Record creating a memory barrier.
void convert(prop_convt &prop_conv)
Interface method to initiate the conversion into a decision procedure format.
exprt make_expression() const
void convert_assumptions(prop_convt &prop_conv)
Converts assumptions: convert the expression the assumption represents.
virtual void function_call(const exprt &guard, const irep_idt &function_identifier, const std::vector< exprt > &ssa_function_arguments, const sourcet &source, bool hidden)
Record a function call.
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)
Record an input.
virtual void goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)
Record a goto instruction.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual void function_return(const exprt &guard, const sourcet &source, bool hidden)
Record return from a function.
Traces of GOTO Programs.
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< exprt > &args)
Record an output.
STL namespace.
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record a beginning of an atomic section.
TO_BE_DOCUMENTED.
Definition: goto_trace.h:30
void validate(const namespacet &ns, const validation_modet vm) const
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record ending 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 shared variable ssa_object: we effectively assign a value from this thread to be visible b...
void convert_function_calls(decision_proceduret &decision_procedure)
Converts function calls: for each argument build an equality between its symbol and the argument itse...
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
Record a global constraint: there is no guard limiting its scope.
void convert_constraints(decision_proceduret &decision_procedure) const
Converts constraints: set the represented condition to True.
Identifies source in the context of symbolic execution.
Definition: symex_target.h:35
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)
Declare a fresh variable.
The interface of the target container for symbolic execution to record its symbolic steps into...
Definition: symex_target.h:23
virtual ~symex_target_equationt()=default
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
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.
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
#define DEPRECATED(msg)
Definition: deprecate.h:23
void convert_goto_instructions(prop_convt &prop_conv)
Converts goto instructions: convert the expression representing the condition of this goto...
literalt const_literal(bool value)
Definition: literal.h:187
void convert_assignments(decision_proceduret &decision_procedure) const
Converts assignments: set the equality lhs==rhs to True.
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 assignme...
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: build a disjunction of negated assertions.
Single SSA step in the equation.
std::list< SSA_stept > SSA_stepst
void convert_decls(prop_convt &prop_conv) const
Converts declarations: these are effectively ignored by the decision procedure.
Base class for all expressions.
Definition: expr.h:54
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)
Record a location.
std::size_t count_assertions() const
validation_modet
std::size_t count_ignored_SSA_steps() const
void output(const namespacet &ns, std::ostream &out) const
void validate(const namespacet &ns, const validation_modet vm) const
Check that the SSA step is well-formed.
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
Remove a variable from the scope.
std::vector< exprt > converted_function_arguments
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: convert the expression the guard represents.
Concrete Goto Program.
void convert_io(decision_proceduret &decision_procedure)
Converts I/O: for each argument build an equality between its symbol and the argument itself...