cprover
|
#include <java_string_library_preprocess.h>
Public Member Functions | |
java_string_library_preprocesst () | |
void | initialize_known_type_table () |
void | initialize_conversion_table () |
fill maps with correspondence from java method names to conversion functions | |
bool | implements_function (const irep_idt &function_id) const |
void | get_all_function_names (std::unordered_set< irep_idt > &methods) const |
codet | code_for_function (const symbolt &symbol, symbol_table_baset &symbol_table, message_handlert &message_handler) |
Should be called to provide code for string functions that are used in the code but for which no implementation is provided. | |
codet | replace_character_call (code_function_callt call) |
std::vector< irep_idt > | get_string_type_base_classes (const irep_idt &class_name) |
Gets the base classes for known String and String-related types, or returns an empty list for other types. | |
void | add_string_type (const irep_idt &class_name, symbol_table_baset &symbol_table) |
Add to the symbol table type declaration for a String-like Java class. | |
bool | is_known_string_type (irep_idt class_name) |
Check whether a class name is known as a string type. | |
Static Public Member Functions | |
static bool | implements_java_char_sequence_pointer (const typet &type) |
static bool | implements_java_char_sequence (const typet &type) |
Private Types | |
typedef std::function< codet(const java_method_typet &, const source_locationt &, const irep_idt &, symbol_table_baset &, message_handlert &)> | conversion_functiont |
typedef std::unordered_map< irep_idt, irep_idt > | id_mapt |
Private Member Functions | |
java_string_library_preprocesst (const java_string_library_preprocesst &)=delete | |
code_blockt | make_float_to_string_code (const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler) |
code_blockt | make_copy_string_code (const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler) |
code_blockt | make_copy_constructor_code (const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler) |
code_returnt | make_string_length_code (const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler) |
Generates code for the String.length method. | |
code_blockt | make_class_identifier_code (const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler) |
exprt::operandst | process_parameters (const java_method_typet::parameterst ¶ms, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &init_code) |
calls string_refine_preprocesst::process_operands with a list of parameters. | |
refined_string_exprt | convert_exprt_to_string_exprt (const exprt &deref, const source_locationt &loc, symbol_table_baset &symbol_table, const irep_idt &function_name, code_blockt &init_code) |
Creates a string_exprt from the input exprt representing a char sequence. | |
exprt::operandst | process_operands (const exprt::operandst &operands, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &init_code) |
for each expression that is of a type implementing strings, we declare a new cprover_string whose contents is deduced from the expression, replace the expression by this cprover_string in the output list, and add an assumption that the object is not null; in the other case the expression is kept as is for the output list. | |
refined_string_exprt | replace_char_array (const exprt &array_pointer, const source_locationt &loc, const irep_idt &function_name, symbol_table_baset &symbol_table, code_blockt &code) |
we declare a new cprover_string whose contents is deduced from the char array. | |
symbol_exprt | fresh_string (const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) |
add a symbol with static lifetime and name containing cprover_string and given type | |
refined_string_exprt | decl_string_expr (const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code) |
Add declaration of a refined string expr whose content and length are fresh symbols. | |
refined_string_exprt | make_nondet_string_expr (const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code) |
add symbols with prefix cprover_string_length and cprover_string_data and construct a string_expr from them. | |
exprt | allocate_fresh_string (const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code) |
declare a new String and allocate it | |
codet | code_return_function_application (const irep_idt &function_id, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table) |
return the result of a function call | |
refined_string_exprt | string_expr_of_function (const irep_idt &function_id, const exprt::operandst &arguments, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code) |
codet | code_assign_components_to_java_string (const exprt &lhs, const exprt &rhs_array, const exprt &rhs_length, const symbol_table_baset &symbol_table, bool is_constructor) |
codet | code_assign_string_expr_to_java_string (const exprt &lhs, const refined_string_exprt &rhs, const symbol_table_baset &symbol_table, bool is_constructor) |
void | code_assign_java_string_to_string_expr (const refined_string_exprt &lhs, const exprt &rhs, const source_locationt &loc, const symbol_table_baset &symbol_table, code_blockt &code) |
refined_string_exprt | string_literal_to_string_expr (const std::string &s, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code) |
code_blockt | make_function_from_call (const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table) |
code_blockt | make_init_function_from_call (const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table, bool is_constructor=true) |
code_blockt | make_assign_and_return_function_from_call (const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table) |
code_blockt | make_assign_function_from_call (const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table) |
code_blockt | make_string_returning_function_from_call (const irep_idt &function_id, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table) |
Static Private Member Functions | |
static bool | java_type_matches_tag (const typet &type, const std::string &tag) |
static bool | is_java_string_pointer_type (const typet &type) |
static bool | is_java_string_type (const typet &type) |
static bool | is_java_string_builder_type (const typet &type) |
static bool | is_java_string_builder_pointer_type (const typet &type) |
static bool | is_java_string_buffer_type (const typet &type) |
static bool | is_java_string_buffer_pointer_type (const typet &type) |
static bool | is_java_char_sequence_type (const typet &type) |
static bool | is_java_char_sequence_pointer_type (const typet &type) |
static bool | is_java_char_array_type (const typet &type) |
static bool | is_java_char_array_pointer_type (const typet &type) |
Private Attributes | |
character_refine_preprocesst | character_preprocess |
const typet | char_type |
const typet | index_type |
const refined_string_typet | refined_string_type |
std::unordered_map< irep_idt, conversion_functiont > | conversion_table |
id_mapt | cprover_equivalent_to_java_function |
id_mapt | cprover_equivalent_to_java_string_returning_function |
id_mapt | cprover_equivalent_to_java_constructor |
id_mapt | cprover_equivalent_to_java_assign_and_return_function |
id_mapt | cprover_equivalent_to_java_assign_function |
const std::array< id_mapt *, 5 > | id_maps |
std::unordered_set< irep_idt > | string_types |
Friends | |
refined_string_exprt | convert_exprt_to_string_exprt_unit_test (java_string_library_preprocesst &preprocess, const exprt &deref, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &init_code) |
Definition at line 37 of file java_string_library_preprocess.h.
|
private |
Definition at line 112 of file java_string_library_preprocess.h.
|
private |
Definition at line 114 of file java_string_library_preprocess.h.
|
inline |
Definition at line 40 of file java_string_library_preprocess.h.
|
privatedelete |
void java_string_library_preprocesst::add_string_type | ( | const irep_idt & | class_name, |
symbol_table_baset & | symbol_table ) |
Add to the symbol table type declaration for a String-like Java class.
class_name | a name for the class such as "java.lang.String" |
symbol_table | symbol table to which the class will be added |
Definition at line 220 of file java_string_library_preprocess.cpp.
|
private |
declare a new String and allocate it
type | a type for string |
loc | a location in the program |
function_id | function the fresh string is created in |
symbol_table | symbol table |
code | code block to which allocation instruction will be added |
Definition at line 549 of file java_string_library_preprocess.cpp.
|
private |
|
private |
|
private |
codet java_string_library_preprocesst::code_for_function | ( | const symbolt & | symbol, |
symbol_table_baset & | symbol_table, | ||
message_handlert & | message_handler ) |
Should be called to provide code for string functions that are used in the code but for which no implementation is provided.
symbol | symbol of the function to provide code for |
symbol_table | a symbol table |
message_handler | a message handler |
Definition at line 1461 of file java_string_library_preprocess.cpp.
|
private |
return the result of a function call
function_id | the name of the function |
arguments | a list of arguments |
type | the return type |
symbol_table | a symbol table |
Definition at line 599 of file java_string_library_preprocess.cpp.
|
private |
Creates a string_exprt from the input exprt representing a char sequence.
expr_to_process | an expression of a type which implements char sequence |
loc | location in the source |
symbol_table | symbol table |
function_id | name of the function in which the code will be added |
init_code | code block, in which declaration will be added: |
Definition at line 309 of file java_string_library_preprocess.cpp.
|
private |
Add declaration of a refined string expr whose content and length are fresh symbols.
loc | source location | |
function_id | name of the function in which the string is defined | |
symbol_table | the symbol table | |
[out] | code | code block to which the declaration is added |
Definition at line 487 of file java_string_library_preprocess.cpp.
|
private |
add a symbol with static lifetime and name containing cprover_string
and given type
type | a type for refined strings |
loc | a location in the program |
function_id | name of the function in which the code will be added |
symbol_table | symbol table |
Definition at line 468 of file java_string_library_preprocess.cpp.
void java_string_library_preprocesst::get_all_function_names | ( | std::unordered_set< irep_idt > & | methods | ) | const |
Definition at line 1445 of file java_string_library_preprocess.cpp.
std::vector< irep_idt > java_string_library_preprocesst::get_string_type_base_classes | ( | const irep_idt & | class_name | ) |
Gets the base classes for known String and String-related types, or returns an empty list for other types.
class_name | class identifier, without "java::" prefix. |
Definition at line 187 of file java_string_library_preprocess.cpp.
bool java_string_library_preprocesst::implements_function | ( | const irep_idt & | function_id | ) | const |
Definition at line 1421 of file java_string_library_preprocess.cpp.
|
inlinestatic |
Definition at line 75 of file java_string_library_preprocess.h.
|
inlinestatic |
Definition at line 68 of file java_string_library_preprocess.h.
void java_string_library_preprocesst::initialize_conversion_table | ( | ) |
fill maps with correspondence from java method names to conversion functions
Definition at line 1519 of file java_string_library_preprocess.cpp.
void java_string_library_preprocesst::initialize_known_type_table | ( | ) |
Definition at line 1510 of file java_string_library_preprocess.cpp.
|
staticprivate |
Definition at line 164 of file java_string_library_preprocess.cpp.
|
staticprivate |
type | a type |
Definition at line 155 of file java_string_library_preprocess.cpp.
|
staticprivate |
type | a type |
Definition at line 141 of file java_string_library_preprocess.cpp.
|
staticprivate |
type | a type |
Definition at line 132 of file java_string_library_preprocess.cpp.
|
staticprivate |
type | a type |
Definition at line 118 of file java_string_library_preprocess.cpp.
|
staticprivate |
type | a type |
Definition at line 109 of file java_string_library_preprocess.cpp.
|
staticprivate |
type | a type |
Definition at line 95 of file java_string_library_preprocess.cpp.
|
staticprivate |
type | a type |
Definition at line 86 of file java_string_library_preprocess.cpp.
|
staticprivate |
type | a type |
Definition at line 64 of file java_string_library_preprocess.cpp.
|
staticprivate |
type | a type |
Definition at line 78 of file java_string_library_preprocess.cpp.
bool java_string_library_preprocesst::is_known_string_type | ( | irep_idt | class_name | ) |
Check whether a class name is known as a string type.
class_name | name of the class |
Definition at line 1504 of file java_string_library_preprocess.cpp.
|
staticprivate |
type | a type |
tag | a string |
Definition at line 56 of file java_string_library_preprocess.cpp.
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
|
private |
add symbols with prefix cprover_string_length and cprover_string_data and construct a string_expr from them.
loc | a location in the program |
function_id | name of the function containing the string |
symbol_table | symbol table |
code | code block to which allocation instruction will be added |
Definition at line 512 of file java_string_library_preprocess.cpp.
|
private |
Generates code for the String.length method.
type | type of the function |
loc | location in the source |
function_id | unused |
symbol_table | symbol table |
message_handler | a message handler |
Definition at line 1400 of file java_string_library_preprocess.cpp.
|
private |
|
private |
for each expression that is of a type implementing strings, we declare a new cprover_string
whose contents is deduced from the expression, replace the expression by this cprover_string in the output list, and add an assumption that the object is not null; in the other case the expression is kept as is for the output list.
Also does the same thing for char array references.
operands | a list of expressions |
loc | location in the source |
function_id | name of the function in which the code will be added |
symbol_table | symbol table |
init_code | code block, in which declaration of some arguments may be added |
Definition at line 337 of file java_string_library_preprocess.cpp.
|
private |
calls string_refine_preprocesst::process_operands with a list of parameters.
params | a list of function parameters |
loc | location in the source |
function_id | name of the function in which the code will be added |
symbol_table | symbol table |
init_code | code block, in which declaration of some arguments may be added |
Definition at line 280 of file java_string_library_preprocess.cpp.
|
private |
we declare a new cprover_string
whose contents is deduced from the char array.
array_pointer | an expression of type char array pointer |
loc | location in the source |
function_id | name of the function in which the string is defined |
symbol_table | symbol table |
code | code block, in which some assignments will be added |
Definition at line 431 of file java_string_library_preprocess.cpp.
|
inline |
Definition at line 58 of file java_string_library_preprocess.h.
|
private |
|
private |
|
friend |
|
private |
Definition at line 102 of file java_string_library_preprocess.h.
|
private |
Definition at line 100 of file java_string_library_preprocess.h.
|
private |
Definition at line 117 of file java_string_library_preprocess.h.
|
private |
Definition at line 133 of file java_string_library_preprocess.h.
|
private |
Definition at line 138 of file java_string_library_preprocess.h.
|
private |
Definition at line 129 of file java_string_library_preprocess.h.
|
private |
Definition at line 121 of file java_string_library_preprocess.h.
|
private |
Definition at line 125 of file java_string_library_preprocess.h.
|
private |
Definition at line 140 of file java_string_library_preprocess.h.
|
private |
Definition at line 103 of file java_string_library_preprocess.h.
|
private |
Definition at line 104 of file java_string_library_preprocess.h.
|
private |
Definition at line 152 of file java_string_library_preprocess.h.