diff --git a/src/java_bytecode/generic_parameter_specialization_map_keys.cpp b/src/java_bytecode/generic_parameter_specialization_map_keys.cpp index 45f4b86c392..18cc04a0918 100644 --- a/src/java_bytecode/generic_parameter_specialization_map_keys.cpp +++ b/src/java_bytecode/generic_parameter_specialization_map_keys.cpp @@ -99,15 +99,21 @@ const void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer( pointer_type.subtype().get(ID_identifier) == pointer_subtype_struct.get(ID_name)); - const java_generic_typet &generic_pointer = - to_java_generic_type(pointer_type); - - // If the pointer points to an incomplete class, don't treat the generics - if(!pointer_subtype_struct.get_bool(ID_incomplete_class)) + // If the pointer points to: + // - an incomplete class or + // - a class that is neither generic nor implicitly generic (this + // may be due to unsupported class signature) + // then ignore the generic types in the pointer and do not add any pairs. + // TODO TG-1996 should decide how mocking and generics should work + // together. Currently an incomplete class is never marked as generic. If + // this changes in TG-1996 then the condition below should be updated. + if( + !pointer_subtype_struct.get_bool(ID_incomplete_class) && + (is_java_generic_class_type(pointer_subtype_struct) || + is_java_implicitly_generic_class_type(pointer_subtype_struct))) { - PRECONDITION( - is_java_generic_class_type(pointer_subtype_struct) || - is_java_implicitly_generic_class_type(pointer_subtype_struct)); + const java_generic_typet &generic_pointer = + to_java_generic_type(pointer_type); const std::vector &generic_parameters = get_all_generic_parameters(pointer_subtype_struct); @@ -135,14 +141,23 @@ const void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol( const symbol_typet &symbol_type, const typet &symbol_struct) { - if(is_java_generic_symbol_type(symbol_type)) + // If the struct is: + // - an incomplete class or + // - a class that is neither generic nor implicitly generic (this + // may be due to unsupported class signature) + // then ignore the generic types in the symbol_type and do not add any pairs. + // TODO TG-1996 should decide how mocking and generics should work + // together. Currently an incomplete class is never marked as generic. If + // this changes in TG-1996 then the condition below should be updated. + if( + is_java_generic_symbol_type(symbol_type) && + !symbol_struct.get_bool(ID_incomplete_class) && + (is_java_generic_class_type(symbol_struct) || + is_java_implicitly_generic_class_type(symbol_struct))) { - java_generic_symbol_typet generic_symbol = + const java_generic_symbol_typet &generic_symbol = to_java_generic_symbol_type(symbol_type); - PRECONDITION( - is_java_generic_class_type(symbol_struct) || - is_java_implicitly_generic_class_type(symbol_struct)); const std::vector &generic_parameters = get_all_generic_parameters(symbol_struct); diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 6c84b21f532..93a473cf9b4 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -202,10 +202,12 @@ void java_bytecode_convert_classt::convert(const classt &c) } class_type=generic_class_type; } - catch(unsupported_java_class_signature_exceptiont) + catch(const unsupported_java_class_signature_exceptiont &e) { - warning() << "we currently don't support parsing for example double " - "bounded, recursive and wild card generics" << eom; + warning() << "Class: " << c.name + << "\n could not parse signature: " << c.signature.value() + << "\n " << e.what() << "\n ignoring that the class is generic" + << eom; } } @@ -253,11 +255,12 @@ void java_bytecode_convert_classt::convert(const classt &c) base, superclass_ref.value(), qualified_classname); class_type.add_base(generic_base); } - catch(unsupported_java_class_signature_exceptiont) + catch(const unsupported_java_class_signature_exceptiont &e) { - debug() << "unsupported generic superclass signature " - << id2string(*superclass_ref) - << " falling back on using the descriptor" << eom; + warning() << "Superclass: " << c.extends << " of class: " << c.name + << "\n could not parse signature: " << superclass_ref.value() + << "\n " << e.what() + << "\n ignoring that the superclass is generic" << eom; class_type.add_base(base); } } @@ -292,11 +295,12 @@ void java_bytecode_convert_classt::convert(const classt &c) base, interface_ref.value(), qualified_classname); class_type.add_base(generic_base); } - catch(unsupported_java_class_signature_exceptiont) + catch(const unsupported_java_class_signature_exceptiont &e) { - debug() << "unsupported generic interface signature " - << id2string(*interface_ref) - << " falling back on using the descriptor" << eom; + warning() << "Interface: " << interface << " of class: " << c.name + << "\n could not parse signature: " << interface_ref.value() + << "\n " << e.what() + << "\n ignoring that the interface is generic" << eom; class_type.add_base(base); } } diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 366674e85dc..7d4007add8a 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -286,18 +286,21 @@ code_typet member_type_lazy( } else { - message.warning() << "method: " << class_name << "." << method_name - << "\n signature: " << signature.value() << "\n descriptor: " - << descriptor << "\n different number of parameters, reverting to " - "descriptor" << message.eom; + message.warning() << "Method: " << class_name << "." << method_name + << "\n signature: " << signature.value() + << "\n descriptor: " << descriptor + << "\n different number of parameters, reverting to " + "descriptor" + << message.eom; } } - catch(unsupported_java_class_signature_exceptiont &e) + catch(const unsupported_java_class_signature_exceptiont &e) { - message.warning() << "method: " << class_name << "." << method_name - << "\n could not parse signature: " << signature.value() << "\n " - << e.what() << "\n" << " reverting to descriptor: " - << descriptor << message.eom; + message.warning() << "Method: " << class_name << "." << method_name + << "\n could not parse signature: " << signature.value() + << "\n " << e.what() << "\n" + << " reverting to descriptor: " << descriptor + << message.eom; } } return to_code_type(member_type_from_descriptor); diff --git a/unit/goto-programs/goto_program_generics/GenericBases.java b/unit/goto-programs/goto_program_generics/GenericBases.java index 65b5b2a5534..fc4da5293dd 100644 --- a/unit/goto-programs/goto_program_generics/GenericBases.java +++ b/unit/goto-programs/goto_program_generics/GenericBases.java @@ -1,21 +1,3 @@ -// Helper classes -class Wrapper { - public T field; -} - -class IntWrapper { - public int i; -} - -class TwoWrapper { - public K first; - public V second; -} - -interface InterfaceWrapper { - public T method(T t); -} - // A class extending a generic class instantiated with a standard library class class SuperclassInst extends Wrapper { public void foo() { @@ -24,14 +6,14 @@ public void foo() { } // A class extending a generic class instantiated with a user-defined class -class SuperclassInst2 extends Wrapper { +class SuperclassInst2 extends Wrapper { public void foo() { this.field.i = 5; } } // A class extending an instantiated nested generic class -class SuperclassInst3 extends Wrapper> { +class SuperclassInst3 extends Wrapper> { public void foo() { this.field.field.i = 5; } @@ -54,7 +36,7 @@ public void foo() { // A generic class extending a generic class with both instantiated and // uninstantiated parameters -class SuperclassMixed extends TwoWrapper { +class SuperclassMixed extends PairWrapper { public void foo(U value) { this.first = value; this.second.i = 5; @@ -99,7 +81,7 @@ public void foo(U value) { } public Inner inner; - class InnerGen extends TwoWrapper { + class InnerGen extends PairWrapper { public void foo(U uvalue, T tvalue) { this.first = uvalue; this.second = tvalue; @@ -113,11 +95,23 @@ class InnerThree extends Inner { } class SuperclassInnerUninstTest { - SuperclassInnerUninst f; + SuperclassInnerUninst f; public void foo() { - IntWrapper x = new IntWrapper(); + IWrapper x = new IWrapper(0); f.inner.foo(x); f.inner_gen.foo(x,true); f.inner_three.foo(x); } } + +class SuperclassUnsupported extends UnsupportedWrapper1 { + public void foo() { + this.field = new SuperclassUnsupported(); + } +} + +class SuperclassOpaque extends OpaqueWrapper { + public void foo() { + this.field.i = 5; + } +} diff --git a/unit/goto-programs/goto_program_generics/GenericFieldOpaque.class b/unit/goto-programs/goto_program_generics/GenericFieldOpaque.class new file mode 100644 index 00000000000..af3ed9cbcab Binary files /dev/null and b/unit/goto-programs/goto_program_generics/GenericFieldOpaque.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFieldUnsupported.class b/unit/goto-programs/goto_program_generics/GenericFieldUnsupported.class new file mode 100644 index 00000000000..692e93e4516 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/GenericFieldUnsupported.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter$Outer$InnerClass.class b/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter$Outer$InnerClass.class index faa5d2304ea..05209db8695 100644 Binary files a/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter$Outer$InnerClass.class and b/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter$Outer$InnerClass.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter$Outer.class b/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter$Outer.class index fa60ef8a06e..32483eb9b8a 100644 Binary files a/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter$Outer.class and b/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter$Outer.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter.class b/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter.class index 26460abadeb..7138dfe2505 100644 Binary files a/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter.class and b/unit/goto-programs/goto_program_generics/GenericFields$GenericInnerOuter.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$GenericMethodParameter.class b/unit/goto-programs/goto_program_generics/GenericFields$GenericMethodParameter.class index d94e1b6e0b3..69e1f54703b 100644 Binary files a/unit/goto-programs/goto_program_generics/GenericFields$GenericMethodParameter.class and b/unit/goto-programs/goto_program_generics/GenericFields$GenericMethodParameter.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$GenericMethodUninstantiatedParameter.class b/unit/goto-programs/goto_program_generics/GenericFields$GenericMethodUninstantiatedParameter.class index 970da292bad..46c27ddbe61 100644 Binary files a/unit/goto-programs/goto_program_generics/GenericFields$GenericMethodUninstantiatedParameter.class and b/unit/goto-programs/goto_program_generics/GenericFields$GenericMethodUninstantiatedParameter.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$GenericRewriteParameter$A.class b/unit/goto-programs/goto_program_generics/GenericFields$GenericRewriteParameter$A.class index 1fa20e2c5f9..e035d0adc4f 100644 Binary files a/unit/goto-programs/goto_program_generics/GenericFields$GenericRewriteParameter$A.class and b/unit/goto-programs/goto_program_generics/GenericFields$GenericRewriteParameter$A.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$GenericRewriteParameter.class b/unit/goto-programs/goto_program_generics/GenericFields$GenericRewriteParameter.class index 419f729c848..45c2286ccc9 100644 Binary files a/unit/goto-programs/goto_program_generics/GenericFields$GenericRewriteParameter.class and b/unit/goto-programs/goto_program_generics/GenericFields$GenericRewriteParameter.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$MultipleGenericFields.class b/unit/goto-programs/goto_program_generics/GenericFields$MultipleGenericFields.class index d757be60547..c7fbb48fb8d 100644 Binary files a/unit/goto-programs/goto_program_generics/GenericFields$MultipleGenericFields.class and b/unit/goto-programs/goto_program_generics/GenericFields$MultipleGenericFields.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$NestedGenericFields.class b/unit/goto-programs/goto_program_generics/GenericFields$NestedGenericFields.class index e987035b12f..c92726f7d39 100644 Binary files a/unit/goto-programs/goto_program_generics/GenericFields$NestedGenericFields.class and b/unit/goto-programs/goto_program_generics/GenericFields$NestedGenericFields.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$PairGenericField.class b/unit/goto-programs/goto_program_generics/GenericFields$PairGenericField.class index e1fb3fe67c3..0bcf607ff16 100644 Binary files a/unit/goto-programs/goto_program_generics/GenericFields$PairGenericField.class and b/unit/goto-programs/goto_program_generics/GenericFields$PairGenericField.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields$SimpleGenericField.class b/unit/goto-programs/goto_program_generics/GenericFields$SimpleGenericField.class index f2990766703..42289355217 100644 Binary files a/unit/goto-programs/goto_program_generics/GenericFields$SimpleGenericField.class and b/unit/goto-programs/goto_program_generics/GenericFields$SimpleGenericField.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields.class b/unit/goto-programs/goto_program_generics/GenericFields.class index b25d3be89ab..4414ff12968 100644 Binary files a/unit/goto-programs/goto_program_generics/GenericFields.class and b/unit/goto-programs/goto_program_generics/GenericFields.class differ diff --git a/unit/goto-programs/goto_program_generics/GenericFields.java b/unit/goto-programs/goto_program_generics/GenericFields.java index 92833f7743c..b83152c95b4 100644 --- a/unit/goto-programs/goto_program_generics/GenericFields.java +++ b/unit/goto-programs/goto_program_generics/GenericFields.java @@ -1,24 +1,8 @@ -class SimpleWrapper { - public T field; - public T[] array_field; - - public int int_field; -} - -class IWrapper { - public int i; -} - -class PairWrapper { - public K key; - public V value; -} - public class GenericFields { IWrapper field; class SimpleGenericField { - SimpleWrapper field_input; + Wrapper field_input; public void foo() { field_input.field.i = 5; field_input.array_field = new IWrapper[2]; @@ -26,8 +10,8 @@ public void foo() { } class MultipleGenericFields { - SimpleWrapper field_input1; - SimpleWrapper field_input2; + Wrapper field_input1; + Wrapper field_input2; public void foo() { field_input1.field.i = 10; field_input2.field.i = 20; @@ -35,7 +19,7 @@ public void foo() { } class NestedGenericFields { - SimpleWrapper> field_input1; + Wrapper> field_input1; public void foo() { field_input1.field.field.i = 30; } @@ -44,19 +28,19 @@ public void foo() { class PairGenericField { PairWrapper field_input; public void foo() { - field_input.key.i = 40; - field_input.value.i = 50; + field_input.first.i = 40; + field_input.second.i = 50; } } class GenericMethodParameter { - public void foo(SimpleWrapper v) { + public void foo(Wrapper v) { v.field.i = 20; } } class GenericMethodUninstantiatedParameter { - public void foo_unspec(SimpleWrapper v) { + public void foo_unspec(Wrapper v) { v.int_field=10; } } @@ -96,3 +80,35 @@ public void foo(A v) { } } } + +// class that implements two generic interfaces +class InterfacesImplementation implements InterfaceWrapper, + InterfacePairWrapper { + public IWrapper method(IWrapper t) { + return t; + } + public IWrapper method(IWrapper t, IWrapper tt) { + if (t.i>0) + { + return t; + } + else + { + return tt; + } + } +} +class GenericFieldUnsupported { + public UnsupportedWrapper2 f; + public void foo() { + f.field.method(new IWrapper(0)); + f.field.method(new IWrapper(0), new IWrapper(2)); + } +} + +class GenericFieldOpaque { + public OpaqueWrapper f; + public void foo() { + f.field.i = 0; + } +} diff --git a/unit/goto-programs/goto_program_generics/GenericHelper.java b/unit/goto-programs/goto_program_generics/GenericHelper.java new file mode 100644 index 00000000000..fb7c9e73e0d --- /dev/null +++ b/unit/goto-programs/goto_program_generics/GenericHelper.java @@ -0,0 +1,46 @@ +// int wrapper +class IWrapper { + public int i; + public IWrapper(int ii) { + i = ii; + } +} + +// simple generic class +class Wrapper { + public T field; + public T[] array_field; + public int int_field; +} + +// generic class with two parameters +class PairWrapper { + public K first; + public V second; +} + +// simple generic interface +interface InterfaceWrapper { + public T method(T t); +} + +// generic interface with two parameters +interface InterfacePairWrapper { + public K method(K k, V v); +} + +// generic class with unsupported signature - generic bound +class UnsupportedWrapper1> { + public T field; +} + +// generic class with unsupported signature - multiple bounds +class UnsupportedWrapper2 +{ + public T field; +} + +// generic opaque class, make sure the .class file is not available +class OpaqueWrapper { + public T field; +} diff --git a/unit/goto-programs/goto_program_generics/IWrapper.class b/unit/goto-programs/goto_program_generics/IWrapper.class index 9374dd90e43..ec21b63d591 100644 Binary files a/unit/goto-programs/goto_program_generics/IWrapper.class and b/unit/goto-programs/goto_program_generics/IWrapper.class differ diff --git a/unit/goto-programs/goto_program_generics/IntWrapper.class b/unit/goto-programs/goto_program_generics/IntWrapper.class deleted file mode 100644 index 0ab2423e107..00000000000 Binary files a/unit/goto-programs/goto_program_generics/IntWrapper.class and /dev/null differ diff --git a/unit/goto-programs/goto_program_generics/InterfacePairWrapper.class b/unit/goto-programs/goto_program_generics/InterfacePairWrapper.class new file mode 100644 index 00000000000..17c6e673c1c Binary files /dev/null and b/unit/goto-programs/goto_program_generics/InterfacePairWrapper.class differ diff --git a/unit/goto-programs/goto_program_generics/InterfaceWrapper.class b/unit/goto-programs/goto_program_generics/InterfaceWrapper.class index 84a1e72c248..b25811c0e3b 100644 Binary files a/unit/goto-programs/goto_program_generics/InterfaceWrapper.class and b/unit/goto-programs/goto_program_generics/InterfaceWrapper.class differ diff --git a/unit/goto-programs/goto_program_generics/InterfacesImplementation.class b/unit/goto-programs/goto_program_generics/InterfacesImplementation.class new file mode 100644 index 00000000000..0e6ba2412e5 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/InterfacesImplementation.class differ diff --git a/unit/goto-programs/goto_program_generics/PairWrapper.class b/unit/goto-programs/goto_program_generics/PairWrapper.class index 3684152febb..f9ab0e804a9 100644 Binary files a/unit/goto-programs/goto_program_generics/PairWrapper.class and b/unit/goto-programs/goto_program_generics/PairWrapper.class differ diff --git a/unit/goto-programs/goto_program_generics/SimpleWrapper.class b/unit/goto-programs/goto_program_generics/SimpleWrapper.class deleted file mode 100644 index fbff730183d..00000000000 Binary files a/unit/goto-programs/goto_program_generics/SimpleWrapper.class and /dev/null differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInnerInst$Inner.class b/unit/goto-programs/goto_program_generics/SuperclassInnerInst$Inner.class index af39fafee64..ee81c13a881 100644 Binary files a/unit/goto-programs/goto_program_generics/SuperclassInnerInst$Inner.class and b/unit/goto-programs/goto_program_generics/SuperclassInnerInst$Inner.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInnerInst$InnerGen.class b/unit/goto-programs/goto_program_generics/SuperclassInnerInst$InnerGen.class index 3ae78c84180..fc848963c31 100644 Binary files a/unit/goto-programs/goto_program_generics/SuperclassInnerInst$InnerGen.class and b/unit/goto-programs/goto_program_generics/SuperclassInnerInst$InnerGen.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInnerInst.class b/unit/goto-programs/goto_program_generics/SuperclassInnerInst.class index 35d49ee1151..c31665988b0 100644 Binary files a/unit/goto-programs/goto_program_generics/SuperclassInnerInst.class and b/unit/goto-programs/goto_program_generics/SuperclassInnerInst.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$Inner.class b/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$Inner.class index dce417187a0..4ca3fc455bb 100644 Binary files a/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$Inner.class and b/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$Inner.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$InnerGen.class b/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$InnerGen.class index a87c8573a0e..0f1256aadb7 100644 Binary files a/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$InnerGen.class and b/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$InnerGen.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$InnerThree.class b/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$InnerThree.class index c89fee8796a..acc0c4d43db 100644 Binary files a/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$InnerThree.class and b/unit/goto-programs/goto_program_generics/SuperclassInnerUninst$InnerThree.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInnerUninst.class b/unit/goto-programs/goto_program_generics/SuperclassInnerUninst.class index 5e496ac02e8..a6510be62ca 100644 Binary files a/unit/goto-programs/goto_program_generics/SuperclassInnerUninst.class and b/unit/goto-programs/goto_program_generics/SuperclassInnerUninst.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInnerUninstTest.class b/unit/goto-programs/goto_program_generics/SuperclassInnerUninstTest.class index 085f7e320e2..bdf06a3383f 100644 Binary files a/unit/goto-programs/goto_program_generics/SuperclassInnerUninstTest.class and b/unit/goto-programs/goto_program_generics/SuperclassInnerUninstTest.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInst.class b/unit/goto-programs/goto_program_generics/SuperclassInst.class index bdd24f4a62f..0b205f2008e 100644 Binary files a/unit/goto-programs/goto_program_generics/SuperclassInst.class and b/unit/goto-programs/goto_program_generics/SuperclassInst.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInst2.class b/unit/goto-programs/goto_program_generics/SuperclassInst2.class index 4a9bbf66465..38df3f7eb0b 100644 Binary files a/unit/goto-programs/goto_program_generics/SuperclassInst2.class and b/unit/goto-programs/goto_program_generics/SuperclassInst2.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassInst3.class b/unit/goto-programs/goto_program_generics/SuperclassInst3.class index d91f3da54ae..7c27c0186ea 100644 Binary files a/unit/goto-programs/goto_program_generics/SuperclassInst3.class and b/unit/goto-programs/goto_program_generics/SuperclassInst3.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassMixed.class b/unit/goto-programs/goto_program_generics/SuperclassMixed.class index 0b2f3b90c69..55addb8093e 100644 Binary files a/unit/goto-programs/goto_program_generics/SuperclassMixed.class and b/unit/goto-programs/goto_program_generics/SuperclassMixed.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassMixedTest.class b/unit/goto-programs/goto_program_generics/SuperclassMixedTest.class index 550ff51a98e..3c22ba33d7d 100644 Binary files a/unit/goto-programs/goto_program_generics/SuperclassMixedTest.class and b/unit/goto-programs/goto_program_generics/SuperclassMixedTest.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassOpaque.class b/unit/goto-programs/goto_program_generics/SuperclassOpaque.class new file mode 100644 index 00000000000..3b384284877 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/SuperclassOpaque.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassUninst.class b/unit/goto-programs/goto_program_generics/SuperclassUninst.class index 8b30a539bbf..257e727dcd2 100644 Binary files a/unit/goto-programs/goto_program_generics/SuperclassUninst.class and b/unit/goto-programs/goto_program_generics/SuperclassUninst.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassUninstTest.class b/unit/goto-programs/goto_program_generics/SuperclassUninstTest.class index a6c038edac5..1bfcdc48317 100644 Binary files a/unit/goto-programs/goto_program_generics/SuperclassUninstTest.class and b/unit/goto-programs/goto_program_generics/SuperclassUninstTest.class differ diff --git a/unit/goto-programs/goto_program_generics/SuperclassUnsupported.class b/unit/goto-programs/goto_program_generics/SuperclassUnsupported.class new file mode 100644 index 00000000000..e48285ed5b8 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/SuperclassUnsupported.class differ diff --git a/unit/goto-programs/goto_program_generics/TwoWrapper.class b/unit/goto-programs/goto_program_generics/TwoWrapper.class deleted file mode 100644 index 7181bd114ba..00000000000 Binary files a/unit/goto-programs/goto_program_generics/TwoWrapper.class and /dev/null differ diff --git a/unit/goto-programs/goto_program_generics/UnsupportedWrapper1.class b/unit/goto-programs/goto_program_generics/UnsupportedWrapper1.class new file mode 100644 index 00000000000..d69c6316220 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/UnsupportedWrapper1.class differ diff --git a/unit/goto-programs/goto_program_generics/UnsupportedWrapper2.class b/unit/goto-programs/goto_program_generics/UnsupportedWrapper2.class new file mode 100644 index 00000000000..236d9ce4c10 Binary files /dev/null and b/unit/goto-programs/goto_program_generics/UnsupportedWrapper2.class differ diff --git a/unit/goto-programs/goto_program_generics/Wrapper.class b/unit/goto-programs/goto_program_generics/Wrapper.class index ae6aa9aaf61..496c09349ca 100644 Binary files a/unit/goto-programs/goto_program_generics/Wrapper.class and b/unit/goto-programs/goto_program_generics/Wrapper.class differ diff --git a/unit/goto-programs/goto_program_generics/generic_bases_test.cpp b/unit/goto-programs/goto_program_generics/generic_bases_test.cpp index dd0e0deacb0..e29fe0d9223 100644 --- a/unit/goto-programs/goto_program_generics/generic_bases_test.cpp +++ b/unit/goto-programs/goto_program_generics/generic_bases_test.cpp @@ -9,6 +9,8 @@ #include #include #include +#include +#include // NOTE: To inspect these tests at any point, use expr2java. // A good way to verify the validity of a test is to iterate @@ -86,7 +88,7 @@ SCENARIO( this_tmp_name, {"Wrapper"}, "field", - "java::IntWrapper", + "java::IWrapper", {"java::java.lang.Object"}, entry_point_code); } @@ -128,7 +130,7 @@ SCENARIO( wrapper_tmp_name, {}, "field", - "java::IntWrapper", + "java::IWrapper", {}, entry_point_code); } @@ -214,7 +216,7 @@ SCENARIO( { require_goto_statements::require_struct_component_assignment( f_tmp_name, - {"TwoWrapper"}, + {"PairWrapper"}, "first", "java::java.lang.Boolean", {"java::java.lang.Object"}, @@ -222,9 +224,9 @@ SCENARIO( require_goto_statements::require_struct_component_assignment( f_tmp_name, - {"TwoWrapper"}, + {"PairWrapper"}, "second", - "java::IntWrapper", + "java::IWrapper", {"java::java.lang.Object"}, entry_point_code); } @@ -354,7 +356,7 @@ SCENARIO( inner_tmp_name, {"Wrapper"}, "field", - "java::IntWrapper", + "java::IWrapper", {"java::java.lang.Object"}, entry_point_code); } @@ -373,14 +375,14 @@ SCENARIO( { require_goto_statements::require_struct_component_assignment( inner_gen_tmp_name, - {"TwoWrapper"}, + {"PairWrapper"}, "first", - "java::IntWrapper", + "java::IWrapper", {"java::java.lang.Object"}, entry_point_code); require_goto_statements::require_struct_component_assignment( inner_gen_tmp_name, - {"TwoWrapper"}, + {"PairWrapper"}, "second", "java::java.lang.Boolean", {"java::java.lang.Object"}, @@ -403,7 +405,7 @@ SCENARIO( inner_three_tmp_name, {"Wrapper"}, "field", - "java::IntWrapper", + "java::IWrapper", {"java::java.lang.Object"}, entry_point_code); } @@ -412,3 +414,100 @@ SCENARIO( } } } + +SCENARIO( + "Ignore generics for incomplete and non-generic bases", + "[core][goto_program_generics][generic_bases_test]") +{ + GIVEN( + "A class extending a generic class with unsupported class signature (thus" + " not marked as generic)") + { + const symbol_tablet &symbol_table = load_java_class( + "SuperclassUnsupported", + "./goto-programs/goto_program_generics", + "SuperclassUnsupported.foo"); + + THEN("The struct for UnsupportedWrapper1 is complete and non-generic") + { + const std::string superclass_name = "java::UnsupportedWrapper1"; + const symbolt &superclass_symbol = + require_symbol::require_symbol_exists(symbol_table, superclass_name); + + require_type::require_complete_java_non_generic_class( + superclass_symbol.type); + } + + WHEN("The method input argument is created in the entry point function") + { + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + // We trace the creation of the object that is being supplied as + // the input to the method under test. There must be one non-null + // assignment only, and usually looks like this: + // this = &tmp_object_factory$1; + const irep_idt &this_tmp_name = + require_goto_statements::require_entry_point_argument_assignment( + "this", entry_point_code); + + THEN("Object 'this' created has unspecialized inherited field") + { + // tmp_object_factory$1.@UnsupportedWrapper1.field = + // &tmp_object_factory$2; + // struct java.lang.Object { __CPROVER_string @class_identifier; + // boolean @lock; } tmp_object_factory$2; + require_goto_statements::require_struct_component_assignment( + this_tmp_name, + {"UnsupportedWrapper1"}, + "field", + "java::java.lang.Object", + {}, + entry_point_code); + } + } + } + + GIVEN( + "A class extending a generic class that is mocked (thus incomplete and not " + "marked as generic)") + { + const symbol_tablet &symbol_table = load_java_class( + "SuperclassOpaque", + "./goto-programs/goto_program_generics", + "SuperclassOpaque.foo"); + + THEN("The struct for OpaqueWrapper is incomplete and not-generic") + { + const std::string superclass_name = "java::OpaqueWrapper"; + const symbolt &superclass_symbol = + require_symbol::require_symbol_exists(symbol_table, superclass_name); + + require_type::require_incomplete_class(superclass_symbol.type); + require_type::require_java_non_generic_class(superclass_symbol.type); + } + + WHEN("The method input argument is created in the entry point function") + { + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + // For an explanation of this part, look at the comments for the similar + // parts of the previous tests. + const irep_idt &this_tmp_name = + require_goto_statements::require_entry_point_argument_assignment( + "this", entry_point_code); + + THEN("Object 'this' created has unspecialized inherited field") + { + require_goto_statements::require_struct_component_assignment( + this_tmp_name, + {"OpaqueWrapper"}, + "field", + "java::java.lang.Object", + {}, + entry_point_code); + } + } + } +} diff --git a/unit/goto-programs/goto_program_generics/generic_parameters_test.cpp b/unit/goto-programs/goto_program_generics/generic_parameters_test.cpp index 4f65efcef46..731b577423c 100644 --- a/unit/goto-programs/goto_program_generics/generic_parameters_test.cpp +++ b/unit/goto-programs/goto_program_generics/generic_parameters_test.cpp @@ -9,6 +9,8 @@ #include #include #include +#include +#include // NOTE: To inspect these tests at any point, use expr2java. // A good way to verify the validity of a test is to iterate @@ -39,14 +41,14 @@ SCENARIO( require_goto_statements::require_entry_point_argument_assignment( "this", entry_point_code); - THEN("Object 'this' has field 'field_input' of type SimpleWrapper") + THEN("Object 'this' has field 'field_input' of type Wrapper") { const auto &field_input_name = require_goto_statements::require_struct_component_assignment( tmp_object_name, {}, "field_input", - "java::SimpleWrapper", + "java::Wrapper", {}, entry_point_code); @@ -100,14 +102,14 @@ SCENARIO( require_goto_statements::require_entry_point_argument_assignment( "this", entry_point_code); - THEN("Object 'this' has field 'field_input1' of type SimpleWrapper") + THEN("Object 'this' has field 'field_input1' of type Wrapper") { const auto &field_input1_name = require_goto_statements::require_struct_component_assignment( tmp_object_name, {}, "field_input1", - "java::SimpleWrapper", + "java::Wrapper", {}, entry_point_code); @@ -123,14 +125,14 @@ SCENARIO( } } - THEN("Object 'this' has field 'field_input2' of type SimpleWrapper") + THEN("Object 'this' has field 'field_input2' of type Wrapper") { const auto &field_input2_name = require_goto_statements::require_struct_component_assignment( tmp_object_name, {}, "field_input2", - "java::SimpleWrapper", + "java::Wrapper", {}, entry_point_code); @@ -167,25 +169,25 @@ SCENARIO( require_goto_statements::require_entry_point_argument_assignment( "this", entry_point_code); - THEN("Object 'this' has field 'field_input1' of type SimpleWrapper") + THEN("Object 'this' has field 'field_input1' of type Wrapper") { const auto &field_input1_name = require_goto_statements::require_struct_component_assignment( tmp_object_name, {}, "field_input1", - "java::SimpleWrapper", + "java::Wrapper", {}, entry_point_code); - THEN("Object 'field_input1' has field 'field' of type SimpleWrapper") + THEN("Object 'field_input1' has field 'field' of type Wrapper") { const auto &field_name = require_goto_statements::require_struct_component_assignment( field_input1_name, {}, "field", - "java::SimpleWrapper", + "java::Wrapper", {}, entry_point_code); @@ -233,7 +235,7 @@ SCENARIO( require_goto_statements::require_struct_component_assignment( field_input_name, {}, - "key", + "first", "java::IWrapper", {}, entry_point_code); @@ -244,7 +246,7 @@ SCENARIO( require_goto_statements::require_struct_component_assignment( field_input_name, {}, - "value", + "second", "java::IWrapper", {}, entry_point_code); @@ -274,7 +276,7 @@ SCENARIO( require_goto_statements::require_entry_point_argument_assignment( "v", entry_point_code); - THEN("Object 'v' is of type SimpleWrapper") + THEN("Object 'v' is of type Wrapper") { const auto &tmp_object_declaration = require_goto_statements::require_declaration_of_name( @@ -284,7 +286,7 @@ SCENARIO( // and verify that it is what we expect. const auto &tmp_object_struct = to_struct_type(tmp_object_declaration.symbol().type()); - REQUIRE(tmp_object_struct.get_tag() == "SimpleWrapper"); + REQUIRE(tmp_object_struct.get_tag() == "Wrapper"); THEN("Object 'v' has field 'field' of type IWrapper") { @@ -323,7 +325,7 @@ SCENARIO( require_goto_statements::require_entry_point_argument_assignment( "v", entry_point_code); - THEN("Object 'v' is of type SimpleWrapper") + THEN("Object 'v' is of type Wrapper") { const auto &tmp_object_declaration = require_goto_statements::require_declaration_of_name( @@ -333,7 +335,7 @@ SCENARIO( // and verify that it is what we expect. const auto &tmp_object_struct = to_struct_type(tmp_object_declaration.symbol().type()); - REQUIRE(tmp_object_struct.get_tag() == "SimpleWrapper"); + REQUIRE(tmp_object_struct.get_tag() == "Wrapper"); THEN( "Object 'v' has field 'field' of type Object (upper bound of the " @@ -486,3 +488,128 @@ SCENARIO( } } } + +SCENARIO( + "Ignore generic parameters in fields and methods with incomplete and " + "non-generic types", + "[core][goto_program_generics][generic_parameters_test]") +{ + GIVEN( + "A class with a generic field pointing to a class with unsupported " + "signature (thus not marked as generic)") + { + const symbol_tablet &symbol_table = load_java_class( + "GenericFieldUnsupported", + "./goto-programs/goto_program_generics", + "GenericFieldUnsupported.foo"); + + THEN("The struct for UnsupportedWrapper2 is complete and non-generic") + { + const std::string field_class_name = "java::UnsupportedWrapper2"; + const symbolt &superclass_symbol = + require_symbol::require_symbol_exists(symbol_table, field_class_name); + + require_type::require_complete_java_non_generic_class( + superclass_symbol.type); + } + + WHEN("The method input argument is created in the entry point function") + { + // We trace the creation of the object that is being supplied as + // the input to the method under test. There must be one non-null + // assignment only, and usually looks like this: + // this = &tmp_object_factory$1; + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + const irep_idt &tmp_object_name = + require_goto_statements::require_entry_point_argument_assignment( + "this", entry_point_code); + + THEN("Object 'this' has field 'f' of type UnsupportedWrapper2") + { + // tmp_object_factory$1.f = &tmp_object_factory$2; + // struct UnsupportedWrapper2 { struct java.lang.Object + // @java.lang.Object; struct java.lang.Object *field; } + // tmp_object_factory$2; + const auto &field_input_name = + require_goto_statements::require_struct_component_assignment( + tmp_object_name, + {}, + "f", + "java::UnsupportedWrapper2", + {}, + entry_point_code); + + THEN("Object 'f' has unspecialized field 'field'") + { + // tmp_object_factory$2.field = &tmp_object_factory$3; + // struct java.lang.Object { __CPROVER_string @class_identifier; + // boolean @lock; } tmp_object_factory$3; + require_goto_statements::require_struct_component_assignment( + field_input_name, + {}, + "field", + "java::java.lang.Object", + {}, + entry_point_code); + } + } + } + } + + GIVEN( + "A class with a generic field pointing to a mocked class (thus " + "incomplete and not marked as generic)") + { + const symbol_tablet &symbol_table = load_java_class( + "GenericFieldOpaque", + "./goto-programs/goto_program_generics", + "GenericFieldOpaque.foo"); + + THEN("The struct for OpaqueWrapper is incomplete and not-generic") + { + const std::string field_class_name = "java::OpaqueWrapper"; + const symbolt &field_class_symbol = + require_symbol::require_symbol_exists(symbol_table, field_class_name); + + require_type::require_incomplete_class(field_class_symbol.type); + require_type::require_java_non_generic_class(field_class_symbol.type); + } + + WHEN("The method input argument is created in the entry point function") + { + // For an explanation of this part, look at the comments for the similar + // parts of the previous tests. + const std::vector &entry_point_code = + require_goto_statements::require_entry_point_statements(symbol_table); + + const irep_idt &tmp_object_name = + require_goto_statements::require_entry_point_argument_assignment( + "this", entry_point_code); + + THEN("Object 'this' has field 'f' of type OpaqueWrapper") + { + const auto &field_input_name = + require_goto_statements::require_struct_component_assignment( + tmp_object_name, + {}, + "f", + "java::OpaqueWrapper", + {}, + entry_point_code); + + THEN("Object 'f' has unspecialized field 'field'") + { + require_goto_statements::require_struct_component_assignment( + field_input_name, + {}, + "field", + "java::java.lang.Object", + {}, + entry_point_code); + } + } + } + } +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp index 16036dbe05f..7c8eb84bc38 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp @@ -23,7 +23,7 @@ SCENARIO( const symbolt &class_symbol = new_symbol_table.lookup_ref(class_prefix); const java_class_typet &java_class_type = - require_type::require_java_non_generic_class(class_symbol.type); + require_type::require_complete_java_non_generic_class(class_symbol.type); WHEN("Parsing an inner class with type variable") { @@ -33,7 +33,7 @@ SCENARIO( { const symbolt &class_symbol = new_symbol_table.lookup_ref(inner_name); const java_generic_class_typet &java_generic_class_type = - require_type::require_java_generic_class( + require_type::require_complete_java_generic_class( class_symbol.type, {inner_name + "::E"}); THEN("The fields are of correct types") @@ -56,7 +56,7 @@ SCENARIO( const symbolt &class_symbol = new_symbol_table.lookup_ref(boundedinner_name); const java_generic_class_typet &java_generic_class_type = - require_type::require_java_generic_class( + require_type::require_complete_java_generic_class( class_symbol.type, {boundedinner_name + "::NUM"}); // TODO extend when bounds are parsed correctly - TG-1286 @@ -94,7 +94,7 @@ SCENARIO( new_symbol_table.lookup_ref(doubleboundedinner_name); // TODO the symbol should be generic - TG-1349 // const java_generic_class_typet &java_generic_class_type = - // require_type::require_java_generic_class( + // require_type::require_complete_java_generic_class( // class_symbol.type, {doubleboundedinner_name + "::T"}); // TODO extend when bounds are parsed correctly - TG-1286 @@ -121,7 +121,7 @@ SCENARIO( const symbolt &class_symbol = new_symbol_table.lookup_ref(twoelementinner_name); const java_generic_class_typet &java_generic_class_type = - require_type::require_java_generic_class( + require_type::require_complete_java_generic_class( class_symbol.type, {twoelementinner_name + "::K", twoelementinner_name + "::V"}); diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp index 000c630415f..471c896281d 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp @@ -24,7 +24,8 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_non_generic_class(derived_symbol.type); + require_type::require_complete_java_non_generic_class( + derived_symbol.type); THEN("The base for superclass has the correct generic type information") { @@ -46,7 +47,8 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_non_generic_class(derived_symbol.type); + require_type::require_complete_java_non_generic_class( + derived_symbol.type); THEN("The base for superclass has the correct generic type information") { @@ -69,7 +71,7 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_generic_class(derived_symbol.type); + require_type::require_complete_java_generic_class(derived_symbol.type); THEN("The base for superclasss has the correct generic type information") { @@ -91,7 +93,7 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_generic_class(derived_symbol.type); + require_type::require_complete_java_generic_class(derived_symbol.type); THEN("The base for superclass has the correct generic type information") { @@ -113,7 +115,7 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_generic_class(derived_symbol.type); + require_type::require_complete_java_generic_class(derived_symbol.type); THEN("The base for superclass has the correct generic type information") { @@ -136,7 +138,8 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_non_generic_class(derived_symbol.type); + require_type::require_complete_java_non_generic_class( + derived_symbol.type); THEN("The base for superclass has the correct generic type information") { @@ -159,7 +162,7 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_generic_class(derived_symbol.type); + require_type::require_complete_java_generic_class(derived_symbol.type); THEN("The base for superclass has the correct generic type information") { @@ -183,7 +186,7 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_implicitly_generic_class( + require_type::require_complete_java_implicitly_generic_class( derived_symbol.type, {"java::ContainsInnerClassGeneric::T"}); THEN("The base for superclass has the correct generic type information") @@ -206,7 +209,8 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_non_generic_class(derived_symbol.type); + require_type::require_complete_java_non_generic_class( + derived_symbol.type); THEN("The base for superclass has the correct generic type information") { @@ -229,7 +233,8 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_non_generic_class(derived_symbol.type); + require_type::require_complete_java_non_generic_class( + derived_symbol.type); THEN("The bases have the correct generic type information") { @@ -261,7 +266,7 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_generic_class(derived_symbol.type); + require_type::require_complete_java_generic_class(derived_symbol.type); THEN("The bases have the correct generic type information") { @@ -294,7 +299,8 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_non_generic_class(derived_symbol.type); + require_type::require_complete_java_non_generic_class( + derived_symbol.type); THEN("The bases have the correct generic type information") { @@ -332,7 +338,8 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_non_generic_class(derived_symbol.type); + require_type::require_complete_java_non_generic_class( + derived_symbol.type); THEN("The bases have the correct generic type information") { @@ -374,7 +381,7 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_generic_class(derived_symbol.type); + require_type::require_complete_java_generic_class(derived_symbol.type); THEN("The bases have the correct generic type information") { @@ -418,7 +425,8 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_non_generic_class(derived_symbol.type); + require_type::require_complete_java_non_generic_class( + derived_symbol.type); THEN("The bases have the correct generic type information") { @@ -455,7 +463,8 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_non_generic_class(derived_symbol.type); + require_type::require_complete_java_non_generic_class( + derived_symbol.type); THEN("The bases have the correct generic type information") { @@ -499,7 +508,7 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_generic_class(derived_symbol.type); + require_type::require_complete_java_generic_class(derived_symbol.type); THEN("The bases have the correct generic type information") { @@ -533,7 +542,8 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_implicitly_generic_class(derived_symbol.type); + require_type::require_complete_java_implicitly_generic_class( + derived_symbol.type); THEN("The base for superclass is implicitly generic") { @@ -553,7 +563,8 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_implicitly_generic_class(derived_symbol.type); + require_type::require_complete_java_implicitly_generic_class( + derived_symbol.type); THEN("The base for superclass is generic *and* implicitly generic") { @@ -575,7 +586,8 @@ SCENARIO( const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &derived_class_type = - require_type::require_java_implicitly_generic_class(derived_symbol.type); + require_type::require_complete_java_implicitly_generic_class( + derived_symbol.type); THEN("The base for superclass is generic *and* implicitly generic") { diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp index 126454ad71d..2290733637e 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp @@ -22,7 +22,7 @@ SCENARIO( const symbolt &class_symbol = new_symbol_table.lookup_ref(class_prefix); const java_generic_class_typet &java_generic_class = - require_type::require_java_generic_class( + require_type::require_complete_java_generic_class( class_symbol.type, {class_prefix + "::T"}); THEN("There should be field t") diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp index 5717ff29f3a..cc5e540b7e0 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp @@ -27,7 +27,7 @@ SCENARIO( const symbolt &class_symbol = new_symbol_table.lookup_ref(class_prefix); const java_generic_class_typet &java_generic_class = - require_type::require_java_generic_class( + require_type::require_complete_java_generic_class( class_symbol.type, {class_prefix + "::T"}); const struct_typet class_struct = to_struct_type(class_symbol.type); @@ -79,7 +79,7 @@ SCENARIO( const symbolt &class_symbol = new_symbol_table.lookup_ref(class_prefix); const java_generic_class_typet &java_generic_class = - require_type::require_java_generic_class( + require_type::require_complete_java_generic_class( class_symbol.type, {class_prefix + "::T", class_prefix + "::U"}); const struct_typet class_struct = to_struct_type(class_symbol.type); diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp index 5c70107e5e7..666952b242a 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp @@ -26,7 +26,7 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(class_prefix)); const symbolt &class_symbol = new_symbol_table.lookup_ref(class_prefix); const java_generic_class_typet &java_generic_class = - require_type::require_java_generic_class( + require_type::require_complete_java_generic_class( class_symbol.type, {class_prefix + "::T"}); THEN( diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp index 6196edfe33c..b90ad2b3c68 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp @@ -26,7 +26,7 @@ SCENARIO( const symbolt &class_symbol = new_symbol_table.lookup_ref(outer_class_prefix); const java_generic_class_typet &generic_class = - require_type::require_java_generic_class( + require_type::require_complete_java_generic_class( class_symbol.type, {outer_class_prefix + "::T"}); THEN("There is a field f1 of generic type with correct arguments") { @@ -68,7 +68,7 @@ SCENARIO( THEN("It has correct implicit generic types") { const java_implicitly_generic_class_typet &java_class = - require_type::require_java_implicitly_generic_class( + require_type::require_complete_java_implicitly_generic_class( class_symbol.type, {outer_class_prefix + "::T"}); THEN( @@ -105,7 +105,7 @@ SCENARIO( THEN("It has correct implicit generic types") { const java_implicitly_generic_class_typet &java_class = - require_type::require_java_implicitly_generic_class( + require_type::require_complete_java_implicitly_generic_class( class_symbol.type, {outer_class_prefix + "::T"}); THEN( @@ -149,10 +149,10 @@ SCENARIO( THEN("It has correct generic types and implicit generic types") { - require_type::require_java_implicitly_generic_class( + require_type::require_complete_java_implicitly_generic_class( class_symbol.type, {outer_class_prefix + "::T"}); const java_generic_class_typet &generic_class = - require_type::require_java_generic_class( + require_type::require_complete_java_generic_class( class_symbol.type, {generic_inner_class_prefix + "::U"}); THEN( @@ -194,10 +194,10 @@ SCENARIO( THEN("It has correct generic types and implicit generic types") { - require_type::require_java_implicitly_generic_class( + require_type::require_complete_java_implicitly_generic_class( class_symbol.type, {outer_class_prefix + "::T", outer_class_prefix + "$GenericInner::U"}); - require_type::require_java_generic_class( + require_type::require_complete_java_generic_class( class_symbol.type, {generic_inner_inner_class_prefix + "::V"}); } } @@ -212,7 +212,7 @@ SCENARIO( THEN("It has correct generic types and no implicit generic types") { REQUIRE(!is_java_implicitly_generic_class_type(class_symbol.type)); - require_type::require_java_generic_class( + require_type::require_complete_java_generic_class( class_symbol.type, {static_inner_class_prefix + "::U"}); } } diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp index 149f46bcee2..d0c7916ad0b 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp @@ -27,7 +27,7 @@ SCENARIO( const symbolt &class_symbol = new_symbol_table.lookup_ref(class_prefix); const java_generic_class_typet &java_generic_class_type = - require_type::require_java_generic_class( + require_type::require_complete_java_generic_class( class_symbol.type, {class_prefix + "::T", class_prefix + "::S"}); const struct_typet class_struct = to_struct_type(class_symbol.type); diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp index 76eac25d9c7..26201973561 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp @@ -24,7 +24,7 @@ SCENARIO( const symbolt &class_symbol = new_symbol_table.lookup_ref(class_prefix); const class_typet &class_type = - require_type::require_java_non_generic_class(class_symbol.type); + require_type::require_complete_java_non_generic_class(class_symbol.type); THEN("The field component should be a pointer to java::Generic") { diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp index 38cbf85a65e..ae5d70318f5 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp @@ -28,7 +28,8 @@ SCENARIO( const symbolt &inner_symbol = new_symbol_table.lookup_ref(inner_prefix); const class_typet &inner_class_type = - require_type::require_java_implicitly_generic_class(inner_symbol.type); + require_type::require_complete_java_implicitly_generic_class( + inner_symbol.type); } THEN( @@ -63,7 +64,8 @@ SCENARIO( const symbolt &inner_enum_symbol = new_symbol_table.lookup_ref(inner_enum_prefix); - require_type::require_java_non_generic_class(inner_enum_symbol.type); + require_type::require_complete_java_non_generic_class( + inner_enum_symbol.type); } THEN( diff --git a/unit/testing-utils/require_type.cpp b/unit/testing-utils/require_type.cpp index 4bcb94aaecb..0ea4bf2e1b2 100644 --- a/unit/testing-utils/require_type.cpp +++ b/unit/testing-utils/require_type.cpp @@ -214,7 +214,7 @@ const typet &require_type::require_java_non_generic_type( /// Checks that the given type is a complete class. /// \param class_type type of the class /// \return class_type of the class -class_typet require_complete_class(const typet &class_type) +class_typet require_type::require_complete_class(const typet &class_type) { REQUIRE(class_type.id() == ID_struct); @@ -225,23 +225,40 @@ class_typet require_complete_class(const typet &class_type) return class_class_type; } -/// Verify that a class is a complete, valid java generic class. +/// Checks that the given type is an incomplete class. +/// \param class_type type of the class +/// \return class_type of the class +class_typet require_type::require_incomplete_class(const typet &class_type) +{ + REQUIRE(class_type.id() == ID_struct); + + const class_typet &class_class_type = to_class_type(class_type); + REQUIRE(class_class_type.is_class()); + REQUIRE(class_class_type.get_bool(ID_incomplete_class)); + + return class_class_type; +} + +/// Verify that a class is a valid java generic class. /// \param class_type: the class /// \return: A reference to the java generic class type. java_generic_class_typet require_type::require_java_generic_class(const typet &class_type) { - const class_typet &class_class_type = require_complete_class(class_type); - java_class_typet java_class_type = to_java_class_type(class_class_type); + REQUIRE(class_type.id() == ID_struct); + + const class_typet &class_class_type = to_class_type(class_type); + const java_class_typet &java_class_type = + to_java_class_type(class_class_type); REQUIRE(is_java_generic_class_type(java_class_type)); - java_generic_class_typet java_generic_class_type = + const java_generic_class_typet &java_generic_class_type = to_java_generic_class_type(java_class_type); return java_generic_class_type; } -/// Verify that a class is a complete, valid java generic class with the +/// Verify that a class is a valid java generic class with the /// specified list of variables. /// \param class_type: the class /// \param type_variables: vector of type variables @@ -251,7 +268,7 @@ java_generic_class_typet require_type::require_java_generic_class( const std::initializer_list &type_variables) { const java_generic_class_typet java_generic_class_type = - require_type::require_java_generic_class(class_type); + require_java_generic_class(class_type); const java_generic_class_typet::generic_typest &generic_type_vars = java_generic_class_type.generic_types(); @@ -261,8 +278,9 @@ java_generic_class_typet require_type::require_java_generic_class( type_variables.begin(), type_variables.end(), generic_type_vars.begin(), - [](const irep_idt &type_var_name, const java_generic_parametert ¶m) - { + []( + const irep_idt &type_var_name, + const java_generic_parametert ¶m) { //NOLINT REQUIRE(is_java_generic_parameter(param)); return param.type_variable().get_identifier() == type_var_name; })); @@ -270,23 +288,50 @@ java_generic_class_typet require_type::require_java_generic_class( return java_generic_class_type; } -/// Verify that a class is a complete, valid java implicitly generic class. +/// Verify that a class is a complete, valid java generic class. +/// \param class_type: the class +/// \return: A reference to the java generic class type. +java_generic_class_typet +require_type::require_complete_java_generic_class(const typet &class_type) +{ + require_complete_class(class_type); + return require_java_generic_class(class_type); +} + +/// Verify that a class is a complete, valid java generic class with the +/// specified list of variables. +/// \param class_type: the class +/// \param type_variables: vector of type variables +/// \return: A reference to the java generic class type. +java_generic_class_typet require_type::require_complete_java_generic_class( + const typet &class_type, + const std::initializer_list &type_variables) +{ + require_complete_java_generic_class(class_type); + return require_java_generic_class(class_type, type_variables); +} + +/// Verify that a class is a valid java implicitly generic class. /// \param class_type: the class /// \return: A reference to the java generic class type. java_implicitly_generic_class_typet require_type::require_java_implicitly_generic_class(const typet &class_type) { - const class_typet &class_class_type = require_complete_class(class_type); - java_class_typet java_class_type = to_java_class_type(class_class_type); + REQUIRE(class_type.id() == ID_struct); + + const class_typet &class_class_type = to_class_type(class_type); + const java_class_typet &java_class_type = + to_java_class_type(class_class_type); REQUIRE(is_java_implicitly_generic_class_type(java_class_type)); - java_implicitly_generic_class_typet java_implicitly_generic_class_type = - to_java_implicitly_generic_class_type(java_class_type); + const java_implicitly_generic_class_typet + &java_implicitly_generic_class_type = + to_java_implicitly_generic_class_type(java_class_type); return java_implicitly_generic_class_type; } -/// Verify that a class is a complete, valid java generic class with the +/// Verify that a class is a valid java generic class with the /// specified list of variables. /// \param class_type: the class /// \param type_variables: vector of type variables @@ -296,8 +341,9 @@ require_type::require_java_implicitly_generic_class( const typet &class_type, const std::initializer_list &implicit_type_variables) { - const java_implicitly_generic_class_typet java_implicitly_generic_class_type = - require_type::require_java_implicitly_generic_class(class_type); + const java_implicitly_generic_class_typet + &java_implicitly_generic_class_type = + require_java_implicitly_generic_class(class_type); const java_implicitly_generic_class_typet::implicit_generic_typest &implicit_generic_type_vars = @@ -308,8 +354,9 @@ require_type::require_java_implicitly_generic_class( implicit_type_variables.begin(), implicit_type_variables.end(), implicit_generic_type_vars.begin(), - [](const irep_idt &type_var_name, const java_generic_parametert ¶m) - { + []( + const irep_idt &type_var_name, + const java_generic_parametert ¶m) { //NOLINT REQUIRE(is_java_generic_parameter(param)); return param.type_variable().get_identifier() == type_var_name; })); @@ -317,14 +364,43 @@ require_type::require_java_implicitly_generic_class( return java_implicitly_generic_class_type; } -/// Verify that a class is a complete, valid nongeneric java class +/// Verify that a class is a complete, valid java implicitly generic class. +/// \param class_type: the class +/// \return: A reference to the java generic class type. +java_implicitly_generic_class_typet +require_type::require_complete_java_implicitly_generic_class( + const typet &class_type) +{ + require_complete_class(class_type); + return require_java_implicitly_generic_class(class_type); +} + +/// Verify that a class is a complete, valid java generic class with the +/// specified list of variables. +/// \param class_type: the class +/// \param type_variables: vector of type variables +/// \return: A reference to the java generic class type. +java_implicitly_generic_class_typet +require_type::require_complete_java_implicitly_generic_class( + const typet &class_type, + const std::initializer_list &implicit_type_variables) +{ + require_complete_class(class_type); + return require_java_implicitly_generic_class( + class_type, implicit_type_variables); +} + +/// Verify that a class is a valid nongeneric java class /// \param class_type: the class /// \return: A reference to the java generic class type. java_class_typet require_type::require_java_non_generic_class(const typet &class_type) { - const class_typet &class_class_type = require_complete_class(class_type); - java_class_typet java_class_type = to_java_class_type(class_class_type); + REQUIRE(class_type.id() == ID_struct); + + const class_typet &class_class_type = to_class_type(class_type); + const java_class_typet &java_class_type = + to_java_class_type(class_class_type); REQUIRE(!is_java_generic_class_type(java_class_type)); REQUIRE(!is_java_implicitly_generic_class_type(java_class_type)); @@ -332,6 +408,16 @@ require_type::require_java_non_generic_class(const typet &class_type) return java_class_type; } +/// Verify that a class is a complete, valid nongeneric java class +/// \param class_type: the class +/// \return: A reference to the java generic class type. +java_class_typet +require_type::require_complete_java_non_generic_class(const typet &class_type) +{ + require_complete_class(class_type); + return require_java_non_generic_class(class_type); +} + /// Verify a given type is a symbol type, optionally with a specific identifier /// \param type: The type to check /// \param identifier: The identifier the symbol type should have diff --git a/unit/testing-utils/require_type.h b/unit/testing-utils/require_type.h index ccf5db53315..66c76940a7a 100644 --- a/unit/testing-utils/require_type.h +++ b/unit/testing-utils/require_type.h @@ -70,9 +70,20 @@ const typet &require_java_non_generic_type( const typet &type, const optionalt &expect_subtype); +class_typet require_complete_class(const typet &class_type); + +class_typet require_incomplete_class(const typet &class_type); + java_generic_class_typet require_java_generic_class(const typet &class_type); java_generic_class_typet require_java_generic_class( + const typet &class_type, + const std::initializer_list &type_variables); + +java_generic_class_typet +require_complete_java_generic_class(const typet &class_type); + +java_generic_class_typet require_complete_java_generic_class( const typet &class_type, const std::initializer_list &type_parameters); @@ -83,8 +94,19 @@ java_implicitly_generic_class_typet require_java_implicitly_generic_class( const typet &class_type, const std::initializer_list &implicit_type_variables); +java_implicitly_generic_class_typet +require_complete_java_implicitly_generic_class(const typet &class_type); + +java_implicitly_generic_class_typet +require_complete_java_implicitly_generic_class( + const typet &class_type, + const std::initializer_list &implicit_type_variables); + java_class_typet require_java_non_generic_class(const typet &class_type); +java_class_typet +require_complete_java_non_generic_class(const typet &class_type); + java_generic_symbol_typet require_java_generic_symbol_type( const typet &type, const std::string &identifier);