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(expr.id()==ID_symbol &&
152  expr.get_bool(ID_C_SSA_symbol))
153  {
154  return to_ssa_expr(expr).get_object_name()==identifier;
155  }
156  else if(expr.id()==ID_symbol)
157  {
158  return to_symbol_expr(expr).get_identifier() == identifier;
159  }
160  else if(expr.id()==ID_dereference)
161  {
162  // aliasing may happen here
163  const std::vector<exprt> expr_set =
164  value_set.get_value_set(to_dereference_expr(expr).pointer(), ns);
165  const auto original_names = make_range(expr_set).map(
166  [](const exprt &e) { return get_original_name(e); });
167  const std::unordered_set<irep_idt> symbols =
168  find_symbols_or_nexts(original_names.begin(), original_names.end());
169  return symbols.find(identifier)!=symbols.end();
170  }
171  else
172  forall_operands(it, expr)
173  if(is_used(*it, identifier))
174  return true;
175 
176  return false;
177 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
value_sett::get_value_set
void get_value_set(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:359
postcondition.h
Generate Equation using Symbolic Execution.
postconditiont::ns
const namespacet & ns
Definition: postcondition.cpp:32
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
SSA_stept
Single SSA step in the equation.
Definition: ssa_step.h:45
find_symbols_or_nexts
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.
Definition: find_symbols.cpp:18
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:46
postconditiont::weaken
void weaken(exprt &dest)
Definition: postcondition.cpp:100
and_exprt
Boolean AND.
Definition: std_expr.h:2137
value_sett
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:45
exprt
Base class for all expressions.
Definition: expr.h:53
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:47
ssa_exprt::get_object_name
irep_idt get_object_name() const
bool_typet
The Boolean type.
Definition: std_types.h:37
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
postconditiont::strengthen
void strengthen(exprt &dest)
Definition: postcondition.cpp:122
equal_exprt
Equality.
Definition: std_expr.h:1190
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
find_symbols.h
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:148
SSA_stept::ssa_lhs
ssa_exprt ssa_lhs
Definition: ssa_step.h:141
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:2823
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
postconditiont::s
const goto_symex_statet & s
Definition: postcondition.cpp:35
postconditiont::postconditiont
postconditiont(const namespacet &_ns, const value_sett &_value_set, const SSA_stept &_SSA_step, const goto_symex_statet &_s)
Definition: postcondition.cpp:22
irept::swap
void swap(irept &irep)
Definition: irep.h:463
get_original_name
exprt get_original_name(exprt expr)
Undo all levels of renaming.
Definition: renaming_level.cpp:169
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
postconditiont::compute
void compute(exprt &dest)
Definition: postcondition.cpp:91
irept::id
const irep_idt & id() const
Definition: irep.h:418
postconditiont::is_used
bool is_used(const exprt &expr, const irep_idt &identifier)
Definition: postcondition.cpp:143
postconditiont
Definition: postcondition.cpp:20
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:41
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2944
goto_symex_state.h
Symbolic Execution.
postconditiont::value_set
const value_sett & value_set
Definition: postcondition.cpp:33
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:257
SSA_stept::ssa_rhs
exprt ssa_rhs
Definition: ssa_step.h:143
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
postconditiont::is_used_address_of
bool is_used_address_of(const exprt &expr, const irep_idt &identifier)
Definition: postcondition.cpp:66
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
std_expr.h
API to expression classes.
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
postconditiont::SSA_step
const SSA_stept & SSA_step
Definition: postcondition.cpp:34