From 9981faba6f96fcf45a325304f2642df9f8cebbe8 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 11 Jun 2018 11:34:20 +0100 Subject: [PATCH 1/8] Correct doxygen documentation --- jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp index e3b10b0ebbf..656c225a0ea 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp @@ -15,8 +15,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com /// Notes `method_symbol_name` is referenced from some reachable function, and /// should therefore be elaborated. -/// \par parameters: `method_symbol_name`: method name; must exist in symbol -/// table. +/// \param: `method_symbol_name`: method name; must exist in symbol table. void ci_lazy_methods_neededt::add_needed_method( const irep_idt &method_symbol_name) { @@ -26,8 +25,7 @@ void ci_lazy_methods_neededt::add_needed_method( /// 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. -/// \par parameters: `class_symbol_name`: class name; must exist in symbol -/// table. +/// \param: `class_symbol_name`: class name; must exist in symbol table. /// \return Returns true if `class_symbol_name` is new (not seen before). bool ci_lazy_methods_neededt::add_needed_class( const irep_idt &class_symbol_name) From b67ae26b4ecee36027932fe80394ee8743066fc4 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 11 Jun 2018 11:34:10 +0100 Subject: [PATCH 2/8] Add can_cast_type for symbol_typet --- src/util/std_types.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/util/std_types.h b/src/util/std_types.h index 591a91d4de4..9693f10b78e 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -151,6 +151,12 @@ inline symbol_typet &to_symbol_type(typet &type) return static_cast(type); } +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_symbol; +} + /*! \brief Base type of C structs and unions, and C++ classes */ class struct_union_typet:public typet From 9d42bc87a0094fc611124908ee529cc312c92824 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 12 Jun 2018 11:59:22 +0100 Subject: [PATCH 3/8] Move method for gathering all instantiated types into ci_lazy_methods_needed --- jbmc/src/java_bytecode/ci_lazy_methods.cpp | 140 ++---------------- jbmc/src/java_bytecode/ci_lazy_methods.h | 15 -- .../java_bytecode/ci_lazy_methods_needed.cpp | 108 ++++++++++++++ .../java_bytecode/ci_lazy_methods_needed.h | 19 ++- 4 files changed, 134 insertions(+), 148 deletions(-) diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp index 3a8eae3fc30..15739328aa4 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods.cpp @@ -113,7 +113,10 @@ bool ci_lazy_methodst::operator()( { std::unordered_set initial_callable_methods; ci_lazy_methods_neededt initial_lazy_methods( - initial_callable_methods, instantiated_classes, symbol_table); + initial_callable_methods, + instantiated_classes, + symbol_table, + pointer_type_selector); initialize_instantiated_classes( methods_to_convert_later, namespacet(symbol_table), initial_lazy_methods); methods_to_convert_later.insert( @@ -298,7 +301,10 @@ ci_lazy_methodst::convert_and_analyze_method( // Note this wraps *references* to methods_to_convert_later & // instantiated_classes ci_lazy_methods_neededt needed_methods( - methods_to_convert_later, instantiated_classes, symbol_table); + methods_to_convert_later, + instantiated_classes, + symbol_table, + pointer_type_selector); const bool could_not_convert_function = method_converter(method_name, needed_methods); @@ -430,8 +436,7 @@ void ci_lazy_methodst::initialize_instantiated_classes( if(param.type().id()==ID_pointer) { const pointer_typet &original_pointer=to_pointer_type(param.type()); - initialize_all_instantiated_classes_from_pointer( - original_pointer, ns, needed_lazy_methods); + needed_lazy_methods.add_all_needed_classes(original_pointer); } } } @@ -448,75 +453,6 @@ void ci_lazy_methodst::initialize_instantiated_classes( needed_lazy_methods.add_needed_class("java::" + id2string(id)); } -/// Build up list of methods for types for a pointer and any types it -/// might be subsituted for. See -/// `initialize_instantiated_classes` for more details. -/// \param pointer_type: The type to gather methods for. -/// \param ns: global namespace -/// \param [out] needed_lazy_methods: Populated with all Java reference types -/// whose references may be passed, directly or indirectly, to any of the -/// functions in `entry_points` -void ci_lazy_methodst::initialize_all_instantiated_classes_from_pointer( - const pointer_typet &pointer_type, - const namespacet &ns, - ci_lazy_methods_neededt &needed_lazy_methods) -{ - initialize_instantiated_classes_from_pointer( - pointer_type, - ns, - needed_lazy_methods); - - // TODO we should be passing here a map that maps generic parameters - // to concrete types in the current context TG-2664 - const pointer_typet &subbed_pointer_type = - pointer_type_selector.convert_pointer_type(pointer_type, {}, ns); - - if(subbed_pointer_type!=pointer_type) - { - initialize_instantiated_classes_from_pointer( - subbed_pointer_type, ns, needed_lazy_methods); - } -} - -/// Build up list of methods for types for a specific pointer type. See -/// `initialize_instantiated_classes` for more details. -/// \param pointer_type: The type to gather methods for. -/// \param ns: global namespace -/// \param [out] needed_lazy_methods: Populated with all Java reference types -/// whose references may be passed, directly or indirectly, to any of the -/// functions in `entry_points` -void ci_lazy_methodst::initialize_instantiated_classes_from_pointer( - const pointer_typet &pointer_type, - const namespacet &ns, - ci_lazy_methods_neededt &needed_lazy_methods) -{ - const symbol_typet &class_type=to_symbol_type(pointer_type.subtype()); - const auto ¶m_classid=class_type.get_identifier(); - - // Note here: different arrays may have different element types, so we should - // explore again even if we've seen this classid before in the array case. - if(needed_lazy_methods.add_needed_class(param_classid) || - is_java_array_tag(param_classid)) - { - gather_field_types(pointer_type.subtype(), ns, needed_lazy_methods); - } - - if(is_java_generic_type(pointer_type)) - { - // Assume if this is a generic like X, then any concrete parameters - // will at some point be instantiated. - const auto &generic_args = - to_java_generic_type(pointer_type).generic_type_arguments(); - for(const auto &generic_arg : generic_args) - { - if(!is_java_generic_parameter(generic_arg)) - { - initialize_instantiated_classes_from_pointer( - generic_arg, ns, needed_lazy_methods); - } - } - } -} /// Get places where virtual functions are called. /// \param e: expression tree to search @@ -611,64 +547,6 @@ void ci_lazy_methodst::gather_needed_globals( gather_needed_globals(*opit, symbol_table, needed); } -/// See param needed_lazy_methods -/// \param class_type: root of class tree to search -/// \param ns: global namespace -/// \param [out] needed_lazy_methods: Popualted with all Java reference types -/// reachable starting at `class_type`. For example if `class_type` is -/// `symbol_typet("java::A")` and A has a B field, then `B` (but not `A`) will -/// noted as a needed class. -void ci_lazy_methodst::gather_field_types( - const typet &class_type, - const namespacet &ns, - ci_lazy_methods_neededt &needed_lazy_methods) -{ - const auto &underlying_type=to_struct_type(ns.follow(class_type)); - if(is_java_array_tag(underlying_type.get_tag())) - { - // If class_type is not a symbol this may be a reference array, - // but we can't tell what type. - if(class_type.id() == ID_symbol) - { - const typet &element_type = - java_array_element_type(to_symbol_type(class_type)); - if(element_type.id() == ID_pointer) - { - // This is a reference array -- mark its element type available. - initialize_all_instantiated_classes_from_pointer( - to_pointer_type(element_type), ns, needed_lazy_methods); - } - } - } - else - { - for(const auto &field : underlying_type.components()) - { - if(field.type().id() == ID_struct || field.type().id() == ID_symbol) - gather_field_types(field.type(), ns, needed_lazy_methods); - else if(field.type().id() == ID_pointer) - { - if(field.type().subtype().id() == ID_symbol) - { - initialize_all_instantiated_classes_from_pointer( - to_pointer_type(field.type()), ns, needed_lazy_methods); - } - else - { - // If raw structs were possible this would lead to missed - // dependencies, as both array element and specialised generic type - // information cannot be obtained in this case. - // We should therefore only be skipping pointers such as the uint16t* - // in our internal String representation. - INVARIANT( - field.type().subtype().id() != ID_struct, - "struct types should be referred to by symbol at this stage"); - } - } - } - } -} - /// Find a virtual callee, if one is defined and the callee type is known to /// exist. /// \param instantiated_classes: set of classes that can be instantiated. diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.h b/jbmc/src/java_bytecode/ci_lazy_methods.h index 156e67fe240..7e9d506488c 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.h +++ b/jbmc/src/java_bytecode/ci_lazy_methods.h @@ -121,16 +121,6 @@ class ci_lazy_methodst:public messaget const namespacet &ns, ci_lazy_methods_neededt &needed_lazy_methods); - void initialize_all_instantiated_classes_from_pointer( - const pointer_typet &pointer_type, - const namespacet &ns, - ci_lazy_methods_neededt &needed_lazy_methods); - - void initialize_instantiated_classes_from_pointer( - const pointer_typet &pointer_type, - const namespacet &ns, - ci_lazy_methods_neededt &needed_lazy_methods); - void gather_virtual_callsites( const exprt &e, std::unordered_set &result); @@ -146,11 +136,6 @@ class ci_lazy_methodst:public messaget const symbol_tablet &symbol_table, symbol_tablet &needed); - void gather_field_types( - const typet &class_type, - const namespacet &ns, - ci_lazy_methods_neededt &needed_lazy_methods); - irep_idt get_virtual_method_target( const std::unordered_set &instantiated_classes, const irep_idt &call_basename, diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp index 656c225a0ea..d713242c47e 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp @@ -11,7 +11,10 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "ci_lazy_methods.h" +#include #include +#include +#include /// Notes `method_symbol_name` is referenced from some reachable function, and /// should therefore be elaborated. @@ -41,3 +44,108 @@ bool ci_lazy_methods_neededt::add_needed_class( return true; } + +/// Add to the needed classes all classes specified, the replacement type if it +/// will be replaced, and all fields it contains. +/// \param pointer_type: The type to add +void ci_lazy_methods_neededt::add_all_needed_classes( + const pointer_typet &pointer_type) +{ + namespacet ns{symbol_table}; + initialize_instantiated_classes_from_pointer(pointer_type, ns); + + // TODO we should be passing here a map that maps generic parameters + // to concrete types in the current context TG-2664 + const pointer_typet &subbed_pointer_type = + pointer_type_selector.convert_pointer_type(pointer_type, {}, ns); + + if(subbed_pointer_type != pointer_type) + { + initialize_instantiated_classes_from_pointer(subbed_pointer_type, ns); + } +} + +/// Build up list of methods for types for a specific pointer type. See +/// `add_all_needed_classes` for more details. +/// \param pointer_type: The type to gather methods for. +/// \param ns: global namespace +void ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer( + const pointer_typet &pointer_type, + const namespacet &ns) +{ + const symbol_typet &class_type = to_symbol_type(pointer_type.subtype()); + const auto ¶m_classid = class_type.get_identifier(); + + // Note here: different arrays may have different element types, so we should + // explore again even if we've seen this classid before in the array case. + if(add_needed_class(param_classid) || is_java_array_tag(param_classid)) + { + gather_field_types(pointer_type.subtype(), ns); + } + + if(is_java_generic_type(pointer_type)) + { + // Assume if this is a generic like X, then any concrete parameters + // will at some point be instantiated. + const auto &generic_args = + to_java_generic_type(pointer_type).generic_type_arguments(); + for(const auto &generic_arg : generic_args) + { + if(!is_java_generic_parameter(generic_arg)) + { + initialize_instantiated_classes_from_pointer(generic_arg, ns); + } + } + } +} + +/// For a given type, gather all fields referenced by that type +/// \param class_type: root of class tree to search +/// \param ns: global namespaces. +void ci_lazy_methods_neededt::gather_field_types( + const typet &class_type, + const namespacet &ns) +{ + const auto &underlying_type = to_struct_type(ns.follow(class_type)); + if(is_java_array_tag(underlying_type.get_tag())) + { + // If class_type is not a symbol this may be a reference array, + // but we can't tell what type. + if(class_type.id() == ID_symbol) + { + const typet &element_type = + java_array_element_type(to_symbol_type(class_type)); + if(element_type.id() == ID_pointer) + { + // This is a reference array -- mark its element type available. + add_all_needed_classes(to_pointer_type(element_type)); + } + } + } + else + { + for(const auto &field : underlying_type.components()) + { + if(field.type().id() == ID_struct || field.type().id() == ID_symbol) + gather_field_types(field.type(), ns); + else if(field.type().id() == ID_pointer) + { + if(field.type().subtype().id() == ID_symbol) + { + add_all_needed_classes(to_pointer_type(field.type())); + } + else + { + // If raw structs were possible this would lead to missed + // dependencies, as both array element and specialised generic type + // information cannot be obtained in this case. + // We should therefore only be skipping pointers such as the uint16t* + // in our internal String representation. + INVARIANT( + field.type().subtype().id() != ID_struct, + "struct types should be referred to by symbol at this stage"); + } + } + } + } +} diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.h b/jbmc/src/java_bytecode/ci_lazy_methods_needed.h index ecb95c0d129..e062962050d 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods_needed.h +++ b/jbmc/src/java_bytecode/ci_lazy_methods_needed.h @@ -17,22 +17,29 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include +class select_pointer_typet; +class pointer_typet; + class ci_lazy_methods_neededt { public: ci_lazy_methods_neededt( std::unordered_set &_callable_methods, std::unordered_set &_instantiated_classes, - symbol_tablet &_symbol_table) + symbol_tablet &_symbol_table, + const select_pointer_typet &pointer_type_selector) : callable_methods(_callable_methods), instantiated_classes(_instantiated_classes), - symbol_table(_symbol_table) + symbol_table(_symbol_table), + pointer_type_selector(pointer_type_selector) {} void add_needed_method(const irep_idt &); // Returns true if new bool add_needed_class(const irep_idt &); + void add_all_needed_classes(const pointer_typet &pointer_type); + private: // callable_methods is a vector because it's used as a work-list // which is periodically cleared. It can't be relied upon to @@ -45,6 +52,14 @@ class ci_lazy_methods_neededt // repeatedly exploring a class hierarchy. std::unordered_set &instantiated_classes; symbol_tablet &symbol_table; + + const select_pointer_typet &pointer_type_selector; + + void initialize_instantiated_classes_from_pointer( + const pointer_typet &pointer_type, + const namespacet &ns); + + void gather_field_types(const typet &class_type, const namespacet &ns); }; #endif From 20645c9f3f3e1e4f1e58a76cfd466a44e8de47e1 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 18 Jun 2018 11:10:41 +0100 Subject: [PATCH 4/8] Add classes to needed classes for parameters and returns for opaque calls Use gather all fields when setting up the return of an opaque method This can be considered an input to the function under test, so therefore we need to set it up in the same way. --- jbmc/src/java_bytecode/ci_lazy_methods.cpp | 11 ----------- jbmc/src/java_bytecode/java_bytecode_language.cpp | 10 ++++++++++ 2 files changed, 10 insertions(+), 11 deletions(-) diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.cpp b/jbmc/src/java_bytecode/ci_lazy_methods.cpp index 15739328aa4..647dc6b9c84 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods.cpp @@ -177,17 +177,6 @@ bool ci_lazy_methodst::operator()( symbol_table); } - // cproverNondetInitialize has to be force-loaded for mocks to return valid - // objects (objects which satisfy invariants specified in the - // cproverNondetInitialize method) - for(const auto &class_name : instantiated_classes) - { - const irep_idt cprover_validate = - id2string(class_name) + ".cproverNondetInitialize:()V"; - if(symbol_table.symbols.count(cprover_validate)) - methods_already_populated.insert(cprover_validate); - } - // Remove symbols for methods that were declared but never used: symbol_tablet keep_symbols; // Manually keep @inflight_exception, as it is unused at this stage diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 6baf3216e63..a280cbab41f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -1038,6 +1038,16 @@ bool java_bytecode_languaget::convert_single_method( return false; } + // The return of an opaque function is a source of an otherwise invisible + // instantiation, so here we ensure we've loaded the appropriate classes. + const code_typet function_type = to_code_type(symbol.type); + if( + const pointer_typet *pointer_return_type = + type_try_dynamic_cast(function_type.return_type())) + { + needed_lazy_methods->add_all_needed_classes(*pointer_return_type); + } + return true; } From a71889372e20e95d7336790e5904c43e2d8a6499 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 12 Jun 2018 13:40:44 +0100 Subject: [PATCH 5/8] Adding test to ensure methods on return type of opaque function These methods should be loaded for all classes where an instance might be seen and the return of an opaque method is one such instance. --- .../jbmc/lazyloading_opaquereturn/Bar.class | Bin 0 -> 333 bytes .../jbmc/lazyloading_opaquereturn/Bar.java | 7 +++++++ .../jbmc/lazyloading_opaquereturn/Baz.class | Bin 0 -> 317 bytes .../jbmc/lazyloading_opaquereturn/Baz.java | 5 +++++ .../jbmc/lazyloading_opaquereturn/Foo.class | Bin 0 -> 445 bytes .../jbmc/lazyloading_opaquereturn/Foo.java | 11 +++++++++++ .../jbmc/lazyloading_opaquereturn/Gen.class | Bin 0 -> 400 bytes .../jbmc/lazyloading_opaquereturn/Gen.java | 3 +++ .../jbmc/lazyloading_opaquereturn/GenFiller.class | Bin 0 -> 351 bytes .../jbmc/lazyloading_opaquereturn/GenFiller.java | 7 +++++++ .../jbmc/lazyloading_opaquereturn/Opaque.java | 6 ++++++ .../jbmc/lazyloading_opaquereturn/TestClass.class | Bin 0 -> 449 bytes .../jbmc/lazyloading_opaquereturn/TestClass.java | 5 +++++ .../jbmc/lazyloading_opaquereturn/test.desc | 12 ++++++++++++ 14 files changed, 56 insertions(+) create mode 100644 jbmc/regression/jbmc/lazyloading_opaquereturn/Bar.class create mode 100644 jbmc/regression/jbmc/lazyloading_opaquereturn/Bar.java create mode 100644 jbmc/regression/jbmc/lazyloading_opaquereturn/Baz.class create mode 100644 jbmc/regression/jbmc/lazyloading_opaquereturn/Baz.java create mode 100644 jbmc/regression/jbmc/lazyloading_opaquereturn/Foo.class create mode 100644 jbmc/regression/jbmc/lazyloading_opaquereturn/Foo.java create mode 100644 jbmc/regression/jbmc/lazyloading_opaquereturn/Gen.class create mode 100644 jbmc/regression/jbmc/lazyloading_opaquereturn/Gen.java create mode 100644 jbmc/regression/jbmc/lazyloading_opaquereturn/GenFiller.class create mode 100644 jbmc/regression/jbmc/lazyloading_opaquereturn/GenFiller.java create mode 100644 jbmc/regression/jbmc/lazyloading_opaquereturn/Opaque.java create mode 100644 jbmc/regression/jbmc/lazyloading_opaquereturn/TestClass.class create mode 100644 jbmc/regression/jbmc/lazyloading_opaquereturn/TestClass.java create mode 100644 jbmc/regression/jbmc/lazyloading_opaquereturn/test.desc diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/Bar.class b/jbmc/regression/jbmc/lazyloading_opaquereturn/Bar.class new file mode 100644 index 0000000000000000000000000000000000000000..d35c14928a9960375ac22837829b2b08e116846c GIT binary patch literal 333 zcmZ9G%}N775QM8Y`xDn_Vm##R%^z?t-V_fCLSTspCHL9Q5GSlVGH!zSR-S|$d;lLR zShGkF57Sgt_t(?koAnof3mm5CV36P-!B8M?d}Bd;Wopx03p&RqQ$cuZXIjwDO|2)( z=R&(jRa8udxh+*SRnB<-8-~r3c@;$YjdGWQQTgKRO1p`zXSx}4uThnGC!Idnr7QKF z@vFL=K3}Mn>LEtLpXmhypJbJ)=h=O+&}D-o1iTpFp$HLC1yn>>yL4IG0ix4S$Vc1W jVT~DkC}r)nI>IiM&-S+PS?iho2jf4WY{7kw2k8F*|GhNC literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/Bar.java b/jbmc/regression/jbmc/lazyloading_opaquereturn/Bar.java new file mode 100644 index 00000000000..5382afb1aaf --- /dev/null +++ b/jbmc/regression/jbmc/lazyloading_opaquereturn/Bar.java @@ -0,0 +1,7 @@ +public class Bar { + public int x; + + public void cproverNondetInitialize() { + + } +} diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/Baz.class b/jbmc/regression/jbmc/lazyloading_opaquereturn/Baz.class new file mode 100644 index 0000000000000000000000000000000000000000..85193230e37b923a025227722ffb4bbc741ac545 GIT binary patch literal 317 zcmZ8byH3ME5S(@VAjTwthMJCtgc~|gibO&}vO)n$e|AoAk@2C!Ns+&zibRnQ;G-hO z21O`a?B2}I%vcF!s= z$(&@iP~}uP)8IeSuV2lFAjn2)bt^b6-kn`)H?h@B*AL7!sx&LQ<0rdtg}ygU)B)Ak zbG1|nd<6WNSTJaqv{cng`k2pkQR56AFKx;LFGIi{5~ZBN8CgFoS}WJ1EKCbr zeInnGdoz`6sWZ4&31NMtXNgQR%K@#Nb@R~Iaja~o$A)TGCpzs3l+Q0F0+l;6WovVw z6E)0ULS@G?j0>}gWIT~p=lT~`(r3NQFY6n_S?y?H%}Uv!Nv0}&;9Mny&C~*WISFE!%!0>ouA&rYDDfx2$GhOL;<<2(Ttl78V_m`yAHM|+ x#$A$tSui`7ZxF9VOOvr$KrUkK|1@A9Eh>S7t@*0ZWdDucAEVeB57}PA(KoMGP-6f9 literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/Foo.java b/jbmc/regression/jbmc/lazyloading_opaquereturn/Foo.java new file mode 100644 index 00000000000..d5765648a32 --- /dev/null +++ b/jbmc/regression/jbmc/lazyloading_opaquereturn/Foo.java @@ -0,0 +1,11 @@ +public class Foo { + public Bar subType; + + public Baz[] arraySubtype; + + public Gen genSubtype; + + public void cproverNondetInitialize() { + + } +} diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/Gen.class b/jbmc/regression/jbmc/lazyloading_opaquereturn/Gen.class new file mode 100644 index 0000000000000000000000000000000000000000..baaed0ba8e21e4dbacb75e3fd07bc3a0b4a11c9f GIT binary patch literal 400 zcmZXQy-ve06orrT+k`+%fHJcc2D&go6bT{062Z`@yA!P9DkLZ*m3S;BBnBRUheDi0 zWhfndeb49P>wEqE^Z5nf0>?f~9J)AiF%}SwK$tA$N=^$|E~XFJQsvE+fH%{NQZ{X^ z1k5xgaUxynCZ?R6&IPQS>XB!|M3?Hmea=*!%B&y>lPZ_RT-LhNYiKo3`c=SA?o`QI z<4w=o%b(Bh3=!Xp>6%38<#uoJHWKh>Ra@ukR(Bl?SmV5#DZl_88>SW*{htyiF!&dM z;Id$IcbFM)nXw8yMxW%m*MNQY0r5^?Vu#To?k)$6L7&^$#U9mggN&$*b?JSCy*l^> DiQP|g literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/Gen.java b/jbmc/regression/jbmc/lazyloading_opaquereturn/Gen.java new file mode 100644 index 00000000000..afcffe05ae6 --- /dev/null +++ b/jbmc/regression/jbmc/lazyloading_opaquereturn/Gen.java @@ -0,0 +1,3 @@ +public class Gen { + T t; +} diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/GenFiller.class b/jbmc/regression/jbmc/lazyloading_opaquereturn/GenFiller.class new file mode 100644 index 0000000000000000000000000000000000000000..70deaa0b6b7bc7619ccf445b625cc660c68ac1fc GIT binary patch literal 351 zcmZ9Hy-veG5QJwP{}3l6Ar#bf{7AT=1JNLXB3YpTr9V3-xac^e!%4wgQ6W+A06Y|8 zY(*BLxYf+;eyiK>pU*D<=h#ot!z968f~i0Z-%Jo+8fWS&LGS2zAqcOlr522H}gSEaHGaYuSz zt$nFENi*u0vz6MYAz~zgewPX+O`cih9<#e*rOO(J2zUd)uOmc66;Kgm-J#3c4iKGu oK;GMSpEYLOKq>36)e#0%O}5*?r>$r9AB_KiJa!9?I38g93oSf5@Bjb+ literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/GenFiller.java b/jbmc/regression/jbmc/lazyloading_opaquereturn/GenFiller.java new file mode 100644 index 00000000000..1e9d6a5720a --- /dev/null +++ b/jbmc/regression/jbmc/lazyloading_opaquereturn/GenFiller.java @@ -0,0 +1,7 @@ +public class GenFiller { + public int i; + + public void cproverNondetInitialize() { + + } + diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/Opaque.java b/jbmc/regression/jbmc/lazyloading_opaquereturn/Opaque.java new file mode 100644 index 00000000000..9d7bf8d1c19 --- /dev/null +++ b/jbmc/regression/jbmc/lazyloading_opaquereturn/Opaque.java @@ -0,0 +1,6 @@ +public class Opaque +{ + static Foo opaqueMethod() { + return null; + } +} diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/TestClass.class b/jbmc/regression/jbmc/lazyloading_opaquereturn/TestClass.class new file mode 100644 index 0000000000000000000000000000000000000000..5bdb52e0006ce79c2a837315ae4d5ec339e1df21 GIT binary patch literal 449 zcmYLFO;5r=5Pd@nrKJku_qXT;Jjlh1!FZ5_#H7kW!hKsBSyH>$52HWJghb=PAK;HN zPLb42cHX?VZ)SJ)`{(luz&TDVl(1@H4eKU0uxVlo+Xi+F>=H_sGL*>`L2I^#1ih<9 zKB4N!(7#I`T|XKKH(;giC{F}K5y^}%L_HbHm{4&Bew=gz5yu^ZoiOR8p_fP%66l5Z z4Z*rsY2^7mnRQ#v3(h9uS=ca8Hn3-79|r~wZ5*Lt;MhhLHG-MD3AN1M4n+9S?z7J@Nn>Chr|#f&%EqE|Euu_kKm$eopKKMtCX_jv z%-W2^SUi0Pz0Hp;j-|QCLvwEb85ozCnOM$?FBZj>4-{t5X3#tTEiAqX&|pE&+gMz{ M!?I3T;aEWZ7kPS2(EtDd literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/TestClass.java b/jbmc/regression/jbmc/lazyloading_opaquereturn/TestClass.java new file mode 100644 index 00000000000..dc1cbf52248 --- /dev/null +++ b/jbmc/regression/jbmc/lazyloading_opaquereturn/TestClass.java @@ -0,0 +1,5 @@ +public class TestClass { + public static void testFunction() { + int x = Opaque.opaqueMethod().subType.x; + } +} diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/test.desc b/jbmc/regression/jbmc/lazyloading_opaquereturn/test.desc new file mode 100644 index 00000000000..761e3f73d8d --- /dev/null +++ b/jbmc/regression/jbmc/lazyloading_opaquereturn/test.desc @@ -0,0 +1,12 @@ +CORE +TestClass.class +--function TestClass.testFunction --lazy-methods --verbosity 10 +CI lazy methods: elaborate java::Foo\.cproverNondetInitialize:\(\)V +CI lazy methods: elaborate java::Bar\.cproverNondetInitialize:\(\)V +CI lazy methods: elaborate java::Baz\.cproverNondetInitialize:\(\)V +CI lazy methods: elaborate java::GenFiller\.cproverNondetInitialize:\(\)V +-- +-- +Testing that the return type of an opaque method is correctly elaborated. The +cproverNondetInitialize should be loaded for all classes where an instance might +be seen. From 409d892d42de6e642249a6e4e89f56bad9ace6fc Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 12 Jun 2018 18:23:22 +0100 Subject: [PATCH 6/8] Don't forcibly instantiate abstract classes If a class is abstract then there definitely isn't an instance of it so we shouldn't load those methods. --- jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp index d713242c47e..a855f235591 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp @@ -52,6 +52,12 @@ void ci_lazy_methods_neededt::add_all_needed_classes( const pointer_typet &pointer_type) { namespacet ns{symbol_table}; + const java_class_typet &underlying_type = + to_java_class_type(ns.follow(pointer_type.subtype())); + + if(underlying_type.is_abstract()) + return; + initialize_instantiated_classes_from_pointer(pointer_type, ns); // TODO we should be passing here a map that maps generic parameters From d7d5f635292e2dbb8d053c9b151df5ef37cfaef1 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 13 Jun 2018 09:20:09 +0100 Subject: [PATCH 7/8] Disable lazy loading opaque return for symex driven loading --- jbmc/regression/jbmc/lazyloading_opaquereturn/test.desc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/jbmc/regression/jbmc/lazyloading_opaquereturn/test.desc b/jbmc/regression/jbmc/lazyloading_opaquereturn/test.desc index 761e3f73d8d..882dc0b8b44 100644 --- a/jbmc/regression/jbmc/lazyloading_opaquereturn/test.desc +++ b/jbmc/regression/jbmc/lazyloading_opaquereturn/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure TestClass.class --function TestClass.testFunction --lazy-methods --verbosity 10 CI lazy methods: elaborate java::Foo\.cproverNondetInitialize:\(\)V @@ -10,3 +10,4 @@ CI lazy methods: elaborate java::GenFiller\.cproverNondetInitialize:\(\)V Testing that the return type of an opaque method is correctly elaborated. The cproverNondetInitialize should be loaded for all classes where an instance might be seen. +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods From e95f59d86e2870e02df7f6ee8d9a20193941ec87 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 14 Jun 2018 10:18:34 +0100 Subject: [PATCH 8/8] Don't instantiate abstract types when they are returned from stubs This is less agressive than the original solution of not instantating abstract types in ci_lazy_methods at all. This is done to minimize the changes this PR introduces. --- jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp | 5 ----- jbmc/src/java_bytecode/java_bytecode_language.cpp | 12 +++++++++++- 2 files changed, 11 insertions(+), 6 deletions(-) diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp index a855f235591..b1467c205c0 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp @@ -52,11 +52,6 @@ void ci_lazy_methods_neededt::add_all_needed_classes( const pointer_typet &pointer_type) { namespacet ns{symbol_table}; - const java_class_typet &underlying_type = - to_java_class_type(ns.follow(pointer_type.subtype())); - - if(underlying_type.is_abstract()) - return; initialize_instantiated_classes_from_pointer(pointer_type, ns); diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index a280cbab41f..155304d7514 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -1045,7 +1045,17 @@ bool java_bytecode_languaget::convert_single_method( const pointer_typet *pointer_return_type = type_try_dynamic_cast(function_type.return_type())) { - needed_lazy_methods->add_all_needed_classes(*pointer_return_type); + // If the return type is abstract, we won't forcibly instantiate it here + // otherwise this can cause abstract methods to be explictly called + // TODO(tkiley): Arguably no abstract class should ever be added to + // TODO(tkiley): ci_lazy_methods_neededt, but this needs further + // TODO(tkiley): investigation + namespacet ns{symbol_table}; + const java_class_typet &underlying_type = + to_java_class_type(ns.follow(pointer_return_type->subtype())); + + if(!underlying_type.is_abstract()) + needed_lazy_methods->add_all_needed_classes(*pointer_return_type); } return true;