cprover
java_string_library_preprocesst Class Reference

#include <java_string_library_preprocess.h>

+ Inheritance diagram for java_string_library_preprocesst:
+ 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)
 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_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...
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. More...
 

Static Public Member Functions

static bool implements_java_char_sequence_pointer (const typet &type)
 
static bool implements_java_char_sequence (const typet &type)
 
- Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
 

Private Types

typedef std::function< codet(const java_method_typet &, const source_locationt &, const irep_idt &, symbol_table_baset &)> 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)
 Provide code for the String.valueOf(F) function. More...
 
code_blockt make_string_format_code (const java_method_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...
 
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)
 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)
 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)
 Generates code for the String.length method. More...
 
code_blockt make_object_get_class_code (const java_method_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 java_method_typet::parameterst &params, 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...
 
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, 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_name, 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_name, 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_name, 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_name, 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_name, 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...
 
struct_exprt make_argument_for_format (const exprt &argv, std::size_t 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...
 
optionalt< symbol_exprtget_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 tmp_typename. More...

 
dereference_exprt get_object_at_index (const exprt &argv, std::size_t index)
 Helper for format function. 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, symbol_tablet &symbol_table, code_blockt &init_code)
 

Additional Inherited Members

- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Attributes inherited from messaget
static eomt eom
 
static const commandt reset
 return to default formatting, as defined by the terminal More...
 
static const commandt red
 render text with red foreground color More...
 
static const commandt green
 render text with green foreground color More...
 
static const commandt yellow
 render text with yellow foreground color More...
 
static const commandt blue
 render text with blue foreground color More...
 
static const commandt magenta
 render text with magenta foreground color More...
 
static const commandt cyan
 render text with cyan foreground color More...
 
static const commandt bright_red
 render text with bright red foreground color More...
 
static const commandt bright_green
 render text with bright green foreground color More...
 
static const commandt bright_yellow
 render text with bright yellow foreground color More...
 
static const commandt bright_blue
 render text with bright blue foreground color More...
 
static const commandt bright_magenta
 render text with bright magenta foreground color More...
 
static const commandt bright_cyan
 render text with bright cyan foreground color More...
 
static const commandt bold
 render text with bold font More...
 
static const commandt faint
 render text with faint font More...
 
static const commandt italic
 render italic text More...
 
static const commandt underline
 render underlined text More...
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Detailed Description

Definition at line 35 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 108 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 38 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_tablet 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 208 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 570 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 828 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 892 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 873 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 
)

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
Returns
Code for the body of the String functions if they are part of the supported String functions, nil_exprt otherwise.

Definition at line 1800 of file java_string_library_preprocess.cpp.

◆ code_return_function_application()

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

return the result of a function call

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

Definition at line 611 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,
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
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 301 of file java_string_library_preprocess.cpp.

◆ decl_string_expr()

refined_string_exprt java_string_library_preprocesst::decl_string_expr ( const source_locationt loc,
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
symbol_tablethe symbol table
code[out] : code block to which the declaration is added
Returns
refined string expr with fresh content and length symbols

Definition at line 499 of file java_string_library_preprocess.cpp.

◆ fresh_array()

symbol_exprt java_string_library_preprocesst::fresh_array ( const typet type,
const source_locationt location,
symbol_tablet symbol_table 
)
private

add a symbol in the table with static lifetime and name containing cprover_string_array and given type

Parameters
typean array type
locationa location in the program
symbol_tablesymbol table

Definition at line 248 of file java_string_library_preprocess.cpp.

◆ fresh_string()

symbol_exprt java_string_library_preprocesst::fresh_string ( const typet type,
const source_locationt loc,
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
symbol_tablesymbol table
Returns
a new symbol

Definition at line 482 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 1785 of file java_string_library_preprocess.cpp.

◆ get_object_at_index()

dereference_exprt java_string_library_preprocesst::get_object_at_index ( const exprt argv,
std::size_t  index 
)
private

Helper for format function.

Returns the expression:

*((void**)(argv->data)+index )

which corresponds to the object at position index in argv.

Parameters
argvreference to an array of references
indexindex of the desired object
Returns
An expression representing the object at position index of argv.

Definition at line 1293 of file java_string_library_preprocess.cpp.

◆ get_primitive_value_of_object()

optionalt< symbol_exprt > java_string_library_preprocesst::get_primitive_value_of_object ( const exprt object,
irep_idt  type_name,
const source_locationt loc,
symbol_table_baset symbol_table,
code_blockt code 
)
private

Adds to the code an assignment of the form

type_name tmp_type_name
tmp_type_name = ((Classname*)arg_i)->value

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.

Parameters
objectan expression representing a reference to an object
type_namename 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
loca location in the source
symbol_tablethe symbol table
codecode block to which we are adding some assignments
Returns
An expression contaning a symbol 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 1195 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 182 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 1761 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 70 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 63 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 1857 of file java_string_library_preprocess.cpp.

◆ initialize_known_type_table()

void java_string_library_preprocesst::initialize_known_type_table ( )

Definition at line 1848 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 159 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 150 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 136 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 127 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 113 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 104 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 90 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 81 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 59 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 73 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 1842 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 51 of file java_string_library_preprocess.cpp.

◆ make_argument_for_format()

struct_exprt java_string_library_preprocesst::make_argument_for_format ( const exprt argv,
std::size_t  index,
const struct_typet structured_type,
const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_table,
code_blockt code 
)
private

Helper for format function.

Adds code:

string_expr arg_i_string_expr;
int tmp_int;
float tmp_float;
char tmp_char;
boolean tmp_boolean;
Object* arg_i=get_object_at_index(argv, index)
if(arg_i.@class_identifier=="java::java.lang.String")
{
arg_i_string_expr = (string_expr)((String*)arg_i_as_string)
}
tmp_int=((Integer)arg_i)->value
tmp_float=((Float)arg_i)->value
tmp_char=((Char)arg_i)->value
tmp_boolean=((Boolean)arg_i)->value
arg_i_struct = { string_expr=arg_i_string_expr;
integer=tmp_int; float=tmp_float; char=tmp_char; boolean=tmp_boolean}

and returns arg_i_struct.

TODO: date_time and hash code are not implemented

Parameters
argvreference to an array of references
indexindex of the desired argument
structured_typetype for arguments of the internal format function
loca location in the source
function_idfunction the generated expression will be used in
symbol_tablethe symbol table
codecode block to which we are adding some assignments
Returns
An expression of type structured_type representing the possible values of the argument at position index of argv.

Definition at line 1338 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_name,
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_namename 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 1138 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_name,
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_namename 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 1163 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 
)
private

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

Parameters
typetype of the function
loclocation in the source
function_idunused
symbol_tablesymbol table
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 1701 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 
)
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
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 1658 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 
)
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
Returns
Code corresponding to the Java conversion of floats to strings.

