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 
19 #include <util/invariant.h>
20 
21 bool has_nondet(const exprt &dest)
22 {
23  forall_operands(it, dest)
24  if(has_nondet(*it))
25  return true;
26 
27  if(dest.id()==ID_side_effect)
28  {
29  const side_effect_exprt &side_effect_expr=to_side_effect_expr(dest);
30  const irep_idt &statement=side_effect_expr.get_statement();
31 
32  if(statement==ID_nondet)
33  return true;
34  }
35 
36  return false;
37 }
38 
39 void approximate_nondet_rec(exprt &dest, unsigned &count)
40 {
41  if(dest.id()==ID_side_effect &&
42  to_side_effect_expr(dest).get_statement()==ID_nondet)
43  {
44  count++;
45  dest.set(ID_identifier, "wp::nondet::"+std::to_string(count));
46  dest.id(ID_nondet_symbol);
47  return;
48  }
49 
50  Forall_operands(it, dest)
51  approximate_nondet_rec(*it, count);
52 }
53 
55 {
56  static unsigned count=0; // not proper, should be quantified
57  approximate_nondet_rec(dest, count);
58 }
59 
61 enum class aliasingt { A_MAY, A_MUST, A_MUSTNOT };
62 
64  const exprt &e1, const exprt &e2,
65  const namespacet &ns)
66 {
67  // deal with some dereferencing
68  if(
69  e1.id() == ID_dereference &&
70  to_dereference_expr(e1).pointer().id() == ID_address_of)
71  {
72  return aliasing(
73  to_address_of_expr(to_dereference_expr(e1).pointer()).object(), e2, ns);
74  }
75 
76  if(
77  e2.id() == ID_dereference &&
78  to_dereference_expr(e2).pointer().id() == ID_address_of)
79  {
80  return aliasing(
81  e1, to_address_of_expr(to_dereference_expr(e2).pointer()).object(), ns);
82  }
83 
84  // fairly radical. Ignores struct prefixes and the like.
85  if(e1.type() != e2.type())
86  return aliasingt::A_MUSTNOT;
87 
88  // syntactically the same?
89  if(e1==e2)
90  return aliasingt::A_MUST;
91 
92  // the trivial case first
93  if(e1.id()==ID_symbol && e2.id()==ID_symbol)
94  {
95  if(to_symbol_expr(e1).get_identifier()==
96  to_symbol_expr(e2).get_identifier())
97  return aliasingt::A_MUST;
98  else
99  return aliasingt::A_MUSTNOT;
100  }
101 
102  // an array or struct will never alias with a variable,
103  // nor will a struct alias with an array
104 
105  if(e1.id()==ID_index || e1.id()==ID_struct)
106  if(e2.id()!=ID_dereference && e1.id()!=e2.id())
107  return aliasingt::A_MUSTNOT;
108 
109  if(e2.id()==ID_index || e2.id()==ID_struct)
110  if(e2.id()!=ID_dereference && e1.id()!=e2.id())
111  return aliasingt::A_MUSTNOT;
112 
113  // we give up, and say it may
114  // (could do much more here)
115 
116  return aliasingt::A_MAY;
117 }
118 
121  exprt &dest,
122  const exprt &what,
123  const exprt &by,
124  const namespacet &ns)
125 {
126  if(dest.id()!=ID_address_of)
127  Forall_operands(it, dest)
128  substitute_rec(*it, what, by, ns);
129 
130  // possibly substitute?
131  if(dest.id()==ID_member ||
132  dest.id()==ID_index ||
133  dest.id()==ID_dereference ||
134  dest.id()==ID_symbol)
135  {
136  // could these be possible the same?
137  switch(aliasing(dest, what, ns))
138  {
139  case aliasingt::A_MUST:
140  dest=by; // they are always the same
141  break;
142 
143  case aliasingt::A_MAY:
144  {
145  // consider possible aliasing between 'what' and 'dest'
146  const address_of_exprt what_address(what);
147  const address_of_exprt dest_address(dest);
148 
149  equal_exprt alias_cond=equal_exprt(what_address, dest_address);
150 
151  const if_exprt if_expr(alias_cond, by, dest, dest.type());
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(new_lhs, exprt(ID_member_name), rhs);
173  new_rhs.where().set(ID_component_name, component_name);
174 
175  lhs=new_lhs;
176  rhs=new_rhs;
177 
178  rewrite_assignment(lhs, rhs); // rec. call
179  }
180  else if(lhs.id()==ID_index) // turn s[i]:=e into s:=(s with [i]=e)
181  {
182  const index_exprt index_expr=to_index_expr(lhs);
183  exprt new_lhs=index_expr.array();
184 
185  with_exprt new_rhs(new_lhs, index_expr.index(), rhs);
186 
187  lhs=new_lhs;
188  rhs=new_rhs;
189 
190  rewrite_assignment(lhs, rhs); // rec. call
191  }
192 }
193 
195  const code_assignt &code,
196  const exprt &post,
197  const namespacet &ns)
198 {
199  exprt pre=post;
200 
201  exprt lhs=code.lhs(),
202  rhs=code.rhs();
203 
204  // take care of non-determinism in the RHS
205  approximate_nondet(rhs);
206 
207  rewrite_assignment(lhs, rhs);
208 
209  // replace lhs by rhs in pre
210  substitute_rec(pre, lhs, rhs, ns);
211 
212  return pre;
213 }
214 
216  const code_assumet &code,
217  const exprt &post,
218  const namespacet &)
219 {
220  return implies_exprt(code.assumption(), post);
221 }
222 
224  const code_declt &code,
225  const exprt &post,
226  const namespacet &ns)
227 {
228  // Model decl(var) as var = nondet()
229  const exprt &var = code.symbol();
231  code_assignt assignment(var, nondet);
232 
233  return wp_assign(assignment, post, ns);
234 }
235 
237  const codet &code,
238  const exprt &post,
239  const namespacet &ns)
240 {
241  const irep_idt &statement=code.get_statement();
242 
243  if(statement==ID_assign)
244  return wp_assign(to_code_assign(code), post, ns);
245  else if(statement==ID_assume)
246  return wp_assume(to_code_assume(code), post, ns);
247  else if(statement==ID_skip)
248  return post;
249  else if(statement==ID_decl)
250  return wp_decl(to_code_decl(code), post, ns);
251  else if(statement==ID_assert)
252  return post;
253  else if(statement==ID_expression)
254  return post;
255  else if(statement==ID_printf)
256  return post; // ignored
257  else if(statement==ID_asm)
258  return post; // ignored
259  else if(statement==ID_fence)
260  return post; // ignored
262  false, "sorry, wp(", id2string(statement), "...) is not implemented");
263 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3050
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
aliasingt::A_MUST
@ A_MUST
substitute_rec
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:120
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
to_code_decl
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:450
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
invariant.h
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
code_assumet::assumption
const exprt & assumption() const
Definition: std_code.h:541
exprt
Base class for all expressions.
Definition: expr.h:53
has_nondet
bool has_nondet(const exprt &dest)
Definition: wp.cpp:21
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
approximate_nondet
void approximate_nondet(exprt &dest)
Approximate the non-deterministic choice in a way cheaper than by (proper) quantification.
Definition: wp.cpp:54
aliasingt
aliasingt
consider possible aliasing
Definition: wp.cpp:61
aliasingt::A_MUSTNOT
@ A_MUSTNOT
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1931
equal_exprt
Equality.
Definition: std_expr.h:1190
wp_decl
exprt wp_decl(const code_declt &code, const exprt &post, const namespacet &ns)
Definition: wp.cpp:223
INVARIANT_WITH_DIAGNOSTICS
#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
approximate_nondet_rec
void approximate_nondet_rec(exprt &dest, unsigned &count)
Definition: wp.cpp:39
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
to_code_assume
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:568
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3435
aliasing
aliasingt aliasing(const exprt &e1, const exprt &e2, const namespacet &ns)
Definition: wp.cpp:63
wp_assign
exprt wp_assign(const code_assignt &code, const exprt &post, const namespacet &ns)
Definition: wp.cpp:194
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:535
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
std_code.h
code_declt::symbol
symbol_exprt & symbol()
Definition: std_code.h:408
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1897
source_locationt
Definition: source_location.h:20
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
aliasingt::A_MAY
@ A_MAY
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2944
rewrite_assignment
void rewrite_assignment(exprt &lhs, exprt &rhs)
Definition: wp.cpp:164
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
wp_assume
exprt wp_assume(const code_assumet &code, const exprt &post, const namespacet &)
Definition: wp.cpp:215
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3419
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
wp
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:236
index_exprt
Array index operator.
Definition: std_expr.h:1293
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:71
std_expr.h
API to expression classes.
with_exprt::where
exprt & where()
Definition: std_expr.h:3070
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1866
wp.h
Weakest Preconditions.
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35