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/expr_iterator.h>
16 #include <util/expr_util.h>
17 #include <util/fresh_symbol.h>
18 #include <util/prefix.h>
19 
20 #include "class_identifier.h"
21 #include "goto_model.h"
22 #include "remove_skip.h"
24 
26 {
27 public:
29  const symbol_table_baset &_symbol_table,
30  const class_hierarchyt &_class_hierarchy)
31  : ns(_symbol_table),
32  symbol_table(_symbol_table),
33  class_hierarchy(_class_hierarchy)
34  {
35  }
36 
37  void get_functions(const exprt &, dispatch_table_entriest &) const;
38 
39 private:
40  const namespacet ns;
42 
44 
45  typedef std::function<
47  const irep_idt &,
48  const irep_idt &)>
51  const irep_idt &,
53  const irep_idt &,
56  const function_call_resolvert &) const;
57  exprt
58  get_method(const irep_idt &class_id, const irep_idt &component_name) const;
59 };
60 
62 {
63 public:
65  symbol_table_baset &_symbol_table,
66  const class_hierarchyt &_class_hierarchy)
67  : class_hierarchy(_class_hierarchy),
68  symbol_table(_symbol_table),
70  {
71  }
72 
73  void operator()(goto_functionst &functions);
74 
76  const irep_idt &function_id,
77  goto_programt &goto_program);
78 
79 private:
83 
85  const irep_idt &function_id,
86  goto_programt &goto_program,
87  goto_programt::targett target);
88 };
89 
95  code_function_callt &call,
96  const symbol_exprt &function_symbol,
97  const namespacet &ns)
98 {
99  call.function() = function_symbol;
100  // Cast the pointers to the correct type for the new callee:
101  // Note the `this` pointer is expected to change type, but other pointers
102  // could also change due to e.g. using a different alias to refer to the same
103  // type (in Java, for example, we see ArrayList.add(ArrayList::E arg)
104  // overriding Collection.add(Collection::E arg))
105  const auto &callee_parameters =
106  to_code_type(ns.lookup(function_symbol.get_identifier()).type).parameters();
107  auto &call_args = call.arguments();
108 
109  INVARIANT(
110  callee_parameters.size() == call_args.size(),
111  "function overrides must have matching argument counts");
112 
113  for(std::size_t i = 0; i < call_args.size(); ++i)
114  {
115  const typet &need_type = callee_parameters[i].type();
116 
117  if(call_args[i].type() != need_type)
118  {
119  // If this wasn't language agnostic code we'd also like to check
120  // compatibility-- for example, Java overrides may have differing generic
121  // qualifiers, but not different base types.
122  INVARIANT(
123  call_args[i].type().id() == ID_pointer,
124  "where overriding function argument types differ, "
125  "those arguments must be pointer-typed");
126  call_args[i] = typecast_exprt(call_args[i], need_type);
127  }
128  }
129 }
130 
144  const goto_programt &goto_program,
146  const exprt &argument_for_this,
147  const symbol_exprt &temp_var_for_this)
148 {
149  goto_programt checks_directly_preceding_function_call;
150 
151  while(instr_it != goto_program.instructions.cbegin())
152  {
153  instr_it = std::prev(instr_it);
154 
155  if(instr_it->type == ASSERT)
156  {
157  continue;
158  }
159 
160  if(instr_it->type != ASSUME)
161  {
162  break;
163  }
164 
165  exprt guard = instr_it->get_condition();
166 
167  bool changed = false;
168  for(auto expr_it = guard.depth_begin(); expr_it != guard.depth_end();
169  ++expr_it)
170  {
171  if(*expr_it == argument_for_this)
172  {
173  expr_it.mutate() = temp_var_for_this;
174  changed = true;
175  }
176  }
177 
178  if(changed)
179  {
180  checks_directly_preceding_function_call.insert_before(
181  checks_directly_preceding_function_call.instructions.cbegin(),
183  }
184  }
185 
186  return checks_directly_preceding_function_call;
187 }
188 
201  const irep_idt &function_id,
202  const goto_programt &goto_program,
203  const goto_programt::targett target,
204  exprt &argument_for_this,
205  symbol_table_baset &symbol_table,
206  const source_locationt &vcall_source_loc,
207  goto_programt &new_code_for_this_argument)
208 {
209  if(has_subexpr(argument_for_this, ID_dereference))
210  {
211  // Create a temporary for the `this` argument. This is so that
212  // \ref goto_symext::try_filter_value_sets can reduce the value-set for
213  // `this` to those elements with the correct class identifier.
214  symbolt &temp_symbol = get_fresh_aux_symbol(
215  argument_for_this.type(),
216  id2string(function_id),
217  "this_argument",
218  vcall_source_loc,
219  symbol_table.lookup_ref(function_id).mode,
220  symbol_table);
221  const symbol_exprt temp_var_for_this = temp_symbol.symbol_expr();
222 
223  new_code_for_this_argument.add(
224  goto_programt::make_decl(temp_var_for_this, vcall_source_loc));
225  new_code_for_this_argument.add(
227  temp_var_for_this, argument_for_this, vcall_source_loc));
228 
229  goto_programt checks_directly_preceding_function_call =
231  goto_program, target, argument_for_this, temp_var_for_this);
232 
233  new_code_for_this_argument.destructive_append(
234  checks_directly_preceding_function_call);
235 
236  argument_for_this = temp_var_for_this;
237  }
238 }
239 
259  symbol_table_baset &symbol_table,
260  const irep_idt &function_id,
261  goto_programt &goto_program,
262  goto_programt::targett target,
263  const dispatch_table_entriest &functions,
264  virtual_dispatch_fallback_actiont fallback_action)
265 {
266  INVARIANT(
267  target->is_function_call(),
268  "remove_virtual_function must target a FUNCTION_CALL instruction");
269 
270  namespacet ns(symbol_table);
271  goto_programt::targett next_target = std::next(target);
272 
273  if(functions.empty())
274  {
275  target->turn_into_skip();
276  remove_skip(goto_program, target, next_target);
277  return next_target; // give up
278  }
279 
280  // only one option?
281  if(functions.size()==1 &&
283  {
284  if(!functions.front().symbol_expr.has_value())
285  {
286  target->turn_into_skip();
287  remove_skip(goto_program, target, next_target);
288  }
289  else
290  {
291  auto c = target->get_function_call();
292  create_static_function_call(c, *functions.front().symbol_expr, ns);
293  target->set_function_call(c);
294  }
295  return next_target;
296  }
297 
298  const auto &vcall_source_loc=target->source_location;
299 
300  code_function_callt code(target->get_function_call());
301  goto_programt new_code_for_this_argument;
302 
304  function_id,
305  goto_program,
306  target,
307  code.arguments()[0],
308  symbol_table,
309  vcall_source_loc,
310  new_code_for_this_argument);
311 
312  const exprt &this_expr = code.arguments()[0];
313 
314  // Create a skip as the final target for each branch to jump to at the end
315  goto_programt final_skip;
316 
317  goto_programt::targett t_final =
318  final_skip.add(goto_programt::make_skip(vcall_source_loc));
319 
320  // build the calls and gotos
321 
322  goto_programt new_code_calls;
323  goto_programt new_code_gotos;
324 
325  INVARIANT(
326  this_expr.type().id() == ID_pointer, "this parameter must be a pointer");
327  INVARIANT(
328  this_expr.type().subtype() != empty_typet(),
329  "this parameter must not be a void pointer");
330 
331  // So long as `this` is already not `void*` typed, the second parameter
332  // is ignored:
333  exprt this_class_identifier =
335 
336  // If instructed, add an ASSUME(FALSE) to handle the case where we don't
337  // match any expected type:
339  {
340  new_code_calls.add(
341  goto_programt::make_assumption(false_exprt(), vcall_source_loc));
342  }
343 
344  // get initial identifier for grouping
345  INVARIANT(!functions.empty(), "Function dispatch table cannot be empty.");
346  const auto &last_function_symbol = functions.back().symbol_expr;
347 
348  std::map<irep_idt, goto_programt::targett> calls;
349  // Note backwards iteration, to get the fallback candidate first.
350  for(auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it)
351  {
352  const auto &fun=*it;
353  irep_idt id_or_empty = fun.symbol_expr.has_value()
354  ? fun.symbol_expr->get_identifier()
355  : irep_idt();
356  auto insertit = calls.insert({id_or_empty, goto_programt::targett()});
357 
358  // Only create one call sequence per possible target:
359  if(insertit.second)
360  {
361  if(fun.symbol_expr.has_value())
362  {
363  // call function
364  auto new_call = code;
365 
366  create_static_function_call(new_call, *fun.symbol_expr, ns);
367 
368  goto_programt::targett t1 = new_code_calls.add(
369  goto_programt::make_function_call(new_call, vcall_source_loc));
370 
371  insertit.first->second = t1;
372  }
373  else
374  {
375  goto_programt::targett t1 = new_code_calls.add(
376  goto_programt::make_assertion(false_exprt(), vcall_source_loc));
377 
378  // No definition for this type; shouldn't be possible...
379  t1->source_location.set_comment(
380  "cannot find calls for " +
381  id2string(code.function().get(ID_identifier)) + " dispatching " +
382  id2string(fun.class_id));
383 
384  insertit.first->second = t1;
385  }
386 
387  // goto final
388  new_code_calls.add(
389  goto_programt::make_goto(t_final, true_exprt(), vcall_source_loc));
390  }
391 
392  // Fall through to the default callee if possible:
393  if(
394  fallback_action ==
396  fun.symbol_expr.has_value() == last_function_symbol.has_value() &&
397  (!fun.symbol_expr.has_value() ||
398  *fun.symbol_expr == *last_function_symbol))
399  {
400  // Nothing to do
401  }
402  else
403  {
404  const constant_exprt fun_class_identifier(fun.class_id, string_typet());
405  const equal_exprt class_id_test(
406  fun_class_identifier, this_class_identifier);
407 
408  // If the previous GOTO goes to the same callee, join it
409  // (e.g. turning IF x GOTO y into IF x || z GOTO y)
410  if(
411  it != functions.crbegin() &&
412  std::prev(it)->symbol_expr.has_value() == fun.symbol_expr.has_value() &&
413  (!fun.symbol_expr.has_value() ||
414  *(std::prev(it)->symbol_expr) == *fun.symbol_expr))
415  {
416  INVARIANT(
417  !new_code_gotos.empty(),
418  "a dispatch table entry has been processed already, "
419  "which should have created a GOTO");
420  new_code_gotos.instructions.back().guard =
421  or_exprt(new_code_gotos.instructions.back().guard, class_id_test);
422  }
423  else
424  {
425  new_code_gotos.add(goto_programt::make_goto(
426  insertit.first->second, class_id_test, vcall_source_loc));
427  }
428  }
429  }
430 
431  goto_programt new_code;
432 
433  // patch them all together
434  new_code.destructive_append(new_code_for_this_argument);
435  new_code.destructive_append(new_code_gotos);
436  new_code.destructive_append(new_code_calls);
437  new_code.destructive_append(final_skip);
438 
439  // set locations
441  {
442  const irep_idt property_class=it->source_location.get_property_class();
443  const irep_idt comment=it->source_location.get_comment();
444  it->source_location=target->source_location;
445  if(!property_class.empty())
446  it->source_location.set_property_class(property_class);
447  if(!comment.empty())
448  it->source_location.set_comment(comment);
449  }
450 
451  goto_program.destructive_insert(next_target, new_code);
452 
453  // finally, kill original invocation
454  target->turn_into_skip();
455 
456  // only remove skips within the virtual-function handling block
457  remove_skip(goto_program, target, next_target);
458 
459  return next_target;
460 }
461 
472  const irep_idt &function_id,
473  goto_programt &goto_program,
474  goto_programt::targett target)
475 {
476  const code_function_callt &code = target->get_function_call();
477 
478  const exprt &function = code.function();
479  INVARIANT(
481  "remove_virtual_function must take a function call instruction whose "
482  "function is a class method descriptor ");
483  INVARIANT(
484  !code.arguments().empty(),
485  "virtual function calls must have at least a this-argument");
486 
488  dispatch_table_entriest functions;
489  get_callees.get_functions(function, functions);
490 
492  symbol_table,
493  function_id,
494  goto_program,
495  target,
496  functions,
498 }
499 
515  const irep_idt &this_id,
516  const optionalt<symbol_exprt> &last_method_defn,
517  const irep_idt &component_name,
518  dispatch_table_entriest &functions,
519  dispatch_table_entries_mapt &entry_map,
520  const function_call_resolvert &resolve_function_call) const
521 {
522  auto findit=class_hierarchy.class_map.find(this_id);
523  if(findit==class_hierarchy.class_map.end())
524  return;
525 
526  for(const auto &child : findit->second.children)
527  {
528  // Skip if we have already visited this and we found a function call that
529  // did not resolve to non java.lang.Object.
530  auto it = entry_map.find(child);
531  if(
532  it != entry_map.end() &&
533  (!it->second.symbol_expr.has_value() ||
534  !has_prefix(
535  id2string(it->second.symbol_expr->get_identifier()),
536  "java::java.lang.Object")))
537  {
538  continue;
539  }
540  exprt method = get_method(child, component_name);
541  dispatch_table_entryt function(child);
542  if(method.is_not_nil())
543  {
544  function.symbol_expr=to_symbol_expr(method);
545  function.symbol_expr->set(ID_C_class, child);
546  }
547  else
548  {
549  function.symbol_expr=last_method_defn;
550  }
551  if(!function.symbol_expr.has_value())
552  {
553  const auto resolved_call = resolve_function_call(child, component_name);
554  if(resolved_call)
555  {
556  function.class_id = resolved_call->get_class_identifier();
557  const symbolt &called_symbol = symbol_table.lookup_ref(
558  resolved_call->get_full_component_identifier());
559 
560  function.symbol_expr = called_symbol.symbol_expr();
561  function.symbol_expr->set(
562  ID_C_class, resolved_call->get_class_identifier());
563  }
564  }
565  functions.push_back(function);
566  entry_map.emplace(child, function);
567 
569  child,
570  function.symbol_expr,
571  component_name,
572  functions,
573  entry_map,
574  resolve_function_call);
575  }
576 }
577 
583  const exprt &function,
584  dispatch_table_entriest &functions) const
585 {
586  // class part of function to call
587  const irep_idt class_id=function.get(ID_C_class);
588  const std::string class_id_string(id2string(class_id));
589  const irep_idt function_name = function.get(ID_component_name);
590  const std::string function_name_string(id2string(function_name));
591  INVARIANT(!class_id.empty(), "All virtual functions must have a class");
592 
593  resolve_inherited_componentt get_virtual_call_target{symbol_table};
594  const function_call_resolvert resolve_function_call =
595  [&get_virtual_call_target](
596  const irep_idt &class_id, const irep_idt &function_name) {
597  return get_virtual_call_target(class_id, function_name, false);
598  };
599 
600  const auto resolved_call =
601  get_virtual_call_target(class_id, function_name, false);
602 
603  // might be an abstract function
604  dispatch_table_entryt root_function(class_id);
605 
606  if(resolved_call)
607  {
608  root_function.class_id = resolved_call->get_class_identifier();
609 
610  const symbolt &called_symbol =
611  symbol_table.lookup_ref(resolved_call->get_full_component_identifier());
612 
613  root_function.symbol_expr=called_symbol.symbol_expr();
614  root_function.symbol_expr->set(
615  ID_C_class, resolved_call->get_class_identifier());
616  }
617 
618  // iterate over all children, transitively
619  dispatch_table_entries_mapt entry_map;
621  class_id,
622  root_function.symbol_expr,
623  function_name,
624  functions,
625  entry_map,
626  resolve_function_call);
627 
628  if(root_function.symbol_expr.has_value())
629  functions.push_back(root_function);
630 
631  // Sort for the identifier of the function call symbol expression, grouping
632  // together calls to the same function. Keep java.lang.Object entries at the
633  // end for fall through. The reasoning is that this is the case with most
634  // entries in realistic cases.
635  std::sort(
636  functions.begin(),
637  functions.end(),
638  [](const dispatch_table_entryt &a, const dispatch_table_entryt &b) {
639  irep_idt a_id = a.symbol_expr.has_value()
640  ? a.symbol_expr->get_identifier()
641  : irep_idt();
642  irep_idt b_id = b.symbol_expr.has_value()
643  ? b.symbol_expr->get_identifier()
644  : irep_idt();
645 
646  if(has_prefix(id2string(a_id), "java::java.lang.Object"))
647  return false;
648  else if(has_prefix(id2string(b_id), "java::java.lang.Object"))
649  return true;
650  else
651  {
652  int cmp = a_id.compare(b_id);
653  if(cmp == 0)
654  return a.class_id < b.class_id;
655  else
656  return cmp < 0;
657  }
658  });
659 }
660 
667  const irep_idt &class_id,
668  const irep_idt &component_name) const
669 {
670  const irep_idt &id=
672  class_id, component_name);
673 
674  const symbolt *symbol;
675  if(ns.lookup(id, symbol))
676  return nil_exprt();
677 
678  return symbol->symbol_expr();
679 }
680 
685  const irep_idt &function_id,
686  goto_programt &goto_program)
687 {
688  bool did_something=false;
689 
690  for(goto_programt::instructionst::iterator
691  target = goto_program.instructions.begin();
692  target != goto_program.instructions.end();
693  ) // remove_virtual_function returns the next instruction to process
694  {
695  if(target->is_function_call())
696  {
697  const code_function_callt &code = target->get_function_call();
698 
700  {
701  target = remove_virtual_function(function_id, goto_program, target);
702  did_something=true;
703  continue;
704  }
705  }
706 
707  ++target;
708  }
709 
710  if(did_something)
711  goto_program.update();
712 
713  return did_something;
714 }
715 
719 {
720  bool did_something=false;
721 
722  for(goto_functionst::function_mapt::iterator f_it=
723  functions.function_map.begin();
724  f_it!=functions.function_map.end();
725  f_it++)
726  {
727  const irep_idt &function_id = f_it->first;
728  goto_programt &goto_program=f_it->second.body;
729 
730  if(remove_virtual_functions(function_id, goto_program))
731  did_something=true;
732  }
733 
734  if(did_something)
735  functions.compute_location_numbers();
736 }
737 
743  symbol_table_baset &symbol_table,
744  goto_functionst &goto_functions)
745 {
746  class_hierarchyt class_hierarchy;
747  class_hierarchy(symbol_table);
748  remove_virtual_functionst rvf(symbol_table, class_hierarchy);
749  rvf(goto_functions);
750 }
751 
760  symbol_table_baset &symbol_table,
761  goto_functionst &goto_functions,
762  const class_hierarchyt &class_hierarchy)
763 {
764  remove_virtual_functionst rvf(symbol_table, class_hierarchy);
765  rvf(goto_functions);
766 }
767 
771 {
773  goto_model.symbol_table, goto_model.goto_functions);
774 }
775 
782  goto_modelt &goto_model,
783  const class_hierarchyt &class_hierarchy)
784 {
786  goto_model.symbol_table, goto_model.goto_functions, class_hierarchy);
787 }
788 
794 {
795  class_hierarchyt class_hierarchy;
796  class_hierarchy(function.get_symbol_table());
797  remove_virtual_functionst rvf(function.get_symbol_table(), class_hierarchy);
799  function.get_function_id(), function.get_goto_function().body);
800 }
801 
810  goto_model_functiont &function,
811  const class_hierarchyt &class_hierarchy)
812 {
813  remove_virtual_functionst rvf(function.get_symbol_table(), class_hierarchy);
815  function.get_function_id(), function.get_goto_function().body);
816 }
817 
837  symbol_tablet &symbol_table,
838  const irep_idt &function_id,
839  goto_programt &goto_program,
840  goto_programt::targett instruction,
841  const dispatch_table_entriest &dispatch_table,
842  virtual_dispatch_fallback_actiont fallback_action)
843 {
845  symbol_table,
846  function_id,
847  goto_program,
848  instruction,
849  dispatch_table,
850  fallback_action);
851 
852  goto_program.update();
853 
854  return next;
855 }
856 
858  goto_modelt &goto_model,
859  const irep_idt &function_id,
860  goto_programt &goto_program,
861  goto_programt::targett instruction,
862  const dispatch_table_entriest &dispatch_table,
863  virtual_dispatch_fallback_actiont fallback_action)
864 {
866  goto_model.symbol_table,
867  function_id,
868  goto_program,
869  instruction,
870  dispatch_table,
871  fallback_action);
872 }
873 
875  const exprt &function,
876  const symbol_table_baset &symbol_table,
877  const class_hierarchyt &class_hierarchy,
878  dispatch_table_entriest &overridden_functions)
879 {
880  get_virtual_calleest get_callees(symbol_table, class_hierarchy);
881  get_callees.get_functions(function, overridden_functions);
882 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1177
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION
@ CALL_LAST_FUNCTION
When no callee type matches, call the last passed function, which is expected to be some safe default...
virtual_dispatch_fallback_actiont
virtual_dispatch_fallback_actiont
Specifies remove_virtual_function's behaviour when the actual supplied parameter does not match any o...
Definition: remove_virtual_functions.h:58
dispatch_table_entryt
Definition: remove_virtual_functions.h:68
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
has_subexpr
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:139
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:43
get_callees
std::set< irep_idt > get_callees(const call_grapht::directed_grapht &graph, const irep_idt &function)
Get functions directly callable from a given function.
Definition: call_graph_helpers.cpp:31
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:331
virtual_dispatch_fallback_actiont::ASSUME_FALSE
@ ASSUME_FALSE
When no callee type matches, ASSUME false, thus preventing any complete trace from using this path.
typet
The type of an expression, extends irept.
Definition: type.h:29
fresh_symbol.h
dispatch_table_entryt::class_id
irep_idt class_id
Definition: remove_virtual_functions.h:98
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
create_static_function_call
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.
Definition: remove_virtual_functions.cpp:94
get_class_identifier_field
exprt get_class_identifier_field(const exprt &this_expr_in, const struct_tag_typet &suggested_type, const namespacet &ns)
Definition: class_identifier.cpp:56
prefix.h
goto_programt::update
void update()
Update all indices.
Definition: goto_program.cpp:541
remove_virtual_functions.h
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
remove_virtual_functions
void remove_virtual_functions(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...
Definition: remove_virtual_functions.cpp:742
goto_model.h
goto_functionst::compute_location_numbers
void compute_location_numbers()
Definition: goto_functions.cpp:18
goto_programt::empty
bool empty() const
Is the program empty?
Definition: goto_program.h:762
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
dispatch_table_entriest
std::vector< dispatch_table_entryt > dispatch_table_entriest
Definition: remove_virtual_functions.h:101
remove_virtual_functionst::remove_virtual_functionst
remove_virtual_functionst(symbol_table_baset &_symbol_table, const class_hierarchyt &_class_hierarchy)
Definition: remove_virtual_functions.cpp:64
irep_idt
dstringt irep_idt
Definition: irep.h:32
get_virtual_calleest::function_call_resolvert
std::function< optionalt< resolve_inherited_componentt::inherited_componentt > const irep_idt &, const irep_idt &)> function_call_resolvert
Definition: remove_virtual_functions.cpp:49
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:920
replace_virtual_function_with_dispatch_table
static goto_programt::targett replace_virtual_function_with_dispatch_table(symbol_table_baset &symbol_table, const irep_idt &function_id, 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...
Definition: remove_virtual_functions.cpp:258
equal_exprt
Equality.
Definition: std_expr.h:1196
get_virtual_calleest::ns
const namespacet ns
Definition: remove_virtual_functions.cpp:40
remove_virtual_functionst::ns
namespacet ns
Definition: remove_virtual_functions.cpp:82
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1024
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:998
resolve_inherited_component.h
remove_virtual_functionst::remove_virtual_functions
bool remove_virtual_functions(const irep_idt &function_id, goto_programt &goto_program)
Remove all virtual function calls in a GOTO program and replace them with calls to their most derived...
Definition: remove_virtual_functions.cpp:684
get_virtual_calleest::get_functions
void get_functions(const exprt &, dispatch_table_entriest &) const
Used to get dispatch entries to call for the given function.
Definition: remove_virtual_functions.cpp:582
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
goto_programt::make_function_call
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
Definition: goto_program.h:1049
remove_virtual_functionst::remove_virtual_function
goto_programt::targett remove_virtual_function(const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target)
Replace specified virtual function call with a static call to its most derived implementation.
Definition: remove_virtual_functions.cpp:471
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1186
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
goto_programt::insert_before
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:639
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
get_virtual_calleest::class_hierarchy
const class_hierarchyt & class_hierarchy
Definition: remove_virtual_functions.cpp:43
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
empty_typet
The empty type.
Definition: std_types.h:46
or_exprt
Boolean OR.
Definition: std_expr.h:2274
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:677
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
get_virtual_calleest::get_virtual_calleest
get_virtual_calleest(const symbol_table_baset &_symbol_table, const class_hierarchyt &_class_hierarchy)
Definition: remove_virtual_functions.cpp:28
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:851
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
nil_exprt
The NIL expression.
Definition: std_expr.h:4002
get_virtual_calleest::symbol_table
const symbol_table_baset & symbol_table
Definition: remove_virtual_functions.cpp:41
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
dispatch_table_entryt::symbol_expr
optionalt< symbol_exprt > symbol_expr
Definition: remove_virtual_functions.h:97
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
dispatch_table_entries_mapt
std::map< irep_idt, dispatch_table_entryt > dispatch_table_entries_mapt
Definition: remove_virtual_functions.h:102
class_hierarchyt::class_map
class_mapt class_map
Definition: class_hierarchy.h:55
dstringt::empty
bool empty() const
Definition: dstring.h:88
false_exprt
The Boolean constant false.
Definition: std_expr.h:3993
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1231
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:669
source_locationt
Definition: source_location.h:20
remove_virtual_function
goto_programt::targett remove_virtual_function(symbol_tablet &symbol_table, const irep_idt &function_id, 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...
Definition: remove_virtual_functions.cpp:836
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
expr_util.h
Deprecated expression utility functions.
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
process_this_argument
static void process_this_argument(const irep_idt &function_id, const goto_programt &goto_program, const goto_programt::targett target, exprt &argument_for_this, symbol_table_baset &symbol_table, const source_locationt &vcall_source_loc, goto_programt &new_code_for_this_argument)
If argument_for_this contains a dereference then create a temporary variable for it and use that inst...
Definition: remove_virtual_functions.cpp:200
expr_iterator.h
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
remove_virtual_functionst::symbol_table
symbol_table_baset & symbol_table
Definition: remove_virtual_functions.cpp:81
get_virtual_calleest::get_child_functions_rec
void get_child_functions_rec(const irep_idt &, const optionalt< 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.
Definition: remove_virtual_functions.cpp:514
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
can_cast_expr< class_method_descriptor_exprt >
bool can_cast_expr< class_method_descriptor_exprt >(const exprt &base)
Definition: std_expr.h:4637
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
ASSUME
@ ASSUME
Definition: goto_program.h:35
string_typet
String type.
Definition: std_types.h:1655
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
class_identifier.h
analyse_checks_directly_preceding_function_call
static goto_programt analyse_checks_directly_preceding_function_call(const goto_programt &goto_program, goto_programt::const_targett instr_it, const exprt &argument_for_this, const symbol_exprt &temp_var_for_this)
Duplicate ASSUME instructions involving argument_for_this for temp_var_for_this.
Definition: remove_virtual_functions.cpp:143
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:905
resolve_inherited_componentt::build_full_component_identifier
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...
Definition: resolve_inherited_component.cpp:88
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2042
remove_skip.h
true_exprt
The Boolean constant true.
Definition: std_expr.h:3984
constant_exprt
A constant literal expression.
Definition: std_expr.h:3935
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:333
collect_virtual_function_callees
void collect_virtual_function_callees(const exprt &function, const symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, dispatch_table_entriest &overridden_functions)
Given a function expression representing a virtual method of a class, the function computes all overr...
Definition: remove_virtual_functions.cpp:874
ASSERT
@ ASSERT
Definition: goto_program.h:36
comment
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
get_fresh_aux_symbol
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Definition: fresh_symbol.cpp:32
get_virtual_calleest::get_method
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.
Definition: remove_virtual_functions.cpp:666
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
remove_virtual_functionst::class_hierarchy
const class_hierarchyt & class_hierarchy
Definition: remove_virtual_functions.cpp:80
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
code_function_callt::function
exprt & function()
Definition: std_code.h:1221
validation_modet::INVARIANT
@ INVARIANT
remove_virtual_functionst
Definition: remove_virtual_functions.cpp:62
get_virtual_calleest
Definition: remove_virtual_functions.cpp:26
remove_virtual_functionst::operator()
void operator()(goto_functionst &functions)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
Definition: remove_virtual_functions.cpp:718
resolve_inherited_componentt
Definition: resolve_inherited_component.h:22