Loading...

Searching...

No Matches

java_bytecode_convert_method.cpp File Reference

JAVA Bytecode Language Conversion. More...

#include "java_bytecode_convert_method_class.h"
#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/c_types.h>
#include <util/expr_initializer.h>
#include <util/floatbv_expr.h>
#include <util/ieee_float.h>
#include <util/invariant.h>
#include <util/namespace.h>
#include <util/prefix.h>
#include <util/prefix_filter.h>
#include <util/std_expr.h>
#include <util/symbol_table_base.h>
#include <util/threeval.h>
#include <goto-programs/resolve_inherited_component.h>
#include <analyses/uncaught_exceptions_analysis.h>
#include "bytecode_info.h"
#include "java_bytecode_convert_method.h"
#include "java_expr.h"
#include "java_static_initializers.h"
#include "java_string_library_preprocess.h"
#include "java_string_literal_expr.h"
#include "java_types.h"
#include "java_utils.h"
#include "lambda_synthesis.h"
#include "pattern.h"
#include <algorithm>
#include <limits>

+ Include dependency graph for java_bytecode_convert_method.cpp:

[フレーム]

Go to the source code of this file.

Functions

static void assign_parameter_names (java_method_typet &ftype, const irep_idt &name_prefix, symbol_table_baset &symbol_table)

Iterates through the parameters of the function type ftype, finds a new new name for each parameter and renames them in ftype.parameters() as well as in the symbol_table.

void create_method_stub_symbol (const irep_idt &identifier, const irep_idt &base_name, const irep_idt &pretty_name, const typet &type, const irep_idt &declaring_class, symbol_table_baset &symbol_table, message_handlert &message_handler)

static bool is_constructor (const irep_idt &method_name)

java_method_typet member_type_lazy (const std::string &descriptor, const std::optional< std::string > &signature, const std::string &class_name, const std::string &method_name, message_handlert &message_handler)

Returns the member type for a method, based on signature or descriptor.

void java_bytecode_convert_method_lazy (symbolt &class_symbol, const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt &m, symbol_table_baset &symbol_table, message_handlert &message_handler)

This creates a method symbol in the symtab, but doesn't actually perform method conversion just yet.

static irep_idt get_method_identifier (const irep_idt &class_identifier, const java_bytecode_parse_treet::methodt &method)

void create_parameter_names (const java_bytecode_parse_treet::methodt &m, const irep_idt &method_identifier, java_method_typet::parameterst &parameters, const java_bytecode_convert_methodt::method_offsett &slots_for_parameters)

Extracts the names of parameters from the local variable table in the method, and uses it to construct sensible names/identifiers for the parameters in the parameters on the java_method_typet and the external variables vector.

void create_parameter_symbols (const java_method_typet::parameterst &parameters, expanding_vectort< std::vector< java_bytecode_convert_methodt::variablet > > &variables, symbol_table_baset &symbol_table)

static irep_idt get_if_cmp_operator (const u1 bytecode)

static member_exprt to_member (const exprt &pointer, const fieldref_exprt &field_reference, const namespacet &ns)

Build a member exprt for accessing a specific field that may come from a base class.

static void gather_symbol_live_ranges (java_bytecode_convert_methodt::method_offsett pc, const exprt &e, std::map< irep_idt, java_bytecode_convert_methodt::variablet > &result)

static std::size_t get_bytecode_type_width (const typet &ty)

static void adjust_invoke_argument_types (const java_method_typet::parameterst &parameters, code_function_callt::argumentst &arguments)

static exprt conditional_array_cast (const exprt &expr, char type_char)

Add typecast if necessary to expr to make it compatible with array type corresponding to type_char (see java_array_type(const char)).

void java_bytecode_initialize_parameter_names (symbolt &method_symbol, const java_bytecode_parse_treet::methodt::local_variable_tablet &local_variable_table, symbol_table_baset &symbol_table)

This uses a cut-down version of the logic in java_bytecode_convert_methodt::convert to initialize symbols for the parameters and update the parameters in the type of method_symbol with names read from the local_variable_table read from the bytecode.

void java_bytecode_convert_method (const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &method, symbol_table_baset &symbol_table, message_handlert &message_handler, size_t max_array_length, bool throw_assertion_error, std::optional< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support, const std::optional< prefix_filtert > &method_context, bool assert_no_exceptions_thrown)

Detailed Description

JAVA Bytecode Language Conversion.

Definition in file java_bytecode_convert_method.cpp.

Function Documentation

◆ adjust_invoke_argument_types()

static void adjust_invoke_argument_types ( const java_method_typet::parameterst & parameters,

code_function_callt::argumentst & arguments

)

static

Definition at line 2207 of file java_bytecode_convert_method.cpp.

◆ assign_parameter_names()

static void assign_parameter_names ( java_method_typet & ftype,

const irep_idt & name_prefix,

symbol_table_baset & symbol_table

)

static

Iterates through the parameters of the function type ftype, finds a new new name for each parameter and renames them in ftype.parameters() as well as in the symbol_table.

Assigns parameter names (side-effects on ftype) to function stub parameters, which are initially nameless as method conversion hasn't happened. Also creates symbols in symbol_table.

Parameters: [in,out] ftype Function type whose parameters should be named.

name_prefix Prefix for parameter names, typically the parent function's name.

[in,out] symbol_table Global symbol table.

Definition at line 62 of file java_bytecode_convert_method.cpp.

◆ conditional_array_cast()

static exprt conditional_array_cast ( const exprt & expr,

char type_char

)

static

Add typecast if necessary to expr to make it compatible with array type corresponding to type_char (see java_array_type(const char)).

Character 'b' is used both for byte and boolean arrays, so if expr is a boolean array and we are using a b operation we can skip the typecast.

