Add brief documentation of overlay classes

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 {
+}

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 {
 }

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 {
 }

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);
+  }
+}

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'$

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

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)
 {