Add support for Java annotations with Class value #2260

antlechner · 2018-05-30T16:28:13Z

Java annotations can store element-value pairs, where each value is of type String, Enum, Class, annotation, array or a primitive type. The Class case was among the cases that did not have support in the java bytecode parser before. For minimal support (without storing any reference to java.lang.Class), we can just store the name of the type as retrieved from the constant pool in a symbol_exprt.

This feature is not used in cbmc yet, but will be used in Diffblue code soon. A unit test has been added to make sure its functionality is preserved here.

antlechner · 2018-05-30T16:47:17Z

The first 4 commits are from #2247, so only the last commit needs to be reviewed. Once #2247 has been merged I will rebase this PR.

mgudemann · 2018-05-30T17:04:12Z

jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp

+    });
+  if(annotation_it == annotations.end())
+    return {};
+  return *annotation_it;


maye use return ... ? ... : ... ; here

return (annotation_it == annotations.end()) ? {} : *annotation_it;
gives me an error, it doesn't like the {} in this notation. Is there anything I could replace it with? I've seen the two returns in other parts of the code as well...

ah, right, this is interpreted differently here. One would have to use return (annotation_it == annotations.end()) ? optionalt<java_bytecode_parse_treet::annotationt>() : *annotation_it; which isn't really shorter. So better stay with the original code.

Two returns is fine in that case. The two expressions in the ternary operator need to have the same type, but we cannot directly deduce the type of {}. Changing that to make it compile would probably be more complicated than the original if(...) return {}; return ..;.

mgudemann · 2018-05-30T17:04:34Z

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -1509,6 +1509,8 @@ void java_bytecode_parsert::relement_value_pairs(
  }
 }

+/// Corresponds to the element_value structure
+/// Described in Java 8 specification 4.7.16.1


please add link to section

