[SEC-180] Add ability to overlay classes with new definitions of existing methods

regression/cbmc-java/generics_type_param/test.desc

@@ -3,9 +3,9 @@ GenericFields$SimpleGenericField.class
 --cover location --function GenericFields\$SimpleGenericField.foo --verbosity 10
 ^EXIT=0$
 ^SIGNAL=0$
-Reading class AWrapper
-Reading class FWrapper
-Reading class IWrapper
+Parsing class AWrapper
+Parsing class FWrapper
+Parsing class IWrapper
 --
 failed to load class \`AWrapper\'
 failed to load class \`FWrapper\'

regression/cbmc-java/overlay-class/Test.java

@@ -0,0 +1,14 @@
+public class Test
+{
+  public int x;
+
+  public static void main(String[] args)
+  {
+    assert(false);
+  }
+
+  public static void notOverlain()
+  {
+    assert(true);
+  }
+}

regression/cbmc-java/overlay-class/annotations/com/diffblue/OverlayClassImplementation.java

@@ -0,0 +1,4 @@
+package com.diffblue;
+
+public @interface OverlayClassImplementation {
+}

regression/cbmc-java/overlay-class/annotations/com/diffblue/OverlayMethodImplementation.java

@@ -0,0 +1,4 @@
+package com.diffblue;
+
+public @interface OverlayMethodImplementation {
+}

regression/cbmc-java/overlay-class/correct-overlay/Test.java

@@ -0,0 +1,14 @@
+import com.diffblue.OverlayClassImplementation;
+import com.diffblue.OverlayMethodImplementation;
+
+@OverlayClassImplementation
+public class Test
+{
+  public int x;
+
+  @OverlayMethodImplementation
+  public static void main(String[] args)
+  {
+    assert(true);
+  }
+}

regression/cbmc-java/overlay-class/correct-test.desc

@@ -0,0 +1,17 @@
+CORE
+Test.class
+--classpath `./format_classpath.sh . annotations correct-overlay` --verbosity 10
+^Getting class `Test' from file \.[\\/]Test\.class$
+^Getting class `Test' from file correct-overlay[\\/]Test\.class$
+^Adding symbol from overlay class:  field 'x'$
+^Adding symbol from overlay class:  method 'java::Test\.<init>:\(\)V'$
+^Field definition for java::Test\.x already loaded from overlay class$
+^Adding symbol from overlay class:  method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
+^Method java::Test\.<init>:\(\)V exists in an overlay class without being marked as an overlay and also exists in the underlying class
+^Adding symbol:  method 'java::Test\.notOverlain:\(\)V'$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^Skipping class Test marked with OverlayClassImplementation but found before original definition$
+^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$

regression/cbmc-java/overlay-class/duplicate-test.desc

@@ -0,0 +1,17 @@
+CORE
+Test.class
+--classpath `./format_classpath.sh . annotations . correct-overlay` --verbosity 10
+^Getting class `Test' from file \.[\\/]Test\.class$
+^Getting class `Test' from file correct-overlay[\\/]Test\.class$
+^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$
+^Adding symbol from overlay class:  field 'x'$
+^Adding symbol from overlay class:  method 'java::Test\.<init>:\(\)V'$
+^Field definition for java::Test\.x already loaded from overlay class$
+^Adding symbol from overlay class:  method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
+^Method java::Test\.<init>:\(\)V exists in an overlay class without being marked as an overlay and also exists in the underlying class
+^Adding symbol:  method 'java::Test\.notOverlain:\(\)V'$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^Skipping class Test marked with OverlayClassImplementation but found before original definition$

regression/cbmc-java/overlay-class/format_classpath.sh

@@ -0,0 +1,12 @@
+#!/bin/bash
+
+unameOut="$(uname -s)"
+case "${unameOut}" in
+    CYGWIN*)    separator=";";;
+    MINGW*)     separator=";";;
+    MSYS*)      separator=";";;
+    Windows*)   separator=";";;
+    *)          separator=":"
+esac
+
+echo -n `IFS=$separator; echo "$*"`

regression/cbmc-java/overlay-class/misordered-test.desc

@@ -0,0 +1,16 @@
+CORE
+Test.class
+--classpath `./format_classpath.sh annotations correct-overlay .` --verbosity 10
+^Getting class `Test' from file correct-overlay[\\/]Test\.class$
+^Getting class `Test' from file \.[\\/]Test\.class$
+^Skipping class Test marked with OverlayClassImplementation but found before original definition$
+^Adding symbol:  field 'x'$
+^Adding symbol:  method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
+^Adding symbol:  method 'java::Test\.notOverlain:\(\)V'$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$
+^Adding symbol from overlay class
+exists in an overlay class without being marked as an overlay and also exists in the underlying class

regression/cbmc-java/overlay-class/unmarked-overlay/Test.java

@@ -0,0 +1,11 @@
+import com.diffblue.OverlayClassImplementation;
+import com.diffblue.OverlayMethodImplementation;
+
+public class Test
+{
+  @OverlayMethodImplementation
+  public static void main(String[] args)
+  {
+    assert(false);
+  }
+}

regression/cbmc-java/overlay-class/unmarked-test.desc

@@ -0,0 +1,16 @@
+CORE
+Test.class
+--classpath `./format_classpath.sh . annotations unmarked-overlay` --verbosity 10
+^Getting class `Test' from file \.[\\/]Test\.class$
+^Getting class `Test' from file unmarked-overlay[\\/]Test\.class$
+^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$
+^Adding symbol:  field 'x'$
+^Adding symbol:  method 'java::Test\.main:\(\[Ljava/lang/String;\)V'$
+^Adding symbol:  method 'java::Test\.notOverlain:\(\)V'$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^Skipping class Test marked with OverlayClassImplementation but found before original definition$
+^Adding symbol from overlay class
+exists in an overlay class without being marked as an overlay and also exists in the underlying class

src/java_bytecode/ci_lazy_methods.cpp

@@ -85,15 +85,15 @@ bool ci_lazy_methodst::operator()(
       reachable_classes.push_back(main_class);
     else
       reachable_classes = main_jar_classes;
-    for(const auto &classname : reachable_classes)
+    for(const irep_idt &class_name : reachable_classes)
     {
-      const auto &methods=
-        java_class_loader.class_map.at(classname).parsed_class.methods;
+      const auto &methods =
+        java_class_loader.get_original_class(class_name).parsed_class.methods;
       for(const auto &method : methods)
       {
-        const irep_idt methodid="java::"+id2string(classname)+"."+
-          id2string(method.name)+":"+
-          id2string(method.descriptor);
+        const irep_idt methodid =
+          "java::" + id2string(class_name) + "." + id2string(method.name)
+            + ":" + id2string(method.descriptor);
         method_worklist2.push_back(methodid);
       }
     }