From 49089b1fde30ec909091168a09981200cf6d4f0f Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Fri, 17 Aug 2018 00:22:48 +0100 Subject: [PATCH 1/2] Fix lazy loading of enum static initializers Rather than calling clinit_wrapper on every parameter to the entry method that is an enum, we should first load all the classes that may be needed before we enter the entry method, and then call clinit_wrapper on all of those which are enums. For example, the case of an enum field of an argument to the entry method would have previously hit an invariant violation. --- jbmc/src/java_bytecode/ci_lazy_methods.cpp | 35 +++++++++---------- jbmc/src/java_bytecode/ci_lazy_methods.h | 4 +-- .../java_bytecode/ci_lazy_methods_needed.h | 5 +++ 3 files changed, 23 insertions(+), 21 deletions(-) diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp index 414b2a51ad0..f4c7f502d66 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods.cpp @@ -382,16 +382,6 @@ void ci_lazy_methodst::initialize_instantiated_classes( if(param.type().id()==ID_pointer) { const pointer_typet &original_pointer = to_pointer_type(param.type()); - const auto &original_type = ns.follow(original_pointer.subtype()); - // Special case for enums. We may want to generalise this, see TG-4689 - // and the comment in java_object_factoryt::gen_nondet_pointer_init. - if( - can_cast_type(original_type) && - to_java_class_type(original_type).get_base("java::java.lang.Enum")) - { - add_clinit_call_for_pointer_type( - original_pointer, ns.get_symbol_table(), needed_lazy_methods); - } needed_lazy_methods.add_all_needed_classes(original_pointer); } } @@ -407,28 +397,35 @@ void ci_lazy_methodst::initialize_instantiated_classes( // As in class_loader, ensure these classes stay available for(const auto &id : extra_instantiated_classes) needed_lazy_methods.add_needed_class("java::" + id2string(id)); + + // Special case for enums. We may want to generalise this, see TG-4689 + // and the comment in java_object_factoryt::gen_nondet_pointer_init. + for(const auto &found_class : needed_lazy_methods.get_instantiated_classes()) + { + const auto &class_type = to_java_class_type(ns.lookup(found_class).type); + if(class_type.get_base("java::java.lang.Enum")) + add_clinit_call(found_class, ns.get_symbol_table(), needed_lazy_methods); + } } /// Helper function for `initialize_instantiated_classes`. -/// For a given pointer_typet that is being noted as needed in -/// `needed_lazy_methods`, notes that its static initializer is also needed. -/// This applies the same logic to the class of `pointer_type` that +/// For a given class id that is being noted as needed in `needed_lazy_methods`, +/// notes that its static initializer is also needed. +/// This applies the same logic to the given class that /// `java_bytecode_convert_methodt::get_clinit_call` applies e.g. to classes /// whose constructor we call in a method body. This duplication is unavoidable /// due to the fact that ci_lazy_methods essentially has to go through the same /// logic as __CPROVER_start in its initial setup. -/// \param pointer_type: The given pointer_typet +/// \param class_id: The given class id /// \param symbol_table: Used to look up occurrences of static initializers /// \param [out] needed_lazy_methods: Gets notified of any static initializers /// that need to be loaded -void ci_lazy_methodst::add_clinit_call_for_pointer_type( - const pointer_typet &pointer_type, +void ci_lazy_methodst::add_clinit_call( + const irep_idt &class_id, const symbol_tablet &symbol_table, ci_lazy_methods_neededt &needed_lazy_methods) { - const irep_idt &pointer_id = - to_symbol_type(pointer_type.subtype()).get_identifier(); - const irep_idt &clinit_wrapper = clinit_wrapper_name(pointer_id); + const irep_idt &clinit_wrapper = clinit_wrapper_name(class_id); if(symbol_table.symbols.count(clinit_wrapper)) needed_lazy_methods.add_needed_method(clinit_wrapper); } diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.h b/jbmc/src/java_bytecode/ci_lazy_methods.h index 905258f1c4d..7683264368d 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.h +++ b/jbmc/src/java_bytecode/ci_lazy_methods.h @@ -120,8 +120,8 @@ class ci_lazy_methodst:public messaget const namespacet &ns, ci_lazy_methods_neededt &needed_lazy_methods); - void add_clinit_call_for_pointer_type( - const pointer_typet &pointer_type, + void add_clinit_call( + const irep_idt &class_id, const symbol_tablet &symbol_table, ci_lazy_methods_neededt &needed_lazy_methods); diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.h b/jbmc/src/java_bytecode/ci_lazy_methods_needed.h index e062962050d..da9c3fe83ac 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods_needed.h +++ b/jbmc/src/java_bytecode/ci_lazy_methods_needed.h @@ -34,6 +34,11 @@ class ci_lazy_methods_neededt pointer_type_selector(pointer_type_selector) {} + std::unordered_set get_instantiated_classes() + { + return instantiated_classes; + } + void add_needed_method(const irep_idt &); // Returns true if new bool add_needed_class(const irep_idt &); From df0605e64d997cdd2e2222adcd4cbeaefd865e87 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Fri, 17 Aug 2018 00:26:46 +0100 Subject: [PATCH 2/2] Add test for enum field of argument type --- .../jbmc/NondetEnumArgField/Color.class | Bin 0 -> 800 bytes .../regression/jbmc/NondetEnumArgField/Color.java | 5 +++++ .../jbmc/NondetEnumArgField/MyClass.class | Bin 0 -> 321 bytes .../jbmc/NondetEnumArgField/MyClass.java | 11 +++++++++++ .../NondetEnumArgField/NondetEnumArgField.class | Bin 0 -> 590 bytes .../NondetEnumArgField/NondetEnumArgField.java | 8 ++++++++ jbmc/regression/jbmc/NondetEnumArgField/test.desc | 9 +++++++++ 7 files changed, 33 insertions(+) create mode 100644 jbmc/regression/jbmc/NondetEnumArgField/Color.class create mode 100644 jbmc/regression/jbmc/NondetEnumArgField/Color.java create mode 100644 jbmc/regression/jbmc/NondetEnumArgField/MyClass.class create mode 100644 jbmc/regression/jbmc/NondetEnumArgField/MyClass.java create mode 100644 jbmc/regression/jbmc/NondetEnumArgField/NondetEnumArgField.class create mode 100644 jbmc/regression/jbmc/NondetEnumArgField/NondetEnumArgField.java create mode 100644 jbmc/regression/jbmc/NondetEnumArgField/test.desc diff --git a/jbmc/regression/jbmc/NondetEnumArgField/Color.class b/jbmc/regression/jbmc/NondetEnumArgField/Color.class new file mode 100644 index 0000000000000000000000000000000000000000..5fc329a12dd4d7c143e62f9e22715f6818584af6 GIT binary patch literal 800 zcmZuu?@!ZE6g{u)*6z{$piXoHMG>VP$~2KrTL?I-F z+w+rjB7Zb$&B3M{_?NY{`+}aQL~pC@)`S9pJc*E=bO4pQ5H1iX;5L@PaEGEb^5WwY zuy0Ty80Ba$Sk+C#&_f{pxwkPVi8az|0-1a0ll%ga*q7h8|3#W zqu@RatdhMF6_7~r?frz-vvlNMehu3 a*3OcY3W}trPUj73rQoXh13Z)>*8T#fV2(2Y literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/NondetEnumArgField/Color.java b/jbmc/regression/jbmc/NondetEnumArgField/Color.java new file mode 100644 index 00000000000..0fd41d395d0 --- /dev/null +++ b/jbmc/regression/jbmc/NondetEnumArgField/Color.java @@ -0,0 +1,5 @@ +public enum Color { + RED, + GREEN, + BLUE +} diff --git a/jbmc/regression/jbmc/NondetEnumArgField/MyClass.class b/jbmc/regression/jbmc/NondetEnumArgField/MyClass.class new file mode 100644 index 0000000000000000000000000000000000000000..cd6a0cf1dfa0ceecb37456fd5c6601dfed5fec7d GIT binary patch literal 321 zcmXYrKTE?<6vfX?)1-YSZPcy~ZrZ^v;-a_&1fkKP;{K98G&M~mO@)4^E`lI9xC(wK z@w`wTocr&0-o3wnU*7=EF;Z|5_0hq;j{_fv0?7paG_H!Oz7%*@d6_rYg3ih5qri=; zxe*Mfd1>y}%hc2lIxX1gEjNj2o~wCF-U`B5qqCPpzwQ7vtJZa9ZgNWp$tEuJYIU~I zZ#saFUVtt(-R|^~qGjo{JOYO5dVid;i_!IKpf{N<3 uO*`5{K(*)vqea8<2b>>xk=jP1EgKH3Wx!3==<_N5AF}E|6g`6$8vX<4Rx$(t literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/NondetEnumArgField/MyClass.java b/jbmc/regression/jbmc/NondetEnumArgField/MyClass.java new file mode 100644 index 00000000000..31278f1cdbc --- /dev/null +++ b/jbmc/regression/jbmc/NondetEnumArgField/MyClass.java @@ -0,0 +1,11 @@ +public class MyClass { + + private Color c; + + public int myMethod() { + if (c == null) + return 10; + return 20; + } + +} diff --git a/jbmc/regression/jbmc/NondetEnumArgField/NondetEnumArgField.class b/jbmc/regression/jbmc/NondetEnumArgField/NondetEnumArgField.class new file mode 100644 index 0000000000000000000000000000000000000000..59691e3307e44570e730f96a3f19165028de093d GIT binary patch literal 590 zcmZWm$x6dO82NRkSDm0mo0RzX2Q z?>>`=|Aa0F8JH#Wt&{KH_fG(2lyoGK*D;NmF(gpXP}HF!uVGfl9OgAF5OO6m2!tQn zo*Nw6f!T0`MW8D}qGG#txJyvhH!cY3foBOqs%E?5q|lAY<}Q0m<|{Pw;7hSK>9k`38ED zKuq$Sh&~ciQb_Y&LaT`J0A@E|5vx2y=^-JL>aZ