#include "java_entry_point.h"
#include <util/config.h>
#include <util/expr_initializer.h>
#include <util/journalling_symbol_table.h>
#include <util/message.h>
#include <util/suffix.h>
#include <goto-programs/adjust_float_expressions.h>
#include <goto-programs/class_identifier.h>
#include <goto-programs/goto_functions.h>
#include <linking/static_lifetime_init.h>
#include "java_bytecode_instrument.h"
#include "java_bytecode_language.h"
#include "java_object_factory.h"
#include "java_string_literals.h"
#include "java_types.h"
#include "java_utils.h"
#include "nondet.h"
#include <cstring>

Include dependency graph for java_entry_point.cpp:

Macros
#define	JAVA_MAIN_METHOD "main:([Ljava/lang/String;)V"

Functions
static std::optional< codet >	record_return_value (const symbolt &function, const symbol_table_baset &symbol_table)

static code_blockt	record_pointer_parameters (const symbolt &function, const std::vector< exprt > &arguments, const symbol_table_baset &symbol_table)

static codet	record_exception (const symbolt &function, const symbol_table_baset &symbol_table)

void	create_java_initialize (symbol_table_baset &symbol_table)
	Adds `__cprover_initialize` to the `symbol_table` but does not generate code for it yet. More...

static bool	should_init_symbol (const symbolt &sym)

irep_idt	get_java_class_literal_initializer_signature ()
	Get the symbol name of java.lang.Class' initializer method. More...

static const symbolt *	get_class_literal_initializer (const symbolt &symbol, const symbol_table_baset &symbol_table)
	If symbol is a class literal, and an appropriate initializer method exists, return a pointer to its symbol. More...

static constant_exprt	constant_bool (bool val)

static std::unordered_set< irep_idt >	init_symbol (const symbolt &sym, code_blockt &code_block, symbol_table_baset &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, message_handlert &message_handler)

void	java_static_lifetime_init (symbol_table_baset &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, java_object_factory_parameterst object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, message_handlert &message_handler)
	Adds the body to __CPROVER_initialize. More...

bool	is_java_main (const symbolt &function)
	Checks whether the given symbol is a valid java main method i.e. More...

std::pair< code_blockt, std::vector< exprt > >	java_build_arguments (const symbolt &function, symbol_table_baset &symbol_table, bool assume_init_pointers_not_null, java_object_factory_parameterst object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler)

static code_blockt	java_record_outputs (const symbolt &function, const exprt::operandst &main_arguments, symbol_table_baset &symbol_table)
	Mark return value, pointer type parameters and the exception as outputs. More...

main_function_resultt	get_main_symbol (const symbol_table_baset &symbol_table, const irep_idt &main_class, message_handlert &message_handler)
	Figures out the entry point of the code to verify. More...

bool	java_entry_point (symbol_table_baset &symbol_table, const irep_idt &main_class, message_handlert &message_handler, bool assume_init_pointers_not_null, bool assert_uncaught_exceptions, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, const build_argumentst &build_arguments)
	Given the `symbol_table` and the `main_class` to test, this function generates a new function __CPROVER__start that calls the method under tests. More...

bool	generate_java_start_function (const symbolt &symbol, symbol_table_baset &symbol_table, message_handlert &message_handler, bool assert_uncaught_exceptions, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, const build_argumentst &build_arguments)
	Generate a _start function for a specific function. More...

Macro Definition Documentation

◆ JAVA_MAIN_METHOD

#define JAVA_MAIN_METHOD "main:([Ljava/lang/String;)V"

Definition at line 33 of file java_entry_point.cpp.

Function Documentation

◆ constant_bool()

static constant_exprt constant_bool ( bool val )

static

Definition at line 103 of file java_entry_point.cpp.

◆ create_java_initialize()

void create_java_initialize ( symbol_table_baset & symbol_table )

Adds __cprover_initialize to the symbol_table but does not generate code for it yet.

Definition at line 48 of file java_entry_point.cpp.

◆ generate_java_start_function()

bool generate_java_start_function	(	const symbolt &	symbol,
		class symbol_table_baset &	symbol_table,
		class message_handlert &	message_handler,
		bool	assert_uncaught_exceptions,
		const java_object_factory_parameterst &	object_factory_parameters,
		const select_pointer_typet &	pointer_type_selector,
		const build_argumentst &	build_arguments
	)

Generate a _start function for a specific function.

