Set max-nondet-string-length to 10000 by default #4643

majakusber · 2019-05-10T09:35:12Z

Unless no-refine-strings is defined. If no max-nondet-string-length is set and a long string is generated, it gets discarded in the trace which causes problems in test-gen trace interpreter.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

romainbrenguier · 2019-05-10T12:32:28Z

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 1000000000


This is not big enough to cause an overflow (which is what one of the assertion is checking here), the maximum java integer is 2147483647 so you should use at least half that, 2000000000 should work

I agree with @romainbrenguier about the overflow. However, if this is about finding overflows / checking if they occur, please could it say that somewhere in the test or the commit message.

Thank you, I adjusted the value

The java file already say:

// 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;

maybe the desc file should mention that we explicitly set the length limit high to be able to detect overflow behaviors.

I added explanation to the .desc files about the overflow

martin-cs

Seems reasonable in principle but if there are overflow issues, I would rather they were actually documented / discussed.

martin-cs · 2019-05-10T13:13:31Z

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 1000000000


I agree with @romainbrenguier about the overflow. However, if this is about finding overflows / checking if they occur, please could it say that somewhere in the test or the commit message.

src/solvers/strings/string_refinement.h

martin-cs · 2019-05-10T13:21:20Z

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);


Why 10,000? Does this affect performance? If so is this a good choice? Creating an array of 10,000 16-bit characters is a non-trivial amount for the SAT solver to handle.

As documented here: https://github.com/diffblue/test-gen/blob/develop/doc/cl-options.md
The performance should not be affected in any significant way. The value is anyway recommended to be set, so setting the default value is only to make sure that we do not trip over it if we forget.

Has the option any effect if no-refine-strings is specified?

No, the two options cannot be specified together:

cbmc/jbmc/src/jbmc/jbmc_parse_options.cpp

Line 281 in 88f2a96

if(

@svorenova : I don't have access to that documentation.

@martin-cs Here is screenshot:

That sounds like an argument for it to be 100 rather than 10000.

I think that's because the doc is more concerned with test-generation than verification. If you are interested in the trace generated by jbmc it's better to use a reasonable value like 100, otherwise you can set it as high as you want.

peterschrammel · 2019-05-10T13:26:01Z

jbmc/regression/jbmc-strings/StringContains03/test.desc

 ^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.
+>his tests the behaviour of string refinement on very large strings.


peterschrammel · 2019-05-10T13:43:19Z

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);


Has the option any effect if no-refine-strings is specified?

Unless no-refine-strings is defined

majakusber · 2019-05-10T14:24:00Z

@peterschrammel @martin-cs @romainbrenguier Ready for re-review. Please note that this is high priority as it's needed for a long-overdue test-gen bump.

romainbrenguier · 2019-05-10T14:43:38Z

src/util/object_factory_parameters.cpp

@@ -8,6 +8,7 @@ Author: Diffblue Ltd

 #include "object_factory_parameters.h"

+#include <solvers/strings/max_nondet_string_length_default.h>


