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,
167  ai_baset &,
168  const namespacet &)
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 &,
259  const namespacet &) 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 
276  a_it1!=aliases.end();
277  a_it1++)
278  {
279  bool first=true;
280 
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,
305  locationt)
306 {
307  bool changed=has_values.is_false();
309 
310  for(const auto &cleanup : b.cleanup_map)
311  {
312  const std::set<irep_idt> &b_cleanup=cleanup.second.cleanup_functions;
313  std::set<irep_idt> &a_cleanup=cleanup_map[cleanup.first].cleanup_functions;
314  auto old_size=a_cleanup.size();
315  a_cleanup.insert(b_cleanup.begin(), b_cleanup.end());
316  if(a_cleanup.size()!=old_size)
317  changed=true;
318  }
319 
320  // kill empty ones
321 
322  for(cleanup_mapt::iterator a_it=cleanup_map.begin();
323  a_it!=cleanup_map.end();
324  ) // no a_it++
325  {
326  if(a_it->second.cleanup_functions.empty())
327  a_it=cleanup_map.erase(a_it);
328  else
329  a_it++;
330  }
331 
332  // do union
334  it!=b.aliases.end(); it++)
335  {
336  irep_idt b_root=b.aliases.find(it);
337 
338  if(!aliases.same_set(*it, b_root))
339  {
340  aliases.make_union(*it, b_root);
341  changed=true;
342  }
343  }
344 
345  // isolate non-tracked ones
346  #if 0
348  it!=aliases.end(); it++)
349  {
350  if(cleanup_map.find(*it)==cleanup_map.end())
351  aliases.isolate(it);
352  }
353  #endif
354 
355  return changed;
356 }
357 
359  const exprt &lhs,
360  std::set<irep_idt> &cleanup_functions)
361 {
362  if(lhs.id()==ID_symbol)
363  {
364  const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();
365 
366  // pointer with cleanup function?
367  const escape_domaint::cleanup_mapt::const_iterator m_it=
368  cleanup_map.find(identifier);
369 
370  if(m_it!=cleanup_map.end())
371  {
372  // count the aliases
373 
374  std::size_t count=0;
375 
376  for(const auto &alias : aliases)
377  {
378  if(alias!=identifier && aliases.same_set(alias, identifier))
379  count+=1;
380  }
381 
382  // There is an alias? Then we are still ok.
383  if(count==0)
384  {
385  cleanup_functions.insert(
386  m_it->second.cleanup_functions.begin(),
387  m_it->second.cleanup_functions.end());
388  }
389  }
390  }
391 }
392 
394  goto_functionst::goto_functiont &goto_function,
395  goto_programt::targett location,
396  const exprt &lhs,
397  const std::set<irep_idt> &cleanup_functions,
398  bool is_object,
399  const namespacet &ns)
400 {
401  source_locationt source_location=location->source_location;
402 
403  for(const auto &cleanup : cleanup_functions)
404  {
405  symbol_exprt function=ns.lookup(cleanup).symbol_expr();
406  const code_typet &function_type=to_code_type(function.type());
407 
408  goto_function.body.insert_before_swap(location);
409  code_function_callt code;
410  code.lhs().make_nil();
411  code.function()=function;
412  code.function().add_source_location()=source_location;
413 
414  if(function_type.parameters().size()==1)
415  {
416  typet param_type=function_type.parameters().front().type();
417  exprt arg=lhs;
418  if(is_object)
419  arg=address_of_exprt(arg);
420  if(arg.type()!=param_type)
421  arg.make_typecast(param_type);
422  code.arguments().push_back(arg);
423  }
424 
425  location->make_function_call(code);
426  location->source_location=source_location;
427  }
428 }
429 
431  goto_modelt &goto_model)
432 {
433  const namespacet ns(goto_model.symbol_table);
434 
435  Forall_goto_functions(f_it, goto_model.goto_functions)
436  {
437  Forall_goto_program_instructions(i_it, f_it->second.body)
438  {
439  get_state(i_it);
440 
441  const goto_programt::instructiont &instruction=*i_it;
442 
443  switch(instruction.type)
444  {
445  case ASSIGN:
446  {
447  const code_assignt &code_assign=to_code_assign(instruction.code);
448 
449  std::set<irep_idt> cleanup_functions;
450  operator[](i_it).check_lhs(code_assign.lhs(), cleanup_functions);
452  f_it->second,
453  i_it,
454  code_assign.lhs(),
455  cleanup_functions,
456  false,
457  ns);
458  }
459  break;
460 
461  case DEAD:
462  {
463  const code_deadt &code_dead=to_code_dead(instruction.code);
464 
465  std::set<irep_idt> cleanup_functions1;
466 
467  escape_domaint &d=operator[](i_it);
468 
469  const escape_domaint::cleanup_mapt::const_iterator m_it=
470  d.cleanup_map.find("&"+id2string(code_dead.get_identifier()));
471 
472  // does it have a cleanup function for the object?
473  if(m_it!=d.cleanup_map.end())
474  {
475  cleanup_functions1.insert(
476  m_it->second.cleanup_functions.begin(),
477  m_it->second.cleanup_functions.end());
478  }
479 
480  std::set<irep_idt> cleanup_functions2;
481 
482  d.check_lhs(code_dead.symbol(), cleanup_functions2);
483 
485  f_it->second,
486  i_it,
487  code_dead.symbol(),
488  cleanup_functions1,
489  true,
490  ns);
492  f_it->second,
493  i_it,
494  code_dead.symbol(),
495  cleanup_functions2,
496  false,
497  ns);
498 
499  for(const auto &c : cleanup_functions1)
500  {
501  (void)c;
502  i_it++;
503  }
504 
505  for(const auto &c : cleanup_functions2)
506  {
507  (void)c;
508  i_it++;
509  }
510  }
511  break;
512 
513  default:
514  {
515  }
516  }
517  }
518 
519  Forall_goto_program_instructions(i_it, f_it->second.body)
520  get_state(i_it);
521  }
522 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3424
The type of an expression.
Definition: type.h:22
bool is_false() const
Definition: threeval.h:26
iterator end()
Definition: union_find.h:274
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:291
virtual statet & get_state(locationt l) override
Definition: ai.h:348
Base type of functions.
Definition: std_types.h:764
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
const irep_idt & get_identifier() const
Definition: std_code.cpp:19
exprt & object()
Definition: std_expr.h:3178
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:344
const exprt & op() const
Definition: std_expr.h:340
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:185
exprt & symbol()
Definition: std_code.h:268
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:993
const irep_idt & get_identifier() const
Definition: std_expr.h:128
static tvt unknown()
Definition: threeval.h:33
void transform(locationt from, 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 isolate(typename numbering< T >::const_iterator it)
Definition: union_find.h:250
typet & type()
Definition: expr.h:56
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Definition: std_expr.h:3199
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:188
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
iterator begin()
Definition: union_find.h:270
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
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:240
bool same_set(const T &a, const T &b) const
Definition: union_find.h:169
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:209
escape_domaint & operator[](locationt l)
Definition: ai.h:304
argumentst & arguments()
Definition: std_code.h:890
instructionst::iterator targett
Definition: goto_program.h:397
A declaration of a local variable.
Definition: std_code.h:254
bool is_known() const
Definition: threeval.h:28
exprt & rhs()
Definition: std_code.h:214
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:74
::goto_functiont goto_functiont
A function call.
Definition: std_code.h:858
cleanup_mapt cleanup_map
Field-insensitive, location-sensitive, over-approximative escape analysis.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Operator to return the address of an object.
Definition: std_expr.h:3168
exprt & symbol()
Definition: std_code.h:321
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:878
numbering_typet::const_iterator const_iterator
Definition: union_find.h:147
The basic interface of an abstract interpreter.
Definition: ai.h:32
Base class for all expressions.
Definition: expr.h:42
const parameterst & parameters() const
Definition: std_types.h:905
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:218
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
bool merge(const escape_domaint &b, locationt from, locationt to)
A removal of a local variable.
Definition: std_code.h:307
void make_nil()
Definition: irep.h:315
source_locationt & add_source_location()
Definition: expr.h:130
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
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:90
bool make_union(const T &a, const T &b)
Definition: union_find.h:150
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:73
void make_typecast(const typet &_type)
Definition: expr.cpp:84
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
Assignment.
Definition: std_code.h:196
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909