See java_entry_point for more details.

Parameters

symbol	The symbol representing the function to call
symbol_table	Global symbol table
message_handler	Where to write output to
assert_uncaught_exceptions	Add an uncaught-exception check
object_factory_parameters	Parameters for creation of arguments
pointer_type_selector	Logic for substituting types of pointers
build_arguments	The function which builds the `codet`s which initialise the arguments for a function.

Returns: true if error occurred on entry point search, false otherwise

Definition at line 637 of file java_entry_point.cpp.

◆ get_class_literal_initializer()

static const symbolt* get_class_literal_initializer	(	const symbolt &	symbol,
		const symbol_table_baset &	symbol_table
	)

static

If symbol is a class literal, and an appropriate initializer method exists, return a pointer to its symbol.

If not, return null.

Parameters

symbol	possible class literal symbol
symbol_table	table to search

Returns: pointer to the initializer method symbol or null

Definition at line 90 of file java_entry_point.cpp.

◆ get_java_class_literal_initializer_signature()

irep_idt get_java_class_literal_initializer_signature ( )

Get the symbol name of java.lang.Class' initializer method.

This method should initialize a Class instance with known properties of the type it represents, such as its name, whether it is abstract, or an enumeration, etc. The method may or may not exist in any particular symbol table; it is up to the caller to check. The method's Java signature is: void cproverInitializeClassLiteral( String name, boolean isAnnotation, boolean isArray, boolean isInterface, boolean isSynthetic, boolean isLocalClass, boolean isMemberClass, boolean isEnum);

Returns: Class initializer method's symbol name.

Definition at line 77 of file java_entry_point.cpp.

◆ get_main_symbol()

main_function_resultt get_main_symbol	(	const symbol_table_baset &	symbol_table,
		const irep_idt &	main_class,
		message_handlert &	message_handler
	)

Figures out the entry point of the code to verify.

Definition at line 548 of file java_entry_point.cpp.

◆ init_symbol()

static std::unordered_set<irep_idt> init_symbol	(	const symbolt &	sym,
		code_blockt &	code_block,
		symbol_table_baset &	symbol_table,
		const source_locationt &	source_location,
		bool	assume_init_pointers_not_null,
		const java_object_factory_parameterst &	object_factory_parameters,
		const select_pointer_typet &	pointer_type_selector,
		bool	string_refinement_enabled,
		message_handlert &	message_handler
	)

static

Definition at line 108 of file java_entry_point.cpp.

◆ is_java_main()

bool is_java_main ( const symbolt & function )

Checks whether the given symbol is a valid java main method i.e.

it must be public, static, called 'main' and have signature void(String[])

Parameters

function the function symbol

Returns: true if it is a valid main method

Definition at line 305 of file java_entry_point.cpp.

◆ java_build_arguments()

std::pair<code_blockt, std::vector<exprt> > java_build_arguments	(	const symbolt &	function,
		symbol_table_baset &	symbol_table,
		bool	assume_init_pointers_not_null,
		java_object_factory_parameterst	object_factory_parameters,
		const select_pointer_typet &	pointer_type_selector,
		message_handlert &	message_handler
	)

Parameters

function	The function under test, for which to build the arguments.
symbol_table	For the purposes of adding any local variables generated or any functions which are generated and called.
assume_init_pointers_not_null	If this is true then any reference type parameters to the function under tests are assumed to be non-null.
object_factory_parameters	Configuration of the object factory.
pointer_type_selector	Means of selecting the type of value constructed for reference types which are initialised by the code returned.
message_handler	log

Returns: A pairing of the code to initialise the arguments and a std::vector of the expressions for these arguments. The vector contains one element per parameter of function. The vector of expressions can be used as arguments for function. The code returned allocates the objects used as test arguments for the function under test (function) and non-deterministically initializes them. This code returned must be placed into the code block of the function call, before the function call. Typically this code block would be __CPROVER__start.

Definition at line 321 of file java_entry_point.cpp.

◆ java_entry_point()

bool java_entry_point	(	class symbol_table_baset &	symbol_table,
		const irep_idt &	main_class,
		class message_handlert &	message_handler,
		bool	assume_init_pointers_not_null,
		bool	assert_uncaught_exceptions,
		const java_object_factory_parameterst &	object_factory_parameters,
		const select_pointer_typet &	pointer_type_selector,
		bool	string_refinement_enabled,
		const build_argumentst &	build_arguments
	)

