Load static initializers for enum types returned by opaque methods #3124

antlechner · 2018-10-08T16:32:39Z

Each commit message has a non-empty body, explaining why the change was made.
My contribution is formatted in line with CODING_STANDARD.md.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
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). [Not 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. [None.]

Previously static initializers for enum types were only loaded for those types that are reachable from the arguments to the entry method.
This would lead to an invariant violation when an opaque method returned an enum type (which needs to be nondet-initialized just like arguments to the entry method).
This PR solves this problem by moving the code for marking the static initializers of enums as loaded from ci_lazy_methods to ci_lazy_methods_needed, and applying it to all deterministic and
nondeterministic enums that are reachable in some way from the entry method.
Including deterministic enums is not a problem, since we load static initializers for all types (enums and others) whose constructor we use anyway.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 5bad705).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87232902
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 · 2018-10-09T07:37:55Z

@antlechner, Looks good. Do you have a TG bump?

allredj · 2018-10-09T08:18:28Z

OK, found it: https://github.com/diffblue/test-gen/pull/2361

smowton

Couple of questions to check, generally lgtm

smowton · 2018-10-09T08:19:20Z

jbmc/regression/jbmc/NondetEnumOpaqueReturn/NondetEnumOpaqueReturn.java

+    if (c == null)
+      return;
+    assert c != null;
+    boolean isRed = c.name().startsWith("RED") && c.name().length() == 3


startsWith -> equals?

It's equivalent, yes, (and you wouldn't need c.name().length() == 3) but pointer analysis doesn't cope very well with equals because it's defined in Object and overridden almost everywhere.

🚫 This looks like a workaround.equals also has to work...

@smowton @peterschrammel I originally had equals in my original enum tests but @romainbrenguier suggested that I use startsWith and length instead because it's quicker, and we don't want these tests to take too long. equals would work as well, it would just take a bit longer I think.

I'm fine with that as long as we are sure that equals works as well (but takes a bit longer).

I checked locally just to be sure, and using equals works too, all the tests would pass with that. I'll leave the tests as they are, since they are testing properties of the returned enums, not String methods, and it's better to save a bit of time here.

smowton · 2018-10-09T08:19:47Z

jbmc/regression/jbmc/NondetEnumOpaqueReturn/NondetEnumOpaqueReturn.java

+      && c.ordinal() == 1;
+    boolean isBlue = c.name().startsWith("BLUE") && c.name().length() == 4
+      && c.ordinal() == 2;
+    assert (isGreen || isBlue);


Why are these negative assertions but canChooseSomeConstant is a positive assertion?

Positive assertions check for correctness whereas negative assertions check for reachability (as unreachable assertions cannot be violated by cbmc).

Yes, the positive assertion checks that jbmc will always choose something in the set of the three constants, and the negative assertions check that for any two given constants, there is something else that it can choose (namely, the third constant).

peterschrammel · 2018-10-09T09:02:06Z

jbmc/regression/jbmc/NondetEnumOpaqueReturn/NondetEnumOpaqueReturn.java

+    if (c == null)
+      return;
+    assert c != null;
+    boolean isRed = c.name().startsWith("RED") && c.name().length() == 3


🚫 This looks like a workaround.equals also has to work...

peterschrammel · 2018-10-09T09:03:51Z

jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp

