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  exprt what_address=address_of_exprt(what);
142  exprt dest_address=address_of_exprt(dest);
143 
144  equal_exprt alias_cond=equal_exprt(what_address, dest_address);
145 
146  if_exprt if_expr;
147 
148  if_expr.cond()=alias_cond;
149  if_expr.type()=dest.type();
150  if_expr.true_case()=by;
151  if_expr.false_case()=dest;
152 
153  dest=if_expr;
154  return;
155  }
156 
158  // nothing to do
159  break;
160  }
161  }
162 }
163 
165 {
166  if(lhs.id()==ID_member) // turn s.x:=e into s:=(s with .x=e)
167  {
168  const member_exprt member_expr=to_member_expr(lhs);
169  irep_idt component_name=member_expr.get_component_name();
170  exprt new_lhs=member_expr.struct_op();
171 
172  with_exprt new_rhs;
173  new_rhs.type()=new_lhs.type();
174  new_rhs.old()=new_lhs;
175  new_rhs.where().id(ID_member_name);
176  new_rhs.where().set(ID_component_name, component_name);
177  new_rhs.new_value()=rhs;
178 
179  lhs=new_lhs;
180  rhs=new_rhs;
181 
182  rewrite_assignment(lhs, rhs); // rec. call
183  }
184  else if(lhs.id()==ID_index) // turn s[i]:=e into s:=(s with [i]=e)
185  {
186  const index_exprt index_expr=to_index_expr(lhs);
187  exprt new_lhs=index_expr.array();
188 
189  with_exprt new_rhs;
190  new_rhs.type()=new_lhs.type();
191  new_rhs.old()=new_lhs;
192  new_rhs.where()=index_expr.index();
193  new_rhs.new_value()=rhs;
194 
195  lhs=new_lhs;
196  rhs=new_rhs;
197 
198  rewrite_assignment(lhs, rhs); // rec. call
199  }
200 }
201 
203  const code_assignt &code,
204  const exprt &post,
205  const namespacet &ns)
206 {
207  exprt pre=post;
208 
209  exprt lhs=code.lhs(),
210  rhs=code.rhs();
211 
212  // take care of non-determinism in the RHS
213  approximate_nondet(rhs);
214 
215  rewrite_assignment(lhs, rhs);
216 
217  // replace lhs by rhs in pre
218  substitute_rec(pre, lhs, rhs, ns);
219 
220  return pre;
221 }
222 
224  const code_assumet &code,
225  const exprt &post,
226  const namespacet &ns)
227 {
228  return implies_exprt(code.assumption(), post);
229 }
230 
232  const code_declt &code,
233  const exprt &post,
234  const namespacet &ns)
235 {
236  // Model decl(var) as var = nondet()
237  const exprt &var = code.symbol();
238  side_effect_expr_nondett nondet(var.type());
239  code_assignt assignment(var, nondet);
240 
241  return wp_assign(assignment, post, ns);
242 }
243 
245  const codet &code,
246  const exprt &post,
247  const namespacet &ns)
248 {
249  const irep_idt &statement=code.get_statement();
250 
251  if(statement==ID_assign)
252  return wp_assign(to_code_assign(code), post, ns);
253  else if(statement==ID_assume)
254  return wp_assume(to_code_assume(code), post, ns);
255  else if(statement==ID_skip)
256  return post;
257  else if(statement==ID_decl)
258  return wp_decl(to_code_decl(code), post, ns);
259  else if(statement==ID_assert)
260  return post;
261  else if(statement==ID_expression)
262  return post;
263  else if(statement==ID_printf)
264  return post; // ignored
265  else if(statement==ID_free)
266  return post; // ignored
267  else if(statement==ID_asm)
268  return post; // ignored
269  else if(statement==ID_fence)
270  return post; // ignored
271  else
272  throw "sorry, wp("+id2string(statement)+"...) not implemented";
273 }
const irep_idt & get_statement() const
Definition: std_code.h:37
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:218
exprt & true_case()
Definition: std_expr.h:2805
exprt wp_assume(const code_assumet &code, const exprt &post, const namespacet &ns)
Definition: wp.cpp:223
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:244
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
exprt & op0()
Definition: expr.h:84
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:298
exprt & symbol()
Definition: std_code.h:205
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
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:120
void approximate_nondet(exprt &dest)
approximate the non-deterministic choice in a way cheaper than by (proper) quantification ...
Definition: wp.cpp:53
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt & cond()
Definition: std_expr.h:2795
exprt & old()
Definition: std_expr.h:2878
exprt & new_value()
Definition: std_expr.h:2898
typet & type()
Definition: expr.h:60
exprt wp_decl(const code_declt &code, const exprt &post, const namespacet &ns)
Definition: wp.cpp:231
boolean implication
Definition: std_expr.h:1926
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1023
Extract member of struct or union.
Definition: std_expr.h:3214
equality
Definition: std_expr.h:1082
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
const irep_idt & id() const
Definition: irep.h:189
exprt wp_assign(const code_assignt &code, const exprt &post, const namespacet &ns)
Definition: wp.cpp:202
exprt & lhs()
Definition: std_code.h:157
A declaration of a local variable.
Definition: std_code.h:192
exprt & rhs()
Definition: std_code.h:162
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Weakest Preconditions.
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1037
#define forall_operands(it, expr)
Definition: expr.h:17
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
Operator to return the address of an object.
Definition: std_expr.h:2593
exprt & false_case()
Definition: std_expr.h:2815
An assumption.
Definition: std_code.h:274
void rewrite_assignment(exprt &lhs, exprt &rhs)
Definition: wp.cpp:164
exprt & index()
Definition: std_expr.h:1208
Base class for all expressions.
Definition: expr.h:46
const exprt & struct_op() const
Definition: std_expr.h:3270
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
const exprt & assumption() const
Definition: std_code.h:287
Operator to update elements in structs and arrays.
Definition: std_expr.h:2861
irep_idt get_component_name() const
Definition: std_expr.h:3249
#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:19
exprt & where()
Definition: std_expr.h:2888
Base Type Computation.
An expression containing a side effect.
Definition: std_code.h:997
operandst & operands()
Definition: expr.h:70
exprt & array()
Definition: std_expr.h:1198
Assignment.
Definition: std_code.h:144
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
const irep_idt & get_statement() const
Definition: std_code.h:1012
array index operator
Definition: std_expr.h:1170