Java_string_libraries_preprocess, gives code for methods on strings of the java standard library. More...

#include "java_string_library_preprocess.h"
#include <util/arith_tools.h>
#include <util/bitvector_expr.h>
#include <util/c_types.h>
#include <util/expr_initializer.h>
#include <util/floatbv_expr.h>
#include <util/ieee_float.h>
#include <util/refined_string_type.h>
#include <util/std_code.h>
#include <util/string_expr.h>
#include <util/symbol_table_base.h>
#include <goto-programs/allocate_objects.h>
#include <goto-programs/class_identifier.h>
#include "java_types.h"
#include "java_utils.h"

Include dependency graph for java_string_library_preprocess.cpp:

Go to the source code of this file.

Functions
static irep_idt	get_tag (const typet &type)

static typet	string_length_type ()

static const typet &	get_data_type (const typet &type, const symbol_table_baset &symbol_table)
	Finds the type of the data component. More...

static const typet &	get_length_type (const typet &type, const symbol_table_baset &symbol_table)
	Finds the type of the length component. More...

static exprt	get_length (const exprt &expr, const symbol_table_baset &symbol_table)
	access length member More...

static exprt	get_data (const exprt &expr, const symbol_table_baset &symbol_table)
	access data member More...

static codet	code_assign_function_application (const exprt &lhs, const irep_idt &function_id, const exprt::operandst &arguments, symbol_table_baset &symbol_table)
	assign the result of a function call More...

