cprover
Loading...
Searching...
No Matches
wp.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Weakest Preconditions
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "wp.h"
13
14// #include <langapi/language_util.h>
15
17
18#include <util/invariant.h>
19#include <util/pointer_expr.h>
20#include <util/std_code.h>
21
22bool has_nondet(const exprt &dest)
23{
25 if(has_nondet(*it))
26 return true;
27
28 if(dest.id()==ID_side_effect)
29 {
31 const irep_idt &statement=side_effect_expr.get_statement();
32
33 if(statement==ID_nondet)
34 return true;
35 }
36
37 return false;
38}
39
40void approximate_nondet_rec(exprt &dest, unsigned &count)
41{
42 if(dest.id()==ID_side_effect &&
43 to_side_effect_expr(dest).get_statement()==ID_nondet)
44 {
45 count++;
46 dest.set(ID_identifier, "wp::nondet::"+std::to_string(count));
48 return;
49 }
50
52 approximate_nondet_rec(*it, count);
53}
54
56{
57 static unsigned count=0; // not proper, should be quantified
59}
60
63
65 const exprt &e1, const exprt &e2,
66 const namespacet &ns)
67{
68 // deal with some dereferencing
69 if(
70 e1.id() == ID_dereference &&
71 to_dereference_expr(e1).pointer().id() == ID_address_of)
72 {
73 return aliasing(
74 to_address_of_expr(to_dereference_expr(e1).pointer()).object(), e2, ns);
75 }
76
77 if(
78 e2.id() == ID_dereference &&
79 to_dereference_expr(e2).pointer().id() == ID_address_of)
80 {
81 return aliasing(
82 e1, to_address_of_expr(to_dereference_expr(e2).pointer()).object(), ns);
83 }
84
85 // fairly radical. Ignores struct prefixes and the like.
86 if(e1.type() != e2.type())
88
89 // syntactically the same?
90 if(e1==e2)
91 return aliasingt::A_MUST;
92
93 // the trivial case first
94 if(e1.id()==ID_symbol && e2.id()==ID_symbol)
95 {
98 return aliasingt::A_MUST;
99 else
101 }
102
103 // an array or struct will never alias with a variable,
104 // nor will a struct alias with an array
105
106 if(e1.id()==ID_index || e1.id()==ID_struct)
107 if(e2.id()!=ID_dereference && e1.id()!=e2.id())
109
110 if(e2.id()==ID_index || e2.id()==ID_struct)
111 if(e2.id()!=ID_dereference && e1.id()!=e2.id())
113
114 // we give up, and say it may
115 // (could do much more here)
116
117 return aliasingt::A_MAY;
118}
119
122 exprt &dest,
123 const exprt &what,
124 const exprt &by,
125 const namespacet &ns)
126{
127 if(dest.id()!=ID_address_of)
129 substitute_rec(*it, what, by, ns);
130
131 // possibly substitute?
132 if(dest.id()==ID_member ||
133 dest.id()==ID_index ||
134 dest.id()==ID_dereference ||
135 dest.id()==ID_symbol)
136 {
137 // could these be possible the same?
138 switch(aliasing(dest, what, ns))
139 {
141 dest=by; // they are always the same
142 break;
143
144 case aliasingt::A_MAY:
145 {
146 // consider possible aliasing between 'what' and 'dest'
147 const address_of_exprt what_address(what);
149
151
152 const if_exprt if_expr(alias_cond, by, dest, dest.type());
153
155 return;
156 }
157
159 // nothing to do
160 break;
161 }
162 }
163}
164
166{
167 if(lhs.id()==ID_member) // turn s.x:=e into s:=(s with .x=e)
168 {
170 irep_idt component_name=member_expr.get_component_name();
171 exprt new_lhs=member_expr.struct_op();
172
174 new_rhs.where().set(ID_component_name, component_name);
175
176 lhs=new_lhs;
177 rhs=new_rhs;
178
179 rewrite_assignment(lhs, rhs); // rec. call
180 }
181 else if(lhs.id()==ID_index) // turn s[i]:=e into s:=(s with [i]=e)
182 {
184 exprt new_lhs=index_expr.array();
185
186 with_exprt new_rhs(new_lhs, index_expr.index(), rhs);
187
188 lhs=new_lhs;
189 rhs=new_rhs;
190
191 rewrite_assignment(lhs, rhs); // rec. call
192 }
193}
194
196 const code_assignt &code,
197 const exprt &post,
198 const namespacet &ns)
199{
200 exprt pre=post;
201
202 exprt lhs=code.lhs(),
203 rhs=code.rhs();
204
205 // take care of non-determinism in the RHS
207
208 rewrite_assignment(lhs, rhs);
209
210 // replace lhs by rhs in pre
211 substitute_rec(pre, lhs, rhs, ns);
212
213 return pre;
214}
215
217 const code_assumet &code,
218 const exprt &post,
219 const namespacet &)
220{
221 return implies_exprt(code.assumption(), post);
222}
223
225 const code_declt &code,
226 const exprt &post,
227 const namespacet &ns)
228{
229 // Model decl(var) as var = nondet()
230 const exprt &var = code.symbol();
232 code_assignt assignment(var, nondet);
233
234 return wp_assign(assignment, post, ns);
235}
236
238 const codet &code,
239 const exprt &post,
240 const namespacet &ns)
241{
242 const irep_idt &statement=code.get_statement();
243
244 if(statement==ID_assign)
245 return wp_assign(to_code_assign(code), post, ns);
246 else if(statement==ID_assume)
247 return wp_assume(to_code_assume(code), post, ns);
248 else if(statement==ID_skip)
249 return post;
250 else if(statement==ID_decl)
251 return wp_decl(to_code_decl(code), post, ns);
252 else if(statement==ID_assert)
253 return post;
254 else if(statement==ID_expression)
255 return post;
256 else if(statement==ID_printf)
257 return post; // ignored
258 else if(statement==ID_asm)
259 return post; // ignored
260 else if(statement==ID_fence)
261 return post; // ignored
263 false, "sorry, wp(", id2string(statement), "...) is not implemented");
264}
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
A codet representing an assignment in the program.
An assumption, which must hold in subsequent code.
Definition std_code.h:217
const exprt & assumption() const
Definition std_code.h:223
A codet representing the declaration of a local variable.
symbol_exprt & symbol()
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
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
typet & type()
Return the type of the expression.
Definition expr.h:82
The trinary if-then-else operator.
Definition std_expr.h:2226
Boolean implication.
Definition std_expr.h:2037
Array index operator.
Definition std_expr.h:1328
const irep_idt & id() const
Definition irep.h:396
Extract member of struct or union.
Definition std_expr.h:2667
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
An expression containing a side effect.
Definition std_code.h:1450
Operator to update elements in structs and arrays.
Definition std_expr.h:2312
#define forall_operands(it, expr)
Definition expr.h:18
#define Forall_operands(it, expr)
Definition expr.h:25
const code_assignt & to_code_assign(const codet &code)
const code_declt & to_code_decl(const codet &code)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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.
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
Definition invariant.h:437
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition std_code.h:1506
const code_assumet & to_code_assume(const codet &code)
Definition std_code.h:251
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
exprt wp_assign(const code_assignt &code, const exprt &post, const namespacet &ns)
Definition wp.cpp:195
void approximate_nondet_rec(exprt &dest, unsigned &count)
Definition wp.cpp:40
exprt wp_assume(const code_assumet &code, const exprt &post, const namespacet &)
Definition wp.cpp:216
void approximate_nondet(exprt &dest)
Approximate the non-deterministic choice in a way cheaper than by (proper) quantification.
Definition wp.cpp:55
exprt wp_decl(const code_declt &code, const exprt &post, const namespacet &ns)
Definition wp.cpp:224
exprt wp(const codet &code, const exprt &post, const namespacet &ns)
Compute the weakest precondition of the given program piece code with respect to the expression post.
Definition wp.cpp:237
void substitute_rec(exprt &dest, const exprt &what, const exprt &by, const namespacet &ns)
replace 'what' by 'by' in 'dest', considering possible aliasing
Definition wp.cpp:121
aliasingt
consider possible aliasing
Definition wp.cpp:62
aliasingt aliasing(const exprt &e1, const exprt &e2, const namespacet &ns)
Definition wp.cpp:64
bool has_nondet(const exprt &dest)
Definition wp.cpp:22
void rewrite_assignment(exprt &lhs, exprt &rhs)
Definition wp.cpp:165
Weakest Preconditions.