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