Loading...

Searching...

No Matches

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

void set_language_options (const optionst &, message_handlert &) override

Consume options that are java bytecode specific.

virtual bool preprocess (std::istream &instream, const std::string &path, std::ostream &outstream, message_handlert &message_handler) override

ANSI-C preprocessing.

bool parse (std::istream &instream, const std::string &path, message_handlert &message_handler) 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_table_baset &symbol_table, message_handlert &message_handler) override

Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and language-specific library functions.

bool typecheck (symbol_table_baset &context, const std::string &module, message_handlert &message_handler) override

virtual bool final (symbol_table_baset &context) override

Final adjustments, e.g.

void show_parse (std::ostream &out, message_handlert &) 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, message_handlert &message_handler) 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, message_handlert &message_handler) override

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

- Public Member Functions inherited from languaget

virtual void dependencies (const std::string &module, std::set< std::string > &modules)

virtual bool interfaces (symbol_table_baset &symbol_table, message_handlert &message_handler)

virtual bool can_keep_file_local ()

Is it possible to call three-argument typecheck() on this object?

virtual bool typecheck (symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler, const bool keep_file_local)

typecheck without removing specified entries from the 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.

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, message_handlert &message_handler)

bool convert_single_method (const irep_idt &function_id, symbol_table_baset &symbol_table, std::optional< ci_lazy_methods_neededt > needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols, message_handlert &)

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, std::optional< ci_lazy_methods_neededt > needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols, message_handlert &)

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_table_baset &, message_handlert &)

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

Protected Attributes

std::optional< java_bytecode_language_optionst > language_options

irep_idt main_class

std::vector< irep_idt > main_jar_classes

java_class_loadert java_class_loader

java_object_factory_parameterst object_factory_parameters

method_bytecodet method_bytecode

java_string_library_preprocesst string_preprocess

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 (message_handlert &)

void initialize_class_loader (message_handlert &)

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

Detailed Description

Definition at line 259 of file java_bytecode_language.h.

Constructor & Destructor Documentation

◆ ~java_bytecode_languaget()

java_bytecode_languaget::~java_bytecode_languaget ( )

virtual

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

◆ java_bytecode_languaget() [2/2]

java_bytecode_languaget::java_bytecode_languaget ( )

inline

Definition at line 296 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 1618 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,

message_handlert & message_handler

)

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_id method ID to convert

symtab global symbol table

message_handler message handler

Reimplemented from languaget.

Definition at line 1184 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,

lazy_class_to_declared_symbols_mapt & class_to_declared_symbols,

message_handlert & message_handler

)

inlineprotected

Definition at line 337 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,

std::optional< ci_lazy_methods_neededt > needed_lazy_methods,

lazy_class_to_declared_symbols_mapt & class_to_declared_symbols,

message_handlert & message_handler

)

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.

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_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.

message_handler message handler

Definition at line 1282 of file java_bytecode_language.cpp.

◆ convert_single_method_code()

bool java_bytecode_languaget::convert_single_method_code ( const irep_idt & function_id,

symbol_table_baset & symbol_table,

std::optional< ci_lazy_methods_neededt > needed_lazy_methods,

lazy_class_to_declared_symbols_mapt & class_to_declared_symbols,

message_handlert & message_handler

)

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_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.

message_handler message handler

Definition at line 1341 of file java_bytecode_language.cpp.

◆ description()

std::string java_bytecode_languaget::description ( ) const

inlineoverridevirtual

Implements languaget.

Definition at line 325 of file java_bytecode_language.h.

◆ do_ci_lazy_method_conversion()

bool java_bytecode_languaget::do_ci_lazy_method_conversion ( symbol_table_baset & symbol_table,

message_handlert & message_handler

)

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

message_handler message handler

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

◆ extensions()

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

overridevirtual

Implements languaget.

Definition at line 272 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 1506 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: expr the expression to format

code the formatted expression

ns a namespace

Returns: false if conversion succeeds

Reimplemented from languaget.

Definition at line 1537 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: type the type to format

code the formatted type

ns a namespace

