From cc6136b281910886de8d43cf76f66349d9436699 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Mon, 8 Oct 2018 15:49:00 +0100 Subject: [PATCH 1/2] CI lazy methods: load clinit for all enum types Previously static initializers for enum types were only loaded for those types that are reachable from the arguments to the entry method. This would lead to an invariant violation when an opaque method returned an enum type (which needs to be nondet-initialized just like arguments to the entry method). This commit solves this problem by moving the code for marking the static initializers of enums as loaded from ci_lazy_methods to ci_lazy_methods_needed, and applying it to all deterministic and nondeterministic enums that are reachable in some way from the entry method. Including deterministic enums is not a problem, since we load static initializers for all types (enums and others) whose constructor we use anyway. --- jbmc/src/java_bytecode/ci_lazy_methods.cpp | 31 ------------------- jbmc/src/java_bytecode/ci_lazy_methods.h | 5 --- .../java_bytecode/ci_lazy_methods_needed.cpp | 27 ++++++++++++++++ .../java_bytecode/ci_lazy_methods_needed.h | 8 ++--- 4 files changed, 30 insertions(+), 41 deletions(-) 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); From f9da0bd9fa60ed0e73038be45f3286bf0663c271 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Mon, 8 Oct 2018 17:20:14 +0100 Subject: [PATCH 2/2] Add tests for enums returned by opaque methods The tests were copied from jbmc/regression/jbmc/NondetEnumArg and adapted for the case where the enum is returned by an opaque method (Opaque.class has been deleted). --- .../jbmc/NondetEnumOpaqueReturn/Color.class | Bin 0 -> 800 bytes .../jbmc/NondetEnumOpaqueReturn/Color.java | 5 ++ .../NondetEnumOpaqueReturn.class | Bin 0 -> 1724 bytes .../NondetEnumOpaqueReturn.java | 54 ++++++++++++++++++ .../jbmc/NondetEnumOpaqueReturn/Opaque.java | 9 +++ .../test_some_constant.desc | 11 ++++ .../test_specific_constant1.desc | 7 +++ .../test_specific_constant2.desc | 7 +++ .../test_specific_constant3.desc | 7 +++ 9 files changed, 100 insertions(+) create mode 100644 jbmc/regression/jbmc/NondetEnumOpaqueReturn/Color.class create mode 100644 jbmc/regression/jbmc/NondetEnumOpaqueReturn/Color.java create mode 100644 jbmc/regression/jbmc/NondetEnumOpaqueReturn/NondetEnumOpaqueReturn.class create mode 100644 jbmc/regression/jbmc/NondetEnumOpaqueReturn/NondetEnumOpaqueReturn.java create mode 100644 jbmc/regression/jbmc/NondetEnumOpaqueReturn/Opaque.java create mode 100644 jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_some_constant.desc create mode 100644 jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant1.desc create mode 100644 jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant2.desc create mode 100644 jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant3.desc diff --git a/jbmc/regression/jbmc/NondetEnumOpaqueReturn/Color.class b/jbmc/regression/jbmc/NondetEnumOpaqueReturn/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/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 0000000000000000000000000000000000000000..4b126779257d4bd79e2360c27d3c23098d9cbd36 GIT binary patch literal 1724 zcmb`HTW=Fb6vzMLti9{aI=S=8e&{Pq=}S3tI|GnV~@g8dl%Mg zzCk}hpX#T)@dg4UBY{*ND^=wi0qTD?zJLNs9(b9ZJ?B3&=XcJT`S<wJk{wcdwlYZcM zZtbd5v$rdI>g)Vo^QCmTs$*EK)VaH{SgN$*Ft@zA zUy|QD>eP{S&n?TK=+>(n_w5IDxhaFX@6O({AKDfMFi3zshlTT4u#iE&KvucuDz>{b zccqP8^nK4~Y!)uyTheY8uj;sH;Sw%eSj3WrWh@CquWc5K>&(OI+U=si(5KJW@tuVg zToFihkJ{M2CrivowBS`dpIhw6pdb*>O|ONP%QU%ml~e;Xb=PeLzT@uD`@vp&HUX1a z_Ji6_PH>kc$n9S>tx8yt?v4_$gf|3q&o4W!U11fwhZHJo0P>V&&GBWqlNMGlsMEov zcQDT8O0)AsDytI7SqzL8gB*wWH^#5vH=2I|@l*-%RZFDiab(+4G0J9*()Z*QB0s-C z&&_-j+S<%N(4Ia+w1Fh2y{{0XPk%krgpr9iVg7|9YTiU|Y!`i;S`FyhBWOKKp(YV( zhFcnAm)lUI?Y2bAp{Va8k=_zT+oA<63?Mt&z`$4osX?vLjYL63LZ}5KIM-khBf&hR zp))52rii%+6W7s;-(aCi?;q&HpUmB3q;Q0*jw1dJ86CqqM$+Re;w>gccN|rj8f|9^ zZ+M`_MYa8zIt=q(Vh&(l4w3tboFsB5?_JtFiNJ~*tagH-rCIL`^N?prFOX>i!}t{= z@EN!w%p%qyoamwrDYUT;+J7xH|1)TZDfyQnJ4&)+BpX)`D#<2EHiZQo$2v~n7rvSg zklRQ0LFq!WufHhSLCt))n$3{xB*{*ZY?fqmBs)#AGbB4pvU4PxKY+|&$F}eIe0alw ibSBwEs(t;QBid~i^(d(Ot{NeVh_#|#g=74QVElh{&_<8| literal 0 HcmV?d00001 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.