Go to the documentation of this file.
50 typedef std::function<
70 symbol_table(_symbol_table),
71 class_hierarchy(_class_hierarchy)
91 function.
id()==ID_virtual_function,
92 "remove_virtual_function must take a virtual function call instruction");
95 "virtual function calls must have at least a this-argument");
118 const auto &callee_type =
122 this_param !=
nullptr,
123 "Virtual function callees must have a `this` argument");
126 call.
arguments()[0].make_typecast(need_type);
151 target->is_function_call(),
152 "remove_virtual_function must target a FUNCTION_CALL instruction");
158 if(functions.empty())
166 if(functions.size()==1 &&
182 const auto &vcall_source_loc=target->source_location;
188 t_final->source_location=vcall_source_loc;
190 t_final->make_skip();
198 const auto &last_function_symbol=functions.back().symbol_expr;
201 INVARIANT(this_type.
id() == ID_pointer,
"this parameter must be a pointer");
204 "this parameter must not be a void pointer");
208 exprt this_class_identifier =
217 newinst->source_location=vcall_source_loc;
221 INVARIANT(!functions.empty(),
"Function dispatch table cannot be empty.");
223 std::map<irep_idt, goto_programt::targett> calls;
225 for(
auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it)
228 auto insertit=calls.insert(
235 t1->source_location=vcall_source_loc;
236 if(!fun.symbol_expr.get_identifier().empty())
239 t1->make_function_call(code);
247 t1->source_location.set_comment(
248 "cannot find calls for " +
252 insertit.first->second=t1;
255 t3->source_location=vcall_source_loc;
260 if(fallback_action ==
262 fun.symbol_expr == last_function_symbol)
270 fun_class_identifier, this_class_identifier);
274 if(it != functions.crbegin() &&
275 std::prev(it)->symbol_expr == fun.symbol_expr)
278 !new_code_gotos.
empty(),
279 "a dispatch table entry has been processed already, "
280 "which should have created a GOTO");
287 new_goto->source_location = vcall_source_loc;
288 new_goto->make_goto(insertit.first->second, class_id_test);
303 const irep_idt property_class=it->source_location.get_property_class();
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);
310 it->source_location.set_comment(
comment);
350 for(
const auto &child : findit->second.children)
354 auto it = entry_map.find(child);
356 it != entry_map.end() &&
358 id2string(it->second.symbol_expr.get_identifier()),
359 "java::java.lang.Object"))
368 function.symbol_expr.set(ID_C_class, child);
372 function.symbol_expr=last_method_defn;
377 &resolved_call = resolve_function_call(child, component_name);
386 function.symbol_expr.
set(
390 functions.push_back(
function);
391 entry_map.insert({child,
function});
395 function.symbol_expr,
399 resolve_function_call);
408 const exprt &
function,
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");
421 [&get_virtual_call_target](
423 return get_virtual_call_target(class_id, function_name,
false);
427 &resolved_call = get_virtual_call_target(class_id, function_name,
false);
456 resolve_function_call);
459 functions.push_back(root_function);
472 id2string(a.symbol_expr.get_identifier()),
"java::java.lang.Object"))
476 id2string(b.symbol_expr.get_identifier()),
"java::java.lang.Object"))
480 int cmp = a.symbol_expr.get_identifier().compare(
481 b.symbol_expr.get_identifier());
483 return a.class_id < b.class_id;
497 const irep_idt &component_name)
const
501 class_id, component_name);
516 bool did_something=
false;
518 for(goto_programt::instructionst::iterator
523 if(target->is_function_call())
542 return did_something;
549 bool did_something=
false;
551 for(goto_functionst::function_mapt::iterator f_it=
573 class_hierarchy(symbol_table);
589 class_hierarchy(
function.get_symbol_table());
618 class_hierarchy(symbol_table);
622 goto_program, instruction, dispatch_table, fallback_action);
645 const exprt &
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...
#define Forall_goto_program_instructions(it, program)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
@ 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
Specifies remove_virtual_function's behaviour when the actual supplied parameter does not match any o...
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const typet & subtype() const
Non-graph-based representation of the class hierarchy.
bool is_valid() const
Use to check if this inherited_componentt has been fully constructed.
std::string comment(const rw_set_baset::entryt &entry, bool write)
@ ASSUME_FALSE
When no callee type matches, ASSUME false, thus preventing any complete trace from using this path.
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.
The type of an expression, extends irept.
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...
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
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.
exprt get_class_identifier_field(const exprt &this_expr_in, const struct_tag_typet &suggested_type, const namespacet &ns)
void update()
Update all indices.
void compute_location_numbers()
bool empty() const
Is the program empty?
Base class for all expressions.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
irep_idt get_full_component_identifier() const
Get the full name of this function.
A struct tag type, i.e., struct_typet with an identifier.
std::vector< dispatch_table_entryt > dispatch_table_entriest
function_mapt function_map
Expression to hold a symbol (variable)
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...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
targett add_instruction()
Adds an instruction at the end.
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality at the top level.
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 destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
const std::string & id2string(const irep_idt &d)
const irep_idt & get_identifier() const
The symbol table base class interface.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
std::map< irep_idt, dispatch_table_entryt > dispatch_table_entries_mapt
const code_function_callt & to_code_function_call(const codet &code)
The Boolean constant false.
void get_functions(const exprt &, dispatch_table_entriest &)
Used to get dispatch entries to call for the given function.
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
irep_idt get_class_identifier() const
const symbol_table_baset & symbol_table
instructionst instructions
The list of instructions in the goto program.
A collection of goto functions.
std::function< resolve_inherited_componentt::inherited_componentt(const irep_idt &, const irep_idt &)> function_call_resolvert
goto_functionst goto_functions
GOTO functions.
remove_virtual_functionst(const symbol_table_baset &_symbol_table, const class_hierarchyt &_class_hierarchy)
const irep_idt & get(const irep_namet &name) const
void operator()(goto_functionst &goto_functions)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
void set(const irep_namet &name, const irep_idt &value)
A generic container class for the GOTO intermediate representation of one function.
bool has_prefix(const std::string &s, const std::string &prefix)
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...
The Boolean constant true.
A constant literal expression.
void collect_virtual_function_callees(const exprt &function, const symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, dispatch_table_entriest &overridden_functions)
symbol_tablet symbol_table
Symbol table.
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
const class_hierarchyt & class_hierarchy
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...
instructionst::iterator targett