cprover
java_bytecode_language.cpp File Reference
Include dependency graph for java_bytecode_language.cpp:

Go to the source code of this file.

Functions

static irep_idt get_virtual_method_target (const std::set< irep_idt > &needed_classes, const irep_idt &call_basename, const irep_idt &classname, const symbol_tablet &symbol_table)
 Find a virtual callee, if one is defined and the callee type is known to exist. More...
 
static void get_virtual_method_targets (const code_function_callt &c, const std::set< irep_idt > &needed_classes, std::vector< irep_idt > &needed_methods, symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy)
 Find possible callees, excluding types that are not known to be instantiated. More...
 
static void gather_virtual_callsites (const exprt &e, std::vector< const code_function_callt *> &result)
 See output. More...
 
static void gather_needed_globals (const exprt &e, const symbol_tablet &symbol_table, symbol_tablet &needed)
 See output. More...
 
static void gather_field_types (const typet &class_type, const namespacet &ns, ci_lazy_methodst &lazy_methods)
 See output. More...
 
static void initialize_needed_classes (const std::vector< irep_idt > &entry_points, const namespacet &ns, const class_hierarchyt &ch, ci_lazy_methodst &lazy_methods)
 See output. More...
 
languagetnew_java_bytecode_language ()
 

Function Documentation

§ gather_field_types()

static void gather_field_types ( const typet class_type,
const namespacet ns,
ci_lazy_methodst lazy_methods 
)
static

See output.

parameters: class_type: root of class tree to search
ns: global namespace
Returns
Populates lazy_methods with all Java reference types reachable starting at class_type. For example if class_type is symbol_typet("java::A") and A has a B field, then B (but not A) will noted as a needed class.

Definition at line 323 of file java_bytecode_language.cpp.

References ci_lazy_methodst::add_needed_class(), namespace_baset::follow(), java_bytecode_languaget::lazy_methods, to_struct_type(), and to_symbol_type().

Referenced by initialize_needed_classes().

§ gather_needed_globals()

static void gather_needed_globals ( const exprt e,
const symbol_tablet symbol_table,
symbol_tablet needed 
)
static

See output.

parameters: e: expression tree to search
symbol_table: global symtab
Returns
Populates needed with global variable symbols referenced from e or its children.

Definition at line 293 of file java_bytecode_language.cpp.

References symbol_tablet::add(), forall_operands, irept::id(), symbol_tablet::symbols, and to_symbol_expr().

Referenced by java_bytecode_languaget::do_ci_lazy_method_conversion().

§ gather_virtual_callsites()

static void gather_virtual_callsites ( const exprt e,
std::vector< const code_function_callt *> &  result 
)
static

See output.

parameters: e: expression tree to search
Returns
Populates result with pointers to each function call within e that calls a virtual function.

Definition at line 273 of file java_bytecode_language.cpp.

References forall_operands, code_function_callt::function(), codet::get_statement(), irept::id(), to_code(), and to_code_function_call().

Referenced by java_bytecode_languaget::do_ci_lazy_method_conversion().

§ get_virtual_method_target()

static irep_idt get_virtual_method_target ( const std::set< irep_idt > &  needed_classes,
const irep_idt call_basename,
const irep_idt classname,
const symbol_tablet symbol_table 
)
static

Find a virtual callee, if one is defined and the callee type is known to exist.

parameters: needed_classes: set of classes that can be instantiated.
Any potential callee not in this set will be ignored. call_basename: unqualified function name with type signature (e.g. "f:(I)") classname: class name that may define or override a function named call_basename. symbol_table: global symtab
Returns
Returns the fully qualified name of classname's definition of call_basename if found and classname is present in needed_classes, or irep_idt() otherwise.

Definition at line 168 of file java_bytecode_language.cpp.

References symbol_tablet::has_symbol(), and id2string().

Referenced by get_virtual_method_targets().

§ get_virtual_method_targets()

static void get_virtual_method_targets ( const code_function_callt c,
const std::set< irep_idt > &  needed_classes,
std::vector< irep_idt > &  needed_methods,
symbol_tablet symbol_table,
const class_hierarchyt class_hierarchy 
)
static

Find possible callees, excluding types that are not known to be instantiated.

parameters: c: function call whose potential target functions should
be determined. needed_classes: set of classes that can be instantiated. Any potential callee not in this set will be ignored. symbol_table: global symtab class_hierarchy: global class hierarchy
Returns
Populates needed_methods with all possible c callees, taking needed_classes into account (virtual function overrides defined on classes that are not 'needed' are ignored)

Definition at line 195 of file java_bytecode_language.cpp.

References symbol_tablet::add(), symbolt::base_name, class_hierarchyt::class_map, code_function_callt::function(), irept::get(), class_hierarchyt::get_children_trans(), get_virtual_method_target(), id2string(), irept::make_nil(), symbolt::mode, symbolt::name, symbolt::type, exprt::type(), and symbolt::value.

Referenced by java_bytecode_languaget::do_ci_lazy_method_conversion().

§ initialize_needed_classes()

static void initialize_needed_classes ( const std::vector< irep_idt > &  entry_points,
const namespacet ns,
const class_hierarchyt ch,
ci_lazy_methodst lazy_methods 
)
static

See output.

parameters: entry_points: list of fully-qualified function names that
we should assume are reachable ns: global namespace ch: global class hierarchy
Returns
Populates lazy_methods with all Java reference types whose references may be passed, directly or indirectly, to any of the functions in entry_points.

Definition at line 354 of file java_bytecode_language.cpp.

References ci_lazy_methodst::add_needed_class(), gather_field_types(), class_hierarchyt::get_parents_trans(), java_bytecode_languaget::lazy_methods, namespacet::lookup(), to_code_type(), and to_symbol_type().

Referenced by java_bytecode_languaget::do_ci_lazy_method_conversion().

§ new_java_bytecode_language()