cprover
java_string_library_preprocess.cpp File Reference

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

Include dependency graph for java_string_library_preprocess.cpp:

Go to the source code of this file.

Functions

irep_idt get_tag (const typet &type)
 
typet string_data_type (const symbol_tablet &symbol_table)
 
typet string_length_type ()
 
static typet get_data_type (const typet &type, const symbol_tablet &symbol_table)
 Finds the type of the data component. More...
 
static typet get_length_type (const typet &type, const symbol_tablet &symbol_table)
 Finds the type of the length component. More...
 
static exprt get_length (const exprt &expr, const symbol_tablet &symbol_table)
 access length member More...
 
static exprt get_data (const exprt &expr, const symbol_tablet &symbol_table)
 access data member More...
 
static codet code_assign_function_application (const exprt &lhs, const irep_idt &function_name, 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, 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, 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_set, symbol_table_baset &symbol_table, const source_locationt &loc, 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,
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
arrayinfinite size character array expression
lengthinteger expression
symbol_tablethe symbol table
locsource location
code[out] : code block to which declaration and calls get added

Definition at line 718 of file java_string_library_preprocess.cpp.

References code_blockt::add(), code_assign_function_application(), get_fresh_aux_symbol(), java_int_type(), loc, and symbolt::symbol_expr().

Referenced by initialize_nondet_string_fields(), and java_string_library_preprocesst::make_nondet_string_expr().

◆ add_character_set_constraint()

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

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

Parameters
pointera character pointer expression
lengthlength of the character sequence pointed by pointer
char_setcharacter 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_tablethe symbol table
locsource location
code[out] : code block to which declaration and calls get added

Definition at line 753 of file java_string_library_preprocess.cpp.

References code_blockt::add(), code_assign_function_application(), get_fresh_aux_symbol(), irept::id(), java_int_type(), loc, PRECONDITION, and exprt::type().

Referenced by initialize_nondet_string_fields().

◆ add_keys_to_container()

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

◆ 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,
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
pointera character pointer expression
arraya character array expression
symbol_tablethe symbol table
locsource location
code[out] : code block to which declaration and calls get added

Definition at line 684 of file java_string_library_preprocess.cpp.

References code_blockt::add(), code_assign_function_application(), get_fresh_aux_symbol(), irept::id(), java_int_type(), loc, PRECONDITION, and exprt::type().

Referenced by initialize_nondet_string_fields(), java_string_library_preprocesst::make_nondet_string_expr(), and java_string_library_preprocesst::replace_char_array().

◆ code_assign_function_application()

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

assign the result of a function call

Parameters
lhsan expression
function_namethe name of the function
argumentsa list of arguments
symbol_tablea symbol table
Returns
the following code:
lhs = <function_name>(arguments)

Definition at line 618 of file java_string_library_preprocess.cpp.

References make_function_application(), and exprt::type().

Referenced by add_array_to_length_association(), add_character_set_constraint(), add_pointer_to_array_association(), and java_string_library_preprocesst::string_expr_of_function().

◆ get_data()

static exprt get_data ( const exprt expr,
const symbol_tablet symbol_table 
)
static

access data member

Parameters
expran expression of structured type with data component
symbol_tablesymbol table
Returns
expression representing the "data" member

Definition at line 442 of file java_string_library_preprocess.cpp.

References get_data_type(), and exprt::type().

Referenced by java_string_library_preprocesst::code_assign_java_string_to_string_expr(), and java_string_library_preprocesst::replace_char_array().

◆ get_data_type()

static typet get_data_type ( const typet type,
const symbol_tablet symbol_table 
)
static

Finds the type of the data component.

Parameters
typea type containing a "data" component
symbol_tablesymbol table
Returns
type of the "data" component

Definition at line 395 of file java_string_library_preprocess.cpp.

References CHECK_RETURN, struct_union_typet::component_type(), irept::id(), symbol_table_baset::lookup(), PRECONDITION, to_struct_type(), to_symbol_type(), and symbolt::type.

Referenced by get_data().

◆ get_length()

static exprt get_length ( const exprt expr,
const symbol_tablet symbol_table 
)
static

access length member

Parameters
expran expression of structured type with length component
symbol_tablesymbol table
Returns
expression representing the "length" member

Definition at line 432 of file java_string_library_preprocess.cpp.

References get_length_type(), and exprt::type().

Referenced by java_string_library_preprocesst::code_assign_java_string_to_string_expr(), java_string_library_preprocesst::make_string_length_code(), and java_string_library_preprocesst::replace_char_array().

◆ get_length_type()

static typet get_length_type ( const typet type,
const symbol_tablet symbol_table 
)
static

Finds the type of the length component.

Parameters
typea type containing a "length" component
symbol_tablesymbol table
Returns
type of the "length" component

Definition at line 414 of file java_string_library_preprocess.cpp.

References CHECK_RETURN, struct_union_typet::component_type(), irept::id(), symbol_table_baset::lookup(), PRECONDITION, to_struct_type(), to_symbol_type(), and symbolt::type.

Referenced by get_length().

◆ get_tag()

◆ 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_tablethe symbol table
locsource location
function_idname of the function containing the array
code[out] : code block where the declaration gets added
Returns
created symbol expression

Definition at line 655 of file java_string_library_preprocess.cpp.

References code_blockt::add(), get_fresh_aux_symbol(), id2string(), java_char_type(), java_int_type(), loc, symbolt::symbol_expr(), and exprt::type().

Referenced by initialize_nondet_string_fields(), and java_string_library_preprocesst::make_nondet_string_expr().

◆ string_data_type()

typet string_data_type ( const symbol_tablet symbol_table)
Parameters
symbol_tablea symbol_table containing an entry for java Strings
Returns
the type of data fields in java Strings.

Definition at line 173 of file java_string_library_preprocess.cpp.

References struct_union_typet::component_number(), struct_union_typet::components(), symbol_table_baset::lookup(), to_struct_type(), and symbolt::type.

◆ string_length_type()

typet string_length_type ( )
Returns
the type of the length field in java Strings.

Definition at line 184 of file java_string_library_preprocess.cpp.

References java_int_type().

Referenced by java_string_library_preprocesst::add_string_type().