From c66e88641b35a7d7637445fd9647e62ff2c088f5 Mon Sep 17 00:00:00 2001 From: svorenova Date: Fri, 10 May 2019 10:32:33 +0100 Subject: [PATCH 1/3] Set max-nondet-string-length to 10000 by default Unless no-refine-strings is defined --- src/solvers/strings/string_refinement.h | 3 ++- src/util/object_factory_parameters.cpp | 4 ++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/solvers/strings/string_refinement.h b/src/solvers/strings/string_refinement.h index 22616d63b51..83189522ac1 100644 --- a/src/solvers/strings/string_refinement.h +++ b/src/solvers/strings/string_refinement.h @@ -45,7 +45,8 @@ Author: Alberto Griggio, alberto.griggio@gmail.com " --string-input-value st restrict non-null strings to a fixed value st;\n" /* NOLINT(*) */ \ " the switch can be used multiple times to give\n" /* NOLINT(*) */ \ " several strings\n" /* NOLINT(*) */ \ - " --max-nondet-string-length n bound the length of nondet (e.g. input) strings\n" /* NOLINT(*) */ + " --max-nondet-string-length n bound the length of nondet (e.g. input) strings;\n" /* NOLINT(*) */ \ + " set to 10000 by default\n" /* NOLINT(*) */ // The integration of the string solver into CBMC is incomplete. Therefore, // it is not turned on by default and not all options are available. diff --git a/src/util/object_factory_parameters.cpp b/src/util/object_factory_parameters.cpp index 9926f6e86d9..54cae4d0088 100644 --- a/src/util/object_factory_parameters.cpp +++ b/src/util/object_factory_parameters.cpp @@ -74,6 +74,10 @@ void parse_object_factory_options(const cmdlinet &cmdline, optionst &options) "max-nondet-string-length", cmdline.get_value("max-nondet-string-length")); } + else if(!cmdline.isset("no-refine-strings")) + { + options.set_option("max-nondet-string-length", 10000); + } if(cmdline.isset("string-printable")) { options.set_option("string-printable", true); From 1e821fd2c1eb3695ecff9db3e01320ecf9cac3b8 Mon Sep 17 00:00:00 2001 From: svorenova Date: Fri, 10 May 2019 11:21:19 +0100 Subject: [PATCH 2/3] Update strings regression tests --- jbmc/regression/jbmc-strings/StringContains03/test.desc | 6 +++--- jbmc/regression/jbmc-strings/long_string/test_abort.desc | 3 ++- .../string-non-empty-option/test_non_empty.desc | 4 +++- 3 files changed, 8 insertions(+), 5 deletions(-) diff --git a/jbmc/regression/jbmc-strings/StringContains03/test.desc b/jbmc/regression/jbmc-strings/StringContains03/test.desc index c40eeaa688f..a191de45da5 100644 --- a/jbmc/regression/jbmc-strings/StringContains03/test.desc +++ b/jbmc/regression/jbmc-strings/StringContains03/test.desc @@ -1,11 +1,11 @@ CORE Test.class ---function Test.check +--function Test.check --max-nondet-string-length 1000000000 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ file Test.java line 20 .*: FAILURE$ -- -- ---max-nondet-string-length is not used on purpose, because this tests the behaviour -of string refinement on very large strings. +This tests the behaviour of string refinement on very large strings. +max-nondet-string-length is set big enough to cause an overflow. diff --git a/jbmc/regression/jbmc-strings/long_string/test_abort.desc b/jbmc/regression/jbmc-strings/long_string/test_abort.desc index 16e6b93c80d..b7f744ef549 100644 --- a/jbmc/regression/jbmc-strings/long_string/test_abort.desc +++ b/jbmc/regression/jbmc-strings/long_string/test_abort.desc @@ -1,6 +1,6 @@ CORE Test.class ---function Test.checkAbort --trace +--function Test.checkAbort --trace --max-nondet-string-length 1000000000 ^EXIT=10$ ^SIGNAL=0$ dynamic_object[0-9]*=\(assignment removed\) @@ -8,3 +8,4 @@ dynamic_object[0-9]*=\(assignment removed\) -- This tests that the object does not appear in the trace, because concretizing a string of the required length may take too much memory. +max-nondet-string-length is set big enough to cause an overflow. 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 index ce942f21ec6..4367dab85aa 100644 --- 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 @@ -1,6 +1,6 @@ CORE Test.class ---function Test.checkMinLength --string-non-empty +--function Test.checkMinLength --string-non-empty --max-nondet-string-length 2000000000 ^EXIT=10$ ^SIGNAL=0$ assertion.* line 11 function java::Test.checkMinLength.*: SUCCESS @@ -9,3 +9,5 @@ assertion.* line 17 function java::Test.checkMinLength.*: FAILURE assertion.* line 19 function java::Test.checkMinLength.*: FAILURE -- ^Building error trace +-- +max-nondet-string-length is set big enough to cause an overflow. From 15e549373651489b924a05d18f9d58de5327140a Mon Sep 17 00:00:00 2001 From: svorenova Date: Fri, 10 May 2019 15:15:28 +0100 Subject: [PATCH 3/3] Add a constant for the default max-nondet-string-length --- src/solvers/strings/string_refinement.h | 3 ++- src/util/magic.h | 2 ++ src/util/object_factory_parameters.cpp | 10 +++++++--- 3 files changed, 11 insertions(+), 4 deletions(-) diff --git a/src/solvers/strings/string_refinement.h b/src/solvers/strings/string_refinement.h index 83189522ac1..a1644bfd93d 100644 --- a/src/solvers/strings/string_refinement.h +++ b/src/solvers/strings/string_refinement.h @@ -21,6 +21,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com #define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_H #include +#include #include #include #include @@ -46,7 +47,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com " the switch can be used multiple times to give\n" /* NOLINT(*) */ \ " several strings\n" /* NOLINT(*) */ \ " --max-nondet-string-length n bound the length of nondet (e.g. input) strings;\n" /* NOLINT(*) */ \ - " set to 10000 by default\n" /* NOLINT(*) */ + " set to " + std::to_string(MAX_NONDET_STRING_LENGTH_DEFAULT) + " by default\n" /* NOLINT(*) */ // The integration of the string solver into CBMC is incomplete. Therefore, // it is not turned on by default and not all options are available. diff --git a/src/util/magic.h b/src/util/magic.h index 2f086f6cbff..24fd0d1acf5 100644 --- a/src/util/magic.h +++ b/src/util/magic.h @@ -16,4 +16,6 @@ const std::size_t MAX_CONCRETE_STRING_SIZE = 1 << 26; // The top end of the range of integers for which dstrings are precomputed constexpr std::size_t DSTRING_NUMBERS_MAX = 64; +const int MAX_NONDET_STRING_LENGTH_DEFAULT = 10000; + #endif diff --git a/src/util/object_factory_parameters.cpp b/src/util/object_factory_parameters.cpp index 54cae4d0088..a0da2a8a844 100644 --- a/src/util/object_factory_parameters.cpp +++ b/src/util/object_factory_parameters.cpp @@ -8,8 +8,9 @@ Author: Diffblue Ltd #include "object_factory_parameters.h" -#include -#include +#include "cmdline.h" +#include "magic.h" +#include "options.h" void object_factory_parameterst::set(const optionst &options) { @@ -68,6 +69,7 @@ void parse_object_factory_options(const cmdlinet &cmdline, optionst &options) options.set_option( "min-null-tree-depth", cmdline.get_value("min-null-tree-depth")); } + if(cmdline.isset("max-nondet-string-length")) { options.set_option( @@ -76,8 +78,10 @@ void parse_object_factory_options(const cmdlinet &cmdline, optionst &options) } else if(!cmdline.isset("no-refine-strings")) { - options.set_option("max-nondet-string-length", 10000); + options.set_option( + "max-nondet-string-length", MAX_NONDET_STRING_LENGTH_DEFAULT); } + if(cmdline.isset("string-printable")) { options.set_option("string-printable", true);