diff --git a/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/IgnoredMethodImplementation.class b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/IgnoredMethodImplementation.class new file mode 100644 index 00000000000..b4f2e7ea3a3 Binary files /dev/null and b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/IgnoredMethodImplementation.class differ diff --git a/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/IgnoredMethodImplementation.java b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/IgnoredMethodImplementation.java new file mode 100644 index 00000000000..6789123fa4c --- /dev/null +++ b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/IgnoredMethodImplementation.java @@ -0,0 +1,8 @@ +package org.cprover; + +/** + * Ignored methods are documented above + * `java_bytecode_convert_classt::is_ignored_method`. + */ +public @interface IgnoredMethodImplementation { +} diff --git a/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayClassImplementation.java b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayClassImplementation.java index 5262c83ab2f..81377c12f43 100644 --- a/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayClassImplementation.java +++ b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayClassImplementation.java @@ -1,4 +1,8 @@ package org.cprover; +/** + * Overlay classes are documented above `is_overlay_class()` in + * jbmc/src/java_bytecode/java_class_loader.cpp. + */ public @interface OverlayClassImplementation { } diff --git a/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayMethodImplementation.java b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayMethodImplementation.java index b885d4b6348..337d8244d55 100644 --- a/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayMethodImplementation.java +++ b/jbmc/regression/jbmc/overlay-class/annotations/org/cprover/OverlayMethodImplementation.java @@ -1,4 +1,8 @@ package org.cprover; +/** + * Overlay methods are documented above + * `java_bytecode_convert_classt::is_overlay_method`. + */ public @interface OverlayMethodImplementation { } diff --git a/jbmc/regression/jbmc/overlay-class/ignored-method/Test.class b/jbmc/regression/jbmc/overlay-class/ignored-method/Test.class new file mode 100644 index 00000000000..2809640b3bc Binary files /dev/null and b/jbmc/regression/jbmc/overlay-class/ignored-method/Test.class differ diff --git a/jbmc/regression/jbmc/overlay-class/ignored-method/Test.java b/jbmc/regression/jbmc/overlay-class/ignored-method/Test.java new file mode 100644 index 00000000000..db380c6a7a9 --- /dev/null +++ b/jbmc/regression/jbmc/overlay-class/ignored-method/Test.java @@ -0,0 +1,12 @@ +import org.cprover.OverlayClassImplementation; +import org.cprover.IgnoredMethodImplementation; + +@OverlayClassImplementation +public class Test +{ + @IgnoredMethodImplementation + public static void main(String[] args) + { + assert(true); + } +} diff --git a/jbmc/regression/jbmc/overlay-class/ignored-test.desc b/jbmc/regression/jbmc/overlay-class/ignored-test.desc new file mode 100644 index 00000000000..3649feb74c9 --- /dev/null +++ b/jbmc/regression/jbmc/overlay-class/ignored-test.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--classpath `../../../../scripts/format_classpath.sh . annotations . ignored-method` --verbosity 10 +^Ignoring method: 'java::Test\.main:\(\[Ljava/lang/String;\)V'$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^Skipping class Test marked with OverlayClassImplementation but found before original definition$ +^Adding symbol from overlay class: method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$ diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 2a8d909d10f..306df0a0ef6 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -118,11 +118,44 @@ class java_bytecode_convert_classt:public messaget // see definition below for more info static void add_array_types(symbol_tablet &symbol_table); + /// Check if a method is an overlay method by searching for + /// `ID_overlay_method` in its list of annotations. + /// + /// An overlay method is a method with the annotation + /// \@OverlayMethodImplementation. They should only appear in + /// [overlay classes](\ref java_class_loader.cpp::is_overlay_class). They + /// will be loaded by JBMC instead of the method with the same signature + /// in the underlying class. It is an error if there is no method with the + /// same signature in the underlying class. It is an error if a method in + /// an overlay class has the same signature as a method in the underlying + /// class and it isn't marked as an overlay method or an + /// [ignored method](\ref java_bytecode_convert_classt::is_ignored_method). + /// + /// \param method: a `methodt` object from a java bytecode parse tree + /// \return true if the method is an overlay method, else false static bool is_overlay_method(const methodt &method) { return method.has_annotation(ID_overlay_method); } + /// Check if a method is an ignored method by searching for + /// `ID_ignored_method` in its list of annotations. + /// + /// An ignored method is a method with the annotation + /// \@IgnoredMethodImplementation. They will be ignored by JBMC. They are + /// intended for use in + /// [overlay classes](\ref java_class_loader.cpp::is_overlay_class), in + /// particular for methods which must exist in the overlay class so that + /// it will compile, e.g. default constructors, but which we do not want + /// to overlay the corresponding method in the + /// underlying class. It is an error if a method in + /// an overlay class has the same signature as a method in the underlying + /// class and it isn't marked as an + /// [overlay method](\ref java_bytecode_convert_classt::is_overlay_method) + /// or an ignored method. + /// + /// \param method: a `methodt` object from a java bytecode parse tree + /// \return true if the method is an ignored method, else false static bool is_ignored_method(const methodt &method) { return method.has_annotation(ID_ignored_method); @@ -468,11 +501,16 @@ void java_bytecode_convert_classt::convert( { for(const methodt &method : overlay_class.get().methods) { - if(is_ignored_method(method)) - continue; const irep_idt method_identifier = qualified_classname + "." + id2string(method.name) + ":" + method.descriptor; + if(is_ignored_method(method)) + { + debug() + << "Ignoring method: '" << method_identifier << "'" + << eom; + continue; + } if(method_bytecode.contains_method(method_identifier)) { // This method has already been discovered and added to method_bytecode @@ -511,11 +549,16 @@ void java_bytecode_convert_classt::convert( } for(const methodt &method : c.methods) { - if(is_ignored_method(method)) - continue; const irep_idt method_identifier= qualified_classname + "." + id2string(method.name) + ":" + method.descriptor; + if(is_ignored_method(method)) + { + debug() + << "Ignoring method: '" << method_identifier << "'" + << eom; + continue; + } if(method_bytecode.contains_method(method_identifier)) { // This method has already been discovered while parsing an overlay diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index 97431351e33..2d155ddb8ee 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/jbmc/src/java_bytecode/java_class_loader.cpp @@ -69,9 +69,25 @@ java_class_loadert::parse_tree_with_overlayst &java_class_loadert::operator()( } /// Check if class is an overlay class by searching for `ID_overlay_class` in -/// its list of annotations. TODO(nathan) give a short explanation about what -/// overlay classes are. -/// \param c: a `classt` object from a java byte code parse tree +/// its list of annotations. +/// +/// An overlay class is a class with the annotation +/// \@OverlayClassImplementation. They serve the following purpose. When the JVM +/// searches the classpath for a particular class, it uses the first match, +/// and ignores any later matches. JBMC, however, will take account of later +/// matches as long as they are overlay classes. The +/// first match is then referred to as the underlying class. The +/// overlay classes can change the methods of the underlying class in the +/// following ways: adding a field (by having a new field), adding a method +/// (by having a new method) or +/// [changing the definition of a method](\ref java_bytecode_convert_classt::is_overlay_method). +/// It is an error if a method in an overlay class has the same signature as +/// a method in the underlying class and it isn't marked as an +/// [overlay method](\ref java_bytecode_convert_classt::is_overlay_method) +/// or an +/// [ignored method](\ref java_bytecode_convert_classt::is_ignored_method). +/// +/// \param c: a `classt` object from a java bytecode parse tree /// \return true if parsed class is an overlay class, else false static bool is_overlay_class(const java_bytecode_parse_treet::classt &c) {