const symbol_table_baset &symbol_table,

const irep_idt &main_class,

const std::vector<irep_idt> &main_jar_classes,

const std::vector<load_extra_methodst> &lazy_methods_extra_entry_points,

java_class_loadert &java_class_loader,

const std::vector<irep_idt> &extra_instantiated_classes,

const select_pointer_typet &pointer_type_selector,

const synthetic_methods_mapt &synthetic_methods)

: main_class(main_class),

main_jar_classes(main_jar_classes),

lazy_methods_extra_entry_points(lazy_methods_extra_entry_points),

java_class_loader(java_class_loader),

extra_instantiated_classes(extra_instantiated_classes),

pointer_type_selector(pointer_type_selector),

synthetic_methods(synthetic_methods)

{

// build the class hierarchy

class_hierarchy(symbol_table);

{

static const struct_tag_typet class_type("java::java.lang.Class");

for(auto it = expr.depth_begin(); it != expr.depth_end(); ++it)

{

if(can_cast_expr<symbol_exprt>(*it) &&

it->type() == class_type &&

has_suffix(

id2string(to_symbol_expr(*it).get_identifier()),

JAVA_CLASS_MODEL_SUFFIX))

{

return true;

}

}

return false;

std::unordered_set<irep_idt> &methods_to_convert_later,

std::unordered_set<irep_idt> &instantiated_classes,

const std::unordered_set<class_method_descriptor_exprt, irep_hash>

&virtual_functions,

symbol_table_baset &symbol_table)

{

ci_lazy_methods_neededt lazy_methods_loader(

methods_to_convert_later,

instantiated_classes,

symbol_table,

pointer_type_selector);

bool any_new_classes = false;

for(const class_method_descriptor_exprt &virtual_function : virtual_functions)

{

std::unordered_set<irep_idt> candidate_target_methods;

get_virtual_method_targets(

virtual_function,

instantiated_classes,

candidate_target_methods,

symbol_table);

if(!candidate_target_methods.empty())

continue;

const java_method_typet &java_method_type =

to_java_method_type(virtual_function.type());

// Add the call class to instantiated_classes and assert that it

// didn't already exist. It can't be instantiated already, otherwise it

// would give a concrete definition of the called method, and

// candidate_target_methods would be non-empty.

const irep_idt &call_class = virtual_function.class_id();

bool was_missing = instantiated_classes.count(call_class) == 0;

CHECK_RETURN(was_missing);

any_new_classes = true;

const typet &this_type = java_method_type.get_this()->type();

if(

const pointer_typet *this_pointer_type =

type_try_dynamic_cast<pointer_typet>(this_type))

{

lazy_methods_loader.add_all_needed_classes(*this_pointer_type);

}

// That should in particular have added call_class to the possibly

// instantiated types.

bool still_missing = instantiated_classes.count(call_class) == 0;

CHECK_RETURN(!still_missing);

// Make sure we add our return type as required, as we may not have

// seen any concrete instances of it being created.

const typet &return_type = java_method_type.return_type();

if(

const pointer_typet *return_pointer_type =

type_try_dynamic_cast<pointer_typet>(return_type))

{

lazy_methods_loader.add_all_needed_classes(*return_pointer_type);

}

// Check that `get_virtual_method_target` returns a method now

const irep_idt &method_name = virtual_function.mangled_method_name();

const irep_idt method_id = get_virtual_method_target(

instantiated_classes, method_name, call_class, symbol_table);

CHECK_RETURN(!method_id.empty());

// Add what it returns to methods_to_convert_later

methods_to_convert_later.insert(method_id);

}

return any_new_classes;

const method_convertert &method_converter,

std::unordered_set<irep_idt> &methods_already_populated,

const bool class_initializer_already_seen,

const irep_idt &method_name,

symbol_table_baset &symbol_table,

std::unordered_set<irep_idt> &methods_to_convert_later,

std::unordered_set<irep_idt> &instantiated_classes,

std::unordered_set<class_method_descriptor_exprt, irep_hash>

&called_virtual_functions,

message_handlert &message_handler)

{

convert_method_resultt result;

if(!methods_already_populated.insert(method_name).second)

return result;

messaget log{message_handler};

log.debug() << "CI lazy methods: elaborate " << method_name << messaget::eom;

// Note this wraps *references* to methods_to_convert_later &

// instantiated_classes

ci_lazy_methods_neededt needed_methods(

methods_to_convert_later,

instantiated_classes,

symbol_table,

pointer_type_selector);

if(method_converter(method_name, needed_methods))

return result;

const exprt &method_body = symbol_table.lookup_ref(method_name).value;

gather_virtual_callsites(method_body, called_virtual_functions);

if(!class_initializer_already_seen && references_class_model(method_body))

{

result.class_initializer_seen = true;

const irep_idt initializer_signature =

get_java_class_literal_initializer_signature();

if(symbol_table.has_symbol(initializer_signature))

methods_to_convert_later.insert(initializer_signature);

}

result.new_method_seen = true;

return result;

const symbol_table_baset &symbol_table,

message_handlert &message_handler)

{

std::unordered_set<irep_idt> methods_to_convert_later;

const main_function_resultt main_function =

get_main_symbol(symbol_table, this->main_class, message_handler);

if(!main_function.is_success())

{

// Failed, mark all functions in the given main class(es)

// reachable.

std::vector<irep_idt> reachable_classes;

if(!this->main_class.empty())

reachable_classes.push_back(this->main_class);

else

reachable_classes = this->main_jar_classes;

for(const irep_idt &class_name : reachable_classes)

{

const auto &methods =

this->java_class_loader.get_original_class(class_name)

.parsed_class.methods;

for(const auto &method : methods)

{

const irep_idt methodid = "java::" + id2string(class_name) + "." +

id2string(method.name) + ":" +

id2string(method.descriptor);

methods_to_convert_later.insert(methodid);

}

}

}

else

methods_to_convert_later.insert(main_function.main_function.name);

return methods_to_convert_later;

const std::unordered_set<irep_idt> &entry_points,

const namespacet &ns,

ci_lazy_methods_neededt &needed_lazy_methods)

{

for(const auto &mname : entry_points)

{

const auto &symbol=ns.lookup(mname);

const auto &mtype = to_java_method_type(symbol.type);

for(const auto &param : mtype.parameters())

{

if(param.type().id()==ID_pointer)

{

const pointer_typet &original_pointer = to_pointer_type(param.type());

needed_lazy_methods.add_all_needed_classes(original_pointer);

}

}

}

// Also add classes whose instances are magically

// created by the JVM and so won't be spotted by

// looking for constructors and calls as usual:

needed_lazy_methods.add_needed_class("java::java.lang.String");

needed_lazy_methods.add_needed_class("java::java.lang.Class");

needed_lazy_methods.add_needed_class("java::java.lang.Object");

// As in class_loader, ensure these classes stay available

for(const auto &id : extra_instantiated_classes)

needed_lazy_methods.add_needed_class("java::" + id2string(id));

const exprt &e,

std::unordered_set<class_method_descriptor_exprt, irep_hash> &result)

{

if(e.id()!=ID_code)

return;

const codet &c=to_code(e);

if(

c.get_statement() == ID_function_call &&

can_cast_expr<class_method_descriptor_exprt>(

to_code_function_call(c).function()))

{

result.insert(

to_class_method_descriptor_expr(to_code_function_call(c).function()));

}

else

{

for(const exprt &op : e.operands())

gather_virtual_callsites(op, result);

}

const class_method_descriptor_exprt &called_function,

const std::unordered_set<irep_idt> &instantiated_classes,

std::unordered_set<irep_idt> &callable_methods,

symbol_table_baset &symbol_table)

{

const auto &call_class = called_function.class_id();

const auto &method_name = called_function.mangled_method_name();

class_hierarchyt::idst self_and_child_classes =

class_hierarchy.get_children_trans(call_class);

self_and_child_classes.push_back(call_class);

for(const irep_idt &class_name : self_and_child_classes)

{

const irep_idt method_id = get_virtual_method_target(

instantiated_classes, method_name, class_name, symbol_table);

if(!method_id.empty())

callable_methods.insert(method_id);

}

const exprt &e,

const symbol_table_baset &symbol_table,

symbol_table_baset &needed)

{

if(e.id()==ID_symbol)

{

// If the symbol isn't in the symbol table at all, then it is defined

// on an opaque type (i.e. we don't have the class definition at this point)

// and will be created during the typecheck phase.

// We don't mark it as 'needed' as it doesn't exist yet to keep.

const auto findit=

symbol_table.symbols.find(to_symbol_expr(e).get_identifier());

if(findit!=symbol_table.symbols.end() &&

findit->second.is_static_lifetime)

{

needed.add(findit->second);

// Gather any globals referenced in the initialiser:

gather_needed_globals(findit->second.value, symbol_table, needed);

}

}

else

{

for(const auto &op : e.operands())

gather_needed_globals(op, symbol_table, needed);

}

const std::unordered_set<irep_idt> &instantiated_classes,

const irep_idt &call_basename,

const irep_idt &classname,

const symbol_table_baset &symbol_table)

{

// Program-wide, is this class ever instantiated?

if(!instantiated_classes.count(classname))

return irep_idt();

auto resolved_call =

get_inherited_method_implementation(call_basename, classname, symbol_table);

if(resolved_call)

return resolved_call->get_full_component_identifier();

else

return irep_idt();