39 if(cmd.
isset(
"java-max-input-array-length"))
41 std::stoi(cmd.
get_value(
"java-max-input-array-length"));
42 if(cmd.
isset(
"java-max-vla-length"))
44 if(cmd.
isset(
"lazy-methods-context-sensitive"))
46 else if(cmd.
isset(
"lazy-methods"))
51 if(cmd.
isset(
"java-cp-include-files"))
62 throw "cannot read JSON input configuration for JAR loading";
65 throw "the JSON file has a wrong format";
66 jsont include_files=json_cp_config[
"jar"];
68 throw "the JSON file has a wrong format";
71 for(
const jsont &file_entry : include_files.
array)
84 return {
"class",
"jar" };
94 std::istream &instream,
95 const std::string &path,
96 std::ostream &outstream)
103 std::istream &instream,
104 const std::string &path)
125 std::string manifest_main_class=manifest[
"Main-Class"];
127 if(manifest_main_class!=
"")
136 status() <<
"JAR file without entry point: loading class files" <<
eom;
169 const std::set<irep_idt> &needed_classes,
175 if(!needed_classes.count(classname))
197 const std::set<irep_idt> &needed_classes,
198 std::vector<irep_idt> &needed_methods,
202 const auto &called_function=c.
function();
203 assert(called_function.id()==ID_virtual_function);
205 const auto &call_class=called_function.
get(ID_C_class);
206 assert(!call_class.empty());
207 const auto &call_basename=called_function.get(ID_component_name);
208 assert(!call_basename.empty());
210 auto old_size=needed_methods.size();
213 for(
const auto &child_class : child_classes)
221 if(!child_method.empty())
222 needed_methods.push_back(child_method);
225 irep_idt parent_class_id=call_class;
234 if(!parent_method.empty())
236 needed_methods.push_back(parent_method);
241 auto findit=class_hierarchy.
class_map.find(parent_class_id);
242 if(findit==class_hierarchy.
class_map.end())
246 const auto &entry=findit->second;
247 if(entry.parents.empty())
250 parent_class_id=entry.parents[0];
255 if(needed_methods.size()==old_size)
260 symbol.
name=stubname;
265 symbol_table.
add(symbol);
275 std::vector<const code_function_callt *> &
result)
298 if(e.
id()==ID_symbol)
305 if(findit!=symbol_table.
symbols.end() &&
306 findit->second.is_static_lifetime)
308 needed.
add(findit->second);
324 const typet &class_type,
329 for(
const auto &field : underlying_type.components())
331 if(field.type().id()==ID_struct || field.type().id()==ID_symbol)
333 else if(field.type().id()==ID_pointer)
336 if(field.type().subtype().id()!=ID_symbol)
338 const auto &field_classid=
355 const std::vector<irep_idt> &entry_points,
360 for(
const auto &mname : entry_points)
362 const auto &symbol=ns.
lookup(mname);
364 for(
const auto ¶m : mtype.parameters())
366 if(param.type().id()==ID_pointer)
368 const auto ¶m_classid=
370 std::vector<irep_idt> class_and_parents=
372 class_and_parents.push_back(param_classid);
373 for(
const auto &classid : class_and_parents)
390 const std::string &module)
396 for(java_class_loadert::class_mapt::const_iterator
401 if(c_it->second.parsed_class.name.empty())
404 debug() <<
"Converting class " << c_it->first <<
eom;
455 std::vector<irep_idt> method_worklist1;
456 std::vector<irep_idt> method_worklist2;
460 if(main_function.stop_convert)
463 std::vector<irep_idt> reachable_classes;
468 for(
const auto &classname : reachable_classes)
472 for(
const auto &method : methods)
477 method_worklist2.push_back(methodid);
482 method_worklist2.push_back(main_function.main_function.name);
484 std::set<irep_idt> needed_classes;
487 std::vector<irep_idt> needed_clinits;
496 initial_lazy_methods);
497 method_worklist2.insert(
498 method_worklist2.end(),
499 needed_clinits.begin(),
500 needed_clinits.end());
503 std::set<irep_idt> methods_already_populated;
504 std::vector<const code_function_callt *> virtual_callsites;
506 bool any_new_methods;
509 any_new_methods=
false;
510 while(!method_worklist2.empty())
512 std::swap(method_worklist1, method_worklist2);
513 for(
const auto &mname : method_worklist1)
515 if(!methods_already_populated.insert(mname).second)
517 auto findit=lazy_methods.find(mname);
518 if(findit==lazy_methods.end())
523 debug() <<
"CI lazy methods: elaborate " << mname <<
eom;
524 const auto &parsed_method=findit->second;
531 *parsed_method.first,
532 *parsed_method.second,
541 any_new_methods=
true;
543 method_worklist1.clear();
549 debug() <<
"CI lazy methods: add virtual method targets (" 550 << virtual_callsites.size()
554 for(
const auto &callsite : virtual_callsites)
565 while(any_new_methods);
570 for(
const auto &sym : symbol_table.
symbols)
572 if(sym.second.is_static_lifetime)
574 if(lazy_methods.count(sym.first) &&
575 !methods_already_populated.count(sym.first))
579 if(sym.second.type.id()==ID_code)
581 keep_symbols.
add(sym.second);
584 debug() <<
"CI lazy methods: removed " 586 <<
" unreachable methods and globals" 589 symbol_table.
swap(keep_symbols);
600 std::set<irep_idt> &methods)
const 603 methods.insert(kv.first);
621 *lazy_method_entry.first,
622 *lazy_method_entry.second,
682 const std::string &code,
683 const std::string &module,
692 std::istringstream i_preprocessed(code);
696 java_bytecode_parser.clear();
697 java_bytecode_parser.filename=
"";
698 java_bytecode_parser.in=&i_preprocessed;
700 java_bytecode_parser.grammar=java_bytecode_parsert::EXPRESSION;
701 java_bytecode_parser.mode=java_bytecode_parsert::GCC;
702 java_bytecode_scanner_init();
704 bool result=java_bytecode_parser.parse();
706 if(java_bytecode_parser.parse_tree.items.empty())
710 expr=java_bytecode_parser.parse_tree.items.front().value();
720 java_bytecode_parser.clear();
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...
const irep_idt & get_statement() const
The type of an expression.
irep_idt name
The unique identifier.
std::string type2java(const typet &type, const namespacet &ns)
const typet & follow(const typet &src) const
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
const std::string & id2string(const irep_idt &d)
lazy_methodst lazy_methods
java_class_loadert java_class_loader
irep_idt mode
Language mode.
std::string java_cp_include_files
void modules_provided(std::set< std::string > &modules) override
void load_entire_jar(java_class_loader_limitt &, const std::string &f)
exprt value
Initial value of symbol.
std::string get_value(char option) const
static void gather_field_types(const typet &class_type, const namespacet &ns, ci_lazy_methodst &lazy_methods)
See output.
size_t max_user_array_length
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void show_parse(std::ostream &out) override
static mstreamt & eom(mstreamt &m)
bool java_bytecode_convert_class(const java_bytecode_parse_treet &parse_tree, symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, lazy_methodst &lazy_methods, lazy_methods_modet lazy_methods_mode, bool string_refinement_enabled, const character_refine_preprocesst &character_preprocess)
bool java_entry_point(symbol_tablet &symbol_table, const irep_idt &main_class, message_handlert &message_handler, bool assume_init_pointers_not_null, size_t max_nondet_array_length)
find entry point and create initialization code for function symbol_table main class message_handler ...
size_t max_nondet_array_length
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
virtual void lazy_methods_provided(std::set< irep_idt > &) const override
Provide feedback to language_filest so that when asked for a lazy method, it can delegate to this ins...
void java_bytecode_convert_method(const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &method, symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, safe_pointer< ci_lazy_methodst > lazy_methods, const character_refine_preprocesst &character_refine)
bool from_expr(const exprt &expr, std::string &code, const namespacet &ns) override
bool assume_inputs_non_null
static irep_idt get_virtual_method_target(const std::set< irep_idt > &needed_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.
JAVA Bytecode Language Type Checking.
const irep_idt & id() const
std::set< std::string > extensions() const override
virtual bool isset(char option) const
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
static std::string file_to_class_name(const std::string &)
character_refine_preprocesst character_preprocess
bool java_bytecode_typecheck(symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
JAVA Bytecode Language Conversion.
virtual void get_language_options(const cmdlinet &) override
Consume options that are java bytecode specific.
void add_jar_file(const std::string &f)
bool typecheck(symbol_tablet &context, const std::string &module) override
static void gather_virtual_callsites(const exprt &e, std::vector< const code_function_callt *> &result)
See output.
virtual bool preprocess(std::istream &instream, const std::string &path, std::ostream &outstream) override
ANSI-C preprocessing.
const irep_idt & get(const irep_namet &name) const
void set_java_cp_include_files(std::string &)
#define forall_operands(it, expr)
virtual void set_message_handler(message_handlert &_message_handler)
struct configt::javat java
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
std::map< irep_idt, lazy_method_valuet > lazy_methodst
main_function_resultt get_main_symbol(symbol_tablet &symbol_table, const irep_idt &main_class, message_handlert &message_handler, bool allow_no_body)
languaget * new_java_bytecode_language()
bool to_expr(const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
bool from_type(const typet &type, std::string &code, const namespacet &ns) override
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
virtual void convert_lazy_method(const irep_idt &id, symbol_tablet &) override
Promote a lazy-converted method (one whose type is known but whose body hasn't been converted) into a...
typet type
Type of symbol.
message_handlert & get_message_handler()
std::map< std::string, std::string > manifestt
bool final(symbol_tablet &context) override
Base class for all expressions.
bool parse(std::istream &instream, const std::string &path) override
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
irep_idt base_name
Base (non-scoped) name.
static void initialize_needed_classes(const std::vector< irep_idt > &entry_points, const namespacet &ns, const class_hierarchyt &ch, ci_lazy_methodst &lazy_methods)
See output.
void initialize_conversion_table()
fill maps with correspondance from java method names to conversion functions
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
bool has_symbol(const irep_idt &name) const
const codet & to_code(const exprt &expr)
java_bytecode_languaget()
bool string_refinement_enabled
bool has_suffix(const std::string &s, const std::string &suffix)
lazy_methods_modet lazy_methods_mode
void swap(symbol_tablet &other)
void java_internal_additions(symbol_tablet &dest)
A statement in a programming language.
JAVA Bytecode Language Conversion.
idst get_children_trans(const irep_idt &id) const
static void gather_needed_globals(const exprt &e, const symbol_tablet &symbol_table, symbol_tablet &needed)
See output.
message_handlert * message_handler
idst get_parents_trans(const irep_idt &id) const
bool do_ci_lazy_method_conversion(symbol_tablet &, lazy_methodst &)
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from th...
std::vector< irep_idt > main_jar_classes
std::string expr2java(const exprt &expr, const namespacet &ns)
const code_function_callt & to_code_function_call(const codet &code)
virtual ~java_bytecode_languaget()
static void get_virtual_method_targets(const code_function_callt &c, const std::set< irep_idt > &needed_classes, std::vector< irep_idt > &needed_methods, symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy)
Find possible callees, excluding types that are not known to be instantiated.