36 const std::vector<irep_idt> &main_jar_classes,
37 const std::vector<load_extra_methodst> &lazy_methods_extra_entry_points,
39 const std::vector<irep_idt> &extra_instantiated_classes,
44 main_class(main_class),
45 main_jar_classes(main_jar_classes),
46 lazy_methods_extra_entry_points(lazy_methods_extra_entry_points),
47 java_class_loader(java_class_loader),
48 extra_instantiated_classes(extra_instantiated_classes),
49 pointer_type_selector(pointer_type_selector),
50 synthetic_methods(synthetic_methods)
64 static const symbol_typet class_type(
"java::java.lang.Class");
69 it->type() == class_type &&
101 std::unordered_set<irep_idt> methods_to_convert_later =
106 std::vector<irep_idt> extra_entry_points;
109 const auto &extra_methods = extra_function_generator(symbol_table);
110 extra_entry_points.insert(
111 extra_entry_points.end(), extra_methods.begin(), extra_methods.end());
113 methods_to_convert_later.insert(
114 extra_entry_points.begin(), extra_entry_points.end());
116 std::unordered_set<irep_idt> instantiated_classes;
119 std::unordered_set<irep_idt> initial_callable_methods;
121 initial_callable_methods,
122 instantiated_classes,
126 methods_to_convert_later,
namespacet(symbol_table), initial_lazy_methods);
127 methods_to_convert_later.insert(
128 initial_callable_methods.begin(), initial_callable_methods.end());
131 std::unordered_set<irep_idt> methods_already_populated;
132 std::unordered_set<exprt, irep_hash> virtual_function_calls;
133 bool class_initializer_seen =
false;
135 bool any_new_classes =
true;
136 while(any_new_classes)
138 bool any_new_methods =
true;
139 while(any_new_methods)
141 any_new_methods =
false;
142 while(!methods_to_convert_later.empty())
144 std::unordered_set<irep_idt> methods_to_convert;
145 std::swap(methods_to_convert, methods_to_convert_later);
146 for(
const auto &mname : methods_to_convert)
150 methods_already_populated,
151 class_initializer_seen,
154 methods_to_convert_later,
155 instantiated_classes,
156 virtual_function_calls);
157 any_new_methods |= conversion_result.new_method_seen;
158 class_initializer_seen |= conversion_result.class_initializer_seen;
165 debug() <<
"CI lazy methods: add virtual method targets (" 166 << virtual_function_calls.size() <<
" callsites)" <<
eom;
168 for(
const exprt &
function : virtual_function_calls)
172 instantiated_classes,
173 methods_to_convert_later,
179 methods_to_convert_later,
180 instantiated_classes,
181 virtual_function_calls,
191 for(
const auto &sym : symbol_table.
symbols)
195 if(sym.second.is_static_lifetime)
197 if(sym.second.type.id()==ID_code)
204 !methods_already_populated.count(sym.first))
211 keep_symbols.
add(sym.second);
214 debug() <<
"CI lazy methods: removed " 216 <<
" unreachable methods and globals" <<
eom;
218 symbol_table.
swap(keep_symbols);
231 std::unordered_set<irep_idt> &methods_to_convert_later,
232 std::unordered_set<irep_idt> &instantiated_classes,
233 const std::unordered_set<exprt, irep_hash> &virtual_function_calls,
236 bool any_new_classes =
false;
237 for(
const exprt &virtual_function_call : virtual_function_calls)
239 std::unordered_set<irep_idt> candidate_target_methods;
241 virtual_function_call,
242 instantiated_classes,
243 candidate_target_methods,
246 if(!candidate_target_methods.empty())
251 const irep_idt &call_class = virtual_function_call.get(ID_C_class);
252 auto ret_class = instantiated_classes.insert(call_class);
254 any_new_classes =
true;
258 virtual_function_call.get(ID_component_name);
260 instantiated_classes, call_basename, call_class, symbol_table);
264 methods_to_convert_later.insert(method_name);
266 return any_new_classes;
281 std::unordered_set<irep_idt> &methods_already_populated,
282 const bool class_initializer_already_seen,
285 std::unordered_set<irep_idt> &methods_to_convert_later,
286 std::unordered_set<irep_idt> &instantiated_classes,
287 std::unordered_set<exprt, irep_hash> &virtual_function_calls)
290 if(!methods_already_populated.insert(method_name).second)
293 debug() <<
"CI lazy methods: elaborate " << method_name <<
eom;
298 methods_to_convert_later,
299 instantiated_classes,
303 const bool could_not_convert_function =
304 method_converter(method_name, needed_methods);
305 if(could_not_convert_function)
313 result.class_initializer_seen =
true;
314 const irep_idt initializer_signature =
316 if(symbol_table.
has_symbol(initializer_signature))
317 methods_to_convert_later.insert(initializer_signature);
319 result.new_method_seen =
true;
328 std::unordered_set<irep_idt>
331 std::unordered_set<irep_idt> methods_to_convert_later;
339 std::vector<irep_idt> reachable_classes;
341 reachable_classes.push_back(this->main_class);
344 for(
const irep_idt &class_name : reachable_classes)
346 const auto &methods =
349 for(
const auto &method : methods)
354 methods_to_convert_later.insert(methodid);
360 return methods_to_convert_later;
372 const std::unordered_set<irep_idt> &entry_points,
376 for(
const auto &mname : entry_points)
378 const auto &symbol=ns.
lookup(mname);
380 for(
const auto ¶m : mtype.parameters())
382 if(param.type().id()==ID_pointer)
409 std::unordered_set<exprt, irep_hash> &result)
437 const exprt &called_function,
438 const std::unordered_set<irep_idt> &instantiated_classes,
439 std::unordered_set<irep_idt> &callable_methods,
444 const auto &call_class=called_function.
get(ID_C_class);
446 !call_class.empty(),
"All virtual calls should be aimed at a class");
447 const auto &call_basename=called_function.
get(ID_component_name);
449 !call_basename.empty(),
450 "Virtual function must have a reasonable name after removing class");
454 self_and_child_classes.push_back(call_class);
456 for(
const irep_idt &class_name : self_and_child_classes)
459 instantiated_classes, call_basename, class_name, symbol_table);
460 if(!method_name.
empty())
461 callable_methods.insert(method_name);
475 if(e.
id()==ID_symbol)
483 if(findit!=symbol_table.
symbols.end() &&
484 findit->second.is_static_lifetime)
486 needed.
add(findit->second);
509 const std::unordered_set<irep_idt> &instantiated_classes,
515 if(!instantiated_classes.count(classname))
520 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.
depth_iteratort depth_begin()
#define CHECK_RETURN(CONDITION)
static mstreamt & eom(mstreamt &m)
#define INVARIANT(CONDITION, REASON)
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
A reference into the symbol table.
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.
#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 a generic exprt to a symbol_exprt.
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
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 generic typet to a pointer_typet.
goto_programt coverage_criteriont message_handlert & message_handler
void swap(symbol_tablet &other)
const java_bytecode_parse_treet & get_original_class(const irep_idt &class_name)
A statement in a programming language.
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 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.