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 #include <util/symbol_table.h>
20 
21 #include "class_hierarchy.h"
22 #include "class_identifier.h"
23 #include "goto_model.h"
24 #include "remove_skip.h"
26 
28 {
29 public:
31  const symbol_table_baset &_symbol_table,
32  const class_hierarchyt &_class_hierarchy)
33  : ns(_symbol_table),
34  symbol_table(_symbol_table),
35  class_hierarchy(_class_hierarchy)
36  {
37  }
38 
39  void get_functions(const exprt &, dispatch_table_entriest &) const;
40 
41 private:
42  const namespacet ns;
44 
46 
47  typedef std::function<
49  const irep_idt &,
50  const irep_idt &)>
53  const irep_idt &,
55  const irep_idt &,
58  exprt
59  get_method(const irep_idt &class_id, const irep_idt &component_name) const;
60 };
61 
63 {
64 public:
66  symbol_table_baset &_symbol_table,
67  const class_hierarchyt &_class_hierarchy)
68  : class_hierarchy(_class_hierarchy),
69  symbol_table(_symbol_table),
71  {
72  }
73 
74  void operator()(goto_functionst &functions);
75 
77  const irep_idt &function_id,
78  goto_programt &goto_program);
79 
80 private:
84 
86  const irep_idt &function_id,
87  goto_programt &goto_program,
88  goto_programt::targett target);
89 };
90 
96  code_function_callt &call,
97  const symbol_exprt &function_symbol,
98  const namespacet &ns)
99 {
100  call.function() = function_symbol;
101  // Cast the pointers to the correct type for the new callee:
102  // Note the `this` pointer is expected to change type, but other pointers
103  // could also change due to e.g. using a different alias to refer to the same
104  // type (in Java, for example, we see ArrayList.add(ArrayList::E arg)
105  // overriding Collection.add(Collection::E arg))
106  const auto &callee_parameters =
107  to_code_type(ns.lookup(function_symbol.get_identifier()).type).parameters();
108  auto &call_args = call.arguments();
109 
110  INVARIANT(
111  callee_parameters.size() == call_args.size(),
112  "function overrides must have matching argument counts");
113 
114  for(std::size_t i = 0; i < call_args.size(); ++i)
115  {
116  const typet &need_type = callee_parameters[i].type();
117 
118  if(call_args[i].type() != need_type)
119  {
120  // If this wasn't language agnostic code we'd also like to check
121  // compatibility-- for example, Java overrides may have differing generic
122  // qualifiers, but not different base types.
123  INVARIANT(
124  call_args[i].type().id() == ID_pointer,
125  "where overriding function argument types differ, "
126  "those arguments must be pointer-typed");
127  call_args[i] = typecast_exprt(call_args[i], need_type);
128  }
129  }
130 }
131 
145  const goto_programt &goto_program,
147  const exprt &argument_for_this,
148  const symbol_exprt &temp_var_for_this)
149 {
150  goto_programt checks_directly_preceding_function_call;
151 
152  while(instr_it != goto_program.instructions.cbegin())
153  {
154  instr_it = std::prev(instr_it);
155 
156  if(instr_it->type == ASSERT)
157  {
158  continue;
159  }
160 
161  if(instr_it->type != ASSUME)
162  {
163  break;
164  }
165 
166  exprt guard = instr_it->get_condition();
167 
168  bool changed = false;
169  for(auto expr_it = guard.depth_begin(); expr_it != guard.depth_end();
170  ++expr_it)
171  {
172  if(*expr_it == argument_for_this)
173  {
174  expr_it.mutate() = temp_var_for_this;
175  changed = true;
176  }
177  }
178 
179  if(changed)
180  {
181  checks_directly_preceding_function_call.insert_before(
182  checks_directly_preceding_function_call.instructions.cbegin(),
184  }
185  }
186 
187  return checks_directly_preceding_function_call;
188 }
189 
202  const irep_idt &function_id,
203  const goto_programt &goto_program,
204  const goto_programt::targett target,
205  exprt &argument_for_this,
206  symbol_table_baset &symbol_table,
207  const source_locationt &vcall_source_loc,
208  goto_programt &new_code_for_this_argument)
209 {
210  if(has_subexpr(argument_for_this, ID_dereference))
211  {
212  // Create a temporary for the `this` argument. This is so that
213  // \ref goto_symext::try_filter_value_sets can reduce the value-set for
214  // `this` to those elements with the correct class identifier.
215  symbolt &temp_symbol = get_fresh_aux_symbol(
216  argument_for_this.type(),
217  id2string(function_id),
218  "this_argument",
219  vcall_source_loc,
220  symbol_table.lookup_ref(function_id).mode,
221  symbol_table);
222  const symbol_exprt temp_var_for_this = temp_symbol.symbol_expr();
223 
224  new_code_for_this_argument.add(
225  goto_programt::make_decl(temp_var_for_this, vcall_source_loc));
226  new_code_for_this_argument.add(
228  temp_var_for_this, argument_for_this, vcall_source_loc));
229 
230  goto_programt checks_directly_preceding_function_call =
232  goto_program, target, argument_for_this, temp_var_for_this);
233 
234  new_code_for_this_argument.destructive_append(
235  checks_directly_preceding_function_call);
236 
237  argument_for_this = temp_var_for_this;
238  }
239 }
240 
260  symbol_table_baset &symbol_table,
261  const irep_idt &function_id,
262  goto_programt &goto_program,
263  goto_programt::targett target,
264  const dispatch_table_entriest &functions,
265  virtual_dispatch_fallback_actiont fallback_action)
266 {
267  INVARIANT(
268  target->is_function_call(),
269  "remove_virtual_function must target a FUNCTION_CALL instruction");
270 
271  namespacet ns(symbol_table);
272  goto_programt::targett next_target = std::next(target);
273 
274  if(functions.empty())
275  {
276  target->turn_into_skip();
277  remove_skip(goto_program, target, next_target);
278  return next_target; // give up
279  }
280 
281  // only one option?
282  if(functions.size()==1 &&
284  {
285  if(!functions.front().symbol_expr.has_value())
286  {
287  target->turn_into_skip();
288  remove_skip(goto_program, target, next_target);
289  }
290  else
291  {
292  auto c = target->get_function_call();
293  create_static_function_call(c, *functions.front().symbol_expr, ns);
294  target->set_function_call(c);
295  }
296  return next_target;
297  }
298 
299  const auto &vcall_source_loc=target->source_location;
300 
301  code_function_callt code(target->get_function_call());
302  goto_programt new_code_for_this_argument;
303 
305  function_id,
306  goto_program,
307  target,
308  code.arguments()[0],
309  symbol_table,
310  vcall_source_loc,
311  new_code_for_this_argument);
312 
313  const exprt &this_expr = code.arguments()[0];
314 
315  // Create a skip as the final target for each branch to jump to at the end
316  goto_programt final_skip;
317 
318  goto_programt::targett t_final =
319  final_skip.add(goto_programt::make_skip(vcall_source_loc));
320 
321  // build the calls and gotos
322 
323  goto_programt new_code_calls;
324  goto_programt new_code_gotos;
325 
326  INVARIANT(
327  this_expr.type().id() == ID_pointer, "this parameter must be a pointer");
328  INVARIANT(
329  this_expr.type().subtype() != empty_typet(),
330  "this parameter must not be a void pointer");
331 
332  // So long as `this` is already not `void*` typed, the second parameter
333  // is ignored:
334  exprt this_class_identifier =
336 
337  // If instructed, add an ASSUME(FALSE) to handle the case where we don't
338  // match any expected type:
340  {
341  new_code_calls.add(
342  goto_programt::make_assumption(false_exprt(), vcall_source_loc));
343  }
344 
345  // get initial identifier for grouping
346  INVARIANT(!functions.empty(), "Function dispatch table cannot be empty.");
347  const auto &last_function_symbol = functions.back().symbol_expr;
348 
349  std::map<irep_idt, goto_programt::targett> calls;
350  // Note backwards iteration, to get the fallback candidate first.
351  for(auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it)
352  {
353  const auto &fun=*it;
354  irep_idt id_or_empty = fun.symbol_expr.has_value()
355  ? fun.symbol_expr->get_identifier()
356  : irep_idt();
357  auto insertit = calls.insert({id_or_empty, goto_programt::targett()});
358 
359  // Only create one call sequence per possible target:
360  if(insertit.second)
361  {
362  if(fun.symbol_expr.has_value())
363  {
364  // call function
365  auto new_call = code;
366 
367  create_static_function_call(new_call, *fun.symbol_expr, ns);
368 
369  goto_programt::targett t1 = new_code_calls.add(
370  goto_programt::make_function_call(new_call, vcall_source_loc));
371 
372  insertit.first->second = t1;
373  }
374  else
375  {
376  goto_programt::targett t1 = new_code_calls.add(
377  goto_programt::make_assertion(false_exprt(), vcall_source_loc));
378 
379  // No definition for this type; shouldn't be possible...
380  t1->source_location.set_comment(
381  "cannot find calls for " +
382  id2string(code.function().get(ID_identifier)) + " dispatching " +
383  id2string(fun.class_id));
384 
385  insertit.first->second = t1;
386  }
387 
388  // goto final
389  new_code_calls.add(
390  goto_programt::make_goto(t_final, true_exprt(), vcall_source_loc));
391  }
392 
393  // Fall through to the default callee if possible:
394  if(
395  fallback_action ==
397  fun.symbol_expr.has_value() == last_function_symbol.has_value() &&
398  (!fun.symbol_expr.has_value() ||
399  *fun.symbol_expr == *last_function_symbol))
400  {
401  // Nothing to do
402  }
403  else
404  {
405  const constant_exprt fun_class_identifier(fun.class_id, string_typet());
406  const equal_exprt class_id_test(
407  fun_class_identifier, this_class_identifier);
408 
409  // If the previous GOTO goes to the same callee, join it
410  // (e.g. turning IF x GOTO y into IF x || z GOTO y)
411  if(
412  it != functions.crbegin() &&
413  std::prev(it)->symbol_expr.has_value() == fun.symbol_expr.has_value() &&
414  (!fun.symbol_expr.has_value() ||
415  *(std::prev(it)->symbol_expr) == *fun.symbol_expr))
416  {
417  INVARIANT(
418  !new_code_gotos.empty(),
419  "a dispatch table entry has been processed already, "
420  "which should have created a GOTO");
421  new_code_gotos.instructions.back().guard =
422  or_exprt(new_code_gotos.instructions.back().guard, class_id_test);
423  }
424  else
425  {
426  new_code_gotos.add(goto_programt::make_goto(
427  insertit.first->second, class_id_test, vcall_source_loc));
428  }
429  }
430  }
431 
432  goto_programt new_code;
433 
434  // patch them all together
435  new_code.destructive_append(new_code_for_this_argument);
436  new_code.destructive_append(new_code_gotos);
437  new_code.destructive_append(new_code_calls);
438  new_code.destructive_append(final_skip);
439 
440  // set locations
441  for(auto &instruction : new_code.instructions)
442  {
443  source_locationt &source_location = instruction.source_location;
444 
445  const irep_idt property_class = source_location.get_property_class();
446  const irep_idt comment = source_location.get_comment();
447  source_location = target->source_location;
448  if(!property_class.empty())
449  source_location.set_property_class(property_class);
450  if(!comment.empty())
451  source_location.set_comment(comment);
452  }
453 
454  goto_program.destructive_insert(next_target, new_code);
455 
456  // finally, kill original invocation
457  target->turn_into_skip();
458 
459  // only remove skips within the virtual-function handling block
460  remove_skip(goto_program, target, next_target);
461 
462  return next_target;
463 }
464 
475  const irep_idt &function_id,
476  goto_programt &goto_program,
477  goto_programt::targett target)
478 {
479  const exprt &function = as_const(*target).call_function();
480  INVARIANT(
482  "remove_virtual_function must take a function call instruction whose "
483  "function is a class method descriptor ");
484  INVARIANT(
485  !as_const(*target).call_arguments().empty(),
486  "virtual function calls must have at least a this-argument");
487 
489  dispatch_table_entriest functions;
490  get_callees.get_functions(function, functions);
491 
493  symbol_table,
494  function_id,
495  goto_program,
496  target,
497  functions,
499 }
500 
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) const
520 {
521  auto findit=class_hierarchy.class_map.find(this_id);
522  if(findit==class_hierarchy.class_map.end())
523  return;
524 
525  for(const auto &child : findit->second.children)
526  {
527  // Skip if we have already visited this and we found a function call that
528  // did not resolve to non java.lang.Object.
529  auto it = entry_map.find(child);
530  if(
531  it != entry_map.end() &&
532  (!it->second.symbol_expr.has_value() ||
533  !has_prefix(
534  id2string(it->second.symbol_expr->get_identifier()),
535  "java::java.lang.Object")))
536  {
537  continue;
538  }
539  exprt method = get_method(child, component_name);
540  dispatch_table_entryt function(child);
541  if(method.is_not_nil())
542  {
543  function.symbol_expr=to_symbol_expr(method);
544  function.symbol_expr->set(ID_C_class, child);
545  }
546  else
547  {
548  function.symbol_expr=last_method_defn;
549  }
550  if(!function.symbol_expr.has_value())
551  {
552  const auto resolved_call = get_inherited_method_implementation(
553  component_name, child, symbol_table);
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, function.symbol_expr, component_name, functions, entry_map);
570  }
571 }
572 
578  const exprt &function,
579  dispatch_table_entriest &functions) const
580 {
581  // class part of function to call
582  const irep_idt class_id=function.get(ID_C_class);
583  const std::string class_id_string(id2string(class_id));
584  const irep_idt function_name = function.get(ID_component_name);
585  const std::string function_name_string(id2string(function_name));
586  INVARIANT(!class_id.empty(), "All virtual functions must have a class");
587 
588  auto resolved_call =
589  get_inherited_method_implementation(function_name, class_id, symbol_table);
590 
591  // might be an abstract function
592  dispatch_table_entryt root_function(class_id);
593 
594  if(resolved_call)
595  {
596  root_function.class_id = resolved_call->get_class_identifier();
597 
598  const symbolt &called_symbol =
599  symbol_table.lookup_ref(resolved_call->get_full_component_identifier());
600 
601  root_function.symbol_expr=called_symbol.symbol_expr();
602  root_function.symbol_expr->set(
603  ID_C_class, resolved_call->get_class_identifier());
604  }
605 
606  // iterate over all children, transitively
607  dispatch_table_entries_mapt entry_map;
609  class_id, root_function.symbol_expr, function_name, functions, entry_map);
610 
611  if(root_function.symbol_expr.has_value())
612  functions.push_back(root_function);
613 
614  // Sort for the identifier of the function call symbol expression, grouping
615  // together calls to the same function. Keep java.lang.Object entries at the
616  // end for fall through. The reasoning is that this is the case with most
617  // entries in realistic cases.
618  std::sort(
619  functions.begin(),
620  functions.end(),
621  [](const dispatch_table_entryt &a, const dispatch_table_entryt &b) {
622  irep_idt a_id = a.symbol_expr.has_value()
623  ? a.symbol_expr->get_identifier()
624  : irep_idt();
625  irep_idt b_id = b.symbol_expr.has_value()
626  ? b.symbol_expr->get_identifier()
627  : irep_idt();
628 
629  if(has_prefix(id2string(a_id), "java::java.lang.Object"))
630  return false;
631  else if(has_prefix(id2string(b_id), "java::java.lang.Object"))
632  return true;
633  else
634  {
635  int cmp = a_id.compare(b_id);
636  if(cmp == 0)
637  return a.class_id < b.class_id;
638  else
639  return cmp < 0;
640  }
641  });
642 }
643 
650  const irep_idt &class_id,
651  const irep_idt &component_name) const
652 {
653  const irep_idt &id=
655  class_id, component_name);
656 
657  const symbolt *symbol;
658  if(ns.lookup(id, symbol))
659  return nil_exprt();
660 
661  return symbol->symbol_expr();
662 }
663 
668  const irep_idt &function_id,
669  goto_programt &goto_program)
670 {
671  bool did_something=false;
672 
673  for(goto_programt::instructionst::iterator
674  target = goto_program.instructions.begin();
675  target != goto_program.instructions.end();
676  ) // remove_virtual_function returns the next instruction to process
677  {
678  if(target->is_function_call())
679  {
681  as_const(*target).call_function()))
682  {
683  target = remove_virtual_function(function_id, goto_program, target);
684  did_something=true;
685  continue;
686  }
687  }
688 
689  ++target;
690  }
691 
692  if(did_something)
693  goto_program.update();
694 
695  return did_something;
696 }
697 
701 {
702  bool did_something=false;
703 
704  for(goto_functionst::function_mapt::iterator f_it=
705  functions.function_map.begin();
706  f_it!=functions.function_map.end();
707  f_it++)
708  {
709  const irep_idt &function_id = f_it->first;
710  goto_programt &goto_program=f_it->second.body;
711 
712  if(remove_virtual_functions(function_id, goto_program))
713  did_something=true;
714  }
715 
716  if(did_something)
717  functions.compute_location_numbers();
718 }
719 
725  symbol_table_baset &symbol_table,
726  goto_functionst &goto_functions)
727 {
728  class_hierarchyt class_hierarchy;
729  class_hierarchy(symbol_table);
730  remove_virtual_functionst rvf(symbol_table, class_hierarchy);
731  rvf(goto_functions);
732 }
733 
742  symbol_table_baset &symbol_table,
743  goto_functionst &goto_functions,
744  const class_hierarchyt &class_hierarchy)
745 {
746  remove_virtual_functionst rvf(symbol_table, class_hierarchy);
747  rvf(goto_functions);
748 }
749 
753 {
755  goto_model.symbol_table, goto_model.goto_functions);
756 }
757 
764  goto_modelt &goto_model,
765  const class_hierarchyt &class_hierarchy)
766 {
768  goto_model.symbol_table, goto_model.goto_functions, class_hierarchy);
769 }
770 
776 {
777  class_hierarchyt class_hierarchy;
778  class_hierarchy(function.get_symbol_table());
779  remove_virtual_functionst rvf(function.get_symbol_table(), class_hierarchy);
781  function.get_function_id(), function.get_goto_function().body);
782 }
783 
792  goto_model_functiont &function,
793  const class_hierarchyt &class_hierarchy)
794 {
795  remove_virtual_functionst rvf(function.get_symbol_table(), class_hierarchy);
797  function.get_function_id(), function.get_goto_function().body);
798 }
799 
819  symbol_tablet &symbol_table,
820  const irep_idt &function_id,
821  goto_programt &goto_program,
822  goto_programt::targett instruction,
823  const dispatch_table_entriest &dispatch_table,
824  virtual_dispatch_fallback_actiont fallback_action)
825 {
827  symbol_table,
828  function_id,
829  goto_program,
830  instruction,
831  dispatch_table,
832  fallback_action);
833 
834  goto_program.update();
835 
836  return next;
837 }
838 
840  goto_modelt &goto_model,
841  const irep_idt &function_id,
842  goto_programt &goto_program,
843  goto_programt::targett instruction,
844  const dispatch_table_entriest &dispatch_table,
845  virtual_dispatch_fallback_actiont fallback_action)
846 {
848  goto_model.symbol_table,
849  function_id,
850  goto_program,
851  instruction,
852  dispatch_table,
853  fallback_action);
854 }
855 
857  const exprt &function,
858  const symbol_table_baset &symbol_table,
859  const class_hierarchyt &class_hierarchy,
860  dispatch_table_entriest &overridden_functions)
861 {
862  get_virtual_calleest get_callees(symbol_table, class_hierarchy);
863  get_callees.get_functions(function, overridden_functions);
864 }
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
std::set< irep_idt > get_callees(const call_grapht::directed_grapht &graph, const irep_idt &function)
Get functions directly callable from a given function.
Class Hierarchy.
exprt get_class_identifier_field(const exprt &this_expr_in, const struct_tag_typet &suggested_type, const namespacet &ns)
Extract class identifier.
Non-graph-based representation of the class hierarchy.
class_mapt class_map
codet representation of a function call statement.
Definition: std_code.h:1213
exprt & function()
Definition: std_code.h:1248
argumentst & arguments()
Definition: std_code.h:1258
const parameterst & parameters() const
Definition: std_types.h:655
A constant literal expression.
Definition: std_expr.h:2753
optionalt< symbol_exprt > symbol_expr
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
The empty type.
Definition: std_types.h:51
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
depth_iteratort depth_end()
Definition: expr.cpp:267
depth_iteratort depth_begin()
Definition: expr.cpp:265
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2811
const symbol_table_baset & symbol_table
void get_child_functions_rec(const irep_idt &, const optionalt< symbol_exprt > &, const irep_idt &, dispatch_table_entriest &, dispatch_table_entries_mapt &) const
Used by get_functions to track the most-derived parent that provides an override of a given function.
get_virtual_calleest(const symbol_table_baset &_symbol_table, const class_hierarchyt &_class_hierarchy)
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.
void get_functions(const exprt &, dispatch_table_entriest &) const
Used to get dispatch entries to call for the given function.
const class_hierarchyt & class_hierarchy
std::function< optionalt< resolve_inherited_componentt::inherited_componentt > const irep_idt &, const irep_idt &)> function_call_resolvert
A collection of goto functions.
function_mapt function_map
void compute_location_numbers()
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:963
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
void update()
Update all indices.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:744
instructionst::iterator targett
Definition: goto_program.h:646
instructionst::const_iterator const_targett
Definition: goto_program.h:647
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:736
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:909
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:753
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
bool empty() const
Is the program empty?
Definition: goto_program.h:826
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:978
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:951
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:706
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The NIL expression.
Definition: std_expr.h:2820
Boolean OR.
Definition: std_expr.h:2028
remove_virtual_functionst(symbol_table_baset &_symbol_table, const class_hierarchyt &_class_hierarchy)
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...
void operator()(goto_functionst &functions)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
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.
const class_hierarchyt & class_hierarchy
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...
void set_comment(const irep_idt &comment)
const irep_idt & get_comment() const
void set_property_class(const irep_idt &property_class)
const irep_idt & get_property_class() const
String type.
Definition: std_types.h:880
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
The symbol table base class interface.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
irep_idt mode
Language mode.
Definition: symbol.h:49
The Boolean constant true.
Definition: std_expr.h:2802
Semantic type conversion.
Definition: std_expr.h:1866
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
Forward depth-first search iterators These iterators' copy operations are expensive,...
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:137
Deprecated expression utility functions.
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 ...
Fresh auxiliary symbol creation.
Symbol Table + CFG.
@ ASSERT
Definition: goto_program.h:34
@ ASSUME
Definition: goto_program.h:33
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
nonstd::optional< T > optionalt
Definition: optional.h:35
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
Program Transformation.
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...
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...
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.
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.
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...
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...
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...
Functions for replacing virtual function call with a static function calls in functions,...
std::map< irep_idt, dispatch_table_entryt > dispatch_table_entries_mapt
virtual_dispatch_fallback_actiont
Specifies remove_virtual_function's behaviour when the actual supplied parameter does not match any o...
@ ASSUME_FALSE
When no callee type matches, ASSUME false, thus preventing any complete trace from using this path.
@ CALL_LAST_FUNCTION
When no callee type matches, call the last passed function, which is expected to be some safe default...
std::vector< dispatch_table_entryt > dispatch_table_entriest
optionalt< resolve_inherited_componentt::inherited_componentt > get_inherited_method_implementation(const irep_idt &call_basename, const irep_idt &classname, const symbol_tablet &symbol_table)
Given a class and a component, identify the concrete method it is resolved to.
Given a class and a component (either field or method), find the closest parent that defines that com...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
bool can_cast_expr< class_method_descriptor_exprt >(const exprt &base)
Definition: std_expr.h:3318
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
Author: Diffblue Ltd.