cprover
|
#include <java_bytecode_language.h>
Public Member Functions | |
void | set_language_options (const optionst &) override |
Consume options that are java bytecode specific. | |
void | set_message_handler (message_handlert &message_handler) override |
virtual bool | preprocess (std::istream &instream, const std::string &path, std::ostream &outstream) override |
ANSI-C preprocessing. | |
virtual bool | parse () |
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when we have have been given a main class. | |
bool | parse (std::istream &instream, const std::string &path) override |
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when we have a JAR file given via the -jar option: a) the argument of the –main-class command-line option, b) the manifest file of the JAR If no main class was found, all classes in the JAR file are loaded. | |
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. | |
bool | typecheck (symbol_tablet &context, const std::string &module) override |
virtual bool | final (symbol_table_baset &context) override |
Final adjustments, e.g. | |
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. | |
bool | from_type (const typet &type, std::string &code, const namespacet &ns) override |
Formats the given type in a language-specific way. | |
bool | to_expr (const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override |
Parses the given string into an expression. | |
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. | |
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. | |
![]() | |
virtual void | set_language_options (const optionst &) |
Set language-specific options. | |
virtual bool | preprocess (std::istream &instream, const std::string &path, std::ostream &outstream) |
virtual bool | parse (std::istream &instream, const std::string &path)=0 |
virtual bool | generate_support_functions (symbol_tablet &symbol_table)=0 |
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and language-specific library functions. | |
virtual void | dependencies (const std::string &module, std::set< std::string > &modules) |
virtual void | modules_provided (std::set< std::string > &modules) |
virtual void | methods_provided (std::unordered_set< irep_idt > &methods) const |
Should fill methods with the symbol identifiers of all methods this languaget can provide a body for, but doesn't populate that body in languaget::typecheck (i.e. | |
virtual void | convert_lazy_method (const irep_idt &function_id, symbol_table_baset &symbol_table) |
Requests this languaget should populate the body of method function_id in symbol_table . | |
virtual bool | final (symbol_table_baset &symbol_table) |
Final adjustments, e.g. | |
virtual bool | interfaces (symbol_tablet &symbol_table) |
virtual bool | typecheck (symbol_tablet &symbol_table, const std::string &module)=0 |
virtual bool | can_keep_file_local () |
Is it possible to call three-argument typecheck() on this object? | |
virtual bool | typecheck (symbol_tablet &symbol_table, const std::string &module, const bool keep_file_local) |
typecheck without removing specified entries from the symbol table | |
virtual std::string | id () const =0 |
virtual std::string | description () const =0 |
virtual std::set< std::string > | extensions () const =0 |
virtual void | show_parse (std::ostream &out)=0 |
virtual bool | from_expr (const exprt &expr, std::string &code, const namespacet &ns) |
Formats the given expression in a language-specific way. | |
virtual bool | from_type (const typet &type, std::string &code, const namespacet &ns) |
Formats the given type in a language-specific way. | |
virtual bool | type_to_name (const typet &type, std::string &name, const namespacet &ns) |
Encodes the given type in a language-specific way. | |
virtual bool | to_expr (const std::string &code, const std::string &module, exprt &expr, const namespacet &ns)=0 |
Parses the given string into an expression. | |
virtual std::unique_ptr< languaget > | new_language ()=0 |
languaget () | |
virtual | ~languaget () |
Protected Member Functions | |
void | convert_single_method (const irep_idt &function_id, symbol_table_baset &symbol_table, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols) |
bool | convert_single_method (const irep_idt &function_id, symbol_table_baset &symbol_table, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols) |
Convert a method (one whose type is known but whose body hasn't been converted) if it doesn't already have a body, and lift clinit calls if requested by the user. | |
bool | convert_single_method_code (const irep_idt &function_id, symbol_table_baset &symbol_table, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols) |
Convert a method (one whose type is known but whose body hasn't been converted) but don't run typecheck, etc. | |
bool | do_ci_lazy_method_conversion (symbol_tablet &) |
Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from the main entry point. | |
const select_pointer_typet & | get_pointer_type_selector () const |
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. | |
void | parse_from_main_class () |
void | initialize_class_loader () |
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). | |
stub_global_initializer_factoryt | stub_global_initializer_factory |
class_hierarchyt | class_hierarchy |
std::unordered_map< std::string, object_creation_referencet > | references |
Map used in all calls to functions that deterministically create objects (currently only assign_from_json). | |
Additional Inherited Members |
Definition at line 272 of file java_bytecode_language.h.
|
virtual |
Definition at line 1599 of file java_bytecode_language.cpp.
|
inline |
Definition at line 306 of file java_bytecode_language.h.
|
inline |
Definition at line 313 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 1607 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 1185 of file java_bytecode_language.cpp.
|
inlineprotected |
Definition at line 350 of file java_bytecode_language.h.
|
protected |
Convert a method (one whose type is known but whose body hasn't been converted) if it doesn't already have a body, and lift clinit calls if requested by the user.
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 |
class_to_declared_symbols | maps classes to the symbols that they declare. |
Definition at line 1282 of file java_bytecode_language.cpp.
|
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 |
class_to_declared_symbols | maps classes to the symbols that they declare. |
Definition at line 1335 of file java_bytecode_language.cpp.
|
inlineoverridevirtual |
Implements languaget.
Definition at line 339 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).
symbol_table | global symbol table |
Definition at line 1116 of file java_bytecode_language.cpp.
|
overridevirtual |
Implements languaget.
Definition at line 271 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 1499 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 1528 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 1537 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 1056 of file java_bytecode_language.cpp.
|
protected |
Definition at line 1150 of file java_bytecode_language.cpp.
|
inlineoverridevirtual |
Implements languaget.
Definition at line 338 of file java_bytecode_language.h.
|
private |
Definition at line 297 of file java_bytecode_language.cpp.
|
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 1161 of file java_bytecode_language.cpp.
|
overridevirtual |
Reimplemented from languaget.
Definition at line 276 of file java_bytecode_language.cpp.
|
inlineoverridevirtual |
Implements languaget.
Definition at line 335 of file java_bytecode_language.h.
|
virtual |
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when we have have been given a main class.
Definition at line 367 of file java_bytecode_language.cpp.
|
overridevirtual |
We set the main class (i.e. class to start the class loading analysis, see java_class_loadert) when we have a JAR file given via the -jar option: a) the argument of the –main-class command-line option, b) 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 382 of file java_bytecode_language.cpp.
|
private |
Definition at line 325 of file java_bytecode_language.cpp.
|
overridevirtual |
ANSI-C preprocessing.
Reimplemented from languaget.
Definition at line 282 of file java_bytecode_language.cpp.
|
overridevirtual |
Consume options that are java bytecode specific.
Reimplemented from languaget.
Definition at line 260 of file java_bytecode_language.cpp.
|
overridevirtual |
Reimplemented from messaget.
Definition at line 291 of file java_bytecode_language.cpp.
|
overridevirtual |
Implements languaget.
Definition at line 1505 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 1546 of file java_bytecode_language.cpp.
|
overridevirtual |
Implements languaget.
Definition at line 807 of file java_bytecode_language.cpp.
|
private |
Definition at line 393 of file java_bytecode_language.h.
|
protected |
Definition at line 378 of file java_bytecode_language.h.
|
protected |
Definition at line 375 of file java_bytecode_language.h.
|
protected |
Definition at line 376 of file java_bytecode_language.h.
|
protected |
Definition at line 377 of file java_bytecode_language.h.
|
protected |
Definition at line 380 of file java_bytecode_language.h.
|
protected |
Definition at line 379 of file java_bytecode_language.h.
|
private |
Definition at line 386 of file java_bytecode_language.h.
|
private |
Map used in all calls to functions that deterministically create objects (currently only assign_from_json).
It tracks objects that should be reference-equal to each other by mapping IDs of such objects to symbols that store their values.
Definition at line 399 of file java_bytecode_language.h.
|
protected |
Definition at line 381 of file java_bytecode_language.h.
|
private |
Definition at line 392 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 391 of file java_bytecode_language.h.