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 typecheck (symbol_tablet &context, const std::string &module) override
 
bool final (symbol_tablet &context) override
 
void show_parse (std::ostream &out) override
 
virtual ~java_bytecode_languaget ()
 
 java_bytecode_languaget ()
 
bool from_expr (const exprt &expr, std::string &code, const namespacet &ns) override
 
bool from_type (const typet &type, std::string &code, const namespacet &ns) override
 
bool to_expr (const std::string &code, const std::string &module, exprt &expr, const namespacet &ns) override
 
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 lazy_methods_provided (std::set< irep_idt > &) 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 &id, symbol_tablet &) 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)
 
 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)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

Protected Member Functions

bool do_ci_lazy_method_conversion (symbol_tablet &, lazy_methodst &)
 Uses a simple context-insensitive ('ci') analysis to determine which methods may be reachable from the main entry point. More...
 

Protected Attributes

irep_idt main_class
 
std::vector< irep_idtmain_jar_classes
 
java_class_loadert java_class_loader
 
bool assume_inputs_non_null
 
size_t max_nondet_array_length
 
size_t max_user_array_length
 
lazy_methodst lazy_methods
 
lazy_methods_modet lazy_methods_mode
 
bool string_refinement_enabled
 
character_refine_preprocesst character_preprocess
 
std::string java_cp_include_files
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

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 mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 37 of file java_bytecode_language.h.

Constructor & Destructor Documentation

◆ ~java_bytecode_languaget()

java_bytecode_languaget::~java_bytecode_languaget ( )
virtual

Definition at line 728 of file java_bytecode_language.cpp.

◆ java_bytecode_languaget()

java_bytecode_languaget::java_bytecode_languaget ( )
inline

Definition at line 61 of file java_bytecode_language.h.

Referenced by new_language().

Member Function Documentation

◆ convert_lazy_method()

void java_bytecode_languaget::convert_lazy_method ( const irep_idt id,
symbol_tablet symtab 
)
overridevirtual

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

parameters: id: method ID to convert
symtab: global symbol table
Returns
Amends the symbol table entry for function id, which should be a lazy method provided by this instance of java_bytecode_languaget. It should initially have a nil value. After this method completes, it will have a value representing the method body, identical to that produced using eager method conversion.

Reimplemented from languaget.

Definition at line 615 of file java_bytecode_language.cpp.

References character_preprocess, messaget::get_message_handler(), java_bytecode_convert_method(), lazy_methods, and max_user_array_length.

◆ description()

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

Reimplemented from languaget.

Definition at line 86 of file java_bytecode_language.h.

◆ do_ci_lazy_method_conversion()

bool java_bytecode_languaget::do_ci_lazy_method_conversion ( symbol_tablet symbol_table,
lazy_methodst lazy_methods 
)
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
lazy_methods: 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 448 of file java_bytecode_language.cpp.

References symbol_tablet::add(), character_preprocess, java_class_loadert::class_map, messaget::debug(), dstringt::empty(), messaget::eom(), gather_needed_globals(), gather_virtual_callsites(), get_main_symbol(), messaget::get_message_handler(), get_virtual_method_targets(), id2string(), initialize_needed_classes(), java_bytecode_convert_method(), java_class_loader, lazy_methods, symbol_tablet::lookup(), main_class, main_jar_classes, max_user_array_length, symbol_tablet::swap(), symbol_tablet::symbols, and symbolt::value.

Referenced by typecheck().

◆ extensions()

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

Reimplemented from languaget.

Definition at line 82 of file java_bytecode_language.cpp.

◆ final()

◆ from_expr()

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

Reimplemented from languaget.

Definition at line 663 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

Reimplemented from languaget.

Definition at line 672 of file java_bytecode_language.cpp.

References type2java().

◆ get_language_options()

◆ id()

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

Reimplemented from languaget.

Definition at line 85 of file java_bytecode_language.h.

◆ lazy_methods_provided()

void java_bytecode_languaget::lazy_methods_provided ( std::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 599 of file java_bytecode_language.cpp.

References lazy_methods.

◆ modules_provided()

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

Reimplemented from languaget.

Definition at line 87 of file java_bytecode_language.cpp.

◆ new_language()

languaget* java_bytecode_languaget::new_language ( )
inlineoverridevirtual

Implements languaget.

Definition at line 82 of file java_bytecode_language.h.

References java_bytecode_languaget().

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

◆ show_parse()

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

Implements languaget.

Definition at line 653 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

◆ typecheck()

Member Data Documentation

◆ assume_inputs_non_null

bool java_bytecode_languaget::assume_inputs_non_null
protected

Definition at line 100 of file java_bytecode_language.h.

Referenced by final(), and get_language_options().

◆ character_preprocess

character_refine_preprocesst java_bytecode_languaget::character_preprocess
protected

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

Referenced by get_language_options(), and parse().

◆ lazy_methods

lazy_methodst java_bytecode_languaget::lazy_methods
protected

◆ lazy_methods_mode

lazy_methods_modet java_bytecode_languaget::lazy_methods_mode
protected

Definition at line 104 of file java_bytecode_language.h.

Referenced by get_language_options(), and typecheck().

◆ main_class

irep_idt java_bytecode_languaget::main_class
protected

Definition at line 97 of file java_bytecode_language.h.

Referenced by do_ci_lazy_method_conversion(), final(), parse(), and show_parse().

◆ main_jar_classes

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

Definition at line 98 of file java_bytecode_language.h.

Referenced by do_ci_lazy_method_conversion(), and parse().

◆ max_nondet_array_length

size_t java_bytecode_languaget::max_nondet_array_length
protected

Definition at line 101 of file java_bytecode_language.h.

Referenced by final(), and get_language_options().

◆ max_user_array_length

size_t java_bytecode_languaget::max_user_array_length
protected

◆ string_refinement_enabled

bool java_bytecode_languaget::string_refinement_enabled
protected

Definition at line 105 of file java_bytecode_language.h.

Referenced by get_language_options(), and typecheck().


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