From 6d8662638a888b569172efb16842fdad72cc5774 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 9 Aug 2018 10:41:35 +0100 Subject: [PATCH 1/3] Update jbmc/lib/java-models-library to java-models-library#9 (String of char array) https://github.com/diffblue/java-models-library/pull/9 --- jbmc/lib/java-models-library | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library index c9d9226d346..3163b09a9f4 160000 --- a/jbmc/lib/java-models-library +++ b/jbmc/lib/java-models-library @@ -1 +1 @@ -Subproject commit c9d9226d34649c21f30bb99f92e0a3d6e5fb8977 +Subproject commit 3163b09a9f43ebe637caf508427b52e41e1993f2 From bd292f745ee9973106cc151140dff3a2c605492f Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 20 Jun 2018 12:18:07 +0100 Subject: [PATCH 2/3] Stop preprocessing for unsupported functions Conversion from char array to string does not work, because the string refinement is not aware of the operations performed on the arrays. To construct strings from char array, the constructors have to be implemented using loops instead. --- .../java_string_library_preprocess.cpp | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index ff2dd7c23e3..cd046a48cb0 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -1922,13 +1922,6 @@ void java_string_library_preprocesst::initialize_conversion_table() std::placeholders::_2, std::placeholders::_3, std::placeholders::_4); - conversion_table["java::java.lang.String.:([CII)V"] = std::bind( - &java_string_library_preprocesst::make_init_from_array_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3, - std::placeholders::_4); cprover_equivalent_to_java_constructor ["java::java.lang.String.:()V"]= ID_cprover_string_empty_string_func; @@ -1956,12 +1949,6 @@ void java_string_library_preprocesst::initialize_conversion_table() 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; @@ -2108,9 +2095,6 @@ void java_string_library_preprocesst::initialize_conversion_table() 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; cprover_equivalent_to_java_assign_and_return_function ["java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_double_func; From f6c3023712a8c6ed1cb7a6711df6598439e56c21 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 20 Jun 2018 12:22:19 +0100 Subject: [PATCH 3/3] Remove unused functions --- .../java_string_library_preprocess.cpp | 81 ------------------- .../java_string_library_preprocess.h | 20 ----- 2 files changed, 101 deletions(-) diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index cd046a48cb0..bae9a3db4e3 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -168,18 +168,6 @@ bool java_string_library_preprocesst::is_java_char_array_pointer_type( return false; } -/// \param symbol_table: a symbol_table containing an entry for java Strings -/// \return the type of data fields in java Strings. -typet string_data_type(const symbol_tablet &symbol_table) -{ - symbolt sym=*symbol_table.lookup("java::java.lang.String"); - typet concrete_type=sym.type; - struct_typet struct_type=to_struct_type(concrete_type); - std::size_t index=struct_type.component_number("data"); - typet data_type=struct_type.components()[index].type(); - return data_type; -} - /// \return the type of the length field in java Strings. typet string_length_type() { @@ -589,26 +577,6 @@ exprt java_string_library_preprocesst::allocate_fresh_string( return str; } -/// declare a new character array and allocate it -/// \param type: a type for string -/// \param loc: a location in the program -/// \param symbol_table: symbol table -/// \param code: code block to which allocation instruction will be added -/// \return a new array -exprt java_string_library_preprocesst::allocate_fresh_array( - const typet &type, - const source_locationt &loc, - const irep_idt &function_id, - symbol_tablet &symbol_table, - code_blockt &code) -{ - exprt array=fresh_array(type, loc, symbol_table); - code.add(code_declt(array), loc); - allocate_dynamic_object_with_decl( - array, symbol_table, loc, function_id, code); - return array; -} - /// assign the result of a function call /// \param lhs: an expression /// \param function_name: the name of the function @@ -1719,55 +1687,6 @@ codet java_string_library_preprocesst::make_copy_constructor_code( return code; } -/// Used to provide code for constructor from a char array. -/// The implementation is similar to substring except the 3rd argument is a -/// count instead of end index -/// \param type: type of the function call -/// \param loc: location in the program_invocation_name -/// \param function_id: unused -/// \param symbol_table: symbol table -/// \return code implementing String intitialization from a char array and -/// arguments offset and end. -codet java_string_library_preprocesst::make_init_from_array_code( - const java_method_typet &type, - const source_locationt &loc, - const irep_idt &function_id, - symbol_table_baset &symbol_table) -{ - (void)function_id; - - // Code for the output - code_blockt code; - - java_method_typet::parameterst params = type.parameters(); - PRECONDITION(params.size() == 4); - exprt::operandst args = - process_parameters(type.parameters(), loc, symbol_table, code); - INVARIANT( - args.size() == 4, "process_parameters preserves number of arguments"); - - /// \todo this assumes the array to be constant between all calls to - /// string primitives, which may not be true in general. - refined_string_exprt string_arg = to_string_expr(args[1]); - - // The third argument is `count`, whereas the third argument of substring - // is `end` which corresponds to `offset+count` - refined_string_exprt string_expr = string_expr_of_function( - ID_cprover_string_substring_func, - {args[1], args[2], plus_exprt(args[2], args[3])}, - loc, - symbol_table, - code); - - // Assign string_expr to `this` object - symbol_exprt arg_this(params[0].get_identifier(), params[0].type()); - code.add( - code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table), - loc); - - return code; -} - /// Generates code for the String.length method /// \param type: type of the function /// \param loc: location in the source diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h index dca4e97d2cd..f3b7ac829b0 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.h +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h @@ -43,7 +43,6 @@ class java_string_library_preprocesst:public messaget void initialize_known_type_table(); void initialize_conversion_table(); - void initialize_refined_string_type(); bool implements_function(const irep_idt &function_id) const; void get_all_function_names(std::unordered_set &methods) const; @@ -151,12 +150,6 @@ class java_string_library_preprocesst:public messaget const irep_idt &function_id, symbol_table_baset &symbol_table); - codet make_string_to_char_array_code( - const java_method_typet &type, - const source_locationt &loc, - const irep_idt &function_id, - symbol_tablet &symbol_table); - codet make_string_format_code( const java_method_typet &type, const source_locationt &loc, @@ -254,13 +247,6 @@ class java_string_library_preprocesst:public messaget symbol_table_baset &symbol_table, code_blockt &code); - exprt allocate_fresh_array( - const typet &type, - const source_locationt &loc, - const irep_idt &function_id, - symbol_tablet &symbol_table, - code_blockt &code); - codet code_return_function_application( const irep_idt &function_name, const exprt::operandst &arguments, @@ -346,12 +332,6 @@ class java_string_library_preprocesst:public messaget code_blockt &code); exprt get_object_at_index(const exprt &argv, std::size_t index); - - codet make_init_from_array_code( - const java_method_typet &type, - const source_locationt &loc, - const irep_idt &function_id, - symbol_table_baset &symbol_table); }; exprt make_nondet_infinite_char_array(