diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index aaf0aad6b90..b9230c6b4e6 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -20,7 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -905,14 +904,6 @@ bool cbmc_parse_optionst::process_goto_program( status() << "Partial Inlining" << eom; goto_partial_inline(goto_functions, ns, ui_message_handler); - - if(cmdline.isset("refine-strings")) - { - status() << "Preprocessing for string refinement" << eom; - string_refine_preprocesst( - symbol_table, goto_functions, ui_message_handler); - } - // remove returns, gcc vectors, complex remove_returns(symbol_table, goto_functions); remove_vector(symbol_table, goto_functions); diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 1a3583bff53..60bfc304801 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -58,7 +58,6 @@ SRC = basic_blocks.cpp \ slice_global_inits.cpp \ string_abstraction.cpp \ string_instrumentation.cpp \ - string_refine_preprocess.cpp \ system_library_symbols.cpp \ vcd_goto_trace.cpp \ wp.cpp \ diff --git a/src/goto-programs/string_refine_preprocess.cpp b/src/goto-programs/string_refine_preprocess.cpp deleted file mode 100644 index bbba1b8d49a..00000000000 --- a/src/goto-programs/string_refine_preprocess.cpp +++ /dev/null @@ -1,1583 +0,0 @@ -/*******************************************************************\ - -Module: Preprocess a goto-programs so that calls to the java String - library are recognized by the string solver - -Author: Romain Brenguier - -Date: September 2016 - -\*******************************************************************/ - -#include -#include -#include -#include -#include -#include -#include -#include -#include - -#include "string_refine_preprocess.h" - -/*******************************************************************\ - -Function: string_refine_preprocesst::check_java_type - - Inputs: a type and a string - - Outputs: Boolean telling whether the type is a struct with the given - tag or a symbolic type with the tag prefixed by "java::" - -\*******************************************************************/ - -bool string_refine_preprocesst::check_java_type( - const typet &type, const std::string &tag) -{ - if(type.id()==ID_symbol) - { - irep_idt tag_id=to_symbol_type(type).get_identifier(); - return tag_id=="java::"+tag; - } - else if(type.id()==ID_struct) - { - irep_idt tag_id=to_struct_type(type).get_tag(); - return tag_id==tag; - } - return false; -} -/*******************************************************************\ - -Function: string_refine_preprocesst::is_java_string_pointer_type - - Inputs: a type - - Outputs: Boolean telling whether the type is that of java string pointers - -\*******************************************************************/ - -bool string_refine_preprocesst::is_java_string_pointer_type(const typet &type) -{ - if(type.id()==ID_pointer) - { - const pointer_typet &pt=to_pointer_type(type); - const typet &subtype=pt.subtype(); - return is_java_string_type(subtype); - } - return false; -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::is_java_string_type - - Inputs: a type - - Outputs: Boolean telling whether the type is that of java string - -\*******************************************************************/ - -bool string_refine_preprocesst::is_java_string_type(const typet &type) -{ - return check_java_type(type, "java.lang.String"); -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::is_java_string_builder_type - - Inputs: a type - - Outputs: Boolean telling whether the type is that of java string builder - -\*******************************************************************/ - -bool string_refine_preprocesst::is_java_string_builder_type(const typet &type) -{ - return check_java_type(type, "java.lang.StringBuilder"); -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::is_java_string_builder_pointer_type - - Inputs: a type - - Outputs: Boolean telling whether the type is that of java StringBuilder - pointers - -\*******************************************************************/ - -bool string_refine_preprocesst::is_java_string_builder_pointer_type( - const typet &type) -{ - if(type.id()==ID_pointer) - { - const pointer_typet &pt=to_pointer_type(type); - const typet &subtype=pt.subtype(); - return is_java_string_builder_type(subtype); - } - return false; -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::is_java_string_buffer_type - - Inputs: a type - - Outputs: Boolean telling whether the type is that of java string buffer - -\*******************************************************************/ - -bool string_refine_preprocesst::is_java_string_buffer_type(const typet &type) -{ - return check_java_type(type, "java.lang.StringBuffer"); -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::is_java_string_buffer_pointer_type - - Inputs: a type - - Outputs: Boolean telling whether the type is that of java StringBuffer - pointers - -\*******************************************************************/ - -bool string_refine_preprocesst::is_java_string_buffer_pointer_type( - const typet &type) -{ - if(type.id()==ID_pointer) - { - const pointer_typet &pt=to_pointer_type(type); - const typet &subtype=pt.subtype(); - return is_java_string_buffer_type(subtype); - } - return false; -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::is_java_char_sequence_type - - Inputs: a type - - Outputs: Boolean telling whether the type is that of java char sequence - -\*******************************************************************/ - -bool string_refine_preprocesst::is_java_char_sequence_type(const typet &type) -{ - return check_java_type(type, "java.lang.CharSequence"); -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::is_java_char_sequence_pointer_type - - Inputs: a type - - Outputs: Boolean telling whether the type is that of a pointer - to a java char sequence - -\*******************************************************************/ - -bool string_refine_preprocesst::is_java_char_sequence_pointer_type( - const typet &type) -{ - if(type.id()==ID_pointer) - { - const pointer_typet &pt=to_pointer_type(type); - const typet &subtype=pt.subtype(); - return is_java_char_sequence_type(subtype); - } - return false; -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::is_java_char_array_type - - Inputs: a type - - Outputs: Boolean telling whether the type is that of java char array - -\*******************************************************************/ - -bool string_refine_preprocesst::is_java_char_array_type(const typet &type) -{ - return check_java_type(type, "array[char]"); -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::is_java_char_array_pointer_type - - Inputs: a type - - Outputs: Boolean telling whether the type is that of a pointer - to a java char array - -\*******************************************************************/ - -bool string_refine_preprocesst::is_java_char_array_pointer_type( - const typet &type) -{ - if(type.id()==ID_pointer) - { - const pointer_typet &pt=to_pointer_type(type); - const typet &subtype=pt.subtype(); - return is_java_char_array_type(subtype); - } - return false; -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::fresh_array - - Inputs: - type - an array type - location - a location in the program - - Outputs: a new symbol - - Purpose: add a symbol with static lifetime and name containing - `cprover_string_array` and given type - -\*******************************************************************/ - -symbol_exprt string_refine_preprocesst::fresh_array( - const typet &type, const source_locationt &location) -{ - symbolt array_symbol=get_fresh_aux_symbol( - type, - "cprover_string_array", - "cprover_string_array", - location, - ID_java, - symbol_table); - array_symbol.is_static_lifetime=true; - return array_symbol.symbol_expr(); -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::fresh_string - - Inputs: - type - a type for refined strings - location - a location in the program - - Outputs: a new symbol - - Purpose: add a symbol with static lifetime and name containing - `cprover_string` and given type - -\*******************************************************************/ - -symbol_exprt string_refine_preprocesst::fresh_string( - const typet &type, const source_locationt &location) -{ - symbolt array_symbol=get_fresh_aux_symbol( - type, "cprover_string", "cprover_string", location, ID_java, symbol_table); - array_symbol.is_static_lifetime=true; - return array_symbol.symbol_expr(); -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::declare_function - - Inputs: a name and a type - - Purpose: declare a function with the given name and type - -\*******************************************************************/ - -void string_refine_preprocesst::declare_function( - irep_idt function_name, const typet &type) -{ - auxiliary_symbolt func_symbol; - func_symbol.base_name=function_name; - func_symbol.is_static_lifetime=false; - func_symbol.mode=ID_java; - func_symbol.name=function_name; - func_symbol.type=type; - symbol_table.add(func_symbol); - goto_functions.function_map[function_name]; -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::get_data_and_length_type_of_char_array - - Inputs: an expression, a reference to a data type and a reference to a - length type - - Purpose: assuming the expression is a char array, figure out what - the types for length and data are and put them into the references - given as argument - -\*******************************************************************/ - -void string_refine_preprocesst::get_data_and_length_type_of_char_array( - const exprt &expr, typet &data_type, typet &length_type) -{ - typet object_type=ns.follow(expr.type()); - assert(object_type.id()==ID_struct); - const struct_typet &struct_type=to_struct_type(object_type); - for(auto component : struct_type.components()) - if(component.get_name()=="length") - length_type=component.type(); - else if(component.get_name()=="data") - data_type=component.type(); -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::get_data_and_length_type_of_string - - Inputs: an expression, a reference to a data type and a reference to a - length type - - Purpose: assuming the expression is a java string, figure out what - the types for length and data are and put them into the references - given as argument - -\*******************************************************************/ - -void string_refine_preprocesst::get_data_and_length_type_of_string( - const exprt &expr, typet &data_type, typet &length_type) -{ - assert(implements_java_char_sequence(pointer_typet(expr.type()))); - typet object_type=ns.follow(expr.type()); - const struct_typet &struct_type=to_struct_type(object_type); - for(const auto &component : struct_type.components()) - if(component.get_name()=="length") - length_type=component.type(); - else if(component.get_name()=="data") - data_type=component.type(); -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::make_cprover_string_assign - - Inputs: a goto_program, a position in this program, an expression and a - location - - Outputs: an expression - - Purpose: Introduce a temporary variable for cprover strings; - returns the cprover_string corresponding to rhs if it is a string - pointer and the original rhs otherwise. - -\*******************************************************************/ - -exprt string_refine_preprocesst::make_cprover_string_assign( - goto_programt &goto_program, - goto_programt::targett &target, - const exprt &rhs, - const source_locationt &location) -{ - if(implements_java_char_sequence(rhs.type())) - { - // We do the following assignments: - // 1 length= *(rhs->length) - // 2 cprover_string_array = *(rhs->data) - // 3 cprover_string = { length; cprover_string_array } - - dereference_exprt deref(rhs, rhs.type().subtype()); - typet data_type, length_type; - get_data_and_length_type_of_string(deref, data_type, length_type); - std::list assignments; - - // 1) cprover_string_length= *(rhs->length) - symbolt sym_length=get_fresh_aux_symbol( - length_type, - "cprover_string_length", - "cprover_string_length", - location, - ID_java, - symbol_table); - symbol_exprt cprover_length=sym_length.symbol_expr(); - member_exprt length(deref, "length", length_type); - assignments.emplace_back(cprover_length, length); - - // 2) cprover_string_array = *(rhs->data) - symbol_exprt array_lhs=fresh_array(data_type.subtype(), location); - member_exprt data(deref, "data", data_type); - dereference_exprt deref_data(data, data_type.subtype()); - assignments.emplace_back(array_lhs, deref_data); - - // 3) cprover_string = { cprover_string_length; cprover_string_array } - // This assignment is useful for finding witnessing strings for counter - // examples - refined_string_typet ref_type(length_type, java_char_type()); - string_exprt new_rhs(cprover_length, array_lhs, ref_type); - - symbol_exprt lhs=fresh_string(new_rhs.type(), location); - assignments.emplace_back(lhs, new_rhs); - - insert_assignments( - goto_program, target, target->function, location, assignments); - target=goto_program.insert_after(target); - return new_rhs; - } - else if(rhs.id()==ID_typecast && - implements_java_char_sequence(rhs.op0().type())) - { - exprt new_rhs=make_cprover_string_assign( - goto_program, target, rhs.op0(), location); - return typecast_exprt(new_rhs, rhs.type()); - } - else - return rhs; -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::make_cprover_char_array_assign - - Inputs: a goto_program, a position in this program, an expression of - type char array pointer and a location - - Outputs: a string expression - - Purpose: Introduce a temporary variable for cprover strings; - returns the cprover_string corresponding to rhs - -\*******************************************************************/ - -string_exprt string_refine_preprocesst::make_cprover_char_array_assign( - goto_programt &goto_program, - goto_programt::targett &target, - const exprt &rhs, - const source_locationt &location) -{ - assert(is_java_char_array_pointer_type(rhs.type())); - - // We do the following assignments: - // deref=*(rhs->data) - // array= typecast(&deref); - // string={ rhs->length; array } - - dereference_exprt deref(rhs, rhs.type().subtype()); - typet length_type, data_type; - get_data_and_length_type_of_char_array(deref, data_type, length_type); - assert(data_type.id()==ID_pointer); - typet char_type=to_pointer_type(data_type).subtype(); - - refined_string_typet ref_type(length_type, java_char_type()); - typet content_type=ref_type.get_content_type(); - std::list assignments; - - // deref=*(rhs->data) - member_exprt array_rhs(deref, "data", data_type); - dereference_exprt deref_array(array_rhs, data_type.subtype()); - symbolt sym_lhs_deref=get_fresh_aux_symbol( - data_type.subtype(), - "char_array_assign$deref", - "char_array_assign$deref", - location, - ID_java, - symbol_table); - symbol_exprt lhs_deref=sym_lhs_deref.symbol_expr(); - assignments.emplace_back(lhs_deref, deref_array); - - // array=convert_pointer_to_char_array(*rhs->data) - declare_function(ID_cprover_string_array_of_char_pointer_func, content_type); - function_application_exprt fun_app(symbol_exprt( - ID_cprover_string_array_of_char_pointer_func), content_type); - fun_app.arguments().push_back(deref_array); - symbol_exprt array=fresh_array(content_type, location); - assignments.emplace_back(array, fun_app); - - // string={ rhs->length; string_array } - string_exprt new_rhs(get_length(deref, length_type), array, ref_type); - symbol_exprt lhs=fresh_string(ref_type, location); - assignments.emplace_back(lhs, new_rhs); - - insert_assignments( - goto_program, target, target->function, location, assignments); - target=goto_program.insert_after(target); - return new_rhs; -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::make_normal_assign - - Inputs: a goto_program, a position in this program, an expression lhs, - a function type, a function name, a vector of arguments, a location - and a signature - - Purpose: replace the current instruction by: - > lhs=function_name(arguments) : return_type @ location - If given, signature can force String conversion of given arguments. - The convention for signature is one character by argument - and 'S' denotes string. - -\*******************************************************************/ - -void string_refine_preprocesst::make_normal_assign( - goto_programt &goto_program, - goto_programt::targett target, - const exprt &lhs, - const code_typet &function_type, - const irep_idt &function_name, - const exprt::operandst &arguments, - const source_locationt &location, - const std::string &signature) -{ - function_application_exprt rhs( - symbol_exprt(function_name), function_type.return_type()); - rhs.add_source_location()=location; - declare_function(function_name, function_type); - - exprt::operandst processed_arguments=process_arguments( - goto_program, target, arguments, location, signature); - rhs.arguments()=processed_arguments; - - code_assignt assignment(lhs, rhs); - assignment.add_source_location()=location; - target->make_assignment(); - target->code=assignment; -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::insert_assignments - - Inputs: a goto_program, a position in this program, a list of assignments - - Purpose: add the assignments to the program in the order they are given - -\*******************************************************************/ - -void string_refine_preprocesst::insert_assignments( - goto_programt &goto_program, - goto_programt::targett &target, - irep_idt function, - source_locationt location, - const std::list &va) -{ - if(va.empty()) - return; - - auto i=va.begin(); - target->make_assignment(); - target->code=*i; - target->function=function; - target->source_location=location; - for(i++; i!=va.end(); i++) - { - target=goto_program.insert_after(target); - target->make_assignment(); - target->code=*i; - target->function=function; - target->source_location=location; - } -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::make_string_assign - - Inputs: a goto_program, a position in this program, an expression lhs, - a function type, a function name, a vector of arguments, a location - and a signature - - Purpose: replace the current instruction by: - > lhs=malloc(String *) - > lhs->length=function_name_length(arguments) - > tmp_data=function_name_data(arguments) - > lhs->data=&tmp_data - -\*******************************************************************/ - -void string_refine_preprocesst::make_string_assign( - goto_programt &goto_program, - goto_programt::targett &target, - const exprt &lhs, - const code_typet &function_type, - const irep_idt &function_name, - const exprt::operandst &arguments, - const source_locationt &location, - const std::string &signature) -{ - assert(implements_java_char_sequence(function_type.return_type())); - dereference_exprt deref(lhs, lhs.type().subtype()); - typet object_type=ns.follow(deref.type()); - exprt object_size=size_of_expr(object_type, ns); - typet length_type, data_type; - get_data_and_length_type_of_string(deref, data_type, length_type); - - std::string fnamel=id2string(function_name)+"_length"; - std::string fnamed=id2string(function_name)+"_data"; - declare_function(fnamel, length_type); - declare_function(fnamed, data_type); - function_application_exprt rhs_length(symbol_exprt(fnamel), length_type); - function_application_exprt rhs_data( - symbol_exprt(fnamed), data_type.subtype()); - - exprt::operandst processed_arguments=process_arguments( - goto_program, target, arguments, location, signature); - rhs_length.arguments()=processed_arguments; - rhs_data.arguments()=processed_arguments; - - symbolt sym_length=get_fresh_aux_symbol( - length_type, "length", "length", location, ID_java, symbol_table); - symbol_exprt tmp_length=sym_length.symbol_expr(); - symbol_exprt tmp_array=fresh_array(data_type.subtype(), location); - member_exprt lhs_length(deref, "length", length_type); - member_exprt lhs_data(deref, "data", tmp_array.type()); - - // lhs=malloc(String *) - assert(object_size.is_not_nil()); // got nil object_size - side_effect_exprt malloc_expr(ID_malloc); - malloc_expr.copy_to_operands(object_size); - malloc_expr.type()=pointer_typet(object_type); - malloc_expr.add_source_location()=location; - - refined_string_typet ref_type(length_type, data_type.subtype().subtype()); - string_exprt str(tmp_length, tmp_array, ref_type); - symbol_exprt cprover_string_sym=fresh_string(ref_type, location); - - std::list assigns; - assigns.emplace_back(lhs, malloc_expr); - assigns.emplace_back(tmp_length, rhs_length); - assigns.emplace_back(lhs_length, tmp_length); - assigns.emplace_back(tmp_array, rhs_data); - assigns.emplace_back(cprover_string_sym, str); - assigns.emplace_back(lhs_data, address_of_exprt(tmp_array)); - insert_assignments(goto_program, target, target->function, location, assigns); -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::make_string_function - - Inputs: a position in a goto program, a function name, an expression lhs, - a function type, name, arguments, a location and a signature string - - Purpose: at the current position replace `lhs=s.some_function(x,...)` - by `lhs=function_name(s,x,...)`; - -\*******************************************************************/ - -void string_refine_preprocesst::make_string_function( - goto_programt &goto_program, - goto_programt::targett &target, - const exprt &lhs, - const code_typet &function_type, - const irep_idt &function_name, - const exprt::operandst &arguments, - const source_locationt &location, - const std::string &signature) -{ - if(signature.length()>0) - { - if(signature.back()=='S') - { - make_string_assign( - goto_program, - target, - lhs, - function_type, - function_name, - arguments, - location, - signature); - } - else - make_normal_assign( - goto_program, - target, - lhs, - function_type, - function_name, - arguments, - location, - signature); - } - else if(implements_java_char_sequence(function_type.return_type())) - make_string_assign( - goto_program, - target, - lhs, - function_type, - function_name, - arguments, - location, - signature); - else - make_normal_assign( - goto_program, - target, - lhs, - function_type, - function_name, - arguments, - location, - signature); -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::make_string_function - - Inputs: a position in a goto program, a function name and two Boolean options - - Purpose: at the current position replace `lhs=s.some_function(x,...)` - by `lhs=function_name(s,x,...)`; - option `assign_first_arg` uses `s` instead of `lhs` in the resulting - expression, Warning : it assumes that `s` is string-like - option `skip_first_arg`, removes `s` from the arguments, ie `x` is - the first one; - arguments that are string (TODO: and char array) are replaced - by string_exprt - -\*******************************************************************/ - -void string_refine_preprocesst::make_string_function( - goto_programt &goto_program, - goto_programt::targett &target, - const irep_idt &function_name, - const std::string &signature, - bool assign_first_arg, - bool skip_first_arg) -{ - code_function_callt &function_call=to_code_function_call(target->code); - code_typet function_type=to_code_type(function_call.function().type()); - code_typet new_type; - const source_locationt loc=function_call.source_location(); - declare_function(function_name, function_type); - function_application_exprt rhs; - std::vector args; - if(assign_first_arg) - { - assert(!function_call.arguments().empty()); - rhs.type()=function_call.arguments()[0].type(); - } - else - rhs.type()=function_type.return_type(); - rhs.add_source_location()=function_call.source_location(); - rhs.function()=symbol_exprt(function_name); - - std::size_t start_index=skip_first_arg?1:0; - for(std::size_t i=start_index; i tmp=function_name(x,...) - > s->data=tmp.data - > s->length=tmp.length - > r=s - -\*******************************************************************/ - -void string_refine_preprocesst::make_string_function_side_effect( - goto_programt &goto_program, - goto_programt::targett &target, - const irep_idt &function_name, - const std::string &signature) -{ - // Cannot use const & here - code_function_callt function_call=to_code_function_call(target->code); - source_locationt loc=function_call.source_location(); - std::list assignments; - const exprt &lhs=function_call.lhs(); - assert(!function_call.arguments().empty()); - const exprt &s=function_call.arguments()[0]; - code_typet function_type=to_code_type(function_call.type()); - - function_type.return_type()=s.type(); - - if(lhs.is_not_nil()) - { - symbol_exprt tmp_string=fresh_string(lhs.type(), loc); - - make_string_assign( - goto_program, - target, - tmp_string, - function_type, - function_name, - function_call.arguments(), - loc, - signature); - dereference_exprt deref_lhs(s, s.type().subtype()); - typet data_type, length_type; - get_data_and_length_type_of_string(deref_lhs, data_type, length_type); - member_exprt lhs_data(deref_lhs, "data", data_type); - member_exprt lhs_length(deref_lhs, "length", length_type); - dereference_exprt deref_rhs(tmp_string, s.type().subtype()); - member_exprt rhs_data(deref_rhs, "data", data_type); - member_exprt rhs_length(deref_rhs, "length", length_type); - assignments.emplace_back(lhs_length, rhs_length); - assignments.emplace_back(lhs_data, rhs_data); - assignments.emplace_back(lhs, s); - target=goto_program.insert_after(target); - insert_assignments( - goto_program, target, target->function, loc, assignments); - } - else - { - make_string_function( - goto_program, target, function_name, signature, true, false); - } -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::build_function_application - - Inputs: a function name, a type, a location and a vector of arguments - - Outputs: a function application expression - - Purpose: declare a function and construct an function application expression - with the given function name, type, location and arguments - -\*******************************************************************/ - -function_application_exprt - string_refine_preprocesst::build_function_application( - const irep_idt &function_name, - const typet &type, - const source_locationt &location, - const exprt::operandst &arguments) -{ - declare_function(function_name, type); - function_application_exprt function_app(symbol_exprt(function_name), type); - function_app.add_source_location()=location; - for(const auto &arg : arguments) - function_app.arguments().push_back(arg); - - return function_app; -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::make_to_char_array_function - - Inputs: a goto program and a position in that goto program - - Purpose: at the given position replace `return_tmp0=s.toCharArray()` with: - > return_tmp0 = malloc(array[char]); - > return_tmp0->data=&((s->data)[0]) - > return_tmp0->length=s->length - -\*******************************************************************/ - -void string_refine_preprocesst::make_to_char_array_function( - goto_programt &goto_program, goto_programt::targett &target) -{ - const code_function_callt &function_call=to_code_function_call(target->code); - source_locationt location=function_call.source_location(); - - assert(!function_call.arguments().empty()); - const exprt &string_argument=function_call.arguments()[0]; - assert(is_java_string_pointer_type(string_argument.type())); - - typet deref_type=function_call.lhs().type().subtype(); - const exprt &lhs=function_call.lhs(); - dereference_exprt deref_lhs(lhs, deref_type); - - dereference_exprt deref(string_argument, string_argument.type().subtype()); - typet length_type, data_type; - get_data_and_length_type_of_string(deref, data_type, length_type); - std::list assignments; - - // lhs=malloc(array[char]) - typet object_type=ns.follow(deref_type); - exprt object_size=size_of_expr(object_type, ns); - - if(object_size.is_nil()) - debug() << "string_refine_preprocesst::make_to_char_array_function " - << "got nil object_size" << eom; - - side_effect_exprt malloc_expr(ID_malloc); - malloc_expr.copy_to_operands(object_size); - malloc_expr.type()=pointer_typet(object_type); - malloc_expr.add_source_location()=location; - assignments.emplace_back(lhs, malloc_expr); - - - // &((s->data)[0]) - exprt rhs_data=get_data(deref, data_type); - dereference_exprt rhs_array(rhs_data, data_type.subtype()); - exprt first_index=from_integer(0, java_int_type()); - index_exprt first_element(rhs_array, first_index, java_char_type()); - address_of_exprt rhs_pointer(first_element); - - // return_tmp0->data=&((s->data)[0]) - exprt lhs_data=get_data(deref_lhs, data_type); - assignments.emplace_back(lhs_data, rhs_pointer); - - // return_tmp0->length=s->length - exprt rhs_length=get_length(deref, length_type); - exprt lhs_length=get_length(deref_lhs, length_type); - assignments.emplace_back(lhs_length, rhs_length); - insert_assignments( - goto_program, target, target->function, location, assignments); -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::process_arguments - - Inputs: a goto program, a position, a list of expressions, a location and a - signature - - Outputs: a list of expressions - - Purpose: for each expression that is a string or that is at a position with - an 'S' character in the signature, 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. - -\*******************************************************************/ - -exprt::operandst string_refine_preprocesst::process_arguments( - goto_programt &goto_program, - goto_programt::targett &target, - const exprt::operandst &arguments, - const source_locationt &location, - const std::string &signature) -{ - exprt::operandst new_arguments; - - for(std::size_t i=0; isecond; - else - return ""; -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::replace_string_calls - - Inputs: a function in a goto_program - - Purpose: goes through the instructions, replace function calls to string - function by equivalent instructions using functions defined - for the string solver, replace string literals by string - expressions of the type used by the string solver - TODO: the current implementation is only for java functions, - we should add support for other languages - -\*******************************************************************/ - -void string_refine_preprocesst::replace_string_calls( - goto_functionst::function_mapt::iterator f_it) -{ - goto_programt &goto_program=f_it->second.body; - - Forall_goto_program_instructions(target, goto_program) - { - if(target->is_function_call()) - { - const code_function_callt function_call= - to_code_function_call(target->code); - - if(function_call.function().id()==ID_symbol) - { - const irep_idt &function_id= - to_symbol_expr(function_call.function()).get_identifier(); - std::string signature=function_signature(function_id); - - auto it=string_functions.find(function_id); - if(it!=string_functions.end()) - make_string_function( - goto_program, target, it->second, signature, false, false); - - it=side_effect_functions.find(function_id); - if(it!=side_effect_functions.end()) - make_string_function_side_effect( - goto_program, target, it->second, signature); - - it=string_function_calls.find(function_id); - if(it!=string_function_calls.end()) - make_string_function_call( - goto_program, target, it->second, signature); - - if(function_id==irep_idt("java::java.lang.String.toCharArray:()[C")) - make_to_char_array_function(goto_program, target); - } - } - else - { - if(target->is_assign()) - { - // In assignments we replace string literals and C string functions - code_assignt assignment=to_code_assign(target->code); - - exprt new_rhs=assignment.rhs(); - code_assignt new_assignment(assignment.lhs(), new_rhs); - - if(new_rhs.id()==ID_function_application) - { - function_application_exprt f=to_function_application_expr(new_rhs); - const exprt &name=f.function(); - assert(name.id()==ID_symbol); - const irep_idt &id=to_symbol_expr(name).get_identifier(); - auto it=c_string_functions.find(id); - if(it!=c_string_functions.end()) - { - declare_function(it->second, f.type()); - f.function()=symbol_exprt(it->second); - new_assignment=code_assignt(assignment.lhs(), f); - } - } - - new_assignment.add_source_location()=assignment.source_location(); - target->make_assignment(); - target->code=new_assignment; - } - } - } - return; -} - -/*******************************************************************\ - -Function: string_refine_preprocesst::initialize_string_function_table - - Purpose: fill maps with correspondance from java method names to cprover - functions - -\*******************************************************************/ - -void string_refine_preprocesst::initialize_string_function_table() -{ - // String library - string_function_calls - ["java::java.lang.String.:(Ljava/lang/String;)V"]= - ID_cprover_string_copy_func; - string_function_calls - ["java::java.lang.String.:(Ljava/lang/StringBuilder;)V"]= - ID_cprover_string_copy_func; - string_function_calls["java::java.lang.String.:([C)V"]= - ID_cprover_string_copy_func; - string_function_calls["java::java.lang.String.:([CII)V"]= - ID_cprover_string_copy_func; - string_function_calls["java::java.lang.String.:()V"]= - ID_cprover_string_empty_string_func; - // Not supported java.lang.String.:(Ljava/lang/StringBuffer;) - - string_functions["java::java.lang.String.charAt:(I)C"]= - ID_cprover_string_char_at_func; - string_functions["java::java.lang.String.codePointAt:(I)I"]= - ID_cprover_string_code_point_at_func; - string_functions["java::java.lang.String.codePointBefore:(I)I"]= - ID_cprover_string_code_point_before_func; - string_functions["java::java.lang.String.codePointCount:(II)I"]= - ID_cprover_string_code_point_count_func; - string_functions["java::java.lang.String.compareTo:(Ljava/lang/String;)I"]= - ID_cprover_string_compare_to_func; - // Not supported "java.lang.String.contentEquals" - string_functions - ["java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]= - ID_cprover_string_concat_func; - string_functions - ["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]= - ID_cprover_string_contains_func; - string_functions - ["java::java.lang.String.copyValueOf:([CII)Ljava/lang/String;"]= - ID_cprover_string_copy_func; - string_functions - ["java::java.lang.String.copyValueOf:([C)Ljava/lang/String;"]= - ID_cprover_string_copy_func; - string_functions["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]= - ID_cprover_string_endswith_func; - string_functions["java::java.lang.String.equals:(Ljava/lang/Object;)Z"]= - ID_cprover_string_equal_func; - string_functions - ["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]= - ID_cprover_string_equals_ignore_case_func; - // Not supported "java.lang.String.format" - // Not supported "java.lang.String.getBytes" - // Not supported "java.lang.String.getChars" - string_functions["java::java.lang.String.hashCode:()I"]= - ID_cprover_string_hash_code_func; - string_functions["java::java.lang.String.indexOf:(I)I"]= - ID_cprover_string_index_of_func; - string_functions["java::java.lang.String.indexOf:(II)I"]= - ID_cprover_string_index_of_func; - string_functions["java::java.lang.String.indexOf:(Ljava/lang/String;)I"]= - ID_cprover_string_index_of_func; - string_functions["java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]= - ID_cprover_string_index_of_func; - string_functions["java::java.lang.String.intern:()Ljava/lang/String;"]= - ID_cprover_string_intern_func; - string_functions["java::java.lang.String.isEmpty:()Z"]= - ID_cprover_string_is_empty_func; - string_functions["java::java.lang.String.lastIndexOf:(I)I"]= - ID_cprover_string_last_index_of_func; - string_functions["java::java.lang.String.lastIndexOf:(II)I"]= - ID_cprover_string_last_index_of_func; - string_functions - ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I"]= - ID_cprover_string_last_index_of_func; - string_functions - ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]= - ID_cprover_string_last_index_of_func; - string_functions["java::java.lang.String.length:()I"]= - ID_cprover_string_length_func; - // Not supported "java.lang.String.matches" - string_functions["java::java.lang.String.offsetByCodePoints:(II)I"]= - ID_cprover_string_offset_by_code_point_func; - // Not supported "java.lang.String.regionMatches" - string_functions["java::java.lang.String.replace:(CC)Ljava/lang/String;"]= - ID_cprover_string_replace_func; - // Not supported "java.lang.String.replace:(LCharSequence;LCharSequence)" - // Not supported "java.lang.String.replaceAll" - // Not supported "java.lang.String.replaceFirst" - // Not supported "java.lang.String.split" - string_functions["java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]= - ID_cprover_string_startswith_func; - string_functions - ["java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]= - ID_cprover_string_startswith_func; - string_functions - ["java::java.lang.String.subSequence:(II)Ljava/lang/CharSequence;"]= - ID_cprover_string_substring_func; - string_functions["java::java.lang.String.substring:(II)Ljava/lang/String;"]= - ID_cprover_string_substring_func; - string_functions["java::java.lang.String.substring:(I)Ljava/lang/String;"]= - ID_cprover_string_substring_func; - // "java.lang.String.toCharArray has a special treatment in the - // replace_string_calls function - string_functions["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]= - ID_cprover_string_to_lower_case_func; - // Not supported "java.lang.String.toLowerCase:(Locale)" - // Not supported "java.lang.String.toString:()" - string_functions["java::java.lang.String.toUpperCase:()Ljava/lang/String;"]= - ID_cprover_string_to_upper_case_func; - // Not supported "java.lang.String.toUpperCase:(Locale)" - string_functions["java::java.lang.String.trim:()Ljava/lang/String;"]= - ID_cprover_string_trim_func; - string_functions["java::java.lang.String.valueOf:(Z)Ljava/lang/String;"]= - ID_cprover_string_of_bool_func; - string_functions["java::java.lang.String.valueOf:(C)Ljava/lang/String;"]= - ID_cprover_string_of_char_func; - string_functions["java::java.lang.String.valueOf:([C)Ljava/lang/String;"]= - ID_cprover_string_copy_func; - string_functions["java::java.lang.String.valueOf:([CII)Ljava/lang/String;"]= - ID_cprover_string_copy_func; - string_functions["java::java.lang.String.valueOf:(D)Ljava/lang/String;"]= - ID_cprover_string_of_double_func; - string_functions["java::java.lang.String.valueOf:(F)Ljava/lang/String;"]= - ID_cprover_string_of_float_func; - string_functions["java::java.lang.String.valueOf:(I)Ljava/lang/String;"]= - ID_cprover_string_of_int_func; - string_functions["java::java.lang.String.valueOf:(J)Ljava/lang/String;"]= - ID_cprover_string_of_long_func; - // Not supported "java.lang.String.valueOf:(LObject;)" - - // StringBuilder library - string_function_calls - ["java::java.lang.StringBuilder.:(Ljava/lang/String;)V"]= - ID_cprover_string_copy_func; - string_function_calls["java::java.lang.StringBuilder.:()V"]= - ID_cprover_string_empty_string_func; - - side_effect_functions - ["java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;"]= - ID_cprover_string_concat_bool_func; - side_effect_functions - ["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]= - ID_cprover_string_concat_char_func; - side_effect_functions - ["java::java.lang.StringBuilder.append:([C)" - "Ljava/lang/StringBuilder;"]= - ID_cprover_string_concat_func; - // Not supported: "java.lang.StringBuilder.append:([CII)" - // Not supported: "java.lang.StringBuilder.append:(LCharSequence;)" - side_effect_functions - ["java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"]= - ID_cprover_string_concat_double_func; - side_effect_functions - ["java::java.lang.StringBuilder.append:(F)Ljava/lang/StringBuilder;"]= - ID_cprover_string_concat_float_func; - side_effect_functions - ["java::java.lang.StringBuilder.append:(I)Ljava/lang/StringBuilder;"]= - ID_cprover_string_concat_int_func; - side_effect_functions - ["java::java.lang.StringBuilder.append:(J)Ljava/lang/StringBuilder;"]= - ID_cprover_string_concat_long_func; - // Not supported: "java.lang.StringBuilder.append:(LObject;)" - side_effect_functions - ["java::java.lang.StringBuilder.append:(Ljava/lang/String;)" - "Ljava/lang/StringBuilder;"]= - ID_cprover_string_concat_func; - side_effect_functions - ["java::java.lang.StringBuilder.appendCodePoint:(I)" - "Ljava/lang/StringBuilder;"]= - ID_cprover_string_concat_code_point_func; - // Not supported: "java.lang.StringBuilder.append:(Ljava/lang/StringBuffer;)" - // Not supported: "java.lang.StringBuilder.capacity:()" - string_functions["java::java.lang.StringBuilder.charAt:(I)C"]= - ID_cprover_string_char_at_func; - string_functions["java::java.lang.StringBuilder.codePointAt:(I)I"]= - ID_cprover_string_code_point_at_func; - string_functions["java::java.lang.StringBuilder.codePointBefore:(I)I"]= - ID_cprover_string_code_point_before_func; - string_functions["java::java.lang.StringBuilder.codePointCount:(II)I"]= - ID_cprover_string_code_point_count_func; - side_effect_functions - ["java::java.lang.StringBuilder.delete:(II)Ljava/lang/StringBuilder;"]= - ID_cprover_string_delete_func; - side_effect_functions - ["java::java.lang.StringBuilder.deleteCharAt:(I)Ljava/lang/StringBuilder;"]= - ID_cprover_string_delete_char_at_func; - // Not supported: "java.lang.StringBuilder.ensureCapacity:()" - // Not supported: "java.lang.StringBuilder.getChars:()" - // Not supported: "java.lang.StringBuilder.indexOf:()" - side_effect_functions - ["java::java.lang.StringBuilder.insert:(IZ)Ljava/lang/StringBuilder;"]= - ID_cprover_string_insert_bool_func; - side_effect_functions - ["java::java.lang.StringBuilder.insert:(IC)Ljava/lang/StringBuilder;"]= - ID_cprover_string_insert_char_func; - side_effect_functions - ["java::java.lang.StringBuilder.insert:(I[C)Ljava/lang/StringBuilder;"]= - ID_cprover_string_insert_func; - side_effect_functions - ["java::java.lang.StringBuilder.insert:(I[CII)Ljava/lang/StringBuilder;"]= - ID_cprover_string_insert_func; - // Not supported "java.lang.StringBuilder.insert:(ILCharSequence;)" - // Not supported "java.lang.StringBuilder.insert:(ILCharSequence;II)" - // Not supported "java.lang.StringBuilder.insert:(ID)" - // Not supported "java.lang.StringBuilder.insert:(IF)" - side_effect_functions - ["java::java.lang.StringBuilder.insert:(II)Ljava/lang/StringBuilder;"]= - ID_cprover_string_insert_int_func; - side_effect_functions - ["java::java.lang.StringBuilder.insert:(IJ)Ljava/lang/StringBuilder;"]= - ID_cprover_string_insert_long_func; - // Not supported "java.lang.StringBuilder.insert:(ILObject;)" - side_effect_functions - ["java::java.lang.StringBuilder.insert:(ILjava/lang/String;)" - "Ljava/lang/StringBuilder;"]= - ID_cprover_string_insert_func; - // Not supported "java.lang.StringBuilder.lastIndexOf" - string_functions["java::java.lang.StringBuilder.length:()I"]= - ID_cprover_string_length_func; - // Not supported "java.lang.StringBuilder.offsetByCodePoints" - // Not supported "java.lang.StringBuilder.replace" - // Not supported "java.lang.StringBuilder.reverse" - side_effect_functions["java::java.lang.StringBuilder.setCharAt:(IC)V"]= - ID_cprover_string_char_set_func; - side_effect_functions - ["java::java.lang.StringBuilder.setLength:(I)V"]= - ID_cprover_string_set_length_func; - // Not supported "java.lang.StringBuilder.subSequence" - string_functions - ["java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]= - ID_cprover_string_substring_func; - string_functions - ["java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]= - ID_cprover_string_substring_func; - string_functions - ["java::java.lang.StringBuilder.toString:()Ljava/lang/String;"]= - ID_cprover_string_copy_func; - // Not supported "java.lang.StringBuilder.trimToSize" - // TODO clean irep ids from insert_char_array etc... - - // StringBuffer library - string_function_calls - ["java::java.lang.StringBuffer.:(Ljava/lang/String;)V"]= - ID_cprover_string_copy_func; - string_function_calls["java::java.lang.StringBuffer.:()V"]= - ID_cprover_string_empty_string_func; - - side_effect_functions - ["java::java.lang.StringBuffer.append:(Z)Ljava/lang/StringBuffer;"]= - ID_cprover_string_concat_bool_func; - side_effect_functions - ["java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]= - ID_cprover_string_concat_char_func; - side_effect_functions - ["java::java.lang.StringBuffer.append:([C)" - "Ljava/lang/StringBuffer;"]= - ID_cprover_string_concat_func; - // Not supported: "java.lang.StringBuffer.append:([CII)" - // Not supported: "java.lang.StringBuffer.append:(LCharSequence;)" - side_effect_functions - ["java::java.lang.StringBuffer.append:(D)Ljava/lang/StringBuffer;"]= - ID_cprover_string_concat_double_func; - side_effect_functions - ["java::java.lang.StringBuffer.append:(F)Ljava/lang/StringBuffer;"]= - ID_cprover_string_concat_float_func; - side_effect_functions - ["java::java.lang.StringBuffer.append:(I)Ljava/lang/StringBuffer;"]= - ID_cprover_string_concat_int_func; - side_effect_functions - ["java::java.lang.StringBuffer.append:(J)Ljava/lang/StringBuffer;"]= - ID_cprover_string_concat_long_func; - // Not supported: "java.lang.StringBuffer.append:(LObject;)" - side_effect_functions - ["java::java.lang.StringBuffer.append:(Ljava/lang/String;)" - "Ljava/lang/StringBuffer;"]= - ID_cprover_string_concat_func; - side_effect_functions - ["java::java.lang.StringBuffer.appendCodePoint:(I)" - "Ljava/lang/StringBuffer;"]= - ID_cprover_string_concat_code_point_func; - // Not supported: "java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)" - // Not supported: "java.lang.StringBuffer.capacity:()" - string_functions["java::java.lang.StringBuffer.charAt:(I)C"]= - ID_cprover_string_char_at_func; - string_functions["java::java.lang.StringBuffer.codePointAt:(I)I"]= - ID_cprover_string_code_point_at_func; - string_functions["java::java.lang.StringBuffer.codePointBefore:(I)I"]= - ID_cprover_string_code_point_before_func; - string_functions["java::java.lang.StringBuffer.codePointCount:(II)I"]= - ID_cprover_string_code_point_count_func; - side_effect_functions - ["java::java.lang.StringBuffer.delete:(II)Ljava/lang/StringBuffer;"]= - ID_cprover_string_delete_func; - side_effect_functions - ["java::java.lang.StringBuffer.deleteCharAt:(I)Ljava/lang/StringBuffer;"]= - ID_cprover_string_delete_char_at_func; - // Not supported: "java.lang.StringBuffer.ensureCapacity:()" - // Not supported: "java.lang.StringBuffer.getChars:()" - // Not supported: "java.lang.StringBuffer.indexOf:()" - side_effect_functions - ["java::java.lang.StringBuffer.insert:(IZ)Ljava/lang/StringBuffer;"]= - ID_cprover_string_insert_bool_func; - side_effect_functions - ["java::java.lang.StringBuffer.insert:(IC)Ljava/lang/StringBuffer;"]= - ID_cprover_string_insert_char_func; - side_effect_functions - ["java::java.lang.StringBuffer.insert:(I[C)Ljava/lang/StringBuffer;"]= - ID_cprover_string_insert_func; - side_effect_functions - ["java::java.lang.StringBuffer.insert:(I[CII)Ljava/lang/StringBuffer;"]= - ID_cprover_string_insert_func; - // Not supported "java.lang.StringBuffer.insert:(ILCharSequence;)" - // Not supported "java.lang.StringBuffer.insert:(ILCharSequence;II)" - // Not supported "java.lang.StringBuffer.insert:(ID)" - // Not supported "java.lang.StringBuffer.insert:(IF)" - side_effect_functions - ["java::java.lang.StringBuffer.insert:(II)Ljava/lang/StringBuffer;"]= - ID_cprover_string_insert_int_func; - side_effect_functions - ["java::java.lang.StringBuffer.insert:(IJ)Ljava/lang/StringBuffer;"]= - ID_cprover_string_insert_long_func; - // Not supported "java.lang.StringBuffer.insert:(ILObject;)" - side_effect_functions - ["java::java.lang.StringBuffer.insert:(ILjava/lang/String;)" - "Ljava/lang/StringBuffer;"]= - ID_cprover_string_insert_func; - // Not supported "java.lang.StringBuffer.lastIndexOf" - string_functions["java::java.lang.StringBuffer.length:()I"]= - ID_cprover_string_length_func; - // Not supported "java.lang.StringBuffer.offsetByCodePoints" - // Not supported "java.lang.StringBuffer.replace" - // Not supported "java.lang.StringBuffer.reverse" - side_effect_functions["java::java.lang.StringBuffer.setCharAt:(IC)V"]= - ID_cprover_string_char_set_func; - side_effect_functions - ["java::java.lang.StringBuffer.setLength:(I)V"]= - ID_cprover_string_set_length_func; - // Not supported "java.lang.StringBuffer.subSequence" - string_functions - ["java::java.lang.StringBuffer.substring:(II)Ljava/lang/String;"]= - ID_cprover_string_substring_func; - string_functions - ["java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]= - ID_cprover_string_substring_func; - string_functions - ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"]= - ID_cprover_string_copy_func; - // Not supported "java.lang.StringBuffer.trimToSize" - - // Other libraries - string_functions["java::java.lang.CharSequence.charAt:(I)C"]= - ID_cprover_string_char_at_func; - string_functions["java::java.lang.Float.toString:(F)Ljava/lang/String;"]= - ID_cprover_string_of_float_func; - string_functions["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]= - ID_cprover_string_of_int_hex_func; - string_functions["java::java.lang.Integer.parseInt:(Ljava/lang/String;)I"]= - ID_cprover_string_parse_int_func; - string_functions["java::java.lang.Integer.toString:(I)Ljava/lang/String;"]= - ID_cprover_string_of_int_func; - - // C functions - c_string_functions["__CPROVER_uninterpreted_string_literal_func"]= - ID_cprover_string_literal_func; - c_string_functions["__CPROVER_uninterpreted_string_char_at_func"]= - ID_cprover_string_char_at_func; - c_string_functions["__CPROVER_uninterpreted_string_equal_func"]= - ID_cprover_string_equal_func; - c_string_functions["__CPROVER_uninterpreted_string_concat_func"]= - ID_cprover_string_concat_func; - c_string_functions["__CPROVER_uninterpreted_string_length_func"]= - ID_cprover_string_length_func; - c_string_functions["__CPROVER_uninterpreted_string_substring_func"]= - ID_cprover_string_substring_func; - c_string_functions["__CPROVER_uninterpreted_string_is_prefix_func"]= - ID_cprover_string_is_prefix_func; - c_string_functions["__CPROVER_uninterpreted_string_is_suffix_func"]= - ID_cprover_string_is_suffix_func; - c_string_functions["__CPROVER_uninterpreted_string_contains_func"]= - ID_cprover_string_contains_func; - c_string_functions["__CPROVER_uninterpreted_string_index_of_func"]= - ID_cprover_string_index_of_func; - c_string_functions["__CPROVER_uninterpreted_string_last_index_of_func"]= - ID_cprover_string_last_index_of_func; - c_string_functions["__CPROVER_uninterpreted_string_char_set_func"]= - ID_cprover_string_char_set_func; - c_string_functions["__CPROVER_uninterpreted_string_copy_func"]= - ID_cprover_string_copy_func; - c_string_functions["__CPROVER_uninterpreted_string_parse_int_func"]= - ID_cprover_string_parse_int_func; - c_string_functions["__CPROVER_uninterpreted_string_of_int_func"]= - ID_cprover_string_of_int_func; - - // Signatures - signatures["java::java.lang.String.equals:(Ljava/lang/Object;)Z"]="SSZ"; - signatures["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]= - "SSZ"; - signatures["java::java.lang.StringBuilder.insert:(IZ)" - "Ljava/lang/StringBuilder;"]="SIZ_"; - signatures["java::java.lang.StringBuilder.insert:(IJ)" - "Ljava/lang/StringBuilder;"]="SIJ_"; - signatures["java::java.lang.StringBuilder.insert:(II)" - "Ljava/lang/StringBuilder;"]="SII_"; - signatures["java::java.lang.StringBuilder.insert:(IC)" - "Ljava/lang/StringBuilder;"]="SIC_"; - signatures["java::java.lang.StringBuilder.insert:(ILjava/lang/String;)" - "Ljava/lang/StringBuilder;"]="SIS_"; - signatures["java::java.lang.StringBuilder.insert:(ILjava/lang/String;)" - "Ljava/lang/StringBuilder;"]="SIS_"; - signatures["java::java.lang.StringBuilder.insert:(I[C)" - "Ljava/lang/StringBuilder;"]="SI[_"; - signatures["java::java.lang.String.intern:()Ljava/lang/String;"]="SV"; -} - -/*******************************************************************\ - -Constructor: string_refine_preprocesst::string_refine_preprocesst - - Inputs: a symbol table, goto functions, a message handler - - Purpose: process the goto function by replacing calls to string functions - -\*******************************************************************/ - -string_refine_preprocesst::string_refine_preprocesst( - symbol_tablet &_symbol_table, - goto_functionst &_goto_functions, - message_handlert &_message_handler): - messaget(_message_handler), - ns(_symbol_table), - symbol_table(_symbol_table), - goto_functions(_goto_functions), - next_symbol_id(0), - jls_ptr(symbol_typet("java::java.lang.String")) -{ - initialize_string_function_table(); - Forall_goto_functions(it, goto_functions) - replace_string_calls(it); -} diff --git a/src/goto-programs/string_refine_preprocess.h b/src/goto-programs/string_refine_preprocess.h deleted file mode 100644 index df419c73750..00000000000 --- a/src/goto-programs/string_refine_preprocess.h +++ /dev/null @@ -1,203 +0,0 @@ -/*******************************************************************\ - -Module: Preprocess a goto-programs so that calls to the java String - library are recognized by the PASS algorithm - -Author: Romain Brenguier - -Date: September 2016 - -\*******************************************************************/ - -#ifndef CPROVER_GOTO_PROGRAMS_STRING_REFINE_PREPROCESS_H -#define CPROVER_GOTO_PROGRAMS_STRING_REFINE_PREPROCESS_H - -#include -#include -#include - -class string_refine_preprocesst:public messaget -{ - public: - string_refine_preprocesst( - symbol_tablet &, goto_functionst &, message_handlert &); - - private: - namespacet ns; - symbol_tablet & symbol_table; - goto_functionst & goto_functions; - - typedef std::unordered_map id_mapt; - typedef std::unordered_map expr_mapt; - - // Map name of Java string functions to there equivalent in the solver - id_mapt side_effect_functions; - id_mapt string_functions; - id_mapt c_string_functions; - id_mapt string_function_calls; - - std::unordered_map signatures; - - // unique id for each newly created symbols - int next_symbol_id; - - void initialize_string_function_table(); - - static bool check_java_type(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); - - static bool implements_java_char_sequence(const typet &type) - { - return - is_java_char_sequence_pointer_type(type) || - is_java_string_builder_pointer_type(type) || - is_java_string_buffer_pointer_type(type) || - is_java_string_pointer_type(type); - } - - symbol_exprt fresh_array( - const typet &type, const source_locationt &location); - symbol_exprt fresh_string( - const typet &type, const source_locationt &location); - - // get the data member of a java string - static exprt get_data(const exprt &string, const typet &data_type) - { - return member_exprt(string, "data", data_type); - } - - // get the length member of a java string - exprt get_length(const exprt &string, const typet &length_type) - { - return member_exprt(string, "length", length_type); - } - - // type of pointers to string - pointer_typet jls_ptr; - exprt replace_string(const exprt &in); - exprt replace_string_in_assign(const exprt &in); - - void insert_assignments( - goto_programt &goto_program, - goto_programt::targett &target, - irep_idt function, - source_locationt location, - const std::list &va); - - exprt replace_string_pointer(const exprt &in); - - // Replace string builders by expression of the mapping and make - // assignments for strings as string_exprt - exprt::operandst process_arguments( - goto_programt &goto_program, - goto_programt::targett &target, - const exprt::operandst &arguments, - const source_locationt &location, - const std::string &signature=""); - - // Signature of the named function if it is defined in the signature map, - // empty string otherwise - std::string function_signature(const irep_idt &function_id); - - void declare_function(irep_idt function_name, const typet &type); - - void get_data_and_length_type_of_string( - const exprt &expr, typet &data_type, typet &length_type); - - void get_data_and_length_type_of_char_array( - const exprt &expr, typet &data_type, typet &length_type); - - function_application_exprt build_function_application( - const irep_idt &function_name, - const typet &type, - const source_locationt &location, - const exprt::operandst &arguments); - - void make_normal_assign( - goto_programt &goto_program, - goto_programt::targett target, - const exprt &lhs, - const code_typet &function_type, - const irep_idt &function_name, - const exprt::operandst &arguments, - const source_locationt &location, - const std::string &signature=""); - - void make_string_assign( - goto_programt &goto_program, - goto_programt::targett &target, - const exprt &lhs, - const code_typet &function_type, - const irep_idt &function_name, - const exprt::operandst &arguments, - const source_locationt &location, - const std::string &signature); - - exprt make_cprover_string_assign( - goto_programt &goto_program, - goto_programt::targett &target, - const exprt &rhs, - const source_locationt &location); - - string_exprt make_cprover_char_array_assign( - goto_programt &goto_program, - goto_programt::targett &target, - const exprt &rhs, - const source_locationt &location); - - void make_string_function( - goto_programt &goto_program, - goto_programt::targett &target, - const irep_idt &function_name, - const std::string &signature, - bool assign_first_arg=false, - bool skip_first_arg=false); - - void make_string_function( - goto_programt &goto_program, - goto_programt::targett &target, - const exprt &lhs, - const code_typet &function_type, - const irep_idt &function_name, - const exprt::operandst &arguments, - const source_locationt &location, - const std::string &signature); - - void make_string_function_call( - goto_programt &goto_program, - goto_programt::targett &target, - const irep_idt &function_name, - const std::string &signature); - - void make_string_function_side_effect( - goto_programt &goto_program, - goto_programt::targett &target, - const irep_idt &function_name, - const std::string &signature); - - void make_to_char_array_function( - goto_programt &goto_program, goto_programt::targett &); - - void replace_string_calls(goto_functionst::function_mapt::iterator f_it); -}; - -#endif diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index 677987cfc9b..0334b20595f 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -20,6 +20,7 @@ SRC = bytecode_info.cpp \ java_object_factory.cpp \ java_pointer_casts.cpp \ java_root_class.cpp \ + java_string_library_preprocess.cpp \ java_types.cpp \ java_utils.cpp \ # Empty last line diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index ef905eebad2..29be4f70617 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -31,13 +31,13 @@ class java_bytecode_convert_classt:public messaget size_t _max_array_length, lazy_methodst& _lazy_methods, lazy_methods_modet _lazy_methods_mode, - bool _string_refinement_enabled): + const java_string_library_preprocesst &_string_preprocess): messaget(_message_handler), symbol_table(_symbol_table), max_array_length(_max_array_length), lazy_methods(_lazy_methods), lazy_methods_mode(_lazy_methods_mode), - string_refinement_enabled(_string_refinement_enabled) + string_preprocess(_string_preprocess) { } @@ -47,18 +47,10 @@ class java_bytecode_convert_classt:public messaget if(parse_tree.loading_successful) convert(parse_tree.parsed_class); - else if(string_refinement_enabled && - parse_tree.parsed_class.name=="java.lang.String") - add_string_type("java.lang.String"); - else if(string_refinement_enabled && - parse_tree.parsed_class.name=="java.lang.StringBuilder") - add_string_type("java.lang.StringBuilder"); - else if(string_refinement_enabled && - parse_tree.parsed_class.name=="java.lang.CharSequence") - add_string_type("java.lang.CharSequence"); - else if(string_refinement_enabled && - parse_tree.parsed_class.name=="java.lang.StringBuffer") - add_string_type("java.lang.StringBuffer"); + else if(string_preprocess.is_known_string_type( + parse_tree.parsed_class.name)) + string_preprocess.add_string_type( + parse_tree.parsed_class.name, symbol_table); else generate_class_stub(parse_tree.parsed_class.name); } @@ -71,7 +63,7 @@ class java_bytecode_convert_classt:public messaget const size_t max_array_length; lazy_methodst &lazy_methods; lazy_methods_modet lazy_methods_mode; - bool string_refinement_enabled; + java_string_library_preprocesst string_preprocess; // conversion void convert(const classt &c); @@ -79,7 +71,6 @@ class java_bytecode_convert_classt:public messaget void generate_class_stub(const irep_idt &class_name); void add_array_types(); - void add_string_type(const irep_idt &class_name); }; /*******************************************************************\ @@ -486,7 +477,7 @@ bool java_bytecode_convert_class( size_t max_array_length, lazy_methodst &lazy_methods, lazy_methods_modet lazy_methods_mode, - bool string_refinement_enabled) + const java_string_library_preprocesst &string_preprocess) { java_bytecode_convert_classt java_bytecode_convert_class( symbol_table, @@ -494,7 +485,7 @@ bool java_bytecode_convert_class( max_array_length, lazy_methods, lazy_methods_mode, - string_refinement_enabled); + string_preprocess); try { @@ -518,66 +509,3 @@ bool java_bytecode_convert_class( return true; } - -/*******************************************************************\ - -Function: java_bytecode_convert_classt::add_string_type - - Inputs: a name for the class such as "java.lang.String" - - Purpose: Implements the java.lang.String type in the case that - we provide an internal implementation. - -\*******************************************************************/ - -void java_bytecode_convert_classt::add_string_type(const irep_idt &class_name) -{ - class_typet string_type; - string_type.set_tag(class_name); - string_type.components().resize(3); - string_type.components()[0].set_name("@java.lang.Object"); - string_type.components()[0].set_pretty_name("@java.lang.Object"); - string_type.components()[0].type()=symbol_typet("java::java.lang.Object"); - string_type.components()[1].set_name("length"); - string_type.components()[1].set_pretty_name("length"); - string_type.components()[1].type()=java_int_type(); - string_type.components()[2].set_name("data"); - string_type.components()[2].set_pretty_name("data"); - // Use a pointer-to-unbounded-array instead of a pointer-to-char. - // Saves some casting in the string refinement algorithm but may - // be unnecessary. - string_type.components()[2].type()=pointer_typet( - array_typet(java_char_type(), infinity_exprt(java_int_type()))); - string_type.add_base(symbol_typet("java::java.lang.Object")); - - symbolt string_symbol; - string_symbol.name="java::"+id2string(class_name); - string_symbol.base_name=id2string(class_name); - string_symbol.type=string_type; - string_symbol.is_type=true; - - symbol_table.add(string_symbol); - - // Also add a stub of `String.equals` so that remove-virtual-functions - // generates a check for Object.equals vs. String.equals. - // No need to fill it in, as pass_preprocess will replace the calls again. - symbolt string_equals_symbol; - string_equals_symbol.name= - "java::java.lang.String.equals:(Ljava/lang/Object;)Z"; - string_equals_symbol.base_name=id2string(class_name)+".equals"; - string_equals_symbol.pretty_name=id2string(class_name)+".equals"; - string_equals_symbol.mode=ID_java; - - code_typet string_equals_type; - string_equals_type.return_type()=java_boolean_type(); - code_typet::parametert thisparam; - thisparam.set_this(); - thisparam.type()=pointer_typet(symbol_typet(string_symbol.name)); - code_typet::parametert otherparam; - otherparam.type()=pointer_typet(symbol_typet("java::java.lang.Object")); - string_equals_type.parameters().push_back(thisparam); - string_equals_type.parameters().push_back(otherparam); - string_equals_symbol.type=std::move(string_equals_type); - - symbol_table.add(string_equals_symbol); -} diff --git a/src/java_bytecode/java_bytecode_convert_class.h b/src/java_bytecode/java_bytecode_convert_class.h index 9ce5cc8c7cc..3bf4e59c85f 100644 --- a/src/java_bytecode/java_bytecode_convert_class.h +++ b/src/java_bytecode/java_bytecode_convert_class.h @@ -22,6 +22,6 @@ bool java_bytecode_convert_class( size_t max_array_length, lazy_methodst &, lazy_methods_modet, - bool string_refinement_enabled); + const java_string_library_preprocesst &string_preprocess); #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 9e295f2dcc6..63cfb1a9cd5 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_bytecode_convert_method_class.h" #include "bytecode_info.h" #include "java_types.h" +#include "java_string_library_preprocess.h" #include #include @@ -1555,6 +1556,11 @@ codet java_bytecode_convert_methodt::convert_instructions( symbol.name, symbol_table); + // The string refinement module may provide a definition for this + // function. + symbol.value=string_preprocess.code_for_function( + id, to_code_type(symbol.type), loc, symbol_table); + symbol_table.add(symbol); } @@ -1576,7 +1582,10 @@ codet java_bytecode_convert_methodt::convert_instructions( } call.function().add_source_location()=loc; - c=call; + + // Replacing call if it is a function of the Character library, + // returning the same call otherwise + c=string_preprocess.replace_character_call(call); if(!use_this) { @@ -2767,7 +2776,8 @@ void java_bytecode_convert_method( symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, - safe_pointer lazy_methods) + safe_pointer lazy_methods, + const java_string_library_preprocesst &string_preprocess) { static const std::unordered_set methods_to_ignore { @@ -2796,7 +2806,8 @@ void java_bytecode_convert_method( symbol_table, message_handler, max_array_length, - lazy_methods); + lazy_methods, + string_preprocess); java_bytecode_convert_method(class_symbol, method); } diff --git a/src/java_bytecode/java_bytecode_convert_method.h b/src/java_bytecode/java_bytecode_convert_method.h index db6fcc729e1..78dd9226f76 100644 --- a/src/java_bytecode/java_bytecode_convert_method.h +++ b/src/java_bytecode/java_bytecode_convert_method.h @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include "java_string_library_preprocess.h" #include "java_bytecode_parse_tree.h" #include "ci_lazy_methods.h" @@ -24,14 +25,16 @@ void java_bytecode_convert_method( symbol_tablet &symbol_table, message_handlert &message_handler, size_t max_array_length, - safe_pointer lazy_methods); + safe_pointer lazy_methods, + const java_string_library_preprocesst &string_preprocess); inline void java_bytecode_convert_method( const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &method, symbol_tablet &symbol_table, message_handlert &message_handler, - size_t max_array_length) + size_t max_array_length, + const java_string_library_preprocesst &string_preprocess) { java_bytecode_convert_method( class_symbol, @@ -39,7 +42,8 @@ inline void java_bytecode_convert_method( symbol_table, message_handler, max_array_length, - safe_pointer::create_null()); + safe_pointer::create_null(), + string_preprocess); } void java_bytecode_convert_method_lazy( diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h index da9196e6a67..cf3c66b8661 100644 --- a/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/src/java_bytecode/java_bytecode_convert_method_class.h @@ -32,11 +32,13 @@ class java_bytecode_convert_methodt:public messaget symbol_tablet &_symbol_table, message_handlert &_message_handler, size_t _max_array_length, - safe_pointer _lazy_methods): + safe_pointer _lazy_methods, + const java_string_library_preprocesst &_string_preprocess): messaget(_message_handler), symbol_table(_symbol_table), max_array_length(_max_array_length), - lazy_methods(_lazy_methods) + lazy_methods(_lazy_methods), + string_preprocess(_string_preprocess) { } @@ -59,6 +61,7 @@ class java_bytecode_convert_methodt:public messaget irep_idt method_id; irep_idt current_method; typet method_return_type; + java_string_library_preprocesst string_preprocess; public: struct holet diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 69f9f3eb2a4..404ffc95c69 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -511,6 +511,9 @@ bool java_bytecode_languaget::typecheck( symbol_tablet &symbol_table, const std::string &module) { + if(string_refinement_enabled) + string_preprocess.initialize_conversion_table(); + // first convert all for(java_class_loadert::class_mapt::const_iterator c_it=java_class_loader.class_map.begin(); @@ -529,7 +532,7 @@ bool java_bytecode_languaget::typecheck( max_user_array_length, lazy_methods, lazy_methods_mode, - string_refinement_enabled)) + string_preprocess)) return true; } @@ -551,7 +554,8 @@ bool java_bytecode_languaget::typecheck( *method_sig.second.second, symbol_table, get_message_handler(), - max_user_array_length); + max_user_array_length, + string_preprocess); } } // Otherwise our caller is in charge of elaborating methods on demand. @@ -678,7 +682,8 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion( symbol_table, get_message_handler(), max_user_array_length, - safe_pointer::create_non_null(&lazy_methods)); + safe_pointer::create_non_null(&lazy_methods), + string_preprocess); gather_virtual_callsites( symbol_table.lookup(mname).value, virtual_callsites); @@ -788,7 +793,8 @@ void java_bytecode_languaget::convert_lazy_method( *lazy_method_entry.second, symtab, get_message_handler(), - max_user_array_length); + max_user_array_length, + string_preprocess); } /*******************************************************************\ diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index 2da26b71ad6..929cc354518 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "java_class_loader.h" +#include "java_string_library_preprocess.h" #define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5 @@ -99,6 +100,7 @@ class java_bytecode_languaget:public languaget lazy_methodst lazy_methods; lazy_methods_modet lazy_methods_mode; bool string_refinement_enabled; + java_string_library_preprocesst string_preprocess; std::string java_cp_include_files; }; diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 011f2ad2be3..c2c032eecc7 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -132,6 +132,130 @@ class java_object_factoryt /*******************************************************************\ +Function: allocate_dynamic_object + + Inputs: + target_expr - expression to which the necessary memory will be allocated + allocate_type - type of the object allocated + symbol_table - symbol table + loc - location in the source + output_code - code block to which the necessary code is added + symbols_created - created symbols to be declared by the caller + cast_needed - Boolean flags saying where we need to cast the malloc site + + Outputs: Expression representing the malloc site allocated. + + Purpose: Generates code for allocating a dynamic object. + This is used in allocate_object and for allocating strings + in the library preprocessing. + +\*******************************************************************/ + +exprt allocate_dynamic_object( + const exprt &target_expr, + const typet &allocate_type, + symbol_tablet &symbol_table, + const source_locationt &loc, + code_blockt &output_code, + std::vector &symbols_created, + bool cast_needed) +{ + // build size expression + exprt object_size=size_of_expr(allocate_type, namespacet(symbol_table)); + + if(allocate_type.id()!=ID_empty) + { + assert(!object_size.is_nil() && "size of Java objects should be known"); + // malloc expression + exprt malloc_expr=side_effect_exprt(ID_malloc); + malloc_expr.copy_to_operands(object_size); + typet result_type=pointer_typet(allocate_type); + malloc_expr.type()=result_type; + // Create a symbol for the malloc expression so we can initialize + // without having to do it potentially through a double-deref, which + // breaks the to-SSA phase. + symbolt &malloc_sym=new_tmp_symbol( + symbol_table, + loc, + pointer_typet(allocate_type), + "malloc_site"); + symbols_created.push_back(&malloc_sym); + code_assignt assign=code_assignt(malloc_sym.symbol_expr(), malloc_expr); + assign.add_source_location()=loc; + output_code.copy_to_operands(assign); + malloc_expr=malloc_sym.symbol_expr(); + if(cast_needed) + malloc_expr=typecast_exprt(malloc_expr, target_expr.type()); + code_assignt code(target_expr, malloc_expr); + code.add_source_location()=loc; + output_code.copy_to_operands(code); + return malloc_sym.symbol_expr(); + } + else + { + // make null + null_pointer_exprt null_pointer_expr(to_pointer_type(target_expr.type())); + code_assignt code(target_expr, null_pointer_expr); + code.add_source_location()=loc; + output_code.copy_to_operands(code); + return exprt(); + } +} + +/*******************************************************************\ + +Function: allocate_dynamic_object_with_decl + + Inputs: + target_expr - expression to which the necessary memory will be allocated + allocate_type - type of the object allocated + symbol_table - symbol table + loc - location in the source + output_code - code block to which the necessary code is added + cast_needed - Boolean flags saying where we need to cast the malloc site + + Outputs: Expression representing the malloc site allocated. + + Purpose: Generates code for allocating a dynamic object. + This is a static version of allocate_dynamic_object that can + be called from outside java_object_factory and which takes care + of creating the associated declarations. + +\*******************************************************************/ + +exprt allocate_dynamic_object_with_decl( + const exprt &target_expr, + const typet &allocate_type, + symbol_tablet &symbol_table, + const source_locationt &loc, + code_blockt &output_code, + bool cast_needed) +{ + std::vector symbols_created; + + exprt result=allocate_dynamic_object( + target_expr, + allocate_type, + symbol_table, + loc, + output_code, + symbols_created, + cast_needed); + + // Add the following code to output_code for each symbol that's been created: + // ; + for(const symbolt * const symbol_ptr : symbols_created) + { + code_declt decl(symbol_ptr->symbol_expr()); + decl.add_source_location()=loc; + output_code.add(decl); + } + + return result; +} + +/*******************************************************************\ + Function: java_object_factoryt::allocate_object Inputs: @@ -174,47 +298,14 @@ exprt java_object_factoryt::allocate_object( } else { - // build size expression - exprt object_size=size_of_expr(allocate_type, namespacet(symbol_table)); - - if(allocate_type.id()!=ID_empty) - { - assert(!object_size.is_nil() && "size of Java objects should be known"); - // malloc expression - exprt malloc_expr=side_effect_exprt(ID_malloc); - malloc_expr.copy_to_operands(object_size); - typet result_type=pointer_typet(allocate_type); - malloc_expr.type()=result_type; - // Create a symbol for the malloc expression so we can initialize - // without having to do it potentially through a double-deref, which - // breaks the to-SSA phase. - symbolt &malloc_sym=new_tmp_symbol( - symbol_table, - loc, - pointer_typet(allocate_type), - "malloc_site"); - symbols_created.push_back(&malloc_sym); - code_assignt assign=code_assignt(malloc_sym.symbol_expr(), malloc_expr); - code_assignt &malloc_assign=assign; - malloc_assign.add_source_location()=loc; - assignments.copy_to_operands(malloc_assign); - malloc_expr=malloc_sym.symbol_expr(); - if(cast_needed) - malloc_expr=typecast_exprt(malloc_expr, target_expr.type()); - code_assignt code(target_expr, malloc_expr); - code.add_source_location()=loc; - assignments.copy_to_operands(code); - return malloc_sym.symbol_expr(); - } - else - { - // make null - null_pointer_exprt null_pointer_expr(to_pointer_type(target_expr.type())); - code_assignt code(target_expr, null_pointer_expr); - code.add_source_location()=loc; - assignments.copy_to_operands(code); - return exprt(); - } + return allocate_dynamic_object( + target_expr, + allocate_type, + symbol_table, + loc, + assignments, + symbols_created, + cast_needed); } } diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h index d2d2d0d937f..69ab7250ca7 100644 --- a/src/java_bytecode/java_object_factory.h +++ b/src/java_bytecode/java_object_factory.h @@ -40,4 +40,21 @@ void gen_nondet_init( size_t max_nondet_array_length, update_in_placet update_in_place=NO_UPDATE_IN_PLACE); +exprt allocate_dynamic_object( + const exprt &target_expr, + const typet &allocate_type, + symbol_tablet &symbol_table, + const source_locationt &loc, + code_blockt &output_code, + std::vector &symbols_created, + bool cast_needed=false); + +exprt allocate_dynamic_object_with_decl( + const exprt &target_expr, + const typet &allocate_type, + symbol_tablet &symbol_table, + const source_locationt &loc, + code_blockt &output_code, + bool cast_needed=false); + #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp new file mode 100644 index 00000000000..34e5f84bfd7 --- /dev/null +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -0,0 +1,2304 @@ +/*******************************************************************\ + +Module: 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. + +Author: Romain Brenguier + +Date: April 2017 + +\*******************************************************************/ + +#include +#include +#include +#include +#include +#include +#include "java_types.h" +#include "java_object_factory.h" + +#include "java_string_library_preprocess.h" + +/*******************************************************************\ + +Function: java_string_library_preprocesst::java_type_matches_tag + + Inputs: + type - a type + tag - a string + + Output: Boolean telling whether the type is a struct with the given + tag or a symbolic type with the tag prefixed by "java::" + +\*******************************************************************/ + +bool java_string_library_preprocesst::java_type_matches_tag( + const typet &type, const std::string &tag) +{ + if(type.id()==ID_symbol) + { + irep_idt tag_id=to_symbol_type(type).get_identifier(); + return tag_id=="java::"+tag; + } + else if(type.id()==ID_struct) + { + irep_idt tag_id=to_struct_type(type).get_tag(); + return tag_id==tag; + } + return false; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::is_java_string_pointer_type + + Inputs: a type + + Output: Boolean telling whether the type is that of java string pointer + +\*******************************************************************/ + +bool java_string_library_preprocesst::is_java_string_pointer_type( + const typet &type) +{ + if(type.id()==ID_pointer) + { + const pointer_typet &pt=to_pointer_type(type); + const typet &subtype=pt.subtype(); + return is_java_string_type(subtype); + } + return false; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::is_java_string_type + + Inputs: a type + + Output: Boolean telling whether the type is that of java string + +\*******************************************************************/ + +bool java_string_library_preprocesst::is_java_string_type( + const typet &type) +{ + return java_type_matches_tag(type, "java.lang.String"); +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::is_java_string_builder_type + + Inputs: a type + + Output: Boolean telling whether the type is that of java StringBuilder + +\*******************************************************************/ + +bool java_string_library_preprocesst::is_java_string_builder_type( + const typet &type) +{ + return java_type_matches_tag(type, "java.lang.StringBuilder"); +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::is_java_string_builder_pointer_type + + Inputs: a type + + Output: Boolean telling whether the type is that of java StringBuilder + pointers + +\*******************************************************************/ + +bool java_string_library_preprocesst::is_java_string_builder_pointer_type( + const typet &type) +{ + if(type.id()==ID_pointer) + { + const pointer_typet &pt=to_pointer_type(type); + const typet &subtype=pt.subtype(); + return is_java_string_builder_type(subtype); + } + return false; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::is_java_string_buffer_type + + Inputs: a type + + Output: Boolean telling whether the type is that of java StringBuffer + +\*******************************************************************/ + +bool java_string_library_preprocesst::is_java_string_buffer_type( + const typet &type) +{ + return java_type_matches_tag(type, "java.lang.StringBuffer"); +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::is_java_string_buffer_pointer_type + + Inputs: a type + + Output: Boolean telling whether the type is that of java StringBuffer + pointers + +\*******************************************************************/ + +bool java_string_library_preprocesst::is_java_string_buffer_pointer_type( + const typet &type) +{ + if(type.id()==ID_pointer) + { + const pointer_typet &pt=to_pointer_type(type); + const typet &subtype=pt.subtype(); + return is_java_string_buffer_type(subtype); + } + return false; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::is_java_char_sequence_type + + Inputs: a type + + Output: Boolean telling whether the type is that of java char sequence + +\*******************************************************************/ + +bool java_string_library_preprocesst::is_java_char_sequence_type( + const typet &type) +{ + return java_type_matches_tag(type, "java.lang.CharSequence"); +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::is_java_char_sequence_pointer_type + + Inputs: a type + + Output: Boolean telling whether the type is that of a pointer + to a java char sequence + +\*******************************************************************/ + +bool java_string_library_preprocesst::is_java_char_sequence_pointer_type( + const typet &type) +{ + if(type.id()==ID_pointer) + { + const pointer_typet &pt=to_pointer_type(type); + const typet &subtype=pt.subtype(); + return is_java_char_sequence_type(subtype); + } + return false; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::is_java_char_array_type + + Inputs: a type + + Output: Boolean telling whether the type is that of java char array + +\*******************************************************************/ + +bool java_string_library_preprocesst::is_java_char_array_type( + const typet &type) +{ + return java_type_matches_tag(type, "array[char]"); +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::is_java_char_array_pointer_type + + Inputs: a type + + Outputs: Boolean telling whether the type is that of a pointer + to a java char array + +\*******************************************************************/ + +bool java_string_library_preprocesst::is_java_char_array_pointer_type( + const typet &type) +{ + if(type.id()==ID_pointer) + { + const pointer_typet &pt=to_pointer_type(type); + const typet &subtype=pt.subtype(); + return is_java_char_array_type(subtype); + } + return false; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::string_data_type + + Inputs: + symbol_table - a symbol_table containing an entry for java Strings + + Output: the type of data fields in java Strings. + +\*******************************************************************/ + +typet string_data_type(symbol_tablet symbol_table) +{ + symbolt sym=symbol_table.lookup("java::java.lang.String"); + typet concrete_type=sym.type; + // TODO: Check that this is indeed the 'length' field. + typet data_type=to_struct_type(concrete_type).components()[2].type(); + return data_type; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::string_length_type + + Outputs: the type of the length field in java Strings. + +\*******************************************************************/ + +typet string_length_type() +{ + return java_int_type(); +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::add_string_type + + Inputs: + class_name - a name for the class such as "java.lang.String" + symbol_table - symbol table to which the class will be added + + Purpose: Add to the symbol table type declaration for a String-like + Java class. + +\*******************************************************************/ + +void java_string_library_preprocesst::add_string_type( + const irep_idt &class_name, symbol_tablet &symbol_table) +{ + class_typet string_type; + string_type.set_tag(class_name); + string_type.components().resize(3); + string_type.components()[0].set_name("@java.lang.Object"); + string_type.components()[0].set_pretty_name("@java.lang.Object"); + string_type.components()[0].type()=symbol_typet("java::java.lang.Object"); + string_type.components()[1].set_name("length"); + string_type.components()[1].set_pretty_name("length"); + string_type.components()[1].type()=string_length_type(); + string_type.components()[2].set_name("data"); + string_type.components()[2].set_pretty_name("data"); + // Use a pointer-to-unbounded-array instead of a pointer-to-char. + // Saves some casting in the string refinement algorithm but may + // be unnecessary. + string_type.components()[2].type()=pointer_typet( + array_typet(java_char_type(), infinity_exprt(string_length_type()))); + string_type.add_base(symbol_typet("java::java.lang.Object")); + + symbolt string_symbol; + string_symbol.name="java::"+id2string(class_name); + string_symbol.base_name=id2string(class_name); + string_symbol.pretty_name=id2string(class_name); + string_symbol.type=string_type; + string_symbol.is_type=true; + + symbol_table.add(string_symbol); +} + +/*******************************************************************\ + +Function: fresh_array + + Inputs: + type - an array type + location - a location in the program + symbol_table - symbol table + + Output: a new symbol + + Purpose: add a symbol in the table with static lifetime and name + containing `cprover_string_array` and given type + +\*******************************************************************/ + +symbol_exprt java_string_library_preprocesst::fresh_array( + const typet &type, + const source_locationt &location, + symbol_tablet &symbol_table) +{ + symbolt array_symbol=get_fresh_aux_symbol( + type, + "cprover_string_array", + "cprover_string_array", + location, + ID_java, + symbol_table); + array_symbol.is_static_lifetime=true; + return array_symbol.symbol_expr(); +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::declare_function + + Inputs: + function_name - a name + type - a type + symbol_table - symbol table + + Purpose: declare a function with the given name and type + +\*******************************************************************/ + +void java_string_library_preprocesst::declare_function( + irep_idt function_name, const typet &type, symbol_tablet &symbol_table) +{ + auxiliary_symbolt func_symbol; + func_symbol.base_name=function_name; + func_symbol.pretty_name=function_name; + func_symbol.is_static_lifetime=false; + func_symbol.mode=ID_java; + func_symbol.name=function_name; + func_symbol.type=type; + symbol_table.add(func_symbol); +} + +/*******************************************************************\ + +Function: string_refine_preprocesst::process_arguments + + Inputs: + 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 + + Output: a list of expressions + + Purpose: calls string_refine_preprocesst::process_operands with a + list of parameters. + +\*******************************************************************/ + +exprt::operandst java_string_library_preprocesst::process_parameters( + const code_typet::parameterst ¶ms, + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &init_code) +{ + exprt::operandst ops; + for(const auto &p : params) + { + symbol_exprt sym(p.get_identifier(), p.type()); + ops.push_back(sym); + } + return process_operands(ops, loc, symbol_table, init_code); +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::process_single_operand + + Inputs: + processed_ops - the list of processed operands to populate + op_to_process - 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 + + Purpose: Creates a string_exprt from the input exprt and adds it to + processed_ops + +\*******************************************************************/ + +void java_string_library_preprocesst::process_single_operand( + exprt::operandst &processed_ops, + const exprt &op_to_process, + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &init_code) +{ + member_exprt length( + op_to_process, "length", string_length_type()); + member_exprt data(op_to_process, "data", string_data_type(symbol_table)); + dereference_exprt deref_data(data, data.type().subtype()); + string_exprt string_expr=fresh_string_expr(loc, symbol_table, init_code); + exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, init_code); + init_code.add(code_declt(string_expr_sym)); + init_code.add(code_assignt(string_expr.length(), length)); + init_code.add( + code_assignt(string_expr.content(), deref_data)); + init_code.add(code_assignt(string_expr_sym, string_expr)); + processed_ops.push_back(string_expr); +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::process_operands + + Inputs: + 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 + + Output: a list of expressions + + Purpose: 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. + +\*******************************************************************/ + +exprt::operandst java_string_library_preprocesst::process_operands( + const exprt::operandst &operands, + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &init_code) +{ + exprt::operandst ops; + for(const auto &p : operands) + { + if(implements_java_char_sequence(p.type())) + { + dereference_exprt deref(p, to_pointer_type(p.type()).subtype()); + process_single_operand(ops, deref, loc, symbol_table, init_code); + } + else if(is_java_char_array_pointer_type(p.type())) + { + ops.push_back(replace_char_array(p, loc, symbol_table, init_code)); + } + else + { + ops.push_back(p); + } + } + return ops; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::process_equals_function_operands + + Inputs: + 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 + + Output: a list of expressions + + Purpose: 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. + +\*******************************************************************/ + +exprt::operandst + java_string_library_preprocesst::process_equals_function_operands( + const exprt::operandst &operands, + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &init_code) +{ + assert(operands.size()==2); + exprt::operandst ops; + exprt op0=operands[0]; + exprt op1=operands[1]; + + assert(implements_java_char_sequence(op0.type())); + dereference_exprt deref0(op0, to_pointer_type(op0.type()).subtype()); + process_single_operand(ops, deref0, loc, symbol_table, init_code); + + // TODO: Manage the case where we have a non-String Object (this should + // probably be handled upstream. At any rate, the following code should be + // protected with assertions on the type of op1. + typecast_exprt tcast(op1, to_pointer_type(op0.type())); + dereference_exprt deref1(tcast, to_pointer_type(op0.type()).subtype()); + process_single_operand(ops, deref1, loc, symbol_table, init_code); + return ops; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::get_data_type + + Inputs: + type - a type containing a "data" component + symbol_table - symbol table + + Output: type of the "data" component + + Purpose: Finds the type of the data component + +\*******************************************************************/ + +typet java_string_library_preprocesst::get_data_type( + const typet &type, const symbol_tablet &symbol_table) +{ + if(type.id()==ID_symbol) + { + symbolt sym=symbol_table.lookup(to_symbol_type(type).get_identifier()); + assert(sym.type.id()!=ID_symbol); + return get_data_type(sym.type, symbol_table); + } + else + { + assert(type.id()==ID_struct); + const struct_typet &struct_type=to_struct_type(type); + for(auto component : struct_type.components()) + if(component.get_name()=="data") + return component.type(); + assert(false && "type does not contain data component"); + } +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::get_length_type + + Inputs: + type - a type containing a "length" component + symbol_table - symbol table + + Output: type of the "length" component + + Purpose: Finds the type of the length component + +\*******************************************************************/ + +typet java_string_library_preprocesst::get_length_type( + const typet &type, const symbol_tablet &symbol_table) +{ + if(type.id()==ID_symbol) + { + symbolt sym=symbol_table.lookup(to_symbol_type(type).get_identifier()); + assert(sym.type.id()!=ID_symbol); + return get_length_type(sym.type, symbol_table); + } + else + { + assert(type.id()==ID_struct); + const struct_typet &struct_type=to_struct_type(type); + for(auto component : struct_type.components()) + if(component.get_name()=="length") + return component.type(); + assert(false && "type does not contain length component"); + } +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::get_length + + Inputs: + expr - an expression of structured type with length component + symbol_table - symbol table + + Output: expression representing the "length" member + + Purpose: access length member + +\*******************************************************************/ + +exprt java_string_library_preprocesst::get_length( + const exprt &expr, const symbol_tablet &symbol_table) +{ + return member_exprt( + expr, "length", get_length_type(expr.type(), symbol_table)); +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::get_data + + Inputs: + expr - an expression of structured type with length component + symbol_table - symbol table + + Output: expression representing the "data" member + + Purpose: access data member + +\*******************************************************************/ + +exprt java_string_library_preprocesst::get_data( + const exprt &expr, const symbol_tablet &symbol_table) +{ + return member_exprt(expr, "data", get_data_type(expr.type(), symbol_table)); +} + +/*******************************************************************\ + +Function: string_refine_preprocesst::replace_char_array + + Inputs: + 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 + + Output: a string expression + + Purpose: we declare a new `cprover_string` whose contents is deduced + from the char array. + +\*******************************************************************/ + +string_exprt java_string_library_preprocesst::replace_char_array( + const exprt &array_pointer, + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &code) +{ + refined_string_typet ref_type=refined_string_type; + dereference_exprt array(array_pointer, array_pointer.type().subtype()); + exprt array_data=get_data(array, symbol_table); + // `deref_array` is *(array_pointer->data)` + const typet &content_type=ref_type.get_content_type(); + dereference_exprt deref_array(array_data, array_data.type().subtype()); + + // lhs_deref <- convert_pointer_to_char_array(*(array_pointer->data)) + symbolt sym_char_array=get_fresh_aux_symbol( + content_type, "char_array", "char_array", loc, ID_java, symbol_table); + symbol_exprt char_array=sym_char_array.symbol_expr(); + code.add(code_assign_function_application( + char_array, + ID_cprover_string_array_of_char_pointer_func, + {deref_array}, + symbol_table)); + + // string_expr is `{ rhs->length; string_array }` + string_exprt string_expr( + get_length(array, symbol_table), char_array, refined_string_type); + // string_expr_sym <- { rhs->length; string_array } + symbol_exprt string_expr_sym= + fresh_string(refined_string_type, loc, symbol_table); + code.add(code_assignt(string_expr_sym, string_expr)); + + return string_expr; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::fresh_string + + Inputs: + type - a type for refined strings + loc - a location in the program + symbol_table - symbol table + + Output: a new symbol + + Purpose: add a symbol with static lifetime and name containing + `cprover_string` and given type + +\*******************************************************************/ + +symbol_exprt java_string_library_preprocesst::fresh_string( + const typet &type, const source_locationt &loc, symbol_tablet &symbol_table) +{ + symbolt string_symbol=get_fresh_aux_symbol( + type, "cprover_string", "cprover_string", loc, ID_java, symbol_table); + string_symbol.is_static_lifetime=true; + return string_symbol.symbol_expr(); +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::fresh_string_expr + + Inputs: + loc - a location in the program + symbol_table - symbol table + code - code block to which allocation instruction will be added + + Output: a new string_expr + + Purpose: add symbols with prefix cprover_string_length and + cprover_string_data and construct a string_expr from them. + +\*******************************************************************/ + +string_exprt java_string_library_preprocesst::fresh_string_expr( + const source_locationt &loc, symbol_tablet &symbol_table, code_blockt &code) +{ + refined_string_typet type=refined_string_type; + symbolt sym_length=get_fresh_aux_symbol( + type.get_index_type(), + "cprover_string_length", + "cprover_string_length", + loc, + ID_java, + symbol_table); + symbol_exprt length_field=sym_length.symbol_expr(); + symbol_exprt content_field=fresh_array( + type.get_content_type(), loc, symbol_table); + string_exprt str(length_field, content_field, type); + code.add(code_declt(length_field)); + code.add(code_declt(content_field)); + return str; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::fresh_string_expr_symbol + + Inputs: + loc - a location in the program + symbol_table - symbol table + code - code block to which allocation instruction will be added + + Output: a new expression of refined string type + + Purpose: add symbols with prefix cprover_string_length and + cprover_string_data and construct a string_expr from them. + +\*******************************************************************/ + +exprt java_string_library_preprocesst::fresh_string_expr_symbol( + const source_locationt &loc, symbol_tablet &symbol_table, code_blockt &code) +{ + symbolt sym=get_fresh_aux_symbol( + refined_string_type, + "cprover_string", + "cprover_string", + loc, + ID_java, + symbol_table); + code.add(code_declt(sym.symbol_expr())); + return sym.symbol_expr(); +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::allocate_fresh_string + + Inputs: + type - a type for string + loc - a location in the program + symbol_table - symbol table + code - code block to which allocation instruction will be added + + Output: a new string + + Purpose: declare a new String and allocate it + +\*******************************************************************/ + +exprt java_string_library_preprocesst::allocate_fresh_string( + const typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &code) +{ + exprt str=fresh_string(type, loc, symbol_table); + code.add(code_declt(str)); + (void) allocate_dynamic_object_with_decl( + str, str.type().subtype(), symbol_table, loc, code, false); + return str; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::allocate_fresh_array + + Inputs: + type - a type for string + loc - a location in the program + symbol_table - symbol table + code - code block to which allocation instruction will be added + + Output: a new array + + Purpose: declare a new character array and allocate it + +\*******************************************************************/ + +exprt java_string_library_preprocesst::allocate_fresh_array( + const typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &code) +{ + exprt array=fresh_array(type, loc, symbol_table); + code.add(code_declt(array)); + (void) allocate_dynamic_object_with_decl( + array, array.type().subtype(), symbol_table, loc, code, false); + return array; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::make_function_application + + Inputs: + function_name - the name of the function + arguments - a list of arguments + type - return type of the function + symbol_table - a symbol table + + Output: a function application representing: function_name(arguments) + +\*******************************************************************/ + +exprt java_string_library_preprocesst::make_function_application( + const irep_idt &function_name, + const exprt::operandst &arguments, + const typet &type, + symbol_tablet &symbol_table) +{ + // Names of function to call + std::string fun_name=id2string(function_name); + + // Declaring the function + declare_function(fun_name, type, symbol_table); + + // Function application + function_application_exprt call(symbol_exprt(fun_name), type); + call.arguments()=arguments; + return call; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::code_assign_function_application + + Inputs: + lhs - an expression + function_name - the name of the function + arguments - a list of arguments + symbol_table - a symbol table + + Output: the following code: + > lhs=function_name_length(arguments) + + Purpose: assign the result of a function call + +\*******************************************************************/ + +codet java_string_library_preprocesst::code_assign_function_application( + const exprt &lhs, + const irep_idt &function_name, + const exprt::operandst &arguments, + symbol_tablet &symbol_table) +{ + exprt fun_app=make_function_application( + function_name, arguments, lhs.type(), symbol_table); + return code_assignt(lhs, fun_app); +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::code_return_function_application + + Inputs: + function_name - the name of the function + arguments - a list of arguments + type - the return type + symbol_table - a symbol table + + Output: the following code: + > return function_name_length(arguments) + + Purpose: return the result of a function call + +\*******************************************************************/ + +codet java_string_library_preprocesst::code_return_function_application( + const irep_idt &function_name, + const exprt::operandst &arguments, + const typet &type, + symbol_tablet &symbol_table) +{ + exprt fun_app=make_function_application( + function_name, arguments, type, symbol_table); + return code_returnt(fun_app); +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::code_assign_function_to_string_expr + + Inputs: + string_expr - a string expression + function_name - the name of the function + arguments - arguments of the function + symbol_table - symbol table + + Output: return the following code: + > str.length <- function_name_length(arguments) + > str.data <- function_name_data(arguments) + +\*******************************************************************/ + +codet java_string_library_preprocesst::code_assign_function_to_string_expr( + const string_exprt &string_expr, + const irep_idt &function_name, + const exprt::operandst &arguments, + symbol_tablet &symbol_table) +{ + // Names of function to call + std::string fun_name_length=id2string(function_name)+"_length"; + std::string fun_name_data=id2string(function_name)+"_data"; + + // Assignments + codet assign_fun_length=code_assign_function_application( + string_expr.length(), fun_name_length, arguments, symbol_table); + codet assign_fun_data=code_assign_function_application( + string_expr.content(), fun_name_data, arguments, symbol_table); + + return code_blockt({assign_fun_length, assign_fun_data}); +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::string_expr_of_function_application + + Inputs: + function_name - the name of the function + arguments - arguments of the function + loc - a location in the program + symbol_table - symbol table + code - code block in which we add instructions + + Output: return a string expr str and add the following code: + > array str.data + > str.length <- function_name_length(arguments) + > str.data <- function_name_data(arguments) + +\*******************************************************************/ + +string_exprt java_string_library_preprocesst:: + string_expr_of_function_application( + const irep_idt &function_name, + const exprt::operandst &arguments, + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &code) +{ + string_exprt string_expr=fresh_string_expr(loc, symbol_table, code); + code.add(code_assign_function_to_string_expr( + string_expr, function_name, arguments, symbol_table)); + return string_expr; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst:: + code_assign_string_expr_to_java_string + + Inputs: + lhs - an expression representing a java string + rhs - a string expression + symbol_table - symbol table + + Output: return the following code: + > lhs->length=rhs.length + > lhs->data=&rhs.data + +\*******************************************************************/ + +codet java_string_library_preprocesst::code_assign_string_expr_to_java_string( + const exprt &lhs, + const string_exprt &rhs, + symbol_tablet &symbol_table) +{ + assert(implements_java_char_sequence(lhs.type())); + dereference_exprt deref(lhs, lhs.type().subtype()); + + // Fields of the string object + exprt lhs_length=get_length(deref, symbol_table); + exprt lhs_data=get_data(deref, symbol_table); + + // Assignments + code_blockt code; + code.add(code_assignt(lhs_length, rhs.length())); + code.add( + code_assignt(lhs_data, address_of_exprt(rhs.content()))); + return code; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst:: + code_assign_string_expr_to_new_java_string + + Inputs: + lhs - an expression representing a java string + rhs - a string expression + loc - a location in the program + symbol_table - symbol table + + Output: return the following code: + > lhs->length=rhs.length + > lhs->data=&rhs.data + +\*******************************************************************/ + +codet java_string_library_preprocesst:: + code_assign_string_expr_to_new_java_string( + const exprt &lhs, + const string_exprt &rhs, + const source_locationt &loc, + symbol_tablet &symbol_table) +{ + assert(implements_java_char_sequence(lhs.type())); + dereference_exprt deref(lhs, lhs.type().subtype()); + + // Fields of the string object + exprt lhs_length=get_length(deref, symbol_table); + exprt lhs_data=get_data(deref, symbol_table); + + // Assignments + code_blockt code; + // new array <- malloc(char[]) + exprt new_array=allocate_fresh_array( + get_data_type(deref.type(), symbol_table), loc, symbol_table, code); + code.add(code_assignt( + dereference_exprt(new_array, new_array.type().subtype()), rhs.content())); + code.add(code_assignt(lhs_length, rhs.length())); + code.add(code_assignt(lhs_data, new_array)); + return code; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst:: + code_assign_java_string_to_string_expr + + Inputs: + lhs - a string expression + rhs - an expression representing a java string + symbol_table - symbol table + + Output: return the following code: + > lhs.length=rhs->length + > lhs.data=*(rhs->data) + +\*******************************************************************/ + +codet java_string_library_preprocesst::code_assign_java_string_to_string_expr( + const string_exprt &lhs, const exprt &rhs, symbol_tablet &symbol_table) +{ + assert(implements_java_char_sequence(rhs.type())); + + typet deref_type; + if(rhs.type().subtype().id()==ID_symbol) + deref_type=symbol_table.lookup( + to_symbol_type(rhs.type().subtype()).get_identifier()).type; + else + deref_type=rhs.type().subtype(); + + dereference_exprt deref(rhs, deref_type); + + // Fields of the string object + exprt rhs_length=get_length(deref, symbol_table); + exprt member_data=get_data(deref, symbol_table); + dereference_exprt rhs_data(member_data, member_data.type().subtype()); + + // Assignments + code_blockt code; + code.add(code_assignt(lhs.length(), rhs_length)); + code.add(code_assignt(lhs.content(), rhs_data)); + return code; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst:: + code_assign_string_literal_to_string_expr + + Inputs: + lhs - an expression representing a java string + tmp_string - a temporary string to hold the literal + s - the literal to be assigned + symbol_table - symbol table + + Output: return the following code: + > tmp_string = "s" + > lhs = (string_expr) tmp_string + +\*******************************************************************/ + +codet java_string_library_preprocesst:: + code_assign_string_literal_to_string_expr( + const string_exprt &lhs, + const exprt &tmp_string, + const std::string &s, + symbol_tablet &symbol_table) +{ + code_blockt code; + code.add(code_assignt(tmp_string, string_literal(s))); + code.add(code_assign_java_string_to_string_expr( + lhs, tmp_string, symbol_table)); + return code; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst:: + make_string_builder_append_object_code + + Inputs: + type - type of the function called + loc - location in the program + symbol_table - symbol table + + Outputs: code for the StringBuilder.append(Object) function: + > string1 = arguments[1].toString() + > string_expr1 = string_to_string_expr(string1) + > string_expr2 = concat(this, string_expr1) + > this = string_expr_to_string(string_expr2) + > return this + +\*******************************************************************/ + +codet java_string_library_preprocesst::make_string_builder_append_object_code( + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table) +{ + code_typet::parameterst params=type.parameters(); + assert(params.size()==1); + exprt this_obj=symbol_exprt(params[0].get_identifier(), params[0].type()); + + // Code to be returned + code_blockt code; + + // String expression that will hold the result + string_exprt string_expr1=fresh_string_expr(loc, symbol_table, code); + + exprt::operandst arguments=process_parameters( + type.parameters(), loc, symbol_table, code); + assert(arguments.size()==2); + + // > string1 = arguments[1].toString() + exprt string1=fresh_string(this_obj.type(), loc, symbol_table); + code_function_callt fun_call; + fun_call.lhs()=string1; + // TODO: we should look in the symbol table for such a symbol + fun_call.function()=symbol_exprt( + "java::java.lang.Object.toString:()Ljava/lang/String;"); + fun_call.arguments().push_back(arguments[1]); + code_typet fun_type; + fun_type.return_type()=string1.type(); + fun_call.function().type()=fun_type; + code.add(fun_call); + + // > string_expr1 = string_to_string_expr(string1) + code.add(code_assign_java_string_to_string_expr( + string_expr1, string1, symbol_table)); + + // > string_expr2 = concat(this, string1) + exprt::operandst concat_arguments(arguments); + concat_arguments[1]=string_expr1; + string_exprt string_expr2=string_expr_of_function_application( + ID_cprover_string_concat_func, concat_arguments, loc, symbol_table, code); + + // > this = string_expr + code.add(code_assign_string_expr_to_java_string( + this_obj, string_expr2, symbol_table)); + + // > return this + code.add(code_returnt(this_obj)); + + return code; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::make_equals_code + + Inputs: + type - type of the function call + loc - location in the program_invocation_name + symbol_table - symbol table + + Outputs: Code corresponding to: + > string_expr1 = {this->length; *this->data} + > string_expr2 = {arg->length; *arg->data} + > return cprover_string_equal(string_expr1, string_expr2) + + Purpose: Used to provide code for the Java String.equals(Object) function. + +\*******************************************************************/ + +codet java_string_library_preprocesst::make_equals_function_code( + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table) +{ + // TODO: Code should return false if Object is not String. + code_blockt code; + exprt::operandst ops; + for(const auto &p : type.parameters()) + { + symbol_exprt sym(p.get_identifier(), p.type()); + ops.push_back(sym); + } + exprt::operandst args=process_equals_function_operands( + ops, loc, symbol_table, code); + code.add(code_return_function_application( + ID_cprover_string_equal_func, args, type.return_type(), symbol_table)); + return code; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst:: + make_string_builder_append_float_code + + Inputs: + type - type of the function call + loc - location in the program_invocation_name + symbol_table - symbol table + + Outputs: Code corresponding to: + > string1 = arguments[1].toString() + > string_expr1 = string_to_string_expr(string1) + > string_expr2 = concat(this, string_expr1) + > this = string_expr_to_string(string_expr2) + > return this + + Purpose: Used to provide code for the Java StringBuilder.append(F) + function. + +\*******************************************************************/ + +codet java_string_library_preprocesst::make_string_builder_append_float_code( + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table) +{ + code_typet::parameterst params=type.parameters(); + assert(params.size()==1); + exprt this_obj=symbol_exprt(params[0].get_identifier(), params[0].type()); + + // Getting types + typet length_type=string_length_type(); + + // Code to be returned + code_blockt code; + + // String expression that will hold the result + refined_string_typet ref_type(length_type, java_char_type()); + string_exprt string_expr1=fresh_string_expr(loc, symbol_table, code); + + exprt::operandst arguments=process_parameters( + type.parameters(), loc, symbol_table, code); + assert(arguments.size()==2); + + // > string1 = arguments[1].toString() + exprt string1=fresh_string(this_obj.type(), loc, symbol_table); + code_function_callt fun_call; + fun_call.lhs()=string1; + // TODO: we should look in the symbol table for such a symbol + fun_call.function()=symbol_exprt( + "java::java.lang.Float.toString:()Ljava/lang/String;"); + fun_call.arguments().push_back(arguments[1]); + code_typet fun_type; + fun_type.return_type()=string1.type(); + fun_call.function().type()=fun_type; + code.add(fun_call); + + // > string_expr1 = string_to_string_expr(string1) + code.add(code_assign_java_string_to_string_expr( + string_expr1, string1, symbol_table)); + + // > string_expr2 = concat(this, string1) + exprt::operandst concat_arguments(arguments); + concat_arguments[1]=string_expr1; + + string_exprt string_expr2=string_expr_of_function_application( + ID_cprover_string_concat_func, concat_arguments, loc, symbol_table, code); + + // > this = string_expr + code.add(code_assign_string_expr_to_java_string( + this_obj, string_expr2, symbol_table)); + + // > return this + code.add(code_returnt(this_obj)); + + return code; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::string_literal + + Inputs: + s - a string + + Outputs: an expression representing a Java string literal with the + given content. + + Purpose: construct a Java string literal from a constant string value + +\*******************************************************************/ + +exprt java_string_library_preprocesst::string_literal(const std::string &s) +{ + exprt string_literal(ID_java_string_literal); + string_literal.set(ID_value, s); + return string_literal; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::make_float_to_string_code + + Inputs: + type - type of the function call + loc - location in the program_invocation_name + symbol_table - symbol table + + Outputs: Code corresponding to: + > String * str; + > str = MALLOC(String); + > String * tmp_string; + > int string_expr_length; + > char[] string_expr_content; + > CPROVER_string string_expr_sym; + > if arguments[1]==NaN + > then {tmp_string="NaN"; string_expr=(string_expr)tmp_string} + > if arguments[1]==Infinity + > then {tmp_string="Infinity"; string_expr=(string_expr)tmp_string} + > if 1e-3 then string_expr=cprover_float_to_string(arguments[1]) + > else string_expr=cprover_float_to_scientific_notation_string(arg[1]) + > string_expr_sym=string_expr; + > str=(String*) string_expr; + > return str; + + Purpose: Provide code for the Float.toString(F) function. + +\*******************************************************************/ + +codet java_string_library_preprocesst::make_float_to_string_code( + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table) +{ + // Getting the argument + code_typet::parameterst params=type.parameters(); + assert(params.size()==1 && "wrong number of parameters in Float.toString"); + exprt arg=symbol_exprt(params[0].get_identifier(), params[0].type()); + + // Holder for output code + code_blockt code; + + // Declaring and allocating String * str + exprt str=allocate_fresh_string(type.return_type(), loc, symbol_table, code); + exprt tmp_string=fresh_string(type.return_type(), loc, symbol_table); + + // Declaring CPROVER_string string_expr + string_exprt string_expr=fresh_string_expr(loc, symbol_table, code); + exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, code); + + // List of the different cases + std::vector case_list; + + // First case in the list is the default + code_ifthenelset case_sci_notation; + ieee_float_spect float_spec=ieee_float_spect::single_precision(); + // Subcase of 0.0 + // TODO: case of -0.0 + ieee_floatt zero_float(float_spec); + zero_float.from_float(0.0); + constant_exprt zero=zero_float.to_expr(); + case_sci_notation.cond()=ieee_float_equal_exprt(arg, zero); + case_sci_notation.then_case()=code_assign_string_literal_to_string_expr( + string_expr, tmp_string, "0.0", symbol_table); + + // Subcase of computerized scientific notation + case_sci_notation.else_case()=code_assign_function_to_string_expr( + string_expr, ID_cprover_string_of_float_func, {arg}, symbol_table); + case_list.push_back(case_sci_notation); + + // Case of NaN + code_ifthenelset case_nan; + case_nan.cond()=isnan_exprt(arg); + case_nan.then_case()=code_assign_string_literal_to_string_expr( + string_expr, tmp_string, "NaN", symbol_table); + case_list.push_back(case_nan); + + // Case of Infinity + code_ifthenelset case_infinity; + code_ifthenelset case_minus_infinity; + + case_infinity.cond()=isinf_exprt(arg); + // Case -Infinity + exprt isneg=extractbit_exprt(arg, float_spec.width()-1); + case_minus_infinity.cond()=isneg; + case_minus_infinity.then_case()=code_assign_string_literal_to_string_expr( + string_expr, tmp_string, "-Infinity", symbol_table); + case_minus_infinity.else_case()=code_assign_string_literal_to_string_expr( + string_expr, tmp_string, "Infinity", symbol_table); + case_infinity.then_case()=case_minus_infinity; + case_list.push_back(case_infinity); + + // Case of simple notation + code_ifthenelset case_simple_notation; + + ieee_floatt bound_inf_float(float_spec); + ieee_floatt bound_sup_float(float_spec); + bound_inf_float.from_float(1e-3); + bound_sup_float.from_float(1e7); + constant_exprt bound_inf=bound_inf_float.to_expr(); + constant_exprt bound_sup=bound_sup_float.to_expr(); + + and_exprt is_simple_float( + binary_relation_exprt(arg, ID_ge, bound_inf), + binary_relation_exprt(arg, ID_lt, bound_sup)); + case_simple_notation.cond()=is_simple_float; + case_simple_notation.then_case()=code_assign_function_to_string_expr( + string_expr, ID_cprover_string_of_float_func, {arg}, symbol_table); + case_list.push_back(case_simple_notation); + + // Combining all cases + for(std::size_t i=1; i(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}; + + Purpose: Generate the goto code for string initialization. + +\*******************************************************************/ + +codet java_string_library_preprocesst::make_init_function_from_call( + const irep_idt &function_name, + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table, + bool ignore_first_arg) +{ + code_typet::parameterst params=type.parameters(); + + // The first parameter is the object to be initialized + assert(!params.empty()); + exprt arg_this=symbol_exprt(params[0].get_identifier(), params[0].type()); + if(ignore_first_arg) + params.erase(params.begin()); + + // Holder for output code + code_blockt code; + + // Processing parameters + exprt::operandst args=process_parameters(params, loc, symbol_table, code); + + // string_expr <- function(arg1) + string_exprt string_expr=string_expr_of_function_application( + function_name, args, loc, symbol_table, code); + + // arg_this <- string_expr + code.add(code_assign_string_expr_to_new_java_string( + arg_this, string_expr, loc, symbol_table)); + + // string_expr_sym <- {string_expr.length, string_expr.content} + exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, code); + code.add(code_assignt(string_expr_sym, string_expr)); + + return code; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst:: + make_assign_and_return_function_from_call + + Inputs: + 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 + + Outputs: Code calling function with the given function name. + + Purpose: Call a cprover internal function, assign the result to + object `this` and return it. + +\*******************************************************************/ + +codet java_string_library_preprocesst:: + make_assign_and_return_function_from_call( + const irep_idt &function_name, + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table) +{ + // This is similar to assign functions except we return a pointer to `this` + code_blockt code; + code.add(make_assign_function_from_call( + function_name, type, loc, symbol_table)); + code_typet::parameterst params=type.parameters(); + assert(!params.empty()); + exprt arg_this=symbol_exprt(params[0].get_identifier(), params[0].type()); + code.add(code_returnt(arg_this)); + return code; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::make_assign_function_from_call + + Inputs: + 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 + + Outputs: Code assigning result of a call to the function with given + function name. + + Purpose: Call a cprover internal function and assign the result to + object `this`. + +\*******************************************************************/ + +codet java_string_library_preprocesst::make_assign_function_from_call( + const irep_idt &function_name, + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table) +{ + // This is similar to initialization function except we do not ignore + // the first argument + codet code=make_init_function_from_call( + function_name, type, loc, symbol_table, false); + return code; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::make_string_to_char_array_code + + Inputs: + type - type of the function called + loc - location in the source + symbol_table - the symbol table + + Outputs: Code corresponding to + > return_tmp0 = malloc(array[char]); + > return_tmp0->data=&((s->data)[0]) + > return_tmp0->length=s->length + + Purpose: Used to provide our own implementation of the + java.lang.String.toCharArray:()[C function. + +\*******************************************************************/ + +codet java_string_library_preprocesst::make_string_to_char_array_code( + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table) +{ + code_blockt code; + assert(!type.parameters().empty()); + const code_typet::parametert &p=type.parameters()[0]; + symbol_exprt string_argument(p.get_identifier(), p.type()); + assert(implements_java_char_sequence(string_argument.type())); + dereference_exprt deref(string_argument, string_argument.type().subtype()); + + // lhs <- malloc(array[char]) + exprt lhs=fresh_array(type.return_type(), loc, symbol_table); + allocate_dynamic_object_with_decl( + lhs, lhs.type().subtype(), symbol_table, loc, code); + + // first_element_address is `&((string_argument->data)[0])` + exprt data=get_data(deref, symbol_table); + dereference_exprt deref_data(data, data.type().subtype()); + exprt first_index=from_integer(0, string_length_type()); + index_exprt first_element(deref_data, first_index, java_char_type()); + address_of_exprt first_element_address(first_element); + + // lhs->data <- &((string_argument->data)[0]) + dereference_exprt deref_lhs(lhs, lhs.type().subtype()); + exprt lhs_data=get_data(deref_lhs, symbol_table); + code.add(code_assignt(lhs_data, first_element_address)); + + // lhs->length <- s->length + exprt rhs_length=get_length(deref, symbol_table); + exprt lhs_length=get_length(deref_lhs, symbol_table); + code.add(code_assignt(lhs_length, rhs_length)); + + // return lhs + code.add(code_returnt(lhs)); + return code; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::make_function_from_call + + Inputs: + function_name - name of the function to be called + type - type of the function + loc - location in the source + symbol_table - symbol table + + Outputs: Code corresponding to: + > return function_name(args); + + Purpose: Provide code for a function that calls a function from the + solver and simply returns it. + +\*******************************************************************/ + +codet java_string_library_preprocesst::make_function_from_call( + const irep_idt &function_name, + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table) +{ + code_blockt code; + exprt::operandst args=process_parameters( + type.parameters(), loc, symbol_table, code); + code.add(code_return_function_application( + function_name, args, type.return_type(), symbol_table)); + return code; +} + +/*******************************************************************\ + +Function: + java_string_library_preprocesst::make_string_returning_function_from_call + + Inputs: + function_name - name of the function to be called + type - type of the function + loc - location in the source + symbol_table - symbol table + + Outputs: Code corresponding to: + > string_expr = function_name(args) + > string = string_expr_to_string(string) + > return string + + Purpose: Provide code for a function that calls a function from the + solver and return the string_expr result as a Java string. + +\*******************************************************************/ + +codet java_string_library_preprocesst:: + make_string_returning_function_from_call( + const irep_idt &function_name, + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table) +{ + // Code for the output + code_blockt code; + + // Calling the function + exprt::operandst arguments=process_parameters( + type.parameters(), loc, symbol_table, code); + + // String expression that will hold the result + string_exprt string_expr=string_expr_of_function_application( + function_name, arguments, loc, symbol_table, code); + + // Assigning string_expr to symbol for keeping track of it + exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, code); + code.add(code_assignt(string_expr_sym, string_expr)); + + // Assigning to string + exprt str=allocate_fresh_string(type.return_type(), loc, symbol_table, code); + code.add(code_assign_string_expr_to_new_java_string( + str, string_expr, loc, symbol_table)); + + // Return value + code.add(code_returnt(str)); + return code; +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::code_for_function + + Inputs: + function_id - name of the function + type - its type + loc - location in the program + symbol_table - a symbol table + + Outputs: Code for the body of the String functions if they are part + of the supported String functions, nil_exprt otherwise. + + Purpose: Should be called to provide code for string functions that + are used in the code but for which no implementation is + provided. + +\*******************************************************************/ + +exprt java_string_library_preprocesst::code_for_function( + const irep_idt &function_id, + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table) +{ + auto it_id=cprover_equivalent_to_java_function.find(function_id); + if(it_id!=cprover_equivalent_to_java_function.end()) + return make_function_from_call(it_id->second, type, loc, symbol_table); + + it_id=cprover_equivalent_to_java_string_returning_function.find(function_id); + if(it_id!=cprover_equivalent_to_java_string_returning_function.end()) + return make_string_returning_function_from_call( + it_id->second, type, loc, symbol_table); + + it_id=cprover_equivalent_to_java_constructor.find(function_id); + if(it_id!=cprover_equivalent_to_java_constructor.end()) + return make_init_function_from_call( + it_id->second, type, loc, symbol_table); + + it_id=cprover_equivalent_to_java_assign_and_return_function.find(function_id); + if(it_id!=cprover_equivalent_to_java_assign_and_return_function.end()) + return make_assign_and_return_function_from_call( + it_id->second, type, loc, symbol_table); + + it_id=cprover_equivalent_to_java_assign_function.find(function_id); + if(it_id!=cprover_equivalent_to_java_assign_function.end()) + return make_assign_function_from_call( + it_id->second, type, loc, symbol_table); + + auto it=conversion_table.find(function_id); + if(it!=conversion_table.end()) + return it->second(type, loc, symbol_table); + + return nil_exprt(); +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::is_known_string_type + + Inputs: + class_name - name of the class + + Outputs: True if the type is one that is known to our preprocessing, + false otherwise + + Purpose: Check whether a class name is known as a string type. + +\*******************************************************************/ + +bool java_string_library_preprocesst::is_known_string_type( + irep_idt class_name) +{ + return string_types.find(class_name)!=string_types.end(); +} + +/*******************************************************************\ + +Function: java_string_library_preprocesst::initialize_conversion_table + + Purpose: fill maps with correspondence from java method names to + conversion functions + +\*******************************************************************/ + +void java_string_library_preprocesst::initialize_conversion_table() +{ + character_preprocess.initialize_conversion_table(); + + string_types= + std::unordered_set{"java.lang.String", + "java.lang.StringBuilder", + "java.lang.CharSequence", + "java.lang.StringBuffer"}; + + // String library + cprover_equivalent_to_java_constructor + ["java::java.lang.String.:(Ljava/lang/String;)V"]= + ID_cprover_string_copy_func; + cprover_equivalent_to_java_constructor + ["java::java.lang.String.:(Ljava/lang/StringBuilder;)V"]= + ID_cprover_string_copy_func; + cprover_equivalent_to_java_constructor + ["java::java.lang.String.:([C)V"]= + ID_cprover_string_copy_func; + cprover_equivalent_to_java_constructor + ["java::java.lang.String.:([CII)V"]= + ID_cprover_string_copy_func; + cprover_equivalent_to_java_constructor + ["java::java.lang.String.:()V"]= + ID_cprover_string_empty_string_func; + // Not supported java.lang.String.:(Ljava/lang/StringBuffer;) + + cprover_equivalent_to_java_function + ["java::java.lang.String.charAt:(I)C"]= + ID_cprover_string_char_at_func; + cprover_equivalent_to_java_function + ["java::java.lang.String.codePointAt:(I)I"]= + ID_cprover_string_code_point_at_func; + cprover_equivalent_to_java_function + ["java::java.lang.String.codePointBefore:(I)I"]= + ID_cprover_string_code_point_before_func; + cprover_equivalent_to_java_function + ["java::java.lang.String.codePointCount:(II)I"]= + ID_cprover_string_code_point_count_func; + cprover_equivalent_to_java_function + ["java::java.lang.String.compareTo:(Ljava/lang/String;)I"]= + ID_cprover_string_compare_to_func; + // Not supported "java.lang.String.contentEquals" + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.concat:(Ljava/lang/String;)Ljava/lang/String;"]= + ID_cprover_string_concat_func; + cprover_equivalent_to_java_function + ["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]= + ID_cprover_string_contains_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.copyValueOf:([CII)Ljava/lang/String;"]= + ID_cprover_string_copy_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.copyValueOf:([C)Ljava/lang/String;"]= + ID_cprover_string_copy_func; + cprover_equivalent_to_java_function + ["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]= + ID_cprover_string_endswith_func; + + conversion_table["java::java.lang.String.equals:(Ljava/lang/Object;)Z"]= + std::bind( + &java_string_library_preprocesst::make_equals_function_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3); + cprover_equivalent_to_java_function + ["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]= + ID_cprover_string_equals_ignore_case_func; + // Not supported "java.lang.String.format" + // Not supported "java.lang.String.getBytes" + // Not supported "java.lang.String.getChars" + cprover_equivalent_to_java_function + ["java::java.lang.String.hashCode:()I"]= + ID_cprover_string_hash_code_func; + cprover_equivalent_to_java_function + ["java::java.lang.String.indexOf:(I)I"]= + ID_cprover_string_index_of_func; + cprover_equivalent_to_java_function + ["java::java.lang.String.indexOf:(II)I"]= + ID_cprover_string_index_of_func; + cprover_equivalent_to_java_function + ["java::java.lang.String.indexOf:(Ljava/lang/String;)I"]= + ID_cprover_string_index_of_func; + cprover_equivalent_to_java_function + ["java::java.lang.String.indexOf:(Ljava/lang/String;I)I"]= + ID_cprover_string_index_of_func; + cprover_equivalent_to_java_function + ["java::java.lang.String.intern:()Ljava/lang/String;"]= + ID_cprover_string_intern_func; + cprover_equivalent_to_java_function + ["java::java.lang.String.isEmpty:()Z"]= + ID_cprover_string_is_empty_func; + cprover_equivalent_to_java_function + ["java::java.lang.String.lastIndexOf:(I)I"]= + ID_cprover_string_last_index_of_func; + cprover_equivalent_to_java_function + ["java::java.lang.String.lastIndexOf:(II)I"]= + ID_cprover_string_last_index_of_func; + cprover_equivalent_to_java_function + ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;)I"]= + ID_cprover_string_last_index_of_func; + cprover_equivalent_to_java_function + ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]= + ID_cprover_string_last_index_of_func; + cprover_equivalent_to_java_function + ["java::java.lang.String.length:()I"]= + ID_cprover_string_length_func; + // Not supported "java.lang.String.matches" + cprover_equivalent_to_java_function + ["java::java.lang.String.offsetByCodePoints:(II)I"]= + ID_cprover_string_offset_by_code_point_func; + // Not supported "java.lang.String.regionMatches" + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.replace:(CC)Ljava/lang/String;"]= + ID_cprover_string_replace_func; + // Not supported "java.lang.String.replace:(LCharSequence;LCharSequence)" + // Not supported "java.lang.String.replaceAll" + // Not supported "java.lang.String.replaceFirst" + // Not supported "java.lang.String.split" + cprover_equivalent_to_java_function + ["java::java.lang.String.startsWith:(Ljava/lang/String;)Z"]= + ID_cprover_string_startswith_func; + cprover_equivalent_to_java_function + ["java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]= + ID_cprover_string_startswith_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.subSequence:(II)Ljava/lang/CharSequence;"]= + ID_cprover_string_substring_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.substring:(II)Ljava/lang/String;"]= + ID_cprover_string_substring_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.substring:(I)Ljava/lang/String;"]= + ID_cprover_string_substring_func; + conversion_table + ["java::java.lang.String.toCharArray:()[C"]= + std::bind( + &java_string_library_preprocesst::make_string_to_char_array_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3); + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]= + ID_cprover_string_to_lower_case_func; + // Not supported "java.lang.String.toLowerCase:(Locale)" + // Not supported "java.lang.String.toString:()" + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.toUpperCase:()Ljava/lang/String;"]= + ID_cprover_string_to_upper_case_func; + // Not supported "java.lang.String.toUpperCase:(Locale)" + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.trim:()Ljava/lang/String;"]= + ID_cprover_string_trim_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.valueOf:(Z)Ljava/lang/String;"]= + ID_cprover_string_of_bool_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.valueOf:(C)Ljava/lang/String;"]= + ID_cprover_string_of_char_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.valueOf:([C)Ljava/lang/String;"]= + ID_cprover_string_copy_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.valueOf:([CII)Ljava/lang/String;"]= + ID_cprover_string_copy_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.valueOf:(D)Ljava/lang/String;"]= + ID_cprover_string_of_double_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.valueOf:(F)Ljava/lang/String;"]= + ID_cprover_string_of_float_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.valueOf:(I)Ljava/lang/String;"]= + ID_cprover_string_of_int_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.String.valueOf:(J)Ljava/lang/String;"]= + ID_cprover_string_of_long_func; + // Not supported "java.lang.String.valueOf:(LObject;)" + + // StringBuilder library + cprover_equivalent_to_java_constructor + ["java::java.lang.StringBuilder.:(Ljava/lang/String;)V"]= + ID_cprover_string_copy_func; + cprover_equivalent_to_java_constructor + ["java::java.lang.StringBuilder.:()V"]= + ID_cprover_string_empty_string_func; + + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;"]= + ID_cprover_string_concat_bool_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]= + ID_cprover_string_concat_char_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.append:([C)" + "Ljava/lang/StringBuilder;"]= + ID_cprover_string_concat_func; + // Not supported: "java.lang.StringBuilder.append:([CII)" + // Not supported: "java.lang.StringBuilder.append:(LCharSequence;)" + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"]= + ID_cprover_string_concat_double_func; + conversion_table["java::java.lang.StringBuilder.append:" + "(F)Ljava/lang/StringBuilder;"]= + std::bind( + &java_string_library_preprocesst::make_string_builder_append_float_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3); + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.append:(I)Ljava/lang/StringBuilder;"]= + ID_cprover_string_concat_int_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.append:(J)Ljava/lang/StringBuilder;"]= + ID_cprover_string_concat_long_func; + + conversion_table["java::java.lang.StringBuilder.append:" + "(Ljava/lang/Object;)Ljava/lang/StringBuilder;"]= + std::bind( + &java_string_library_preprocesst::make_string_builder_append_object_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3); + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.append:(Ljava/lang/String;)" + "Ljava/lang/StringBuilder;"]= + ID_cprover_string_concat_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.appendCodePoint:(I)" + "Ljava/lang/StringBuilder;"]= + ID_cprover_string_concat_code_point_func; + // Not supported: "java.lang.StringBuilder.append:(Ljava/lang/StringBuffer;)" + // Not supported: "java.lang.StringBuilder.capacity:()" + cprover_equivalent_to_java_function + ["java::java.lang.StringBuilder.charAt:(I)C"]= + ID_cprover_string_char_at_func; + cprover_equivalent_to_java_function + ["java::java.lang.StringBuilder.codePointAt:(I)I"]= + ID_cprover_string_code_point_at_func; + cprover_equivalent_to_java_function + ["java::java.lang.StringBuilder.codePointBefore:(I)I"]= + ID_cprover_string_code_point_before_func; + cprover_equivalent_to_java_function + ["java::java.lang.StringBuilder.codePointCount:(II)I"]= + ID_cprover_string_code_point_count_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.delete:(II)Ljava/lang/StringBuilder;"]= + ID_cprover_string_delete_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.deleteCharAt:(I)Ljava/lang/StringBuilder;"]= + ID_cprover_string_delete_char_at_func; + // Not supported: "java.lang.StringBuilder.ensureCapacity:()" + // Not supported: "java.lang.StringBuilder.getChars:()" + // Not supported: "java.lang.StringBuilder.indexOf:()" + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.insert:(IZ)Ljava/lang/StringBuilder;"]= + ID_cprover_string_insert_bool_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.insert:(IC)Ljava/lang/StringBuilder;"]= + ID_cprover_string_insert_char_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.insert:(I[C)Ljava/lang/StringBuilder;"]= + ID_cprover_string_insert_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.insert:(I[CII)Ljava/lang/StringBuilder;"]= + ID_cprover_string_insert_func; + // Not supported "java.lang.StringBuilder.insert:(ILCharSequence;)" + // Not supported "java.lang.StringBuilder.insert:(ILCharSequence;II)" + // Not supported "java.lang.StringBuilder.insert:(ID)" + // Not supported "java.lang.StringBuilder.insert:(IF)" + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.insert:(II)Ljava/lang/StringBuilder;"]= + ID_cprover_string_insert_int_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.insert:(IJ)Ljava/lang/StringBuilder;"]= + ID_cprover_string_insert_long_func; + // Not supported "java.lang.StringBuilder.insert:(ILObject;)" + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuilder.insert:(ILjava/lang/String;)" + "Ljava/lang/StringBuilder;"]= + ID_cprover_string_insert_func; + // Not supported "java.lang.StringBuilder.lastIndexOf" + cprover_equivalent_to_java_function + ["java::java.lang.StringBuilder.length:()I"]= + ID_cprover_string_length_func; + // Not supported "java.lang.StringBuilder.offsetByCodePoints" + // Not supported "java.lang.StringBuilder.replace" + // Not supported "java.lang.StringBuilder.reverse" + cprover_equivalent_to_java_assign_function + ["java::java.lang.StringBuilder.setCharAt:(IC)V"]= + ID_cprover_string_char_set_func; + cprover_equivalent_to_java_assign_function + ["java::java.lang.StringBuilder.setLength:(I)V"]= + ID_cprover_string_set_length_func; + // Not supported "java.lang.StringBuilder.subSequence" + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.StringBuilder.substring:(II)Ljava/lang/String;"]= + ID_cprover_string_substring_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]= + ID_cprover_string_substring_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.StringBuilder.toString:()Ljava/lang/String;"]= + ID_cprover_string_copy_func; + // Not supported "java.lang.StringBuilder.trimToSize" + // TODO clean irep ids from insert_char_array etc... + + // StringBuffer library + cprover_equivalent_to_java_constructor + ["java::java.lang.StringBuffer.:(Ljava/lang/String;)V"]= + ID_cprover_string_copy_func; + cprover_equivalent_to_java_constructor + ["java::java.lang.StringBuffer.:()V"]= + ID_cprover_string_empty_string_func; + + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuffer.append:(Z)Ljava/lang/StringBuffer;"]= + ID_cprover_string_concat_bool_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuffer.append:(C)Ljava/lang/StringBuffer;"]= + ID_cprover_string_concat_char_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuffer.append:([C)" + "Ljava/lang/StringBuffer;"]= + ID_cprover_string_concat_func; + // Not supported: "java.lang.StringBuffer.append:([CII)" + // Not supported: "java.lang.StringBuffer.append:(LCharSequence;)" + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuffer.append:(D)Ljava/lang/StringBuffer;"]= + ID_cprover_string_concat_double_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuffer.append:(F)Ljava/lang/StringBuffer;"]= + ID_cprover_string_concat_float_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuffer.append:(I)Ljava/lang/StringBuffer;"]= + ID_cprover_string_concat_int_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuffer.append:(J)Ljava/lang/StringBuffer;"]= + ID_cprover_string_concat_long_func; + // Not supported: "java.lang.StringBuffer.append:(LObject;)" + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuffer.append:(Ljava/lang/String;)" + "Ljava/lang/StringBuffer;"]= + ID_cprover_string_concat_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuffer.appendCodePoint:(I)" + "Ljava/lang/StringBuffer;"]= + ID_cprover_string_concat_code_point_func; + // Not supported: "java.lang.StringBuffer.append:(Ljava/lang/StringBuffer;)" + // Not supported: "java.lang.StringBuffer.capacity:()" + cprover_equivalent_to_java_function + ["java::java.lang.StringBuffer.charAt:(I)C"]= + ID_cprover_string_char_at_func; + cprover_equivalent_to_java_function + ["java::java.lang.StringBuffer.codePointAt:(I)I"]= + ID_cprover_string_code_point_at_func; + cprover_equivalent_to_java_function + ["java::java.lang.StringBuffer.codePointBefore:(I)I"]= + ID_cprover_string_code_point_before_func; + cprover_equivalent_to_java_function + ["java::java.lang.StringBuffer.codePointCount:(II)I"]= + ID_cprover_string_code_point_count_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuffer.delete:(II)Ljava/lang/StringBuffer;"]= + ID_cprover_string_delete_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuffer.deleteCharAt:(I)Ljava/lang/StringBuffer;"]= + ID_cprover_string_delete_char_at_func; + // Not supported: "java.lang.StringBuffer.ensureCapacity:()" + // Not supported: "java.lang.StringBuffer.getChars:()" + // Not supported: "java.lang.StringBuffer.indexOf:()" + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuffer.insert:(IZ)Ljava/lang/StringBuffer;"]= + ID_cprover_string_insert_bool_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuffer.insert:(IC)Ljava/lang/StringBuffer;"]= + ID_cprover_string_insert_char_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuffer.insert:(I[C)Ljava/lang/StringBuffer;"]= + ID_cprover_string_insert_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuffer.insert:(I[CII)Ljava/lang/StringBuffer;"]= + ID_cprover_string_insert_func; + // Not supported "java.lang.StringBuffer.insert:(ILCharSequence;)" + // Not supported "java.lang.StringBuffer.insert:(ILCharSequence;II)" + // Not supported "java.lang.StringBuffer.insert:(ID)" + // Not supported "java.lang.StringBuffer.insert:(IF)" + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuffer.insert:(II)Ljava/lang/StringBuffer;"]= + ID_cprover_string_insert_int_func; + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuffer.insert:(IJ)Ljava/lang/StringBuffer;"]= + ID_cprover_string_insert_long_func; + // Not supported "java.lang.StringBuffer.insert:(ILObject;)" + cprover_equivalent_to_java_assign_and_return_function + ["java::java.lang.StringBuffer.insert:(ILjava/lang/String;)" + "Ljava/lang/StringBuffer;"]= + ID_cprover_string_insert_func; + // Not supported "java.lang.StringBuffer.lastIndexOf" + cprover_equivalent_to_java_function + ["java::java.lang.StringBuffer.length:()I"]= + ID_cprover_string_length_func; + // Not supported "java.lang.StringBuffer.offsetByCodePoints" + // Not supported "java.lang.StringBuffer.replace" + // Not supported "java.lang.StringBuffer.reverse" + cprover_equivalent_to_java_assign_function + ["java::java.lang.StringBuffer.setCharAt:(IC)V"]= + ID_cprover_string_char_set_func; + cprover_equivalent_to_java_assign_function + ["java::java.lang.StringBuffer.setLength:(I)V"]= + ID_cprover_string_set_length_func; + // Not supported "java.lang.StringBuffer.subSequence" + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.StringBuffer.substring:(II)Ljava/lang/String;"]= + ID_cprover_string_substring_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]= + ID_cprover_string_substring_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"]= + ID_cprover_string_copy_func; + // Not supported "java.lang.StringBuffer.trimToSize" + + // Other libraries + cprover_equivalent_to_java_function + ["java::java.lang.CharSequence.charAt:(I)C"]= + ID_cprover_string_char_at_func; + conversion_table + ["java::java.lang.Float.toString:(F)Ljava/lang/String;"]= + std::bind( + &java_string_library_preprocesst::make_float_to_string_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3); + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.Integer.toHexString:(I)Ljava/lang/String;"]= + ID_cprover_string_of_int_hex_func; + cprover_equivalent_to_java_function + ["java::java.lang.Integer.parseInt:(Ljava/lang/String;)I"]= + ID_cprover_string_parse_int_func; + cprover_equivalent_to_java_string_returning_function + ["java::java.lang.Integer.toString:(I)Ljava/lang/String;"]= + ID_cprover_string_of_int_func; +} diff --git a/src/java_bytecode/java_string_library_preprocess.h b/src/java_bytecode/java_string_library_preprocess.h new file mode 100644 index 00000000000..beeed0145ff --- /dev/null +++ b/src/java_bytecode/java_string_library_preprocess.h @@ -0,0 +1,302 @@ +/*******************************************************************\ + +Module: Produce code for simple implementation of String Java libraries + +Author: Romain Brenguier + +Date: March 2017 + +\*******************************************************************/ + +#ifndef CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H +#define CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H + +#include +#include +#include +#include +#include + +#include // should get rid of this + +#include +#include +#include "character_refine_preprocess.h" +#include "java_types.h" + +class java_string_library_preprocesst:public messaget +{ +public: + java_string_library_preprocesst(): + refined_string_type(java_int_type(), java_char_type()) {} + + void initialize_conversion_table(); + void initialize_refined_string_type(); + + exprt code_for_function( + const irep_idt &function_id, + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table); + + codet replace_character_call(code_function_callt call) + { + return character_preprocess.replace_character_call(call); + } + void add_string_type(const irep_idt &class_name, symbol_tablet &symbol_table); + bool is_known_string_type(irep_idt class_name); + +private: + 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); + static bool implements_java_char_sequence(const typet &type) + { + return + is_java_char_sequence_pointer_type(type) || + is_java_string_builder_pointer_type(type) || + is_java_string_buffer_pointer_type(type) || + is_java_string_pointer_type(type); + } + + character_refine_preprocesst character_preprocess; + + const refined_string_typet refined_string_type; + + typedef + std::function + conversion_functiont; + + typedef std::unordered_map id_mapt; + + // Table mapping each java method signature to the code generating function + std::unordered_map + conversion_table; + + // Some Java functions have an equivalent in the solver that we will + // call with the same argument and will return the same result + id_mapt cprover_equivalent_to_java_function; + + // Some Java functions have an equivalent except that they should + // return Java Strings instead of string_exprt + id_mapt cprover_equivalent_to_java_string_returning_function; + + // Some Java initialization function initialize strings with the + // same result as some function of the solver + id_mapt cprover_equivalent_to_java_constructor; + + // Some Java functions have an equivalent in the solver except that + // in addition they assign the result to the object on which it is called + id_mapt cprover_equivalent_to_java_assign_and_return_function; + + // Some Java functions have an equivalent in the solver except that + // they assign the result to the object on which it is called instead + // of returning it + id_mapt cprover_equivalent_to_java_assign_function; + + // A set tells us what java types should be considered as string objects + std::unordered_set string_types; + + // Conversion functions + codet make_string_builder_append_object_code( + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table); + + codet make_equals_function_code( + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table); + + codet make_string_builder_append_float_code( + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table); + + codet make_float_to_string_code( + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table); + + codet make_string_to_char_array_code( + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table); + + // Auxiliary functions + codet code_for_scientific_notation( + const exprt &arg, + const ieee_float_spect &float_spec, + const string_exprt &string_expr, + const exprt &tmp_string, + const refined_string_typet &refined_string_type, + const source_locationt &loc, + symbol_tablet &symbol_table); + + // Helper functions + exprt::operandst process_parameters( + const code_typet::parameterst ¶ms, + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &init_code); + + void process_single_operand( + exprt::operandst &processed_ops, + const exprt &deref, + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &init_code); + + exprt::operandst process_operands( + const exprt::operandst &operands, + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &init_code); + + exprt::operandst process_equals_function_operands( + const exprt::operandst &operands, + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &init_code); + + string_exprt replace_char_array( + const exprt &array_pointer, + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &code); + + void declare_function( + irep_idt function_name, const typet &type, symbol_tablet &symbol_table); + + typet get_data_type( + const typet &type, const symbol_tablet &symbol_table); + typet get_length_type( + const typet &type, const symbol_tablet &symbol_table); + exprt get_data(const exprt &expr, const symbol_tablet &symbol_table); + exprt get_length(const exprt &expr, const symbol_tablet &symbol_table); + + symbol_exprt fresh_string( + const typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table); + + symbol_exprt fresh_array( + const typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table); + + string_exprt fresh_string_expr( + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &code); + + exprt fresh_string_expr_symbol( + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &code); + + exprt allocate_fresh_string( + const typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &code); + + exprt allocate_fresh_array( + const typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &code); + + exprt make_function_application( + const irep_idt &function_name, + const exprt::operandst &arguments, + const typet &type, + symbol_tablet &symbol_table); + + codet code_assign_function_application( + const exprt &lhs, + const irep_idt &function_name, + const exprt::operandst &arguments, + symbol_tablet &symbol_table); + + codet code_return_function_application( + const irep_idt &function_name, + const exprt::operandst &arguments, + const typet &type, + symbol_tablet &symbol_table); + + codet code_assign_function_to_string_expr( + const string_exprt &string_expr, + const irep_idt &function_name, + const exprt::operandst &arguments, + symbol_tablet &symbol_table); + + string_exprt string_expr_of_function_application( + const irep_idt &function_name, + const exprt::operandst &arguments, + const source_locationt &loc, + symbol_tablet &symbol_table, + code_blockt &code); + + codet code_assign_string_expr_to_java_string( + const exprt &lhs, const string_exprt &rhs, symbol_tablet &symbol_table); + + codet code_assign_string_expr_to_new_java_string( + const exprt &lhs, + const string_exprt &rhs, + const source_locationt &loc, + symbol_tablet &symbol_table); + + codet code_assign_java_string_to_string_expr( + const string_exprt &lhs, const exprt &rhs, symbol_tablet &symbol_table); + + codet code_assign_string_literal_to_string_expr( + const string_exprt &lhs, + const exprt &tmp_string, + const std::string &s, + symbol_tablet &symbol_table); + + exprt string_literal(const std::string &s); + + codet make_function_from_call( + const irep_idt &function_name, + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table); + + codet make_init_function_from_call( + const irep_idt &function_name, + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table, + bool ignore_first_arg=true); + + codet make_assign_and_return_function_from_call( + const irep_idt &function_name, + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table); + + codet make_assign_function_from_call( + const irep_idt &function_name, + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table); + + codet make_string_returning_function_from_call( + const irep_idt &function_name, + const code_typet &type, + const source_locationt &loc, + symbol_tablet &symbol_table); +}; + +#endif // CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H