cprover
java_bytecode_convert_method.cpp File Reference

JAVA Bytecode Language Conversion. More...

#include "java_bytecode_convert_method.h"
#include "java_bytecode_convert_method_class.h"
#include "bytecode_info.h"
#include "java_types.h"
#include <util/arith_tools.h>
#include <util/c_types.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 <linking/zero_initializer.h>
#include <goto-programs/cfg.h>
#include <analyses/cfg_dominators.h>
#include <limits>
#include <algorithm>
#include <functional>
#include <unordered_set>
Include dependency graph for java_bytecode_convert_method.cpp:

Go to the source code of this file.

Classes

class  patternt
 

Functions

static bool operator== (const irep_idt &what, const patternt &pattern)
 
const size_t SLOTS_PER_INTEGER (1u)
 
const size_t INTEGER_WIDTH (64u)
 
static size_t count_slots (const size_t value, const code_typet::parametert &param)
 
static size_t get_variable_slots (const code_typet::parametert &param)
 
static irep_idt strip_java_namespace_prefix (const irep_idt to_strip)
 
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)
 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_convert_method (const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &method, symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, safe_pointer< ci_lazy_methodst > lazy_methods, const character_refine_preprocesst &character_refine)
 

Detailed Description

JAVA Bytecode Language Conversion.

Definition in file java_bytecode_convert_method.cpp.

Function Documentation

◆ count_slots()

static size_t count_slots ( const size_t  value,
const code_typet::parametert param 
)
static

◆ gather_symbol_live_ranges()

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

◆ get_bytecode_type_width()

static unsigned get_bytecode_type_width ( const typet ty)
static

◆ get_if_cmp_operator()

static irep_idt get_if_cmp_operator ( const irep_idt stmt)
static

◆ get_variable_slots()

static size_t get_variable_slots ( const code_typet::parametert param)
static

Definition at line 79 of file java_bytecode_convert_method.cpp.

References count_slots().

Referenced by java_bytecode_convert_methodt::convert().

◆ INTEGER_WIDTH()

const size_t INTEGER_WIDTH ( 64u  )

Referenced by count_slots().

◆ java_bytecode_convert_method()

void java_bytecode_convert_method ( const symbolt class_symbol,
const java_bytecode_parse_treet::methodt method,
symbol_tablet symbol_table,
message_handlert message_handler,
size_t  max_array_length,
safe_pointer< ci_lazy_methodst lazy_methods,
const character_refine_preprocesst character_refine 
)

◆ java_bytecode_convert_method_lazy()

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 
)

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: class this method belongs to
method_identifier: fully qualified method name, including type signature (e.g. "x.y.z.f:(I)") m: parsed method object to convert symbol_table: global symbol table (will be modified)

Definition at line 207 of file java_bytecode_convert_method.cpp.

References symbol_tablet::add(), symbolt::base_name, java_bytecode_parse_treet::methodt::base_name, id2string(), 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(), java_type_from_string(), symbolt::location, symbolt::mode, symbolt::name, code_typet::parameters(), symbolt::pretty_name, irept::set(), source_locationt::set_function(), code_typet::parametert::set_this(), java_bytecode_parse_treet::membert::signature, java_bytecode_parse_treet::methodt::source_location, to_code_type(), symbolt::type, and exprt::type().

Referenced by java_bytecode_convert_classt::convert().

◆ operator==()

static bool operator== ( const irep_idt what,
const patternt pattern 
)
static

Definition at line 64 of file java_bytecode_convert_method.cpp.

◆ SLOTS_PER_INTEGER()

const size_t SLOTS_PER_INTEGER ( 1u  )

Referenced by count_slots().

◆ strip_java_namespace_prefix()

static irep_idt strip_java_namespace_prefix ( const irep_idt  to_strip)
static

◆ to_member()

static member_exprt to_member ( const exprt pointer,
const exprt fieldref 
)
static