Java class literals: init using a library hook when possible #2237

smowton · 2018-05-24T17:11:03Z

The Java library definition of java.lang.Class, when nondet initialized, can be quite time
consuming due to the enumeration constant dictionary's internal array. Instead, let's give
the library a chance to set Class constants (literals like MyClass.class) itself.

While we're at it we might as well gain the ability to prove some properties of the literals.
We currently supply those class attributes that are easy to come by in the parse tree; with a
little more effort in the parser IsLocalClass and IsMemberClass could be determined, and
the String literal for the name requires just a little more effort too.

peterschrammel · 2018-05-24T17:24:00Z

jbmc/src/java_bytecode/java_entry_point.cpp

+          name_str.substr(0, name_str.size() - strlen("@class_model"));
+        const symbolt &class_symbol = symbol_table.lookup_ref(class_name);
+
+        bool class_is_array = has_prefix(name_str, "java::array[");


Use is_java_array_tag() from java_types.h

peterschrammel · 2018-05-24T17:25:00Z

src/util/irep_ids.def

 IREP_ID_TWO(C_annotations, #annotations)
 IREP_ID_ONE(final)
+IREP_ID_ONE(synthetic)
+IREP_ID_ONE(interface)


Do we have to distinguish interfaces and abstract classes?

Even if there isn't a feature we know about yet for which we have to distinguish between between interfaces and abstract classes, I think it is worth preserving this information from the class files. Otherwise we may have to return to this later to separate one flag into two.

We currently tag interface types with ID_abstract. If we want to change this, the distinction needs to be made in all places where we use ID_abstract.

I agree with Tom and since is ID_abstract field is left unchanged by this PR I think nothing needs updating (I suppose interfaces are marked as abstract in the bytecode).

Agree with @thk123 -- interfaces are abstract, not all abstract things are interfaces, so I think this does the right thing already.

thk123

Missing desc file but otherwise LGTM

thk123 · 2018-05-25T09:29:53Z

jbmc/src/java_bytecode/java_entry_point.cpp

+  if(!has_suffix(id2string(symbol.name), "@class_model"))
+    return nullptr;
+  return symbol_table.lookup(
+    "java::java.lang.Class.cproverInitializeClassLiteral:(ZZZZZZZ)V");


What is with the ZZZZZZZ?

Type descriptor -- 7 boolean parameters, void return.

thk123 · 2018-05-25T09:31:59Z

src/util/irep_ids.def

 IREP_ID_TWO(C_annotations, #annotations)
 IREP_ID_ONE(final)
+IREP_ID_ONE(synthetic)
+IREP_ID_ONE(interface)


I agree with Tom and since is ID_abstract field is left unchanged by this PR I think nothing needs updating (I suppose interfaces are marked as abstract in the bytecode).

thk123 · 2018-05-25T09:33:07Z

jbmc/regression/jbmc/class-literals/Test.java

+
+  public static void main() {
+
+    assert ExampleAnnotation.class.isAnnotation();


Possibly being dense but there is no .desc file in this PR - shouldn't there be?

Er, yes. Will fix.

smowton · 2018-05-25T11:06:02Z

Updated to handle class names, cooperate with lazy methods, and fix a couple of the snags mentioned here. Out of time for now, but TODO: add tests to make sure we don't crash when dealing with arrays of various types (primitives, multi-dimensional, arrays of objects, arrays of generic objects...)

smowton · 2018-05-29T16:52:11Z

@peterschrammel @thk123 this is now ready to go I think -- it's not perfect (getting array types' names right is a bit more work, as is extracting isLocalClass and isMemberClass), but it's better than what we had and makes __cprover_initialize considerably simpler when the models library provides the needed hook.

smowton · 2018-05-29T16:54:09Z

Bump: https://github.com/diffblue/test-gen/pull/1865

peterschrammel

@smowton, I think you have to rebase once more.

peterschrammel · 2018-05-30T14:23:29Z

jbmc/regression/jbmc/class-literals/ExampleAnnotation.java

@@ -0,0 +1,4 @@
+


weird empty lines (here and in other java files)

thk123

Sorry for not spotting these the first time around.

thk123 · 2018-05-30T14:24:42Z

jbmc/regression/jbmc/class-literals/Test.java

+
+    assert ExampleAnnotation.class.isAnnotation();
+    assert ExampleInterface.class.isInterface();
+    assert ExampleEnum.class.isEnum();


Missing asserts for synethetic (which might be hard), local class and member class (which I suppose shouldn't be too hard to create?), this is obviously not important if these aren't supported, but for the avoidance of confusion, perhaps remove them from your java/lang/Class model

I see only synthetic actually works - if possible please add an assert (perhaps using a hand created class file?)

thk123 · 2018-05-30T14:25:29Z

jbmc/src/java_bytecode/ci_lazy_methods.cpp

+///   class
+static bool references_class_model(const exprt &expr)
+{
+  symbol_typet class_type("java::java.lang.Class");


Consider making this static or const so clear isn't changing.

thk123 · 2018-05-30T14:26:21Z

jbmc/src/java_bytecode/ci_lazy_methods.cpp

+    if(can_cast_expr<symbol_exprt>(*it) &&
+       it->type() == class_type &&
+       has_suffix(
+         id2string(to_symbol_expr(*it).get_identifier()), "@class_model"))


It'd be good to pull out this magic string since now in two places and not specified by the java spec AFAICT

thk123 · 2018-05-30T14:37:45Z

jbmc/src/java_bytecode/java_entry_point.cpp

+/// etc. The method may or may not exist in any particular symbol table; it is
+/// up to the caller to check.
+/// \return Class initializer method's symbol name.
+irep_idt get_java_class_literal_initializer_signature()


Perhaps the doxygen comment should document the method that must be implemented (I assume @allredj is aware of this, but tagging just in case).

thk123 · 2018-05-30T14:41:09Z

jbmc/src/java_bytecode/java_entry_point.cpp

+    return nullptr;
+  if(symbol.type != symbol_typet("java::java.lang.Class"))
+    return nullptr;
+  if(!has_suffix(id2string(symbol.name), "@class_model"))


thk123 · 2018-05-30T14:41:31Z

jbmc/src/java_bytecode/java_entry_point.cpp

+      {
+        const std::string &name_str = id2string(sym.name);
+        irep_idt class_name =
+          name_str.substr(0, name_str.size() - strlen("@class_model"));


4 times 😛

thk123 · 2018-05-30T14:42:10Z

jbmc/src/java_bytecode/java_entry_point.cpp

+        code_function_callt::argumentst &args = initializer_call.arguments();
+
+        args.push_back(address_of_exprt(sym.symbol_expr())); /* this */
+        args.push_back(address_of_exprt(class_name_literal));


Comment on the end for each one would be great (rather than at the top) so don't have to cross reference

smowton · 2018-05-31T11:29:35Z

@thk123 changes applied.

The Java library definition of java.lang.Class, when nondet initialized, can be quite time consuming due to the enumeration constant dictionary's internal array. Instead, let's give the library a chance to set Class constants (literals like MyClass.class) itself. While we're at it we might as well gain the ability to prove some properties of the literals. We currently supply those class attributes that are easy to come by in the parse tree; with a little more effort in the parser IsLocalClass and IsMemberClass could be determined.

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

smowton requested review from cesaro, mgudemann, peterschrammel and thk123 as code owners May 24, 2018 17:11

peterschrammel reviewed May 24, 2018

View reviewed changes

thk123 reviewed May 25, 2018

View reviewed changes

smowton force-pushed the smowton/feature/initialize-class-literals branch 3 times, most recently from b0059c9 to 712c827 Compare May 25, 2018 11:04

smowton force-pushed the smowton/feature/initialize-class-literals branch 2 times, most recently from 2af582b to 7f6d15e Compare May 29, 2018 16:23

peterschrammel approved these changes May 30, 2018

View reviewed changes

peterschrammel reviewed May 30, 2018

View reviewed changes

jbmc/regression/jbmc/class-literals/ExampleAnnotation.java

@@ -0,0 +1,4 @@

Copy link

Member

peterschrammel May 30, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

weird empty lines (here and in other java files)

thk123 reviewed May 30, 2018

View reviewed changes

smowton force-pushed the smowton/feature/initialize-class-literals branch 2 times, most recently from 742873f to 680af3c Compare May 31, 2018 11:29

smowton force-pushed the smowton/feature/initialize-class-literals branch from 680af3c to b4b7b04 Compare May 31, 2018 13:41

smowton force-pushed the smowton/feature/initialize-class-literals branch from b4b7b04 to 4eda8ad Compare June 1, 2018 10:23

smowton merged commit 3817341 into diffblue:develop Jun 1, 2018

smowton mentioned this pull request Jun 7, 2018

Zero-initialize Class literals before calling initializer function #2303

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Java class literals: init using a library hook when possible #2237

Java class literals: init using a library hook when possible #2237

smowton commented May 24, 2018

peterschrammel May 24, 2018

peterschrammel May 24, 2018

thomasspriggs May 25, 2018

peterschrammel May 25, 2018

thk123 May 25, 2018

smowton May 25, 2018

thk123 left a comment

thk123 May 25, 2018

smowton May 25, 2018

thk123 May 25, 2018

thk123 May 25, 2018

smowton May 25, 2018

smowton commented May 25, 2018

smowton commented May 29, 2018 •

edited

Loading

smowton commented May 29, 2018

peterschrammel left a comment

peterschrammel May 30, 2018

thk123 left a comment

thk123 May 30, 2018

thk123 May 30, 2018

thk123 May 30, 2018

thk123 May 30, 2018

thk123 May 30, 2018

thk123 May 30, 2018

thk123 May 30, 2018

thk123 May 30, 2018

smowton commented May 31, 2018


		public static void main() {

		assert ExampleAnnotation.class.isAnnotation();

Java class literals: init using a library hook when possible #2237

Java class literals: init using a library hook when possible #2237

Conversation

smowton commented May 24, 2018

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

thk123 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

smowton commented May 25, 2018

smowton commented May 29, 2018 • edited Loading

smowton commented May 29, 2018

peterschrammel left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 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

smowton commented May 31, 2018

smowton commented May 29, 2018 •

edited

Loading