CBMC
precondition.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "precondition.h"
13 
14 #include <util/find_symbols.h>
15 #include <util/pointer_expr.h>
16 
18 
19 #include "renaming_level.h"
20 #include "symex_target_equation.h"
21 
23 {
24 public:
26  const namespacet &_ns,
27  value_setst &_value_sets,
28  const goto_programt::const_targett _target,
29  const SSA_stept &_SSA_step,
30  const goto_symex_statet &_s,
32  : ns(_ns),
33  value_sets(_value_sets),
34  target(_target),
35  SSA_step(_SSA_step),
36  s(_s),
38  {
39  }
40 
41 protected:
42  const namespacet &ns;
48  void compute_rec(exprt &dest);
49 
50 public:
51  void compute(exprt &dest);
52 
53 protected:
54  void compute_address_of(exprt &dest);
55 };
56 
58  const namespacet &ns,
59  value_setst &value_sets,
60  const goto_programt::const_targett target,
61  const symex_target_equationt &equation,
62  const goto_symex_statet &s,
63  exprt &dest,
64  message_handlert &message_handler)
65 {
66  for(symex_target_equationt::SSA_stepst::const_reverse_iterator
67  it=equation.SSA_steps.rbegin();
68  it!=equation.SSA_steps.rend();
69  it++)
70  {
71  preconditiont precondition(ns, value_sets, target, *it, s, message_handler);
72  precondition.compute(dest);
73  if(dest.is_false())
74  return;
75  }
76 }
77 
79 {
80  if(dest.id()==ID_symbol)
81  {
82  // leave alone
83  }
84  else if(dest.id()==ID_index)
85  {
86  auto &index_expr = to_index_expr(dest);
87  compute_address_of(index_expr.array());
88  compute(index_expr.index());
89  }
90  else if(dest.id()==ID_member)
91  {
92  compute_address_of(to_member_expr(dest).compound());
93  }
94  else if(dest.id()==ID_dereference)
95  {
96  compute(to_dereference_expr(dest).pointer());
97  }
98 }
99 
101 {
102  compute_rec(dest);
103 }
104 
106 {
107  if(dest.id()==ID_address_of)
108  {
109  // only do index!
110  compute_address_of(to_address_of_expr(dest).object());
111  }
112  else if(dest.id()==ID_dereference)
113  {
114  auto &deref_expr = to_dereference_expr(dest);
115 
116  const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
117 
118  // aliasing may happen here
119 
120  bool may_alias = false;
121  for(const exprt &e : value_sets.get_values(
123  {
124  if(has_symbol_expr(e, lhs_identifier, false))
125  {
126  may_alias = true;
127  break;
128  }
129  }
130 
131  if(may_alias)
132  {
133  exprt tmp;
134  tmp.swap(deref_expr.pointer());
135  dereference(
137  target,
138  tmp,
139  ns,
140  value_sets,
142  deref_expr.swap(tmp);
144  }
145  else
146  {
147  // nah, ok
148  compute_rec(deref_expr.pointer());
149  }
150  }
151  else if(dest==SSA_step.ssa_lhs.get_original_expr())
152  {
154  }
155  else
156  Forall_operands(it, dest)
157  compute_rec(*it);
158 }
Single SSA step in the equation.
Definition: ssa_step.h:47
exprt ssa_rhs
Definition: ssa_step.h:141
symex_targett::sourcet source
Definition: ssa_step.h:49
ssa_exprt ssa_lhs
Definition: ssa_step.h:139
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
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:34
instructionst::const_iterator const_targett
Definition: goto_program.h:615
Central data structure: state.
const irep_idt & id() const
Definition: irep.h:384
void swap(irept &irep)
Definition: irep.h:430
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
value_setst & value_sets
const goto_programt::const_targett target
message_handlert & message_handler
preconditiont(const namespacet &_ns, value_setst &_value_sets, const goto_programt::const_targett _target, const SSA_stept &_SSA_step, const goto_symex_statet &_s, message_handlert &message_handler)
const namespacet & ns
void compute_address_of(exprt &dest)
void compute_rec(exprt &dest)
const SSA_stept & SSA_step
const goto_symex_statet & s
void compute(exprt &dest)
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
irep_idt get_object_name() const
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual std::vector< exprt > get_values(const irep_idt &function_id, goto_programt::const_targett l, const exprt &expr)=0
#define Forall_operands(it, expr)
Definition: expr.h:27
bool has_symbol_expr(const exprt &src, const irep_idt &identifier, bool include_bound_symbols)
Returns true if one of the symbol expressions in src has identifier identifier; if include_bound_symb...
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets, message_handlert &message_handler)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
std::optional< exprt > may_alias(const exprt &a, const exprt &b, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &ns)
Definition: may_alias.cpp:221
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:890
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
void precondition(const namespacet &ns, value_setst &value_sets, const goto_programt::const_targett target, const symex_target_equationt &equation, const goto_symex_statet &s, exprt &dest, message_handlert &message_handler)
Generate Equation using Symbolic Execution.
exprt get_original_name(exprt expr)
Undo all levels of renaming.
Renaming levels.
exprt deref_expr(const exprt &expr)
Wraps a given expression into a dereference_exprt unless it is an address_of_exprt in which case it j...
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2933
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1533
Generate Equation using Symbolic Execution.