diff --git a/jbmc/regression/jbmc/NondetEnumArgField/Color.class b/jbmc/regression/jbmc/NondetEnumArgField/Color.class new file mode 100644 index 00000000000..5fc329a12dd Binary files /dev/null and b/jbmc/regression/jbmc/NondetEnumArgField/Color.class differ 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 00000000000..cd6a0cf1dfa Binary files /dev/null and b/jbmc/regression/jbmc/NondetEnumArgField/MyClass.class differ 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 00000000000..59691e3307e Binary files /dev/null and b/jbmc/regression/jbmc/NondetEnumArgField/NondetEnumArgField.class differ diff --git a/jbmc/regression/jbmc/NondetEnumArgField/NondetEnumArgField.java b/jbmc/regression/jbmc/NondetEnumArgField/NondetEnumArgField.java new file mode 100644 index 00000000000..c60d1f5fde7 --- /dev/null +++ b/jbmc/regression/jbmc/NondetEnumArgField/NondetEnumArgField.java @@ -0,0 +1,8 @@ +public class NondetEnumArgField { + + public static void test(MyClass mc) { + int result = mc.myMethod(); + assert result == 10; + } + +} diff --git a/jbmc/regression/jbmc/NondetEnumArgField/test.desc b/jbmc/regression/jbmc/NondetEnumArgField/test.desc new file mode 100644 index 00000000000..f5b4de914db --- /dev/null +++ b/jbmc/regression/jbmc/NondetEnumArgField/test.desc @@ -0,0 +1,9 @@ +CORE +NondetEnumArgField.class +--function NondetEnumArgField.test --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^VERIFICATION FAILED$ +-- +-- +The test checks that even when none of the enum constants are referenced in user +code, a nondet enum (in this case, a field of an argument) is still correctly +loaded and initialized. 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 &);