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:43
bool is_not_nil() const
Definition: irep.h:103
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.
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:987
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:4424
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:205
TO_BE_DOCUMENTED.
Definition: std_types.h:1569
equality
Definition: std_expr.h:1354
const irep_idt & id() const
Definition: irep.h:189
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:4488
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:860
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:4510
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:828
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...
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:4499
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:848
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:106
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:31
const typet & subtype() const
Definition: type.h:33
Program Transformation.
const class_hierarchyt & class_hierarchy
bool empty() const
Definition: dstring.h:61
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:130
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879
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)