Loading...

Searching...

No Matches

java_bytecode_language.cpp File Reference

#include "java_bytecode_convert_class.h"
#include <util/cmdline.h>
#include <util/config.h>
#include <util/expr_iterator.h>
#include <util/invariant.h>
#include <util/journalling_symbol_table.h>
#include <util/options.h>
#include <util/suffix.h>
#include <util/symbol_table_builder.h>
#include <goto-programs/class_hierarchy.h>
#include <json/json_parser.h>
#include <linking/static_lifetime_init.h>
#include "ci_lazy_methods.h"
#include "create_array_with_type_intrinsic.h"
#include "expr2java.h"
#include "java_bytecode_concurrency_instrumentation.h"
#include "java_bytecode_convert_method.h"
#include "java_bytecode_instrument.h"
#include "java_bytecode_internal_additions.h"
#include "java_bytecode_language.h"
#include "java_bytecode_typecheck.h"
#include "java_class_loader.h"
#include "java_class_loader_limit.h"
#include "java_entry_point.h"
#include "java_static_initializers.h"
#include "java_string_literal_expr.h"
#include "java_string_literals.h"
#include "java_utils.h"
#include "lambda_synthesis.h"
#include "lift_clinit_calls.h"
#include "load_method_by_regex.h"
#include <fstream>
#include <string>

+ Include dependency graph for java_bytecode_language.cpp:

[フレーム]

Go to the source code of this file.

Functions

void parse_java_language_options (const cmdlinet &cmd, optionst &options)

Parse options that are java bytecode specific.

prefix_filtert get_context (const optionst &options)

static void throwMainClassLoadingError (const std::string &main_class)

static void infer_opaque_type_fields (const java_bytecode_parse_treet &parse_tree, symbol_table_baset &symbol_table)

Infer fields that must exist on opaque types from field accesses against them.

static symbol_exprt get_or_create_class_literal_symbol (const irep_idt &class_id, symbol_table_baset &symbol_table)

Create if necessary, then return the constant global java.lang.Class symbol for a given class id.

static exprt get_ldc_result (const exprt &ldc_arg0, symbol_table_baset &symbol_table, bool string_refinement_enabled)

Get result of a Java load-constant (ldc) instruction.

static void generate_constant_global_variables (java_bytecode_parse_treet &parse_tree, symbol_table_baset &symbol_table, bool string_refinement_enabled)

Creates global variables for constants mentioned in a given method.

static void create_stub_global_symbol (symbol_table_baset &symbol_table, const irep_idt &symbol_id, const irep_idt &symbol_basename, const typet &symbol_type, const irep_idt &class_id, bool force_nondet_init)

Add a stub global symbol to the symbol table, initialising pointer-typed symbols with null and primitive-typed ones with an arbitrary (nondet) value.

static irep_idt get_any_incomplete_ancestor_for_stub_static_field (const irep_idt &start_class_id, const symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy)

Find any incomplete ancestor of a given class that can have a stub static field attached to it.

static void create_stub_global_symbols (const java_bytecode_parse_treet &parse_tree, symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, messaget &log)

Search for getstatic and putstatic instructions in a class' bytecode and create stub symbols for any static fields that aren't already in the symbol table.

static void notify_static_method_calls (const codet &function_body, std::optional< ci_lazy_methods_neededt > needed_lazy_methods)

Notify ci_lazy_methods, if present, of any static function calls made by the given function body.

std::unique_ptr< languaget > new_java_bytecode_language ()

Function Documentation

◆ create_stub_global_symbol()

static void create_stub_global_symbol ( symbol_table_baset & symbol_table,

const irep_idt & symbol_id,

const irep_idt & symbol_basename,

const typet & symbol_type,

const irep_idt & class_id,

bool force_nondet_init

)

static

Add a stub global symbol to the symbol table, initialising pointer-typed symbols with null and primitive-typed ones with an arbitrary (nondet) value.

Parameters: symbol_table table to add to

symbol_id new symbol fully-qualified identifier

symbol_basename new symbol basename

symbol_type new symbol type

class_id class id that directly encloses this static field

force_nondet_init if true, always leave the symbol's value nil so it gets nondet initialized during __CPROVER_initialize. Otherwise, pointer- typed globals are initialized null and we expect a synthetic clinit method to be created later.

Definition at line 636 of file java_bytecode_language.cpp.

◆ create_stub_global_symbols()

static void create_stub_global_symbols ( const java_bytecode_parse_treet & parse_tree,

symbol_table_baset & symbol_table,

const class_hierarchyt & class_hierarchy,

messaget & log

)

static

Search for getstatic and putstatic instructions in a class' bytecode and create stub symbols for any static fields that aren't already in the symbol table.

The new symbols are null-initialized for reference-typed globals / static fields, and nondet-initialized for primitives.

Parameters: parse_tree class bytecode

symbol_table symbol table; may gain new symbols

