#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_idt >	get_string_type_base_classes (const irep_idt &class_name)
	Gets the base classes for known String and String-related types, or returns an empty list for other types. More...

void	add_string_type (const irep_idt &class_name, symbol_tablet &symbol_table)
	Add to the symbol table type declaration for a String-like Java class. More...

bool	is_known_string_type (irep_idt class_name)
	Check whether a class name is known as a string type. More...

Public Member Functions inherited from messaget
virtual void	set_message_handler (message_handlert &_message_handler)

message_handlert &	get_message_handler ()

	messaget ()

	messaget (const messaget &other)

messaget &	operator= (const messaget &other)

	messaget (message_handlert &_message_handler)

virtual	~messaget ()

mstreamt &	get_mstream (unsigned message_level) const

mstreamt &	error () const

mstreamt &	warning () const

mstreamt &	result () const

mstreamt &	status () const

mstreamt &	statistics () const

mstreamt &	progress () const

mstreamt &	debug () 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_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)
	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_exprt >	get_primitive_value_of_object (const exprt &object, irep_idt type_name, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
	Adds to the code an assignment of the form. 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_functiont >	conversion_table

id_mapt	cprover_equivalent_to_java_function

id_mapt	cprover_equivalent_to_java_string_returning_function

id_mapt	cprover_equivalent_to_java_constructor

id_mapt	cprover_equivalent_to_java_assign_and_return_function

id_mapt	cprover_equivalent_to_java_assign_function

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

std::unordered_set< irep_idt >	string_types

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

Additional Inherited Members
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_handlert *	message_handler

mstreamt	mstream

Detailed Description

Definition at line 35 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 &)> java_string_library_preprocesst::conversion_functiont

private

Definition at line 106 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 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_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 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

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

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

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

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

symbol	symbol of the function to provide code for
symbol_table	a 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_name	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_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_process	an expression of a type which implements char sequence
loc	location in the source
symbol_table	symbol table
init_code	code block, in which declaration will be added: char *cprover_string_content; int cprover_string_length; cprover_string_length = a->length; cprover_string_content = a->data;

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

loc	source location
symbol_table	the 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

type	an array type
location	a location in the program
symbol_table	symbol 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

type	a type for refined strings
loc	a location in the program
symbol_table	symbol 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

argv	reference to an array of references
index	index 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

object	an expression representing a reference to an object
type_name	name of the corresponding primitive type, this can be one of the following: ID_boolean, ID_char, ID_byte, ID_short, ID_int, ID_long, ID_float, ID_double, ID_void
loc	a location in the source
symbol_table	the symbol table
code	code block to which we are adding some assignments

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

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

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

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

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

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

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

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

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

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

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

argv	reference to an array of references
index	index of the desired argument
structured_type	type for arguments of the internal format function
loc	a location in the source
function_id	function the generated expression will be used in
symbol_table	the symbol table
code	code 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_name	name of the function to be called
type	the type of the function call
loc	location in program
symbol_table	the symbol table to populate

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_name	name of the function to be called
type	the type of the function call
loc	location in program
symbol_table	the symbol table to populate

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

type	type of the function
loc	location in the source
function_id	unused
symbol_table	symbol 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

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

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

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_name	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_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_name	name of the function to be called
type	the type of the function call
loc	location in program
symbol_table	the symbol table to populate
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 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

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

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

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

type	type of the function call
loc	location in the program_invocation_name
function_id	function the generated code will be used in
symbol_table	symbol 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

type	type of the function
loc	location in the source
function_id	unused
symbol_table	symbol 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_name	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_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

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

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

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

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

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

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

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_name	the name of the function
	arguments	arguments of the function
	loc	source location
	symbol_table	symbol table
[out]	code	gets added the following code: int return_code; int str.length; char str.data[str.length] return_code = <function_name>(str.length, str.data, arguments)

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

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

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 134 of file java_string_library_preprocess.h.

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

/builddir/build/BUILD/cbmc-cbmc-5.11/jbmc/src/java_bytecode/java_string_library_preprocess.h
/builddir/build/BUILD/cbmc-cbmc-5.11/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

Additional Inherited Members

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_array()

◆ fresh_string()

◆ get_all_function_names()

◆ get_object_at_index()

◆ get_primitive_value_of_object()

◆ 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_argument_for_format()

◆ make_assign_and_return_function_from_call()

◆ make_assign_function_from_call()

◆ 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_object_get_class_code()

◆ make_string_format_code()

◆ make_string_length_code()

◆ make_string_returning_function_from_call()

◆ process_equals_function_operands()

◆ 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