From 33a31a1be9e3a6d6f897a1d5a7bb00eab07bae57 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 30 Aug 2018 11:17:51 +0100 Subject: [PATCH 1/2] Fix string non empty option --- .../java_bytecode/java_bytecode_language.cpp | 2 ++ .../src/java_bytecode/java_object_factory.cpp | 29 ++++++++++--------- .../java_bytecode/object_factory_parameters.h | 3 ++ src/solvers/refinement/string_refinement.h | 2 ++ 4 files changed, 22 insertions(+), 14 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index f008b7a7b38..f688674cfd4 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -68,6 +68,8 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) object_factory_parameters.max_nondet_string_length = safe_string2size_t(cmd.get_value("max-nondet-string-length")); } + if(cmd.isset("string-non-empty")) + object_factory_parameters.min_nondet_string_length = 1; object_factory_parameters.string_printable = cmd.isset("string-printable"); if(cmd.isset("java-max-vla-length")) diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index d517e93c00a..5d405a0cc3b 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -538,6 +538,7 @@ static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size) /// \param struct_expr [out]: struct that we may initialize /// \param code: block to add pre-requisite declarations (e.g. to allocate a /// data array) +/// \param min_nondet_string_length: minimum length of strings to initialize /// \param max_nondet_string_length: maximum length of strings to initialize /// \param loc: location in the source /// \param function_id: function ID to associate with auxiliary variables @@ -573,6 +574,7 @@ static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size) bool initialize_nondet_string_fields( struct_exprt &struct_expr, code_blockt &code, + const std::size_t &min_nondet_string_length, const std::size_t &max_nondet_string_length, const source_locationt &loc, const irep_idt &function_id, @@ -627,11 +629,10 @@ bool initialize_nondet_string_fields( code.add(code_declt(length_expr)); code.add(code_assignt(length_expr, nondet_length)); - // assume (length_expr >= 0); - code.add( - code_assumet( - binary_relation_exprt( - length_expr, ID_ge, from_integer(0, java_int_type())))); + // assume (length_expr >= min_nondet_string_length); + const exprt min_length = + from_integer(min_nondet_string_length, java_int_type()); + code.add(code_assumet(binary_relation_exprt(length_expr, ID_ge, min_length))); // assume (length_expr <= max_input_length) if(max_nondet_string_length <= max_value(length_expr.type())) @@ -1044,15 +1045,15 @@ 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: - skip_special_string_fields = - initialize_nondet_string_fields( - to_struct_expr(initial_object), - assignments, - object_factory_parameters.max_nondet_string_length, - loc, - object_factory_parameters.function_id, - symbol_table, - object_factory_parameters.string_printable); + skip_special_string_fields = initialize_nondet_string_fields( + to_struct_expr(initial_object), + assignments, + object_factory_parameters.min_nondet_string_length, + object_factory_parameters.max_nondet_string_length, + loc, + object_factory_parameters.function_id, + symbol_table, + object_factory_parameters.string_printable); assignments.copy_to_operands( code_assignt(expr, initial_object)); diff --git a/jbmc/src/java_bytecode/object_factory_parameters.h b/jbmc/src/java_bytecode/object_factory_parameters.h index 50491a12156..838e5ed0b6a 100644 --- a/jbmc/src/java_bytecode/object_factory_parameters.h +++ b/jbmc/src/java_bytecode/object_factory_parameters.h @@ -28,6 +28,9 @@ struct object_factory_parameterst final /// Maximum value for the non-deterministically-chosen length of a string. size_t max_nondet_string_length=MAX_NONDET_STRING_LENGTH; + /// Minimum value for the non-deterministically-chosen length of a string. + size_t min_nondet_string_length = 0; + /// Maximum depth for object hierarchy on input. /// Used to prevent object factory to loop infinitely during the /// generation of code that allocates/initializes data structures of recursive diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 7ee5a580d26..cf042af8280 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -33,11 +33,13 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #define OPT_STRING_REFINEMENT \ "(no-refine-strings)" \ "(string-printable)" \ + "(string-non-empty)" \ "(max-nondet-string-length):" #define HELP_STRING_REFINEMENT \ " --no-refine-strings turn off string refinement\n" \ " --string-printable restrict to printable strings (experimental)\n" /* NOLINT(*) */ \ + " --string-non-empty restrict to non-empty strings (experimental)\n" /* NOLINT(*) */ \ " --max-nondet-string-length n bound the length of nondet (e.g. input) strings\n" /* NOLINT(*) */ // The integration of the string solver into CBMC is incomplete. Therefore, From cf123f06e879cc14ef87414a67c6308cf2f00a8c Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 31 Aug 2018 07:36:55 +0100 Subject: [PATCH 2/2] Test for the string-non-empty option --- .../string-non-empty-option/Test.class | Bin 0 -> 726 bytes .../string-non-empty-option/Test.java | 22 ++++++++++++++++++ .../string-non-empty-option/test.desc | 9 +++++++ .../test_non_empty.desc | 9 +++++++ .../test_non_empty_no_overflow.desc | 9 +++++++ 5 files changed, 49 insertions(+) create mode 100644 jbmc/regression/jbmc-strings/string-non-empty-option/Test.class create mode 100644 jbmc/regression/jbmc-strings/string-non-empty-option/Test.java create mode 100644 jbmc/regression/jbmc-strings/string-non-empty-option/test.desc create mode 100644 jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty.desc create mode 100644 jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty_no_overflow.desc diff --git a/jbmc/regression/jbmc-strings/string-non-empty-option/Test.class b/jbmc/regression/jbmc-strings/string-non-empty-option/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..6d6d48980f927b69faa574e35143c49882378abb GIT binary patch literal 726 zcmZWmT~8B16g{)uk9OHYp%xb`V1a~M5_sXw#@HYRk|GZ!B%lv&x05osZq4l0AJfEy z#0Q_z1QLzwr9W1yoQF5^8 z;sMGImKcibL6UHpie8*N6G_mHc!zLEPPLrBcM*$Ny&zRMUJb4Tu}O8}`c9!)Q3w zZT0#xCDq>iEc)>Rl5PZQiYhN)7D8w)EN{gR;Axz5E)2nzu;{ChIv&U!2b+mfOhQ~nGbmR z4d&?$te<7`a)|72YNRnntV=9w&X(dR^tJgBl@YF?qJk(pHOeYsh89-S9xM`OYd?AN zvPy0?NMfBT8kof^6d_Tf2&yg%e_^FW(cIYej 0; + } else if(nondet == 1) { + assert arg2.length() > 0; + } else if(nondet == 2) { + // For this assertion to be valid, also need to limit the length of + // strings because overflows could cause the sum to be negative. + assert arg1.length() + arg2.length() > 1; + } else { + assert arg1.length() > 1; + } + } +} diff --git a/jbmc/regression/jbmc-strings/string-non-empty-option/test.desc b/jbmc/regression/jbmc-strings/string-non-empty-option/test.desc new file mode 100644 index 00000000000..777a6e5c56f --- /dev/null +++ b/jbmc/regression/jbmc-strings/string-non-empty-option/test.desc @@ -0,0 +1,9 @@ +CORE +Test.class +--function Test.checkMinLength +^EXIT=10$ +^SIGNAL=0$ +assertion.* line 11 function java::Test.checkMinLength.*: FAILURE +assertion.* line 13 function java::Test.checkMinLength.*: FAILURE +assertion.* line 17 function java::Test.checkMinLength.*: FAILURE +assertion.* line 19 function java::Test.checkMinLength.*: FAILURE diff --git a/jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty.desc b/jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty.desc new file mode 100644 index 00000000000..04661a826d7 --- /dev/null +++ b/jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty.desc @@ -0,0 +1,9 @@ +CORE +Test.class +--function Test.checkMinLength --string-non-empty +^EXIT=10$ +^SIGNAL=0$ +assertion.* line 11 function java::Test.checkMinLength.*: SUCCESS +assertion.* line 13 function java::Test.checkMinLength.*: SUCCESS +assertion.* line 17 function java::Test.checkMinLength.*: FAILURE +assertion.* line 19 function java::Test.checkMinLength.*: FAILURE diff --git a/jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty_no_overflow.desc b/jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty_no_overflow.desc new file mode 100644 index 00000000000..119d7b03f11 --- /dev/null +++ b/jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty_no_overflow.desc @@ -0,0 +1,9 @@ +CORE +Test.class +--function Test.checkMinLength --string-non-empty --max-nondet-string-length 100000 +^EXIT=10$ +^SIGNAL=0$ +assertion.* line 11 function java::Test.checkMinLength.*: SUCCESS +assertion.* line 13 function java::Test.checkMinLength.*: SUCCESS +assertion.* line 17 function java::Test.checkMinLength.*: SUCCESS +assertion.* line 19 function java::Test.checkMinLength.*: FAILURE