cprover
Loading...
Searching...
No Matches
postcondition.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: 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"
23
25{
26public:
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
36protected:
37 const namespacet &ns;
41
42public:
43 void compute(exprt &dest);
44
45protected:
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 =
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.
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
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
Definition ssa_expr.cpp:144
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.
#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 address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
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.
bool is_ssa_expr(const exprt &expr)
Definition ssa_expr.h:125
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition ssa_expr.h:145
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
Generate Equation using Symbolic Execution.
Value Set.