36 const std::vector<irep_idt> &main_jar_classes,
37 const std::vector<irep_idt> &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 =
108 methods_to_convert_later.insert(
109 extra_entry_points.begin(), extra_entry_points.end());
111 std::unordered_set<irep_idt> instantiated_classes;
114 std::unordered_set<irep_idt> initial_callable_methods;
116 initial_callable_methods,
117 instantiated_classes,
121 methods_to_convert_later,
namespacet(symbol_table), initial_lazy_methods);
122 methods_to_convert_later.insert(
123 initial_callable_methods.begin(), initial_callable_methods.end());
126 std::unordered_set<irep_idt> methods_already_populated;
127 std::unordered_set<exprt, irep_hash> virtual_function_calls;
128 bool class_initializer_seen =
false;
130 bool any_new_classes =
true;
131 while(any_new_classes)
133 bool any_new_methods =
true;
134 while(any_new_methods)
136 any_new_methods =
false;
137 while(!methods_to_convert_later.empty())
139 std::unordered_set<irep_idt> methods_to_convert;
140 std::swap(methods_to_convert, methods_to_convert_later);
141 for(
const auto &mname : methods_to_convert)
145 methods_already_populated,
146 class_initializer_seen,
149 methods_to_convert_later,
150 instantiated_classes,
151 virtual_function_calls);
152 any_new_methods |= conversion_result.new_method_seen;
153 class_initializer_seen |= conversion_result.class_initializer_seen;
160 debug() <<
"CI lazy methods: add virtual method targets (" 161 << virtual_function_calls.size() <<
" callsites)" <<
eom;
163 for(
const exprt &
function : virtual_function_calls)
167 instantiated_classes,
168 methods_to_convert_later,
174 methods_to_convert_later,
175 instantiated_classes,
176 virtual_function_calls,
186 for(
const auto &sym : symbol_table.
symbols)
190 if(sym.second.is_static_lifetime)
192 if(sym.second.type.id()==ID_code)
199 !methods_already_populated.count(sym.first))
206 keep_symbols.
add(sym.second);
209 debug() <<
"CI lazy methods: removed " 211 <<
" unreachable methods and globals" <<
eom;
213 symbol_table.
swap(keep_symbols);
226 std::unordered_set<irep_idt> &methods_to_convert_later,
227 std::unordered_set<irep_idt> &instantiated_classes,
228 const std::unordered_set<exprt, irep_hash> &virtual_function_calls,
231 bool any_new_classes =
false;
232 for(
const exprt &virtual_function_call : virtual_function_calls)
234 std::unordered_set<irep_idt> candidate_target_methods;
236 virtual_function_call,
237 instantiated_classes,
238 candidate_target_methods,
241 if(!candidate_target_methods.empty())
246 const irep_idt &call_class = virtual_function_call.get(ID_C_class);
247 auto ret_class = instantiated_classes.insert(call_class);
249 any_new_classes =
true;
253 virtual_function_call.get(ID_component_name);
255 instantiated_classes, call_basename, call_class, symbol_table);
259 methods_to_convert_later.insert(method_name);
261 return any_new_classes;
276 std::unordered_set<irep_idt> &methods_already_populated,
277 const bool class_initializer_already_seen,
280 std::unordered_set<irep_idt> &methods_to_convert_later,
281 std::unordered_set<irep_idt> &instantiated_classes,
282 std::unordered_set<exprt, irep_hash> &virtual_function_calls)
285 if(!methods_already_populated.insert(method_name).second)
288 debug() <<
"CI lazy methods: elaborate " << method_name <<
eom;
293 methods_to_convert_later,
294 instantiated_classes,
298 const bool could_not_convert_function =
299 method_converter(method_name, needed_methods);
300 if(could_not_convert_function)
308 result.class_initializer_seen =
true;
309 const irep_idt initializer_signature =
311 if(symbol_table.
has_symbol(initializer_signature))
312 methods_to_convert_later.insert(initializer_signature);
314 result.new_method_seen =
true;
323 std::unordered_set<irep_idt>
326 std::unordered_set<irep_idt> methods_to_convert_later;
334 std::vector<irep_idt> reachable_classes;
336 reachable_classes.push_back(this->main_class);
339 for(
const irep_idt &class_name : reachable_classes)
341 const auto &methods =
344 for(
const auto &method : methods)
349 methods_to_convert_later.insert(methodid);
355 return methods_to_convert_later;
366 std::vector<irep_idt> &methods,
369 std::vector<irep_idt> new_methods;
370 for(
const irep_idt &method : methods)
372 const std::string &method_str=
id2string(method);
375 std::string error_message;
382 throw "entry point "+error_message;
383 new_methods.push_back(internal_name);
387 irep_idt classname=
"java::"+method_str.substr(0, method_str.length()-2);
389 throw "wildcard entry point '"+method_str+
"': unknown class";
391 for(
const auto &name_symbol : symbol_table.
symbols)
393 if(name_symbol.second.type.id()!=ID_code)
398 new_methods.push_back(name_symbol.first);
403 methods=std::move(new_methods);
415 const std::unordered_set<irep_idt> &entry_points,
419 for(
const auto &mname : entry_points)
421 const auto &symbol=ns.
lookup(mname);
423 for(
const auto ¶m : mtype.parameters())
425 if(param.type().id()==ID_pointer)
452 std::unordered_set<exprt, irep_hash> &result)
480 const exprt &called_function,
481 const std::unordered_set<irep_idt> &instantiated_classes,
482 std::unordered_set<irep_idt> &callable_methods,
487 const auto &call_class=called_function.
get(ID_C_class);
489 !call_class.empty(),
"All virtual calls should be aimed at a class");
490 const auto &call_basename=called_function.
get(ID_component_name);
492 !call_basename.empty(),
493 "Virtual function must have a reasonable name after removing class");
497 self_and_child_classes.push_back(call_class);
499 for(
const irep_idt &class_name : self_and_child_classes)
502 instantiated_classes, call_basename, class_name, symbol_table);
503 if(!method_name.
empty())
504 callable_methods.insert(method_name);
518 if(e.
id()==ID_symbol)
526 if(findit!=symbol_table.
symbols.end() &&
527 findit->second.is_static_lifetime)
529 needed.
add(findit->second);
552 const std::unordered_set<irep_idt> &instantiated_classes,
558 if(!instantiated_classes.count(classname))
563 call_resolver(classname, call_basename,
false);
const irep_idt & get_statement() const
irep_idt name
The unique identifier.
ci_lazy_methodst(const symbol_tablet &symbol_table, const irep_idt &main_class, const std::vector< irep_idt > &main_jar_classes, const std::vector< irep_idt > &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.
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
void resolve_method_names(std::vector< irep_idt > &methods, const symbol_tablet &symbol_table)
Translates the given list of method names from human-readable to internal syntax. ...
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.
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
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)
std::vector< irep_idt > lazy_methods_extra_entry_points
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...
bool has_prefix(const std::string &s, const std::string &prefix)
#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
irep_idt resolve_friendly_method_name(const std::string &friendly_name, const symbol_table_baset &symbol_table, std::string &error)
Resolves a user-friendly method name (like packagename.Class.method) into an internal name (like java...
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.
std::vector< irep_idt > idst
bool can_cast_expr< symbol_exprt >(const exprt &base)
message_handlert & get_message_handler()
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
const code_function_callt & to_code_function_call(const codet &code)
Produce code for simple implementation of String Java libraries.