Definition at line 955 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_name,
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_namename of the function to be called
typetype of the function
loclocation in the source
symbol_tablesymbol table
Returns
Code corresponding to:
return function_name(args)

Definition at line 1584 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_name,
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_namename 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 1096 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 534 of file java_string_library_preprocess.cpp.

◆ make_object_get_class_code()

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

Used to provide our own implementation of the java.lang.Object.getClass() function.

Parameters
typetype of the function called
loclocation in the source
function_idfunction the generated code will be added to
symbol_tablethe symbol table
Returns
Code corresponding to
Class class1;
string_expr1 = substr(this->@class_identifier, 6)
class1=Class.forName(string_expr1)
return class1

Definition at line 1504 of file java_string_library_preprocess.cpp.

◆ make_string_format_code()

code_blockt java_string_library_preprocesst::make_string_format_code ( const java_method_typet type,
const source_locationt loc,
const irep_idt function_id,
symbol_table_baset symbol_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

Parameters
typetype of the function call
loclocation in the program_invocation_name
function_idfunction the generated code will be used in
symbol_tablesymbol table
Returns
Code implementing the Java String.format function. Since the exact class of the arguments is not known, we give as argument to the internal format function a structure containing the different possible types.

Definition at line 1444 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 
)
private

Generates code for the String.length method.

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

Definition at line 1742 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_name,
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_namename of the function to be called
typetype of the function
loclocation in the source
symbol_tablesymbol table
Returns
Code corresponding to:
string_expr = function_name(args)
string = new String
string = string_expr_to_string(string)
return string

Definition at line 1614 of file java_string_library_preprocess.cpp.

◆ process_equals_function_operands()

exprt::operandst java_string_library_preprocesst::process_equals_function_operands ( const exprt::operandst operands,
const source_locationt loc,
symbol_table_baset symbol_table,
code_blockt init_code 
)
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.

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

Definition at line 356 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,
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 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.

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

Definition at line 326 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,
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
symbol_tablesymbol table
init_codecode block, in which declaration of some arguments may be added
Returns
a list of expressions

Definition at line 271 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,
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
symbol_tablesymbol table
codecode block, in which some assignments will be added
Returns
a string expression

Definition at line 446 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 54 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_name,
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_name.

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

Parameters
function_namethe 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_name>(str.length, str.data, arguments)
Returns
refined string expression str

Definition at line 780 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 938 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,
symbol_tablet symbol_table,
code_blockt init_code 
)
friend

Member Data Documentation

◆ char_type

const typet java_string_library_preprocesst::char_type
private

Definition at line 97 of file java_string_library_preprocess.h.

◆ character_preprocess

character_refine_preprocesst java_string_library_preprocesst::character_preprocess
private

Definition at line 95 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 111 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 127 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 132 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 123 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 115 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 119 of file java_string_library_preprocess.h.

◆ id_maps

◆ index_type

const typet java_string_library_preprocesst::index_type
private

Definition at line 98 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 99 of file java_string_library_preprocess.h.

◆ string_types

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

Definition at line 146 of file java_string_library_preprocess.h.


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