class_hierarchy global class hierarchy

log message handler used to log warnings when stub static fields are found belonging to non-stub classes.

Definition at line 719 of file java_bytecode_language.cpp.

◆ generate_constant_global_variables()

static void generate_constant_global_variables ( java_bytecode_parse_treet & parse_tree,

symbol_table_baset & symbol_table,

bool string_refinement_enabled

)

static

Creates global variables for constants mentioned in a given method.

These are either string literals, or class literals (the java.lang.Class instance returned by (some_reference_typed_expression).class). The method parse tree is rewritten to directly reference these globals.

Parameters: parse_tree parse tree to search for constant global references

symbol_table global symbol table, to which constant globals will be added.

string_refinement_enabled true if --refine-stings is active, which changes how string literals are structured.

Definition at line 591 of file java_bytecode_language.cpp.

◆ get_any_incomplete_ancestor_for_stub_static_field()

static irep_idt get_any_incomplete_ancestor_for_stub_static_field ( const irep_idt & start_class_id,

const symbol_table_baset & symbol_table,

const class_hierarchyt & class_hierarchy

)

static

Find any incomplete ancestor of a given class that can have a stub static field attached to it.

This specifically excludes java.lang.Object, which we know cannot have static fields.

Parameters: start_class_id class to start searching from

symbol_table global symbol table

class_hierarchy global class hierarchy

Returns: first incomplete ancestor encountered, including start_class_id itself.

Definition at line 677 of file java_bytecode_language.cpp.

◆ get_context()

prefix_filtert get_context ( const optionst & options )

Definition at line 112 of file java_bytecode_language.cpp.

◆ get_ldc_result()

static exprt get_ldc_result ( const exprt & ldc_arg0,

symbol_table_baset & symbol_table,

bool string_refinement_enabled

)

static

Get result of a Java load-constant (ldc) instruction.

Possible cases: 1) Pushing a String causes a reference to a java.lang.String object to be constructed and pushed onto the operand stack. 2) Pushing an int or a float causes a primitive value to be pushed onto the stack. 3) Pushing a Class constant causes a reference to a java.lang.Class to be pushed onto the operand stack

Parameters: ldc_arg0 raw operand to the ldc opcode

symbol_table global symbol table. If the argument ldc_arg0 is a String or Class constant then a new constant global may be added.

string_refinement_enabled true if –refine-strings is enabled, which influences how String literals are structured.

Returns: ldc result

Definition at line 554 of file java_bytecode_language.cpp.

◆ get_or_create_class_literal_symbol()

static symbol_exprt get_or_create_class_literal_symbol ( const irep_idt & class_id,

symbol_table_baset & symbol_table

)

static

Create if necessary, then return the constant global java.lang.Class symbol for a given class id.

Parameters: class_id class identifier

symbol_table global symbol table; a symbol may be added

Returns: java.lang.Class typed symbol expression

Definition at line 513 of file java_bytecode_language.cpp.

◆ infer_opaque_type_fields()

static void infer_opaque_type_fields ( const java_bytecode_parse_treet & parse_tree,

symbol_table_baset & symbol_table

)

static

Infer fields that must exist on opaque types from field accesses against them.

Note that we don't yet try to infer inheritence between opaque types here, so we may introduce the same field onto a type and its ancestor without realising that is in fact the same field, inherited from that ancestor. This can lead to incorrect results when opaque types are cast to other opaque types and their fields do not alias as intended. We set opaque fields as final to avoid assuming they can be overridden.

Parameters: parse_tree class parse tree

symbol_table global symbol table

Definition at line 447 of file java_bytecode_language.cpp.

◆ new_java_bytecode_language()

std::unique_ptr< languaget > new_java_bytecode_language ( )

Definition at line 1532 of file java_bytecode_language.cpp.

◆ notify_static_method_calls()

static void notify_static_method_calls ( const codet & function_body,

std::optional< ci_lazy_methods_neededt > needed_lazy_methods

)

static

Notify ci_lazy_methods, if present, of any static function calls made by the given function body.

Note only static function calls need to be reported – virtual function calls are routinely found by searching the function body after conversion because we can only approximate the possible callees once all function bodies currently believed to be needed have been loaded.

Parameters: function_body function body code

needed_lazy_methods optional ci_lazy_method_neededt interface. If not set, this is a no-op; otherwise, its add_needed_method function will be called for each function call in function_body.

Definition at line 1226 of file java_bytecode_language.cpp.

◆ parse_java_language_options()

void parse_java_language_options ( const cmdlinet & cmd,

optionst & options

)

Parse options that are java bytecode specific.

Parameters: cmd Command line

[out] options The options object that will be updated.

Definition at line 51 of file java_bytecode_language.cpp.

◆ throwMainClassLoadingError()

static void throwMainClassLoadingError ( const std::string & main_class )

static

Definition at line 316 of file java_bytecode_language.cpp.