CBMC
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 "goto_instruction_code.h"
17 
18 #include <util/invariant.h>
19 #include <util/pointer_expr.h>
20 #include <util/std_code.h>
21 
22 bool has_nondet(const exprt &dest)
23 {
24  for(const auto &op : dest.operands())
25  {
26  if(has_nondet(op))
27  return true;
28  }
29 
30  if(dest.id()==ID_side_effect)
31  {
32  const side_effect_exprt &side_effect_expr=to_side_effect_expr(dest);
33  const irep_idt &statement=side_effect_expr.get_statement();
34 
35  if(statement==ID_nondet)
36  return true;
37  }
38 
39  return false;
40 }
41 
42 void approximate_nondet_rec(exprt &dest, unsigned &count)
43 {
44  if(dest.id()==ID_side_effect &&
45  to_side_effect_expr(dest).get_statement()==ID_nondet)
46  {
47  count++;
48  dest.set(ID_identifier, "wp::nondet::"+std::to_string(count));
49  dest.id(ID_nondet_symbol);
50  return;
51  }
52 
53  Forall_operands(it, dest)
54  approximate_nondet_rec(*it, count);
55 }
56 
58 {
59  static unsigned count=0; // not proper, should be quantified
60  approximate_nondet_rec(dest, count);
61 }
62 
64 enum class aliasingt { A_MAY, A_MUST, A_MUSTNOT };
65 
67  const exprt &e1, const exprt &e2,
68  const namespacet &ns)
69 {
70  // deal with some dereferencing
71  if(
72  e1.id() == ID_dereference &&
73  to_dereference_expr(e1).pointer().id() == ID_address_of)
74  {
75  return aliasing(
76  to_address_of_expr(to_dereference_expr(e1).pointer()).object(), e2, ns);
77  }
78 
79  if(
80  e2.id() == ID_dereference &&
81  to_dereference_expr(e2).pointer().id() == ID_address_of)
82  {
83  return aliasing(
84  e1, to_address_of_expr(to_dereference_expr(e2).pointer()).object(), ns);
85  }
86 
87  // fairly radical. Ignores struct prefixes and the like.
88  if(e1.type() != e2.type())
89  return aliasingt::A_MUSTNOT;
90 
91  // syntactically the same?
92  if(e1==e2)
93  return aliasingt::A_MUST;
94 
95  // the trivial case first
96  if(e1.id()==ID_symbol && e2.id()==ID_symbol)
97  {
98  if(to_symbol_expr(e1).get_identifier()==
99  to_symbol_expr(e2).get_identifier())
100  return aliasingt::A_MUST;
101  else
102  return aliasingt::A_MUSTNOT;
103  }
104 
105  // an array or struct will never alias with a variable,
106  // nor will a struct alias with an array
107 
108  if(e1.id()==ID_index || e1.id()==ID_struct)
109  if(e2.id()!=ID_dereference && e1.id()!=e2.id())
110  return aliasingt::A_MUSTNOT;
111 
112  if(e2.id()==ID_index || e2.id()==ID_struct)
113  if(e2.id()!=ID_dereference && e1.id()!=e2.id())
114  return aliasingt::A_MUSTNOT;
115 
116  // we give up, and say it may
117  // (could do much more here)
118 
119  return aliasingt::A_MAY;
120 }
121 
124  exprt &dest,
125  const exprt &what,
126  const exprt &by,
127  const namespacet &ns)
128 {
129  if(dest.id()!=ID_address_of)
130  Forall_operands(it, dest)
131  substitute_rec(*it, what, by, ns);
132 
133  // possibly substitute?
134  if(dest.id()==ID_member ||
135  dest.id()==ID_index ||
136  dest.id()==ID_dereference ||
137  dest.id()==ID_symbol)
138  {
139  // could these be possible the same?
140  switch(aliasing(dest, what, ns))
141  {
142  case aliasingt::A_MUST:
143  dest=by; // they are always the same
144  break;
145 
146  case aliasingt::A_MAY:
147  {
148  // consider possible aliasing between 'what' and 'dest'
149  const address_of_exprt what_address(what);
150  const address_of_exprt dest_address(dest);
151 
152  equal_exprt alias_cond=equal_exprt(what_address, dest_address);
153 
154  const if_exprt if_expr(alias_cond, by, dest, dest.type());
155 
156  dest=if_expr;
157  return;
158  }
159 
161  // nothing to do
162  break;
163  }
164  }
165 }
166 
168 {
169  if(lhs.id()==ID_member) // turn s.x:=e into s:=(s with .x=e)
170  {
171  const member_exprt member_expr=to_member_expr(lhs);
172  irep_idt component_name=member_expr.get_component_name();
173  exprt new_lhs=member_expr.struct_op();
174 
175  with_exprt new_rhs(new_lhs, exprt(ID_member_name), rhs);
176  new_rhs.where().set(ID_component_name, component_name);
177 
178  lhs=new_lhs;
179  rhs=new_rhs;
180 
181  rewrite_assignment(lhs, rhs); // rec. call
182  }
183  else if(lhs.id()==ID_index) // turn s[i]:=e into s:=(s with [i]=e)
184  {
185  const index_exprt index_expr=to_index_expr(lhs);
186  exprt new_lhs=index_expr.array();
187 
188  with_exprt new_rhs(new_lhs, index_expr.index(), 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_asm)
261  return post; // ignored
262  else if(statement==ID_fence)
263  return post; // ignored
265  false, "sorry, wp(", id2string(statement), "...) is not implemented");
266 }
Operator to return the address of an object.
Definition: pointer_expr.h:540
A goto_instruction_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 goto_instruction_codet representing the declaration of a local variable.
symbol_exprt & symbol()
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
const irep_idt & get_statement() const
Definition: std_code_base.h:65
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Equality.
Definition: std_expr.h:1361
Base class for all expressions.
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
The trinary if-then-else operator.
Definition: std_expr.h:2370
Boolean implication.
Definition: std_expr.h:2183
Array index operator.
Definition: std_expr.h:1465
exprt & array()
Definition: std_expr.h:1495
exprt & index()
Definition: std_expr.h:1505
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:408
const irep_idt & id() const
Definition: irep.h:384
Extract member of struct or union.
Definition: std_expr.h:2841
const exprt & struct_op() const
Definition: std_expr.h:2879
irep_idt get_component_name() const
Definition: std_expr.h:2863
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
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
const irep_idt & get_statement() const
Definition: std_code.h:1472
Operator to update elements in structs and arrays.
Definition: std_expr.h:2471
exprt & where()
Definition: std_expr.h:2491
#define Forall_operands(it, expr)
Definition: expr.h:27
const code_assignt & to_code_assign(const goto_instruction_codet &code)
const code_declt & to_code_decl(const goto_instruction_codet &code)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
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:890
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
#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 symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2933
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1533
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:197
void approximate_nondet_rec(exprt &dest, unsigned &count)
Definition: wp.cpp:42
exprt wp_assume(const code_assumet &code, const exprt &post, const namespacet &)
Definition: wp.cpp:218
void approximate_nondet(exprt &dest)
Approximate the non-deterministic choice in a way cheaper than by (proper) quantification.
Definition: wp.cpp:57
exprt wp_decl(const code_declt &code, const exprt &post, const namespacet &ns)
Definition: wp.cpp:226
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
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:123
aliasingt
consider possible aliasing
Definition: wp.cpp:64
aliasingt aliasing(const exprt &e1, const exprt &e2, const namespacet &ns)
Definition: wp.cpp:66
bool has_nondet(const exprt &dest)
Definition: wp.cpp:22
void rewrite_assignment(exprt &lhs, exprt &rhs)
Definition: wp.cpp:167
Weakest Preconditions.