cprover
remove_virtual_functions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove Virtual Function (Method) Calls
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
12 
13 #include <algorithm>
14 
15 #include <util/type_eq.h>
16 
17 #include "class_identifier.h"
18 #include "goto_model.h"
19 #include "remove_skip.h"
21 
23 {
24 public:
26  const symbol_table_baset &_symbol_table,
27  const class_hierarchyt &_class_hierarchy);
28 
29  void operator()(goto_functionst &goto_functions);
30 
32 
36  const dispatch_table_entriest &functions,
37  virtual_dispatch_fallback_actiont fallback_action);
38 
40 
41 protected:
42  const namespacet ns;
44 
46 
49  goto_programt::targett target);
50  typedef std::function<
52  const irep_idt &,
53  const irep_idt &)>
56  const irep_idt &,
57  const symbol_exprt &,
58  const irep_idt &,
61  const function_call_resolvert &) const;
62  exprt
63  get_method(const irep_idt &class_id, const irep_idt &component_name) const;
64 };
65 
67  const symbol_table_baset &_symbol_table,
68  const class_hierarchyt &_class_hierarchy)
69  : ns(_symbol_table),
70  symbol_table(_symbol_table),
71  class_hierarchy(_class_hierarchy)
72 {
73 }
74 
78 {
79  const code_function_callt &code=
80  to_code_function_call(target->code);
81 
82  const exprt &function=code.function();
83  INVARIANT(
84  function.id()==ID_virtual_function,
85  "remove_virtual_function must take a virtual function call instruction");
86  INVARIANT(
87  !code.arguments().empty(),
88  "virtual function calls must have at least a this-argument");
89 
90  dispatch_table_entriest functions;
91  get_functions(function, functions);
92 
95  target,
96  functions,
98 }
99 
105  code_function_callt &call,
106  const symbol_exprt &function_symbol,
107  const namespacet &ns)
108 {
109  call.function() = function_symbol;
110  // Cast the `this` pointer to the correct type for the new callee:
111  const auto &callee_type =
112  to_code_type(ns.lookup(function_symbol.get_identifier()).type);
113  const code_typet::parametert *this_param = callee_type.get_this();
114  INVARIANT(
115  this_param != nullptr,
116  "Virtual function callees must have a `this` argument");
117  typet need_type = this_param->type();
118  if(!type_eq(call.arguments()[0].type(), need_type, ns))
119  call.arguments()[0].make_typecast(need_type);
120 }
121 
124  goto_programt::targett target,
125  const dispatch_table_entriest &functions,
126  virtual_dispatch_fallback_actiont fallback_action)
127 {
128  INVARIANT(
129  target->is_function_call(),
130  "remove_virtual_function must target a FUNCTION_CALL instruction");
131  const code_function_callt &code=
132  to_code_function_call(target->code);
133 
134  goto_programt::targett next_target = std::next(target);
135 
136  if(functions.empty())
137  {
138  target->make_skip();
139  remove_skip(goto_program, target, next_target);
140  return next_target; // give up
141  }
142 
143  // only one option?
144  if(functions.size()==1 &&
146  {
147  if(functions.begin()->symbol_expr==symbol_exprt())
148  {
149  target->make_skip();
150  remove_skip(goto_program, target, next_target);
151  }
152  else
153  {
155  to_code_function_call(target->code), functions.front().symbol_expr, ns);
156  }
157  return next_target;
158  }
159 
160  const auto &vcall_source_loc=target->source_location;
161 
162  // the final target is a skip
163  goto_programt final_skip;
164 
165  goto_programt::targett t_final=final_skip.add_instruction();
166  t_final->source_location=vcall_source_loc;
167 
168  t_final->make_skip();
169 
170  // build the calls and gotos
171 
172  goto_programt new_code_calls;
173  goto_programt new_code_gotos;
174 
175  exprt this_expr=code.arguments()[0];
176  const auto &last_function_symbol=functions.back().symbol_expr;
177 
178  const typet &this_type=this_expr.type();
179  INVARIANT(this_type.id() == ID_pointer, "this parameter must be a pointer");
180  INVARIANT(
181  this_type.subtype() != empty_typet(),
182  "this parameter must not be a void pointer");
183 
184  // So long as `this` is already not `void*` typed, the second parameter
185  // is ignored:
186  exprt this_class_identifier =
188 
189  // If instructed, add an ASSUME(FALSE) to handle the case where we don't
190  // match any expected type:
192  {
193  auto newinst=new_code_calls.add_instruction(ASSUME);
194  newinst->guard=false_exprt();
195  newinst->source_location=vcall_source_loc;
196  }
197 
198  // get initial identifier for grouping
199  INVARIANT(!functions.empty(), "Function dispatch table cannot be empty.");
200 
201  std::map<irep_idt, goto_programt::targett> calls;
202  // Note backwards iteration, to get the fallback candidate first.
203  for(auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it)
204  {
205  const auto &fun=*it;
206  auto insertit=calls.insert(
207  {fun.symbol_expr.get_identifier(), goto_programt::targett()});
208 
209  // Only create one call sequence per possible target:
210  if(insertit.second)
211  {
212  goto_programt::targett t1=new_code_calls.add_instruction();
213  t1->source_location=vcall_source_loc;
214  if(!fun.symbol_expr.get_identifier().empty())
215  {
216  // call function
217  t1->make_function_call(code);
219  to_code_function_call(t1->code), fun.symbol_expr, ns);
220  }
221  else
222  {
223  // No definition for this type; shouldn't be possible...
224  t1->make_assertion(false_exprt());
225  t1->source_location.set_comment(
226  ("cannot find calls for " +
227  id2string(code.function().get(ID_identifier)) + " dispatching " +
228  id2string(fun.class_id)));
229  }
230  insertit.first->second=t1;
231  // goto final
232  goto_programt::targett t3=new_code_calls.add_instruction();
233  t3->source_location=vcall_source_loc;
234  t3->make_goto(t_final, true_exprt());
235  }
236 
237  // Fall through to the default callee if possible:
238  if(fallback_action ==
240  fun.symbol_expr == last_function_symbol)
241  {
242  // Nothing to do
243  }
244  else
245  {
246  const constant_exprt fun_class_identifier(fun.class_id, string_typet());
247  const equal_exprt class_id_test(
248  fun_class_identifier, this_class_identifier);
249 
250  // If the previous GOTO goes to the same callee, join it
251  // (e.g. turning IF x GOTO y into IF x || z GOTO y)
252  if(it != functions.crbegin() &&
253  std::prev(it)->symbol_expr == fun.symbol_expr)
254  {
255  INVARIANT(
256  !new_code_gotos.empty(),
257  "a dispatch table entry has been processed already, "
258  "which should have created a GOTO");
259  new_code_gotos.instructions.back().guard =
260  or_exprt(new_code_gotos.instructions.back().guard, class_id_test);
261  }
262  else
263  {
264  goto_programt::targett new_goto = new_code_gotos.add_instruction();
265  new_goto->source_location = vcall_source_loc;
266  new_goto->make_goto(insertit.first->second, class_id_test);
267  }
268  }
269  }
270 
271  goto_programt new_code;
272 
273  // patch them all together
274  new_code.destructive_append(new_code_gotos);
275  new_code.destructive_append(new_code_calls);
276  new_code.destructive_append(final_skip);
277 
278  // set locations
280  {
281  const irep_idt property_class=it->source_location.get_property_class();
282  const irep_idt comment=it->source_location.get_comment();
283  it->source_location=target->source_location;
284  it->function=target->function;
285  if(!property_class.empty())
286  it->source_location.set_property_class(property_class);
287  if(!comment.empty())
288  it->source_location.set_comment(comment);
289  }
290 
291  goto_program.destructive_insert(next_target, new_code);
292 
293  // finally, kill original invocation
294  target->make_skip();
295 
296  // only remove skips within the virtual-function handling block
297  remove_skip(goto_program, target, next_target);
298 
299  return next_target;
300 }
301 
316  const irep_idt &this_id,
317  const symbol_exprt &last_method_defn,
318  const irep_idt &component_name,
319  dispatch_table_entriest &functions,
320  dispatch_table_entries_mapt &entry_map,
321  const function_call_resolvert &resolve_function_call) const
322 {
323  auto findit=class_hierarchy.class_map.find(this_id);
324  if(findit==class_hierarchy.class_map.end())
325  return;
326 
327  for(const auto &child : findit->second.children)
328  {
329  // Skip if we have already visited this and we found a function call that
330  // did not resolve to non java.lang.Object.
331  auto it = entry_map.find(child);
332  if(
333  it != entry_map.end() &&
334  !has_prefix(
335  id2string(it->second.symbol_expr.get_identifier()),
336  "java::java.lang.Object"))
337  {
338  continue;
339  }
340  exprt method = get_method(child, component_name);
341  dispatch_table_entryt function(child);
342  if(method.is_not_nil())
343  {
344  function.symbol_expr=to_symbol_expr(method);
345  function.symbol_expr.set(ID_C_class, child);
346  }
347  else
348  {
349  function.symbol_expr=last_method_defn;
350  }
351  if(function.symbol_expr == symbol_exprt())
352  {
354  &resolved_call = resolve_function_call(child, component_name);
355  if(resolved_call.is_valid())
356  {
357  function.class_id = resolved_call.get_class_identifier();
358  const symbolt &called_symbol =
360  resolved_call.get_full_component_identifier());
361 
362  function.symbol_expr = called_symbol.symbol_expr();
363  function.symbol_expr.set(
364  ID_C_class, resolved_call.get_class_identifier());
365  }
366  }
367  functions.push_back(function);
368  entry_map.insert({child, function});
369 
371  child,
372  function.symbol_expr,
373  component_name,
374  functions,
375  entry_map,
376  resolve_function_call);
377  }
378 }
379 
385  const exprt &function,
386  dispatch_table_entriest &functions)
387 {
388  // class part of function to call
389  const irep_idt class_id=function.get(ID_C_class);
390  const std::string class_id_string(id2string(class_id));
391  const irep_idt function_name = function.get(ID_component_name);
392  const std::string function_name_string(id2string(function_name));
393  INVARIANT(!class_id.empty(), "All virtual functions must have a class");
394 
395  resolve_inherited_componentt get_virtual_call_target(
397  const function_call_resolvert resolve_function_call =
398  [&get_virtual_call_target](
399  const irep_idt &class_id, const irep_idt &function_name) {
400  return get_virtual_call_target(class_id, function_name, false);
401  };
402 
404  &resolved_call = get_virtual_call_target(class_id, function_name, false);
405 
406  dispatch_table_entryt root_function;
407 
408  if(resolved_call.is_valid())
409  {
410  root_function.class_id=resolved_call.get_class_identifier();
411 
412  const symbolt &called_symbol =
414 
415  root_function.symbol_expr=called_symbol.symbol_expr();
416  root_function.symbol_expr.set(
417  ID_C_class, resolved_call.get_class_identifier());
418  }
419  else
420  {
421  // No definition here; this is an abstract function.
422  root_function.class_id=class_id;
423  }
424 
425  // iterate over all children, transitively
426  dispatch_table_entries_mapt entry_map;
428  class_id,
429  root_function.symbol_expr,
430  function_name,
431  functions,
432  entry_map,
433  resolve_function_call);
434 
435  if(root_function.symbol_expr!=symbol_exprt())
436  functions.push_back(root_function);
437 
438  // Sort for the identifier of the function call symbol expression, grouping
439  // together calls to the same function. Keep java.lang.Object entries at the
440  // end for fall through. The reasoning is that this is the case with most
441  // entries in realistic cases.
442  std::sort(
443  functions.begin(),
444  functions.end(),
446  {
447  if(
448  has_prefix(
449  id2string(a.symbol_expr.get_identifier()), "java::java.lang.Object"))
450  return false;
451  else if(
452  has_prefix(
453  id2string(b.symbol_expr.get_identifier()), "java::java.lang.Object"))
454  return true;
455  else
456  {
457  int cmp = a.symbol_expr.get_identifier().compare(
458  b.symbol_expr.get_identifier());
459  if(cmp == 0)
460  return a.class_id < b.class_id;
461  else
462  return cmp < 0;
463  }
464  });
465 }
466 
468  const irep_idt &class_id,
469  const irep_idt &component_name) const
470 {
471  const irep_idt &id=
473  class_id, component_name);
474 
475  const symbolt *symbol;
476  if(ns.lookup(id, symbol))
477  return nil_exprt();
478 
479  return symbol->symbol_expr();
480 }
481 
484 {
485  bool did_something=false;
486 
487  for(goto_programt::instructionst::iterator
488  target = goto_program.instructions.begin();
489  target != goto_program.instructions.end();
490  ) // remove_virtual_function returns the next instruction to process
491  {
492  if(target->is_function_call())
493  {
494  const code_function_callt &code=
495  to_code_function_call(target->code);
496 
497  if(code.function().id()==ID_virtual_function)
498  {
499  target = remove_virtual_function(goto_program, target);
500  did_something=true;
501  continue;
502  }
503  }
504 
505  ++target;
506  }
507 
508  if(did_something)
510 
511  return did_something;
512 }
513 
515 {
516  bool did_something=false;
517 
518  for(goto_functionst::function_mapt::iterator f_it=
519  functions.function_map.begin();
520  f_it!=functions.function_map.end();
521  f_it++)
522  {
523  goto_programt &goto_program=f_it->second.body;
524 
526  did_something=true;
527  }
528 
529  if(did_something)
530  functions.compute_location_numbers();
531 }
532 
534  const symbol_table_baset &symbol_table,
535  goto_functionst &goto_functions)
536 {
537  class_hierarchyt class_hierarchy;
538  class_hierarchy(symbol_table);
539  remove_virtual_functionst rvf(symbol_table, class_hierarchy);
540  rvf(goto_functions);
541 }
542 
544 {
546  goto_model.symbol_table, goto_model.goto_functions);
547 }
548 
550 {
551  class_hierarchyt class_hierarchy;
552  class_hierarchy(function.get_symbol_table());
553  remove_virtual_functionst rvf(function.get_symbol_table(), class_hierarchy);
554  rvf.remove_virtual_functions(function.get_goto_function().body);
555 }
556 
558  symbol_tablet &symbol_table,
560  goto_programt::targett instruction,
561  const dispatch_table_entriest &dispatch_table,
562  virtual_dispatch_fallback_actiont fallback_action)
563 {
564  class_hierarchyt class_hierarchy;
565  class_hierarchy(symbol_table);
566  remove_virtual_functionst rvf(symbol_table, class_hierarchy);
567 
569  goto_program, instruction, dispatch_table, fallback_action);
570 
572 
573  return next;
574 }
575 
577  goto_modelt &goto_model,
579  goto_programt::targett instruction,
580  const dispatch_table_entriest &dispatch_table,
581  virtual_dispatch_fallback_actiont fallback_action)
582 {
584  goto_model.symbol_table,
585  goto_program,
586  instruction,
587  dispatch_table,
588  fallback_action);
589 }
590 
592  const exprt &function,
593  const symbol_table_baset &symbol_table,
594  const class_hierarchyt &class_hierarchy,
595  dispatch_table_entriest &overridden_functions)
596 {
597  remove_virtual_functionst instance(symbol_table, class_hierarchy);
598  instance.get_functions(function, overridden_functions);
599 }
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: type_eq.cpp:18
The type of an expression.
Definition: type.h:22
void operator()(goto_functionst &goto_functions)
void update()
Update all indices.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
void collect_virtual_function_callees(const exprt &function, const symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, dispatch_table_entriest &overridden_functions)
boolean OR
Definition: std_expr.h:2391
bool remove_virtual_functions(goto_programt &goto_program)
static void create_static_function_call(code_function_callt &call, const symbol_exprt &function_symbol, const namespacet &ns)
Create a concrete function call to replace a virtual one.
Remove Virtual Function (Method) Calls.
Non-graph-based representation of the class hierarchy.
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
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
bool is_valid() const
Use to check if this inherited_componentt has been fully constructed.
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
Definition: goto_program.h:486
virtual_dispatch_fallback_actiont
Specifies remove_virtual_function&#39;s behaviour when the actual supplied parameter does not match any o...
function_mapt function_map
typet & type()
Definition: expr.h:56
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
static irep_idt build_full_component_identifier(const irep_idt &class_name, const irep_idt &component_name)
Build a component name as found in a GOTO symbol table equivalent to the name of a concrete component...
A constant literal expression.
Definition: std_expr.h:4422
std::function< resolve_inherited_componentt::inherited_componentt(const irep_idt &, const irep_idt &)> function_call_resolvert
void remove_virtual_functions(const symbol_table_baset &symbol_table, goto_functionst &goto_functions)
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
TO_BE_DOCUMENTED.
Definition: std_types.h:1578
equality
Definition: std_expr.h:1354
const irep_idt & id() const
Definition: irep.h:259
Symbol Table + CFG.
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
void compute_location_numbers()
The boolean constant true.
Definition: std_expr.h:4486
void get_functions(const exprt &, dispatch_table_entriest &)
Used to get dispatch entries to call for the given function.
argumentst & arguments()
Definition: std_code.h:890
A reference into the symbol table.
Definition: std_types.h:110
instructionst::iterator targett
Definition: goto_program.h:397
std::vector< dispatch_table_entryt > dispatch_table_entriest
const symbol_table_baset & symbol_table
exprt get_method(const irep_idt &class_id, const irep_idt &component_name) const
The NIL expression.
Definition: std_expr.h:4508
The empty type.
Definition: std_types.h:54
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
When no callee type matches, ASSUME false, thus preventing any complete trace from using this path...
The symbol table.
Definition: symbol_table.h:19
void get_child_functions_rec(const irep_idt &, const symbol_exprt &, const irep_idt &, dispatch_table_entriest &, dispatch_table_entries_mapt &, const function_call_resolvert &) const
Used by get_functions to track the most-derived parent that provides an override of a given function...
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Given a class and a component (either field or method), find the closest parent that defines that com...
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
Definition: goto_program.h:495
class_mapt class_map
A function call.
Definition: std_code.h:858
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
When no callee type matches, call the last passed function, which is expected to be some safe default...
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
exprt get_class_identifier_field(const exprt &this_expr_in, const symbol_typet &suggested_type, const namespacet &ns)
bool get_this() const
Definition: std_types.h:850
The boolean constant false.
Definition: std_expr.h:4497
std::map< irep_idt, dispatch_table_entryt > dispatch_table_entries_mapt
goto_programt::targett remove_virtual_function(goto_programt &goto_program, goto_programt::targett target, const dispatch_table_entriest &functions, virtual_dispatch_fallback_actiont fallback_action)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
exprt & function()
Definition: std_code.h:878
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
The symbol table base class interface.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
goto_programt::targett remove_virtual_function(symbol_tablet &symbol_table, goto_programt &goto_program, goto_programt::targett instruction, const dispatch_table_entriest &dispatch_table, virtual_dispatch_fallback_actiont fallback_action)
bool empty() const
Is the program empty?
Definition: goto_program.h:590
int compare(const dstringt &b) const
Definition: dstring.h:118
goto_programt & goto_program
Definition: cover.cpp:63
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Expression to hold a symbol (variable)
Definition: std_expr.h:90
Extract class identifier.
dstringt irep_idt
Definition: irep.h:32
const typet & subtype() const
Definition: type.h:33
Program Transformation.
const class_hierarchyt & class_hierarchy
bool empty() const
Definition: dstring.h:73
irep_idt get_full_component_identifier() const
Get the full name of this function.
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
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition: goto_model.h:147
remove_virtual_functionst(const symbol_table_baset &_symbol_table, const class_hierarchyt &_class_hierarchy)