cprover
|
#include <java_bytecode_language.h>
Public Member Functions | |
void | set_language_options (const optionst &) 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 |
We set the main class (i.e. class to start the class loading analysis from, see java_class_loadert) depending on the file type of path . More... | |
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... | |
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 |
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 |
java_object_factory_parameterst | object_factory_parameters |
size_t | max_user_array_length |
method_bytecodet | method_bytecode |
lazy_methods_modet | lazy_methods_mode |
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 |
bool | nondet_static |
std::vector< irep_idt > | java_load_classes |
![]() | |
bool | language_options_initialized =false |
system_library_symbolst | system_symbols |
Private Member Functions | |
virtual std::vector< load_extra_methodst > | build_extra_entry_points (const optionst &) const |
This method should be overloaded to provide alternative approaches for specifying extra entry points. More... | |
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 |
std::vector< load_extra_methodst > | extra_methods |
Additional Inherited Members |
Definition at line 88 of file java_bytecode_language.h.
|
virtual |
Definition at line 1259 of file java_bytecode_language.cpp.
|
inline |
Definition at line 114 of file java_bytecode_language.h.
|
inline |
Definition at line 125 of file java_bytecode_language.h.
|
privatevirtual |
This method should be overloaded to provide alternative approaches for specifying extra entry points.
To provide a regex entry point, the command line option --lazy-methods-extra-entry-point
can be used directly.
Definition at line 1267 of file java_bytecode_language.cpp.
|
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 973 of file java_bytecode_language.cpp.
|
inlineprotected |
Definition at line 162 of file java_bytecode_language.h.
|
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 1043 of file java_bytecode_language.cpp.
|
inlineoverridevirtual |
Reimplemented from languaget.
Definition at line 151 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 886 of file java_bytecode_language.cpp.
|
overridevirtual |
Reimplemented from languaget.
Definition at line 182 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 1159 of file java_bytecode_language.cpp.
|
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 1188 of file java_bytecode_language.cpp.
|
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 1197 of file java_bytecode_language.cpp.
|
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 844 of file java_bytecode_language.cpp.
|
protected |
Definition at line 916 of file java_bytecode_language.cpp.
|
inlineoverridevirtual |
Reimplemented from languaget.
Definition at line 150 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 927 of file java_bytecode_language.cpp.
|
overridevirtual |
Reimplemented from languaget.
Definition at line 187 of file java_bytecode_language.cpp.
|
inlineoverridevirtual |
Implements languaget.
Definition at line 147 of file java_bytecode_language.h.
|
overridevirtual |
We set the main class (i.e. class to start the class loading analysis from, see java_class_loadert) depending on the file type of path
.
path
can be the name of either a .class file or a .jar file. If it is a .class file, the top-level class in this file is the main class. If it is a .jar file, we first check for the main class in three steps 1) the argument of the –main-class command-line option, 2) the class implied by the argument of the –function option, 3) the manifest file of the JAR. If no main class was found, all classes in the JAR file are loaded.
Implements languaget.
Definition at line 211 of file java_bytecode_language.cpp.
|
overridevirtual |
ANSI-C preprocessing.
Reimplemented from languaget.
Definition at line 193 of file java_bytecode_language.cpp.
|
overridevirtual |
Consume options that are java bytecode specific.
Reimplemented from languaget.
Definition at line 91 of file java_bytecode_language.cpp.
|
overridevirtual |
Implements languaget.
Definition at line 1165 of file java_bytecode_language.cpp.
|
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 1206 of file java_bytecode_language.cpp.
|
overridevirtual |
Implements languaget.
Definition at line 648 of file java_bytecode_language.cpp.
|
protected |
Definition at line 188 of file java_bytecode_language.h.
|
protected |
Definition at line 181 of file java_bytecode_language.h.
|
private |
Definition at line 207 of file java_bytecode_language.h.
|
private |
Definition at line 211 of file java_bytecode_language.h.
|
protected |
Definition at line 179 of file java_bytecode_language.h.
|
protected |
Definition at line 191 of file java_bytecode_language.h.
|
protected |
Definition at line 195 of file java_bytecode_language.h.
|
protected |
Definition at line 185 of file java_bytecode_language.h.
|
protected |
Definition at line 177 of file java_bytecode_language.h.
|
protected |
Definition at line 178 of file java_bytecode_language.h.
|
protected |
Definition at line 183 of file java_bytecode_language.h.
|
protected |
Definition at line 184 of file java_bytecode_language.h.
|
private |
Definition at line 209 of file java_bytecode_language.h.
|
protected |
Definition at line 192 of file java_bytecode_language.h.
|
protected |
Definition at line 182 of file java_bytecode_language.h.
|
private |
Definition at line 200 of file java_bytecode_language.h.
|
protected |
Definition at line 190 of file java_bytecode_language.h.
|
protected |
Definition at line 186 of file java_bytecode_language.h.
|
private |
Definition at line 206 of file java_bytecode_language.h.
|
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 205 of file java_bytecode_language.h.
|
protected |
Definition at line 180 of file java_bytecode_language.h.
|
protected |
Definition at line 189 of file java_bytecode_language.h.
|
protected |
Definition at line 187 of file java_bytecode_language.h.