diff --git a/jbmc/regression/jbmc/NondetEnumOpaqueReturn/Color.class b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/Color.class new file mode 100644 index 00000000000..5fc329a12dd Binary files /dev/null and b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/Color.class differ diff --git a/jbmc/regression/jbmc/NondetEnumOpaqueReturn/Color.java b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/Color.java new file mode 100644 index 00000000000..0fd41d395d0 --- /dev/null +++ b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/Color.java @@ -0,0 +1,5 @@ +public enum Color { + RED, + GREEN, + BLUE +} diff --git a/jbmc/regression/jbmc/NondetEnumOpaqueReturn/NondetEnumOpaqueReturn.class b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/NondetEnumOpaqueReturn.class new file mode 100644 index 00000000000..4b126779257 Binary files /dev/null and b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/NondetEnumOpaqueReturn.class differ diff --git a/jbmc/regression/jbmc/NondetEnumOpaqueReturn/NondetEnumOpaqueReturn.java b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/NondetEnumOpaqueReturn.java new file mode 100644 index 00000000000..d03cf5a1e08 --- /dev/null +++ b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/NondetEnumOpaqueReturn.java @@ -0,0 +1,54 @@ +public class NondetEnumOpaqueReturn { + + public static void canChooseSomeConstant() { + Opaque o = new Opaque(); + Color c = o.getC(); + if (c == null) + return; + assert c != null; + boolean isRed = c.name().startsWith("RED") && c.name().length() == 3 + && c.ordinal() == 0; + boolean isGreen = c.name().startsWith("GREEN") && c.name().length() == 5 + && c.ordinal() == 1; + boolean isBlue = c.name().startsWith("BLUE") && c.name().length() == 4 + && c.ordinal() == 2; + assert (isRed || isGreen || isBlue); + } + + public static void canChooseRed() { + Opaque o = new Opaque(); + Color c = o.getC(); + if (c == null) + return; + boolean isGreen = c.name().startsWith("GREEN") && c.name().length() == 5 + && c.ordinal() == 1; + boolean isBlue = c.name().startsWith("BLUE") && c.name().length() == 4 + && c.ordinal() == 2; + assert (isGreen || isBlue); + } + + public static void canChooseGreen() { + Opaque o = new Opaque(); + Color c = o.getC(); + if (c == null) + return; + boolean isRed = c.name().startsWith("RED") && c.name().length() == 3 + && c.ordinal() == 0; + boolean isBlue = c.name().startsWith("BLUE") && c.name().length() == 4 + && c.ordinal() == 2; + assert (isRed || isBlue); + } + + public static void canChooseBlue() { + Opaque o = new Opaque(); + Color c = o.getC(); + if (c == null) + return; + boolean isRed = c.name().startsWith("RED") && c.name().length() == 3 + && c.ordinal() == 0; + boolean isGreen = c.name().startsWith("GREEN") && c.name().length() == 5 + && c.ordinal() == 1; + assert (isRed || isGreen); + } + +} diff --git a/jbmc/regression/jbmc/NondetEnumOpaqueReturn/Opaque.java b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/Opaque.java new file mode 100644 index 00000000000..653313e07f5 --- /dev/null +++ b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/Opaque.java @@ -0,0 +1,9 @@ +public class Opaque { + + Color c; + + public Color getC() { + return c; + } + +} diff --git a/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_some_constant.desc b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_some_constant.desc new file mode 100644 index 00000000000..4628904c706 --- /dev/null +++ b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_some_constant.desc @@ -0,0 +1,11 @@ +CORE +NondetEnumOpaqueReturn.class +--function NondetEnumOpaqueReturn.canChooseSomeConstant --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +The test checks that the name and ordinal fields of nondet-initialized enums +which have been returned by an opaque method correspond to those of an enum +constant of the same type. diff --git a/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant1.desc b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant1.desc new file mode 100644 index 00000000000..52ab297e335 --- /dev/null +++ b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant1.desc @@ -0,0 +1,7 @@ +CORE +NondetEnumOpaqueReturn.class +--function NondetEnumOpaqueReturn.canChooseRed --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^VERIFICATION FAILED$ +-- +-- +Test 1 of 3 to check that any of the enum constants can be chosen. diff --git a/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant2.desc b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant2.desc new file mode 100644 index 00000000000..22e146eaba5 --- /dev/null +++ b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant2.desc @@ -0,0 +1,7 @@ +CORE +NondetEnumOpaqueReturn.class +--function NondetEnumOpaqueReturn.canChooseGreen --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^VERIFICATION FAILED$ +-- +-- +Test 2 of 3 to check that any of the enum constants can be chosen. diff --git a/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant3.desc b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant3.desc new file mode 100644 index 00000000000..e347386333e --- /dev/null +++ b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant3.desc @@ -0,0 +1,7 @@ +CORE +NondetEnumOpaqueReturn.class +--function NondetEnumOpaqueReturn.canChooseBlue --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^VERIFICATION FAILED$ +-- +-- +Test 3 of 3 to check that any of the enum constants can be chosen. diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp index 4442e51f968..04c650a4d3a 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods.cpp @@ -392,37 +392,6 @@ 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 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 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( - const irep_idt &class_id, - const symbol_tablet &symbol_table, - ci_lazy_methods_neededt &needed_lazy_methods) -{ - 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); } /// Get places where virtual functions are called. diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.h b/jbmc/src/java_bytecode/ci_lazy_methods.h index 7683264368d..f90d2186a8e 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.h +++ b/jbmc/src/java_bytecode/ci_lazy_methods.h @@ -120,11 +120,6 @@ class ci_lazy_methodst:public messaget const namespacet &ns, ci_lazy_methods_neededt &needed_lazy_methods); - void add_clinit_call( - const irep_idt &class_id, - const symbol_tablet &symbol_table, - ci_lazy_methods_neededt &needed_lazy_methods); - void gather_virtual_callsites( const exprt &e, std::unordered_set &result); diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp index c3972be4c2f..e5848b8c2f9 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp @@ -10,6 +10,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com /// Context-insensitive lazy methods container #include "ci_lazy_methods.h" +#include "java_static_initializers.h" #include #include @@ -25,6 +26,24 @@ void ci_lazy_methods_neededt::add_needed_method( callable_methods.insert(method_symbol_name); } +/// For a given class id, note that its static initializer is 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 +/// because ci_lazy_methods essentially has to go through the same logic as +/// __CPROVER_start in its initial setup, and because return values of opaque +/// methods need to be considered in ci_lazy_methods too. +/// \param class_id: The given class id +/// \param symbol_table: Used to look up occurrences of static initializers +void ci_lazy_methods_neededt::add_clinit_call( + const irep_idt &class_id, + const symbol_tablet &symbol_table) +{ + const irep_idt &clinit_wrapper = clinit_wrapper_name(class_id); + if(symbol_table.symbols.count(clinit_wrapper)) + add_needed_method(clinit_wrapper); +} + /// Notes class `class_symbol_name` will be instantiated, or a static field /// belonging to it will be accessed. Also notes that its static initializer is /// therefore reachable. @@ -42,6 +61,14 @@ bool ci_lazy_methods_neededt::add_needed_class( if(symbol_table.symbols.count(cprover_validate)) add_needed_method(cprover_validate); + // Special case for enums. We may want to generalise this, the comment in + // \ref java_object_factoryt::gen_nondet_pointer_init (TG-4689). + namespacet ns(symbol_table); + const auto &class_type = + to_java_class_type(ns.lookup(class_symbol_name).type); + if(class_type.get_base("java::java.lang.Enum")) + add_clinit_call(class_symbol_name, symbol_table); + return true; } diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.h b/jbmc/src/java_bytecode/ci_lazy_methods_needed.h index 49e18d38bbf..8cf58096d89 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods_needed.h +++ b/jbmc/src/java_bytecode/ci_lazy_methods_needed.h @@ -35,11 +35,6 @@ 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 &); @@ -61,6 +56,9 @@ class ci_lazy_methods_neededt const select_pointer_typet &pointer_type_selector; + void + add_clinit_call(const irep_idt &class_id, const symbol_tablet &symbol_table); + void initialize_instantiated_classes_from_pointer( const pointer_typet &pointer_type, const namespacet &ns);