cprover
postcondition.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 "postcondition.h"
13 
14 #include <util/find_symbols.h>
15 #include <util/std_expr.h>
16 
17 #include "goto_symex_state.h"
18 
20 {
21 public:
23  const namespacet &_ns,
24  const value_sett &_value_set,
25  const symex_target_equationt::SSA_stept &_SSA_step,
26  const goto_symex_statet &_s):
27  ns(_ns),
28  value_set(_value_set),
29  SSA_step(_SSA_step),
30  s(_s)
31  {
32  }
33 
34 protected:
35  const namespacet &ns;
39 
40 public:
41  void compute(exprt &dest);
42 
43 protected:
44  void strengthen(exprt &dest);
45  void weaken(exprt &dest);
46  bool is_used_address_of(const exprt &expr, const irep_idt &identifier);
47  bool is_used(const exprt &expr, const irep_idt &identifier);
48 };
49 
51  const namespacet &ns,
52  const value_sett &value_set,
53  const symex_target_equationt &equation,
54  const goto_symex_statet &s,
55  exprt &dest)
56 {
57  for(symex_target_equationt::SSA_stepst::const_iterator
58  it=equation.SSA_steps.begin();
59  it!=equation.SSA_steps.end();
60  it++)
61  {
62  postconditiont postcondition(ns, value_set, *it, s);
63  postcondition.compute(dest);
64  if(dest.is_false())
65  return;
66  }
67 }
68 
70  const exprt &expr,
71  const irep_idt &identifier)
72 {
73  if(expr.id()==ID_symbol)
74  {
75  // leave alone
76  }
77  else if(expr.id()==ID_index)
78  {
79  return is_used_address_of(to_index_expr(expr).array(), identifier) ||
80  is_used(to_index_expr(expr).index(), identifier);
81  }
82  else if(expr.id()==ID_member)
83  {
84  return is_used_address_of(to_member_expr(expr).compound(), identifier);
85  }
86  else if(expr.id()==ID_dereference)
87  {
88  return is_used(to_dereference_expr(expr).pointer(), identifier);
89  }
90 
91  return false;
92 }
93 
95 {
96  // weaken due to assignment
97  weaken(dest);
98 
99  // strengthen due to assignment
100  strengthen(dest);
101 }
102 
104 {
105  if(dest.id()==ID_and &&
106  dest.type()==bool_typet()) // this distributes over "and"
107  {
108  Forall_operands(it, dest)
109  weaken(*it);
110 
111  return;
112  }
113 
114  // we are lazy:
115  // if lhs is mentioned in dest, we use "true".
116 
117  const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
118 
119  if(is_used(dest, lhs_identifier))
120  dest=true_exprt();
121 
122  // otherwise, no weakening needed
123 }
124 
126 {
127  const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
128 
129  if(!is_used(SSA_step.ssa_rhs, lhs_identifier))
130  {
131  // we don't do arrays or structs
132  if(SSA_step.ssa_lhs.type().id()==ID_array ||
133  SSA_step.ssa_lhs.type().id()==ID_struct)
134  return;
135 
137  s.get_original_name(equality);
138 
139  if(dest.is_true())
140  dest.swap(equality);
141  else
142  dest=and_exprt(dest, equality);
143  }
144 }
145 
147  const exprt &expr,
148  const irep_idt &identifier)
149 {
150  if(expr.id()==ID_address_of)
151  {
152  return is_used_address_of(to_address_of_expr(expr).object(), identifier);
153  }
154  else if(expr.id()==ID_symbol &&
155  expr.get_bool(ID_C_SSA_symbol))
156  {
157  return to_ssa_expr(expr).get_object_name()==identifier;
158  }
159  else if(expr.id()==ID_symbol)
160  {
161  return to_symbol_expr(expr).get_identifier() == identifier;
162  }
163  else if(expr.id()==ID_dereference)
164  {
165  // aliasing may happen here
166  value_setst::valuest expr_set;
167  value_set.get_value_set(to_dereference_expr(expr).pointer(), expr_set, ns);
168  std::unordered_set<irep_idt> symbols;
169 
170  for(value_setst::valuest::const_iterator
171  it=expr_set.begin();
172  it!=expr_set.end();
173  it++)
174  {
175  exprt tmp(*it);
176  s.get_original_name(tmp);
177  find_symbols(tmp, symbols);
178  }
179 
180  return symbols.find(identifier)!=symbols.end();
181  }
182  else
183  forall_operands(it, expr)
184  if(is_used(*it, identifier))
185  return true;
186 
187  return false;
188 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symex_target_equationt::SSA_stept::ssa_rhs
exprt ssa_rhs
Definition: symex_target_equation.h:291
postcondition.h
postconditiont::ns
const namespacet & ns
Definition: postcondition.cpp:35
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:26
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
goto_symex_statet
Definition: goto_symex_state.h:34
goto_symex_statet::get_original_name
void get_original_name(exprt &expr) const
Definition: goto_symex_state.cpp:714
postconditiont::weaken
void weaken(exprt &dest)
Definition: postcondition.cpp:103
symex_target_equationt::SSA_stept
Single SSA step in the equation.
Definition: symex_target_equation.h:243
and_exprt
Boolean AND.
Definition: std_expr.h:2409
value_sett
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:41
exprt
Base class for all expressions.
Definition: expr.h:54
postcondition
void postcondition(const namespacet &ns, const value_sett &value_set, const symex_target_equationt &equation, const goto_symex_statet &s, exprt &dest)
Definition: postcondition.cpp:50
ssa_exprt::get_object_name
irep_idt get_object_name() const
Definition: ssa_expr.h:46
value_sett::get_value_set
void get_value_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
Definition: value_set.cpp:320
bool_typet
The Boolean type.
Definition: std_types.h:28
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
postconditiont::strengthen
void strengthen(exprt &dest)
Definition: postcondition.cpp:125
equal_exprt
Equality.
Definition: std_expr.h:1484
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
find_symbols
void find_symbols(const exprt &src, find_symbols_sett &dest)
Definition: find_symbols.cpp:16
find_symbols.h
value_setst::valuest
std::list< exprt > valuest
Definition: value_sets.h:28
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:160
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
postconditiont::s
const goto_symex_statet & s
Definition: postcondition.cpp:38
irept::swap
void swap(irept &irep)
Definition: irep.h:303
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
postconditiont::compute
void compute(exprt &dest)
Definition: postcondition.cpp:94
irept::id
const irep_idt & id() const
Definition: irep.h:259
postconditiont::is_used
bool is_used(const exprt &expr, const irep_idt &identifier)
Definition: postcondition.cpp:146
postconditiont
Definition: postcondition.cpp:19
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:35
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3397
goto_symex_state.h
postconditiont::value_set
const value_sett & value_set
Definition: postcondition.cpp:36
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:369
postconditiont::SSA_step
const symex_target_equationt::SSA_stept & SSA_step
Definition: postcondition.cpp:37
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
postconditiont::is_used_address_of
bool is_used_address_of(const exprt &expr, const irep_idt &identifier)
Definition: postcondition.cpp:69
postconditiont::postconditiont
postconditiont(const namespacet &_ns, const value_sett &_value_set, const symex_target_equationt::SSA_stept &_SSA_step, const goto_symex_statet &_s)
Definition: postcondition.cpp:22
symex_target_equationt::SSA_stept::ssa_lhs
ssa_exprt ssa_lhs
Definition: symex_target_equation.h:289
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
std_expr.h