Include annotations in Java class loading [TG-3831] #3227

antlechner · 2018-10-25T16:21:19Z

Each commit message has a non-empty body, explaining why the change was made. [Except for tests and comment changes.]
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.

For every class, field and method annotation that we see in our initial dependency analysis, we load the class that the annotation is defined in as well as all types of the values it stores.

This can be useful for when we use annotations to analyze properties related to certain classes, or to force-load certain classes.

Currently no such annotations are defined in the cbmc repository, but we are using them in Diffblue code.

NathanJPhillips

This seems like a good PR, fixing the situation where annotations use pointers to types that are not available in the symbol table.

NathanJPhillips · 2018-10-25T16:25:17Z

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -570,6 +576,7 @@ void java_bytecode_parsert::get_class_refs()

  for(const auto &method : parse_tree.parsed_class.methods)
  {
+    get_annotation_refs(method.annotations);


You may also like to iterate over the method parameters and grab the annotations from those too.

Done. I also added tests for that.

NathanJPhillips · 2018-10-25T16:25:54Z

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -603,6 +610,43 @@ void java_bytecode_parsert::get_class_refs()
  }
 }

+/// For each of the given annotations, get a reference to its class and
+/// recursively get class references of the values it stores.
+void java_bytecode_parsert::get_annotation_refs(


Maybe get_annotation_class_refs as it's not references to the annotation that you're getting.

NathanJPhillips · 2018-10-25T16:26:40Z

jbmc/src/java_bytecode/java_bytecode_parser.cpp

+    get_class_refs_rec(annotation.type);
+    for(const auto &element_value_pair : annotation.element_value_pairs)
+    {
+      const exprt &value = element_value_pair.value;


Do we need this abbreviation? Perhaps inline it.

NathanJPhillips · 2018-10-25T16:28:01Z

jbmc/src/java_bytecode/java_bytecode_parser.cpp

+    const typet value_type = java_type_from_string(id2string(value_id));
+    get_class_refs_rec(value_type);
+  }
+  if(const auto &array_expr = expr_try_dynamic_cast<array_exprt>(value))


An else here would shortcut the check.

But that could lead to unexpected behaviour if the todos in get_relement_value are addressed but the ones in this function are not? Since an enum or annotation (in the nested annotation case) could be passed as an argument to this function, so just because the argument is not a symbol_exprt, we can't just assume that it's an array_exprt.

How about else if then?

Yes, I meant an else if, not just an else.

Changed if to else if.
Also moved the new functions below get_class_refs_rec so get_class_refs and get_class_refs_rec are together.

NathanJPhillips · 2018-10-25T16:28:09Z

jbmc/src/java_bytecode/java_bytecode_parser.cpp

+/// See \ref java_bytecode_parsert::get_annotation_refs.
+/// For the different cases of `exprt`, see \ref
+/// java_bytecode_parsert::get_relement_value.
+void java_bytecode_parsert::get_annotation_refs_rec(const exprt &value)


Perhaps get_annotation_value_class_refs?

NathanJPhillips · 2018-10-25T16:31:24Z

jbmc/src/java_bytecode/java_bytecode_parser.cpp

+    for(const exprt &operand : array_expr->operands())
+      get_annotation_refs_rec(operand);
+  }
+  // TODO: enum and annotation cases


annotation -> nested annotation
Add suffix " (once these are correctly parsed by get_relement_value)"

allredj

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

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

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

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

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

majakusber

Looks good, just minor comments. And I learned about annotations on the way 😉

majakusber · 2018-10-26T14:06:26Z

jbmc/src/java_bytecode/java_bytecode_parser.cpp

+    const typet value_type = java_type_from_string(id2string(value_id));
+    get_class_refs_rec(value_type);
+  }
+  if(const auto &array_expr = expr_try_dynamic_cast<array_exprt>(value))


How about else if then?

jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-method.desc

NathanJPhillips

Clarified my earlier suggestion but Approve anyway whether or not you implement this.

NathanJPhillips · 2018-10-26T17:08:35Z

jbmc/src/java_bytecode/java_bytecode_parser.cpp

+    const typet value_type = java_type_from_string(id2string(value_id));
+    get_class_refs_rec(value_type);
+  }
+  if(const auto &array_expr = expr_try_dynamic_cast<array_exprt>(value))


