#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_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_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_idt >	id_mapt

Private Member Functions
	java_string_library_preprocesst (const java_string_library_preprocesst &)=delete

code_blockt	make_float_to_string_code (const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, message_handlert &message_handler)
	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_functiont >	conversion_table

id_mapt	cprover_equivalent_to_java_function

id_mapt	cprover_equivalent_to_java_string_returning_function

id_mapt	cprover_equivalent_to_java_constructor

id_mapt	cprover_equivalent_to_java_assign_and_return_function

id_mapt	cprover_equivalent_to_java_assign_function

const std::array< id_mapt *, 5 >	id_maps

std::unordered_set< irep_idt >	string_types

Friends
refined_string_exprt	convert_exprt_to_string_exprt_unit_test (java_string_library_preprocesst &preprocess, const exprt &deref, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &init_code)

Detailed Description

Definition at line 37 of file java_string_library_preprocess.h.

Member Typedef Documentation

◆ conversion_functiont

typedef std::function<codet( const java_method_typet &, const source_locationt &, const irep_idt &, symbol_table_baset &, message_handlert &)> java_string_library_preprocesst::conversion_functiont

private

Definition at line 112 of file java_string_library_preprocess.h.

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

◆ 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

type	a type for string
loc	a location in the program
function_id	function the fresh string is created in
symbol_table	symbol table
code	code block to which allocation instruction will be added

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

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
is_constructor	the 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

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

lhs	an expression representing a java string
rhs	a string expression
symbol_table	symbol table
is_constructor	the 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

symbol	symbol of the function to provide code for
symbol_table	a symbol table
message_handler	a 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_id	the name of the function
arguments	a list of arguments
type	the return type
symbol_table	a 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_process	an expression of a type which implements char sequence
loc	location in the source
symbol_table	symbol table
function_id	name of the function in which the code will be added
init_code	code block, in which declaration will be added: 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

	loc	source location
	function_id	name of the function in which the string is defined
	symbol_table	the symbol table
[out]	code	code block to which the declaration is added

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

type	a type for refined strings
loc	a location in the program
function_id	name of the function in which the code will be added
symbol_table	symbol table

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_name class 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

type a 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

type a 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

type a 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

type a 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

type a 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

type a 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

type a 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

type a 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

type a 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_name name 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

type	a type
tag	a 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_id	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

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_id	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

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

type	type of the function called
loc	location in the source
function_id	function the generated code will be added to
symbol_table	the symbol table
message_handler	a 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

type	type of the function
loc	location in the source
function_id	name of the function (used for variable naming) where the generated code ends up.
symbol_table	symbol table
message_handler	a 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

type	type of the function
loc	location in the source
function_id	function the generated code will be added to
symbol_table	symbol table
message_handler	a 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

type	type of the function call
loc	location in the program_invocation_name
function_id	function the generated code will be added to
symbol_table	symbol table
message_handler	a 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_id	name of the function to be called
type	type of the function
loc	location in the source
symbol_table	symbol 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_id	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
is_constructor	the 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

loc	a location in the program
function_id	name of the function containing the string
symbol_table	symbol table
code	code block to which allocation instruction will be added

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

type	type of the function
loc	location in the source
function_id	unused
symbol_table	symbol table
message_handler	a 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_id	name of the function to be called
type	type of the function
loc	location in the source
symbol_table	symbol 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

operands	a list of expressions
loc	location in the source
function_id	name of the function in which the code will be added
symbol_table	symbol table
init_code	code block, in which declaration of some arguments may be added

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

params	a list of function parameters
loc	location in the source
function_id	name of the function in which the code will be added
symbol_table	symbol table
init_code	code block, in which declaration of some arguments may be added

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_pointer	an expression of type char array pointer
loc	location in the source
function_id	name of the function in which the string is defined
symbol_table	symbol table
code	code block, in which some assignments will be added

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_id	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_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

	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)

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

const std::array<id_mapt *, 5> java_string_library_preprocesst::id_maps

private

Initial value:

= std::array<id_mapt *, 5>
    {
      {
        &cprover_equivalent_to_java_function,
        &cprover_equivalent_to_java_string_returning_function,
        &cprover_equivalent_to_java_constructor,
        &cprover_equivalent_to_java_assign_and_return_function,
        &cprover_equivalent_to_java_assign_function,
      }
    }

Definition at line 140 of file java_string_library_preprocess.h.

◆ 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:

/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_string_library_preprocess.h
/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Public Member Functions

Static Public Member Functions

Private Types

Private Member Functions

Static Private Member Functions

Private Attributes

Friends

Detailed Description

Member Typedef Documentation

◆ conversion_functiont

◆ id_mapt

Constructor & Destructor Documentation

◆ java_string_library_preprocesst() [1/2]

◆ java_string_library_preprocesst() [2/2]

Member Function Documentation

◆ add_string_type()

◆ allocate_fresh_string()

◆ code_assign_components_to_java_string()

◆ code_assign_java_string_to_string_expr()

◆ code_assign_string_expr_to_java_string()

◆ code_for_function()

◆ code_return_function_application()

◆ convert_exprt_to_string_exprt()

◆ decl_string_expr()

◆ fresh_string()

◆ get_all_function_names()

◆ get_string_type_base_classes()

◆ implements_function()

◆ implements_java_char_sequence()

◆ implements_java_char_sequence_pointer()

◆ initialize_conversion_table()

◆ initialize_known_type_table()

◆ is_java_char_array_pointer_type()

◆ is_java_char_array_type()

◆ is_java_char_sequence_pointer_type()

◆ is_java_char_sequence_type()

◆ is_java_string_buffer_pointer_type()

◆ is_java_string_buffer_type()

◆ is_java_string_builder_pointer_type()

◆ is_java_string_builder_type()

◆ is_java_string_pointer_type()

◆ is_java_string_type()

◆ is_known_string_type()

◆ java_type_matches_tag()

◆ make_assign_and_return_function_from_call()

◆ make_assign_function_from_call()

◆ make_class_identifier_code()

◆ make_copy_constructor_code()

◆ make_copy_string_code()

◆ make_float_to_string_code()

◆ make_function_from_call()

◆ make_init_function_from_call()

◆ make_nondet_string_expr()

◆ make_string_length_code()

◆ make_string_returning_function_from_call()

◆ process_operands()

◆ process_parameters()

◆ replace_char_array()

◆ replace_character_call()

◆ string_expr_of_function()

◆ string_literal_to_string_expr()

Friends And Related Function Documentation

◆ convert_exprt_to_string_exprt_unit_test

Member Data Documentation

◆ char_type

◆ 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

◆ id_maps

◆ index_type

◆ refined_string_type

◆ string_types