cprover
java_bytecode_languaget Class Reference

#include <java_bytecode_language.h>

+ Inheritance diagram for java_bytecode_languaget:
+ Collaboration diagram for java_bytecode_languaget:

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< 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 message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. 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
 
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_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 Member Functions

virtual std::vector< load_extra_methodstbuild_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_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
 
std::vector< load_extra_methodstextra_methods
 

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 commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
 
- Static Public Attributes inherited from messaget
static eomt eom
 
static const commandt reset
 return to default formatting, as defined by the terminal More...
 
static const commandt red
 render text with red foreground color More...
 
static const commandt green
 render text with green foreground color More...
 
static const commandt yellow
 render text with yellow foreground color More...
 
static const commandt blue
 render text with blue foreground color More...
 
static const commandt magenta
 render text with magenta foreground color More...
 
static const commandt cyan
 render text with cyan foreground color More...
 
static const commandt bright_red
 render text with bright red foreground color More...
 
static const commandt bright_green
 render text with bright green foreground color More...
 
static const commandt bright_yellow
 render text with bright yellow foreground color More...
 
static const commandt bright_blue
 render text with bright blue foreground color More...
 
static const commandt bright_magenta
 render text with bright magenta foreground color More...
 
static const commandt bright_cyan
 render text with bright cyan foreground color More...
 
static const commandt bold
 render text with bold font More...
 
static const commandt faint
 render text with faint font More...
 
static const commandt italic
 render italic text More...
 
static const commandt underline
 render underlined text More...
 
- 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 88 of file java_bytecode_language.h.

Constructor & Destructor Documentation

◆ ~java_bytecode_languaget()

java_bytecode_languaget::~java_bytecode_languaget ( )
virtual

Definition at line 1248 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 114 of file java_bytecode_language.h.

◆ java_bytecode_languaget() [2/2]

java_bytecode_languaget::java_bytecode_languaget ( )
inline

Definition at line 125 of file java_bytecode_language.h.

Member Function Documentation

◆ build_extra_entry_points()

std::vector< load_extra_methodst > java_bytecode_languaget::build_extra_entry_points ( const optionst options) const
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 1256 of file java_bytecode_language.cpp.

◆ 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 960 of file java_bytecode_language.cpp.

◆ convert_single_method() [1/2]

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

Definition at line 162 of file java_bytecode_language.h.

◆ 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