Given the symbol_table and the main_class to test, this function generates a new function __CPROVER__start that calls the method under tests.

If __CPROVER__start is already in the symbol_table, it silently returns. Otherwise it finds the method under test using get_main_symbol and constructs a body for __CPROVER__start which does as follows:

Allocates and initializes the parameters of the method under test.
Call it and save its return variable in the variable 'return'.
Declare variable 'return' as an output variable using a code_outputt, together with other objects possibly altered by the execution of the method under test (in java_record_outputs)

When assume_init_pointers_not_null is false, the generated parameter initialization code will non-deterministically set input parameters to either null or a stack-allocated object. Observe that the null/non-null setting only applies to the parameter itself, and is not propagated to other pointers that it might be necessary to initialize in the object tree rooted at the parameter. Parameter max_nondet_array_length provides the maximum length for an array used as part of the input to the method under test, and max_nondet_tree_depth defines the maximum depth of the object tree created for such inputs. This maximum depth is used in conjunction with the so-called "recursive type set" (see field recursive_set in class java_object_factoryt) to bound the depth of the object tree for the parameter. Only when

the depth of the tree is >= max_nondet_tree_depth AND
the type of the object under initialization is already found in the recursive set then that object is not initalized and the reference pointing to it is (deterministically) set to null. This is a source of underapproximation in our approach to test generation, and should perhaps be fixed in the future.

Parameters

symbol_table	Global symbol table
main_class	Identifier of a class within which the main method to be analysed exists. This may be empty if the intention is not to analyse the main method.
message_handler	Where to write output to.
assume_init_pointers_not_null	If this is true then any reference type parameters to the function under tests are assumed to be non-null.
assert_uncaught_exceptions	Add an uncaught-exception check.
object_factory_parameters	Parameters for creation of arguments.
pointer_type_selector	Logic for substituting types of pointers.
string_refinement_enabled	If true, string refinement's string data structure will also be initialised and added to the symbol table.
build_arguments	The function which builds the `codet`s which initialise the arguments for a function.

Returns: true if error occurred on entry point search

Definition at line 602 of file java_entry_point.cpp.

◆ java_record_outputs()

static code_blockt java_record_outputs	(	const symbolt &	function,
		const exprt::operandst &	main_arguments,
		symbol_table_baset &	symbol_table
	)

static

Mark return value, pointer type parameters and the exception as outputs.

Definition at line 476 of file java_entry_point.cpp.

◆ java_static_lifetime_init()

void java_static_lifetime_init	(	symbol_table_baset &	symbol_table,
		const source_locationt &	source_location,
		bool	assume_init_pointers_not_null,
		java_object_factory_parameterst	object_factory_parameters,
		const select_pointer_typet &	pointer_type_selector,
		bool	string_refinement_enabled,
		message_handlert &	message_handler
	)

Adds the body to __CPROVER_initialize.

Definition at line 227 of file java_entry_point.cpp.

◆ record_exception()

static codet record_exception	(	const symbolt &	function,
		const symbol_table_baset &	symbol_table
	)

static

Definition at line 535 of file java_entry_point.cpp.

◆ record_pointer_parameters()

static code_blockt record_pointer_parameters	(	const symbolt &	function,
		const std::vector< exprt > &	arguments,
		const symbol_table_baset &	symbol_table
	)

static

Definition at line 510 of file java_entry_point.cpp.

◆ record_return_value()

static std::optional< codet > record_return_value	(	const symbolt &	function,
		const symbol_table_baset &	symbol_table
	)

static

Definition at line 496 of file java_entry_point.cpp.

◆ should_init_symbol()

static bool should_init_symbol ( const symbolt & sym )

static

Definition at line 61 of file java_entry_point.cpp.

Macros

Functions

Macro Definition Documentation

◆ JAVA_MAIN_METHOD

Function Documentation

◆ constant_bool()

◆ create_java_initialize()

◆ generate_java_start_function()

◆ get_class_literal_initializer()

◆ get_java_class_literal_initializer_signature()

◆ get_main_symbol()

◆ init_symbol()

◆ is_java_main()

◆ java_build_arguments()

◆ java_entry_point()

◆ java_record_outputs()

◆ java_static_lifetime_init()

◆ record_exception()

◆ record_pointer_parameters()

◆ record_return_value()

◆ should_init_symbol()