mgudemann · 2018-05-30T17:04:44Z

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -1526,8 +1528,8 @@ void java_bytecode_parsert::relement_value_pair(

  case 'c':
    {
-      UNUSED u2 class_info_index=read_u2();
-      // todo: class
+      u2 class_info_index=read_u2();


mgudemann · 2018-05-30T17:06:50Z

jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp

+        const auto &element_name = element_value_pair.element_name;
+        REQUIRE(id2string(element_name) == "value");
+        const auto &expr = element_value_pair.value;
+        const auto comp_expr = from_integer(6, java_int_type());


maybe define the magic number somewhere

About this comment and the next (which are from a different PR that this one is based on, see my above comment, so please request changes on that one before it gets merged if you think this is important): I don't quite understand why they need to be defined, it's just a unit test and the numbers are some numbers I picked in the .java files?

I followed @romainbrenguier 's suggestion on #2247 and mentioned that a MyClassAnnotation(6) is being used in the WHEN line (and rebased this one on these changes).

mgudemann · 2018-05-30T17:07:12Z

jbmc/unit/java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp

+        const auto &element_name = element_value_pair.element_name;
+        REQUIRE(id2string(element_name) == "methodValue");
+        const auto &expr = element_value_pair.value;
+        const auto &comp_expr = from_integer(11, java_int_type());


Same here, mentioned MyMethodAnnotation(11) on #2247 and rebased on it here.

mgudemann · 2018-05-30T17:08:03Z

jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp

+        const auto &element_value_pair = annotation.element_value_pairs.front();
+        const auto &id = to_symbol_expr(element_value_pair.value)
+          .get_identifier();
+        REQUIRE(id2string(id) == "Ljava/lang/String;");


I would prefer having the CPROVER format for java object types here

Where can I find that? And similar to my above question: I'm not sure why using hard-coded values in unit tests is a problem?

effectively it would be java::java.lang.String in this case, not the raw JVM string. The java_type_from_string method should return a symbol type with the correct identifier in it.

The problem with java_type_from_string is that it errors if the class is not actually loaded. I'm looking for an alternative that just converts the string without checking if the type is known...
(Edit: looks like I made a mistake somewhere, it's working now so I'll change this.)

Changed it to use java_type_from_string and then compare the string in that type with java::java.langString. Does that make sense?
(The mistake I made before was to run gdb on the unit test, which randomly fails for me on various tests for some reasons even though the tests pass when I run them normally...)

mgudemann · 2018-05-30T17:09:16Z

jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp

+        const auto &element_value_pair = annotation.element_value_pairs.front();
+        const auto &id = to_symbol_expr(element_value_pair.value)
+          .get_identifier();
+        REQUIRE(id2string(id) == "B");


as above, this should probably be a CPROVER interanal java type and not the raw JVM type

in java_types.h we have

typet java_int_type(); typet java_long_type(); typet java_short_type(); typet java_byte_type(); typet java_char_type(); typet java_float_type(); typet java_double_type(); typet java_boolean_type();

Now calling java_type_to_string and comparing it with java_byte_type().

mgudemann · 2018-05-30T17:09:23Z

jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp

+        const auto &element_value_pair = annotation.element_value_pairs.front();
+        const auto &id = to_symbol_expr(element_value_pair.value)
+          .get_identifier();
+        REQUIRE(id2string(id) == "V");


Now calling java_type_to_string and comparing it with void_type().

antlechner · 2018-05-31T11:30:26Z

@mgudemann I've addressed all of your comments, could you please re-review?

antlechner · 2018-05-31T12:27:23Z

#2247 has been merged and this PR has now been rebased on develop.

mgudemann

LGTM

Java annotations can store element-value pairs, where each value is of type String, Enum, Class, annotation, array or a primitive type. The Class case was among the cases that did not have support in the java bytecode parser before. For minimal support (without storing any reference to java.lang.Class), we can just store the name of the type as retrieved from the constant pool in a symbol_exprt.

8de6a33 Merge pull request diffblue#2006 from tautschnig/opt-no-self-loops 6605699 Merge pull request diffblue#2217 from diffblue/c-preprocessing-cleanout f1d787b Merge pull request diffblue#2166 from tautschnig/out-of-bounds 25339d5 Add option not to transform self-loops into assumes 5e6a3af Merge pull request diffblue#2249 from tautschnig/attribute-used d3d888b Bounds check for flexible array members 41003e8 Handle negative byte_extract offsets efea5c4 Fix flattening of access beyond type-specified bounds 0ec87c8 Merge pull request diffblue#2271 from diffblue/letification 090790a Interpret GCC's attribute __used__ 7985716 Merge pull request diffblue#2252 from tautschnig/fresh-symbol-cleanup 022846a letify: use irep_hash_mapt when hashing is expensive 15dff7d Merge pull request diffblue#2260 from antlechner/antonia/annotation-class-value 9a0ffae added irep_hash_mapt da0adfe bugfix: irep_hash_containert now keeps a copy of the contained ireps 45436ce use std::size_t for container sizes 0c26a53 let_count_idt is now a struct e0a5142 Merge pull request diffblue#2206 from diffblue/use-get_identifier e0ad069 Add support for Java annotations with Class value 3817341 Merge pull request diffblue#2237 from smowton/smowton/feature/initialize-class-literals 25c097e use get_identifier() instead of get(ID_identifier) on symbols 4eda8ad Java class literals: init using a library hook when possible 70f13f3 Merge pull request diffblue#1906 from tautschnig/missing-return-semantics 57885a5 Merge pull request diffblue#1868 from tautschnig/fix-1867 b49822e Merge pull request diffblue#2028 from tautschnig/regression-fix 2815e84 Merge pull request diffblue#2259 from smowton/smowton/feature/note-abstract-methods 09b8cf7 Merge pull request diffblue#2014 from tautschnig/cadical-experiment f50237b Merge pull request diffblue#1967 from romainbrenguier/refactor/drop-constraint-inheritance2 3f951dd Merge pull request diffblue#2234 from nmanthey/upstream-fpr c6c2928 Drop inheritance from constraint on exprt 0ffd0ae Replace negation of constraint by a method f653dec use compiler defaults for gcc defines a31f530 remove need to do preprocessing on 16-bit test 24210e9 enable AWS Codebuild to do -m32 bfae4e3 enable Travis to do -m32 34a3d85 Merge pull request diffblue#2247 from antlechner/antonia/annotation-conversion 15ed961 Note when symbol-table entries are abstract methods 3a7135a Add module_dependencies.txt in test folder 1fa0b97 Generalize and rename does_annotation_exist 1db0af4 Define inverse function of convert_annotations ff25b2c get_max: do not parse every symbol name in the symbol table b603703 Add missing override 70da606 Merge pull request diffblue#2251 from tautschnig/rename-cleanup 49429cf Merge pull request diffblue#2257 from owen-jones-diffblue/owen-jones-diffblue/fix-cmake-macro 4b7a195 Improve naming of annotation variables 57d96e5 Fix CMake macro f9058e7 Merge pull request diffblue#2246 from diffblue/z3-fpa 6b0f265 Merge pull request diffblue#2248 from thk123/bugfix/doxygen-including-jbmc 72e99a0 Merge pull request diffblue#2201 from diffblue/remove-incomplete-type-constructors d4abbea smt2 implementation for popcount_exprt e8fa1c9 bswap_exprt now knows how many bits a byte has a6652d2 Merge pull request diffblue#2255 from tautschnig/speedup-no-pointer-check 4b0a2d6 goto_check: do not unnecessarily build size-of expressions 1fe7cd7 remove mathematical_typet() constructor, which produces an incomplete object 25d393b remove vector_typet() constructor, which produces an incomplete object e7c52e4 remove range_typet() constructor, which produces an incomplete object f92083d remove array_typet() constructor, which produces an incomplete object 72f63f3 remove tag_typet() constructor, which produces an incomplete object 516ed14 remove symbol_typet() constructor, which produces an incomplete object 4215f21 Consistently use get_fresh_aux_symbol instead of local implementations e6cd488 Remove unused goto_symext::new_name c24b820 Remove goto_convertt::lookup a816b26 Do not include rename.h when not using its functions 52ab088 called_functions: use unordered_set 157a12c Fix doxyfile to include JBMC documentation 026e93f function-pointer-removal: drop unused set b75fcbc smt2 implementation for bswap_exprt e276b27 Avoid extern/parameter name collisions in show-goto-functions/dump-c output 87c5948 C front-end: Record extern declarations in current scope a47941d perf-test: add -W/--witness-check to validate SV-COMP witness checking 5b0395f perf-test: Update Ubuntu AMI ids for latest version 1288ec7 perf-test: speed up builds just like e7bb127 did afccaec Provide goto-cc in performance tests f802d87 Support CaDiCaL in performance tests, remove redundant script 7872f7c Replace a missing return value by nondet 829068f Don't require the simplifier to solve this regression test git-subtree-dir: cbmc git-subtree-split: 8de6a33

antlechner requested review from cesaro, mgudemann, peterschrammel, smowton and thk123 as code owners May 30, 2018 16:28

antlechner force-pushed the antonia/annotation-class-value branch from 6302e84 to a1b8be2 Compare May 30, 2018 16:45

mgudemann suggested changes May 30, 2018

View reviewed changes

antlechner force-pushed the antonia/annotation-class-value branch 3 times, most recently from 0a171f3 to 47cd22c Compare May 31, 2018 11:27

antlechner force-pushed the antonia/annotation-class-value branch from 47cd22c to 9ab6f31 Compare May 31, 2018 12:26

mgudemann approved these changes May 31, 2018

View reviewed changes

antlechner force-pushed the antonia/annotation-class-value branch from 9ab6f31 to e0ad069 Compare June 1, 2018 15:28

romainbrenguier approved these changes Jun 1, 2018

View reviewed changes

romainbrenguier merged commit 15dff7d into diffblue:develop Jun 1, 2018

antlechner deleted the antonia/annotation-class-value branch June 4, 2018 09:19

Add support for Java annotations with Class value #2260

Add support for Java annotations with Class value #2260

Uh oh!

Conversation

antlechner commented May 30, 2018

Uh oh!

antlechner commented May 30, 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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

antlechner May 31, 2018 • 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!

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!

antlechner May 31, 2018 • 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!

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!

antlechner commented May 31, 2018

Uh oh!

antlechner commented May 31, 2018

Uh oh!

mgudemann left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

antlechner May 31, 2018 •

edited

Loading

antlechner May 31, 2018 •

edited

Loading