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();
197 exprt this_expr=code.arguments()[0];
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 " +
249 id2string(code.function().get(ID_identifier)) +
" dispatching " +
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);
476 id2string(b.symbol_expr.get_identifier()),
"java::java.lang.Object"))
481 b.symbol_expr.get_identifier());
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,
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality at the top level.
The type of an expression, extends irept.
void operator()(goto_functionst &goto_functions)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
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)
Remove all virtual function calls in a GOTO program and replace them with calls to their most derived...
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.
Functions for replacing virtual function call with a static function calls in functions,...
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 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 p to *this. p is destroyed.
virtual_dispatch_fallback_actiont
Specifies remove_virtual_function's behaviour when the actual supplied parameter does not match any o...
A struct tag type, i.e., struct_typet with an identifier.
function_mapt function_map
typet & type()
Return the type of the expression.
symbol_tablet symbol_table
Symbol table.
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...
exprt get_class_identifier_field(const exprt &this_expr_in, const struct_tag_typet &suggested_type, const namespacet &ns)
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)
Remove virtual function calls from all functions in the specified list and replace them with their mo...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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.
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
Returns symbol pointing to a specified method in a specified class.
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.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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 p before target.
codet representation of a function call statement.
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an 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.
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)
Replace virtual function call with a static function call Achieved by substituting a virtual function...
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)
Replace virtual function call with a static function call Achieved by substituting a virtual function...
bool empty() const
Is the program empty?
int compare(const dstringt &b) const
#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 documentation for 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)