#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:

Functions
void	parse_java_language_options (const cmdlinet &cmd, optionst &options)
	Parse options that are java bytecode specific. More...

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. More...

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. More...

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. More...

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. More...

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. More...

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. More...

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. More...

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. More...

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.

Functions

Function Documentation

◆ create_stub_global_symbol()

◆ create_stub_global_symbols()

◆ generate_constant_global_variables()

◆ get_any_incomplete_ancestor_for_stub_static_field()

◆ get_context()

◆ get_ldc_result()

◆ get_or_create_class_literal_symbol()

◆ infer_opaque_type_fields()

◆ new_java_bytecode_language()

◆ notify_static_method_calls()

◆ parse_java_language_options()

◆ throwMainClassLoadingError()