CBMC
java_string_library_preprocesst Class Reference

#include <java_string_library_preprocess.h>

+ Collaboration diagram for java_string_library_preprocesst:

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...
 
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. More...
 
codet replace_character_call (code_function_callt call)
 
std::vector< irep_idtget_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_table_baset &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 java_method_typet &, const source_locationt &, const irep_idt &, symbol_table_baset &, message_handlert &)> conversion_functiont
 
typedef std::unordered_map< irep_idt, irep_idtid_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)
 Provide code for the String.valueOf(F) function. More...
 
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)
 Generates code for a function which copies a string object to a new string object. More...
 
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)
 Generates code for a constructor of a string object from another string object. More...
 
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. More...
 
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)
 Used to provide our own implementation of the CProver.classIdentifier() function. More...
 
exprt::operandst process_parameters (const java_method_typet::parameterst &params, 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. More...
 
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. More...
 
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. More...
 
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. More...
 
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 More...
 
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. 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...
 
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 More...
 
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)
 Create a refined_string_exprt str whose content and length are fresh symbols, calls the string primitive with name function_id. 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, bool is_constructor)
 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, bool is_constructor)
 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...
 
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)
 Provide code for a function that calls a function from the solver and simply returns it. More...
 
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)
 Generate the goto code for string initialization. More...
 
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)
 Call a cprover internal function, assign the result to object this and return it. More...
 
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)
 Call a cprover internal function and assign the result to object this. More...
 
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)
 Provide code for a function that calls a function from the solver and return the string_expr result as a Java string. 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_functiontconversion_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_idtstring_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)
 

Detailed Description

Definition at line 37 of file java_string_library_preprocess.h.

Member Typedef Documentation

◆ conversion_functiont

◆ id_mapt

typedef std::unordered_map<irep_idt, irep_idt> java_string_library_preprocesst::id_mapt
private

Definition at line 114 of file java_string_library_preprocess.h.

Constructor & Destructor Documentation

◆ java_string_library_preprocesst() [1/2]

java_string_library_preprocesst::java_string_library_preprocesst ( )
inline

Definition at line 40 of file java_string_library_preprocess.h.

◆ java_string_library_preprocesst() [2/2]

java_string_library_preprocesst::java_string_library_preprocesst ( const java_string_library_preprocesst )
privatedelete

Member Function Documentation

◆ add_string_type()

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.

Parameters
class_namea name for the class such as "java.lang.String"
symbol_tablesymbol table to which the class will be added

Definition at line 220 of file java_string_library_preprocess.cpp.

◆ allocate_fresh_string()

exprt java_string_library_preprocesst::allocate_fresh_string ( const typet type,
const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table,
code_blockt code 
)
private

declare a new String and allocate it

Parameters
typea type for string
loca location in the program
function_idfunction the fresh string is created in
symbol_tablesymbol table
codecode block to which allocation instruction will be added
Returns
a new string

Definition at line 549 of file java_string_library_preprocess.cpp.

◆ code_assign_components_to_java_string()

codet java_string_library_preprocesst::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 
)
private

Produce code for an assignment of a string expr to a Java string.

Parameters
lhsexpression representing the java string to assign to
rhs_arraypointer to the array to assign
rhs_lengthlength of the array to assign
symbol_tablesymbol table
is_constructorthe assignment happens in the context of a constructor, so the whole object should be initialised, not just its length and data fields.
Returns
return the following code:
lhs = { {Object}, length=rhs_length, data=rhs_array }

Definition at line 797 of file java_string_library_preprocess.cpp.

◆ code_assign_java_string_to_string_expr()

void java_string_library_preprocesst::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 
)
private
Parameters
lhsa string expression
rhsan expression representing a java string
locsource location
symbol_tablesymbol table
[out]codecode block that gets appended the following code:
lhs.length = rhs==null ? 0 : rhs->length
lhs.data=rhs->data

Definition at line 859 of file java_string_library_preprocess.cpp.

◆ code_assign_string_expr_to_java_string()

codet java_string_library_preprocesst::code_assign_string_expr_to_java_string ( const exprt lhs,
const refined_string_exprt rhs,
const symbol_table_baset symbol_table,
bool  is_constructor 
)
private

Produce code for an assignemnt of a string expr to a Java string.

