50 typedef std::function<
70 symbol_table(_symbol_table),
71 class_hierarchy(_class_hierarchy)
84 function.
id()==ID_virtual_function,
85 "remove_virtual_function must take a virtual function call instruction");
88 "virtual function calls must have at least a this-argument");
111 const auto &callee_type =
115 this_param !=
nullptr,
116 "Virtual function callees must have a `this` argument");
119 call.
arguments()[0].make_typecast(need_type);
129 target->is_function_call(),
130 "remove_virtual_function must target a FUNCTION_CALL instruction");
136 if(functions.empty())
144 if(functions.size()==1 &&
160 const auto &vcall_source_loc=target->source_location;
166 t_final->source_location=vcall_source_loc;
168 t_final->make_skip();
175 exprt this_expr=code.arguments()[0];
176 const auto &last_function_symbol=functions.back().symbol_expr;
179 INVARIANT(this_type.
id() == ID_pointer,
"this parameter must be a pointer");
182 "this parameter must not be a void pointer");
186 exprt this_class_identifier =
195 newinst->source_location=vcall_source_loc;
199 INVARIANT(!functions.empty(),
"Function dispatch table cannot be empty.");
201 std::map<irep_idt, goto_programt::targett> calls;
203 for(
auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it)
206 auto insertit=calls.insert(
213 t1->source_location=vcall_source_loc;
214 if(!fun.symbol_expr.get_identifier().empty())
217 t1->make_function_call(code);
225 t1->source_location.set_comment(
226 (
"cannot find calls for " +
227 id2string(code.function().get(ID_identifier)) +
" dispatching " +
230 insertit.first->second=t1;
233 t3->source_location=vcall_source_loc;
238 if(fallback_action ==
240 fun.symbol_expr == last_function_symbol)
248 fun_class_identifier, this_class_identifier);
252 if(it != functions.crbegin() &&
253 std::prev(it)->symbol_expr == fun.symbol_expr)
256 !new_code_gotos.
empty(),
257 "a dispatch table entry has been processed already, " 258 "which should have created a GOTO");
265 new_goto->source_location = vcall_source_loc;
266 new_goto->make_goto(insertit.first->second, class_id_test);
281 const irep_idt property_class=it->source_location.get_property_class();
283 it->source_location=target->source_location;
284 it->function=target->function;
285 if(!property_class.
empty())
286 it->source_location.set_property_class(property_class);
288 it->source_location.set_comment(
comment);
327 for(
const auto &child : findit->second.children)
331 auto it = entry_map.find(child);
333 it != entry_map.end() &&
335 id2string(it->second.symbol_expr.get_identifier()),
336 "java::java.lang.Object"))
345 function.symbol_expr.set(ID_C_class, child);
349 function.symbol_expr=last_method_defn;
354 &resolved_call = resolve_function_call(child, component_name);
363 function.symbol_expr.
set(
367 functions.push_back(
function);
368 entry_map.insert({child,
function});
372 function.symbol_expr,
376 resolve_function_call);
385 const exprt &
function,
389 const irep_idt class_id=
function.get(ID_C_class);
390 const std::string class_id_string(
id2string(class_id));
391 const irep_idt function_name =
function.get(ID_component_name);
392 const std::string function_name_string(
id2string(function_name));
393 INVARIANT(!class_id.
empty(),
"All virtual functions must have a class");
398 [&get_virtual_call_target](
400 return get_virtual_call_target(class_id, function_name,
false);
404 &resolved_call = get_virtual_call_target(class_id, function_name,
false);
433 resolve_function_call);
436 functions.push_back(root_function);
453 id2string(b.symbol_expr.get_identifier()),
"java::java.lang.Object"))
458 b.symbol_expr.get_identifier());
469 const irep_idt &component_name)
const 473 class_id, component_name);
485 bool did_something=
false;
487 for(goto_programt::instructionst::iterator
492 if(target->is_function_call())
511 return did_something;
516 bool did_something=
false;
518 for(goto_functionst::function_mapt::iterator f_it=
538 class_hierarchy(symbol_table);
552 class_hierarchy(
function.get_symbol_table());
565 class_hierarchy(symbol_table);
569 goto_program, instruction, dispatch_table, fallback_action);
592 const exprt &
function,
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
The type of an expression.
void operator()(goto_functionst &goto_functions)
void update()
Update all indices.
const std::string & id2string(const irep_idt &d)
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
void collect_virtual_function_callees(const exprt &function, const symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, dispatch_table_entriest &overridden_functions)
bool remove_virtual_functions(goto_programt &goto_program)
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.
Remove Virtual Function (Method) Calls.
std::string comment(const rw_set_baset::entryt &entry, bool write)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
const irep_idt & get_identifier() const
bool is_valid() const
Use to check if this inherited_componentt has been fully constructed.
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
virtual_dispatch_fallback_actiont
Specifies remove_virtual_function's behaviour when the actual supplied parameter does not match any o...
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
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...
A constant literal expression.
std::function< resolve_inherited_componentt::inherited_componentt(const irep_idt &, const irep_idt &)> function_call_resolvert
void remove_virtual_functions(const symbol_table_baset &symbol_table, goto_functionst &goto_functions)
#define INVARIANT(CONDITION, REASON)
const irep_idt & id() const
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
void compute_location_numbers()
The boolean constant true.
void get_functions(const exprt &, dispatch_table_entriest &)
Used to get dispatch entries to call for the given function.
A reference into the symbol table.
instructionst::iterator targett
std::vector< dispatch_table_entryt > dispatch_table_entriest
const symbol_table_baset & symbol_table
exprt get_method(const irep_idt &class_id, const irep_idt &component_name) const
instructionst instructions
The list of instructions in the goto program.
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...
Given a class and a component (either field or method), find the closest parent that defines that com...
bool has_prefix(const std::string &s, const std::string &prefix)
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
When no callee type matches, call the last passed function, which is expected to be some safe default...
exprt get_class_identifier_field(const exprt &this_expr_in, const symbol_typet &suggested_type, const namespacet &ns)
The boolean constant false.
std::map< irep_idt, dispatch_table_entryt > dispatch_table_entries_mapt
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)
A generic container class for the GOTO intermediate representation of one function.
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
irep_idt get_class_identifier() const
The symbol table base class interface.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
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)
bool empty() const
Is the program empty?
int compare(const dstringt &b) const
goto_programt & goto_program
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
Extract class identifier.
const typet & subtype() const
const class_hierarchyt & class_hierarchy
irep_idt get_full_component_identifier() const
Get the full name of this function.
goto_functionst goto_functions
GOTO functions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void set(const irep_namet &name, const irep_idt &value)
const code_function_callt & to_code_function_call(const codet &code)
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
remove_virtual_functionst(const symbol_table_baset &_symbol_table, const class_hierarchyt &_class_hierarchy)