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 }
remove_virtual_functionst::remove_virtual_function
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...
Definition: remove_virtual_functions.cpp:144
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
virtual_dispatch_fallback_actiont::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:43
dispatch_table_entryt
Definition: remove_virtual_functions.h:53
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
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:96
typet::subtype
const typet & subtype() const
Definition: type.h:38
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:42
resolve_inherited_componentt::inherited_componentt::is_valid
bool is_valid() const
Use to check if this inherited_componentt has been fully constructed.
Definition: resolve_inherited_component.cpp:108
comment
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
virtual_dispatch_fallback_actiont::ASSUME_FALSE
When no callee type matches, ASSUME false, thus preventing any complete trace from using this path.
remove_virtual_functionst::get_child_functions_rec
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.
Definition: remove_virtual_functions.cpp:338
typet
The type of an expression, extends irept.
Definition: type.h:27
remove_virtual_functions
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...
Definition: remove_virtual_functions.cpp:568
dispatch_table_entryt::class_id
irep_idt class_id
Definition: remove_virtual_functions.h:62
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:86
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:111
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
goto_programt::update
void update()
Update all indices.
Definition: goto_program.cpp:506
remove_virtual_functions.h
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:626
exprt
Base class for all expressions.
Definition: expr.h:54
resolve_inherited_componentt::inherited_componentt
Definition: resolve_inherited_component.h:27
goto_modelt
Definition: goto_model.h:24
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:400
resolve_inherited_componentt::inherited_componentt::get_full_component_identifier
irep_idt get_full_component_identifier() const
Get the full name of this function.
Definition: resolve_inherited_component.cpp:100
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
dispatch_table_entriest
std::vector< dispatch_table_entryt > dispatch_table_entriest
Definition: remove_virtual_functions.h:65
irep_idt
dstringt irep_idt
Definition: irep.h:32
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:143
equal_exprt
Equality.
Definition: std_expr.h:1484
resolve_inherited_component.h
remove_virtual_functionst::remove_virtual_functions
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...
Definition: remove_virtual_functions.cpp:513
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
type_eq.h
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
type_eq
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
empty_typet
The empty type.
Definition: std_types.h:48
or_exprt
Boolean OR.
Definition: std_expr.h:2531
remove_virtual_functionst::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:495
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:532
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
nil_exprt
The NIL expression.
Definition: std_expr.h:4461
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
irept::id
const irep_idt & id() const
Definition: irep.h:259
dispatch_table_entries_mapt
std::map< irep_idt, dispatch_table_entryt > dispatch_table_entries_mapt
Definition: remove_virtual_functions.h:66
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
class_hierarchyt::class_map
class_mapt class_map
Definition: class_hierarchy.h:55
dstringt::empty
bool empty() const
Definition: dstring.h:75
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
remove_virtual_functionst::get_functions
void get_functions(const exprt &, dispatch_table_entriest &)
Used to get dispatch entries to call for the given function.
Definition: remove_virtual_functions.cpp:407
dstringt::compare
int compare(const dstringt &b) const
Definition: dstring.h:120
code_typet::parametert::get_this
bool get_this() const
Definition: std_types.h:838
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1109
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:524
resolve_inherited_componentt::inherited_componentt::get_class_identifier
irep_idt get_class_identifier() const
Definition: resolve_inherited_component.h:41
remove_virtual_functionst::symbol_table
const symbol_table_baset & symbol_table
Definition: remove_virtual_functions.cpp:43
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
remove_virtual_functionst::function_call_resolvert
std::function< resolve_inherited_componentt::inherited_componentt(const irep_idt &, const irep_idt &)> function_call_resolvert
Definition: remove_virtual_functions.cpp:54
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
remove_virtual_functionst::remove_virtual_functionst
remove_virtual_functionst(const symbol_table_baset &_symbol_table, const class_hierarchyt &_class_hierarchy)
Definition: remove_virtual_functions.cpp:66
remove_virtual_functionst::operator()
void operator()(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:547
symbolt
Symbol table entry.
Definition: symbol.h:27
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
ASSUME
Definition: goto_program.h:35
string_typet
String type.
Definition: std_types.h:1662
code_typet::parametert
Definition: std_types.h:788
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
class_identifier.h
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
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
remove_virtual_functionst::ns
const namespacet ns
Definition: remove_virtual_functions.cpp:42
remove_skip.h
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
constant_exprt
A constant literal expression.
Definition: std_expr.h:4384
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)
Definition: remove_virtual_functions.cpp:644
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:153
remove_virtual_functionst::class_hierarchy
const class_hierarchyt & class_hierarchy
Definition: remove_virtual_functions.cpp:45
remove_virtual_function
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...
Definition: remove_virtual_functions.cpp:610
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
code_function_callt::function
exprt & function()
Definition: std_code.h:1099
validation_modet::INVARIANT
dispatch_table_entryt::symbol_expr
symbol_exprt symbol_expr
Definition: remove_virtual_functions.h:61
remove_virtual_functionst
Definition: remove_virtual_functions.cpp:22
resolve_inherited_componentt
Definition: resolve_inherited_component.h:21