40 const std::vector<irep_idt> &main_jar_classes,
41 const std::vector<load_extra_methodst> &lazy_methods_extra_entry_points,
43 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 &&
105 std::unordered_set<irep_idt> methods_to_convert_later =
112 std::vector<irep_idt> extra_methods =
113 extra_function_generator(symbol_table);
114 methods_to_convert_later.insert(extra_methods.begin(), extra_methods.end());
117 std::unordered_set<irep_idt> instantiated_classes;
120 std::unordered_set<irep_idt> initial_callable_methods;
122 initial_callable_methods,
123 instantiated_classes,
127 methods_to_convert_later,
namespacet(symbol_table), initial_lazy_methods);
128 methods_to_convert_later.insert(
129 initial_callable_methods.begin(), initial_callable_methods.end());
132 std::unordered_set<irep_idt> methods_already_populated;
133 std::unordered_set<exprt, irep_hash> virtual_function_calls;
134 bool class_initializer_seen =
false;
136 bool any_new_classes =
true;
137 while(any_new_classes)
139 bool any_new_methods =
true;
140 while(any_new_methods)
142 any_new_methods =
false;
143 while(!methods_to_convert_later.empty())
145 std::unordered_set<irep_idt> methods_to_convert;
146 std::swap(methods_to_convert, methods_to_convert_later);
147 for(
const auto &mname : methods_to_convert)
151 methods_already_populated,
152 class_initializer_seen,
155 methods_to_convert_later,
156 instantiated_classes,
157 virtual_function_calls);
158 any_new_methods |= conversion_result.new_method_seen;
159 class_initializer_seen |= conversion_result.class_initializer_seen;
166 debug() <<
"CI lazy methods: add virtual method targets (" 167 << virtual_function_calls.size() <<
" callsites)" <<
eom;
169 for(
const exprt &
function : virtual_function_calls)
173 instantiated_classes,
174 methods_to_convert_later,
180 methods_to_convert_later,
181 instantiated_classes,
182 virtual_function_calls,
192 for(
const auto &sym : symbol_table.
symbols)
196 if(sym.second.is_static_lifetime)
198 if(sym.second.type.id()==ID_code)
205 !methods_already_populated.count(sym.first))
212 keep_symbols.
add(sym.second);
215 debug() <<
"CI lazy methods: removed " 217 <<
" unreachable methods and globals" <<
eom;
219 symbol_table.
swap(keep_symbols);
232 std::unordered_set<irep_idt> &methods_to_convert_later,
233 std::unordered_set<irep_idt> &instantiated_classes,
234 const std::unordered_set<exprt, irep_hash> &virtual_function_calls,
238 methods_to_convert_later,
239 instantiated_classes,
243 bool any_new_classes =
false;
244 for(
const exprt &virtual_function_call : virtual_function_calls)
246 std::unordered_set<irep_idt> candidate_target_methods;
248 virtual_function_call,
249 instantiated_classes,
250 candidate_target_methods,
253 if(!candidate_target_methods.empty())
258 const irep_idt &call_class = virtual_function_call.get(ID_C_class);
259 bool added_class = instantiated_classes.count(call_class) == 0;
265 any_new_classes =
true;
269 virtual_function_call.get(ID_component_name);
271 instantiated_classes, call_basename, call_class, symbol_table);
275 methods_to_convert_later.insert(method_name);
277 return any_new_classes;
292 std::unordered_set<irep_idt> &methods_already_populated,
293 const bool class_initializer_already_seen,
296 std::unordered_set<irep_idt> &methods_to_convert_later,
297 std::unordered_set<irep_idt> &instantiated_classes,
298 std::unordered_set<exprt, irep_hash> &virtual_function_calls)
301 if(!methods_already_populated.insert(method_name).second)
304 debug() <<
"CI lazy methods: elaborate " << method_name <<
eom;
309 methods_to_convert_later,
310 instantiated_classes,
314 if(method_converter(method_name, needed_methods))
322 result.class_initializer_seen =
true;
323 const irep_idt initializer_signature =
325 if(symbol_table.
has_symbol(initializer_signature))
326 methods_to_convert_later.insert(initializer_signature);
328 result.new_method_seen =
true;
337 std::unordered_set<irep_idt>
340 std::unordered_set<irep_idt> methods_to_convert_later;
348 std::vector<irep_idt> reachable_classes;
350 reachable_classes.push_back(this->main_class);
353 for(
const irep_idt &class_name : reachable_classes)
355 const auto &methods =
358 for(
const auto &method : methods)
363 methods_to_convert_later.insert(methodid);
369 return methods_to_convert_later;
381 const std::unordered_set<irep_idt> &entry_points,
385 for(
const auto &mname : entry_points)
387 const auto &symbol=ns.
lookup(mname);
389 for(
const auto ¶m : mtype.parameters())
391 if(param.type().id()==ID_pointer)
417 std::unordered_set<exprt, irep_hash> &result)
445 const exprt &called_function,
446 const std::unordered_set<irep_idt> &instantiated_classes,
447 std::unordered_set<irep_idt> &callable_methods,
452 const auto &call_class=called_function.
get(ID_C_class);
454 !call_class.empty(),
"All virtual calls should be aimed at a class");
455 const auto &call_basename=called_function.
get(ID_component_name);
457 !call_basename.empty(),
458 "Virtual function must have a reasonable name after removing class");
462 self_and_child_classes.push_back(call_class);
464 for(
const irep_idt &class_name : self_and_child_classes)
467 instantiated_classes, call_basename, class_name, symbol_table);
468 if(!method_name.
empty())
469 callable_methods.insert(method_name);
483 if(e.
id()==ID_symbol)
491 if(findit!=symbol_table.
symbols.end() &&
492 findit->second.is_static_lifetime)
494 needed.
add(findit->second);
517 const std::unordered_set<irep_idt> &instantiated_classes,
523 if(!instantiated_classes.count(classname))
528 call_resolver(classname, call_basename,
false);
const irep_idt & get_statement() const
irep_idt name
The unique identifier.
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_tablet &symbol_table, std::unordered_set< irep_idt > &methods_to_convert_later, std::unordered_set< irep_idt > &instantiated_classes, std::unordered_set< exprt, irep_hash > &virtual_function_calls)
Convert a method, add it to the populated set, add needed methods to methods_to_convert_later and add...
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< exprt, irep_hash > &virtual_function_calls, symbol_tablet &symbol_table)
Look for virtual callsites with no candidate targets.
const select_pointer_typet & pointer_type_selector
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.
#define INFLIGHT_EXCEPTION_VARIABLE_NAME
Remove function exceptional returns.
std::function< bool(const irep_idt &function_id, ci_lazy_methods_neededt)> method_convertert
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_tablet &symbol_table)
Find a virtual callee, if one is defined and the callee type is known to exist.
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.
const irep_idt & get_identifier() const
bool is_valid() const
Use to check if this inherited_componentt has been fully constructed.
void gather_virtual_callsites(const exprt &e, std::unordered_set< exprt, irep_hash > &result)
Get places where virtual functions are called.
exprt value
Initial value of symbol.
A struct tag type, i.e., struct_typet with an identifier.
depth_iteratort depth_begin()
#define CHECK_RETURN(CONDITION)
Forward depth-first search iterators These iterators' copy operations are expensive, so use auto&, and avoid std::next(), std::prev() and post-increment iterator.
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...
const irep_idt & id() const
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
void gather_needed_globals(const exprt &e, const symbol_tablet &symbol_table, symbol_tablet &needed)
See output.
irep_idt get_java_class_literal_initializer_signature()
Get the symbol name of java.lang.Class' initializer method.
java_class_loadert & java_class_loader
const irep_idt & get(const irep_namet &name) const
Collect methods needed to be loaded using the lazy method.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define PRECONDITION(CONDITION)
Given a class and a component (either field or method), find the closest parent that defines that com...
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Class that provides messages with a built-in verbosity 'level'.
const synthetic_methods_mapt & synthetic_methods
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
static bool references_class_model(const exprt &expr)
Checks if an expression refers to any class literals (e.g.
const std::vector< load_extra_methodst > & lazy_methods_extra_entry_points
std::vector< irep_idt > idst
bool can_cast_expr< symbol_exprt >(const exprt &base)
message_handlert & get_message_handler()
const java_method_typet & to_java_method_type(const typet &type)
bool contains_method(const irep_idt &method_id) const
mstreamt & result() const
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...
Base class for all expressions.
std::unordered_set< irep_idt > entry_point_methods(const symbol_tablet &symbol_table)
Entry point methods are either:
#define JAVA_CLASS_MODEL_SUFFIX
Class responsible to load .class files.
std::vector< irep_idt > main_jar_classes
const codet & to_code(const exprt &expr)
depth_iteratort depth_end()
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...
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
bool has_suffix(const std::string &s, const std::string &suffix)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
void swap(symbol_tablet &other)
Swap symbol maps between two symbol tables.
const java_bytecode_parse_treet & get_original_class(const irep_idt &class_name)
Data structure for representing an arbitrary statement in a program.
void get_virtual_method_targets(const exprt &called_function, const std::unordered_set< irep_idt > &instantiated_classes, std::unordered_set< irep_idt > &callable_methods, symbol_tablet &symbol_table)
Find possible callees, excluding types that are not known to be instantiated.
idst get_children_trans(const irep_idt &id) const
bool operator()(symbol_tablet &symbol_table, method_bytecodet &method_bytecode, const method_convertert &method_converter)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
irep_idt get_full_component_identifier() const
Get the full name of this function.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
class_hierarchyt class_hierarchy
ci_lazy_methodst(const symbol_tablet &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, message_handlert &message_handler, const synthetic_methods_mapt &synthetic_methods)
Constructor for lazy-method loading.
const code_function_callt & to_code_function_call(const codet &code)
Produce code for simple implementation of String Java libraries.