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 
31  bool remove_virtual_functions(goto_programt &goto_program);
32 
34  goto_programt &goto_program,
36  const dispatch_table_entriest &functions,
37  virtual_dispatch_fallback_actiont fallback_action);
38 
40 
41 protected:
42  const namespacet ns;
44 
46 
48  goto_programt &goto_program,
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 
83  goto_programt &goto_program,
85 {
86  const code_function_callt &code=
87  to_code_function_call(target->code);
88 
89  const exprt &function=code.function();
90  INVARIANT(
91  function.id()==ID_virtual_function,
92  "remove_virtual_function must take a virtual function call instruction");
93  INVARIANT(
94  !code.arguments().empty(),
95  "virtual function calls must have at least a this-argument");
96 
97  dispatch_table_entriest functions;
98  get_functions(function, functions);
99 
101  goto_program,
102  target,
103  functions,
105 }
106 
112  code_function_callt &call,
113  const symbol_exprt &function_symbol,
114  const namespacet &ns)
115 {
116  call.function() = function_symbol;
117  // Cast the `this` pointer to the correct type for the new callee:
118  const auto &callee_type =
119  to_code_type(ns.lookup(function_symbol.get_identifier()).type);
120  const code_typet::parametert *this_param = callee_type.get_this();
121  INVARIANT(
122  this_param != nullptr,
123  "Virtual function callees must have a `this` argument");
124  typet need_type = this_param->type();
125  if(!type_eq(call.arguments()[0].type(), need_type, ns))
126  call.arguments()[0].make_typecast(need_type);
127 }
128 
145  goto_programt &goto_program,
146  goto_programt::targett target,
147  const dispatch_table_entriest &functions,
148  virtual_dispatch_fallback_actiont fallback_action)
149 {
150  INVARIANT(
151  target->is_function_call(),
152  "remove_virtual_function must target a FUNCTION_CALL instruction");
153  const code_function_callt &code=
154  to_code_function_call(target->code);
155 
156  goto_programt::targett next_target = std::next(target);
157 
158  if(functions.empty())
159  {
160  target->make_skip();
161  remove_skip(goto_program, target, next_target);
162  return next_target; // give up
163  }
164 
165  // only one option?
166  if(functions.size()==1 &&
168  {
169  if(functions.begin()->symbol_expr==symbol_exprt())
170  {
171  target->make_skip();
172  remove_skip(goto_program, target, next_target);
173  }
174  else
175  {
177  to_code_function_call(target->code), functions.front().symbol_expr, ns);
178  }
179  return next_target;
180  }
181 
182  const auto &vcall_source_loc=target->source_location;
183 
184  // the final target is a skip
185  goto_programt final_skip;
186 
187  goto_programt::targett t_final=final_skip.add_instruction();
188  t_final->source_location=vcall_source_loc;
189 
190  t_final->make_skip();
191 
192  // build the calls and gotos
193 
194  goto_programt new_code_calls;
195  goto_programt new_code_gotos;
196 
197  exprt this_expr=code.arguments()[0];
198  const auto &last_function_symbol=functions.back().symbol_expr;
199 
200  const typet &this_type=this_expr.type();
201  INVARIANT(this_type.id() == ID_pointer, "this parameter must be a pointer");
202  INVARIANT(
203  this_type.subtype() != empty_typet(),
204  "this parameter must not be a void pointer");
205 
206  // So long as `this` is already not `void*` typed, the second parameter
207  // is ignored:
208  exprt this_class_identifier =
210 
211  // If instructed, add an ASSUME(FALSE) to handle the case where we don't
212  // match any expected type:
214  {
215  auto newinst=new_code_calls.add_instruction(ASSUME);
216  newinst->guard=false_exprt();
217  newinst->source_location=vcall_source_loc;
218  }
219 
220  // get initial identifier for grouping
221  INVARIANT(!functions.empty(), "Function dispatch table cannot be empty.");
222 
223  std::map<irep_idt, goto_programt::targett> calls;
224  // Note backwards iteration, to get the fallback candidate first.
225  for(auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it)
226  {
227  const auto &fun=*it;
228  auto insertit=calls.insert(
229  {fun.symbol_expr.get_identifier(), goto_programt::targett()});
230 
231  // Only create one call sequence per possible target:
232  if(insertit.second)
233  {
234  goto_programt::targett t1=new_code_calls.add_instruction();
235  t1->source_location=vcall_source_loc;
236  if(!fun.symbol_expr.get_identifier().empty())
237  {
238  // call function
239  t1->make_function_call(code);
241  to_code_function_call(t1->code), fun.symbol_expr, ns);
242  }
243  else
244  {
245  // No definition for this type; shouldn't be possible...
246  t1->make_assertion(false_exprt());
247  t1->source_location.set_comment(
248  "cannot find calls for " +
249  id2string(code.function().get(ID_identifier)) + " dispatching " +
250  id2string(fun.class_id));
251  }
252  insertit.first->second=t1;
253  // goto final
254  goto_programt::targett t3=new_code_calls.add_instruction();
255  t3->source_location=vcall_source_loc;
256  t3->make_goto(t_final, true_exprt());
257  }
258 
259  // Fall through to the default callee if possible:
260  if(fallback_action ==
262  fun.symbol_expr == last_function_symbol)
263  {
264  // Nothing to do
265  }
266  else
267  {
268  const constant_exprt fun_class_identifier(fun.class_id, string_typet());
269  const equal_exprt class_id_test(
270  fun_class_identifier, this_class_identifier);
271 
272  // If the previous GOTO goes to the same callee, join it
273  // (e.g. turning IF x GOTO y into IF x || z GOTO y)
274  if(it != functions.crbegin() &&
275  std::prev(it)->symbol_expr == fun.symbol_expr)
276  {
277  INVARIANT(
278  !new_code_gotos.empty(),
279  "a dispatch table entry has been processed already, "
280  "which should have created a GOTO");
281  new_code_gotos.instructions.back().guard =
282  or_exprt(new_code_gotos.instructions.back().guard, class_id_test);
283  }
284  else
285  {
286  goto_programt::targett new_goto = new_code_gotos.add_instruction();
287  new_goto->source_location = vcall_source_loc;
288  new_goto->make_goto(insertit.first->second, class_id_test);
289  }
290  }
291  }
292 
293  goto_programt new_code;
294 
295  // patch them all together
296  new_code.destructive_append(new_code_gotos);
297  new_code.destructive_append(new_code_calls);
298  new_code.destructive_append(final_skip);
299 
300  // set locations
302  {
303  const irep_idt property_class=it->source_location.get_property_class();
304  const irep_idt comment=it->source_location.get_comment();
305  it->source_location=target->source_location;
306  it->function=target->function;
307  if(!property_class.empty())
308  it->source_location.set_property_class(property_class);
309  if(!comment.empty())
310  it->source_location.set_comment(comment);
311  }
312 
313  goto_program.destructive_insert(next_target, new_code);
314 
315  // finally, kill original invocation
316  target->make_skip();
317 
318  // only remove skips within the virtual-function handling block
319  remove_skip(goto_program, target, next_target);
320 
321  return next_target;
322 }
323 
339  const irep_idt &this_id,
340  const symbol_exprt &last_method_defn,
341  const irep_idt &component_name,
342  dispatch_table_entriest &functions,
343  dispatch_table_entries_mapt &entry_map,
344  const function_call_resolvert &resolve_function_call) const
345 {
346  auto findit=class_hierarchy.class_map.find(this_id);
347  if(findit==class_hierarchy.class_map.end())
348  return;
349 
350  for(const auto &child : findit->second.children)
351  {
352  // Skip if we have already visited this and we found a function call that
353  // did not resolve to non java.lang.Object.
354  auto it = entry_map.find(child);
355  if(
356  it != entry_map.end() &&
357  !has_prefix(
358  id2string(it->second.symbol_expr.get_identifier()),
359  "java::java.lang.Object"))
360  {
361  continue;
362  }
363  exprt method = get_method(child, component_name);
364  dispatch_table_entryt function(child);
365  if(method.is_not_nil())
366  {
367  function.symbol_expr=to_symbol_expr(method);
368  function.symbol_expr.set(ID_C_class, child);
369  }
370  else
371  {
372  function.symbol_expr=last_method_defn;
373  }
374  if(function.symbol_expr == symbol_exprt())
375  {
377  &resolved_call = resolve_function_call(child, component_name);
378  if(resolved_call.is_valid())
379  {
380  function.class_id = resolved_call.get_class_identifier();
381  const symbolt &called_symbol =
383  resolved_call.get_full_component_identifier());
384 
385  function.symbol_expr = called_symbol.symbol_expr();
386  function.symbol_expr.set(
387  ID_C_class, resolved_call.get_class_identifier());
388  }
389  }
390  functions.push_back(function);
391  entry_map.insert({child, function});
392 
394  child,
395  function.symbol_expr,
396  component_name,
397  functions,
398  entry_map,
399  resolve_function_call);
400  }
401 }
402 
408  const exprt &function,
409  dispatch_table_entriest &functions)
410 {
411  // class part of function to call
412  const irep_idt class_id=function.get(ID_C_class);
413  const std::string class_id_string(id2string(class_id));
414  const irep_idt function_name = function.get(ID_component_name);
415  const std::string function_name_string(id2string(function_name));
416  INVARIANT(!class_id.empty(), "All virtual functions must have a class");
417 
418  resolve_inherited_componentt get_virtual_call_target(
420  const function_call_resolvert resolve_function_call =
421  [&get_virtual_call_target](
422  const irep_idt &class_id, const irep_idt &function_name) {
423  return get_virtual_call_target(class_id, function_name, false);
424  };
425 
427  &resolved_call = get_virtual_call_target(class_id, function_name, false);
428 
429  dispatch_table_entryt root_function;
430 
431  if(resolved_call.is_valid())
432  {
433  root_function.class_id=resolved_call.get_class_identifier();
434 
435  const symbolt &called_symbol =
437 
438  root_function.symbol_expr=called_symbol.symbol_expr();
439  root_function.symbol_expr.set(
440  ID_C_class, resolved_call.get_class_identifier());
441  }
442  else
443  {
444  // No definition here; this is an abstract function.
445  root_function.class_id=class_id;
446  }
447 
448  // iterate over all children, transitively
449  dispatch_table_entries_mapt entry_map;
451  class_id,
452  root_function.symbol_expr,
453  function_name,
454  functions,
455  entry_map,
456  resolve_function_call);
457 
458  if(root_function.symbol_expr!=symbol_exprt())
459  functions.push_back(root_function);
460 
461  // Sort for the identifier of the function call symbol expression, grouping
462  // together calls to the same function. Keep java.lang.Object entries at the
463  // end for fall through. The reasoning is that this is the case with most
464  // entries in realistic cases.
465  std::sort(
466  functions.begin(),
467  functions.end(),
469  {
470  if(
471  has_prefix(
472  id2string(a.symbol_expr.get_identifier()), "java::java.lang.Object"))
473  return false;
474  else if(
475  has_prefix(
476  id2string(b.symbol_expr.get_identifier()), "java::java.lang.Object"))
477  return true;
478  else
479  {
480  int cmp = a.symbol_expr.get_identifier().compare(
481  b.symbol_expr.get_identifier());
482  if(cmp == 0)
483  return a.class_id < b.class_id;
484  else
485  return cmp < 0;
486  }
487  });
488 }
489 
496  const irep_idt &class_id,
497  const irep_idt &component_name) const
498 {
499  const irep_idt &id=
501  class_id, component_name);
502 
503  const symbolt *symbol;
504  if(ns.lookup(id, symbol))
505  return nil_exprt();
506 
507  return symbol->symbol_expr();
508 }
509 
514  goto_programt &goto_program)
515 {
516  bool did_something=false;
517 
518  for(goto_programt::instructionst::iterator
519  target = goto_program.instructions.begin();
520  target != goto_program.instructions.end();
521  ) // remove_virtual_function returns the next instruction to process
522  {
523  if(target->is_function_call())
524  {
525  const code_function_callt &code=
526  to_code_function_call(target->code);
527 
528  if(code.function().id()==ID_virtual_function)
529  {
530  target = remove_virtual_function(goto_program, target);
531  did_something=true;
532  continue;
533  }
534  }
535 
536  ++target;
537  }
538 
539  if(did_something)
540  goto_program.update();
541 
542  return did_something;
543 }
544 
548 {
549  bool did_something=false;
550 
551  for(goto_functionst::function_mapt::iterator f_it=
552  functions.function_map.begin();
553  f_it!=functions.function_map.end();
554  f_it++)
555  {
556  goto_programt &goto_program=f_it->second.body;
557 
558  if(remove_virtual_functions(goto_program))
559  did_something=true;
560  }
561 
562  if(did_something)
563  functions.compute_location_numbers();
564 }
565 
569  const symbol_table_baset &symbol_table,
570  goto_functionst &goto_functions)
571 {
572  class_hierarchyt class_hierarchy;
573  class_hierarchy(symbol_table);
574  remove_virtual_functionst rvf(symbol_table, class_hierarchy);
575  rvf(goto_functions);
576 }
577 
580 {
582  goto_model.symbol_table, goto_model.goto_functions);
583 }
584 
587 {
588  class_hierarchyt class_hierarchy;
589  class_hierarchy(function.get_symbol_table());
590  remove_virtual_functionst rvf(function.get_symbol_table(), class_hierarchy);
591  rvf.remove_virtual_functions(function.get_goto_function().body);
592 }
593 
611  symbol_tablet &symbol_table,
612  goto_programt &goto_program,
613  goto_programt::targett instruction,
614  const dispatch_table_entriest &dispatch_table,
615  virtual_dispatch_fallback_actiont fallback_action)
616 {
617  class_hierarchyt class_hierarchy;
618  class_hierarchy(symbol_table);
619  remove_virtual_functionst rvf(symbol_table, class_hierarchy);
620 
622  goto_program, instruction, dispatch_table, fallback_action);
623 
624  goto_program.update();
625 
626  return next;
627 }
628 
630  goto_modelt &goto_model,
631  goto_programt &goto_program,
632  goto_programt::targett instruction,
633  const dispatch_table_entriest &dispatch_table,
634  virtual_dispatch_fallback_actiont fallback_action)
635 {
637  goto_model.symbol_table,
638  goto_program,
639  instruction,
640  dispatch_table,
641  fallback_action);
642 }
643 
645  const exprt &function,
646  const symbol_table_baset &symbol_table,
647  const class_hierarchyt &class_hierarchy,
648  dispatch_table_entriest &overridden_functions)
649 {
650  remove_virtual_functionst instance(symbol_table, class_hierarchy);
651  instance.get_functions(function, overridden_functions);
652 }
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality at the top level.
Definition: type_eq.cpp:31
The type of an expression, extends irept.
Definition: type.h:27
void operator()(goto_functionst &goto_functions)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
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:2531
bool remove_virtual_functions(goto_programt &goto_program)
Remove all virtual function calls in a GOTO program and replace them with calls to their most derived...
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.
Functions for replacing virtual function call with a static function calls in functions,...
Non-graph-based representation of the class hierarchy.
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
Type equality.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
const irep_idt & get_identifier() const
Definition: std_expr.h:176
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 p to *this. p is destroyed.
Definition: goto_program.h:524
virtual_dispatch_fallback_actiont
Specifies remove_virtual_function's behaviour when the actual supplied parameter does not match any o...
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
function_mapt function_map
typet & type()
Return the type of the expression.
Definition: expr.h:68
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.
Definition: symbol.h:27
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...
exprt get_class_identifier_field(const exprt &this_expr_in, const struct_tag_typet &suggested_type, const namespacet &ns)
A constant literal expression.
Definition: std_expr.h:4384
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)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:400
String type.
Definition: std_types.h:1662
Equality.
Definition: std_expr.h:1484
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:121
void compute_location_numbers()
The Boolean constant true.
Definition: std_expr.h:4443
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:1109
instructionst::iterator targett
Definition: goto_program.h:414
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
Returns symbol pointing to a specified method in a specified class.
The NIL expression.
Definition: std_expr.h:4461
The empty type.
Definition: std_types.h:48
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
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.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
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 p before target.
Definition: goto_program.h:532
class_mapt class_map
codet representation of a function call statement.
Definition: std_code.h:1036
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
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:35
bool get_this() const
Definition: std_types.h:838
The Boolean constant false.
Definition: std_expr.h:4452
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)
Replace virtual function call with a static function call Achieved by substituting a virtual function...
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
exprt & function()
Definition: std_code.h:1099
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
Base class for all expressions.
Definition: expr.h:54
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)
Replace virtual function call with a static function call Achieved by substituting a virtual function...
bool empty() const
Is the program empty?
Definition: goto_program.h:626
int compare(const dstringt &b) const
Definition: dstring.h:120
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
Expression to hold a symbol (variable)
Definition: std_expr.h:143
Extract class identifier.
dstringt irep_idt
Definition: irep.h:32
const typet & subtype() const
Definition: type.h:38
Program Transformation.
const class_hierarchyt & class_hierarchy
bool empty() const
Definition: dstring.h:75
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 documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
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:1173
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:153
remove_virtual_functionst(const symbol_table_baset &_symbol_table, const class_hierarchyt &_class_hierarchy)