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