cprover
java_bytecode_languaget Class Reference

#include <java_bytecode_language.h>

Inheritance diagram for java_bytecode_languaget:
[legend]
Collaboration diagram for java_bytecode_languaget:
[legend]

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< languagetnew_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...
 
- Public Member Functions inherited from languaget
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 ()
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream. More...
 

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_typetget_pointer_type_selector () const
 
- Protected Member Functions inherited from languaget
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 &parameter)
 To build the parameter symbol and choose its name. More...
 

Protected Attributes

irep_idt main_class
 
std::vector< irep_idtmain_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_idtlazy_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_idtjava_load_classes
 
- Protected Attributes inherited from languaget
bool generate_opaque_stubs =false
 
bool language_options_initialized =false
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Private Attributes

const std::unique_ptr< const select_pointer_typetpointer_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

- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 
- Static Protected Member Functions inherited from languaget
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...
 

Detailed Description

Definition at line 79 of file java_bytecode_language.h.

Constructor & Destructor Documentation

◆ ~java_bytecode_languaget()

java_bytecode_languaget::~java_bytecode_languaget ( )
virtual

Definition at line 1158 of file java_bytecode_language.cpp.

◆ java_bytecode_languaget() [1/2]

java_bytecode_languaget::java_bytecode_languaget ( std::unique_ptr< select_pointer_typet pointer_type_selector)
inline

Definition at line 105 of file java_bytecode_language.h.

◆ java_bytecode_languaget() [2/2]

java_bytecode_languaget::java_bytecode_languaget ( )
inline

Definition at line 115 of file java_bytecode_language.h.

Member Function Documentation

◆ convert_lazy_method()

void java_bytecode_languaget::convert_lazy_method ( const irep_idt function_id,
symbol_table_baset symtab 
)
overridevirtual

Promote a lazy-converted method (one whose type is known but whose body hasn't been converted) into a fully-elaborated one.

Remarks
Amends the symbol table entry for function 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.
Parameters
function_idmethod ID to convert
symtabglobal 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().

◆ convert_single_method() [1/2]

void java_bytecode_languaget::convert_single_method ( const irep_idt function_id,
symbol_table_baset symbol_table 
)
inlineprotected

◆ convert_single_method() [2/2]

bool java_bytecode_languaget::convert_single_method ( const irep_idt function_id,
symbol_table_baset symbol_table,
optionalt< ci_lazy_methods_neededt needed_lazy_methods 
)
protected

◆ description()

std::string java_bytecode_languaget::description ( ) const
inlineoverridevirtual

Reimplemented from languaget.

Definition at line 141 of file java_bytecode_language.h.

◆ do_ci_lazy_method_conversion()

bool java_bytecode_languaget::do_ci_lazy_method_conversion ( symbol_tablet symbol_table,
method_bytecodet method_bytecode 
)
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).

parameters: symbol_table: global symbol table
method_bytecode: map from method names to relevant symbol and parsed-method objects.
Returns
Elaborates lazily-converted methods that may be reachable starting from the main entry point (usually provided with the –function command- line option) (side-effect on the symbol_table). Returns false on success.

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().

◆ extensions()

std::set< std::string > java_bytecode_languaget::extensions ( ) const
overridevirtual

Reimplemented from languaget.

Definition at line 138 of file java_bytecode_language.cpp.

◆ final()

bool java_bytecode_languaget::final ( symbol_table_baset symbol_table)
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.

◆ from_expr()

bool java_bytecode_languaget::from_expr ( const exprt expr,
std::string &  code,
const namespacet ns 
)
overridevirtual

Formats the given expression in a language-specific way.

Parameters
exprthe expression to format
codethe formatted expression
nsa namespace
Returns
false if conversion succeeds

Reimplemented from languaget.

Definition at line 1093 of file java_bytecode_language.cpp.

References expr2java().

◆ from_type()

bool java_bytecode_languaget::from_type ( const typet type,
std::string &  code,
const namespacet ns 
)
overridevirtual

Formats the given type in a language-specific way.

Parameters
typethe type to format
codethe formatted type
nsa namespace
Returns
false if conversion succeeds

Reimplemented from languaget.

Definition at line 1102 of file java_bytecode_language.cpp.

References exprt::type(), and type2java().

◆ generate_support_functions()

bool java_bytecode_languaget::generate_support_functions ( symbol_tablet symbol_table)
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.

◆ get_language_options()

◆ get_pointer_type_selector()

const select_pointer_typet & java_bytecode_languaget::get_pointer_type_selector ( ) const
protected

◆ id()

std::string java_bytecode_languaget::id ( ) const
inlineoverridevirtual

Reimplemented from languaget.

Definition at line 140 of file java_bytecode_language.h.

Referenced by parse().

◆ methods_provided()

void java_bytecode_languaget::methods_provided ( std::unordered_set< irep_idt > &  methods) const
overridevirtual

Provide feedback to language_filest so that when asked for a lazy method, it can delegate to this instance of java_bytecode_languaget.

Returns
Populates 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.

◆ modules_provided()