Convert a method (one whose type is known but whose body hasn't been converted) but don't run typecheck, etc.

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.
Parameters
function_idmethod ID to convert
symbol_tableglobal symbol table
needed_lazy_methodsoptionally a collection of needed methods to update with any methods touched during the conversion

Definition at line 1030 of file java_bytecode_language.cpp.

◆ description()

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

Reimplemented from languaget.

Definition at line 151 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 876 of file java_bytecode_language.cpp.

◆ extensions()

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

Reimplemented from languaget.

Definition at line 181 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 1148 of file java_bytecode_language.cpp.

◆ 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 1177 of file java_bytecode_language.cpp.

◆ 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 1186 of file java_bytecode_language.cpp.

◆ 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 837 of file java_bytecode_language.cpp.

◆ get_pointer_type_selector()

const select_pointer_typet & java_bytecode_languaget::get_pointer_type_selector ( ) const
protected

Definition at line 903 of file java_bytecode_language.cpp.

◆ id()

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

Reimplemented from languaget.

Definition at line 150 of file java_bytecode_language.h.

◆ 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 914 of file java_bytecode_language.cpp.

◆ modules_provided()

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

Reimplemented from languaget.

Definition at line 186 of file java_bytecode_language.cpp.

◆ new_language()

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

Implements languaget.

Definition at line 147 of file java_bytecode_language.h.

◆ parse()

bool java_bytecode_languaget::parse ( std::istream &  instream,
const std::string &  path 
)
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 210 of file java_bytecode_language.cpp.

◆ 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 192 of file java_bytecode_language.cpp.

◆ set_language_options()

void java_bytecode_languaget::set_language_options ( const optionst options)
overridevirtual

Consume options that are java bytecode specific.

Reimplemented from languaget.

Definition at line 90 of file java_bytecode_language.cpp.

◆ show_parse()

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

Implements languaget.

Definition at line 1154 of file java_bytecode_language.cpp.

◆ 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 1195 of file java_bytecode_language.cpp.

◆ typecheck()

bool java_bytecode_languaget::typecheck ( symbol_tablet context,
const std::string &  module 
)
overridevirtual

Implements languaget.

Definition at line 644 of file java_bytecode_language.cpp.

Member Data Documentation

◆ assert_uncaught_exceptions

bool java_bytecode_languaget::assert_uncaught_exceptions
protected

Definition at line 188 of file java_bytecode_language.h.

◆ assume_inputs_non_null

bool java_bytecode_languaget::assume_inputs_non_null
protected

Definition at line 181 of file java_bytecode_language.h.

◆ class_hierarchy

class_hierarchyt java_bytecode_languaget::class_hierarchy
private

Definition at line 207 of file java_bytecode_language.h.

◆ extra_methods

std::vector<load_extra_methodst> java_bytecode_languaget::extra_methods
private

Definition at line 211 of file java_bytecode_language.h.

◆ java_class_loader

java_class_loadert java_bytecode_languaget::java_class_loader
protected

Definition at line 179 of file java_bytecode_language.h.

◆ java_cp_include_files

std::string java_bytecode_languaget::java_cp_include_files
protected

Definition at line 191 of file java_bytecode_language.h.

◆ java_load_classes

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

Definition at line 195 of file java_bytecode_language.h.

◆ lazy_methods_mode

lazy_methods_modet java_bytecode_languaget::lazy_methods_mode
protected

Definition at line 185 of file java_bytecode_language.h.

◆ main_class

irep_idt java_bytecode_languaget::main_class
protected

Definition at line 177 of file java_bytecode_language.h.

◆ main_jar_classes

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

Definition at line 178 of file java_bytecode_language.h.

◆ max_user_array_length

size_t java_bytecode_languaget::max_user_array_length
protected

Definition at line 183 of file java_bytecode_language.h.

◆ method_bytecode

method_bytecodet java_bytecode_languaget::method_bytecode
protected

Definition at line 184 of file java_bytecode_language.h.

◆ no_load_classes

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

Definition at line 209 of file java_bytecode_language.h.

◆ nondet_static

bool java_bytecode_languaget::nondet_static
protected

Definition at line 192 of file java_bytecode_language.h.

◆ object_factory_parameters

object_factory_parameterst java_bytecode_languaget::object_factory_parameters
protected

Definition at line 182 of file java_bytecode_language.h.

◆ pointer_type_selector

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

Definition at line 200 of file java_bytecode_language.h.

◆ string_preprocess

java_string_library_preprocesst java_bytecode_languaget::string_preprocess
protected

Definition at line 190 of file java_bytecode_language.h.

◆ string_refinement_enabled

bool java_bytecode_languaget::string_refinement_enabled
protected

Definition at line 186 of file java_bytecode_language.h.

◆ stub_global_initializer_factory

stub_global_initializer_factoryt java_bytecode_languaget::stub_global_initializer_factory
private

Definition at line 206 of file java_bytecode_language.h.

◆ 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 205 of file java_bytecode_language.h.

◆ threading_support

bool java_bytecode_languaget::threading_support
protected

Definition at line 180 of file java_bytecode_language.h.

◆ throw_assertion_error

bool java_bytecode_languaget::throw_assertion_error
protected

Definition at line 189 of file java_bytecode_language.h.

◆ throw_runtime_exceptions

bool java_bytecode_languaget::throw_runtime_exceptions
protected

Definition at line 187 of file java_bytecode_language.h.


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