solvers is not the right module for this file (util shouldn't depend on solvers).
Consider moving the definition to util/magic.h

Makes sense, moved

smowton

LGTM, one formatting suggestion

smowton · 2019-05-10T15:39:04Z

src/util/object_factory_parameters.cpp

@@ -74,6 +74,11 @@ 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"))


Suggest add blank lines to make clear we've hidden an if/else amongst this sequence of ifs

I get your point, although I would really like to merge this PR and the test-gen bump today (to avoid even more accumulation for the bump over the weekend) so I will not update this.

Suggested change

else if(!cmdline.isset("no-refine-strings"))

else

I don't think the if part is needed.

That would cause the max length to be bounded if --no-refine-strings is given which I think is not desired. And it would be bounded by a reasonably small value. If anyone would like to increase it, while keeping --no-refine-strings, they would get an error as one cannot define both options at the same time.

@smowton I had to restart the CI anyway so I applied your suggestion

peterschrammel · 2019-05-10T15:51:25Z

src/util/object_factory_parameters.cpp

@@ -74,6 +74,11 @@ 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"))


Suggested change

else if(!cmdline.isset("no-refine-strings"))

else

I don't think the if part is needed.

martin-cs

The docs seem to indicate that a lower value would be better but ... that's between you and the major users of this, which is not me so approve.

tautschnig · 2019-05-13T11:01:57Z

I'm obviously late to the party, but I'm not particularly pleased with this fixed bound. My concern, in line with what @martin-cs and @romainbrenguier said is that there does not seem to be any rationale provided as to why it is the most appropriate number. Now we seem to be in a situation where the string length cannot be set to be unbounded anymore?

majakusber · 2019-05-13T11:20:48Z

@tautschnig To use unbounded length, you could use either --no-refine-strings (which however means that no other string refinement options can be used either, namely --string-printable and --string-input-value) or you can set the bound high enough to allow overflow, see @romainbrenguier's comment here: #4643 (comment)

In any case, I'm happy to change the value to what makes the most sense to both CBMC and test-gen users. I do like the idea of having a default value though - I have wasted quite some time trying to debug a failing test before realizing (with the help of Romain) that the problem was the overflow.

The reason why I chose the bound 10000 rather than 100 is that I wanted to restrict the length as little as possible comparing to the unbound length (previous default). And according to the doc, this is the largest number that should still have little effect on performance.

romainbrenguier · 2019-05-13T11:31:47Z

In any case, I'm happy to change the value to what makes the most sense to both CBMC and test-gen users.

You could have different ones for test-gen and CBMC I guess, in particular not having one for CBMC is maybe better.

majakusber · 2019-05-16T09:07:01Z

@romainbrenguier Good idea, I will shortly open a PR for revert and a test-gen PR introducing the bound.

majakusber requested review from kroening, martin-cs, peterschrammel, pkesseli, romainbrenguier, smowton and tautschnig as code owners May 10, 2019 09:35

majakusber self-assigned this May 10, 2019

majakusber force-pushed the max-nondet-string-length-default branch 2 times, most recently from 9b2b116 to e63b6ed Compare May 10, 2019 10:36

owen-mc-diffblue approved these changes May 10, 2019

View reviewed changes

romainbrenguier reviewed May 10, 2019

View reviewed changes

majakusber force-pushed the max-nondet-string-length-default branch from e63b6ed to dd973d1 Compare May 10, 2019 13:18

martin-cs reviewed May 10, 2019

View reviewed changes

peterschrammel reviewed May 10, 2019

View reviewed changes

svorenova added 2 commits May 10, 2019 15:18

Set max-nondet-string-length to 10000 by default

c66e886

Unless no-refine-strings is defined

Update strings regression tests

1e821fd

majakusber force-pushed the max-nondet-string-length-default branch from dd973d1 to 364af8d Compare May 10, 2019 14:18

majakusber force-pushed the max-nondet-string-length-default branch from 364af8d to 2296946 Compare May 10, 2019 14:40

romainbrenguier reviewed May 10, 2019

View reviewed changes

majakusber force-pushed the max-nondet-string-length-default branch from 2296946 to 72be726 Compare May 10, 2019 14:57

smowton approved these changes May 10, 2019

View reviewed changes

peterschrammel approved these changes May 10, 2019

View reviewed changes

Add a constant for the default max-nondet-string-length

15e5493

majakusber force-pushed the max-nondet-string-length-default branch from 72be726 to 15e5493 Compare May 10, 2019 16:02

martin-cs approved these changes May 10, 2019

View reviewed changes

majakusber merged commit 9fd7dd4 into diffblue:develop May 10, 2019

majakusber deleted the max-nondet-string-length-default branch May 10, 2019 17:52

majakusber mentioned this pull request May 16, 2019

Revert "Set max-nondet-string-length to 10000 by default" #4660

Merged

		@@ -8,6 +8,7 @@ Author: Diffblue Ltd

		#include "object_factory_parameters.h"

		#include <solvers/strings/max_nondet_string_length_default.h>

Set max-nondet-string-length to 10000 by default #4643

Set max-nondet-string-length to 10000 by default #4643

Uh oh!

Conversation

majakusber commented May 10, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

majakusber commented May 10, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

majakusber May 10, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented May 13, 2019

Uh oh!

majakusber commented May 13, 2019

Uh oh!

romainbrenguier commented May 13, 2019

Uh oh!

majakusber commented May 16, 2019

Uh oh!

majakusber commented May 10, 2019 •

edited

Loading

majakusber commented May 10, 2019 •

edited

Loading

majakusber May 10, 2019 •

edited

Loading