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/pointer_expr.h>
16 #include <util/range.h>
17 #include <util/std_expr.h>
18 
20 
21 #include "renaming_level.h"
22 #include "symex_target_equation.h"
23 
25 {
26 public:
28  const namespacet &_ns,
29  const value_sett &_value_set,
30  const SSA_stept &_SSA_step,
31  const goto_symex_statet &_s)
32  : ns(_ns), value_set(_value_set), SSA_step(_SSA_step), s(_s)
33  {
34  }
35 
36 protected:
37  const namespacet &ns;
41 
42 public:
43  void compute(exprt &dest);
44 
45 protected:
46  void strengthen(exprt &dest);
47  void weaken(exprt &dest);
48  bool is_used_address_of(const exprt &expr, const irep_idt &identifier);
49  bool is_used(const exprt &expr, const irep_idt &identifier);
50 };
51 
53  const namespacet &ns,
54  const value_sett &value_set,
55  const symex_target_equationt &equation,
56  const goto_symex_statet &s,
57  exprt &dest)
58 {
59  for(symex_target_equationt::SSA_stepst::const_iterator
60  it=equation.SSA_steps.begin();
61  it!=equation.SSA_steps.end();
62  it++)
63  {
64  postconditiont postcondition(ns, value_set, *it, s);
65  postcondition.compute(dest);
66  if(dest.is_false())
67  return;
68  }
69 }
70 
72  const exprt &expr,
73  const irep_idt &identifier)
74 {
75  if(expr.id()==ID_symbol)
76  {
77  // leave alone
78  }
79  else if(expr.id()==ID_index)
80  {
81  return is_used_address_of(to_index_expr(expr).array(), identifier) ||
82  is_used(to_index_expr(expr).index(), identifier);
83  }
84  else if(expr.id()==ID_member)
85  {
86  return is_used_address_of(to_member_expr(expr).compound(), identifier);
87  }
88  else if(expr.id()==ID_dereference)
89  {
90  return is_used(to_dereference_expr(expr).pointer(), identifier);
91  }
92 
93  return false;
94 }
95 
97 {
98  // weaken due to assignment
99  weaken(dest);
100 
101  // strengthen due to assignment
102  strengthen(dest);
103 }
104 
106 {
107  if(dest.id()==ID_and &&
108  dest.type()==bool_typet()) // this distributes over "and"
109  {
110  Forall_operands(it, dest)
111  weaken(*it);
112 
113  return;
114  }
115 
116  // we are lazy:
117  // if lhs is mentioned in dest, we use "true".
118 
119  const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
120 
121  if(is_used(dest, lhs_identifier))
122  dest=true_exprt();
123 
124  // otherwise, no weakening needed
125 }
126 
128 {
129  const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
130 
131  if(!is_used(SSA_step.ssa_rhs, lhs_identifier))
132  {
133  // we don't do arrays or structs
134  if(SSA_step.ssa_lhs.type().id()==ID_array ||
135  SSA_step.ssa_lhs.type().id()==ID_struct)
136  return;
137 
138  exprt equality =
140 
141  if(dest.is_true())
142  dest.swap(equality);
143  else
144  dest=and_exprt(dest, equality);
145  }
146 }
147 
149  const exprt &expr,
150  const irep_idt &identifier)
151 {
152  if(expr.id()==ID_address_of)
153  {
154  return is_used_address_of(to_address_of_expr(expr).object(), identifier);
155  }
156  else if(is_ssa_expr(expr))
157  {
158  return to_ssa_expr(expr).get_object_name()==identifier;
159  }
160  else if(expr.id()==ID_symbol)
161  {
162  return to_symbol_expr(expr).get_identifier() == identifier;
163  }
164  else if(expr.id()==ID_dereference)
165  {
166  // aliasing may happen here
167  const std::vector<exprt> expr_set =
168  value_set.get_value_set(to_dereference_expr(expr).pointer(), ns);
169  const auto original_names = make_range(expr_set).map(
170  [](const exprt &e) { return get_original_name(e); });
171  const std::unordered_set<irep_idt> symbols =
172  find_symbols_or_nexts(original_names.begin(), original_names.end());
173  return symbols.find(identifier)!=symbols.end();
174  }
175  else
176  forall_operands(it, expr)
177  if(is_used(*it, identifier))
178  return true;
179 
180  return false;
181 }
Single SSA step in the equation.
Definition: ssa_step.h:47
exprt ssa_rhs
Definition: ssa_step.h:145
ssa_exprt ssa_lhs
Definition: ssa_step.h:143
Boolean AND.
Definition: std_expr.h:1974
The Boolean type.
Definition: std_types.h:36
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
typet & type()
Return the type of the expression.
Definition: expr.h:82
Central data structure: state.
const irep_idt & id() const
Definition: irep.h:396
void swap(irept &irep)
Definition: irep.h:442
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
const SSA_stept & SSA_step
const namespacet & ns
bool is_used(const exprt &expr, const irep_idt &identifier)
void strengthen(exprt &dest)
const value_sett & value_set
const goto_symex_statet & s
void weaken(exprt &dest)
bool is_used_address_of(const exprt &expr, const irep_idt &identifier)
postconditiont(const namespacet &_ns, const value_sett &_value_set, const SSA_stept &_SSA_step, const goto_symex_statet &_s)
void compute(exprt &dest)
irep_idt get_object_name() const
const irep_idt & get_identifier() const
Definition: std_expr.h:109
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
The Boolean constant true.
Definition: std_expr.h:2856
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:43
std::vector< exprt > get_value_set(exprt expr, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
Definition: value_set.cpp:354
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
Add to the set dest the sub-expressions of src with id ID_symbol or ID_next_symbol.
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:704
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
void postcondition(const namespacet &ns, const value_sett &value_set, const symex_target_equationt &equation, const goto_symex_statet &s, exprt &dest)
Generate Equation using Symbolic Execution.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
exprt get_original_name(exprt expr)
Undo all levels of renaming.
Renaming levels.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
Generate Equation using Symbolic Execution.
Value Set.