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 More... | |
void | initialize_refined_string_type () |
bool | implements_function (const irep_idt &function_id) const |
void | get_all_function_names (std::unordered_set< irep_idt > &methods) const |
exprt | code_for_function (const symbolt &symbol, symbol_table_baset &symbol_table) |
Should be called to provide code for string functions that are used in the code but for which no implementation is provided. More... | |
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. More... | |
void | add_string_type (const irep_idt &class_name, symbol_tablet &symbol_table) |
Add to the symbol table type declaration for a String-like Java class. More... | |
bool | is_known_string_type (irep_idt class_name) |
Check whether a class name is known as a string type. More... | |
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 code_typet &, const source_locationt &, const irep_idt &, symbol_table_baset &)> | 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 | |
codet | make_equals_function_code (const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) |
Used to provide code for the Java String.equals(Object) function. More... | |
codet | make_float_to_string_code (const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) |
Provide code for the String.valueOf(F) function. More... | |
codet | make_string_to_char_array_code (const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_tablet &symbol_table) |
codet | make_string_format_code (const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) |
Used to provide code for the Java String.format function. More... | |
codet | make_copy_string_code (const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) |
Generates code for a function which copies a string object to a new string object. More... | |
codet | make_copy_constructor_code (const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) |
Generates code for a constructor of a string object from another string object. More... | |
codet | make_string_length_code (const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) |
Generates code for the String.length method. More... | |
codet | make_object_get_class_code (const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) |
Used to provide our own implementation of the java.lang.Object.getClass() function. More... | |
exprt::operandst | process_parameters (const code_typet::parameterst ¶ms, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code) |
calls string_refine_preprocesst::process_operands with a list of parameters. More... | |
refined_string_exprt | convert_exprt_to_string_exprt (const exprt &deref, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code) |
Creates a string_exprt from the input exprt representing a char sequence. More... | |
exprt::operandst | process_operands (const exprt::operandst &operands, const source_locationt &loc, 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 and replace the expression by this cprover_string in the output list; in the other case the expression is kept as is for the output list. More... | |
exprt::operandst | process_equals_function_operands (const exprt::operandst &operands, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code) |
Converts the operands of the equals function to string expressions and outputs these conversions. More... | |
refined_string_exprt | replace_char_array (const exprt &array_pointer, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code) |
we declare a new cprover_string whose contents is deduced from the char array. More... | |
symbol_exprt | fresh_string (const typet &type, const source_locationt &loc, symbol_table_baset &symbol_table) |
add a symbol with static lifetime and name containing cprover_string and given type More... | |
symbol_exprt | fresh_array (const typet &type, const source_locationt &loc, symbol_tablet &symbol_table) |
add a symbol in the table with static lifetime and name containing cprover_string_array and given type More... | |
refined_string_exprt | decl_string_expr (const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code) |
Add declaration of a refined string expr whose content and length are fresh symbols. More... | |
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. More... | |
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 More... | |
exprt | allocate_fresh_array (const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_tablet &symbol_table, code_blockt &code) |
declare a new character array and allocate it More... | |
codet | code_return_function_application (const irep_idt &function_name, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table) |
return the result of a function call More... | |
refined_string_exprt | string_expr_of_function (const irep_idt &function_name, const exprt::operandst &arguments, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code) |
Create a refined_string_exprt str whose content and length are fresh symbols, calls the string primitive with name function_name . More... | |
codet | code_assign_components_to_java_string (const exprt &lhs, const exprt &rhs_array, const exprt &rhs_length, const symbol_table_baset &symbol_table) |
Produce code for an assignment of a string expr to a Java string. More... | |
codet | code_assign_string_expr_to_java_string (const exprt &lhs, const refined_string_exprt &rhs, const symbol_table_baset &symbol_table) |
Produce code for an assignemnt of a string expr to a Java string. More... | |
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) |
Create a string expression whose value is given by a literal. More... | |
codet | make_function_from_call (const irep_idt &function_name, const code_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table) |
Provide code for a function that calls a function from the solver and simply returns it. More... | |
codet | make_init_function_from_call (const irep_idt &function_name, const code_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table, bool ignore_first_arg=true) |
Generate the goto code for string initialization. More... | |
codet | make_assign_and_return_function_from_call (const irep_idt &function_name, const code_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table) |
Call a cprover internal function, assign the result to object this and return it. More... | |
codet | make_assign_function_from_call (const irep_idt &function_name, const code_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table) |
Call a cprover internal function and assign the result to object this . More... | |
codet | make_string_returning_function_from_call (const irep_idt &function_name, const code_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table) |
Provide code for a function that calls a function from the solver and return the string_expr result as a Java string. More... | |
exprt | make_argument_for_format (const exprt &argv, int index, const struct_typet &structured_type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code) |
Helper for format function. More... | |
exprt | get_primitive_value_of_object (const exprt &object, irep_idt type_name, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code) |
Adds to the code an assignment of the form type_name tmp_type_name tmp_type_name = ((Classname*)arg_i)->value and returns | |
exprt | get_object_at_index (const exprt &argv, int index) |
Helper for format function. More... | |
codet | make_init_from_array_code (const code_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table) |
Used to provide code for constructor from a char array. More... | |
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, symbol_tablet &symbol_table, code_blockt &init_code) |
Additional Inherited Members |
Definition at line 34 of file java_string_library_preprocess.h.
|
private |
Definition at line 106 of file java_string_library_preprocess.h.
|
private |
Definition at line 108 of file java_string_library_preprocess.h.
|
inline |
Definition at line 37 of file java_string_library_preprocess.h.
|
privatedelete |
void java_string_library_preprocesst::add_string_type | ( | const irep_idt & | class_name, |
symbol_tablet & | 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.
References class_typet::add_base(), symbolt::base_name, struct_union_typet::components(), get_string_type_base_classes(), id2string(), symbolt::is_type, java_char_type(), symbolt::mode, symbol_tablet::move(), symbolt::name, pointer_type(), symbolt::pretty_name, java_class_typet::set_access(), struct_union_typet::set_tag(), string_length_type(), and symbolt::type.
Referenced by java_bytecode_convert_classt::operator()().
|
private |
declare a new character array and allocate it
type | a type for string |
loc | a location in the program |
symbol_table | symbol table |
code | code block to which allocation instruction will be added |
Definition at line 593 of file java_string_library_preprocess.cpp.
References code_blockt::add(), allocate_dynamic_object_with_decl(), fresh_array(), and loc.
|
private |
declare a new String and allocate it
type | a type for string |
loc | a location in the program |
symbol_table | symbol table |
code | code block to which allocation instruction will be added |
Definition at line 575 of file java_string_library_preprocess.cpp.
References allocate_dynamic_object_with_decl(), fresh_string(), and loc.
Referenced by make_copy_string_code(), make_float_to_string_code(), make_object_get_class_code(), make_string_format_code(), and make_string_returning_function_from_call().
|
private |
Produce code for an assignment of a string expr to a Java string.
lhs | expression representing the java string to assign to |
rhs_array | pointer to the array to assign |
rhs_length | length of the array to assign |
symbol_table | symbol table |
Definition at line 834 of file java_string_library_preprocess.cpp.
References checked_dereference(), exprt::copy_to_operands(), get_tag(), implements_java_char_sequence_pointer(), java_root_class_init(), symbol_table_baset::lookup(), PRECONDITION, typet::subtype(), to_struct_type(), and exprt::type().
Referenced by code_assign_string_expr_to_java_string().
|
private |
lhs | a string expression | |
rhs | an expression representing a java string | |
loc | source location | |
symbol_table | symbol table | |
[out] | code | code block that gets appended the following code: lhs.length = rhs==null ? 0 : rhs->length lhs.data=rhs->data |
Definition at line 884 of file java_string_library_preprocess.cpp.
References code_blockt::add(), checked_dereference(), refined_string_exprt::content(), from_integer(), get_data(), get_length(), irept::id(), implements_java_char_sequence_pointer(), refined_string_exprt::length(), loc, symbol_table_baset::lookup_ref(), PRECONDITION, irept::set(), typet::subtype(), to_pointer_type(), to_symbol_type(), and exprt::type().
Referenced by convert_exprt_to_string_exprt(), make_argument_for_format(), make_copy_constructor_code(), and make_copy_string_code().
|
private |
Produce code for an assignemnt of a string expr to a Java string.
lhs | an expression representing a java string |
rhs | a string expression |
symbol_table | symbol table |
Definition at line 866 of file java_string_library_preprocess.cpp.
References code_assign_components_to_java_string(), refined_string_exprt::content(), and refined_string_exprt::length().
Referenced by make_copy_constructor_code(), make_copy_string_code(), make_float_to_string_code(), make_init_from_array_code(), make_init_function_from_call(), make_object_get_class_code(), make_string_format_code(), and make_string_returning_function_from_call().
exprt java_string_library_preprocesst::code_for_function | ( | const symbolt & | symbol, |
symbol_table_baset & | symbol_table | ||
) |
Should be called to provide code for string functions that are used in the code but for which no implementation is provided.
function_id | name of the function |
type | its type |
loc | location in the program |
symbol_table | a symbol table |
Definition at line 1882 of file java_string_library_preprocess.cpp.
References conversion_table, cprover_equivalent_to_java_assign_and_return_function, cprover_equivalent_to_java_assign_function, cprover_equivalent_to_java_constructor, cprover_equivalent_to_java_function, cprover_equivalent_to_java_string_returning_function, loc, symbolt::location, make_assign_and_return_function_from_call(), make_assign_function_from_call(), make_function_from_call(), make_init_function_from_call(), make_string_returning_function_from_call(), symbolt::name, to_code_type(), and symbolt::type.
Referenced by java_bytecode_languaget::convert_single_method().
|
private |
return the result of a function call
function_name | the name of the function |
arguments | a list of arguments |
type | the return type |
symbol_table | a symbol table |
Definition at line 636 of file java_string_library_preprocess.cpp.
References make_function_application().
Referenced by make_function_from_call().
|
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 |
init_code | code block, in which declaration will be added: char *cprover_string_content; int cprover_string_length; cprover_string_length = a->length; cprover_string_content = a->data; |
Definition at line 311 of file java_string_library_preprocess.cpp.
References code_assign_java_string_to_string_expr(), decl_string_expr(), implements_java_char_sequence_pointer(), loc, PRECONDITION, and exprt::type().
Referenced by process_equals_function_operands(), and process_operands().
|
private |
Add declaration of a refined string expr whose content and length are fresh symbols.
loc | source location |
symbol_table | the symbol table |
code | [out] : code block to which the declaration is added |
Definition at line 506 of file java_string_library_preprocess.cpp.
References code_blockt::add(), get_fresh_aux_symbol(), index_type, java_char_type(), loc, pointer_type(), refined_string_type, and symbolt::symbol_expr().
Referenced by convert_exprt_to_string_exprt(), make_copy_constructor_code(), make_copy_string_code(), and make_nondet_string_expr().
|
private |
add a symbol in the table with static lifetime and name containing cprover_string_array
and given type
type | an array type |
location | a location in the program |
symbol_table | symbol table |
Definition at line 258 of file java_string_library_preprocess.cpp.
References get_fresh_aux_symbol(), symbolt::is_static_lifetime, and symbolt::symbol_expr().
Referenced by allocate_fresh_array().
|
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 |
symbol_table | symbol table |
Definition at line 489 of file java_string_library_preprocess.cpp.
References get_fresh_aux_symbol(), symbolt::is_static_lifetime, loc, and symbolt::symbol_expr().
Referenced by allocate_fresh_string().
void java_string_library_preprocesst::get_all_function_names | ( | std::unordered_set< irep_idt > & | methods | ) | const |
Definition at line 1865 of file java_string_library_preprocess.cpp.
References add_keys_to_container(), conversion_table, and id_maps.
Referenced by java_bytecode_languaget::methods_provided().
|
private |
Helper for format function.
Returns the expression:
which corresponds to the object at position index
in argv
.
argv | reference to an array of references |
index | index of the desired object |
index
of argv
. Definition at line 1343 of file java_string_library_preprocess.cpp.
References from_integer(), java_int_type(), pointer_type(), typet::subtype(), and exprt::type().
Referenced by make_argument_for_format().
|
private |
Adds to the code an assignment of the form
and returns tmp_typename
.
In case the class corresponding to type_name
is not available in symbol_table
, the variable is declared but not assigned. Used to access the values of the arguments of String.format
.
object | an expression representing a reference to an object |
type_name | name of the corresponding primitive type, this can be one of the following: ID_boolean, ID_char, ID_byte, ID_short, ID_int, ID_long, ID_float, ID_double, ID_void |
loc | a location in the source |
symbol_table | the symbol table |
code | code block to which we are adding some assignments |
tmp_type_name
where type_name
is the given argument (ie. boolean, char etc.). Which represents the primitive value contained in the given object. Definition at line 1245 of file java_string_library_preprocess.cpp.
References code_blockt::add(), DATA_INVARIANT, messaget::eom(), struct_union_typet::get_component(), get_fresh_aux_symbol(), struct_union_typet::componentt::get_name(), id2string(), irept::is_nil(), java_boolean_type(), java_byte_type(), java_char_type(), java_double_type(), java_float_type(), java_int_type(), java_long_type(), java_short_type(), loc, symbol_table_baset::lookup(), pointer_type(), typet::subtype(), symbolt::symbol_expr(), to_struct_type(), exprt::type(), UNREACHABLE, and messaget::warning().
Referenced by make_argument_for_format().
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 194 of file java_string_library_preprocess.cpp.
References is_known_string_type().
Referenced by add_string_type(), and java_bytecode_languaget::parse().
bool java_string_library_preprocesst::implements_function | ( | const irep_idt & | function_id | ) | const |
Definition at line 1841 of file java_string_library_preprocess.cpp.
References conversion_table, and id_maps.
Referenced by java_bytecode_languaget::convert_single_method(), and java_bytecode_languaget::typecheck().
|
inlinestatic |
Definition at line 70 of file java_string_library_preprocess.h.
References is_java_char_sequence_type(), is_java_string_buffer_type(), is_java_string_builder_type(), and is_java_string_type().
Referenced by initialize_nondet_string_struct().
|
inlinestatic |
Definition at line 63 of file java_string_library_preprocess.h.
References is_java_char_sequence_pointer_type(), is_java_string_buffer_pointer_type(), is_java_string_builder_pointer_type(), and is_java_string_pointer_type().
Referenced by code_assign_components_to_java_string(), code_assign_java_string_to_string_expr(), convert_exprt_to_string_exprt(), java_object_factoryt::gen_nondet_pointer_init(), process_equals_function_operands(), and process_operands().
void java_string_library_preprocesst::initialize_conversion_table | ( | ) |
fill maps with correspondence from java method names to conversion functions
Definition at line 1939 of file java_string_library_preprocess.cpp.
References character_preprocess, conversion_table, cprover_equivalent_to_java_assign_and_return_function, cprover_equivalent_to_java_assign_function, cprover_equivalent_to_java_constructor, cprover_equivalent_to_java_function, cprover_equivalent_to_java_string_returning_function, character_refine_preprocesst::initialize_conversion_table(), make_copy_constructor_code(), make_copy_string_code(), make_equals_function_code(), make_float_to_string_code(), make_init_from_array_code(), make_object_get_class_code(), make_string_format_code(), and make_string_length_code().
Referenced by java_bytecode_languaget::typecheck().
void java_string_library_preprocesst::initialize_known_type_table | ( | ) |
Definition at line 1930 of file java_string_library_preprocess.cpp.
References string_types.
Referenced by java_bytecode_languaget::parse().
void java_string_library_preprocesst::initialize_refined_string_type | ( | ) |
|
staticprivate |
Definition at line 159 of file java_string_library_preprocess.cpp.
References irept::id(), is_java_char_array_type(), typet::subtype(), and to_pointer_type().
Referenced by process_operands().
|
staticprivate |
type | a type |
Definition at line 150 of file java_string_library_preprocess.cpp.
References java_type_matches_tag().
Referenced by is_java_char_array_pointer_type().
|
staticprivate |
type | a type |
Definition at line 136 of file java_string_library_preprocess.cpp.
References irept::id(), is_java_char_sequence_type(), typet::subtype(), and to_pointer_type().
Referenced by implements_java_char_sequence_pointer().
|
staticprivate |
type | a type |
Definition at line 127 of file java_string_library_preprocess.cpp.
References java_type_matches_tag().
Referenced by implements_java_char_sequence(), and is_java_char_sequence_pointer_type().
|
staticprivate |
type | a type |
Definition at line 113 of file java_string_library_preprocess.cpp.
References irept::id(), is_java_string_buffer_type(), typet::subtype(), and to_pointer_type().
Referenced by implements_java_char_sequence_pointer().
|
staticprivate |
type | a type |
Definition at line 104 of file java_string_library_preprocess.cpp.
References java_type_matches_tag().
Referenced by implements_java_char_sequence(), and is_java_string_buffer_pointer_type().
|
staticprivate |
type | a type |
Definition at line 90 of file java_string_library_preprocess.cpp.
References irept::id(), is_java_string_builder_type(), typet::subtype(), and to_pointer_type().
Referenced by implements_java_char_sequence_pointer().
|
staticprivate |
type | a type |
Definition at line 81 of file java_string_library_preprocess.cpp.
References java_type_matches_tag().
Referenced by implements_java_char_sequence(), and is_java_string_builder_pointer_type().
|
staticprivate |
type | a type |
Definition at line 59 of file java_string_library_preprocess.cpp.
References irept::id(), is_java_string_type(), typet::subtype(), and to_pointer_type().
Referenced by implements_java_char_sequence_pointer().
|
staticprivate |
type | a type |
Definition at line 73 of file java_string_library_preprocess.cpp.
References java_type_matches_tag().
Referenced by implements_java_char_sequence(), and is_java_string_pointer_type().
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 1924 of file java_string_library_preprocess.cpp.
References string_types.
Referenced by get_string_type_base_classes(), and java_bytecode_convert_classt::operator()().
|
staticprivate |
type | a type |
tag | a string |
Definition at line 51 of file java_string_library_preprocess.cpp.
References get_tag().
Referenced by is_java_char_array_type(), is_java_char_sequence_type(), is_java_string_buffer_type(), is_java_string_builder_type(), and is_java_string_type().
|
private |
Helper for format function.
Adds code:
and returns arg_i_struct
.
TODO: date_time and hash code are not implemented
argv | reference to an array of references |
index | index of the desired argument |
structured_type | type for arguments of the internal format function |
loc | a location in the source |
symbol_table | the symbol table |
code | code block to which we are adding some assignments |
structured_type
representing the possible values of the argument at position index
of argv
. Definition at line 1391 of file java_string_library_preprocess.cpp.
References code_blockt::add(), allocate_dynamic_object_with_decl(), code_assign_java_string_to_string_expr(), struct_union_typet::components(), code_ifthenelset::cond(), exprt::copy_to_operands(), get_fresh_aux_symbol(), get_object_at_index(), get_primitive_value_of_object(), id2string(), java_reference_type(), loc, make_nondet_string_expr(), symbolt::symbol_expr(), to_pointer_type(), to_string_expr(), and exprt::type().
Referenced by make_string_format_code().
|
private |
Call a cprover internal function, assign the result to object this
and return it.
function_name | name of the function to be called |
type | the type of the function call |
loc | location in program |
symbol_table | the symbol table to populate |
Definition at line 1188 of file java_string_library_preprocess.cpp.
References code_blockt::add(), loc, make_assign_function_from_call(), code_typet::parameters(), and PRECONDITION.
Referenced by code_for_function().
|
private |
Call a cprover internal function and assign the result to object this
.
function_name | name of the function to be called |
type | the type of the function call |
loc | location in program |
symbol_table | the symbol table to populate |
Definition at line 1213 of file java_string_library_preprocess.cpp.
References loc, and make_init_function_from_call().
Referenced by code_for_function(), and make_assign_and_return_function_from_call().
|
private |
Generates code for a constructor of a string object from another string object.
type | type of the function |
loc | location in the source |
symbol_table | symbol table |
Definition at line 1745 of file java_string_library_preprocess.cpp.
References code_blockt::add(), code_assign_java_string_to_string_expr(), code_assign_string_expr_to_java_string(), decl_string_expr(), loc, and code_typet::parameters().
Referenced by initialize_conversion_table().
|
private |
Generates code for a function which copies a string object to a new string object.
type | type of the function |
loc | location in the source |
symbol_table | symbol table |
Definition at line 1704 of file java_string_library_preprocess.cpp.
References code_blockt::add(), allocate_fresh_string(), code_assign_java_string_to_string_expr(), code_assign_string_expr_to_java_string(), decl_string_expr(), code_typet::parametert::get_identifier(), loc, code_typet::parameters(), code_typet::return_type(), and exprt::type().
Referenced by initialize_conversion_table().
|
private |
Used to provide code for the Java String.equals(Object) function.
type | type of the function call |
loc | location in the program_invocation_name |
symbol_table | symbol table |
Definition at line 954 of file java_string_library_preprocess.cpp.
References code_blockt::add(), checked_dereference(), code_ifthenelset::cond(), code_ifthenelset::else_case(), from_integer(), get_fresh_aux_symbol(), loc, make_function_application(), code_typet::parameters(), process_equals_function_operands(), code_typet::return_type(), symbolt::symbol_expr(), and code_ifthenelset::then_case().
Referenced by initialize_conversion_table().
|
private |
Provide code for the String.valueOf(F) function.
type | type of the function call |
loc | location in the program_invocation_name |
symbol_table | symbol table |
Definition at line 1004 of file java_string_library_preprocess.cpp.
References code_blockt::add(), allocate_fresh_string(), ieee_floatt::change_spec(), code_assign_string_expr_to_java_string(), code_ifthenelset::cond(), code_ifthenelset::else_case(), ieee_floatt::from_float(), INVARIANT, loc, code_typet::parameters(), PRECONDITION, code_typet::return_type(), string_expr_of_function(), string_literal_to_string_expr(), code_ifthenelset::then_case(), ieee_floatt::to_expr(), and to_floatbv_type().
Referenced by initialize_conversion_table().
|
private |
Provide code for a function that calls a function from the solver and simply returns it.
function_name | name of the function to be called |
type | type of the function |
loc | location in the source |
symbol_table | symbol table |
Definition at line 1633 of file java_string_library_preprocess.cpp.
References code_blockt::add(), code_return_function_application(), loc, code_typet::parameters(), process_parameters(), and code_typet::return_type().
Referenced by code_for_function().
|
private |
Used to provide code for constructor from a char array.
The implementation is similar to substring except the 3rd argument is a count instead of end index
type | type of the function call |
loc | location in the program_invocation_name |
symbol_table | symbol table |
Definition at line 1780 of file java_string_library_preprocess.cpp.
References code_blockt::add(), code_assign_string_expr_to_java_string(), INVARIANT, loc, code_typet::parameters(), PRECONDITION, process_parameters(), string_expr_of_function(), and to_string_expr().
Referenced by initialize_conversion_table().
|
private |
Generate the goto code for string initialization.
function_name | name of the function to be called |
type | the type of the function call |
loc | location in program |
symbol_table | the symbol table to populate |
ignore_first_arg | boolean flag telling that the first argument should not be part of the arguments of the call (but only used to be assigned the result) |
Definition at line 1147 of file java_string_library_preprocess.cpp.
References code_blockt::add(), code_assign_string_expr_to_java_string(), loc, code_typet::parameters(), PRECONDITION, process_parameters(), and string_expr_of_function().
Referenced by code_for_function(), and make_assign_function_from_call().
|
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 |
symbol_table | symbol table |
code | code block to which allocation instruction will be added |
Definition at line 540 of file java_string_library_preprocess.cpp.
References code_blockt::add(), add_array_to_length_association(), add_pointer_to_array_association(), refined_string_exprt::content(), decl_string_expr(), from_integer(), java_int_type(), refined_string_exprt::length(), loc, make_nondet_infinite_char_array(), and exprt::type().
Referenced by make_argument_for_format(), and string_expr_of_function().
|
private |
Used to provide our own implementation of the java.lang.Object.getClass() function.
type | type of the function called |
loc | location in the source |
symbol_table | the symbol table |
Definition at line 1555 of file java_string_library_preprocess.cpp.
References code_blockt::add(), allocate_fresh_string(), code_function_callt::arguments(), checked_dereference(), code_assign_string_expr_to_java_string(), from_integer(), code_function_callt::function(), get_fresh_aux_symbol(), java_int_type(), java_reference_type(), code_function_callt::lhs(), loc, symbol_table_baset::lookup_ref(), code_typet::parameters(), string_expr_of_function(), typet::subtype(), symbolt::type, and exprt::type().
Referenced by initialize_conversion_table().
|
private |
Used to provide code for the Java String.format function.
TODO: date_time and hash code are not implemented, and we set a limit of 10 arguments
type | type of the function call |
loc | location in the program_invocation_name |
symbol_table | symbol table |
Definition at line 1496 of file java_string_library_preprocess.cpp.
References irept::add(), allocate_fresh_string(), code_assign_string_expr_to_java_string(), struct_union_typet::components(), INVARIANT, java_boolean_type(), java_char_type(), java_float_type(), java_int_type(), loc, make_argument_for_format(), MAX_FORMAT_ARGS, code_typet::parameters(), PRECONDITION, process_parameters(), refined_string_type, code_typet::return_type(), and string_expr_of_function().
Referenced by initialize_conversion_table().
|
private |
Generates code for the String.length method.
type | type of the function |
loc | location in the source |
symbol_table | symbol table |
Definition at line 1828 of file java_string_library_preprocess.cpp.
References checked_dereference(), get_length(), code_typet::parameters(), typet::subtype(), and exprt::type().
Referenced by initialize_conversion_table().
|
private |
Provide code for a function that calls a function from the solver and return the string_expr result as a Java string.
function_name | name of the function to be called |
type | type of the function |
loc | location in the source |
symbol_table | symbol table |
Definition at line 1662 of file java_string_library_preprocess.cpp.
References code_blockt::add(), allocate_fresh_string(), code_assign_string_expr_to_java_string(), loc, code_typet::parameters(), process_parameters(), code_typet::return_type(), and string_expr_of_function().
Referenced by code_for_function().
|
private |
|
private |
Converts the operands of the equals function to string expressions and outputs these conversions.
As a side effect of the conversions it adds some code to init_code.
operands | a list of expressions |
loc | location in the source |
symbol_table | symbol table |
init_code | code block, in which declaration of some arguments may be added |
Definition at line 366 of file java_string_library_preprocess.cpp.
References convert_exprt_to_string_exprt(), implements_java_char_sequence_pointer(), loc, PRECONDITION, to_pointer_type(), and exprt::type().
Referenced by make_equals_function_code().
|
private |
for each expression that is of a type implementing strings, we declare a new cprover_string
whose contents is deduced from the expression and replace the expression by this cprover_string in the output list; 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 |
symbol_table | symbol table |
init_code | code block, in which declaration of some arguments may be added |
Definition at line 336 of file java_string_library_preprocess.cpp.
References convert_exprt_to_string_exprt(), implements_java_char_sequence_pointer(), is_java_char_array_pointer_type(), loc, and replace_char_array().
Referenced by process_parameters().
|
private |
calls string_refine_preprocesst::process_operands with a list of parameters.
params | a list of function parameters |
loc | location in the source |
symbol_table | symbol table |
init_code | code block, in which declaration of some arguments may be added |
Definition at line 281 of file java_string_library_preprocess.cpp.
References loc, and process_operands().
Referenced by make_function_from_call(), make_init_from_array_code(), make_init_function_from_call(), make_string_format_code(), and make_string_returning_function_from_call().
|
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 |
symbol_table | symbol table |
code | code block, in which some assignments will be added |
Definition at line 453 of file java_string_library_preprocess.cpp.
References code_blockt::add(), add_pointer_to_array_association(), checked_dereference(), refined_string_exprt::content(), get_data(), get_fresh_aux_symbol(), get_length(), java_char_type(), java_int_type(), loc, refined_string_type, typet::subtype(), symbolt::symbol_expr(), and exprt::type().
Referenced by process_operands().
|
inline |
Definition at line 54 of file java_string_library_preprocess.h.
References character_preprocess, and character_refine_preprocesst::replace_character_call().
Referenced by java_bytecode_convert_methodt::convert_invoke().
|
private |
Create a refined_string_exprt str
whose content and length are fresh symbols, calls the string primitive with name function_name
.
In the arguments of the primitive str
takes the place of the result and the following arguments are given by parameter `arguments.
function_name | the name of the function | |
arguments | arguments of the function | |
loc | source location | |
symbol_table | symbol table | |
[out] | code | gets added the following code: int return_code; int str.length; char str.data[str.length] return_code = <function_name>(str.length, str.data, arguments) |
str
Definition at line 789 of file java_string_library_preprocess.cpp.
References code_blockt::add(), dstringt::c_str(), code_assign_function_application(), refined_string_exprt::content(), get_fresh_aux_symbol(), java_int_type(), refined_string_exprt::length(), loc, make_nondet_string_expr(), and symbolt::symbol_expr().
Referenced by make_float_to_string_code(), make_init_from_array_code(), make_init_function_from_call(), make_object_get_class_code(), make_string_format_code(), make_string_returning_function_from_call(), and string_literal_to_string_expr().
|
private |
Create a string expression whose value is given by a literal.
s | the literal to be assigned | |
loc | location in the source | |
symbol_table | symbol table | |
[out] | code | gets added the following: tmp_string = "<s>" lhs = cprover_string_literal_func(tmp_string) |
Definition at line 928 of file java_string_library_preprocess.cpp.
References loc, and string_expr_of_function().
Referenced by make_float_to_string_code().
|
friend |
|
private |
Definition at line 97 of file java_string_library_preprocess.h.
|
private |
Definition at line 95 of file java_string_library_preprocess.h.
Referenced by initialize_conversion_table(), and replace_character_call().
|
private |
Definition at line 111 of file java_string_library_preprocess.h.
Referenced by code_for_function(), get_all_function_names(), implements_function(), and initialize_conversion_table().
|
private |
Definition at line 127 of file java_string_library_preprocess.h.
Referenced by code_for_function(), and initialize_conversion_table().
|
private |
Definition at line 132 of file java_string_library_preprocess.h.
Referenced by code_for_function(), and initialize_conversion_table().
|
private |
Definition at line 123 of file java_string_library_preprocess.h.
Referenced by code_for_function(), and initialize_conversion_table().
|
private |
Definition at line 115 of file java_string_library_preprocess.h.
Referenced by code_for_function(), and initialize_conversion_table().
|
private |
Definition at line 119 of file java_string_library_preprocess.h.
Referenced by code_for_function(), and initialize_conversion_table().
|
private |
Definition at line 134 of file java_string_library_preprocess.h.
Referenced by get_all_function_names(), and implements_function().
|
private |
Definition at line 98 of file java_string_library_preprocess.h.
Referenced by decl_string_expr().
|
private |
Definition at line 99 of file java_string_library_preprocess.h.
Referenced by decl_string_expr(), make_string_format_code(), and replace_char_array().
|
private |
Definition at line 146 of file java_string_library_preprocess.h.
Referenced by initialize_known_type_table(), and is_known_string_type().