cprover
|
#include "java_entry_point.h"
#include <util/config.h>
#include <util/expr_initializer.h>
#include <util/string_constant.h>
#include <util/suffix.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_object_factory.h"
#include "java_string_literals.h"
#include "java_utils.h"
#include <util/fresh_symbol.h>
#include <util/nondet.h>
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 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 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) |
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, java_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 java_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 java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector) |
Generate a _start function for a specific function. More... | |
#define JAVA_MAIN_METHOD "main:([Ljava/lang/String;)V" |
Definition at line 28 of file java_entry_point.cpp.
|
static |
Definition at line 116 of file java_entry_point.cpp.
|
static |
Definition at line 30 of file java_entry_point.cpp.
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 java_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.
symbol | The symbol representing the function to call |
symbol_table | Global symbol table |
message_handler | Where to write output to |
assume_init_pointers_not_null | When creating pointers, assume they always take a non-null value. |
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 |
Definition at line 666 of file java_entry_point.cpp.
|
static |
If symbol is a class literal, and an appropriate initializer method exists, return a pointer to its symbol.
If not, return null.
symbol | possible class literal symbol |
symbol_table | table to search |
Definition at line 103 of file java_entry_point.cpp.
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);
Definition at line 90 of file java_entry_point.cpp.
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 516 of file java_entry_point.cpp.
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[])
function | the function symbol |
Definition at line 266 of file java_entry_point.cpp.
exprt::operandst java_build_arguments | ( | const symbolt & | function, |
code_blockt & | init_code, | ||
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 | ||
) |
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.
function
, containing the objects that can be used as arguments for function
. Definition at line 291 of file java_entry_point.cpp.
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 | ||
) |
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:
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
Definition at line 610 of file java_entry_point.cpp.
void java_record_outputs | ( | const symbolt & | function, |
const exprt::operandst & | main_arguments, | ||
code_blockt & | init_code, | ||
symbol_table_baset & | symbol_table | ||
) |
Definition at line 440 of file java_entry_point.cpp.
|
static |
Definition at line 121 of file java_entry_point.cpp.
|
static |
Definition at line 58 of file java_entry_point.cpp.