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 | generate_support_functions (symbol_tablet &symbol_table) override |
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and language-specific library functions. More... | |
bool | typecheck (symbol_tablet &context, const std::string &module) override |
virtual bool | final (symbol_table_baset &context) override |
Final adjustments, e.g. More... | |
void | show_parse (std::ostream &out) override |
virtual | ~java_bytecode_languaget () |
java_bytecode_languaget (std::unique_ptr< select_pointer_typet > pointer_type_selector) | |
java_bytecode_languaget () | |
bool | from_expr (const exprt &expr, std::string &code, const namespacet &ns) override |
Formats the given expression in a language-specific way. More... | |
bool | from_type (const typet &type, std::string &code, const namespacet &ns) override |
Formats the given type in a language-specific way. More... | |
bool | to_expr (const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override |
Parses the given string into an expression. More... | |
std::unique_ptr< 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 | methods_provided (std::unordered_set< irep_idt > &methods) 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 &function_id, symbol_table_baset &symbol_table) 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) |
Encodes the given type in a language-specific way. More... | |
void | set_should_generate_opaque_method_stubs (bool should_generate_stubs) |
Turn on or off stub generation. More... | |
languaget () | |
virtual | ~languaget () |
Protected Member Functions | |
void | convert_single_method (const irep_idt &function_id, symbol_table_baset &symbol_table) |
bool | convert_single_method (const irep_idt &function_id, symbol_table_baset &symbol_table, optionalt< ci_lazy_methods_neededt > needed_lazy_methods) |
Convert a method (one whose type is known but whose body hasn't been converted) but don't run typecheck, etc. More... | |
bool | do_ci_lazy_method_conversion (symbol_tablet &, method_bytecodet &) |
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from the main entry point. More... | |
const select_pointer_typet & | get_pointer_type_selector () const |
![]() | |
void | generate_opaque_method_stubs (symbol_tablet &symbol_table) |
When there are opaque methods (e.g. More... | |
virtual irep_idt | generate_opaque_stub_body (symbolt &symbol, symbol_tablet &symbol_table) |
To generate the stub function for the opaque function in question. More... | |
virtual parameter_symbolt | build_stub_parameter_symbol (const symbolt &function_symbol, size_t parameter_index, const code_typet::parametert ¶meter) |
To build the parameter symbol and choose its name. More... | |
Protected Attributes | |
irep_idt | main_class |
std::vector< irep_idt > | main_jar_classes |
java_class_loadert | java_class_loader |
bool | threading_support |
bool | assume_inputs_non_null |
object_factory_parameterst | object_factory_parameters |
size_t | max_user_array_length |
method_bytecodet | method_bytecode |
lazy_methods_modet | lazy_methods_mode |
std::vector< irep_idt > | lazy_methods_extra_entry_points |
bool | string_refinement_enabled |
bool | throw_runtime_exceptions |
bool | assert_uncaught_exceptions |
bool | throw_assertion_error |
java_string_library_preprocesst | string_preprocess |
std::string | java_cp_include_files |
std::vector< irep_idt > | java_load_classes |
![]() | |
bool | generate_opaque_stubs =false |
bool | language_options_initialized =false |
Private Attributes | |
const std::unique_ptr< const select_pointer_typet > | pointer_type_selector |
synthetic_methods_mapt | synthetic_methods |
Maps synthetic method names on to the particular type of synthetic method (static initializer, initializer wrapper, etc). More... | |
stub_global_initializer_factoryt | stub_global_initializer_factory |
class_hierarchyt | class_hierarchy |
std::unordered_set< std::string > | no_load_classes |
Additional Inherited Members | |
![]() | |
static irep_idt | get_stub_return_symbol_name (const irep_idt &function_id) |
To get the name of the symbol to be used for the return value of the function. More... | |
Definition at line 79 of file java_bytecode_language.h.
|
virtual |
Definition at line 1158 of file java_bytecode_language.cpp.
|
inline |
Definition at line 105 of file java_bytecode_language.h.
|
inline |
Definition at line 115 of file java_bytecode_language.h.
|
overridevirtual |
Promote a lazy-converted method (one whose type is known but whose body hasn't been converted) into a fully-elaborated one.
function_id
, which should be a method provided by this instance of java_bytecode_languaget
to have a value representing the method body identical to that produced using eager method conversion. function_id | method ID to convert |
symtab | global symbol table |
Reimplemented from languaget.
Definition at line 886 of file java_bytecode_language.cpp.
References convert_single_method(), messaget::get_message_handler(), irept::is_not_nil(), java_bytecode_instrument_symbol(), java_bytecode_typecheck_updated_symbols(), symbol_table_baset::lookup_ref(), string_refinement_enabled, throw_runtime_exceptions, and symbolt::value.
Referenced by generate_support_functions().
|
inlineprotected |
Definition at line 152 of file java_bytecode_language.h.
Referenced by convert_lazy_method(), do_ci_lazy_method_conversion(), and typecheck().
|
protected |
Convert a method (one whose type is known but whose body hasn't been converted) but don't run typecheck, etc.
function_id
, which should be a method provided by this instance of java_bytecode_languaget
to have a value representing the method body. function_id | method ID to convert |
symbol_table | global symbol table |
needed_lazy_methods | optionally a collection of needed methods to update with any methods touched during the conversion |
Definition at line 956 of file java_bytecode_language.cpp.
References class_hierarchy, java_string_library_preprocesst::code_for_function(), method_bytecodet::get(), get_clinit_wrapper_body(), messaget::get_message_handler(), get_pointer_type_selector(), stub_global_initializer_factoryt::get_stub_initializer_body(), get_thread_safe_clinit_wrapper_body(), symbol_table_baset::get_writeable_ref(), java_string_library_preprocesst::implements_function(), INVARIANT, class_typet::is_abstract(), irept::is_not_nil(), java_bytecode_convert_method(), java_bytecode_initialize_parameter_names(), symbol_table_baset::lookup_ref(), max_user_array_length, method_bytecode, notify_static_method_calls(), object_factory_parameters, code_typet::return_type(), STATIC_INITIALIZER_WRAPPER, string_preprocess, STUB_CLASS_STATIC_INITIALIZER, stub_global_initializer_factory, synthetic_methods, threading_support, throw_assertion_error, to_code_type(), to_java_class_type(), symbolt::type, and symbolt::value.
|
inlineoverridevirtual |
Reimplemented from languaget.
Definition at line 141 of file java_bytecode_language.h.
|
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).
method_bytecode
: map from method names to relevant symbol and parsed-method objects. Definition at line 802 of file java_bytecode_language.cpp.
References convert_single_method(), messaget::get_message_handler(), get_pointer_type_selector(), java_class_loader, java_load_classes, lazy_methods_extra_entry_points, main_class, main_jar_classes, method_bytecode, and synthetic_methods.
Referenced by typecheck().
|
overridevirtual |
Reimplemented from languaget.
Definition at line 138 of file java_bytecode_language.cpp.
|
overridevirtual |
Final adjustments, e.g.
initializing stub functions and globals that were discovered during function loading
Reimplemented from languaget.
Definition at line 1064 of file java_bytecode_language.cpp.
References languaget::language_options_initialized, and PRECONDITION.
|
overridevirtual |
Formats the given expression in a language-specific way.
expr | the expression to format |
code | the formatted expression |
ns | a namespace |
Reimplemented from languaget.
Definition at line 1093 of file java_bytecode_language.cpp.
References expr2java().
|
overridevirtual |
Formats the given type in a language-specific way.
type | the type to format |
code | the formatted type |
ns | a namespace |
Reimplemented from languaget.
Definition at line 1102 of file java_bytecode_language.cpp.
References exprt::type(), and type2java().
|
overridevirtual |
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and language-specific library functions.
This runs after the typecheck
phase but before lazy function loading. Anything that must wait until lazy function loading is done can be deferred until final
, which runs after lazy function loading is complete. Functions introduced here are visible to lazy loading and can influence its decisions (e.g. picking the types of input parameters and globals), whereas anything introduced during final
cannot.
Implements languaget.
Definition at line 763 of file java_bytecode_language.cpp.
References assert_uncaught_exceptions, assume_inputs_non_null, convert_lazy_method(), get_main_symbol(), messaget::get_message_handler(), get_pointer_type_selector(), main_function_resultt::is_error(), main_function_resultt::is_success(), java_entry_point(), languaget::language_options_initialized, main_class, main_function_resultt::main_function, symbolt::name, object_factory_parameters, PRECONDITION, and string_refinement_enabled.
|
overridevirtual |
Consume options that are java bytecode specific.
Command:line | options |
Reimplemented from languaget.
Definition at line 44 of file java_bytecode_language.cpp.
References jsont::array, assert_uncaught_exceptions, assume_inputs_non_null, configt::javat::classpath, config, DATA_INVARIANT, exception_needed_classes, messaget::get_message_handler(), cmdlinet::get_value(), cmdlinet::get_values(), has_suffix(), jsont::is_array(), jsont::is_object(), jsont::is_string(), cmdlinet::isset(), configt::java, java_cp_include_files, java_load_classes, languaget::language_options_initialized, lazy_methods_extra_entry_points, lazy_methods_mode, LAZY_METHODS_MODE_CONTEXT_INSENSITIVE, LAZY_METHODS_MODE_EAGER, LAZY_METHODS_MODE_EXTERNAL_DRIVER, object_factory_parameterst::max_nondet_array_length, object_factory_parameterst::max_nondet_string_length, object_factory_parameterst::max_nondet_tree_depth, max_user_array_length, no_load_classes, object_factory_parameters, parse_json(), object_factory_parameterst::string_printable, string_refinement_enabled, threading_support, throw_assertion_error, throw_runtime_exceptions, and jsont::value.
|
protected |
Definition at line 829 of file java_bytecode_language.cpp.
References pointer_type_selector, and PRECONDITION.
Referenced by convert_single_method(), do_ci_lazy_method_conversion(), and generate_support_functions().
|
inlineoverridevirtual |
Reimplemented from languaget.
Definition at line 140 of file java_bytecode_language.h.
Referenced by parse().
|
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 840 of file java_bytecode_language.cpp.
References cprover_methods_to_ignore, java_string_library_preprocesst::get_all_function_names(), has_prefix(), id2string(), INVARIANT, method_bytecode, string_preprocess, and synthetic_methods.
|
overridevirtual |
Reimplemented from languaget.
Definition at line 143 of file java_bytecode_language.cpp.
|
inlineoverridevirtual |
Implements languaget.
Definition at line 137 of file java_bytecode_language.h.
|
overridevirtual |
Implements languaget.
Definition at line 158 of file java_bytecode_language.cpp.
References java_class_loadert::add_jar_file(), java_class_loadert::add_load_classes(), config, dstringt::empty(), messaget::eom(), java_class_loadert::file_to_class_name(), java_class_loadert::get_jar_index(), jar_filet::get_manifest(), messaget::get_message_handler(), java_string_library_preprocesst::get_string_type_base_classes(), has_suffix(), id(), java_string_library_preprocesst::initialize_known_type_table(), java_class_loadert::jar_pool(), configt::java, java_class_loader, java_cp_include_files, java_load_classes, languaget::language_options_initialized, java_class_loadert::load_entire_jar(), configt::javat::main_class, main_class, main_jar_classes, PRECONDITION, java_class_loadert::set_extra_class_refs_function(), java_class_loadert::set_java_cp_include_files(), messaget::set_message_handler(), messaget::status(), string_preprocess, string_refinement_enabled, and UNREACHABLE.
|
overridevirtual |
ANSI-C preprocessing.
Reimplemented from languaget.
Definition at line 149 of file java_bytecode_language.cpp.
|
overridevirtual |
Implements languaget.
Definition at line 1070 of file java_bytecode_language.cpp.
References java_class_loader, and main_class.
|
overridevirtual |
Parses the given string into an expression.
code | the string to parse |
module | prefix to be used for identifiers |
expr | the parsed expression |
ns | a namespace |
Implements languaget.
Definition at line 1111 of file java_bytecode_language.cpp.
References java_bytecode_typecheck(), irept::make_nil(), messaget::message_handler, and messaget::result().
|
overridevirtual |
Implements languaget.
Definition at line 578 of file java_bytecode_language.cpp.
References class_hierarchy, convert_single_method(), convert_threadblock(), create_static_initializer_wrappers(), stub_global_initializer_factoryt::create_stub_global_initializer_symbols(), create_stub_global_symbols(), do_ci_lazy_method_conversion(), messaget::eom(), generate_constant_global_variables(), java_class_loadert::get_class_with_overlays_map(), messaget::get_message_handler(), java_string_library_preprocesst::implements_function(), infer_opaque_type_fields(), java_string_library_preprocesst::initialize_conversion_table(), java_bytecode_convert_class(), java_bytecode_instrument(), java_bytecode_typecheck(), java_class_loader, java_internal_additions(), languaget::language_options_initialized, lazy_methods_mode, LAZY_METHODS_MODE_CONTEXT_INSENSITIVE, LAZY_METHODS_MODE_EAGER, mark_java_implicitly_generic_class_type(), max_user_array_length, method_bytecode, no_load_classes, PRECONDITION, messaget::status(), string_preprocess, string_refinement_enabled, stub_global_initializer_factory, symbol_table_baset::symbols, synthetic_methods, threading_support, throw_runtime_exceptions, and messaget::warning().
|
protected |
Definition at line 179 of file java_bytecode_language.h.
Referenced by generate_support_functions(), and get_language_options().
|
protected |
Definition at line 171 of file java_bytecode_language.h.
Referenced by generate_support_functions(), and get_language_options().
|
private |
Definition at line 195 of file java_bytecode_language.h.
Referenced by convert_single_method(), and typecheck().
|
protected |
Definition at line 169 of file java_bytecode_language.h.
Referenced by do_ci_lazy_method_conversion(), parse(), show_parse(), and typecheck().
|
protected |
Definition at line 182 of file java_bytecode_language.h.
Referenced by get_language_options(), and parse().
|
protected |
Definition at line 185 of file java_bytecode_language.h.
Referenced by do_ci_lazy_method_conversion(), get_language_options(), and parse().
|
protected |
Definition at line 176 of file java_bytecode_language.h.
Referenced by do_ci_lazy_method_conversion(), and get_language_options().
|
protected |
Definition at line 175 of file java_bytecode_language.h.
Referenced by get_language_options(), and typecheck().
|
protected |
Definition at line 167 of file java_bytecode_language.h.
Referenced by do_ci_lazy_method_conversion(), generate_support_functions(), parse(), and show_parse().
|
protected |
Definition at line 168 of file java_bytecode_language.h.
Referenced by do_ci_lazy_method_conversion(), and parse().
|
protected |
Definition at line 173 of file java_bytecode_language.h.
Referenced by convert_single_method(), get_language_options(), and typecheck().
|
protected |
Definition at line 174 of file java_bytecode_language.h.
Referenced by convert_single_method(), do_ci_lazy_method_conversion(), methods_provided(), and typecheck().
|
private |
Definition at line 197 of file java_bytecode_language.h.
Referenced by get_language_options(), and typecheck().
|
protected |
Definition at line 172 of file java_bytecode_language.h.
Referenced by convert_single_method(), generate_support_functions(), and get_language_options().
|
private |
Definition at line 188 of file java_bytecode_language.h.
Referenced by get_pointer_type_selector().
|
protected |
Definition at line 181 of file java_bytecode_language.h.
Referenced by convert_single_method(), methods_provided(), parse(), and typecheck().
|
protected |
Definition at line 177 of file java_bytecode_language.h.
Referenced by convert_lazy_method(), generate_support_functions(), get_language_options(), parse(), and typecheck().
|
private |
Definition at line 194 of file java_bytecode_language.h.
Referenced by convert_single_method(), and typecheck().
|
private |
Maps synthetic method names on to the particular type of synthetic method (static initializer, initializer wrapper, etc).
For full documentation see synthetic_method_map.h
Definition at line 193 of file java_bytecode_language.h.
Referenced by convert_single_method(), do_ci_lazy_method_conversion(), methods_provided(), and typecheck().
|
protected |
Definition at line 170 of file java_bytecode_language.h.
Referenced by convert_single_method(), get_language_options(), and typecheck().
|
protected |
Definition at line 180 of file java_bytecode_language.h.
Referenced by convert_single_method(), and get_language_options().
|
protected |
Definition at line 178 of file java_bytecode_language.h.
Referenced by convert_lazy_method(), get_language_options(), and typecheck().