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/pointer_expr.h>
17 #include <util/std_code.h>
18 #include <util/std_expr.h>
19 
20 #include <util/invariant.h>
21 
22 bool has_nondet(const exprt &dest)
23 {
24  forall_operands(it, dest)
25  if(has_nondet(*it))
26  return true;
27 
28  if(dest.id()==ID_side_effect)
29  {
30  const side_effect_exprt &side_effect_expr=to_side_effect_expr(dest);
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 
40 void 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));
47  dest.id(ID_nondet_symbol);
48  return;
49  }
50 
51  Forall_operands(it, dest)
52  approximate_nondet_rec(*it, count);
53 }
54 
56 {
57  static unsigned count=0; // not proper, should be quantified
58  approximate_nondet_rec(dest, count);
59 }
60 
62 enum class aliasingt { A_MAY, A_MUST, A_MUSTNOT };
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())
87  return aliasingt::A_MUSTNOT;
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  {
96  if(to_symbol_expr(e1).get_identifier()==
97  to_symbol_expr(e2).get_identifier())
98  return aliasingt::A_MUST;
99  else
100  return aliasingt::A_MUSTNOT;
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())
108  return aliasingt::A_MUSTNOT;
109 
110  if(e2.id()==ID_index || e2.id()==ID_struct)
111  if(e2.id()!=ID_dereference && e1.id()!=e2.id())
112  return aliasingt::A_MUSTNOT;
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)
128  Forall_operands(it, dest)
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  {
140  case aliasingt::A_MUST:
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);
148  const address_of_exprt dest_address(dest);
149 
150  equal_exprt alias_cond=equal_exprt(what_address, dest_address);
151 
152  const if_exprt if_expr(alias_cond, by, dest, dest.type());
153 
154  dest=if_expr;
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  {
169  const member_exprt member_expr=to_member_expr(lhs);
170  irep_idt component_name=member_expr.get_component_name();
171  exprt new_lhs=member_expr.struct_op();
172 
173  with_exprt new_rhs(new_lhs, exprt(ID_member_name), rhs);
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  {
183  const index_exprt index_expr=to_index_expr(lhs);
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
206  approximate_nondet(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  PRECONDITION(!code.initial_value());
230  // Model decl(var) as var = nondet()
231  const exprt &var = code.symbol();
233  code_assignt assignment(var, nondet);
234 
235  return wp_assign(assignment, post, ns);
236 }
237 
239  const codet &code,
240  const exprt &post,
241  const namespacet &ns)
242 {
243  const irep_idt &statement=code.get_statement();
244 
245  if(statement==ID_assign)
246  return wp_assign(to_code_assign(code), post, ns);
247  else if(statement==ID_assume)
248  return wp_assume(to_code_assume(code), post, ns);
249  else if(statement==ID_skip)
250  return post;
251  else if(statement==ID_decl)
252  return wp_decl(to_code_decl(code), post, ns);
253  else if(statement==ID_assert)
254  return post;
255  else if(statement==ID_expression)
256  return post;
257  else if(statement==ID_printf)
258  return post; // ignored
259  else if(statement==ID_asm)
260  return post; // ignored
261  else if(statement==ID_fence)
262  return post; // ignored
264  false, "sorry, wp(", id2string(statement), "...) is not implemented");
265 }
Operator to return the address of an object.
Definition: pointer_expr.h:200
A codet representing an assignment in the program.
Definition: std_code.h:295
exprt & rhs()
Definition: std_code.h:317
exprt & lhs()
Definition: std_code.h:312
An assumption, which must hold in subsequent code.
Definition: std_code.h:567
const exprt & assumption() const
Definition: std_code.h:573
A codet representing the declaration of a local variable.
Definition: std_code.h:402
symbol_exprt & symbol()
Definition: std_code.h:408
optionalt< exprt > initial_value() const
Returns the initial value to which the declared variable is initialized, or empty in the case where n...
Definition: std_code.h:427
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
const irep_idt & get_statement() const
Definition: std_code.h:71
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:1140
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:2087
Boolean implication.
Definition: std_expr.h:1898
Array index operator.
Definition: std_expr.h:1243
exprt & array()
Definition: std_expr.h:1259
exprt & index()
Definition: std_expr.h:1269
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
const irep_idt & id() const
Definition: irep.h:407
Extract member of struct or union.
Definition: std_expr.h:2528
const exprt & struct_op() const
Definition: std_expr.h:2558
irep_idt get_component_name() const
Definition: std_expr.h:2542
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1968
An expression containing a side effect.
Definition: std_code.h:1898
const irep_idt & get_statement() const
Definition: std_code.h:1920
Operator to update elements in structs and arrays.
Definition: std_expr.h:2173
exprt & where()
Definition: std_expr.h:2193
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:312
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
#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:438
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1954
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:600
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:482
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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:238
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.