{

get_virtual_calleest(

const symbol_table_baset &_symbol_table,

const class_hierarchyt &_class_hierarchy)

: ns(_symbol_table),

symbol_table(_symbol_table),

class_hierarchy(_class_hierarchy)

{

}

void get_functions(const exprt &, dispatch_table_entriest &) const;

const namespacet ns;

const symbol_table_baset &symbol_table;

const class_hierarchyt &class_hierarchy;

typedef std::function<

std::optional<resolve_inherited_componentt::inherited_componentt>(

const irep_idt &,

const irep_idt &)>

function_call_resolvert;

void get_child_functions_rec(

const irep_idt &,

const std::optional<symbol_exprt> &,

const irep_idt &,

dispatch_table_entriest &,

dispatch_table_entries_mapt &) const;

exprt

get_method(const irep_idt &class_id, const irep_idt &component_name) const;

{

remove_virtual_functionst(

symbol_table_baset &_symbol_table,

const class_hierarchyt &_class_hierarchy)

: class_hierarchy(_class_hierarchy),

symbol_table(_symbol_table),

ns(symbol_table)

{

}

void operator()(goto_functionst &functions);

bool remove_virtual_functions(

const irep_idt &function_id,

goto_programt &goto_program);

const class_hierarchyt &class_hierarchy;

symbol_table_baset &symbol_table;

namespacet ns;

goto_programt::targett remove_virtual_function(

const irep_idt &function_id,

goto_programt &goto_program,

goto_programt::targett target);

code_function_callt &call,

const symbol_exprt &function_symbol,

const namespacet &ns)

{

call.function() = function_symbol;

// Cast the pointers to the correct type for the new callee:

// Note the `this` pointer is expected to change type, but other pointers

// could also change due to e.g. using a different alias to refer to the same

// type (in Java, for example, we see ArrayList.add(ArrayList::E arg)

// overriding Collection.add(Collection::E arg))

const auto &callee_parameters =

to_code_type(ns.lookup(function_symbol.get_identifier()).type).parameters();

auto &call_args = call.arguments();

INVARIANT(

callee_parameters.size() == call_args.size(),

"function overrides must have matching argument counts");

for(std::size_t i = 0; i < call_args.size(); ++i)

{

const typet &need_type = callee_parameters[i].type();

if(call_args[i].type() != need_type)

{

// If this wasn't language agnostic code we'd also like to check

// compatibility-- for example, Java overrides may have differing generic

// qualifiers, but not different base types.

INVARIANT(

call_args[i].type().id() == ID_pointer,

"where overriding function argument types differ, "

"those arguments must be pointer-typed");

call_args[i] = typecast_exprt(call_args[i], need_type);

}

}

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)

{

goto_programt checks_directly_preceding_function_call;

while(instr_it != goto_program.instructions.cbegin())

{

instr_it = std::prev(instr_it);

if(instr_it->is_assert())

{

continue;

}

if(!instr_it->is_assume())

{

break;

}

exprt guard = instr_it->condition();

bool changed = false;

for(auto expr_it = guard.depth_begin(); expr_it != guard.depth_end();

++expr_it)

{

if(*expr_it == argument_for_this)

{

expr_it.mutate() = temp_var_for_this;

changed = true;

}

}

if(changed)

{

checks_directly_preceding_function_call.insert_before(

checks_directly_preceding_function_call.instructions.cbegin(),

goto_programt::make_assumption(guard, vcall_source_loc));

}

}

return checks_directly_preceding_function_call;

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(has_subexpr(argument_for_this, ID_dereference))

{

// Create a temporary for the `this` argument. This is so that

// \ref goto_symext::try_filter_value_sets can reduce the value-set for

// `this` to those elements with the correct class identifier.

symbolt &temp_symbol = get_fresh_aux_symbol(

argument_for_this.type(),

id2string(function_id),

"this_argument",

vcall_source_loc,

symbol_table.lookup_ref(function_id).mode,

symbol_table);

const symbol_exprt temp_var_for_this = temp_symbol.symbol_expr();

new_code_for_this_argument.add(

goto_programt::make_decl(temp_var_for_this, vcall_source_loc));

new_code_for_this_argument.add(

goto_programt::make_assignment(

temp_var_for_this, argument_for_this, vcall_source_loc));

goto_programt checks_directly_preceding_function_call =

analyse_checks_directly_preceding_function_call(

goto_program,

target,

argument_for_this,

temp_var_for_this,

vcall_source_loc);

new_code_for_this_argument.destructive_append(

checks_directly_preceding_function_call);

argument_for_this = temp_var_for_this;

}

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)

{

INVARIANT(

target->is_function_call(),

"remove_virtual_function must target a FUNCTION_CALL instruction");

namespacet ns(symbol_table);

goto_programt::targett next_target = std::next(target);

if(functions.empty())

{

target->turn_into_skip();

remove_skip(goto_program, target, next_target);

return next_target; // give up

}

// only one option?

if(functions.size()==1 &&

fallback_action==virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION)

{

if(!functions.front().symbol_expr.has_value())

{

target->turn_into_skip();

remove_skip(goto_program, target, next_target);

}

else

{

auto c = code_function_callt(

target->call_lhs(), target->call_function(), target->call_arguments());

create_static_function_call(c, *functions.front().symbol_expr, ns);

target->call_function() = c.function();

target->call_arguments() = c.arguments();

}

return next_target;

}

const auto &vcall_source_loc = target->source_location();

code_function_callt code(

target->call_lhs(), target->call_function(), target->call_arguments());

goto_programt new_code_for_this_argument;

process_this_argument(

function_id,

goto_program,

target,

code.arguments()[0],

symbol_table,

vcall_source_loc,

new_code_for_this_argument);

const exprt &this_expr = code.arguments()[0];

// Create a skip as the final target for each branch to jump to at the end

goto_programt final_skip;

goto_programt::targett t_final =

final_skip.add(goto_programt::make_skip(vcall_source_loc));

// build the calls and gotos

goto_programt new_code_calls;

goto_programt new_code_gotos;

INVARIANT(

this_expr.type().id() == ID_pointer, "this parameter must be a pointer");

INVARIANT(

to_pointer_type(this_expr.type()).base_type() != empty_typet(),

"this parameter must not be a void pointer");

// So long as `this` is already not `void*` typed, the second parameter

// is ignored:

exprt this_class_identifier =

get_class_identifier_field(this_expr, struct_tag_typet(irep_idt()), ns);

// If instructed, add an ASSUME(FALSE) to handle the case where we don't

// match any expected type:

if(fallback_action==virtual_dispatch_fallback_actiont::ASSUME_FALSE)

{

new_code_calls.add(

goto_programt::make_assumption(false_exprt(), vcall_source_loc));

}

// get initial identifier for grouping

INVARIANT(!functions.empty(), "Function dispatch table cannot be empty.");

const auto &last_function_symbol = functions.back().symbol_expr;

std::map<irep_idt, goto_programt::targett> calls;

// Note backwards iteration, to get the fallback candidate first.

for(auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it)

{

const auto &fun=*it;

irep_idt id_or_empty = fun.symbol_expr.has_value()

? fun.symbol_expr->get_identifier()

: irep_idt();

auto insertit = calls.insert({id_or_empty, goto_programt::targett()});

// Only create one call sequence per possible target:

if(insertit.second)

{

if(fun.symbol_expr.has_value())

{

// call function

auto new_call = code;

create_static_function_call(new_call, *fun.symbol_expr, ns);

goto_programt::targett t1 = new_code_calls.add(

goto_programt::make_function_call(new_call, vcall_source_loc));

insertit.first->second = t1;

}

else

{

source_locationt annotated_location = vcall_source_loc;

// No definition for this type; shouldn't be possible...

annotated_location.set_comment(

"cannot find calls for " +

id2string(code.function().get(ID_identifier)) + " dispatching " +

id2string(fun.class_id));

insertit.first->second = new_code_calls.add(

goto_programt::make_assertion(false_exprt(), annotated_location));

}

// goto final

new_code_calls.add(

goto_programt::make_goto(t_final, true_exprt(), vcall_source_loc));

}

// Fall through to the default callee if possible:

if(

fallback_action ==

virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION &&

fun.symbol_expr.has_value() == last_function_symbol.has_value() &&

(!fun.symbol_expr.has_value() ||

*fun.symbol_expr == *last_function_symbol))

{

// Nothing to do

}

else

{

const constant_exprt fun_class_identifier(fun.class_id, string_typet());

const equal_exprt class_id_test(

fun_class_identifier, this_class_identifier);

// If the previous GOTO goes to the same callee, join it

// (e.g. turning IF x GOTO y into IF x || z GOTO y)

if(

it != functions.crbegin() &&

std::prev(it)->symbol_expr.has_value() == fun.symbol_expr.has_value() &&

(!fun.symbol_expr.has_value() ||

*(std::prev(it)->symbol_expr) == *fun.symbol_expr))

{

INVARIANT(

!new_code_gotos.empty(),

"a dispatch table entry has been processed already, "

"which should have created a GOTO");

new_code_gotos.instructions.back().condition_nonconst() = or_exprt(

new_code_gotos.instructions.back().condition(), class_id_test);

}

else

{

new_code_gotos.add(goto_programt::make_goto(

insertit.first->second, class_id_test, vcall_source_loc));

}

}

}

goto_programt new_code;

// patch them all together

new_code.destructive_append(new_code_for_this_argument);

new_code.destructive_append(new_code_gotos);

new_code.destructive_append(new_code_calls);

new_code.destructive_append(final_skip);

goto_program.destructive_insert(next_target, new_code);

// finally, kill original invocation

target->turn_into_skip();

// only remove skips within the virtual-function handling block

remove_skip(goto_program, target, next_target);

return next_target;

const irep_idt &function_id,

goto_programt &goto_program,

goto_programt::targett target)

{

const exprt &function = as_const(*target).call_function();

INVARIANT(

can_cast_expr<class_method_descriptor_exprt>(function),

"remove_virtual_function must take a function call instruction whose "

"function is a class method descriptor ");

INVARIANT(

!as_const(*target).call_arguments().empty(),

"virtual function calls must have at least a this-argument");

get_virtual_calleest get_callees(symbol_table, class_hierarchy);

dispatch_table_entriest functions;

get_callees.get_functions(function, functions);

return replace_virtual_function_with_dispatch_table(

symbol_table,

function_id,

goto_program,

target,

functions,

virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION);

const irep_idt &this_id,

const std::optional<symbol_exprt> &last_method_defn,

const irep_idt &component_name,

dispatch_table_entriest &functions,

dispatch_table_entries_mapt &entry_map) const

{

auto findit=class_hierarchy.class_map.find(this_id);

if(findit==class_hierarchy.class_map.end())

return;

for(const auto &child : findit->second.children)

{

// Skip if we have already visited this and we found a function call that

// did not resolve to non java.lang.Object.

auto it = entry_map.find(child);

if(

it != entry_map.end() &&

(!it->second.symbol_expr.has_value() ||

!it->second.symbol_expr->get_identifier().starts_with(

"java::java.lang.Object")))

{

continue;

}

exprt method = get_method(child, component_name);

dispatch_table_entryt function(child);

if(method.is_not_nil())

{

function.symbol_expr=to_symbol_expr(method);

function.symbol_expr->set(ID_C_class, child);

}

else

{

function.symbol_expr=last_method_defn;

}

if(!function.symbol_expr.has_value())

{

const auto resolved_call = get_inherited_method_implementation(

component_name, child, symbol_table);

if(resolved_call)

{

function.class_id = resolved_call->get_class_identifier();

const symbolt &called_symbol = symbol_table.lookup_ref(

resolved_call->get_full_component_identifier());

function.symbol_expr = called_symbol.symbol_expr();

function.symbol_expr->set(

ID_C_class, resolved_call->get_class_identifier());

}

}

functions.push_back(function);

entry_map.emplace(child, function);

get_child_functions_rec(

child, function.symbol_expr, component_name, functions, entry_map);

}

const exprt &function,

dispatch_table_entriest &functions) const

{

// class part of function to call

const irep_idt class_id=function.get(ID_C_class);

const std::string class_id_string(id2string(class_id));

const irep_idt function_name = function.get(ID_component_name);

const std::string function_name_string(id2string(function_name));

INVARIANT(!class_id.empty(), "All virtual functions must have a class");

auto resolved_call =

get_inherited_method_implementation(function_name, class_id, symbol_table);

// might be an abstract function

dispatch_table_entryt root_function(class_id);

if(resolved_call)

{

root_function.class_id = resolved_call->get_class_identifier();

const symbolt &called_symbol =

symbol_table.lookup_ref(resolved_call->get_full_component_identifier());

root_function.symbol_expr=called_symbol.symbol_expr();

root_function.symbol_expr->set(

ID_C_class, resolved_call->get_class_identifier());

}

// iterate over all children, transitively

dispatch_table_entries_mapt entry_map;

get_child_functions_rec(

class_id, root_function.symbol_expr, function_name, functions, entry_map);

if(root_function.symbol_expr.has_value())

functions.push_back(root_function);

// Sort for the identifier of the function call symbol expression, grouping

// together calls to the same function. Keep java.lang.Object entries at the

// end for fall through. The reasoning is that this is the case with most

// entries in realistic cases.

std::sort(

functions.begin(),

functions.end(),

[](const dispatch_table_entryt &a, const dispatch_table_entryt &b) {

irep_idt a_id = a.symbol_expr.has_value()

? a.symbol_expr->get_identifier()

: irep_idt();

irep_idt b_id = b.symbol_expr.has_value()

? b.symbol_expr->get_identifier()

: irep_idt();

if(a_id.starts_with("java::java.lang.Object"))

return false;

else if(b_id.starts_with("java::java.lang.Object"))

return true;

else

{

int cmp = a_id.compare(b_id);

if(cmp == 0)

return a.class_id < b.class_id;

else

return cmp < 0;

}

});

const irep_idt &class_id,

const irep_idt &component_name) const

{

const irep_idt &id=

resolve_inherited_componentt::build_full_component_identifier(

class_id, component_name);

const symbolt *symbol;

if(ns.lookup(id, symbol))

return nil_exprt();

return symbol->symbol_expr();

const irep_idt &function_id,

goto_programt &goto_program)

{

bool did_something=false;

for(goto_programt::instructionst::iterator

target = goto_program.instructions.begin();

target != goto_program.instructions.end();

) // remove_virtual_function returns the next instruction to process

{

if(target->is_function_call())

{

if(can_cast_expr<class_method_descriptor_exprt>(

as_const(*target).call_function()))

{

target = remove_virtual_function(function_id, goto_program, target);

did_something=true;

continue;

}

}

++target;

}

if(did_something)

goto_program.update();

return did_something;

symbol_table_baset &symbol_table,

goto_functionst &goto_functions)

{

class_hierarchyt class_hierarchy;

class_hierarchy(symbol_table);

remove_virtual_functionst rvf(symbol_table, class_hierarchy);

rvf(goto_functions);

symbol_table_baset &symbol_table,

goto_functionst &goto_functions,

const class_hierarchyt &class_hierarchy)

{

remove_virtual_functionst rvf(symbol_table, class_hierarchy);

rvf(goto_functions);

{

remove_virtual_functions(

goto_model.symbol_table, goto_model.goto_functions);

goto_modelt &goto_model,

const class_hierarchyt &class_hierarchy)

{

remove_virtual_functions(

goto_model.symbol_table, goto_model.goto_functions, class_hierarchy);

{

class_hierarchyt class_hierarchy;

class_hierarchy(function.get_symbol_table());

remove_virtual_functionst rvf(function.get_symbol_table(), class_hierarchy);

rvf.remove_virtual_functions(

function.get_function_id(), function.get_goto_function().body);

goto_model_functiont &function,

const class_hierarchyt &class_hierarchy)

{

remove_virtual_functionst rvf(function.get_symbol_table(), class_hierarchy);

rvf.remove_virtual_functions(

function.get_function_id(), function.get_goto_function().body);

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)

{

goto_programt::targett next = replace_virtual_function_with_dispatch_table(

symbol_table,

function_id,

goto_program,

instruction,

dispatch_table,

fallback_action);

goto_program.update();

return next;

goto_modelt &goto_model,

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)

{

return remove_virtual_function(

goto_model.symbol_table,

function_id,

goto_program,

instruction,

dispatch_table,

fallback_action);

const exprt &function,

const symbol_table_baset &symbol_table,

const class_hierarchyt &class_hierarchy,

dispatch_table_entriest &overridden_functions)

{

get_virtual_calleest get_callees(symbol_table, class_hierarchy);

get_callees.get_functions(function, overridden_functions);