Parameters
lhsan expression representing a java string
rhsa string expression
symbol_tablesymbol table
is_constructorthe assignment happens in the context of a constructor, so the whole object should be initialised, not just its length and data fields.
Returns
return the following code:
lhs = { {Object}, length=rhs.length, data=rhs.data }

Definition at line 840 of file java_string_library_preprocess.cpp.

◆ code_for_function()

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.

Parameters
symbolsymbol of the function to provide code for
symbol_tablea symbol table
message_handlera message handler
Returns
Code for the body of the String functions if they are part of the supported String functions, nil_exprt otherwise.

Definition at line 1461 of file java_string_library_preprocess.cpp.

◆ code_return_function_application()

codet java_string_library_preprocesst::code_return_function_application ( const irep_idt function_id,
const exprt::operandst arguments,
const typet type,
symbol_table_baset symbol_table 
)
private

return the result of a function call

Parameters
function_idthe name of the function
argumentsa list of arguments
typethe return type
symbol_tablea symbol table
Returns
the following code:
return <function_id>(arguments)

Definition at line 599 of file java_string_library_preprocess.cpp.

◆ convert_exprt_to_string_exprt()

refined_string_exprt java_string_library_preprocesst::convert_exprt_to_string_exprt ( const exprt expr_to_process,
const source_locationt loc,
symbol_table_baset symbol_table,
const irep_idt function_id,
code_blockt init_code 
)
private

Creates a string_exprt from the input exprt representing a char sequence.

Parameters
expr_to_processan expression of a type which implements char sequence
loclocation in the source
symbol_tablesymbol table
function_idname of the function in which the code will be added
init_codecode 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;
Returns
the processed operand: {content=cprover_string_content, length=cprover_string_length}

Definition at line 309 of file java_string_library_preprocess.cpp.

◆ decl_string_expr()

refined_string_exprt java_string_library_preprocesst::decl_string_expr ( const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table,
code_blockt code 
)
private

Add declaration of a refined string expr whose content and length are fresh symbols.

Parameters
locsource location
function_idname of the function in which the string is defined
symbol_tablethe symbol table
[out]codecode block to which the declaration is added
Returns
refined string expr with fresh content and length symbols

Definition at line 487 of file java_string_library_preprocess.cpp.

◆ fresh_string()

symbol_exprt java_string_library_preprocesst::fresh_string ( const typet type,
const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table 
)
private

add a symbol with static lifetime and name containing cprover_string and given type

Parameters
typea type for refined strings
loca location in the program
function_idname of the function in which the code will be added
symbol_tablesymbol table
Returns
a new symbol

Definition at line 468 of file java_string_library_preprocess.cpp.

◆ get_all_function_names()

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.

◆ get_string_type_base_classes()

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.

Parameters
class_nameclass identifier, without "java::" prefix.
Returns
a list of base classes, again without "java::" prefix.

Definition at line 187 of file java_string_library_preprocess.cpp.

◆ implements_function()

bool java_string_library_preprocesst::implements_function ( const irep_idt function_id) const

Definition at line 1421 of file java_string_library_preprocess.cpp.

◆ implements_java_char_sequence()

static bool java_string_library_preprocesst::implements_java_char_sequence ( const typet type)
inlinestatic

Definition at line 75 of file java_string_library_preprocess.h.

◆ implements_java_char_sequence_pointer()

static bool java_string_library_preprocesst::implements_java_char_sequence_pointer ( const typet type)
inlinestatic

Definition at line 68 of file java_string_library_preprocess.h.

◆ initialize_conversion_table()

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.

◆ initialize_known_type_table()

void java_string_library_preprocesst::initialize_known_type_table ( )

Definition at line 1510 of file java_string_library_preprocess.cpp.

◆ is_java_char_array_pointer_type()

bool java_string_library_preprocesst::is_java_char_array_pointer_type ( const typet type)
staticprivate
parameters: a type
Returns
Boolean telling whether the type is that of a pointer to a java char array

Definition at line 164 of file java_string_library_preprocess.cpp.

◆ is_java_char_array_type()

bool java_string_library_preprocesst::is_java_char_array_type ( const typet type)
staticprivate
Parameters
typea type
Returns
Boolean telling whether the type is that of java char array

Definition at line 155 of file java_string_library_preprocess.cpp.

◆ is_java_char_sequence_pointer_type()

bool java_string_library_preprocesst::is_java_char_sequence_pointer_type ( const typet type)
staticprivate
Parameters
typea type
Returns
Boolean telling whether the type is that of a pointer to a java char sequence

