cprover
Loading...
Searching...
No Matches
remove_virtual_functions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Remove Virtual Function (Method) Calls
4
5Author: 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/pointer_expr.h>
19#include <util/prefix.h>
20
21#include "class_hierarchy.h"
22#include "class_identifier.h"
23#include "goto_model.h"
24#include "remove_skip.h"
26
28{
29public:
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
41private:
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{
64public:
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
80private:
84
86 const irep_idt &function_id,
87 goto_programt &goto_program,
89};
90
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
147 const goto_programt &goto_program,
149 const exprt &argument_for_this,
150 const symbol_exprt &temp_var_for_this,
151 const source_locationt &vcall_source_loc)
152{
153 goto_programt checks_directly_preceding_function_call;
154
155 while(instr_it != goto_program.instructions.cbegin())
156 {
157 instr_it = std::prev(instr_it);
158
159 if(instr_it->is_assert())
160 {
161 continue;
162 }
163
164 if(!instr_it->is_assume())
165 {
166 break;
167 }
168
169 exprt guard = instr_it->condition();
170
171 bool changed = false;
172 for(auto expr_it = guard.depth_begin(); expr_it != guard.depth_end();
173 ++expr_it)
174 {
175 if(*expr_it == argument_for_this)
176 {
177 expr_it.mutate() = temp_var_for_this;
178 changed = true;
179 }
180 }
181
182 if(changed)
183 {
184 checks_directly_preceding_function_call.insert_before(
185 checks_directly_preceding_function_call.instructions.cbegin(),
186 goto_programt::make_assumption(guard, vcall_source_loc));
187 }
188 }
189
190 return checks_directly_preceding_function_call;
191}
192
205 const irep_idt &function_id,
206 const goto_programt &goto_program,
207 const goto_programt::targett target,
208 exprt &argument_for_this,
209 symbol_table_baset &symbol_table,
210 const source_locationt &vcall_source_loc,
211 goto_programt &new_code_for_this_argument)
212{
213 if(has_subexpr(argument_for_this, ID_dereference))
214 {
215 // Create a temporary for the `this` argument. This is so that
216 // \ref goto_symext::try_filter_value_sets can reduce the value-set for
217 // `this` to those elements with the correct class identifier.
218 symbolt &temp_symbol = get_fresh_aux_symbol(
219 argument_for_this.type(),
220 id2string(function_id),
221 "this_argument",
222 vcall_source_loc,
223 symbol_table.lookup_ref(function_id).mode,
224 symbol_table);
225 const symbol_exprt temp_var_for_this = temp_symbol.symbol_expr();
226
227 new_code_for_this_argument.add(
228 goto_programt::make_decl(temp_var_for_this, vcall_source_loc));
229 new_code_for_this_argument.add(
231 temp_var_for_this, argument_for_this, vcall_source_loc));
232
233 goto_programt checks_directly_preceding_function_call =
235 goto_program,
236 target,
237 argument_for_this,
238 temp_var_for_this,
239 vcall_source_loc);
240
241 new_code_for_this_argument.destructive_append(
242 checks_directly_preceding_function_call);
243
244 argument_for_this = temp_var_for_this;
245 }
246}
247
267 symbol_table_baset &symbol_table,
268 const irep_idt &function_id,
269 goto_programt &goto_program,
271 const dispatch_table_entriest &functions,
272 virtual_dispatch_fallback_actiont fallback_action)
273{
274 INVARIANT(
275 target->is_function_call(),
276 "remove_virtual_function must target a FUNCTION_CALL instruction");
277
278 namespacet ns(symbol_table);
279 goto_programt::targett next_target = std::next(target);
280
281 if(functions.empty())
282 {
283 target->turn_into_skip();
284 remove_skip(goto_program, target, next_target);
285 return next_target; // give up
286 }
287
288 // only one option?
289 if(functions.size()==1 &&
291 {
292 if(!functions.front().symbol_expr.has_value())
293 {
294 target->turn_into_skip();
295 remove_skip(goto_program, target, next_target);
296 }
297 else
298 {
299 auto c = code_function_callt(
300 target->call_lhs(), target->call_function(), target->call_arguments());
301 create_static_function_call(c, *functions.front().symbol_expr, ns);
302 target->call_function() = c.function();
303 target->call_arguments() = c.arguments();
304 }
305 return next_target;
306 }
307
308 const auto &vcall_source_loc = target->source_location();
309
311 target->call_lhs(), target->call_function(), target->call_arguments());
312 goto_programt new_code_for_this_argument;
313
315 function_id,
316 goto_program,
317 target,
318 code.arguments()[0],
319 symbol_table,
320 vcall_source_loc,
321 new_code_for_this_argument);
322
323 const exprt &this_expr = code.arguments()[0];
324
325 // Create a skip as the final target for each branch to jump to at the end
326 goto_programt final_skip;
327
328 goto_programt::targett t_final =
329 final_skip.add(goto_programt::make_skip(vcall_source_loc));
330
331 // build the calls and gotos
332
333 goto_programt new_code_calls;
334 goto_programt new_code_gotos;
335
336 INVARIANT(
337 this_expr.type().id() == ID_pointer, "this parameter must be a pointer");
338 INVARIANT(
339 to_pointer_type(this_expr.type()).base_type() != empty_typet(),
340 "this parameter must not be a void pointer");
341
342 // So long as `this` is already not `void*` typed, the second parameter
343 // is ignored:
344 exprt this_class_identifier =
346
347 // If instructed, add an ASSUME(FALSE) to handle the case where we don't
348 // match any expected type:
350 {
351 new_code_calls.add(
352 goto_programt::make_assumption(false_exprt(), vcall_source_loc));
353 }
354
355 // get initial identifier for grouping
356 INVARIANT(!functions.empty(), "Function dispatch table cannot be empty.");
357 const auto &last_function_symbol = functions.back().symbol_expr;
358
359 std::map<irep_idt, goto_programt::targett> calls;
360 // Note backwards iteration, to get the fallback candidate first.
361 for(auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it)
362 {
363 const auto &fun=*it;
364 irep_idt id_or_empty = fun.symbol_expr.has_value()
365 ? fun.symbol_expr->get_identifier()
366 : irep_idt();
367 auto insertit = calls.insert({id_or_empty, goto_programt::targett()});
368
369 // Only create one call sequence per possible target:
370 if(insertit.second)
371 {
372 if(fun.symbol_expr.has_value())
373 {
374 // call function
375 auto new_call = code;
376
377 create_static_function_call(new_call, *fun.symbol_expr, ns);
378
379 goto_programt::targett t1 = new_code_calls.add(
380 goto_programt::make_function_call(new_call, vcall_source_loc));
381
382 insertit.first->second = t1;
383 }
384 else
385 {
386 source_locationt annotated_location = vcall_source_loc;
387 // No definition for this type; shouldn't be possible...
388 annotated_location.set_comment(
389 "cannot find calls for " +
390 id2string(code.function().get(ID_identifier)) + " dispatching " +
391 id2string(fun.class_id));
392 insertit.first->second = new_code_calls.add(
393 goto_programt::make_assertion(false_exprt(), annotated_location));
394 }
395
396 // goto final
397 new_code_calls.add(
398 goto_programt::make_goto(t_final, true_exprt(), vcall_source_loc));
399 }
400
401 // Fall through to the default callee if possible:
402 if(
403 fallback_action ==
405 fun.symbol_expr.has_value() == last_function_symbol.has_value() &&
406 (!fun.symbol_expr.has_value() ||
407 *fun.symbol_expr == *last_function_symbol))
408 {
409 // Nothing to do
410 }
411 else
412 {
413 const constant_exprt fun_class_identifier(fun.class_id, string_typet());
414 const equal_exprt class_id_test(
415 fun_class_identifier, this_class_identifier);
416
417 // If the previous GOTO goes to the same callee, join it
418 // (e.g. turning IF x GOTO y into IF x || z GOTO y)
419 if(
420 it != functions.crbegin() &&
421 std::prev(it)->symbol_expr.has_value() == fun.symbol_expr.has_value() &&
422 (!fun.symbol_expr.has_value() ||
423 *(std::prev(it)->symbol_expr) == *fun.symbol_expr))
424 {
425 INVARIANT(
426 !new_code_gotos.empty(),
427 "a dispatch table entry has been processed already, "
428 "which should have created a GOTO");
429 new_code_gotos.instructions.back().condition_nonconst() = or_exprt(
430 new_code_gotos.instructions.back().condition(), class_id_test);
431 }
432 else
433 {
434 new_code_gotos.add(goto_programt::make_goto(
435 insertit.first->second, class_id_test, vcall_source_loc));
436 }
437 }
438 }
439
440 goto_programt new_code;
441
442 // patch them all together
443 new_code.destructive_append(new_code_for_this_argument);
444 new_code.destructive_append(new_code_gotos);
445 new_code.destructive_append(new_code_calls);
446 new_code.destructive_append(final_skip);
447
448 goto_program.destructive_insert(next_target, new_code);
449
450 // finally, kill original invocation
451 target->turn_into_skip();
452
453 // only remove skips within the virtual-function handling block
454 remove_skip(goto_program, target, next_target);
455
456 return next_target;
457}
458
469 const irep_idt &function_id,
470 goto_programt &goto_program,
472{
473 const exprt &function = as_const(*target).call_function();
474 INVARIANT(
476 "remove_virtual_function must take a function call instruction whose "
477 "function is a class method descriptor ");
478 INVARIANT(
479 !as_const(*target).call_arguments().empty(),
480 "virtual function calls must have at least a this-argument");
481
483 dispatch_table_entriest functions;
484 get_callees.get_functions(function, functions);
485
488 function_id,
489 goto_program,
490 target,
491 functions,
493}
494
509 const irep_idt &this_id,
510 const optionalt<symbol_exprt> &last_method_defn,
511 const irep_idt &component_name,
512 dispatch_table_entriest &functions,
513 dispatch_table_entries_mapt &entry_map) const
514{
515 auto findit=class_hierarchy.class_map.find(this_id);
516 if(findit==class_hierarchy.class_map.end())
517 return;
518
519 for(const auto &child : findit->second.children)
520 {
521 // Skip if we have already visited this and we found a function call that
522 // did not resolve to non java.lang.Object.
523 auto it = entry_map.find(child);
524 if(
525 it != entry_map.end() &&
526 (!it->second.symbol_expr.has_value() ||
527 !has_prefix(
528 id2string(it->second.symbol_expr->get_identifier()),
529 "java::java.lang.Object")))
530 {
531 continue;
532 }
533 exprt method = get_method(child, component_name);
534 dispatch_table_entryt function(child);
535 if(method.is_not_nil())
536 {
537 function.symbol_expr=to_symbol_expr(method);
538 function.symbol_expr->set(ID_C_class, child);
539 }
540 else
541 {
542 function.symbol_expr=last_method_defn;
543 }
544 if(!function.symbol_expr.has_value())
545 {
546 const auto resolved_call = get_inherited_method_implementation(
547 component_name, child, symbol_table);
548 if(resolved_call)
549 {
550 function.class_id = resolved_call->get_class_identifier();
551 const symbolt &called_symbol = symbol_table.lookup_ref(
552 resolved_call->get_full_component_identifier());
553
554 function.symbol_expr = called_symbol.symbol_expr();
555 function.symbol_expr->set(
556 ID_C_class, resolved_call->get_class_identifier());
557 }
558 }
559 functions.push_back(function);
560 entry_map.emplace(child, function);
561
563 child, function.symbol_expr, component_name, functions, entry_map);
564 }
565}
566
572 const exprt &function,
573 dispatch_table_entriest &functions) const
574{
575 // class part of function to call
576 const irep_idt class_id=function.get(ID_C_class);
577 const std::string class_id_string(id2string(class_id));
578 const irep_idt function_name = function.get(ID_component_name);
579 const std::string function_name_string(id2string(function_name));
580 INVARIANT(!class_id.empty(), "All virtual functions must have a class");
581
582 auto resolved_call =
583 get_inherited_method_implementation(function_name, class_id, symbol_table);
584
585 // might be an abstract function
586 dispatch_table_entryt root_function(class_id);
587
588 if(resolved_call)
589 {
590 root_function.class_id = resolved_call->get_class_identifier();
591
592 const symbolt &called_symbol =
593 symbol_table.lookup_ref(resolved_call->get_full_component_identifier());
594
595 root_function.symbol_expr=called_symbol.symbol_expr();
596 root_function.symbol_expr->set(
597 ID_C_class, resolved_call->get_class_identifier());
598 }
599
600 // iterate over all children, transitively
603 class_id, root_function.symbol_expr, function_name, functions, entry_map);
604
605 if(root_function.symbol_expr.has_value())
606 functions.push_back(root_function);
607
608 // Sort for the identifier of the function call symbol expression, grouping
609 // together calls to the same function. Keep java.lang.Object entries at the
610 // end for fall through. The reasoning is that this is the case with most
611 // entries in realistic cases.
612 std::sort(
613 functions.begin(),
614 functions.end(),
615 [](const dispatch_table_entryt &a, const dispatch_table_entryt &b) {
616 irep_idt a_id = a.symbol_expr.has_value()
617 ? a.symbol_expr->get_identifier()
618 : irep_idt();
619 irep_idt b_id = b.symbol_expr.has_value()
620 ? b.symbol_expr->get_identifier()
621 : irep_idt();
622
623 if(has_prefix(id2string(a_id), "java::java.lang.Object"))
624 return false;
625 else if(has_prefix(id2string(b_id), "java::java.lang.Object"))
626 return true;
627 else
628 {
629 int cmp = a_id.compare(b_id);
630 if(cmp == 0)
631 return a.class_id < b.class_id;
632 else
633 return cmp < 0;
634 }
635 });
636}
637
644 const irep_idt &class_id,
645 const irep_idt &component_name) const
646{
647 const irep_idt &id=
649 class_id, component_name);
650
651 const symbolt *symbol;
652 if(ns.lookup(id, symbol))
653 return nil_exprt();
654
655 return symbol->symbol_expr();
656}
657
662 const irep_idt &function_id,
663 goto_programt &goto_program)
664{
665 bool did_something=false;
666
667 for(goto_programt::instructionst::iterator
668 target = goto_program.instructions.begin();
669 target != goto_program.instructions.end();
670 ) // remove_virtual_function returns the next instruction to process
671 {
672 if(target->is_function_call())
673 {
675 as_const(*target).call_function()))
676 {
677 target = remove_virtual_function(function_id, goto_program, target);
678 did_something=true;
679 continue;
680 }
681 }
682
683 ++target;
684 }
685
686 if(did_something)
687 goto_program.update();
688
689 return did_something;
690}
691
695{
696 bool did_something=false;
697
698 for(goto_functionst::function_mapt::iterator f_it=
699 functions.function_map.begin();
700 f_it!=functions.function_map.end();
701 f_it++)
702 {
703 const irep_idt &function_id = f_it->first;
704 goto_programt &goto_program=f_it->second.body;
705
706 if(remove_virtual_functions(function_id, goto_program))
707 did_something=true;
708 }
709
710 if(did_something)
711 functions.compute_location_numbers();
712}
713
719 symbol_table_baset &symbol_table,
720 goto_functionst &goto_functions)
721{
722 class_hierarchyt class_hierarchy;
723 class_hierarchy(symbol_table);
724 remove_virtual_functionst rvf(symbol_table, class_hierarchy);
725 rvf(goto_functions);
726}
727
736 symbol_table_baset &symbol_table,
737 goto_functionst &goto_functions,
738 const class_hierarchyt &class_hierarchy)
739{
740 remove_virtual_functionst rvf(symbol_table, class_hierarchy);
741 rvf(goto_functions);
742}
743
747{
749 goto_model.symbol_table, goto_model.goto_functions);
750}
751
758 goto_modelt &goto_model,
759 const class_hierarchyt &class_hierarchy)
760{
762 goto_model.symbol_table, goto_model.goto_functions, class_hierarchy);
763}
764
770{
771 class_hierarchyt class_hierarchy;
772 class_hierarchy(function.get_symbol_table());
773 remove_virtual_functionst rvf(function.get_symbol_table(), class_hierarchy);
775 function.get_function_id(), function.get_goto_function().body);
776}
777
786 goto_model_functiont &function,
787 const class_hierarchyt &class_hierarchy)
788{
789 remove_virtual_functionst rvf(function.get_symbol_table(), class_hierarchy);
791 function.get_function_id(), function.get_goto_function().body);
792}
793
813 symbol_table_baset &symbol_table,
814 const irep_idt &function_id,
815 goto_programt &goto_program,
816 goto_programt::targett instruction,
817 const dispatch_table_entriest &dispatch_table,
818 virtual_dispatch_fallback_actiont fallback_action)
819{
821 symbol_table,
822 function_id,
823 goto_program,
824 instruction,
825 dispatch_table,
826 fallback_action);
827
828 goto_program.update();
829
830 return next;
831}
832
834 goto_modelt &goto_model,
835 const irep_idt &function_id,
836 goto_programt &goto_program,
837 goto_programt::targett instruction,
838 const dispatch_table_entriest &dispatch_table,
839 virtual_dispatch_fallback_actiont fallback_action)
840{
842 goto_model.symbol_table,
843 function_id,
844 goto_program,
845 instruction,
846 dispatch_table,
847 fallback_action);
848}
849
851 const exprt &function,
852 const symbol_table_baset &symbol_table,
853 const class_hierarchyt &class_hierarchy,
854 dispatch_table_entriest &overridden_functions)
855{
856 get_virtual_calleest get_callees(symbol_table, class_hierarchy);
857 get_callees.get_functions(function, overridden_functions);
858}
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
static exprt guard(const exprt::operandst &guards, exprt cond)
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.
goto_instruction_codet representation of a function call statement.
const parameterst & parameters() const
Definition std_types.h:655
A constant literal expression.
Definition std_expr.h:2942
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:39
bool empty() const
Definition dstring.h:90
The empty type.
Definition std_types.h:51
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
depth_iteratort depth_end()
Definition expr.cpp:249
depth_iteratort depth_begin()
Definition expr.cpp:247
typet & type()
Return the type of the expression.
Definition expr.h:84
The Boolean constant false.
Definition std_expr.h:3017
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.
std::function< optionalt< resolve_inherited_componentt::inherited_componentt >(const irep_idt &, const irep_idt &)> function_call_resolvert
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
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:190
const irep_idt & get_function_id()
Get function id.
Definition goto_model.h:239
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
Definition goto_model.h:232
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
Definition goto_model.h:225
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
void update()
Update all indices.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
instructionst::iterator targett
instructionst::const_iterator const_targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
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())
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.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
bool empty() const
Is the program empty?
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
bool is_not_nil() const
Definition irep.h:380
const irep_idt & id() const
Definition irep.h:396
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().
The NIL expression.
Definition std_expr.h:3026
Boolean OR.
Definition std_expr.h:2179
const typet & base_type() const
The type of the data what we point to.
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)
String type.
Definition std_types.h:913
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:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
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.
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:3008
Semantic type conversion.
Definition std_expr.h:2017
The type of an expression, extends irept.
Definition type.h:29
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
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.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
nonstd::optional< T > optionalt
Definition optional.h:35
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
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, const source_locationt &vcall_source_loc)
Duplicate ASSUME instructions involving argument_for_this for temp_var_for_this.
goto_programt::targett remove_virtual_function(symbol_table_baset &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...
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...
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_table_baset &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
bool can_cast_expr< class_method_descriptor_exprt >(const exprt &base)
Definition std_expr.h:3548
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
dstringt irep_idt