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