Definition at line 141 of file java_string_library_preprocess.cpp.

◆ is_java_char_sequence_type()

bool java_string_library_preprocesst::is_java_char_sequence_type ( const typet type)
staticprivate
Parameters
typea type
Returns
Boolean telling whether the type is that of java char sequence

Definition at line 132 of file java_string_library_preprocess.cpp.

◆ is_java_string_buffer_pointer_type()

bool java_string_library_preprocesst::is_java_string_buffer_pointer_type ( const typet type)
staticprivate
Parameters
typea type
Returns
Boolean telling whether the type is that of java StringBuffer pointers

Definition at line 118 of file java_string_library_preprocess.cpp.

◆ is_java_string_buffer_type()

bool java_string_library_preprocesst::is_java_string_buffer_type ( const typet type)
staticprivate
Parameters
typea type
Returns
Boolean telling whether the type is that of java StringBuffer

Definition at line 109 of file java_string_library_preprocess.cpp.

◆ is_java_string_builder_pointer_type()

bool java_string_library_preprocesst::is_java_string_builder_pointer_type ( const typet type)
staticprivate
Parameters
typea type
Returns
Boolean telling whether the type is that of java StringBuilder pointers

Definition at line 95 of file java_string_library_preprocess.cpp.

◆ is_java_string_builder_type()

bool java_string_library_preprocesst::is_java_string_builder_type ( const typet type)
staticprivate
Parameters
typea type
Returns
Boolean telling whether the type is that of java StringBuilder

Definition at line 86 of file java_string_library_preprocess.cpp.

◆ is_java_string_pointer_type()

bool java_string_library_preprocesst::is_java_string_pointer_type ( const typet type)
staticprivate
Parameters
typea type
Returns
Boolean telling whether the type is that of java string pointer

Definition at line 64 of file java_string_library_preprocess.cpp.

◆ is_java_string_type()

bool java_string_library_preprocesst::is_java_string_type ( const typet type)
staticprivate
Parameters
typea type
Returns
Boolean telling whether the type is that of java string

Definition at line 78 of file java_string_library_preprocess.cpp.

◆ is_known_string_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.

Parameters
class_namename of the class
Returns
True if the type is one that is known to our preprocessing, false otherwise

Definition at line 1504 of file java_string_library_preprocess.cpp.

◆ java_type_matches_tag()

bool java_string_library_preprocesst::java_type_matches_tag ( const typet type,
const std::string &  tag 
)
staticprivate
Parameters
typea type
taga string
Returns
Boolean telling whether the type is a struct with the given tag or a symbolic type with the tag prefixed by "java::"

Definition at line 56 of file java_string_library_preprocess.cpp.

◆ make_assign_and_return_function_from_call()

code_blockt java_string_library_preprocesst::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 
)
private

Call a cprover internal function, assign the result to object this and return it.

Parameters
function_idname of the function to be called
typethe type of the function call
loclocation in program
symbol_tablethe symbol table to populate
Returns
Code calling function with the given function name.

Definition at line 1121 of file java_string_library_preprocess.cpp.

◆ make_assign_function_from_call()

code_blockt java_string_library_preprocesst::make_assign_function_from_call ( const irep_idt function_id,
const java_method_typet type,
const source_locationt loc,
symbol_table_baset symbol_table 
)
private

Call a cprover internal function and assign the result to object this.

Parameters
function_idname of the function to be called
typethe type of the function call
loclocation in program
symbol_tablethe symbol table to populate
Returns
Code assigning result of a call to the function with given function name.

Definition at line 1146 of file java_string_library_preprocess.cpp.

◆ make_class_identifier_code()

code_blockt java_string_library_preprocesst::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 
)
private

Used to provide our own implementation of the CProver.classIdentifier() function.

Parameters
typetype of the function called
loclocation in the source
function_idfunction the generated code will be added to
symbol_tablethe symbol table
message_handlera message handler
Returns
Code corresponding to
string_expr1 = substr(obj->@class_identifier, 6)
return string_expr1;

Definition at line 1170 of file java_string_library_preprocess.cpp.

◆ make_copy_constructor_code()

code_blockt java_string_library_preprocesst::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 
)
private

Generates code for a constructor of a string object from another string object.

