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 SSA_stept &_SSA_step,
26  const goto_symex_statet &_s)
27  : ns(_ns), value_set(_value_set), SSA_step(_SSA_step), s(_s)
28  {
29  }
30 
31 protected:
32  const namespacet &ns;
36 
37 public:
38  void compute(exprt &dest);
39 
40 protected:
41  void strengthen(exprt &dest);
42  void weaken(exprt &dest);
43  bool is_used_address_of(const exprt &expr, const irep_idt &identifier);
44  bool is_used(const exprt &expr, const irep_idt &identifier);
45 };
46 
48  const namespacet &ns,
49  const value_sett &value_set,
50  const symex_target_equationt &equation,
51  const goto_symex_statet &s,
52  exprt &dest)
53 {
54  for(symex_target_equationt::SSA_stepst::const_iterator
55  it=equation.SSA_steps.begin();
56  it!=equation.SSA_steps.end();
57  it++)
58  {
59  postconditiont postcondition(ns, value_set, *it, s);
60  postcondition.compute(dest);
61  if(dest.is_false())
62  return;
63  }
64 }
65 
67  const exprt &expr,
68  const irep_idt &identifier)
69 {
70  if(expr.id()==ID_symbol)
71  {
72  // leave alone
73  }
74  else if(expr.id()==ID_index)
75  {
76  return is_used_address_of(to_index_expr(expr).array(), identifier) ||
77  is_used(to_index_expr(expr).index(), identifier);
78  }
79  else if(expr.id()==ID_member)
80  {
81  return is_used_address_of(to_member_expr(expr).compound(), identifier);
82  }
83  else if(expr.id()==ID_dereference)
84  {
85  return is_used(to_dereference_expr(expr).pointer(), identifier);
86  }
87 
88  return false;
89 }
90 
92 {
93  // weaken due to assignment
94  weaken(dest);
95 
96  // strengthen due to assignment
97  strengthen(dest);
98 }
99 
101 {
102  if(dest.id()==ID_and &&
103  dest.type()==bool_typet()) // this distributes over "and"
104  {
105  Forall_operands(it, dest)
106  weaken(*it);
107 
108  return;
109  }
110 
111  // we are lazy:
112  // if lhs is mentioned in dest, we use "true".
113 
114  const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
115 
116  if(is_used(dest, lhs_identifier))
117  dest=true_exprt();
118 
119  // otherwise, no weakening needed
120 }
121 
123 {
124  const irep_idt &lhs_identifier=SSA_step.ssa_lhs.get_object_name();
125 
126  if(!is_used(SSA_step.ssa_rhs, lhs_identifier))
127  {
128  // we don't do arrays or structs
129  if(SSA_step.ssa_lhs.type().id()==ID_array ||
130  SSA_step.ssa_lhs.type().id()==ID_struct)
131  return;
132 
133  exprt equality =
135 
136  if(dest.is_true())
137  dest.swap(equality);
138  else
139  dest=and_exprt(dest, equality);
140  }
141 }
142 
144  const exprt &expr,
145  const irep_idt &identifier)
146 {
147  if(expr.id()==ID_address_of)
148  {
149  return is_used_address_of(to_address_of_expr(expr).object(), identifier);
150  }
151  else if(is_ssa_expr(expr))
152  {
153  return to_ssa_expr(expr).get_object_name()==identifier;
154  }
155  else if(expr.id()==ID_symbol)
156  {
157  return to_symbol_expr(expr).get_identifier() == identifier;
158  }
159  else if(expr.id()==ID_dereference)
160  {
161  // aliasing may happen here
162  const std::vector<exprt> expr_set =
163  value_set.get_value_set(to_dereference_expr(expr).pointer(), ns);
164  const auto original_names = make_range(expr_set).map(
165  [](const exprt &e) { return get_original_name(e); });
166  const std::unordered_set<irep_idt> symbols =
167  find_symbols_or_nexts(original_names.begin(), original_names.end());
168  return symbols.find(identifier)!=symbols.end();
169  }
170  else
171  forall_operands(it, expr)
172  if(is_used(*it, identifier))
173  return true;
174 
175  return false;
176 }
Single SSA step in the equation.
Definition: ssa_step.h:45
exprt ssa_rhs
Definition: ssa_step.h:143
ssa_exprt ssa_lhs
Definition: ssa_step.h:141
Boolean AND.
Definition: std_expr.h:1835
The Boolean type.
Definition: std_types.h:37
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:1140
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:47
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
Central data structure: state.
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:452
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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:110
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:2717
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:45
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:352
#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.
Symbolic Execution.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:312
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
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.
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
exprt get_original_name(exprt expr)
Undo all levels of renaming.
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:190
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297