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 }
const irep_idt & get_identifier() const
Definition: std_expr.h:176
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
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
Symbolic Execution.
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
typet & type()
Return the type of the expression.
Definition: expr.h:68
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
The Boolean type.
Definition: std_types.h:28
bool is_used_address_of(const exprt &expr, const irep_idt &identifier)
void compute(exprt &dest)
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
const value_sett & value_set
postconditiont(const namespacet &_ns, const value_sett &_value_set, const symex_target_equationt::SSA_stept &_SSA_step, const goto_symex_statet &_s)
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3397
void get_original_name(exprt &expr) const
Equality.
Definition: std_expr.h:1484
const irep_idt & id() const
Definition: irep.h:259
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:160
The Boolean constant true.
Definition: std_expr.h:4443
Generate Equation using Symbolic Execution.
const namespacet & ns
Boolean AND.
Definition: std_expr.h:2409
API to expression classes.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
#define forall_operands(it, expr)
Definition: expr.h:20
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:41
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
void postcondition(const namespacet &ns, const value_sett &value_set, const symex_target_equationt &equation, const goto_symex_statet &s, exprt &dest)
void strengthen(exprt &dest)
Single SSA step in the equation.
void weaken(exprt &dest)
Base class for all expressions.
Definition: expr.h:54
irep_idt get_object_name() const
Definition: ssa_expr.h:46
void swap(irept &irep)
Definition: irep.h:303
#define Forall_operands(it, expr)
Definition: expr.h:26
bool is_used(const exprt &expr, const irep_idt &identifier)
const goto_symex_statet & s
std::list< exprt > valuest
Definition: value_sets.h:28
const symex_target_equationt::SSA_stept & SSA_step
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
void find_symbols(const exprt &src, find_symbols_sett &dest)