Parameters
typetype of the function
loclocation in the source
function_idname of the function (used for variable naming) where the generated code ends up.
symbol_tablesymbol table
message_handlera message handler
Returns
Code corresponding to:
string_expr = java_string_to_string_expr(arg1)
string_expr_sym = { string_expr.length; string_expr.content }
this = string_expr_to_java_string(string_expr)

Definition at line 1355 of file java_string_library_preprocess.cpp.

◆ make_copy_string_code()

code_blockt java_string_library_preprocesst::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 
)
private

Generates code for a function which copies a string object to a new string object.

Parameters
typetype of the function
loclocation in the source
function_idfunction the generated code will be added to
symbol_tablesymbol table
message_handlera message handler
Returns
Code corresponding to:
string_expr = string_to_string_expr(arg0)
string_expr_sym = { string_expr.length; string_expr.content }
str = new String
str = string_expr_to_string(string_expr)
return str

Definition at line 1305 of file java_string_library_preprocess.cpp.

◆ make_float_to_string_code()

code_blockt java_string_library_preprocesst::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 
)
private

Provide code for the String.valueOf(F) function.

Parameters
typetype of the function call
loclocation in the program_invocation_name
function_idfunction the generated code will be added to
symbol_tablesymbol table
message_handlera message handler
Returns
Code corresponding to the Java conversion of floats to strings.

Definition at line 917 of file java_string_library_preprocess.cpp.

◆ make_function_from_call()

code_blockt java_string_library_preprocesst::make_function_from_call ( const irep_idt function_id,
const java_method_typet type,
const source_locationt loc,
symbol_table_baset symbol_table 
)
private

Provide code for a function that calls a function from the solver and simply returns it.

Parameters
function_idname of the function to be called
typetype of the function
loclocation in the source
symbol_tablesymbol table
Returns
Code corresponding to:
return function_id(args)

Definition at line 1230 of file java_string_library_preprocess.cpp.

◆ make_init_function_from_call()

code_blockt java_string_library_preprocesst::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 
)
private

Generate the goto code for string initialization.

Parameters
function_idname of the function to be called
typethe type of the function call
loclocation in program
symbol_tablethe symbol table to populate
is_constructorthe function being made is a constructor, so the whole object should be initialised, not just its length and data fields.
Returns
code for the String.<init>(args) function:
cprover_string_length = fun(arg).length;
cprover_string_array = fun(arg).data;
this->length = cprover_string_length;
this->data = cprover_string_array;
cprover_string = {.=cprover_string_length, .=cprover_string_array};

Definition at line 1077 of file java_string_library_preprocess.cpp.

◆ make_nondet_string_expr()

refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr ( const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table,
code_blockt code 
)
private

add symbols with prefix cprover_string_length and cprover_string_data and construct a string_expr from them.

Parameters
loca location in the program
function_idname of the function containing the string
symbol_tablesymbol table
codecode block to which allocation instruction will be added
Returns
a new string_expr

Definition at line 512 of file java_string_library_preprocess.cpp.

◆ make_string_length_code()

code_returnt java_string_library_preprocesst::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 
)
private

Generates code for the String.length method.

Parameters
typetype of the function
loclocation in the source
function_idunused
symbol_tablesymbol table
message_handlera message handler
Returns
Code corresponding to:
str_expr = java_string_to_string_expr(this)
str_expr_sym = str_expr
return this->length

Definition at line 1400 of file java_string_library_preprocess.cpp.

◆ make_string_returning_function_from_call()

code_blockt java_string_library_preprocesst::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 
)
private

Provide code for a function that calls a function from the solver and return the string_expr result as a Java string.

Parameters
function_idname of the function to be called
typetype of the function
loclocation in the source
symbol_tablesymbol table
Returns
Code corresponding to:
string_expr = function_id(args)
string = new String
string = string_expr_to_string(string)
return string

Definition at line 1260 of file java_string_library_preprocess.cpp.

◆ process_operands()

