47 typedef std::function<
112 "function overrides must have matching argument counts");
114 for(std::size_t i = 0; i <
call_args.size(); ++i)
125 "where overriding function argument types differ, "
126 "those arguments must be pointer-typed");
171 bool changed =
false;
275 target->is_function_call(),
276 "remove_virtual_function must target a FUNCTION_CALL instruction");
281 if(functions.empty())
283 target->turn_into_skip();
289 if(functions.size()==1 &&
292 if(!functions.front().symbol_expr.has_value())
294 target->turn_into_skip();
300 target->call_lhs(), target->call_function(), target->call_arguments());
302 target->call_function() =
c.function();
303 target->call_arguments() =
c.arguments();
311 target->call_lhs(), target->call_function(), target->call_arguments());
340 "this parameter must not be a void pointer");
356 INVARIANT(!functions.empty(),
"Function dispatch table cannot be empty.");
359 std::map<irep_idt, goto_programt::targett>
calls;
361 for(
auto it=functions.crbegin(),
itend=functions.crend(); it!=
itend; ++it)
365 ?
fun.symbol_expr->get_identifier()
372 if(
fun.symbol_expr.has_value())
389 "cannot find calls for " +
406 (!
fun.symbol_expr.has_value() ||
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))
427 "a dispatch table entry has been processed already, "
428 "which should have created a GOTO");
451 target->turn_into_skip();
476 "remove_virtual_function must take a function call instruction whose "
477 "function is a class method descriptor ");
479 !
as_const(*target).call_arguments().empty(),
480 "virtual function calls must have at least a this-argument");
523 auto it = entry_map.find(
child);
525 it != entry_map.end() &&
526 (!it->second.symbol_expr.has_value() ||
528 id2string(it->second.symbol_expr->get_identifier()),
529 "java::java.lang.Object")))
559 functions.push_back(function);
560 entry_map.emplace(
child, function);
572 const exprt &function,
580 INVARIANT(!class_id.
empty(),
"All virtual functions must have a class");
603 class_id,
root_function.symbol_expr, function_name, functions, entry_map);
616 irep_idt a_id = a.symbol_expr.has_value()
617 ? a.symbol_expr->get_identifier()
619 irep_idt b_id = b.symbol_expr.has_value()
620 ? b.symbol_expr->get_identifier()
623 if(has_prefix(id2string(a_id),
"java::java.lang.Object"))
625 else if(has_prefix(id2string(b_id),
"java::java.lang.Object"))
629 int cmp = a_id.compare(b_id);
631 return a.class_id < b.class_id;
645 const irep_idt &component_name)
const
649 class_id, component_name);
652 if(
ns.lookup(
id, symbol))
667 for(goto_programt::instructionst::iterator
672 if(target->is_function_call())
698 for(goto_functionst::function_mapt::iterator
f_it=
723 class_hierarchy(symbol_table);
774 rvf.remove_virtual_functions(
790 rvf.remove_virtual_functions(
851 const exprt &function,
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
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.
exprt get_class_identifier_field(const exprt &this_expr_in, const struct_tag_typet &suggested_type, const namespacet &ns)
Extract class identifier.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Non-graph-based representation of the class hierarchy.
goto_instruction_codet representation of a function call statement.
A constant literal expression.
optionalt< symbol_exprt > symbol_expr
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
The Boolean constant false.
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.
const irep_idt & get_function_id()
Get function id.
goto_functionst::goto_functiont & get_goto_function()
Get GOTO function.
journalling_symbol_tablet & get_symbol_table()
Get symbol table.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
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.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
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())
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
remove_virtual_functionst(symbol_table_baset &_symbol_table, const class_hierarchyt &_class_hierarchy)
symbol_table_baset & symbol_table
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...
A struct tag type, i.e., struct_typet with an identifier.
Expression to hold a symbol (variable)
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.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
The Boolean constant true.
Semantic type conversion.
The type of an expression, extends irept.
bool has_prefix(const std::string &s, const std::string &prefix)
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.
const std::string & id2string(const irep_idt &d)
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
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'.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.