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.
Non-graph-based representation of the class hierarchy.
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...
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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)