exprt::operandst java_string_library_preprocesst::process_operands ( const exprt::operandst operands,
const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table,
code_blockt init_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, 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.

Parameters
operandsa list of expressions
loclocation in the source
function_idname of the function in which the code will be added
symbol_tablesymbol table
init_codecode block, in which declaration of some arguments may be added
Returns
a list of expressions

Definition at line 337 of file java_string_library_preprocess.cpp.

◆ process_parameters()

exprt::operandst java_string_library_preprocesst::process_parameters ( const java_method_typet::parameterst params,
const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table,
code_blockt init_code 
)
private

calls string_refine_preprocesst::process_operands with a list of parameters.

Parameters
paramsa list of function parameters
loclocation in the source
function_idname of the function in which the code will be added
symbol_tablesymbol table
init_codecode block, in which declaration of some arguments may be added
Returns
a list of expressions

Definition at line 280 of file java_string_library_preprocess.cpp.

◆ replace_char_array()

refined_string_exprt java_string_library_preprocesst::replace_char_array ( const exprt array_pointer,
const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table,
code_blockt code 
)
private

we declare a new cprover_string whose contents is deduced from the char array.

Parameters
array_pointeran expression of type char array pointer
loclocation in the source
function_idname of the function in which the string is defined
symbol_tablesymbol table
codecode block, in which some assignments will be added
Returns
a string expression

Definition at line 431 of file java_string_library_preprocess.cpp.

◆ replace_character_call()

codet java_string_library_preprocesst::replace_character_call ( code_function_callt  call)
inline

Definition at line 58 of file java_string_library_preprocess.h.

◆ string_expr_of_function()

refined_string_exprt java_string_library_preprocesst::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 
)
private

Create a refined_string_exprt str whose content and length are fresh symbols, calls the string primitive with name function_id.

In the arguments of the primitive str takes the place of the result and the following arguments are given by parameter `arguments.

Parameters
function_idthe name of the function
argumentsarguments of the function
locsource location
symbol_tablesymbol table
[out]codegets added the following code:
int return_code;
int str.length;
char str.data[str.length]
return_code = <function_id>(str.length, str.data, arguments)
Returns
refined string expression str

Definition at line 750 of file java_string_library_preprocess.cpp.

◆ string_literal_to_string_expr()

refined_string_exprt java_string_library_preprocesst::string_literal_to_string_expr ( const std::string &  s,
const source_locationt loc,
symbol_table_baset symbol_table,
code_blockt code 
)
private

Create a string expression whose value is given by a literal.

Parameters
sthe literal to be assigned
loclocation in the source
symbol_tablesymbol table
[out]codegets added the following:
tmp_string = "<s>"
lhs = cprover_string_literal_func(tmp_string)
Returns
a new refined string

Definition at line 896 of file java_string_library_preprocess.cpp.

Friends And Related Function Documentation

◆ convert_exprt_to_string_exprt_unit_test

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 
)
friend

Member Data Documentation

◆ char_type

const typet java_string_library_preprocesst::char_type
private

Definition at line 102 of file java_string_library_preprocess.h.

◆ character_preprocess

character_refine_preprocesst java_string_library_preprocesst::character_preprocess
private

Definition at line 100 of file java_string_library_preprocess.h.

◆ conversion_table

std::unordered_map<irep_idt, conversion_functiont> java_string_library_preprocesst::conversion_table
private

Definition at line 117 of file java_string_library_preprocess.h.

◆ cprover_equivalent_to_java_assign_and_return_function

id_mapt java_string_library_preprocesst::cprover_equivalent_to_java_assign_and_return_function
private

Definition at line 133 of file java_string_library_preprocess.h.

◆ cprover_equivalent_to_java_assign_function

id_mapt java_string_library_preprocesst::cprover_equivalent_to_java_assign_function
private

Definition at line 138 of file java_string_library_preprocess.h.

◆ cprover_equivalent_to_java_constructor

id_mapt java_string_library_preprocesst::cprover_equivalent_to_java_constructor
private

Definition at line 129 of file java_string_library_preprocess.h.

◆ cprover_equivalent_to_java_function

id_mapt java_string_library_preprocesst::cprover_equivalent_to_java_function
private

Definition at line 121 of file java_string_library_preprocess.h.

◆ cprover_equivalent_to_java_string_returning_function

id_mapt java_string_library_preprocesst::cprover_equivalent_to_java_string_returning_function
private

Definition at line 125 of file java_string_library_preprocess.h.

◆ id_maps

◆ index_type

const typet java_string_library_preprocesst::index_type
private

Definition at line 103 of file java_string_library_preprocess.h.

◆ refined_string_type

const refined_string_typet java_string_library_preprocesst::refined_string_type
private

Definition at line 104 of file java_string_library_preprocess.h.

◆ string_types

std::unordered_set<irep_idt> java_string_library_preprocesst::string_types
private

Definition at line 152 of file java_string_library_preprocess.h.


The documentation for this class was generated from the following files: