cprover
escape_analysis.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Field-insensitive, location-sensitive escape analysis
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "escape_analysis.h"
13 
14 #include <util/cprover_prefix.h>
15 #include <util/simplify_expr.h>
16 
18 {
19  const irep_idt &identifier=symbol.get_identifier();
20  if(
21  identifier == CPROVER_PREFIX "memory_leak" ||
22  identifier == CPROVER_PREFIX "malloc_object" ||
23  identifier == CPROVER_PREFIX "dead_object" ||
24  identifier == CPROVER_PREFIX "deallocated")
25  {
26  return false;
27  }
28 
29  return true;
30 }
31 
33 {
34  if(lhs.id()==ID_address_of)
35  return get_function(to_address_of_expr(lhs).object());
36  else if(lhs.id()==ID_typecast)
37  return get_function(to_typecast_expr(lhs).op());
38  else if(lhs.id()==ID_symbol)
39  {
40  irep_idt identifier=to_symbol_expr(lhs).get_identifier();
41  return identifier;
42  }
43 
44  return irep_idt();
45 }
46 
48  const exprt &lhs,
49  const std::set<irep_idt> &cleanup_functions)
50 {
51  if(lhs.id()==ID_symbol)
52  {
53  const symbol_exprt &symbol_expr=to_symbol_expr(lhs);
54  if(is_tracked(symbol_expr))
55  {
56  irep_idt identifier=symbol_expr.get_identifier();
57 
58  if(cleanup_functions.empty())
59  cleanup_map.erase(identifier);
60  else
61  cleanup_map[identifier].cleanup_functions=cleanup_functions;
62  }
63  }
64 }
65 
67  const exprt &lhs,
68  const std::set<irep_idt> &alias_set)
69 {
70  if(lhs.id()==ID_symbol)
71  {
72  const symbol_exprt &symbol_expr=to_symbol_expr(lhs);
73  if(is_tracked(symbol_expr))
74  {
75  irep_idt identifier=symbol_expr.get_identifier();
76 
77  aliases.isolate(identifier);
78 
79  for(const auto &alias : alias_set)
80  {
81  aliases.make_union(identifier, alias);
82  }
83  }
84  }
85 }
86 
88  const exprt &rhs,
89  std::set<irep_idt> &cleanup_functions)
90 {
91  if(rhs.id()==ID_symbol)
92  {
93  const symbol_exprt &symbol_expr=to_symbol_expr(rhs);
94  if(is_tracked(symbol_expr))
95  {
96  irep_idt identifier=symbol_expr.get_identifier();
97 
98  const escape_domaint::cleanup_mapt::const_iterator m_it=
99  cleanup_map.find(identifier);
100 
101  if(m_it!=cleanup_map.end())
102  cleanup_functions.insert(m_it->second.cleanup_functions.begin(),
103  m_it->second.cleanup_functions.end());
104  }
105  }
106  else if(rhs.id()==ID_if)
107  {
108  get_rhs_cleanup(to_if_expr(rhs).true_case(), cleanup_functions);
109  get_rhs_cleanup(to_if_expr(rhs).false_case(), cleanup_functions);
110  }
111  else if(rhs.id()==ID_typecast)
112  {
113  get_rhs_cleanup(to_typecast_expr(rhs).op(), cleanup_functions);
114  }
115 }
116 
118  const exprt &rhs,
119  std::set<irep_idt> &alias_set)
120 {
121  if(rhs.id()==ID_symbol)
122  {
123  const symbol_exprt &symbol_expr=to_symbol_expr(rhs);
124  if(is_tracked(symbol_expr))
125  {
126  irep_idt identifier=symbol_expr.get_identifier();
127  alias_set.insert(identifier);
128 
129  for(const auto &alias : aliases)
130  if(aliases.same_set(alias, identifier))
131  alias_set.insert(alias);
132  }
133  }
134  else if(rhs.id()==ID_if)
135  {
136  get_rhs_aliases(to_if_expr(rhs).true_case(), alias_set);
137  get_rhs_aliases(to_if_expr(rhs).false_case(), alias_set);
138  }
139  else if(rhs.id()==ID_typecast)
140  {
141  get_rhs_aliases(to_typecast_expr(rhs).op(), alias_set);
142  }
143  else if(rhs.id()==ID_address_of)
144  {
145  get_rhs_aliases_address_of(to_address_of_expr(rhs).op(), alias_set);
146  }
147 }
148 
150  const exprt &rhs,
151  std::set<irep_idt> &alias_set)
152 {
153  if(rhs.id()==ID_symbol)
154  {
155  irep_idt identifier=to_symbol_expr(rhs).get_identifier();
156  alias_set.insert("&"+id2string(identifier));
157  }
158  else if(rhs.id()==ID_if)
159  {
160  get_rhs_aliases_address_of(to_if_expr(rhs).true_case(), alias_set);
161  get_rhs_aliases_address_of(to_if_expr(rhs).false_case(), alias_set);
162  }
163  else if(rhs.id()==ID_dereference)
164  {
165  }
166 }
167 
169  const irep_idt &,
170  locationt from,
171  const irep_idt &,
172  locationt,
173  ai_baset &,
174  const namespacet &)
175 {
176  if(has_values.is_false())
177  return;
178 
179  // upcast of ai
180  // escape_analysist &ea=
181  // static_cast<escape_analysist &>(ai);
182 
183  const goto_programt::instructiont &instruction=*from;
184 
185  switch(instruction.type)
186  {
187  case ASSIGN:
188  {
189  const code_assignt &code_assign=to_code_assign(instruction.code);
190 
191  std::set<irep_idt> cleanup_functions;
192  get_rhs_cleanup(code_assign.rhs(), cleanup_functions);
193  assign_lhs_cleanup(code_assign.lhs(), cleanup_functions);
194 
195  std::set<irep_idt> rhs_aliases;
196  get_rhs_aliases(code_assign.rhs(), rhs_aliases);
197  assign_lhs_aliases(code_assign.lhs(), rhs_aliases);
198  }
199  break;
200 
201  case DECL:
202  {
203  const code_declt &code_decl=to_code_decl(instruction.code);
204  aliases.isolate(code_decl.get_identifier());
205  assign_lhs_cleanup(code_decl.symbol(), std::set<irep_idt>());
206  }
207  break;
208 
209  case DEAD:
210  {
211  const code_deadt &code_dead=to_code_dead(instruction.code);
212  aliases.isolate(code_dead.get_identifier());
213  assign_lhs_cleanup(code_dead.symbol(), std::set<irep_idt>());
214  }
215  break;
216 
217  case FUNCTION_CALL:
218  {
219  const code_function_callt &code_function_call=
220  to_code_function_call(instruction.code);
221  const exprt &function=code_function_call.function();
222 
223  if(function.id()==ID_symbol)
224  {
225  const irep_idt &identifier=to_symbol_expr(function).get_identifier();
226  if(identifier == CPROVER_PREFIX "cleanup")
227  {
228  if(code_function_call.arguments().size()==2)
229  {
230  exprt lhs=code_function_call.arguments()[0];
231 
232  irep_idt cleanup_function=
233  get_function(code_function_call.arguments()[1]);
234 
235  if(!cleanup_function.empty())
236  {
237  // may alias other stuff
238  std::set<irep_idt> lhs_set;
239  get_rhs_aliases(lhs, lhs_set);
240 
241  for(const auto &l : lhs_set)
242  {
243  cleanup_map[l].cleanup_functions.insert(cleanup_function);
244  }
245  }
246  }
247  }
248  }
249  }
250  break;
251 
252  case END_FUNCTION:
253  // This is the edge to the call site.
254  break;
255 
256  default:
257  {
258  }
259  }
260 }
261 
263  std::ostream &out,
264  const ai_baset &,
265  const namespacet &) const
266 {
267  if(has_values.is_known())
268  {
269  out << has_values.to_string() << '\n';
270  return;
271  }
272 
273  for(const auto &cleanup : cleanup_map)
274  {
275  out << cleanup.first << ':';
276  for(const auto &id : cleanup.second.cleanup_functions)
277  out << ' ' << id;
278  out << '\n';
279  }
280 
282  a_it1!=aliases.end();
283  a_it1++)
284  {
285  bool first=true;
286 
288  a_it2!=aliases.end();
289  a_it2++)
290  {
291  if(aliases.is_root(a_it1) && a_it1!=a_it2 &&
292  aliases.same_set(a_it1, a_it2))
293  {
294  if(first)
295  {
296  out << "Aliases: " << *a_it1;
297  first=false;
298  }
299  out << ' ' << *a_it2;
300  }
301  }
302 
303  if(!first)
304  out << '\n';
305  }
306 }
307 
309  const escape_domaint &b,
310  locationt,
311  locationt)
312 {
313  bool changed=has_values.is_false();
315 
316  for(const auto &cleanup : b.cleanup_map)
317  {
318  const std::set<irep_idt> &b_cleanup=cleanup.second.cleanup_functions;
319  std::set<irep_idt> &a_cleanup=cleanup_map[cleanup.first].cleanup_functions;
320  auto old_size=a_cleanup.size();
321  a_cleanup.insert(b_cleanup.begin(), b_cleanup.end());
322  if(a_cleanup.size()!=old_size)
323  changed=true;
324  }
325 
326  // kill empty ones
327 
328  for(cleanup_mapt::iterator a_it=cleanup_map.begin();
329  a_it!=cleanup_map.end();
330  ) // no a_it++
331  {
332  if(a_it->second.cleanup_functions.empty())
333  a_it=cleanup_map.erase(a_it);
334  else
335  a_it++;
336  }
337 
338  // do union
340  it!=b.aliases.end(); it++)
341  {
342  irep_idt b_root=b.aliases.find(it);
343 
344  if(!aliases.same_set(*it, b_root))
345  {
346  aliases.make_union(*it, b_root);
347  changed=true;
348  }
349  }
350 
351  // isolate non-tracked ones
352  #if 0
354  it!=aliases.end(); it++)
355  {
356  if(cleanup_map.find(*it)==cleanup_map.end())
357  aliases.isolate(it);
358  }
359  #endif
360 
361  return changed;
362 }
363 
365  const exprt &lhs,
366  std::set<irep_idt> &cleanup_functions)
367 {
368  if(lhs.id()==ID_symbol)
369  {
370  const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();
371 
372  // pointer with cleanup function?
373  const escape_domaint::cleanup_mapt::const_iterator m_it=
374  cleanup_map.find(identifier);
375 
376  if(m_it!=cleanup_map.end())
377  {
378  // count the aliases
379 
380  std::size_t count=0;
381 
382  for(const auto &alias : aliases)
383  {
384  if(alias!=identifier && aliases.same_set(alias, identifier))
385  count+=1;
386  }
387 
388  // There is an alias? Then we are still ok.
389  if(count==0)
390  {
391  cleanup_functions.insert(
392  m_it->second.cleanup_functions.begin(),
393  m_it->second.cleanup_functions.end());
394  }
395  }
396  }
397 }
398 
400  goto_functionst::goto_functiont &goto_function,
401  goto_programt::targett location,
402  const exprt &lhs,
403  const std::set<irep_idt> &cleanup_functions,
404  bool is_object,
405  const namespacet &ns)
406 {
407  source_locationt source_location=location->source_location;
408 
409  for(const auto &cleanup : cleanup_functions)
410  {
411  symbol_exprt function=ns.lookup(cleanup).symbol_expr();
412  const code_typet &function_type=to_code_type(function.type());
413 
414  goto_function.body.insert_before_swap(location);
415  code_function_callt code(function);
416  code.function().add_source_location()=source_location;
417 
418  if(function_type.parameters().size()==1)
419  {
420  typet param_type=function_type.parameters().front().type();
421  exprt arg=lhs;
422  if(is_object)
423  arg=address_of_exprt(arg);
424  if(arg.type()!=param_type)
425  arg.make_typecast(param_type);
426  code.arguments().push_back(arg);
427  }
428 
429  location->make_function_call(code);
430  location->source_location=source_location;
431  }
432 }
433 
435  goto_modelt &goto_model)
436 {
437  const namespacet ns(goto_model.symbol_table);
438 
439  Forall_goto_functions(f_it, goto_model.goto_functions)
440  {
441  Forall_goto_program_instructions(i_it, f_it->second.body)
442  {
443  get_state(i_it);
444 
445  const goto_programt::instructiont &instruction=*i_it;
446 
447  switch(instruction.type)
448  {
449  case ASSIGN:
450  {
451  const code_assignt &code_assign=to_code_assign(instruction.code);
452 
453  std::set<irep_idt> cleanup_functions;
454  operator[](i_it).check_lhs(code_assign.lhs(), cleanup_functions);
456  f_it->second,
457  i_it,
458  code_assign.lhs(),
459  cleanup_functions,
460  false,
461  ns);
462  }
463  break;
464 
465  case DEAD:
466  {
467  const code_deadt &code_dead=to_code_dead(instruction.code);
468 
469  std::set<irep_idt> cleanup_functions1;
470 
471  escape_domaint &d=operator[](i_it);
472 
473  const escape_domaint::cleanup_mapt::const_iterator m_it=
474  d.cleanup_map.find("&"+id2string(code_dead.get_identifier()));
475 
476  // does it have a cleanup function for the object?
477  if(m_it!=d.cleanup_map.end())
478  {
479  cleanup_functions1.insert(
480  m_it->second.cleanup_functions.begin(),
481  m_it->second.cleanup_functions.end());
482  }
483 
484  std::set<irep_idt> cleanup_functions2;
485 
486  d.check_lhs(code_dead.symbol(), cleanup_functions2);
487 
489  f_it->second,
490  i_it,
491  code_dead.symbol(),
492  cleanup_functions1,
493  true,
494  ns);
496  f_it->second,
497  i_it,
498  code_dead.symbol(),
499  cleanup_functions2,
500  false,
501  ns);
502 
503  for(const auto &c : cleanup_functions1)
504  {
505  (void)c;
506  i_it++;
507  }
508 
509  for(const auto &c : cleanup_functions2)
510  {
511  (void)c;
512  i_it++;
513  }
514  }
515  break;
516 
517  default:
518  {
519  }
520  }
521  }
522 
523  Forall_goto_program_instructions(i_it, f_it->second.body)
524  get_state(i_it);
525  }
526 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
The type of an expression, extends irept.
Definition: type.h:27
bool is_false() const
Definition: threeval.h:26
iterator end()
Definition: union_find.h:278
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:399
virtual statet & get_state(locationt l) override
Definition: ai.h:419
Base type of functions.
Definition: std_types.h:751
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
exprt & object()
Definition: std_expr.h:3265
#define CPROVER_PREFIX
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:473
const exprt & op() const
Definition: std_expr.h:371
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:190
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
const irep_idt & get_identifier() const
Definition: std_expr.h:176
const irep_idt & get_identifier() const
Definition: std_code.h:370
static tvt unknown()
Definition: threeval.h:33
void isolate(typename numbering< T >::const_iterator it)
Definition: union_find.h:254
typet & type()
Return the type of the expression.
Definition: expr.h:68
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
const T & find(typename numbering< T >::const_iterator it) const
Definition: union_find.h:192
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
iterator begin()
Definition: union_find.h:274
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
void get_rhs_aliases_address_of(const exprt &, std::set< irep_idt > &)
const char * to_string() const
Definition: threeval.cpp:13
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
bool same_set(const T &a, const T &b) const
Definition: union_find.h:173
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:269
escape_domaint & operator[](locationt l)
Definition: ai.h:375
argumentst & arguments()
Definition: std_code.h:1109
instructionst::iterator targett
Definition: goto_program.h:414
A codet representing the declaration of a local variable.
Definition: std_code.h:352
bool is_known() const
Definition: threeval.h:28
exprt & rhs()
Definition: std_code.h:274
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
void get_rhs_cleanup(const exprt &, std::set< irep_idt > &)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
::goto_functiont goto_functiont
codet representation of a function call statement.
Definition: std_code.h:1036
cleanup_mapt cleanup_map
Field-insensitive, location-sensitive, over-approximative escape analysis.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Operator to return the address of an object.
Definition: std_expr.h:3255
void assign_lhs_aliases(const exprt &, const std::set< irep_idt > &)
symbol_exprt & symbol()
Definition: std_code.h:432
void check_lhs(const exprt &, std::set< irep_idt > &)
symbol_exprt & symbol()
Definition: std_code.h:360
exprt & function()
Definition: std_code.h:1099
numbering_typet::const_iterator const_iterator
Definition: union_find.h:151
The basic interface of an abstract interpreter.
Definition: ai.h:32
Base class for all expressions.
Definition: expr.h:54
const parameterst & parameters() const
Definition: std_types.h:893
void insert_cleanup(goto_functionst::goto_functiont &, goto_programt::targett, const exprt &, const std::set< irep_idt > &, bool is_object, const namespacet &)
#define Forall_goto_functions(it, functions)
bool is_root(const T &a) const
Definition: union_find.h:222
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
bool merge(const escape_domaint &b, locationt from, locationt to)
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:424
source_locationt & add_source_location()
Definition: expr.h:233
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
irep_idt get_function(const exprt &)
goto_programt::const_targett locationt
Definition: ai_domain.h:40
Expression to hold a symbol (variable)
Definition: std_expr.h:143
bool make_union(const T &a, const T &b)
Definition: union_find.h:154
dstringt irep_idt
Definition: irep.h:32
void instrument(goto_modelt &)
void assign_lhs_cleanup(const exprt &, const std::set< irep_idt > &)
bool is_tracked(const symbol_exprt &)
bool empty() const
Definition: dstring.h:75
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
const irep_idt & get_identifier() const
Definition: std_code.h:442
A codet representing an assignment in the program.
Definition: std_code.h:256
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173