cprover
|
#include <java_bytecode_language.h>
Public Member Functions | |
virtual void | get_language_options (const cmdlinet &) override |
Consume options that are java bytecode specific. More... | |
virtual bool | preprocess (std::istream &instream, const std::string &path, std::ostream &outstream) override |
ANSI-C preprocessing. More... | |
bool | parse (std::istream &instream, const std::string &path) override |
bool | typecheck (symbol_tablet &context, const std::string &module) override |
bool | final (symbol_tablet &context) override |
void | show_parse (std::ostream &out) override |
virtual | ~java_bytecode_languaget () |
java_bytecode_languaget () | |
bool | from_expr (const exprt &expr, std::string &code, const namespacet &ns) override |
bool | from_type (const typet &type, std::string &code, const namespacet &ns) override |
bool | to_expr (const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override |
languaget * | new_language () override |
std::string | id () const override |
std::string | description () const override |
std::set< std::string > | extensions () const override |
void | modules_provided (std::set< std::string > &modules) override |
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 instance of java_bytecode_languaget. More... | |
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 fully- elaborated one. More... | |
![]() | |
virtual void | dependencies (const std::string &module, std::set< std::string > &modules) |
virtual bool | interfaces (symbol_tablet &symbol_table) |
virtual bool | type_to_name (const typet &type, std::string &name, const namespacet &ns) |
languaget () | |
virtual | ~languaget () |
Protected Member Functions | |
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 the main entry point. More... | |
Protected Attributes | |
irep_idt | main_class |
std::vector< irep_idt > | main_jar_classes |
java_class_loadert | java_class_loader |
bool | assume_inputs_non_null |
size_t | max_nondet_array_length |
size_t | max_user_array_length |
lazy_methodst | lazy_methods |
lazy_methods_modet | lazy_methods_mode |
bool | string_refinement_enabled |
character_refine_preprocesst | character_preprocess |
std::string | java_cp_include_files |
Additional Inherited Members |
Definition at line 37 of file java_bytecode_language.h.
|
virtual |
Definition at line 728 of file java_bytecode_language.cpp.
|
inline |
Definition at line 61 of file java_bytecode_language.h.
References from_expr(), from_type(), and to_expr().
Referenced by new_java_bytecode_language(), and new_language().
|
overridevirtual |
Promote a lazy-converted method (one whose type is known but whose body hasn't been converted) into a fully- elaborated one.
symtab
: global symbol table id
, which should be a lazy method provided by this instance of java_bytecode_languaget
. It should initially have a nil value. After this method completes, it will have a value representing the method body, identical to that produced using eager method conversion. Reimplemented from languaget.
Definition at line 615 of file java_bytecode_language.cpp.
References character_preprocess, messaget::get_message_handler(), java_bytecode_convert_method(), lazy_methods, and max_user_array_length.
Referenced by description().
|
inlineoverridevirtual |
Reimplemented from languaget.
Definition at line 86 of file java_bytecode_language.h.
References convert_lazy_method(), do_ci_lazy_method_conversion(), extensions(), lazy_methods_provided(), and modules_provided().
|
protected |
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from the main entry point.
In brief, static methods are reachable if we find a callsite in another reachable site, while virtual methods are reachable if we find a virtual callsite targeting a compatible type and a constructor callsite indicating an object of that type may be instantiated (or evidence that an object of that type exists before the main function is entered, such as being passed as a parameter).
lazy_methods
: map from method names to relevant symbol and parsed-method objects. Definition at line 448 of file java_bytecode_language.cpp.
References symbol_tablet::add(), character_preprocess, java_class_loadert::class_map, messaget::debug(), dstringt::empty(), messaget::eom(), gather_needed_globals(), gather_virtual_callsites(), get_main_symbol(), messaget::get_message_handler(), get_virtual_method_targets(), id2string(), initialize_needed_classes(), java_bytecode_convert_method(), java_class_loader, lazy_methods, symbol_tablet::lookup(), main_class, main_jar_classes, max_user_array_length, symbol_tablet::swap(), symbol_tablet::symbols, and symbolt::value.
Referenced by description(), and typecheck().
|
overridevirtual |
Reimplemented from languaget.
Definition at line 82 of file java_bytecode_language.cpp.
Referenced by description().
|
overridevirtual |
Reimplemented from languaget.
Definition at line 629 of file java_bytecode_language.cpp.
References assume_inputs_non_null, main_function_resultt::error_found, get_main_symbol(), messaget::get_message_handler(), java_entry_point(), java_internal_additions(), main_class, main_function_resultt::main_function, max_nondet_array_length, and main_function_resultt::stop_convert.
|
overridevirtual |
Reimplemented from languaget.
Definition at line 663 of file java_bytecode_language.cpp.
References expr2java().
Referenced by java_bytecode_languaget().
|
overridevirtual |
Reimplemented from languaget.
Definition at line 672 of file java_bytecode_language.cpp.
References type2java().
Referenced by java_bytecode_languaget().
|
overridevirtual |
Consume options that are java bytecode specific.
Command:line | options |
Reimplemented from languaget.
Definition at line 35 of file java_bytecode_language.cpp.
References jsont::array, assume_inputs_non_null, configt::javat::classpath, config, messaget::get_message_handler(), cmdlinet::get_value(), has_suffix(), jsont::is_array(), jsont::is_object(), jsont::is_string(), cmdlinet::isset(), configt::java, java_cp_include_files, lazy_methods_mode, LAZY_METHODS_MODE_CONTEXT_INSENSITIVE, LAZY_METHODS_MODE_CONTEXT_SENSITIVE, LAZY_METHODS_MODE_EAGER, max_nondet_array_length, max_user_array_length, parse_json(), string_refinement_enabled, and jsont::value.
|
inlineoverridevirtual |
Reimplemented from languaget.
Definition at line 85 of file java_bytecode_language.h.
|
overridevirtual |
Provide feedback to language_filest
so that when asked for a lazy method, it can delegate to this instance of java_bytecode_languaget.
methods
with the complete list of lazy methods that are available to convert (those which are valid parameters for convert_lazy_method
) Reimplemented from languaget.
Definition at line 599 of file java_bytecode_language.cpp.
References lazy_methods.
Referenced by description().
|
overridevirtual |
Reimplemented from languaget.
Definition at line 87 of file java_bytecode_language.cpp.
Referenced by description().
|
inlineoverridevirtual |
Implements languaget.
Definition at line 82 of file java_bytecode_language.h.
References java_bytecode_languaget().
|
overridevirtual |
Implements languaget.
Definition at line 102 of file java_bytecode_language.cpp.
References java_class_loadert::add_jar_file(), config, dstringt::empty(), messaget::eom(), java_class_loadert::file_to_class_name(), messaget::get_message_handler(), has_suffix(), java_class_loadert::jar_map, java_class_loadert::jar_pool, configt::java, java_class_loader, java_cp_include_files, java_class_loadert::load_entire_jar(), main_class, configt::javat::main_class, main_jar_classes, java_class_loadert::set_java_cp_include_files(), messaget::set_message_handler(), and messaget::status().
|
overridevirtual |
ANSI-C preprocessing.
Reimplemented from languaget.
Definition at line 93 of file java_bytecode_language.cpp.
|
overridevirtual |
Implements languaget.
Definition at line 653 of file java_bytecode_language.cpp.
References java_class_loader, and main_class.
|
overridevirtual |
Implements languaget.
Definition at line 681 of file java_bytecode_language.cpp.
References java_bytecode_typecheck(), irept::make_nil(), messaget::message_handler, and messaget::result().
Referenced by java_bytecode_languaget().
|
overridevirtual |
Implements languaget.
Definition at line 388 of file java_bytecode_language.cpp.
References character_preprocess, java_class_loadert::class_map, messaget::debug(), do_ci_lazy_method_conversion(), messaget::eom(), messaget::get_message_handler(), character_refine_preprocesst::initialize_conversion_table(), java_bytecode_convert_class(), java_bytecode_typecheck(), java_class_loader, lazy_methods, lazy_methods_mode, LAZY_METHODS_MODE_CONTEXT_INSENSITIVE, max_user_array_length, and string_refinement_enabled.
|
protected |
Definition at line 100 of file java_bytecode_language.h.
Referenced by final(), and get_language_options().
|
protected |
Definition at line 106 of file java_bytecode_language.h.
Referenced by convert_lazy_method(), do_ci_lazy_method_conversion(), and typecheck().
|
protected |
Definition at line 99 of file java_bytecode_language.h.
Referenced by do_ci_lazy_method_conversion(), parse(), show_parse(), and typecheck().
|
protected |
Definition at line 107 of file java_bytecode_language.h.
Referenced by get_language_options(), and parse().
|
protected |
Definition at line 103 of file java_bytecode_language.h.
Referenced by convert_lazy_method(), do_ci_lazy_method_conversion(), gather_field_types(), initialize_needed_classes(), lazy_methods_provided(), and typecheck().
|
protected |
Definition at line 104 of file java_bytecode_language.h.
Referenced by get_language_options(), and typecheck().
|
protected |
Definition at line 97 of file java_bytecode_language.h.
Referenced by do_ci_lazy_method_conversion(), final(), parse(), and show_parse().
|
protected |
Definition at line 98 of file java_bytecode_language.h.
Referenced by do_ci_lazy_method_conversion(), and parse().
|
protected |
Definition at line 101 of file java_bytecode_language.h.
Referenced by final(), and get_language_options().
|
protected |
Definition at line 102 of file java_bytecode_language.h.
Referenced by convert_lazy_method(), do_ci_lazy_method_conversion(), get_language_options(), and typecheck().
|
protected |
Definition at line 105 of file java_bytecode_language.h.
Referenced by get_language_options(), and typecheck().