cprover
|
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/class_identifier.h>
#include <ansi-c/allocate_objects.h>
#include "java_types.h"
#include "java_utils.h"
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. | |
static const typet & | get_length_type (const typet &type, const symbol_table_baset &symbol_table) |
Finds the type of the length component. | |
static exprt | get_length (const exprt &expr, const symbol_table_baset &symbol_table) |
access length member | |
static exprt | get_data (const exprt &expr, const symbol_table_baset &symbol_table) |
access data member | |
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 | |
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. | |
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 . | |
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 . | |
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. | |
copy_constructor_body | add (code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table, true), loc) |
template<typename TMap , typename TContainer > | |
void | add_keys_to_container (const TMap &map, TContainer &container) |
Variables | |
const symbol_exprt | arg_this {params[0].get_identifier(), params[0].type()} |
Create a refined_string_exprt str whose content and length are fresh symbols, calls the string primitive with name function_id . | |
return | copy_constructor_body |
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.
copy_constructor_body add | ( | code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table, true) | , |
loc | ) |
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
.
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 678 of file java_string_library_preprocess.cpp.
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.
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 710 of file java_string_library_preprocess.cpp.
void add_keys_to_container | ( | const TMap & | map, |
TContainer & | container ) |
Definition at line 1432 of file java_string_library_preprocess.cpp.
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
.
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 647 of file java_string_library_preprocess.cpp.
|
static |
assign the result of a function call
lhs | an expression |
function_id | the name of the function |
arguments | a list of arguments |
symbol_table | a symbol table |
Definition at line 578 of file java_string_library_preprocess.cpp.
|
static |
access data member
expr | an expression of structured type with data component |
symbol_table | symbol table |
Definition at line 418 of file java_string_library_preprocess.cpp.
|
static |
Finds the type of the data component.
type | a type containing a "data" component |
symbol_table | symbol table |
Definition at line 368 of file java_string_library_preprocess.cpp.
|
static |
access length member
expr | an expression of structured type with length component |
symbol_table | symbol table |
Definition at line 408 of file java_string_library_preprocess.cpp.
|
static |
Finds the type of the length component.
type | a type containing a "length" component |
symbol_table | symbol table |
Definition at line 388 of file java_string_library_preprocess.cpp.
Definition at line 41 of file java_string_library_preprocess.cpp.
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.
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 |
Definition at line 615 of file java_string_library_preprocess.cpp.
|
static |
Definition at line 177 of file java_string_library_preprocess.cpp.
const symbol_exprt arg_this {params[0].get_identifier(), params[0].type()} |
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. / \param function_id: the name of the function / \param arguments: arguments of the function / \param loc: source location / \param symbol_table: symbol table / \param [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) / ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ / \return refined string expression
str` 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) { int return_code; const symbolt return_code_sym = fresh_java_symbol( java_int_type(), std::string("return_code_") + function_id.c_str(), loc, function_id, symbol_table); const auto return_code = return_code_sym.symbol_expr(); code.add(code_declt(return_code), loc);
const refined_string_exprt string_expr = make_nondet_string_expr(loc, function_id, symbol_table, code);
args is { str.length, str.content, arguments... } exprt::operandst args; args.push_back(string_expr.length()); args.push_back(string_expr.content()); args.insert(args.end(), arguments.begin(), arguments.end());
return_code = <function_id>_data(args) code.add( code_assign_function_application( return_code, function_id, args, symbol_table), loc);
return string_expr; }
/ Produce code for an assignment of a string expr to a Java string. /
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. / |
if(is_constructor) { Initialise the supertype with the appropriate classid: namespacet ns(symbol_table); const struct_typet &lhs_type = ns.follow_tag(to_struct_tag_type(deref.type())); auto zero_base_object = *zero_initializer( lhs_type.components().front().type(), source_locationt{}, ns); set_class_identifier( to_struct_expr(zero_base_object), ns, to_struct_tag_type(deref.type())); struct_exprt struct_rhs( {zero_base_object, rhs_length, rhs_array}, deref.type()); return code_assignt(checked_dereference(lhs), struct_rhs); } else { return code_blockt( {code_assignt(get_length(deref, symbol_table), rhs_length), code_assignt(get_data(deref, symbol_table), rhs_array)}); } }
/ Produce code for an assignemnt of a string expr to a Java string. /
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. / |
/
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 / ~~~~~~~~~~~~~~~~~~~~~~ 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) { PRECONDITION(implements_java_char_sequence_pointer(rhs.type())); |
const dereference_exprt deref = checked_dereference(rhs);
Although we should not reach this code if rhs is null, the association pointer -> length
is added to the solver anyway, so we have to make sure the length is set to something reasonable. auto rhs_length = if_exprt( equal_exprt(rhs, null_pointer_exprt(to_pointer_type(rhs.type()))), from_integer(0, lhs.length().type()), get_length(deref, symbol_table)); rhs_length.set(ID_mode, ID_java);
Assignments code.add(code_assignt(lhs.length(), rhs_length), loc); exprt data_as_array = get_data(deref, symbol_table); code.add(code_assignt{lhs.content(), std::move(data_as_array)}, loc); }
/ Create a string expression whose value is given by a literal /
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) / ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ / |
/ Provide code for the String.valueOf(F) function. /
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 / |
Getting the argument java_method_typet::parameterst params = type.parameters(); PRECONDITION(params.size()==1); PRECONDITION(!params[0].get_identifier().empty()); const symbol_exprt arg(params[0].get_identifier(), params[0].type());
Holder for output code code_blockt code;
Declaring and allocating String * str const exprt str = allocate_fresh_string( type.return_type(), loc, function_id, symbol_table, code);
Expression representing 0.0 const ieee_float_spect float_spec{to_floatbv_type(params[0].type())}; ieee_floatt zero_float(float_spec); zero_float.from_float(0.0); const constant_exprt zero = zero_float.to_expr();
For each possible case with have a condition and a string_exprt std::vector<exprt> condition_list; std::vector<refined_string_exprt> string_expr_list;
Case of computerized scientific notation condition_list.push_back(binary_relation_exprt(arg, ID_ge, zero)); const refined_string_exprt sci_notation = string_expr_of_function( ID_cprover_string_of_float_scientific_notation_func, {arg}, loc, symbol_table, code); string_expr_list.push_back(sci_notation);
Subcase of negative scientific notation condition_list.push_back(binary_relation_exprt(arg, ID_lt, zero)); const refined_string_exprt minus_sign = string_literal_to_string_expr("-", loc, symbol_table, code); const refined_string_exprt neg_sci_notation = string_expr_of_function( ID_cprover_string_concat_func, {minus_sign, sci_notation}, loc, symbol_table, code); string_expr_list.push_back(neg_sci_notation);
Case of NaN condition_list.push_back(isnan_exprt(arg)); const refined_string_exprt nan = string_literal_to_string_expr("NaN", loc, symbol_table, code); string_expr_list.push_back(nan);
Case of Infinity extractbit_exprt is_neg(arg, float_spec.width()-1); condition_list.push_back(and_exprt(isinf_exprt(arg), not_exprt(is_neg))); const refined_string_exprt infinity = string_literal_to_string_expr("Infinity", loc, symbol_table, code); string_expr_list.push_back(infinity);
Case -Infinity condition_list.push_back(and_exprt(isinf_exprt(arg), is_neg)); const refined_string_exprt minus_infinity = string_literal_to_string_expr("-Infinity", loc, symbol_table, code); string_expr_list.push_back(minus_infinity);
Case of 0.0 Note: for zeros we must use equal_exprt and not ieee_float_equal_exprt, the latter disregards the sign condition_list.push_back(equal_exprt(arg, zero)); const refined_string_exprt zero_string = string_literal_to_string_expr("0.0", loc, symbol_table, code); string_expr_list.push_back(zero_string);
Case of -0.0 ieee_floatt minus_zero_float(float_spec); minus_zero_float.from_float(-0.0f); condition_list.push_back(equal_exprt(arg, minus_zero_float.to_expr())); const refined_string_exprt minus_zero_string = string_literal_to_string_expr("-0.0", loc, symbol_table, code); string_expr_list.push_back(minus_zero_string);
Case of simple notation ieee_floatt bound_inf_float(float_spec); ieee_floatt bound_sup_float(float_spec); bound_inf_float.from_float(1e-3f); bound_sup_float.from_float(1e7f); bound_inf_float.change_spec(float_spec); bound_sup_float.change_spec(float_spec); const constant_exprt bound_inf = bound_inf_float.to_expr(); const constant_exprt bound_sup = bound_sup_float.to_expr();
const and_exprt is_simple_float{binary_relation_exprt(arg, ID_ge, bound_inf), binary_relation_exprt(arg, ID_lt, bound_sup)}; condition_list.push_back(is_simple_float);
const refined_string_exprt simple_notation = string_expr_of_function( ID_cprover_string_of_float_func, {arg}, loc, symbol_table, code); string_expr_list.push_back(simple_notation);
Case of a negative number in simple notation const and_exprt is_neg_simple_float{ binary_relation_exprt(arg, ID_le, unary_minus_exprt(bound_inf)), binary_relation_exprt(arg, ID_gt, unary_minus_exprt(bound_sup))}; condition_list.push_back(is_neg_simple_float);
const refined_string_exprt neg_simple_notation = string_expr_of_function( ID_cprover_string_concat_func, {minus_sign, simple_notation}, loc, symbol_table, code); string_expr_list.push_back(neg_simple_notation);
Combining all cases INVARIANT( string_expr_list.size()==condition_list.size(), "number of created strings should correspond to number of conditions");
We do not check the condition of the first element in the list as it will be reached only if all other conditions are not satisfied. codet tmp_code = code_assign_string_expr_to_java_string( str, string_expr_list[0], symbol_table, true); for(std::size_t i=1; i<condition_list.size(); i++) { tmp_code = code_ifthenelset( condition_list[i], code_assign_string_expr_to_java_string( str, string_expr_list[i], symbol_table, true), tmp_code); } code.add(tmp_code, loc);
Return str code.add(code_returnt(str), loc); return code; }
/ Generate the goto code for string initialization. /
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. / |
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}; / 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) { java_method_typet::parameterst params = type.parameters();The first parameter is the object to be initialized PRECONDITION(!params.empty()); PRECONDITION(!params[0].get_identifier().empty()); const symbol_exprt arg_this(params[0].get_identifier(), params[0].type()); if(is_constructor) params.erase(params.begin());
Holder for output code code_blockt code;
Processing parameters const exprt::operandst args = process_parameters(params, loc, function_id, symbol_table, code);
string_expr <- function(arg1) const refined_string_exprt string_expr = string_expr_of_function(function_id, args, loc, symbol_table, code);
arg_this <- string_expr code.add( code_assign_string_expr_to_java_string( arg_this, string_expr, symbol_table, is_constructor), loc);
return code; }
/ Call a cprover internal function, assign the result to object this
and / return it. /
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 / |
this
const java_method_typet::parameterst ¶ms = type.parameters(); PRECONDITION(!params.empty()); PRECONDITION(!params[0].get_identifier().empty()); code_blockt code; code.add(
make_assign_function_from_call(function_id, type, loc, symbol_table), loc); const symbol_exprt arg_this(params[0].get_identifier(), params[0].type()); code.add(code_returnt(arg_this), loc); return code; }/ Call a cprover internal function and assign the result to object this
. /
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 / |
/ Used to provide our own implementation of the CProver.classIdentifier() / function. /
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 / |
Code to be returned code_blockt code;
class_identifier is obj->@class_identifier const member_exprt class_identifier{ checked_dereference(obj), JAVA_CLASS_IDENTIFIER_FIELD_NAME, string_typet()};
string_expr = cprover_string_literal(this->@class_identifier) const refined_string_exprt string_expr = string_expr_of_function( ID_cprover_string_literal_func, {class_identifier}, loc, symbol_table, code);
string_expr1 = substr(string_expr, 6) We do this to remove the "java::" prefix const refined_string_exprt string_expr1 = string_expr_of_function( ID_cprover_string_substring_func, {string_expr, from_integer(6, java_int_type())}, loc, symbol_table, code);
string1 = (String*) string_expr const typet &string_ptr_type = type.return_type(); const exprt string1 = allocate_fresh_string( string_ptr_type, loc, function_id, symbol_table, code); code.add( code_assign_string_expr_to_java_string( string1, string_expr1, symbol_table, true), loc);
return string1; code.add(code_returnt{string1}, loc); return code; }
/ Provide code for a function that calls a function from the solver and simply / returns it. /
function_id | name of the function to be called / |
type | type of the function / |
loc | location in the source / |
symbol_table | symbol table / |
/ Provide code for a function that calls a function from the solver and return / the string_expr result as a Java string. /
function_id | name of the function to be called / |
type | type of the function / |
loc | location in the source / |
symbol_table | symbol table / |
Calling the function const exprt::operandst arguments = process_parameters(type.parameters(), loc, function_id, symbol_table, code);
String expression that will hold the result const refined_string_exprt string_expr = string_expr_of_function(function_id, arguments, loc, symbol_table, code);
Assign to string const exprt str = allocate_fresh_string( type.return_type(), loc, function_id, symbol_table, code); code.add( code_assign_string_expr_to_java_string( str, string_expr, symbol_table, true), loc);
Return value code.add(code_returnt(str), loc); return code; }
/ Generates code for a function which copies a string object to a new string / object. /
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 / |
Code for the output code_blockt code;
String expression that will hold the result const refined_string_exprt string_expr = decl_string_expr(loc, function_id, symbol_table, code);
Assign the argument to string_expr const java_method_typet::parametert &op = type.parameters()[0]; PRECONDITION(!op.get_identifier().empty()); const symbol_exprt arg0{op.get_identifier(), op.type()}; code_assign_java_string_to_string_expr( string_expr, arg0, loc, symbol_table, code);
Allocate and assign the string const exprt str = allocate_fresh_string( type.return_type(), loc, function_id, symbol_table, code); code.add( code_assign_string_expr_to_java_string( str, string_expr, symbol_table, true), loc);
Return value code.add(code_returnt(str), loc); return code; }
/ Generates code for a constructor of a string object from another string / object. /
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 / |
code_blockt copy_constructor_body;
String expression that will hold the result const refined_string_exprt string_expr = decl_string_expr(loc, function_id, symbol_table, copy_constructor_body);
Assign argument to a string_expr const java_method_typet::parameterst ¶ms = type.parameters(); PRECONDITION(!params[0].get_identifier().empty()); PRECONDITION(!params[1].get_identifier().empty()); const symbol_exprt arg1{params[1].get_identifier(), params[1].type()}; code_assign_java_string_to_string_expr( string_expr, arg1, loc, symbol_table, copy_constructor_body);
Assign string_expr to this
object
Definition at line 1379 of file java_string_library_preprocess.cpp.
return copy_constructor_body |
Definition at line 1385 of file java_string_library_preprocess.cpp.