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  assert(expr.operands().size()==2);
80 
81  return
82  is_used_address_of(expr.op0(), identifier) ||
83  is_used(expr.op1(), identifier);
84  }
85  else if(expr.id()==ID_member)
86  {
87  assert(expr.operands().size()==1);
88  return is_used_address_of(expr.op0(), identifier);
89  }
90  else if(expr.id()==ID_dereference)
91  {
92  assert(expr.operands().size()==1);
93  return is_used(expr.op0(), identifier);
94  }
95 
96  return false;
97 }
98 
100 {
101  // weaken due to assignment
102  weaken(dest);
103 
104  // strengthen due to assignment
105  strengthen(dest);
106 }
107 
109 {
110  if(dest.id()==ID_and &&
111  dest.type()==bool_typet()) // this distributes over "and"
112  {
113  Forall_operands(it, dest)
114  weaken(*it);
115 
116  return;
117  }
118 
119  // we are lazy:
120  // if lhs is mentioned in dest, we use "true".
121 
122  const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
123 
124  if(is_used(dest, lhs_identifier))
125  dest=true_exprt();
126 
127  // otherwise, no weakening needed
128 }
129 
131 {
132  const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
133 
134  if(!is_used(SSA_step.ssa_rhs, lhs_identifier))
135  {
136  // we don't do arrays or structs
137  if(SSA_step.ssa_lhs.type().id()==ID_array ||
138  SSA_step.ssa_lhs.type().id()==ID_struct)
139  return;
140 
142  s.get_original_name(equality);
143 
144  if(dest.is_true())
145  dest.swap(equality);
146  else
147  dest=and_exprt(dest, equality);
148  }
149 }
150 
152  const exprt &expr,
153  const irep_idt &identifier)
154 {
155  if(expr.id()==ID_address_of)
156  {
157  // only do index!
158  assert(expr.operands().size()==1);
159  return is_used_address_of(expr.op0(), identifier);
160  }
161  else if(expr.id()==ID_symbol &&
162  expr.get_bool(ID_C_SSA_symbol))
163  {
164  return to_ssa_expr(expr).get_object_name()==identifier;
165  }
166  else if(expr.id()==ID_symbol)
167  {
168  return expr.get(ID_identifier)==identifier;
169  }
170  else if(expr.id()==ID_dereference)
171  {
172  assert(expr.operands().size()==1);
173 
174  // aliasing may happen here
175 
176  value_setst::valuest expr_set;
177  value_set.get_value_set(expr.op0(), expr_set, ns);
178  std::unordered_set<irep_idt, irep_id_hash> symbols;
179 
180  for(value_setst::valuest::const_iterator
181  it=expr_set.begin();
182  it!=expr_set.end();
183  it++)
184  {
185  exprt tmp(*it);
186  s.get_original_name(tmp);
187  find_symbols(tmp, symbols);
188  }
189 
190  return symbols.find(identifier)!=symbols.end();
191  }
192  else
193  forall_operands(it, expr)
194  if(is_used(*it, identifier))
195  return true;
196 
197  return false;
198 }
exprt & op0()
Definition: expr.h:84
bool is_false() const
Definition: expr.cpp:140
void get_value_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Definition: value_set.cpp:314
Symbolic Execution.
bool is_true() const
Definition: expr.cpp:133
typet & type()
Definition: expr.h:60
The proper Booleans.
Definition: std_types.h:33
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:240
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)
void get_original_name(exprt &expr) const
equality
Definition: std_expr.h:1082
const irep_idt & id() const
Definition: irep.h:189
The boolean constant true.
Definition: std_expr.h:3742
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:150
Generate Equation using Symbolic Execution.
const namespacet & ns
boolean AND
Definition: std_expr.h:1852
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:62
#define forall_operands(it, expr)
Definition: expr.h:17
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)
void weaken(exprt &dest)
Base class for all expressions.
Definition: expr.h:46
irep_idt get_object_name() const
Definition: ssa_expr.h:46
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
bool is_used(const exprt &expr, const irep_idt &identifier)
const goto_symex_statet & s
operandst & operands()
Definition: expr.h:70
std::list< exprt > valuest
Definition: value_sets.h:28
const symex_target_equationt::SSA_stept & SSA_step
void find_symbols(const exprt &src, find_symbols_sett &dest)