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

Go to the source code of this file.

Macros

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

Functions

static void create_initialize (symbol_table_baset &symbol_table)
 
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 symboltget_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 void java_static_lifetime_init (symbol_table_baset &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, object_factory_parameterst object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, message_handlert &message_handler)
 
bool is_java_main (const symbolt &function)
 Checks whether the given symbol is a valid java main method i.e. More...
 
exprt::operandst java_build_arguments (const symbolt &function, code_blockt &init_code, symbol_table_baset &symbol_table, bool assume_init_pointers_not_null, object_factory_parameterst object_factory_parameters, const select_pointer_typet &pointer_type_selector)
 Extends init_code with code that allocates the objects used as test arguments for the function under test (function) and non-deterministically initializes them. More...
 
void java_record_outputs (const symbolt &function, const exprt::operandst &main_arguments, code_blockt &init_code, symbol_table_baset &symbol_table)
 
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 object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled)
 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 assume_init_pointers_not_null, bool assert_uncaught_exceptions, const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
 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 26 of file java_entry_point.cpp.

Referenced by get_main_symbol(), and is_java_main().

Function Documentation

◆ constant_bool()

static constant_exprt constant_bool ( bool  val)
static

Definition at line 114 of file java_entry_point.cpp.

References from_integer(), and java_boolean_type().

Referenced by java_static_lifetime_init().

◆ create_initialize()

◆ generate_java_start_function()

bool generate_java_start_function ( const symbolt symbol,
symbol_table_baset symbol_table,
message_handlert message_handler,
bool  assume_init_pointers_not_null,
bool  assert_uncaught_exceptions,
const object_factory_parameterst object_factory_parameters,
const select_pointer_typet pointer_type_selector 
)

Generate a _start function for a specific function.

See java_entry_point for more details.

Parameters
symbolThe symbol representing the function to call
symbol_tableGlobal symbol table
message_handlerWhere to write output to
assume_init_pointers_not_nullWhen creating pointers, assume they always take a non-null value.
max_nondet_array_lengthThe length of the arrays to create when filling them
max_nondet_tree_depthdefines the maximum depth of the object tree (see java_entry_points documentation for details)
pointer_type_selectorLogic for substituting types of pointers
Returns
true if error occurred on entry point search, false otherwise

Definition at line 577 of file java_entry_point.cpp.

References symbol_table_baset::add(), exprt::add_source_location(), code_function_callt::arguments(), symbolt::base_name, exprt::copy_to_operands(), goto_functionst::entry_point(), messaget::eom(), messaget::error(), code_function_callt::function(), code_labelt::get_label(), INITIALIZE_FUNCTION, symbol_table_baset::insert(), symbolt::is_static_lifetime, java_build_arguments(), java_bytecode_instrument_uncaught_exceptions(), JAVA_ENTRY_POINT_EXCEPTION_SYMBOL, JAVA_ENTRY_POINT_RETURN_SYMBOL, java_record_outputs(), java_reference_type(), code_function_callt::lhs(), loc, symbolt::location, irept::make_nil(), message_handler, symbolt::mode, exprt::move_to_operands(), symbolt::name, code_typet::return_type(), irept::swap(), symbolt::symbol_expr(), symbol_table_baset::symbols, to_code_type(), to_pointer_type(), symbolt::type, and symbolt::value.

Referenced by java_entry_point().

◆ 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
symbolpossible class literal symbol
symbol_tabletable to search
Returns
pointer to the initializer method symbol or null

Definition at line 101 of file java_entry_point.cpp.

References get_java_class_literal_initializer_signature(), has_suffix(), id2string(), irept::is_not_nil(), JAVA_CLASS_MODEL_SUFFIX, symbol_table_baset::lookup(), symbolt::name, symbolt::type, and symbolt::value.

Referenced by java_static_lifetime_init().

◆ 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 88 of file java_entry_point.cpp.

Referenced by ci_lazy_methodst::convert_and_analyze_method(), and get_class_literal_initializer().

◆ get_main_symbol()

◆ 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
functionthe function symbol
Returns
true if it is a valid main method

Definition at line 251 of file java_entry_point.cpp.

References irept::get(), has_suffix(), code_typet::has_this(), irept::id(), id2string(), JAVA_MAIN_METHOD, java_type_from_string(), code_typet::parameters(), code_typet::return_type(), dstringt::size(), and to_code_type().

Referenced by get_main_symbol(), and java_build_arguments().

◆ java_build_arguments()

exprt::operandst java_build_arguments ( const symbolt function,
code_blockt init_code,
symbol_table_baset symbol_table,
bool  assume_init_pointers_not_null,
object_factory_parameterst  object_factory_parameters,
const select_pointer_typet pointer_type_selector 
)

Extends init_code with code that allocates the objects used as test arguments for the function under test (function) and non-deterministically initializes them.

All the code generated by this function goes to __CPROVER__start, just before the call to the method under test.

Returns
A std::vector of symbol_exprt, one per parameter of function, containing the objects that can be used as arguments for function.

Definition at line 276 of file java_entry_point.cpp.

References dstringt::empty(), goto_functionst::entry_point(), from_integer(), object_factory_parameterst::function_id, code_typet::parametert::get_base_name(), index_type(), is_java_main(), LOCAL, object_factory_parameterst::max_nonnull_tree_depth, object_factory(), code_typet::parameters(), to_code_type(), to_string(), and exprt::type().

Referenced by generate_java_start_function().

◆ java_entry_point()

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 object_factory_parameterst object_factory_parameters,
const select_pointer_typet pointer_type_selector,
bool  string_refinement_enabled 
)

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:

  1. Allocates and initializes the parameters of the method under test.
  2. Call it and save its return variable in the variable 'return'.
  3. Declare variable 'return' as an output variable (codet with id ID_output), together with other objects possibly altered by the execution 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.
Returns
true if error occurred on entry point search

Definition at line 519 of file java_entry_point.cpp.

References create_initialize(), goto_functionst::entry_point(), generate_java_start_function(), get_main_symbol(), irept::id(), main_function_resultt::is_success(), java_static_lifetime_init(), symbolt::location, main_function_resultt::main_function, message_handler, symbol_table_baset::symbols, and symbolt::type.

Referenced by java_bytecode_languaget::generate_support_functions().

◆ java_record_outputs()

◆ java_static_lifetime_init()

◆ should_init_symbol()