Yes, I meant an else if, not just an else.

allredj

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

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

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

allredj · 2018-10-29T09:53:17Z

jbmc/regression/jbmc/class-loading-annotations/ClassValueAnnotationOnParameter.java

@@ -0,0 +1,4 @@
+public class ClassValueAnnotationOnParameter {
+  public void classValueAnnotatedParameter(
+      @AnnotationWithClassValue(MyClassA.class) int param) {}


⛏️ indent

allredj · 2018-10-29T09:55:28Z

jbmc/regression/jbmc/class-loading-annotations/test-class-value-annotation-on-class.desc

+--verbosity 10
+Getting class `MyClassA' from file \.[\\/]MyClassA\.class
+--
+Getting class `MyClassB' from file \.[\\/]MyClassB\.class


⛏️ 💡 In general I try to be more cautious about the regexes in the non-matching part (because a single type could make the test useless). Consider replacing with Getting class 'MyClassB'.

Good point. Replaced the non-matching regexes with just MyClassB.

allredj

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

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

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

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

antlechner · 2018-10-30T12:30:02Z

cbmc/develop is incompatible with Diffblue products, so this PR will have to wait for a fix.

For every class, field and method annotation that we see in our initial dependency analysis, we load the class that the annotation is defined in as well as all types of the values it stores. This can be useful for when we use annotations to analyze properties related to certain classes, or to force-load certain classes.

allredj

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

antlechner requested review from smowton and NathanJPhillips October 25, 2018 16:21

antlechner requested review from cesaro, cristina-david, peterschrammel, pkesseli and thk123 as code owners October 25, 2018 16:21

antlechner changed the title ~~Include annotations in Java class loading~~ Include annotations in Java class loading [TG-3831] Oct 25, 2018

NathanJPhillips reviewed Oct 25, 2018

View reviewed changes

antlechner force-pushed the load-annotation-classes branch from e835fd7 to 01925c4 Compare October 25, 2018 16:51

allredj reviewed Oct 25, 2018

View reviewed changes

antlechner force-pushed the load-annotation-classes branch from 01925c4 to 6fce632 Compare October 25, 2018 17:21

antlechner requested a review from NathanJPhillips October 25, 2018 17:22

allredj reviewed Oct 25, 2018

View reviewed changes

majakusber assigned antlechner Oct 26, 2018

majakusber approved these changes Oct 26, 2018

View reviewed changes

antlechner added the do not merge label Oct 26, 2018

NathanJPhillips approved these changes Oct 26, 2018

View reviewed changes

antlechner force-pushed the load-annotation-classes branch 2 times, most recently from d3561d3 to 080f05e Compare October 26, 2018 17:29

allredj reviewed Oct 26, 2018

View reviewed changes

allredj approved these changes Oct 29, 2018

View reviewed changes

antlechner force-pushed the load-annotation-classes branch from 080f05e to 2c4b05b Compare October 29, 2018 20:18

allredj reviewed Oct 29, 2018

View reviewed changes

antlechner force-pushed the load-annotation-classes branch from 2c4b05b to c51be4d Compare October 30, 2018 10:26

antlechner removed the do not merge label Oct 30, 2018

allredj reviewed Oct 30, 2018

View reviewed changes

antlechner added the do not merge label Oct 30, 2018

antlechner added 3 commits October 30, 2018 18:33

Turn get_class_refs comment into Doxygen

8e346dd

Add tests for loading of types in annotations

48d9e44

antlechner force-pushed the load-annotation-classes branch from c51be4d to 48d9e44 Compare October 30, 2018 18:33

antlechner removed the do not merge label Oct 30, 2018

allredj reviewed Oct 30, 2018

View reviewed changes

antlechner merged commit 26df513 into diffblue:develop Oct 31, 2018

antlechner deleted the load-annotation-classes branch October 31, 2018 10:25

Include annotations in Java class loading [TG-3831] #3227

Include annotations in Java class loading [TG-3831] #3227

Uh oh!

Conversation

antlechner commented Oct 25, 2018

Uh oh!

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

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!

majakusber left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

NathanJPhillips left a comment

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!

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!

antlechner commented Oct 30, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!