exprt	make_nondet_infinite_char_array (symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
	Declare a fresh symbol of type array of character with infinite size. More...

void	add_pointer_to_array_association (const exprt &pointer, const exprt &array, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
	Add a call to a primitive of the string solver, letting it know that `pointer` points to the first character of `array`. More...

void	add_array_to_length_association (const exprt &array, const exprt &length, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
	Add a call to a primitive of the string solver, letting it know that the actual length of `array` is `length`. More...

void	add_character_set_constraint (const exprt &pointer, const exprt &length, const irep_idt &char_range, symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
	Add a call to a primitive of the string solver which ensures all characters belong to the character set. More...

template<typename TMap , typename TContainer >
void	add_keys_to_container (const TMap &map, TContainer &container)

Detailed Description

Java_string_libraries_preprocess, gives code for methods on strings of the java standard library.

In particular methods from java.lang.String, java.lang.StringBuilder, java.lang.StringBuffer.

Definition in file java_string_library_preprocess.cpp.

Function Documentation

◆ add_array_to_length_association()

void add_array_to_length_association	(	const exprt &	array,
		const exprt &	length,
		symbol_table_baset &	symbol_table,
		const source_locationt &	loc,
		const irep_idt &	function_id,
		code_blockt &	code
	)

Add a call to a primitive of the string solver, letting it know that the actual length of array is length.

Parameters

	array	infinite size character array expression
	length	integer expression
	symbol_table	the symbol table
	loc	source location
	function_id	name of the function in which the code will be added
[out]	code	code block to which declaration and calls get added

Definition at line 677 of file java_string_library_preprocess.cpp.

◆ add_character_set_constraint()

void add_character_set_constraint	(	const exprt &	pointer,
		const exprt &	length,
		const irep_idt &	char_range,
		symbol_table_baset &	symbol_table,
		const source_locationt &	loc,
		const irep_idt &	function_id,
		code_blockt &	code
	)

Add a call to a primitive of the string solver which ensures all characters belong to the character set.

Parameters

	pointer	a character pointer expression
	length	length of the character sequence pointed by `pointer`
	char_range	character set given by a range expression consisting of two characters separated by an hyphen. For instance "a-z" denotes all lower case ascii letters.
	symbol_table	the symbol table
	loc	source location
	function_id	the name of the function
[out]	code	code block to which declaration and calls get added

Definition at line 709 of file java_string_library_preprocess.cpp.

◆ add_keys_to_container()

template<typename TMap , typename TContainer >

void add_keys_to_container	(	const TMap &	map,
		TContainer &	container
	)

Definition at line 1430 of file java_string_library_preprocess.cpp.

◆ add_pointer_to_array_association()

void add_pointer_to_array_association	(	const exprt &	pointer,
		const exprt &	array,
		symbol_table_baset &	symbol_table,
		const source_locationt &	loc,
		const irep_idt &	function_id,
		code_blockt &	code
	)

Add a call to a primitive of the string solver, letting it know that pointer points to the first character of array.

Parameters

	pointer	a character pointer expression
	array	a character array expression
	symbol_table	the symbol table
	loc	source location
	function_id	name of the function in which the code will be added
[out]	code	code block to which declaration and calls get added

Definition at line 646 of file java_string_library_preprocess.cpp.

◆ code_assign_function_application()

static codet code_assign_function_application	(	const exprt &	lhs,
		const irep_idt &	function_id,
		const exprt::operandst &	arguments,
		symbol_table_baset &	symbol_table
	)

static

assign the result of a function call

Parameters

lhs	an expression
function_id	the name of the function
arguments	a list of arguments
symbol_table	a symbol table

Returns: the following code:
lhs = <function_id>(arguments)

Definition at line 577 of file java_string_library_preprocess.cpp.

◆ get_data()

static exprt get_data	(	const exprt &	expr,
		const symbol_table_baset &	symbol_table
	)

static

access data member

Parameters

expr	an expression of structured type with data component
symbol_table	symbol table

Returns: expression representing the "data" member

Definition at line 417 of file java_string_library_preprocess.cpp.

◆ get_data_type()

static const typet& get_data_type	(	const typet &	type,
		const symbol_table_baset &	symbol_table
	)

static

Finds the type of the data component.

Parameters

type	a type containing a "data" component
symbol_table	symbol table

Returns: type of the "data" component

Definition at line 367 of file java_string_library_preprocess.cpp.

◆ get_length()

static exprt get_length	(	const exprt &	expr,
		const symbol_table_baset &	symbol_table
	)

static

access length member

Parameters

expr	an expression of structured type with length component
symbol_table	symbol table

Returns: expression representing the "length" member

Definition at line 407 of file java_string_library_preprocess.cpp.

◆ get_length_type()

static const typet& get_length_type	(	const typet &	type,
		const symbol_table_baset &	symbol_table
	)

static

Finds the type of the length component.

Parameters

type	a type containing a "length" component
symbol_table	symbol table

Returns: type of the "length" component

Definition at line 387 of file java_string_library_preprocess.cpp.

◆ get_tag()

static irep_idt get_tag ( const typet & type )

static

Returns: tag of a struct prefixed by "java::" or symbolic tag empty string if not symbol or struct

Definition at line 40 of file java_string_library_preprocess.cpp.

◆ make_nondet_infinite_char_array()

exprt make_nondet_infinite_char_array	(	symbol_table_baset &	symbol_table,
		const source_locationt &	loc,
		const irep_idt &	function_id,
		code_blockt &	code
	)

Declare a fresh symbol of type array of character with infinite size.

Parameters

	symbol_table	the symbol table
	loc	source location
	function_id	name of the function containing the array
[out]	code	code block where the declaration gets added

Returns: created symbol expression

Definition at line 614 of file java_string_library_preprocess.cpp.

◆ string_length_type()

static typet string_length_type ( )

static

Returns: the type of the length field in java Strings.

Definition at line 176 of file java_string_library_preprocess.cpp.

Functions

Detailed Description

Function Documentation

◆ add_array_to_length_association()

◆ add_character_set_constraint()

◆ add_keys_to_container()

◆ add_pointer_to_array_association()

◆ code_assign_function_application()

◆ get_data()

◆ get_data_type()

◆ get_length()

◆ get_length_type()

◆ get_tag()

◆ make_nondet_infinite_char_array()

◆ string_length_type()