From b3967eb78341c8a3529277923f02bcf17e37733a Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Sun, 7 Apr 2019 17:14:48 +0100 Subject: [PATCH 1/3] Fix strings not being recognized in the object factory For a given struct, the object factory previously checked if it was a string only in the case where skip_classid was set to false and the update strategy was NO_UPDATE_IN_PLACE or MAY_UPDATE_IN_PLACE. This missed some cases, for example the case where no model for String is loaded and the Java method includes a call to a string constructor that depends on a model. In this case the constructor is stubbed and skip_classid is set to true in java_simple_method_stubst. Before this fix, the object factory would go through the components of the string expression as if it was a regular object expression, and hit an invariant violation because the data component is stored as a pointer to an unsignedbv, contradicting the assumption that all pointers point to structs. --- .../src/java_bytecode/java_object_factory.cpp | 126 ++++++++---------- 1 file changed, 59 insertions(+), 67 deletions(-) diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 473f00bced1..4ce445ace46 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -794,77 +794,69 @@ void java_object_factoryt::gen_nondet_struct_init( // * Not if the object has already been initialised by our caller, in which // case they will set `skip_classid` // * Not if we're re-initializing an existing object (i.e. update_in_place) - - bool skip_special_string_fields = false; - - if(!is_sub && - !skip_classid && - update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE) + // * Always if it has a string type. Strings should not be partially updated, + // and the `length` and `data` components of string types need to be + // generated differently from object fields in the general case, see + // \ref java_object_factoryt::initialize_nondet_string_fields. + + const bool is_char_sequence = + java_string_library_preprocesst::implements_java_char_sequence(struct_type); + const bool has_length_and_data = + struct_type.has_component("length") && struct_type.has_component("data"); + const bool skip_special_string_fields = + is_char_sequence && has_length_and_data; + const bool has_string_input_values = + !object_factory_parameters.string_input_values.empty(); + + if(skip_special_string_fields && has_string_input_values && !skip_classid) + { // We're dealing with a string and we should set fixed input values. + // We create a switch statement where each case is an assignment + // of one of the fixed input strings to the input variable in question + const alternate_casest cases = get_string_input_values_code( + expr, object_factory_parameters.string_input_values, symbol_table); + assignments.add(generate_nondet_switch( + id2string(object_factory_parameters.function_id), + cases, + java_int_type(), + ID_java, + location, + symbol_table)); + } + else if( + (!is_sub && !skip_classid && + update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE) || + skip_special_string_fields) { - class_identifier = struct_tag; + // Add an initial all-zero write. Most of the fields of this will be + // overwritten, but it helps to have a whole-structure write that analysis + // passes can easily recognise leaves no uninitialised state behind. - const bool is_char_sequence = - java_string_library_preprocesst - ::implements_java_char_sequence(struct_type); - const bool has_length_and_data = - struct_type.has_component("length") && struct_type.has_component("data"); - const bool has_string_input_values = - !object_factory_parameters.string_input_values.empty(); - - if(is_char_sequence && has_length_and_data && has_string_input_values) - { // We're dealing with a string and we should set fixed input values. - skip_special_string_fields = true; - - // We create a switch statement where each case is an assignment - // of one of the fixed input strings to the input variable in question - - const alternate_casest cases = - get_string_input_values_code( - expr, - object_factory_parameters.string_input_values, - symbol_table); - assignments.add(generate_nondet_switch( - id2string(object_factory_parameters.function_id), - cases, - java_int_type(), - ID_java, + // This code mirrors the `remove_java_new` pass: + auto initial_object = zero_initializer(expr.type(), source_locationt(), ns); + CHECK_RETURN(initial_object.has_value()); + class_identifier = struct_tag; + const irep_idt qualified_clsid = "java::" + id2string(class_identifier); + set_class_identifier( + to_struct_expr(*initial_object), ns, struct_tag_typet(qualified_clsid)); + + // If the initialised type is a special-cased String type (one with length + // and data fields introduced by string-library preprocessing), initialise + // those fields with nondet values + if(skip_special_string_fields) + { // We're dealing with a string + initialize_nondet_string_fields( + to_struct_expr(*initial_object), + assignments, + object_factory_parameters.min_nondet_string_length, + object_factory_parameters.max_nondet_string_length, location, - symbol_table)); - } - else - { - // Add an initial all-zero write. Most of the fields of this will be - // overwritten, but it helps to have a whole-structure write that analysis - // passes can easily recognise leaves no uninitialised state behind. - - // This code mirrors the `remove_java_new` pass: - auto initial_object = - zero_initializer(expr.type(), source_locationt(), ns); - CHECK_RETURN(initial_object.has_value()); - const irep_idt qualified_clsid = "java::" + id2string(class_identifier); - set_class_identifier( - to_struct_expr(*initial_object), ns, struct_tag_typet(qualified_clsid)); - - // If the initialised type is a special-cased String type (one with length - // and data fields introduced by string-library preprocessing), initialise - // those fields with nondet values - if(is_char_sequence && has_length_and_data) - { // We're dealing with a string - skip_special_string_fields = true; - initialize_nondet_string_fields( - to_struct_expr(*initial_object), - assignments, - object_factory_parameters.min_nondet_string_length, - object_factory_parameters.max_nondet_string_length, - location, - object_factory_parameters.function_id, - symbol_table, - object_factory_parameters.string_printable, - allocate_objects); - } - - assignments.add(code_assignt(expr, *initial_object)); + object_factory_parameters.function_id, + symbol_table, + object_factory_parameters.string_printable, + allocate_objects); } + + assignments.add(code_assignt(expr, *initial_object)); } for(const auto &component : components) From 4024eeed7a7af1c6e9a347f29694a63a6e645323 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Mon, 8 Apr 2019 11:06:07 +0100 Subject: [PATCH 2/3] Rename skip_special_string_fields to is_string_type There are more decisions associated with this variable than whether or not to skip the length and data fields. --- jbmc/src/java_bytecode/java_object_factory.cpp | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 4ce445ace46..6babd7e40d6 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -803,12 +803,11 @@ void java_object_factoryt::gen_nondet_struct_init( java_string_library_preprocesst::implements_java_char_sequence(struct_type); const bool has_length_and_data = struct_type.has_component("length") && struct_type.has_component("data"); - const bool skip_special_string_fields = - is_char_sequence && has_length_and_data; + const bool is_string_type = is_char_sequence && has_length_and_data; const bool has_string_input_values = !object_factory_parameters.string_input_values.empty(); - if(skip_special_string_fields && has_string_input_values && !skip_classid) + if(is_string_type && has_string_input_values && !skip_classid) { // We're dealing with a string and we should set fixed input values. // We create a switch statement where each case is an assignment // of one of the fixed input strings to the input variable in question @@ -825,7 +824,7 @@ void java_object_factoryt::gen_nondet_struct_init( else if( (!is_sub && !skip_classid && update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE) || - skip_special_string_fields) + is_string_type) { // Add an initial all-zero write. Most of the fields of this will be // overwritten, but it helps to have a whole-structure write that analysis @@ -842,7 +841,7 @@ void java_object_factoryt::gen_nondet_struct_init( // If the initialised type is a special-cased String type (one with length // and data fields introduced by string-library preprocessing), initialise // those fields with nondet values - if(skip_special_string_fields) + if(is_string_type) { // We're dealing with a string initialize_nondet_string_fields( to_struct_expr(*initial_object), @@ -882,7 +881,7 @@ void java_object_factoryt::gen_nondet_struct_init( code.add_source_location() = location; assignments.add(code); } - else if(skip_special_string_fields && (name == "length" || name == "data")) + else if(is_string_type && (name == "length" || name == "data")) { // In this case these were set up above. continue; From 9bc1a6ed47b57c5a8211d16e8d76367a2c89e16b Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Mon, 8 Apr 2019 11:33:12 +0100 Subject: [PATCH 3/3] Add test for stubbed string constructor --- .../jbmc-strings/stubbed-constructor/Test.class | Bin 0 -> 625 bytes .../jbmc-strings/stubbed-constructor/Test.java | 11 +++++++++++ .../jbmc-strings/stubbed-constructor/test.desc | 12 ++++++++++++ 3 files changed, 23 insertions(+) create mode 100644 jbmc/regression/jbmc-strings/stubbed-constructor/Test.class create mode 100644 jbmc/regression/jbmc-strings/stubbed-constructor/Test.java create mode 100644 jbmc/regression/jbmc-strings/stubbed-constructor/test.desc diff --git a/jbmc/regression/jbmc-strings/stubbed-constructor/Test.class b/jbmc/regression/jbmc-strings/stubbed-constructor/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..103a0768413799a20ff58c0b49bdbfe80cdb86bd GIT binary patch literal 625 zcmY*WT~8B16g_vprrj=dDT4I_6hUn@kr!St#7L?p1k{I8lZB`0b^=@Lu9@BPV|ek= zXElLDjK2GyG~U@r8(wDaoO|!N=brif_xn!(8)*CR(G;S2<;M~hxW@trm92R6pT_TIV;!qkiD|0tbJLTdJdpurFiQwcygriY z(R#PgNqS`P)c`dF0oHJz(41CmUrK(db*5Q@VH0=|;2~O9xZd`MDrR-oVTa(h4m)NQ zFFuxfn^C8=(`LLrW$ujF4#MI<<%w2<$sk^?7;}QXIKT>9>a*1pHjO@xY_I{C<+IMO zCBBJo_t81%iz!6Nr&oeDs+gOUW^njxfT!Yz8`_8Hu8_zATOc+ok;FT-z@{0-(ZQ<~tPWr>?SsliAM^aq;)^8(ixUYHEuC