cprover
wp.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Weakest Preconditions
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "wp.h"
13 
14 // #include <langapi/language_util.h>
15 
16 #include <util/std_expr.h>
17 #include <util/std_code.h>
18 #include <util/base_type.h>
19 
20 bool has_nondet(const exprt &dest)
21 {
22  forall_operands(it, dest)
23  if(has_nondet(*it))
24  return true;
25 
26  if(dest.id()==ID_side_effect)
27  {
28  const side_effect_exprt &side_effect_expr=to_side_effect_expr(dest);
29  const irep_idt &statement=side_effect_expr.get_statement();
30 
31  if(statement==ID_nondet)
32  return true;
33  }
34 
35  return false;
36 }
37 
38 void approximate_nondet_rec(exprt &dest, unsigned &count)
39 {
40  if(dest.id()==ID_side_effect &&
41  to_side_effect_expr(dest).get_statement()==ID_nondet)
42  {
43  count++;
44  dest.set(ID_identifier, "wp::nondet::"+std::to_string(count));
45  dest.id(ID_nondet_symbol);
46  return;
47  }
48 
49  Forall_operands(it, dest)
50  approximate_nondet_rec(*it, count);
51 }
52 
54 {
55  static unsigned count=0; // not proper, should be quantified
56  approximate_nondet_rec(dest, count);
57 }
58 
60 enum class aliasingt { A_MAY, A_MUST, A_MUSTNOT };
61 
63  const exprt &e1, const exprt &e2,
64  const namespacet &ns)
65 {
66  // deal with some dereferencing
67  if(e1.id()==ID_dereference &&
68  e1.operands().size()==1 &&
69  e1.op0().id()==ID_address_of &&
70  e1.op0().operands().size()==1)
71  return aliasing(e1.op0().op0(), e2, ns);
72 
73  if(e2.id()==ID_dereference &&
74  e2.operands().size()==1 &&
75  e2.op0().id()==ID_address_of &&
76  e2.op0().operands().size()==1)
77  return aliasing(e1, e2.op0().op0(), ns);
78 
79  // fairly radical. Ignores struct prefixes and the like.
80  if(!base_type_eq(e1.type(), e2.type(), ns))
81  return aliasingt::A_MUSTNOT;
82 
83  // syntactically the same?
84  if(e1==e2)
85  return aliasingt::A_MUST;
86 
87  // the trivial case first
88  if(e1.id()==ID_symbol && e2.id()==ID_symbol)
89  {
92  return aliasingt::A_MUST;
93  else
94  return aliasingt::A_MUSTNOT;
95  }
96 
97  // an array or struct will never alias with a variable,
98  // nor will a struct alias with an array
99 
100  if(e1.id()==ID_index || e1.id()==ID_struct)
101  if(e2.id()!=ID_dereference && e1.id()!=e2.id())
102  return aliasingt::A_MUSTNOT;
103 
104  if(e2.id()==ID_index || e2.id()==ID_struct)
105  if(e2.id()!=ID_dereference && e1.id()!=e2.id())
106  return aliasingt::A_MUSTNOT;
107 
108  // we give up, and say it may
109  // (could do much more here)
110 
111  return aliasingt::A_MAY;
112 }
113 
116  exprt &dest,
117  const exprt &what,
118  const exprt &by,
119  const namespacet &ns)
120 {
121  if(dest.id()!=ID_address_of)
122  Forall_operands(it, dest)
123  substitute_rec(*it, what, by, ns);
124 
125  // possibly substitute?
126  if(dest.id()==ID_member ||
127  dest.id()==ID_index ||
128  dest.id()==ID_dereference ||
129  dest.id()==ID_symbol)
130  {
131  // could these be possible the same?
132  switch(aliasing(dest, what, ns))
133  {
134  case aliasingt::A_MUST:
135  dest=by; // they are always the same
136  break;
137 
138  case aliasingt::A_MAY:
139  {
140  // consider possible aliasing between 'what' and 'dest'
141  const address_of_exprt what_address(what);
142  const address_of_exprt dest_address(dest);
143 
144  equal_exprt alias_cond=equal_exprt(what_address, dest_address);
145 
146  const if_exprt if_expr(alias_cond, by, dest, dest.type());
147 
148  dest=if_expr;
149  return;
150  }
151 
153  // nothing to do
154  break;
155  }
156  }
157 }
158 
160 {
161  if(lhs.id()==ID_member) // turn s.x:=e into s:=(s with .x=e)
162  {
163  const member_exprt member_expr=to_member_expr(lhs);
164  irep_idt component_name=member_expr.get_component_name();
165  exprt new_lhs=member_expr.struct_op();
166 
167  with_exprt new_rhs;
168  new_rhs.type()=new_lhs.type();
169  new_rhs.old()=new_lhs;
170  new_rhs.where().id(ID_member_name);
171  new_rhs.where().set(ID_component_name, component_name);
172  new_rhs.new_value()=rhs;
173 
174  lhs=new_lhs;
175  rhs=new_rhs;
176 
177  rewrite_assignment(lhs, rhs); // rec. call
178  }
179  else if(lhs.id()==ID_index) // turn s[i]:=e into s:=(s with [i]=e)
180  {
181  const index_exprt index_expr=to_index_expr(lhs);
182  exprt new_lhs=index_expr.array();
183 
184  with_exprt new_rhs;
185  new_rhs.type()=new_lhs.type();
186  new_rhs.old()=new_lhs;
187  new_rhs.where()=index_expr.index();
188  new_rhs.new_value()=rhs;
189 
190  lhs=new_lhs;
191  rhs=new_rhs;
192 
193  rewrite_assignment(lhs, rhs); // rec. call
194  }
195 }
196 
198  const code_assignt &code,
199  const exprt &post,
200  const namespacet &ns)
201 {
202  exprt pre=post;
203 
204  exprt lhs=code.lhs(),
205  rhs=code.rhs();
206 
207  // take care of non-determinism in the RHS
208  approximate_nondet(rhs);
209 
210  rewrite_assignment(lhs, rhs);
211 
212  // replace lhs by rhs in pre
213  substitute_rec(pre, lhs, rhs, ns);
214 
215  return pre;
216 }
217 
219  const code_assumet &code,
220  const exprt &post,
221  const namespacet &)
222 {
223  return implies_exprt(code.assumption(), post);
224 }
225 
227  const code_declt &code,
228  const exprt &post,
229  const namespacet &ns)
230 {
231  // Model decl(var) as var = nondet()
232  const exprt &var = code.symbol();
234  code_assignt assignment(var, nondet);
235 
236  return wp_assign(assignment, post, ns);
237 }
238 
240  const codet &code,
241  const exprt &post,
242  const namespacet &ns)
243 {
244  const irep_idt &statement=code.get_statement();
245 
246  if(statement==ID_assign)
247  return wp_assign(to_code_assign(code), post, ns);
248  else if(statement==ID_assume)
249  return wp_assume(to_code_assume(code), post, ns);
250  else if(statement==ID_skip)
251  return post;
252  else if(statement==ID_decl)
253  return wp_decl(to_code_decl(code), post, ns);
254  else if(statement==ID_assert)
255  return post;
256  else if(statement==ID_expression)
257  return post;
258  else if(statement==ID_printf)
259  return post; // ignored
260  else if(statement==ID_free)
261  return post; // ignored
262  else if(statement==ID_asm)
263  return post; // ignored
264  else if(statement==ID_fence)
265  return post; // ignored
266  else
267  throw "sorry, wp("+id2string(statement)+"...) not implemented";
268 }
const irep_idt & get_statement() const
Definition: std_code.h:40
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:291
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:239
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
exprt & op0()
Definition: expr.h:72
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:390
exprt & symbol()
Definition: std_code.h:268
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:326
bool has_nondet(const exprt &dest)
Definition: wp.cpp:20
void approximate_nondet_rec(exprt &dest, unsigned &count)
Definition: wp.cpp:38
const irep_idt & get_identifier() const
Definition: std_expr.h:128
void approximate_nondet(exprt &dest)
approximate the non-deterministic choice in a way cheaper than by (proper) quantification ...
Definition: wp.cpp:53
The trinary if-then-else operator.
Definition: std_expr.h:3359
exprt & old()
Definition: std_expr.h:3476
exprt & new_value()
Definition: std_expr.h:3496
typet & type()
Definition: expr.h:56
exprt wp_decl(const code_declt &code, const exprt &post, const namespacet &ns)
Definition: wp.cpp:226
boolean implication
Definition: std_expr.h:2339
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1326
Extract member of struct or union.
Definition: std_expr.h:3869
equality
Definition: std_expr.h:1354
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:240
const irep_idt & id() const
Definition: irep.h:259
exprt wp_assign(const code_assignt &code, const exprt &post, const namespacet &ns)
Definition: wp.cpp:197
exprt & lhs()
Definition: std_code.h:209
A declaration of a local variable.
Definition: std_code.h:254
exprt & rhs()
Definition: std_code.h:214
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Weakest Preconditions.
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3953
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1340
#define forall_operands(it, expr)
Definition: expr.h:17
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
exprt wp_assume(const code_assumet &code, const exprt &post, const namespacet &)
Definition: wp.cpp:218
aliasingt aliasing(const exprt &e1, const exprt &e2, const namespacet &ns)
Definition: wp.cpp:62
void substitute_rec(exprt &dest, const exprt &what, const exprt &by, const namespacet &ns)
replace &#39;what&#39; by &#39;by&#39; in &#39;dest&#39;, considering possible aliasing
Definition: wp.cpp:115
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Operator to return the address of an object.
Definition: std_expr.h:3168
An assumption, which must hold in subsequent code.
Definition: std_code.h:357
void rewrite_assignment(exprt &lhs, exprt &rhs)
Definition: wp.cpp:159
exprt & index()
Definition: std_expr.h:1496
Base class for all expressions.
Definition: expr.h:42
const exprt & struct_op() const
Definition: std_expr.h:3909
const exprt & assumption() const
Definition: std_code.h:371
Operator to update elements in structs and arrays.
Definition: std_expr.h:3459
std::string to_string(const string_constraintt &expr)
Used for debug printing.
irep_idt get_component_name() const
Definition: std_expr.h:3893
#define Forall_operands(it, expr)
Definition: expr.h:23
aliasingt
consider possible aliasing
Definition: wp.cpp:60
A statement in a programming language.
Definition: std_code.h:21
exprt & where()
Definition: std_expr.h:3486
Base Type Computation.
An expression containing a side effect.
Definition: std_code.h:1271
operandst & operands()
Definition: expr.h:66
exprt & array()
Definition: std_expr.h:1486
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
Assignment.
Definition: std_code.h:196
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
const irep_idt & get_statement() const
Definition: std_code.h:1292
array index operator
Definition: std_expr.h:1462