[TG-7648] Constant propagation of substring operations #4941

danpoe · 2019-07-23T15:58:35Z

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.
n/a 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).
n/a 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.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: eaeadb6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/120411659

…g-concatenation [TG-8293] Constant propagation for empty strings and string concatenation [blocks: #4941]

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 415535e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/122582457
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

smowton · 2019-08-13T08:01:51Z

jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation1/Main.java

+    String s5 = sb.substring(0, 1);
+    assert s5.length() == 1;
+    assert s5.startsWith("a");
+  }


Additionally check that out-of-range begin- or end-indices still throw as expected?

@smowton Exceptions are a thing of the model library. There are already a couple of tests there:
https://github.com/diffblue/models-library/blob/develop/modelTests/maven/java/lang/String/src/main/java/L1Substring_int.java
https://github.com/diffblue/models-library/blob/develop/modelTests/maven/java/lang/String/src/main/java/L1Substring_int_int.java
which seem sufficient to me.

Of course these would only fail when the test-gen bump is updated, but I don't see how they coiuld.

I think @smowton is referring to the case where all the arguments to substring() are constant, but the indices are out of bounds. In this case the constant propagator should not simplify anything and the statement should just be symex'd normally. Whether that then later leads to an exception is a thing of the models library. I'll add a test to check that no simplification occurs for out of bounds indices.

smowton · 2019-08-13T08:02:29Z

jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test3.desc

@@ -0,0 +1,9 @@
+CORE symex-driven-lazy-loading-expected-failure


Any idea why the xfail?

When using symex driven lazy loading it seems that jbmc does not fully honor the --property option as several additional VCCs are generated (e.g. null pointer checks). Those regression tests though check that a specific VCC is not simplified. This is currently done by selecting that VCC via --property and then checking that jbmc prints Generated 1 VCC(s), 1 remaining after simplification. If there would be more VCCs we could not check that this one VCC is the one that is not simplified.

smowton · 2019-08-13T08:03:02Z

src/goto-symex/goto_symex.cpp

@@ -310,6 +314,26 @@ goto_symext::try_evaluate_constant_string(
  return try_get_string_data_array(s_pointer_opt->get(), ns);
 }

+optionalt<std::reference_wrapper<const constant_exprt>>


optionalt<reference_wrapper<T>> -> T*

It was suggested in a previous PR to use optional references as they provide some additional semantic information. I don't really mind either way but we should be consistent about it.

I don't think there is a semantic difference, a reference wrapper is basically a pointer that can't be null, by making it optional you can get the empty optional which is basically equivalent to a null pointer, so it's just a verbose way of saying the same thing.

Yes, I agree that they behave the same. What I meant was that when using an optionalt it's clear from the signature of the method that it returns an optional value, whereas when using a plain pointer that's not necessarily clear.

I suppose I would always assume a pointer might be null, otherwise you'd use a reference

Sure, though a nullpointer return value could suggest that some kind of error has occured, whereas optionalt would suggest that this is part of normal and expected behavior.

allredj · 2019-08-13T08:19:38Z

jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation1/Main.java

+    String s5 = sb.substring(0, 1);
+    assert s5.length() == 1;
+    assert s5.startsWith("a");
+  }


@smowton Exceptions are a thing of the model library. There are already a couple of tests there:
https://github.com/diffblue/models-library/blob/develop/modelTests/maven/java/lang/String/src/main/java/L1Substring_int.java
https://github.com/diffblue/models-library/blob/develop/modelTests/maven/java/lang/String/src/main/java/L1Substring_int_int.java
which seem sufficient to me.

Of course these would only fail when the test-gen bump is updated, but I don't see how they coiuld.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: e0ef78e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/123016840

This implements constant propagation of ID_cprover_string_substring_func function application expressions. These are in turn used by the various substring operations of String and StringBuilder.

… tests Add regression tests that check that the constant propagator does not simplify substring() invocations with only constant arguments when the indices are out of bounds.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 7da4f78).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/123397270
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: e56041f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/123399979

danpoe requested review from kroening, martin-cs, peterschrammel, pkesseli, romainbrenguier, smowton and tautschnig as code owners July 23, 2019 15:58

danpoe added the dependent - do not merge label Jul 23, 2019

danpoe changed the title ~~Constant propagation of substring operations~~ Constant propagation of substring operations [depends-on: #4885] Jul 23, 2019

danpoe force-pushed the feature/constant-propagate-string-substring branch from 9c03585 to eaeadb6 Compare July 23, 2019 16:07

allredj reviewed Jul 24, 2019

View reviewed changes

danpoe changed the title ~~Constant propagation of substring operations [depends-on: #4885]~~ [TG-7648] Constant propagation of substring operations [depends-on: #4885] Jul 25, 2019

danpoe added a commit that referenced this pull request Aug 8, 2019

Merge pull request #4885 from danpoe/feature/constant-propagate-strin…

aa5fcda

…g-concatenation [TG-8293] Constant propagation for empty strings and string concatenation [blocks: #4941]

danpoe force-pushed the feature/constant-propagate-string-substring branch from eaeadb6 to a006aae Compare August 8, 2019 13:54

danpoe removed the dependent - do not merge label Aug 8, 2019

danpoe changed the title ~~[TG-7648] Constant propagation of substring operations [depends-on: #4885]~~ [TG-7648] Constant propagation of substring operations Aug 8, 2019

danpoe force-pushed the feature/constant-propagate-string-substring branch 6 times, most recently from 4b31584 to 415535e Compare August 9, 2019 10:36

allredj reviewed Aug 9, 2019

View reviewed changes

smowton approved these changes Aug 13, 2019

View reviewed changes

allredj approved these changes Aug 13, 2019

View reviewed changes

danpoe force-pushed the feature/constant-propagate-string-substring branch from 415535e to e0ef78e Compare August 13, 2019 15:24

allredj reviewed Aug 13, 2019

View reviewed changes

danpoe force-pushed the feature/constant-propagate-string-substring branch from e0ef78e to 7da4f78 Compare August 15, 2019 14:33

Implement constant propagation for substring operations

8f9a9c7

This implements constant propagation of ID_cprover_string_substring_func function application expressions. These are in turn used by the various substring operations of String and StringBuilder.

danpoe force-pushed the feature/constant-propagate-string-substring branch from 7da4f78 to e56041f Compare August 15, 2019 14:50

Add String.substring() and StringBuilder.substring() regression error…

e56041f

… tests Add regression tests that check that the constant propagator does not simplify substring() invocations with only constant arguments when the indices are out of bounds.

allredj reviewed Aug 15, 2019

View reviewed changes

danpoe merged commit 744671a into diffblue:develop Aug 15, 2019

allredj reviewed Aug 15, 2019

View reviewed changes

danpoe deleted the feature/constant-propagate-string-substring branch June 2, 2020 17:17

		@@ -0,0 +1,9 @@
		CORE symex-driven-lazy-loading-expected-failure

[TG-7648] Constant propagation of substring operations #4941

[TG-7648] Constant propagation of substring operations #4941

Uh oh!

Conversation

danpoe commented Jul 23, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj 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!

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

danpoe commented Jul 23, 2019 •

edited

Loading