42 const std::vector<irep_idt> &main_jar_classes,
43 const std::vector<load_extra_methodst> &lazy_methods_extra_entry_points,
45 const std::vector<irep_idt> &extra_instantiated_classes,
48 : main_class(main_class),
49 main_jar_classes(main_jar_classes),
50 lazy_methods_extra_entry_points(lazy_methods_extra_entry_points),
51 java_class_loader(java_class_loader),
52 extra_instantiated_classes(extra_instantiated_classes),
53 pointer_type_selector(pointer_type_selector),
54 synthetic_methods(synthetic_methods)
73 it->type() == class_type &&
107 std::unordered_set<irep_idt> methods_to_convert_later =
114 std::vector<irep_idt> extra_methods =
115 extra_function_generator(symbol_table);
116 methods_to_convert_later.insert(extra_methods.begin(), extra_methods.end());
119 std::unordered_set<irep_idt> instantiated_classes;
122 std::unordered_set<irep_idt> initial_callable_methods;
124 initial_callable_methods,
125 instantiated_classes,
129 methods_to_convert_later,
namespacet(symbol_table), initial_lazy_methods);
130 methods_to_convert_later.insert(
131 initial_callable_methods.begin(), initial_callable_methods.end());
134 std::unordered_set<irep_idt> methods_already_populated;
135 std::unordered_set<class_method_descriptor_exprt, irep_hash>
136 called_virtual_functions;
137 bool class_initializer_seen =
false;
141 bool any_new_classes =
true;
142 while(any_new_classes)
144 bool any_new_methods =
true;
145 while(any_new_methods)
147 any_new_methods =
false;
148 while(!methods_to_convert_later.empty())
150 std::unordered_set<irep_idt> methods_to_convert;
151 std::swap(methods_to_convert, methods_to_convert_later);
152 for(
const auto &mname : methods_to_convert)
156 methods_already_populated,
157 class_initializer_seen,
160 methods_to_convert_later,
161 instantiated_classes,
162 called_virtual_functions,
164 any_new_methods |= conversion_result.new_method_seen;
165 class_initializer_seen |= conversion_result.class_initializer_seen;
172 log.debug() <<
"CI lazy methods: add virtual method targets ("
173 << called_virtual_functions.size() <<
" callsites)"
177 called_virtual_functions)
180 called_virtual_function,
181 instantiated_classes,
182 methods_to_convert_later,
188 methods_to_convert_later,
189 instantiated_classes,
190 called_virtual_functions,
200 for(
const auto &sym : symbol_table.
symbols)
204 if(sym.second.is_static_lifetime)
206 if(sym.second.type.id()==ID_code)
213 !methods_already_populated.count(sym.first))
220 keep_symbols.
add(sym.second);
223 log.debug() <<
"CI lazy methods: removed "
229 auto it = sorted_to_keep.cbegin();
230 for(
const auto &
id : all_sorted)
232 if(it == sorted_to_keep.cend() ||
id != *it)
249 std::unordered_set<irep_idt> &methods_to_convert_later,
250 std::unordered_set<irep_idt> &instantiated_classes,
251 const std::unordered_set<class_method_descriptor_exprt, irep_hash>
256 methods_to_convert_later,
257 instantiated_classes,
261 bool any_new_classes =
false;
264 std::unordered_set<irep_idt> candidate_target_methods;
267 instantiated_classes,
268 candidate_target_methods,
271 if(!candidate_target_methods.empty())
281 const irep_idt &call_class = virtual_function.class_id();
282 bool was_missing = instantiated_classes.count(call_class) == 0;
284 any_new_classes =
true;
289 type_try_dynamic_cast<pointer_typet>(this_type))
296 bool still_missing = instantiated_classes.count(call_class) == 0;
304 type_try_dynamic_cast<pointer_typet>(return_type))
310 const irep_idt &method_name = virtual_function.mangled_method_name();
312 instantiated_classes, method_name, call_class, symbol_table);
316 methods_to_convert_later.insert(method_id);
318 return any_new_classes;
333 std::unordered_set<irep_idt> &methods_already_populated,
334 const bool class_initializer_already_seen,
337 std::unordered_set<irep_idt> &methods_to_convert_later,
338 std::unordered_set<irep_idt> &instantiated_classes,
339 std::unordered_set<class_method_descriptor_exprt, irep_hash>
340 &called_virtual_functions,
344 if(!methods_already_populated.insert(method_name).second)
348 log.debug() <<
"CI lazy methods: elaborate " << method_name <<
messaget::eom;
353 methods_to_convert_later,
354 instantiated_classes,
358 if(method_converter(method_name, needed_methods))
367 const irep_idt initializer_signature =
369 if(symbol_table.
has_symbol(initializer_signature))
370 methods_to_convert_later.insert(initializer_signature);
385 std::unordered_set<irep_idt> methods_to_convert_later;
393 std::vector<irep_idt> reachable_classes;
395 reachable_classes.push_back(this->
main_class);
398 for(
const irep_idt &class_name : reachable_classes)
400 const auto &methods =
403 for(
const auto &method : methods)
408 methods_to_convert_later.insert(methodid);
414 return methods_to_convert_later;
426 const std::unordered_set<irep_idt> &entry_points,
430 for(
const auto &mname : entry_points)
432 const auto &symbol=ns.
lookup(mname);
434 for(
const auto ¶m : mtype.parameters())
436 if(param.type().id()==ID_pointer)
462 std::unordered_set<class_method_descriptor_exprt, irep_hash> &result)
494 const std::unordered_set<irep_idt> &instantiated_classes,
495 std::unordered_set<irep_idt> &callable_methods,
498 const auto &call_class = called_function.
class_id();
503 self_and_child_classes.push_back(call_class);
505 for(
const irep_idt &class_name : self_and_child_classes)
508 instantiated_classes, method_name, class_name, symbol_table);
509 if(!method_id.
empty())
510 callable_methods.insert(method_id);
524 if(e.
id()==ID_symbol)
532 if(findit!=symbol_table.
symbols.end() &&
533 findit->second.is_static_lifetime)
535 needed.
add(findit->second);
560 const std::unordered_set<irep_idt> &instantiated_classes,
566 if(!instantiated_classes.count(classname))
573 return resolved_call->get_full_component_identifier();
static bool references_class_model(const exprt &expr)
Checks if an expression refers to any class literals (e.g.
Collect methods needed to be loaded using the lazy method.
std::function< bool(const irep_idt &function_id, ci_lazy_methods_neededt)> method_convertert
void add_all_needed_classes(const pointer_typet &pointer_type)
Add to the needed classes all classes specified, the replacement type if it will be replaced,...
bool add_needed_class(const irep_idt &)
Notes class class_symbol_name will be instantiated, or a static field belonging to it will be accesse...
convert_method_resultt convert_and_analyze_method(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 a method, add it to the populated set, add needed methods to methods_to_convert_later and add...
const std::vector< irep_idt > & extra_instantiated_classes
irep_idt get_virtual_method_target(const std::unordered_set< irep_idt > &instantiated_classes, const irep_idt &call_basename, const irep_idt &classname, const symbol_table_baset &symbol_table)
Find a virtual callee, if one is defined and the callee type is known to exist.
void get_virtual_method_targets(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)
Find possible callees, excluding types that are not known to be instantiated.
std::vector< irep_idt > main_jar_classes
const select_pointer_typet & pointer_type_selector
const std::vector< load_extra_methodst > & lazy_methods_extra_entry_points
class_hierarchyt class_hierarchy
void gather_virtual_callsites(const exprt &e, std::unordered_set< class_method_descriptor_exprt, irep_hash > &result)
Get places where virtual functions are called.
java_class_loadert & java_class_loader
bool operator()(symbol_table_baset &symbol_table, method_bytecodet &method_bytecode, const method_convertert &method_converter, message_handlert &message_handler)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
const synthetic_methods_mapt & synthetic_methods
ci_lazy_methodst(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)
Constructor for lazy-method loading.
void gather_needed_globals(const exprt &e, const symbol_table_baset &symbol_table, symbol_table_baset &needed)
See output.
void initialize_instantiated_classes(const std::unordered_set< irep_idt > &entry_points, const namespacet &ns, ci_lazy_methods_neededt &needed_lazy_methods)
Build up a list of methods whose type may be passed around reachable from the entry point.
bool handle_virtual_methods_with_no_callees(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)
Look for virtual callsites with no candidate targets.
std::unordered_set< irep_idt > entry_point_methods(const symbol_table_baset &symbol_table, message_handlert &message_handler)
Entry point methods are either:
idst get_children_trans(const irep_idt &id) const
std::vector< irep_idt > idst
An expression describing a method on a class.
const irep_idt & class_id() const
Unique identifier in the symbol table, of the compile time type of the class which this expression is...
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
const typet & return_type() const
const parametert * get_this() const
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
depth_iteratort depth_end()
depth_iteratort depth_begin()
typet & type()
Return the type of the expression.
const irep_idt & id() const
Class responsible to load .class files.
const java_bytecode_parse_treet & get_original_class(const irep_idt &class_name)
Class that provides messages with a built-in verbosity 'level'.
bool contains_method(const irep_idt &method_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().
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
A struct tag type, i.e., struct_typet with an identifier.
const irep_idt & get_identifier() const
The symbol table base class interface.
std::vector< irep_idt > sorted_symbol_names() const
Build and return a lexicographically sorted vector of symbol names from all symbols stored in this sy...
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
The type of an expression, extends irept.
Forward depth-first search iterators These iterators' copy operations are expensive,...
const code_function_callt & to_code_function_call(const goto_instruction_codet &code)
const std::string & id2string(const irep_idt &d)
#define JAVA_CLASS_MODEL_SUFFIX
main_function_resultt get_main_symbol(const symbol_table_baset &symbol_table, const irep_idt &main_class, message_handlert &message_handler)
Figures out the entry point of the code to verify.
irep_idt get_java_class_literal_initializer_signature()
Get the symbol name of java.lang.Class' initializer method.
const java_method_typet & to_java_method_type(const typet &type)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Remove function exceptional returns.
#define INFLIGHT_EXCEPTION_VARIABLE_NAME
std::optional< 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 CHECK_RETURN(CONDITION)
const codet & to_code(const exprt &expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
bool can_cast_expr< class_method_descriptor_exprt >(const exprt &base)
bool can_cast_expr< symbol_exprt >(const exprt &base)
const class_method_descriptor_exprt & to_class_method_descriptor_expr(const exprt &expr)
Cast an exprt to a class_method_descriptor_exprt.
bool class_initializer_seen
bool has_suffix(const std::string &s, const std::string &suffix)
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.