@@ -42,6 +61,14 @@ bool ci_lazy_methods_neededt::add_needed_class(
  if(symbol_table.symbols.count(cprover_validate))
    add_needed_method(cprover_validate);

+  // Special case for enums. We may want to generalise this, see TG-4689
+  // and the comment in java_object_factoryt::gen_nondet_pointer_init.
+  namespacet ns{symbol_table};


Copy-pasted from another function in this file, but () is probably better so I changed it to that, thanks.

peterschrammel · 2018-10-09T09:04:57Z

jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp

@@ -42,6 +61,14 @@ bool ci_lazy_methods_neededt::add_needed_class(
  if(symbol_table.symbols.count(cprover_validate))
    add_needed_method(cprover_validate);

+  // Special case for enums. We may want to generalise this, see TG-4689


Generalise in what way? Since this is in JBMC, the TG reference is not very helpful.

There is a link to java_object_factoryt::gen_nondet_pointer_init, which has more details. I slightly rephrased this comment, putting the link first and the ticket number only afterwards in brackets so it's clearer that you don't actually need access to the ticket to work on this.

peterschrammel · 2018-10-09T12:24:23Z

https://travis-ci.org/diffblue/cbmc/jobs/439057461#L520

Previously static initializers for enum types were only loaded for those types that are reachable from the arguments to the entry method. This would lead to an invariant violation when an opaque method returned an enum type (which needs to be nondet-initialized just like arguments to the entry method). This commit solves this problem by moving the code for marking the static initializers of enums as loaded from ci_lazy_methods to ci_lazy_methods_needed, and applying it to all deterministic and nondeterministic enums that are reachable in some way from the entry method. Including deterministic enums is not a problem, since we load static initializers for all types (enums and others) whose constructor we use anyway.

The tests were copied from jbmc/regression/jbmc/NondetEnumArg and adapted for the case where the enum is returned by an opaque method (Opaque.class has been deleted).

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 06b2f80).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87335833
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

Passed Diffblue compatibility checks (cbmc commit: f9da0bd).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87344796

antlechner self-assigned this Oct 8, 2018

antlechner requested review from smowton, thk123 and allredj October 8, 2018 16:32

antlechner requested review from cesaro, cristina-david, NathanJPhillips, peterschrammel and pkesseli as code owners October 8, 2018 16:32

allredj reviewed Oct 8, 2018

View reviewed changes

smowton approved these changes Oct 9, 2018

View reviewed changes

peterschrammel reviewed Oct 9, 2018

View reviewed changes

antlechner force-pushed the stub-return-enum branch from 5bad705 to 06b2f80 Compare October 9, 2018 10:02

peterschrammel approved these changes Oct 9, 2018

View reviewed changes

antlechner added 2 commits October 9, 2018 13:38

Add tests for enums returned by opaque methods

f9da0bd

The tests were copied from jbmc/regression/jbmc/NondetEnumArg and adapted for the case where the enum is returned by an opaque method (Opaque.class has been deleted).

antlechner force-pushed the stub-return-enum branch from 06b2f80 to f9da0bd Compare October 9, 2018 12:38

allredj reviewed Oct 9, 2018

View reviewed changes

antlechner merged commit 9ce6a06 into diffblue:develop Oct 9, 2018

antlechner deleted the stub-return-enum branch October 9, 2018 17:04

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Load static initializers for enum types returned by opaque methods #3124

Load static initializers for enum types returned by opaque methods #3124

antlechner commented Oct 8, 2018

allredj left a comment

allredj commented Oct 9, 2018

allredj commented Oct 9, 2018

smowton left a comment

smowton Oct 9, 2018

allredj Oct 9, 2018

peterschrammel Oct 9, 2018

antlechner Oct 9, 2018

peterschrammel Oct 9, 2018

antlechner Oct 9, 2018

smowton Oct 9, 2018

allredj Oct 9, 2018

antlechner Oct 9, 2018

peterschrammel Oct 9, 2018

peterschrammel Oct 9, 2018

antlechner Oct 9, 2018

peterschrammel Oct 9, 2018

antlechner Oct 9, 2018

peterschrammel commented Oct 9, 2018

allredj left a comment

allredj left a comment

Load static initializers for enum types returned by opaque methods #3124

Load static initializers for enum types returned by opaque methods #3124

Conversation

antlechner commented Oct 8, 2018

allredj left a comment

Choose a reason for hiding this comment

allredj commented Oct 9, 2018

allredj commented Oct 9, 2018

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel commented Oct 9, 2018

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment