cprover
|
JAVA Bytecode Language Conversion. More...
#include "java_bytecode_convert_method.h"
#include "java_bytecode_convert_method_class.h"
#include "bytecode_info.h"
#include "java_static_initializers.h"
#include "java_string_library_preprocess.h"
#include "java_types.h"
#include "java_utils.h"
#include "remove_exceptions.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/expr_initializer.h>
#include <util/ieee_float.h>
#include <util/invariant.h>
#include <util/namespace.h>
#include <util/prefix.h>
#include <util/simplify_expr.h>
#include <util/std_expr.h>
#include <util/string2int.h>
#include <util/string_constant.h>
#include <goto-programs/cfg.h>
#include <goto-programs/class_hierarchy.h>
#include <goto-programs/resolve_inherited_component.h>
#include <analyses/cfg_dominators.h>
#include <analyses/uncaught_exceptions_analysis.h>
#include <limits>
#include <algorithm>
#include <functional>
#include <unordered_set>
#include <regex>
Go to the source code of this file.
Classes | |
class | patternt |
Given a string of the format '?blah?', will return true when compared against a string that matches appart from any characters that are '?' in the original string. More... | |
Functions | |
static void | assign_parameter_names (code_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 . More... | |
static bool | operator== (const irep_idt &what, const patternt &pattern) |
static bool | is_constructor (const irep_idt &method_name) |
code_typet | member_type_lazy (const std::string &descriptor, const optionalt< 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. More... | |
void | java_bytecode_convert_method_lazy (const symbolt &class_symbol, const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt &m, symbol_tablet &symbol_table, message_handlert &message_handler) |
This creates a method symbol in the symtab, but doesn't actually perform method conversion just yet. More... | |
static irep_idt | get_if_cmp_operator (const irep_idt &stmt) |
static member_exprt | to_member (const exprt &pointer, const exprt &fieldref) |
static void | gather_symbol_live_ranges (unsigned pc, const exprt &e, std::map< irep_idt, java_bytecode_convert_methodt::variablet > &result) |
static unsigned | get_bytecode_type_width (const typet &ty) |
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. More... | |
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, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy) |
JAVA Bytecode Language Conversion.
Definition in file java_bytecode_convert_method.cpp.
|
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
.
[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. |
ftype
) to function stub parameters, which are initially nameless as method conversion hasn't happened. Also creates symbols in symbol_table
. Definition at line 88 of file java_bytecode_convert_method.cpp.
References symbol_table_baset::add(), symbolt::base_name, id2string(), symbolt::mode, symbolt::name, code_typet::parameters(), to_string(), and symbolt::type.
Referenced by java_bytecode_convert_methodt::convert_invoke().
|
static |
Definition at line 914 of file java_bytecode_convert_method.cpp.
References forall_operands, irept::id(), and to_symbol_expr().
Referenced by java_bytecode_convert_methodt::convert_instructions().
|
static |
Definition at line 972 of file java_bytecode_convert_method.cpp.
References irept::get_unsigned_int(), and irept::id().
Referenced by java_bytecode_convert_methodt::convert_dup2(), java_bytecode_convert_methodt::convert_dup2_x1(), java_bytecode_convert_methodt::convert_dup2_x2(), and java_bytecode_convert_methodt::convert_pop().
Definition at line 628 of file java_bytecode_convert_method.cpp.
Referenced by java_bytecode_convert_methodt::convert_if_cmp().
|
static |
Definition at line 125 of file java_bytecode_convert_method.cpp.
References id2string().
Referenced by java_bytecode_convert_methodt::convert(), java_bytecode_convert_methodt::convert_invoke(), java_simple_method_stubst::create_method_stub(), java_simple_method_stubst::create_method_stub_at(), java_bytecode_convert_method_lazy(), cpp_typecheckt::move_member_initializers(), Parser::rOtherDeclaration(), and cpp_typecheckt::typecheck_compound_declarator().
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, | ||
optionalt< ci_lazy_methods_neededt > | needed_lazy_methods, | ||
java_string_library_preprocesst & | string_preprocess, | ||
const class_hierarchyt & | class_hierarchy | ||
) |
Definition at line 3085 of file java_bytecode_convert_method.cpp.
References cprover_methods_to_ignore, id2string(), java_bytecode_convert_method(), message_handler, symbolt::name, and java_bytecode_parse_treet::membert::name.
Referenced by java_bytecode_languaget::convert_single_method(), and java_bytecode_convert_method().
void java_bytecode_convert_method_lazy | ( | const symbolt & | class_symbol, |
const irep_idt & | method_identifier, | ||
const java_bytecode_parse_treet::methodt & | m, | ||
symbol_tablet & | 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.
method_identifier
: fully qualified method name, including type descriptor (e.g. "x.y.z.f:(I)") m
: parsed method object to convert symbol_table
: global symbol table (will be modified) message_handler
: message handler to collect warnings Definition at line 338 of file java_bytecode_convert_method.cpp.
References symbol_table_baset::add(), java_bytecode_parse_treet::membert::annotations, symbolt::base_name, java_bytecode_parse_treet::methodt::base_name, convert_annotations(), java_bytecode_parse_treet::membert::descriptor, java_bytecode_parse_treet::find_annotation(), id2string(), java_bytecode_parse_treet::methodt::is_abstract, is_constructor(), java_bytecode_parse_treet::membert::is_private, java_bytecode_parse_treet::membert::is_protected, java_bytecode_parse_treet::membert::is_public, java_bytecode_parse_treet::membert::is_static, java_reference_type(), symbolt::location, member_type_lazy(), message_handler, symbolt::mode, symbolt::name, code_typet::parameters(), symbolt::pretty_name, pretty_signature(), irept::set(), code_typet::set_access(), source_locationt::set_function(), code_typet::set_is_constructor(), code_typet::parametert::set_this(), java_bytecode_parse_treet::membert::signature, java_bytecode_parse_treet::methodt::source_location, symbolt::type, and exprt::type().
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.
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 3007 of file java_bytecode_convert_method.cpp.
References symbolt::base_name, id2string(), symbol_table_baset::insert(), java_char_from_type(), java_local_variable_slots(), java_method_parameter_slots(), symbolt::mode, symbolt::name, code_typet::parameters(), to_code_type(), to_string(), and symbolt::type.
Referenced by java_bytecode_languaget::convert_single_method().
code_typet member_type_lazy | ( | const std::string & | descriptor, |
const optionalt< 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.
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 |
Definition at line 257 of file java_bytecode_convert_method.cpp.
References messaget::eom(), irept::id(), INVARIANT, java_type_from_string(), message_handler, code_typet::parameters(), to_code_type(), and messaget::warning().
Referenced by java_bytecode_convert_method_lazy().
Definition at line 120 of file java_bytecode_convert_method.cpp.
|
static |
Definition at line 646 of file java_bytecode_convert_method.cpp.
References checked_dereference(), irept::get(), java_reference_type(), and exprt::type().
Referenced by java_bytecode_convert_methodt::convert_instructions(), and java_bytecode_convert_methodt::convert_putfield().