Returns: false if conversion succeeds

Reimplemented from languaget.

Definition at line 1546 of file java_bytecode_language.cpp.

◆ generate_support_functions()

bool java_bytecode_languaget::generate_support_functions ( symbol_table_baset & symbol_table,

message_handlert & message_handler

)

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 1049 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 1148 of file java_bytecode_language.cpp.

◆ id()

std::string java_bytecode_languaget::id ( ) const

inlineoverridevirtual

Implements languaget.

Definition at line 324 of file java_bytecode_language.h.

◆ initialize_class_loader()

void java_bytecode_languaget::initialize_class_loader ( message_handlert & message_handler )

private

Definition at line 293 of file java_bytecode_language.cpp.

◆ 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.

Parameters: [out] methods 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 1159 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 277 of file java_bytecode_language.cpp.

◆ new_language()

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

inlineoverridevirtual

Implements languaget.

Definition at line 319 of file java_bytecode_language.h.

◆ parse()

bool java_bytecode_languaget::parse ( std::istream & instream,

const std::string & path,

message_handlert & message_handler

)

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

◆ parse_from_main_class()

void java_bytecode_languaget::parse_from_main_class ( message_handlert & message_handler )

private

Definition at line 322 of file java_bytecode_language.cpp.

◆ preprocess()

bool java_bytecode_languaget::preprocess ( std::istream & instream,

const std::string & path,

std::ostream & outstream,

message_handlert & message_handler

)

overridevirtual

ANSI-C preprocessing.

Reimplemented from languaget.

Definition at line 283 of file java_bytecode_language.cpp.

◆ set_language_options()

void java_bytecode_languaget::set_language_options ( const optionst & options,

message_handlert & message_handler

)

overridevirtual

Consume options that are java bytecode specific.

Reimplemented from languaget.

Definition at line 259 of file java_bytecode_language.cpp.

◆ show_parse()

void java_bytecode_languaget::show_parse ( std::ostream & out,

message_handlert & message_handler

)

overridevirtual

Implements languaget.

Definition at line 1512 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,

message_handlert & message_handler

)

overridevirtual

Parses the given string into an expression.

Parameters: code the string to parse

module prefix to be used for identifiers

expr the parsed expression

ns a namespace

message_handler a message handler

Returns: false if the conversion succeeds

Implements languaget.

Definition at line 1555 of file java_bytecode_language.cpp.

◆ typecheck()

bool java_bytecode_languaget::typecheck ( symbol_table_baset & context,

const std::string & module,

message_handlert & message_handler

)

overridevirtual

Implements languaget.

Definition at line 794 of file java_bytecode_language.cpp.

Member Data Documentation

◆ class_hierarchy

class_hierarchyt java_bytecode_languaget::class_hierarchy

private

Definition at line 384 of file java_bytecode_language.h.

◆ java_class_loader

java_class_loadert java_bytecode_languaget::java_class_loader

protected

Definition at line 369 of file java_bytecode_language.h.

◆ language_options

std::optional<java_bytecode_language_optionst> java_bytecode_languaget::language_options

protected

Definition at line 366 of file java_bytecode_language.h.

◆ main_class

irep_idt java_bytecode_languaget::main_class

protected

Definition at line 367 of file java_bytecode_language.h.

◆ main_jar_classes

std::vector<irep_idt> java_bytecode_languaget::main_jar_classes

protected

Definition at line 368 of file java_bytecode_language.h.

◆ method_bytecode

method_bytecodet java_bytecode_languaget::method_bytecode

protected

Definition at line 371 of file java_bytecode_language.h.

◆ object_factory_parameters

java_object_factory_parameterst java_bytecode_languaget::object_factory_parameters

protected

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

◆ references

std::unordered_map<std::string, object_creation_referencet> java_bytecode_languaget::references

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

◆ string_preprocess

java_string_library_preprocesst java_bytecode_languaget::string_preprocess

protected

Definition at line 372 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 383 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 382 of file java_bytecode_language.h.

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

/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_bytecode_language.h
/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_bytecode_language.cpp