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 #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(e1.id()==ID_dereference &&
70  e1.operands().size()==1 &&
71  e1.op0().id()==ID_address_of &&
72  e1.op0().operands().size()==1)
73  return aliasing(e1.op0().op0(), e2, ns);
74 
75  if(e2.id()==ID_dereference &&
76  e2.operands().size()==1 &&
77  e2.op0().id()==ID_address_of &&
78  e2.op0().operands().size()==1)
79  return aliasing(e1, e2.op0().op0(), ns);
80 
81  // fairly radical. Ignores struct prefixes and the like.
82  if(!base_type_eq(e1.type(), e2.type(), ns))
83  return aliasingt::A_MUSTNOT;
84 
85  // syntactically the same?
86  if(e1==e2)
87  return aliasingt::A_MUST;
88 
89  // the trivial case first
90  if(e1.id()==ID_symbol && e2.id()==ID_symbol)
91  {
94  return aliasingt::A_MUST;
95  else
96  return aliasingt::A_MUSTNOT;
97  }
98 
99  // an array or struct will never alias with a variable,
100  // nor will a struct alias with an array
101 
102  if(e1.id()==ID_index || e1.id()==ID_struct)
103  if(e2.id()!=ID_dereference && e1.id()!=e2.id())
104  return aliasingt::A_MUSTNOT;
105 
106  if(e2.id()==ID_index || e2.id()==ID_struct)
107  if(e2.id()!=ID_dereference && e1.id()!=e2.id())
108  return aliasingt::A_MUSTNOT;
109 
110  // we give up, and say it may
111  // (could do much more here)
112 
113  return aliasingt::A_MAY;
114 }
115 
118  exprt &dest,
119  const exprt &what,
120  const exprt &by,
121  const namespacet &ns)
122 {
123  if(dest.id()!=ID_address_of)
124  Forall_operands(it, dest)
125  substitute_rec(*it, what, by, ns);
126 
127  // possibly substitute?
128  if(dest.id()==ID_member ||
129  dest.id()==ID_index ||
130  dest.id()==ID_dereference ||
131  dest.id()==ID_symbol)
132  {
133  // could these be possible the same?
134  switch(aliasing(dest, what, ns))
135  {
136  case aliasingt::A_MUST:
137  dest=by; // they are always the same
138  break;
139 
140  case aliasingt::A_MAY:
141  {
142  // consider possible aliasing between 'what' and 'dest'
143  const address_of_exprt what_address(what);
144  const address_of_exprt dest_address(dest);
145 
146  equal_exprt alias_cond=equal_exprt(what_address, dest_address);
147 
148  const if_exprt if_expr(alias_cond, by, dest, dest.type());
149 
150  dest=if_expr;
151  return;
152  }
153 
155  // nothing to do
156  break;
157  }
158  }
159 }
160 
162 {
163  if(lhs.id()==ID_member) // turn s.x:=e into s:=(s with .x=e)
164  {
165  const member_exprt member_expr=to_member_expr(lhs);
166  irep_idt component_name=member_expr.get_component_name();
167  exprt new_lhs=member_expr.struct_op();
168 
169  with_exprt new_rhs;
170  new_rhs.type()=new_lhs.type();
171  new_rhs.old()=new_lhs;
172  new_rhs.where().id(ID_member_name);
173  new_rhs.where().set(ID_component_name, component_name);
174  new_rhs.new_value()=rhs;
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;
187  new_rhs.type()=new_lhs.type();
188  new_rhs.old()=new_lhs;
189  new_rhs.where()=index_expr.index();
190  new_rhs.new_value()=rhs;
191 
192  lhs=new_lhs;
193  rhs=new_rhs;
194 
195  rewrite_assignment(lhs, rhs); // rec. call
196  }
197 }
198 
200  const code_assignt &code,
201  const exprt &post,
202  const namespacet &ns)
203 {
204  exprt pre=post;
205 
206  exprt lhs=code.lhs(),
207  rhs=code.rhs();
208 
209  // take care of non-determinism in the RHS
210  approximate_nondet(rhs);
211 
212  rewrite_assignment(lhs, rhs);
213 
214  // replace lhs by rhs in pre
215  substitute_rec(pre, lhs, rhs, ns);
216 
217  return pre;
218 }
219 
221  const code_assumet &code,
222  const exprt &post,
223  const namespacet &)
224 {
225  return implies_exprt(code.assumption(), post);
226 }
227 
229  const code_declt &code,
230  const exprt &post,
231  const namespacet &ns)
232 {
233  // Model decl(var) as var = nondet()
234  const exprt &var = code.symbol();
236  code_assignt assignment(var, nondet);
237 
238  return wp_assign(assignment, post, ns);
239 }
240 
242  const codet &code,
243  const exprt &post,
244  const namespacet &ns)
245 {
246  const irep_idt &statement=code.get_statement();
247 
248  if(statement==ID_assign)
249  return wp_assign(to_code_assign(code), post, ns);
250  else if(statement==ID_assume)
251  return wp_assume(to_code_assume(code), post, ns);
252  else if(statement==ID_skip)
253  return post;
254  else if(statement==ID_decl)
255  return wp_decl(to_code_decl(code), post, ns);
256  else if(statement==ID_assert)
257  return post;
258  else if(statement==ID_expression)
259  return post;
260  else if(statement==ID_printf)
261  return post; // ignored
262  else if(statement==ID_asm)
263  return post; // ignored
264  else if(statement==ID_fence)
265  return post; // ignored
267  false, "sorry, wp(", id2string(statement), "...) is not implemented");
268 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3514
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
aliasingt::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:117
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:26
to_code_decl
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:399
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:274
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
with_exprt::new_value
exprt & new_value()
Definition: std_expr.h:3552
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:352
code_assumet::assumption
const exprt & assumption() const
Definition: std_code.h:510
exprt
Base class for all expressions.
Definition: expr.h:54
has_nondet
bool has_nondet(const exprt &dest)
Definition: wp.cpp:22
exprt::op0
exprt & op0()
Definition: expr.h:84
invariant.h
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
approximate_nondet
void approximate_nondet(exprt &dest)
approximate the non-deterministic choice in a way cheaper than by (proper) quantification
Definition: wp.cpp:55
aliasingt
aliasingt
consider possible aliasing
Definition: wp.cpp:62
aliasingt::A_MUSTNOT
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1620
equal_exprt
Equality.
Definition: std_expr.h:1484
wp_decl
exprt wp_decl(const code_declt &code, const exprt &post, const namespacet &ns)
Definition: wp.cpp:228
approximate_nondet_rec
void approximate_nondet_rec(exprt &dest, unsigned &count)
Definition: wp.cpp:40
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
to_code_assume
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:529
with_exprt::old
exprt & old()
Definition: std_expr.h:3532
base_type.h
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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:414
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
base_type_eq
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3931
aliasing
aliasingt aliasing(const exprt &e1, const exprt &e2, const namespacet &ns)
Definition: wp.cpp:64
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
wp_assign
exprt wp_assign(const code_assignt &code, const exprt &post, const namespacet &ns)
Definition: wp.cpp:199
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:496
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:269
index_exprt::index
exprt & index()
Definition: std_expr.h:1631
index_exprt::array
exprt & array()
Definition: std_expr.h:1621
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
irept::id
const irep_idt & id() const
Definition: irep.h:259
std_code.h
code_declt::symbol
symbol_exprt & symbol()
Definition: std_code.h:360
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1586
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:1633
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3890
aliasingt::A_MAY
rewrite_assignment
void rewrite_assignment(exprt &lhs, exprt &rhs)
Definition: wp.cpp:161
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
wp_assume
exprt wp_assume(const code_assumet &code, const exprt &post, const namespacet &)
Definition: wp.cpp:220
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3915
implies_exprt
Boolean implication.
Definition: std_expr.h:2485
exprt::operands
operandst & operands()
Definition: expr.h:78
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:241
index_exprt
Array index operator.
Definition: std_expr.h:1595
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:3255
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:56
std_expr.h
with_exprt::where
exprt & where()
Definition: std_expr.h:3542
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1560
wp.h
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34