Definition at line 2981 of file java_bytecode_convert_method.cpp.

◆ create_method_stub_symbol()

void create_method_stub_symbol ( const irep_idt & identifier,

const irep_idt & base_name,

const irep_idt & pretty_name,

const typet & type,

const irep_idt & declaring_class,

symbol_table_baset & symbol_table,

message_handlert & message_handler

)

Definition at line 94 of file java_bytecode_convert_method.cpp.

◆ create_parameter_names()

void create_parameter_names ( const java_bytecode_parse_treet::methodt & m,

const irep_idt & method_identifier,

java_method_typet::parameterst & parameters,

const java_bytecode_convert_methodt::method_offsett & slots_for_parameters

)

Extracts the names of parameters from the local variable table in the method, and uses it to construct sensible names/identifiers for the parameters in the parameters on the java_method_typet and the external variables vector.

Parameters: m the parsed method whose local variable table contains the name of the parameters

method_identifier the identifier of the method

parameters the java_method_typet's parameters [out]

slots_for_parameters the number of parameter slots available, i.e. a positive integer

Definition at line 422 of file java_bytecode_convert_method.cpp.

◆ create_parameter_symbols()

void create_parameter_symbols ( const java_method_typet::parameterst & parameters,

expanding_vectort< std::vector< java_bytecode_convert_methodt::variablet > > & variables,

symbol_table_baset & symbol_table

)

Definition at line 507 of file java_bytecode_convert_method.cpp.

◆ gather_symbol_live_ranges()

static void gather_symbol_live_ranges ( java_bytecode_convert_methodt::method_offsett pc,

const exprt & e,

std::map< irep_idt, java_bytecode_convert_methodt::variablet > & result

)

static

Definition at line 945 of file java_bytecode_convert_method.cpp.

◆ get_bytecode_type_width()

static std::size_t get_bytecode_type_width ( const typet & ty )

static

Definition at line 999 of file java_bytecode_convert_method.cpp.

◆ get_if_cmp_operator()

static irep_idt get_if_cmp_operator ( const u1 bytecode )

static

Definition at line 630 of file java_bytecode_convert_method.cpp.

◆ get_method_identifier()

static irep_idt get_method_identifier ( const irep_idt & class_identifier,

const java_bytecode_parse_treet::methodt & method

)

static

Definition at line 413 of file java_bytecode_convert_method.cpp.

◆ is_constructor()

static bool is_constructor ( const irep_idt & method_name )

static

Definition at line 119 of file java_bytecode_convert_method.cpp.

◆ java_bytecode_convert_method()

void java_bytecode_convert_method ( const symbolt & class_symbol,

const java_bytecode_parse_treet::methodt & method,

symbol_table_baset & symbol_table,

message_handlert & message_handler,

size_t max_array_length,

bool throw_assertion_error,

std::optional< ci_lazy_methods_neededt > needed_lazy_methods,

java_string_library_preprocesst & string_preprocess,

const class_hierarchyt & class_hierarchy,

bool threading_support,

const std::optional< prefix_filtert > & method_context,

bool assert_no_exceptions_thrown

)

Definition at line 3281 of file java_bytecode_convert_method.cpp.

◆ java_bytecode_convert_method_lazy()

void java_bytecode_convert_method_lazy ( symbolt & class_symbol,

const irep_idt & method_identifier,

const java_bytecode_parse_treet::methodt & m,

symbol_table_baset & symbol_table,

message_handlert & message_handler

)

This creates a method symbol in the symtab, but doesn't actually perform method conversion just yet.

The caller should call java_bytecode_convert_method later to give the symbol/method a body.

Parameters: class_symbol The class this method belongs to. The method, if not static, will be added to the class' list of methods.

method_identifier The fully qualified method name, including type descriptor (e.g. "x.y.z.f:(I)")

m The parsed method object to convert.

symbol_table The global symbol table (will be modified).

message_handler A message handler to collect warnings.

Definition at line 299 of file java_bytecode_convert_method.cpp.

◆ java_bytecode_initialize_parameter_names()

void java_bytecode_initialize_parameter_names ( symbolt & method_symbol,

const java_bytecode_parse_treet::methodt::local_variable_tablet & local_variable_table,

symbol_table_baset & symbol_table

)

This uses a cut-down version of the logic in java_bytecode_convert_methodt::convert to initialize symbols for the parameters and update the parameters in the type of method_symbol with names read from the local_variable_table read from the bytecode.

Remarks: This is useful for pre-initialization for methods generated by the string solver

Parameters: method_symbol The symbol for the method for which to initialize the parameters

local_variable_table The local variable table containing the bytecode for the parameters

symbol_table The symbol table into which to insert symbols for the parameters

Definition at line 3203 of file java_bytecode_convert_method.cpp.

◆ member_type_lazy()

java_method_typet member_type_lazy ( const std::string & descriptor,

const std::optional< std::string > & signature,

const std::string & class_name,

const std::string & method_name,

message_handlert & message_handler

)

Returns the member type for a method, based on signature or descriptor.

Parameters: descriptor descriptor of the method

signature signature of the method

class_name string containing the name of the corresponding class

method_name string containing the name of the method

message_handler message handler to collect warnings

Returns: the constructed member type

Definition at line 229 of file java_bytecode_convert_method.cpp.

◆ to_member()

static member_exprt to_member ( const exprt & pointer,

const fieldref_exprt & field_reference,

const namespacet & ns

)

static

Build a member exprt for accessing a specific field that may come from a base class.

Parameters: pointer The expression to access the field on.

field_reference A getfield/setfield instruction produced by the bytecode parser.

ns Global namespace

Returns: A member expression accessing the field, through base class components if necessary.

Definition at line 656 of file java_bytecode_convert_method.cpp.