Implement model for String.equals #2588

codebyzeb · 2018-07-20T10:26:10Z

String.equals currently handled by CBMC, this removes support
within CBMC so that String.equals will be handled by a model instead.
Includes a pointer update to the definition change in the
java-models-library submodule.

codebyzeb · 2018-07-20T10:39:19Z

Pointer update to: diffblue/java-models-library#7

tautschnig · 2018-07-20T11:33:37Z

I am a nominated reviewer, but I'd hope for @romainbrenguier and @cesaro to weigh in/approve.

romainbrenguier · 2018-07-30T09:40:49Z

jbmc/regression/strings-smoke-tests/java_value_of_long/test.java

@@ -1,5 +1,5 @@
 public class test
-{
+


This is probably an involuntary change

majakusber · 2018-09-11T10:09:50Z

src/solvers/refinement/string_refinement.cpp

-      compute_inverse_function(stream, axiom.univ_var, val, index);
-    implies_exprt instance(
+      compute_inverse_function(axiom.univ_var, val, index);
+    exprt instance = implies_exprt(


Why did this change?

I removed this change

majakusber · 2018-09-11T10:10:45Z

jbmc/regression/jbmc-strings/cprover/CProverString.java

@@ -63,6 +63,14 @@ public static StringBuilder deleteCharAt(StringBuilder sb, int index) {
        return sb.deleteCharAt(index);
    }

+    public static boolean equals(String a, String b)


Why is this here in the regression folder? We are loading models library so I thought the method is implemented there now.

majakusber · 2018-09-11T10:11:09Z

src/solvers/flattening/boolbv_array.cpp


-  if(width==0)
-    return conversion_failed(expr);
+  if(operands.empty() && width == 0)


Has this been investigated?

majakusber · 2018-09-11T12:32:34Z

src/solvers/refinement/string_refinement.cpp

  exprt::operandst conjuncts;
-  for(const auto &index : indexes)
+  for(const auto &index : find_indexes(axiom.body, str, axiom.univ_var))


I'm not sure if I understood this correctly but if there is more than one index via which we access str, all of them would get replaced with the same new index var which is not correct?

If there are several indexes then we get the conjunction of the replacement.
For instance for a formula forall q. s[q+x]='a' && s[q]=c we would get s[v] = 'a' && s[v-x] = c && s[v+x] = 'a' && s[v] = c.
I will add this example to the doxygen.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 7a8e8cb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85036174
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 1f00403).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85385375
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 365d8ca).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85407757
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 408cba9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86245748
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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

allredj

This PR failed Diffblue compatibility checks (cbmc commit: a5cce05).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86248971
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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

allredj

This PR failed Diffblue compatibility checks (cbmc commit: fa07dc7).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86257728
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 9f3d360).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86437726
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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

Includes a pointer update to the definition change in the java-models-library submodule.

String.equals currently handled by CBMC, this removes support within CBMC so that String.equals will be handled by a model instead. CProverString.equals is provided by JBMC instead of String.equals.

The thing we warn about is not an error in itself and it's unlikely the user will understand what this talks about.

The fact that the array is always accessed at the same index, is not a necessary condition for the correctness of the instantiate function.

romainbrenguier · 2018-10-01T14:45:00Z

submodule update now pointing to master

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 87bd027).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86492208
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

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

codebyzeb requested review from cesaro, chrisr-diffblue, kroening, mgudemann, peterschrammel, smowton, tautschnig and thk123 as code owners July 20, 2018 10:26

allredj requested a review from romainbrenguier July 20, 2018 10:32

codebyzeb force-pushed the zgoriely/string-equals branch from 4e8ab5d to 2ba1c31 Compare July 20, 2018 10:36

tautschnig assigned cesaro, romainbrenguier and codebyzeb Jul 20, 2018

codebyzeb force-pushed the zgoriely/string-equals branch from 2ba1c31 to 759e25c Compare July 20, 2018 15:27

allredj added In progress do not merge labels Jul 22, 2018

codebyzeb force-pushed the zgoriely/string-equals branch 2 times, most recently from c333e35 to 6a07c37 Compare July 23, 2018 10:55

romainbrenguier reviewed Jul 30, 2018

View reviewed changes

romainbrenguier force-pushed the zgoriely/string-equals branch from 6a07c37 to c37762f Compare August 1, 2018 07:47

codebyzeb requested review from cristina-david, NathanJPhillips and pkesseli as code owners August 1, 2018 07:47

romainbrenguier force-pushed the zgoriely/string-equals branch 5 times, most recently from e0a5597 to 444c186 Compare August 6, 2018 10:10

majakusber reviewed Sep 11, 2018

View reviewed changes

antlechner unassigned codebyzeb Sep 13, 2018

romainbrenguier force-pushed the zgoriely/string-equals branch from 29bbb88 to 7a8e8cb Compare September 17, 2018 15:27

allredj reviewed Sep 17, 2018

View reviewed changes

romainbrenguier force-pushed the zgoriely/string-equals branch from 7a8e8cb to 1f00403 Compare September 20, 2018 06:05

allredj reviewed Sep 20, 2018

View reviewed changes

romainbrenguier force-pushed the zgoriely/string-equals branch from 1f00403 to 365d8ca Compare September 20, 2018 09:14

allredj reviewed Sep 20, 2018

View reviewed changes

romainbrenguier force-pushed the zgoriely/string-equals branch 2 times, most recently from 408cba9 to a5cce05 Compare September 28, 2018 06:56

allredj reviewed Sep 28, 2018

View reviewed changes

romainbrenguier force-pushed the zgoriely/string-equals branch 3 times, most recently from af56a9b to 9f3d360 Compare October 1, 2018 08:16

allredj reviewed Oct 1, 2018

View reviewed changes

majakusber approved these changes Oct 1, 2018

View reviewed changes

codebyzeb and others added 8 commits October 1, 2018 15:43

Update java-models-library submodule

1b349ed

Includes a pointer update to the definition change in the java-models-library submodule.

Allow empty arrays in convert_array

77131c0

Use java models in String tests

968c239

Stop preprocessing String.equals

7e53e6e

String.equals currently handled by CBMC, this removes support within CBMC so that String.equals will be handled by a model instead. CProverString.equals is provided by JBMC instead of String.equals.

Stop output of useless warning

6d153a2

The thing we warn about is not an error in itself and it's unlikely the user will understand what this talks about.

Relax condition in instantiate

ff740ef

The fact that the array is always accessed at the same index, is not a necessary condition for the correctness of the instantiate function.

Improve documentation of instantiate

a485739

Use java-models-library instead of java_bycode/library

87bd027

romainbrenguier force-pushed the zgoriely/string-equals branch from 9f3d360 to 87bd027 Compare October 1, 2018 14:44

romainbrenguier merged commit 46cd50b into diffblue:develop Oct 1, 2018

allredj reviewed Oct 1, 2018

View reviewed changes

Implement model for String.equals #2588

Implement model for String.equals #2588

Uh oh!

Conversation

codebyzeb commented Jul 20, 2018

Uh oh!

codebyzeb commented Jul 20, 2018

Uh oh!

tautschnig commented Jul 20, 2018

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!

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

romainbrenguier commented Oct 1, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!