void java_bytecode_languaget::modules_provided ( std::set< std::string > &  modules)
overridevirtual

Reimplemented from languaget.

Definition at line 143 of file java_bytecode_language.cpp.

◆ new_language()

std::unique_ptr<languaget> java_bytecode_languaget::new_language ( )
inlineoverridevirtual

Implements languaget.

Definition at line 137 of file java_bytecode_language.h.

◆ parse()

◆ preprocess()

bool java_bytecode_languaget::preprocess ( std::istream &  instream,
const std::string &  path,
std::ostream &  outstream 
)
overridevirtual

ANSI-C preprocessing.

Reimplemented from languaget.

Definition at line 149 of file java_bytecode_language.cpp.

◆ show_parse()

void java_bytecode_languaget::show_parse ( std::ostream &  out)
overridevirtual

Implements languaget.

Definition at line 1070 of file java_bytecode_language.cpp.

References java_class_loader, and main_class.

◆ to_expr()

bool java_bytecode_languaget::to_expr ( const std::string &  code,
const std::string &  module,
exprt expr,
const namespacet ns 
)
overridevirtual

Parses the given string into an expression.

Parameters
codethe string to parse
moduleprefix to be used for identifiers
exprthe parsed expression
nsa namespace
Returns
false if the conversion succeeds

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().

◆ typecheck()

Member Data Documentation

◆ assert_uncaught_exceptions

bool java_bytecode_languaget::assert_uncaught_exceptions
protected

Definition at line 179 of file java_bytecode_language.h.

Referenced by generate_support_functions(), and get_language_options().

◆ assume_inputs_non_null

bool java_bytecode_languaget::assume_inputs_non_null
protected

Definition at line 171 of file java_bytecode_language.h.

Referenced by generate_support_functions(), and get_language_options().

◆ class_hierarchy

class_hierarchyt java_bytecode_languaget::class_hierarchy
private

Definition at line 195 of file java_bytecode_language.h.

Referenced by convert_single_method(), and typecheck().

◆ java_class_loader

java_class_loadert java_bytecode_languaget::java_class_loader
protected

◆ java_cp_include_files

std::string java_bytecode_languaget::java_cp_include_files
protected

Definition at line 182 of file java_bytecode_language.h.

Referenced by get_language_options(), and parse().

◆ java_load_classes

std::vector<irep_idt> java_bytecode_languaget::java_load_classes
protected

◆ lazy_methods_extra_entry_points

std::vector<irep_idt> java_bytecode_languaget::lazy_methods_extra_entry_points
protected

Definition at line 176 of file java_bytecode_language.h.

Referenced by do_ci_lazy_method_conversion(), and get_language_options().

◆ lazy_methods_mode

lazy_methods_modet java_bytecode_languaget::lazy_methods_mode
protected

Definition at line 175 of file java_bytecode_language.h.

Referenced by get_language_options(), and typecheck().

◆ main_class

irep_idt java_bytecode_languaget::main_class
protected

◆ main_jar_classes

std::vector<irep_idt> java_bytecode_languaget::main_jar_classes
protected

Definition at line 168 of file java_bytecode_language.h.

Referenced by do_ci_lazy_method_conversion(), and parse().

◆ max_user_array_length

size_t java_bytecode_languaget::max_user_array_length
protected

◆ method_bytecode

method_bytecodet java_bytecode_languaget::method_bytecode
protected

◆ no_load_classes

std::unordered_set<std::string> java_bytecode_languaget::no_load_classes
private

Definition at line 197 of file java_bytecode_language.h.

Referenced by get_language_options(), and typecheck().

◆ object_factory_parameters

object_factory_parameterst java_bytecode_languaget::object_factory_parameters
protected

◆ pointer_type_selector

const std::unique_ptr<const select_pointer_typet> java_bytecode_languaget::pointer_type_selector
private

Definition at line 188 of file java_bytecode_language.h.

Referenced by get_pointer_type_selector().

◆ string_preprocess

java_string_library_preprocesst java_bytecode_languaget::string_preprocess
protected

◆ string_refinement_enabled

bool java_bytecode_languaget::string_refinement_enabled
protected

◆ stub_global_initializer_factory

stub_global_initializer_factoryt java_bytecode_languaget::stub_global_initializer_factory
private

Definition at line 194 of file java_bytecode_language.h.

Referenced by convert_single_method(), and typecheck().

◆ synthetic_methods

synthetic_methods_mapt java_bytecode_languaget::synthetic_methods
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().

◆ threading_support

bool java_bytecode_languaget::threading_support
protected

◆ throw_assertion_error

bool java_bytecode_languaget::throw_assertion_error
protected

Definition at line 180 of file java_bytecode_language.h.

Referenced by convert_single_method(), and get_language_options().

◆ throw_runtime_exceptions

bool java_bytecode_languaget::throw_runtime_exceptions
protected

Definition at line 178 of file java_bytecode_language.h.

Referenced by convert_lazy_method(), get_language_options(), and typecheck().


The documentation for this class was generated from the following files: