cprover
local_may_alias.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Field-insensitive, location-sensitive may-alias analysis
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "local_may_alias.h"
13
14#include <iterator>
15#include <algorithm>
16
17#include <util/arith_tools.h>
18#include <util/pointer_expr.h>
19#include <util/std_code.h>
20
21#include <util/c_types.h>
23
26{
27 bool changed=false;
28
29 // do union; this should be amortized linear
30 for(std::size_t i=0; i<src.aliases.size(); i++)
31 {
32 std::size_t root=src.aliases.find(i);
33
34 if(!aliases.same_set(i, root))
35 {
36 aliases.make_union(i, root);
37 changed=true;
38 }
39 }
40
41 return changed;
42}
43
45 const exprt &lhs,
46 const exprt &rhs,
47 const loc_infot &loc_info_src,
48 loc_infot &loc_info_dest)
49{
50 if(lhs.id()==ID_symbol)
51 {
52 if(lhs.type().id()==ID_pointer)
53 {
54 unsigned dest_pointer=objects.number(lhs);
55
56 // isolate the lhs pointer
57 loc_info_dest.aliases.isolate(dest_pointer);
58
59 object_sett rhs_set;
60 get_rec(rhs_set, rhs, loc_info_src);
61
62 // make these all aliases
63 for(object_sett::const_iterator
64 p_it=rhs_set.begin();
65 p_it!=rhs_set.end();
66 p_it++)
67 {
68 loc_info_dest.aliases.make_union(dest_pointer, *p_it);
69 }
70 }
71 }
72 else if(lhs.id()==ID_dereference)
73 {
74 // this might invalidate all pointers that are
75 // a) local and dirty
76 // b) global
77 if(lhs.type().id()==ID_pointer)
78 {
79 for(std::size_t i=0; i<objects.size(); i++)
80 {
81 if(objects[i].id()==ID_symbol)
82 {
83 const irep_idt &identifier=
85
86 if(dirty(identifier) || !locals.is_local(identifier))
87 {
88 loc_info_dest.aliases.isolate(i);
89 loc_info_dest.aliases.make_union(i, unknown_object);
90 }
91 }
92 }
93 }
94 }
95 else if(lhs.id()==ID_index)
96 {
97 assign_lhs(to_index_expr(lhs).array(), rhs, loc_info_src, loc_info_dest);
98 }
99 else if(lhs.id()==ID_member)
100 {
102 to_member_expr(lhs).struct_op(), rhs, loc_info_src, loc_info_dest);
103 }
104 else if(lhs.id()==ID_typecast)
105 {
106 assign_lhs(to_typecast_expr(lhs).op(), rhs, loc_info_src, loc_info_dest);
107 }
108 else if(lhs.id()==ID_if)
109 {
110 assign_lhs(to_if_expr(lhs).true_case(), rhs, loc_info_src, loc_info_dest);
111 assign_lhs(to_if_expr(lhs).false_case(), rhs, loc_info_src, loc_info_dest);
112 }
113}
114
115std::set<exprt> local_may_aliast::get(
117 const exprt &rhs) const
118{
119 local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t);
120
121 assert(loc_it!=cfg.loc_map.end());
122
123 const loc_infot &loc_info_src=loc_infos[loc_it->second];
124
125 object_sett result_tmp;
126 get_rec(result_tmp, rhs, loc_info_src);
127
128 std::set<exprt> result;
129
130 for(object_sett::const_iterator
131 it=result_tmp.begin();
132 it!=result_tmp.end();
133 it++)
134 {
135 result.insert(objects[*it]);
136 }
137
138 return result;
139}
140
143 const exprt &src1, const exprt &src2) const
144{
145 local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t);
146
147 assert(loc_it!=cfg.loc_map.end());
148
149 const loc_infot &loc_info_src=loc_infos[loc_it->second];
150
151 object_sett tmp1, tmp2;
152 get_rec(tmp1, src1, loc_info_src);
153 get_rec(tmp2, src2, loc_info_src);
154
155 if(tmp1.find(unknown_object)!=tmp1.end() ||
156 tmp2.find(unknown_object)!=tmp2.end())
157 return true;
158
159 std::list<unsigned> result;
160
161 std::set_intersection(
162 tmp1.begin(), tmp1.end(),
163 tmp2.begin(), tmp2.end(),
164 std::back_inserter(result));
165
166 return !result.empty();
167}
168
170 object_sett &dest,
171 const exprt &rhs,
172 const loc_infot &loc_info_src) const
173{
174 if(rhs.id()==ID_constant)
175 {
176 if(rhs.is_zero())
177 dest.insert(objects.number(exprt(ID_null_object)));
178 else
179 dest.insert(objects.number(exprt(ID_integer_address_object)));
180 }
181 else if(rhs.id()==ID_symbol)
182 {
183 if(rhs.type().id()==ID_pointer)
184 {
185 unsigned src_pointer=objects.number(rhs);
186
187 dest.insert(src_pointer);
188
189 for(std::size_t i=0; i<loc_info_src.aliases.size(); i++)
190 if(loc_info_src.aliases.same_set(src_pointer, i))
191 dest.insert(i);
192 }
193 else
194 dest.insert(unknown_object);
195 }
196 else if(rhs.id()==ID_if)
197 {
198 get_rec(dest, to_if_expr(rhs).false_case(), loc_info_src);
199 get_rec(dest, to_if_expr(rhs).true_case(), loc_info_src);
200 }
201 else if(rhs.id()==ID_address_of)
202 {
203 const exprt &object=to_address_of_expr(rhs).object();
204
205 if(object.id()==ID_symbol)
206 {
207 unsigned object_nr=objects.number(rhs);
208 dest.insert(object_nr);
209
210 for(std::size_t i=0; i<loc_info_src.aliases.size(); i++)
211 if(loc_info_src.aliases.same_set(object_nr, i))
212 dest.insert(i);
213 }
214 else if(object.id()==ID_index)
215 {
216 const index_exprt &index_expr=to_index_expr(object);
217 if(index_expr.array().id()==ID_symbol)
218 {
219 index_exprt tmp1=index_expr;
220 tmp1.index() = from_integer(0, c_index_type());
221 address_of_exprt tmp2(tmp1);
222 unsigned object_nr=objects.number(tmp2);
223 dest.insert(object_nr);
224
225 for(std::size_t i=0; i<loc_info_src.aliases.size(); i++)
226 if(loc_info_src.aliases.same_set(object_nr, i))
227 dest.insert(i);
228 }
229 else if(index_expr.array().id()==ID_string_constant)
230 {
231 index_exprt tmp1=index_expr;
232 tmp1.index() = from_integer(0, c_index_type());
233 address_of_exprt tmp2(tmp1);
234 unsigned object_nr=objects.number(tmp2);
235 dest.insert(object_nr);
236
237 for(std::size_t i=0; i<loc_info_src.aliases.size(); i++)
238 if(loc_info_src.aliases.same_set(object_nr, i))
239 dest.insert(i);
240 }
241 else
242 dest.insert(unknown_object);
243 }
244 else
245 dest.insert(unknown_object);
246 }
247 else if(rhs.id()==ID_typecast)
248 {
249 get_rec(dest, to_typecast_expr(rhs).op(), loc_info_src);
250 }
251 else if(rhs.id()==ID_plus)
252 {
253 const auto &plus_expr = to_plus_expr(rhs);
254
255 if(plus_expr.operands().size() >= 3)
256 {
258 plus_expr.op0().type().id() == ID_pointer,
259 "pointer in pointer-typed sum must be op0");
260 get_rec(dest, plus_expr.op0(), loc_info_src);
261 }
262 else if(plus_expr.operands().size() == 2)
263 {
264 // one must be pointer, one an integer
265 if(plus_expr.op0().type().id() == ID_pointer)
266 {
267 get_rec(dest, plus_expr.op0(), loc_info_src);
268 }
269 else if(plus_expr.op1().type().id() == ID_pointer)
270 {
271 get_rec(dest, plus_expr.op1(), loc_info_src);
272 }
273 else
274 dest.insert(unknown_object);
275 }
276 else
277 dest.insert(unknown_object);
278 }
279 else if(rhs.id()==ID_minus)
280 {
281 const auto &op0 = to_minus_expr(rhs).op0();
282
283 if(op0.type().id() == ID_pointer)
284 {
285 get_rec(dest, op0, loc_info_src);
286 }
287 else
288 dest.insert(unknown_object);
289 }
290 else if(rhs.id()==ID_member)
291 {
292 dest.insert(unknown_object);
293 }
294 else if(rhs.id()==ID_index)
295 {
296 dest.insert(unknown_object);
297 }
298 else if(rhs.id()==ID_dereference)
299 {
300 dest.insert(unknown_object);
301 }
302 else if(rhs.id()==ID_side_effect)
303 {
304 const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs);
305 const irep_idt &statement=side_effect_expr.get_statement();
306
307 if(statement==ID_allocate)
308 {
309 dest.insert(objects.number(exprt(ID_dynamic_object)));
310 }
311 else
312 dest.insert(unknown_object);
313 }
314 else if(rhs.is_nil())
315 {
316 // this means 'empty'
317 }
318 else
319 dest.insert(unknown_object);
320}
321
322void local_may_aliast::build(const goto_functiont &goto_function)
323{
324 if(cfg.nodes.empty())
325 return;
326
327 work_queuet work_queue;
328
329 // put all nodes into work queue
330 for(local_cfgt::node_nrt n=0; n<cfg.nodes.size(); n++)
331 work_queue.push(n);
332
333 unknown_object=objects.number(exprt(ID_unknown));
334
335 loc_infos.resize(cfg.nodes.size());
336
337 (void)goto_function; // unused parameter
338#if 0
339 // feed in sufficiently bad defaults
340 for(code_typet::parameterst::const_iterator
341 it=goto_function.type.parameters().begin();
342 it!=goto_function.type.parameters().end();
343 it++)
344 {
345 const irep_idt &identifier=it->get_identifier();
346 if(is_tracked(identifier))
347 loc_infos[0].points_to[objects.number(identifier)].objects.insert(
349 }
350#endif
351
352#if 0
353 for(localst::locals_mapt::const_iterator
354 l_it=locals.locals_map.begin();
355 l_it!=locals.locals_map.end();
356 l_it++)
357 {
358 if(is_tracked(l_it->first))
359 loc_infos[0].aliases.make_union(
360 objects.number(l_it->second), unknown_object);
361 }
362#endif
363
364 while(!work_queue.empty())
365 {
366 local_cfgt::node_nrt loc_nr=work_queue.top();
367 const local_cfgt::nodet &node=cfg.nodes[loc_nr];
368 const goto_programt::instructiont &instruction=*node.t;
369 work_queue.pop();
370
371 const loc_infot &loc_info_src=loc_infos[loc_nr];
372 loc_infot loc_info_dest=loc_infos[loc_nr];
373
374 switch(instruction.type())
375 {
376 case ASSIGN:
377 {
379 instruction.assign_lhs(),
380 instruction.assign_rhs(),
381 loc_info_src,
382 loc_info_dest);
383 break;
384 }
385
386 case DECL:
388 instruction.decl_symbol(), nil_exprt(), loc_info_src, loc_info_dest);
389 break;
390
391 case DEAD:
393 instruction.dead_symbol(), nil_exprt(), loc_info_src, loc_info_dest);
394 break;
395
396 case FUNCTION_CALL:
397 {
398 const auto &lhs = instruction.call_lhs();
399 if(lhs.is_not_nil())
400 assign_lhs(lhs, nil_exprt(), loc_info_src, loc_info_dest);
401
402 // this might invalidate all pointers that are
403 // a) local and dirty
404 // b) global
405 for(std::size_t i = 0; i < objects.size(); i++)
406 {
407 if(objects[i].id() == ID_symbol)
408 {
409 const irep_idt &identifier =
411
412 if(dirty(identifier) || !locals.is_local(identifier))
413 {
414 loc_info_dest.aliases.isolate(i);
415 loc_info_dest.aliases.make_union(i, unknown_object);
416 }
417 }
418 }
419 break;
420 }
421
422 case CATCH:
423 case THROW:
424 DATA_INVARIANT(false, "Exceptions must be removed before analysis");
425 break;
426 case SET_RETURN_VALUE:
427#if 0
428 DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
429#endif
430 break;
431 case GOTO: // Ignoring the guard is a valid over-approximation
432 case START_THREAD: // Require a concurrent analysis at higher level
433 case END_THREAD: // Require a concurrent analysis at higher level
434 case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
435 case ATOMIC_END: // Ignoring is a valid over-approximation
436 case LOCATION: // No action required
437 case SKIP: // No action required
438 case END_FUNCTION: // No action required
439 case ASSERT: // No action required
440 case ASSUME: // Ignoring is a valid over-approximation
441 break;
442 case OTHER:
443#if 0
445 false, "Unclear what is a safe over-approximation of OTHER");
446#endif
447 break;
448 case INCOMPLETE_GOTO:
450 DATA_INVARIANT(false, "Only complete instructions can be analyzed");
451 break;
452 }
453
454 for(local_cfgt::successorst::const_iterator
455 it=node.successors.begin();
456 it!=node.successors.end();
457 it++)
458 {
459 if(loc_infos[*it].merge(loc_info_dest))
460 work_queue.push(*it);
461 }
462 }
463}
464
466 std::ostream &out,
467 const goto_functiont &goto_function,
468 const namespacet &ns) const
469{
470 unsigned l=0;
471
472 for(const auto &instruction : goto_function.body.instructions)
473 {
474 out << "**** " << instruction.source_location() << "\n";
475
476 const loc_infot &loc_info=loc_infos[l];
477
478 for(std::size_t i=0; i<loc_info.aliases.size(); i++)
479 {
480 if(loc_info.aliases.count(i)!=1 &&
481 loc_info.aliases.find(i)==i) // root?
482 {
483 out << '{';
484 for(std::size_t j=0; j<loc_info.aliases.size(); j++)
485 if(loc_info.aliases.find(j)==i)
486 {
487 assert(j<objects.size());
488 irep_idt identifier;
489 if(objects[j].id() == ID_symbol)
490 identifier = to_symbol_expr(objects[j]).get_identifier();
491 out << ' ' << from_expr(ns, identifier, objects[j]);
492 }
493
494 out << " }";
495 out << "\n";
496 }
497 }
498
499 out << "\n";
500 goto_function.body.output_instruction(ns, irep_idt(), out, instruction);
501 out << "\n";
502
503 l++;
504 }
505}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bitvector_typet c_index_type()
Definition: c_types.cpp:16
Operator to return the address of an object.
Definition: pointer_expr.h:361
exprt & object()
Definition: pointer_expr.h:370
exprt & op0()
Definition: expr.h:99
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
typet & type()
Return the type of the expression.
Definition: expr.h:82
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
goto_programt body
Definition: goto_function.h:26
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:243
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:285
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:227
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:199
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:213
goto_program_instruction_typet type() const
What kind of instruction?
Definition: goto_program.h:343
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
instructionst::const_iterator const_targett
Definition: goto_program.h:593
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
Array index operator.
Definition: std_expr.h:1328
exprt & index()
Definition: std_expr.h:1363
exprt & array()
Definition: std_expr.h:1353
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
goto_programt::const_targett t
Definition: local_cfg.h:28
successorst successors
Definition: local_cfg.h:29
nodest nodes
Definition: local_cfg.h:36
std::size_t node_nrt
Definition: local_cfg.h:22
loc_mapt loc_map
Definition: local_cfg.h:33
bool merge(const loc_infot &src)
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
void assign_lhs(const exprt &lhs, const exprt &rhs, const loc_infot &loc_info_src, loc_infot &loc_info_dest)
void build(const goto_functiont &goto_function)
unsigned unknown_object
numberingt< exprt, irep_hash > objects
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
void get_rec(object_sett &dest, const exprt &rhs, const loc_infot &loc_info_src) const
std::stack< local_cfgt::node_nrt > work_queuet
loc_infost loc_infos
bool aliases(const goto_programt::const_targett t, const exprt &src1, const exprt &src2) const
std::set< unsigned > object_sett
bool is_local(const irep_idt &identifier) const
Definition: locals.h:37
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The NIL expression.
Definition: std_expr.h:2874
number_type number(const key_type &a)
Definition: numbering.h:37
size_type size() const
Definition: numbering.h:66
An expression containing a side effect.
Definition: std_code.h:1450
const irep_idt & get_statement() const
Definition: std_code.h:1472
const irep_idt & get_identifier() const
Definition: std_expr.h:109
size_type size() const
Definition: union_find.h:97
size_type find(size_type a) const
Definition: union_find.cpp:141
size_type count(size_type a) const
Definition: union_find.h:103
void make_union(size_type a, size_type b)
Definition: union_find.cpp:13
bool same_set(size_type a, size_type b) const
Definition: union_find.h:91
void isolate(size_type a)
Definition: union_find.cpp:41
@ FUNCTION_CALL
Definition: goto_program.h:49
@ ATOMIC_END
Definition: goto_program.h:44
@ DEAD
Definition: goto_program.h:48
@ END_FUNCTION
Definition: goto_program.h:42
@ ASSIGN
Definition: goto_program.h:46
@ ASSERT
Definition: goto_program.h:36
@ SET_RETURN_VALUE
Definition: goto_program.h:45
@ ATOMIC_BEGIN
Definition: goto_program.h:43
@ CATCH
Definition: goto_program.h:51
@ END_THREAD
Definition: goto_program.h:40
@ SKIP
Definition: goto_program.h:38
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
@ START_THREAD
Definition: goto_program.h:39
@ THROW
Definition: goto_program.h:50
@ DECL
Definition: goto_program.h:47
@ OTHER
Definition: goto_program.h:37
@ GOTO
Definition: goto_program.h:34
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
dstringt irep_idt
Definition: irep.h:37
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Field-insensitive, location-sensitive may-alias analysis.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1506
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:953
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:998
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.