Add ability to overlay classes with new definitions of existing methods

Allows multiple definitions of the same class to appear on the classpath, so long as all but the first definition are marked with the attribute @java::com.diffblue.security.OverlayClassImplementation. Overlay class definitions can contain methods with the same signature as methods in the original class, so long as these are marked with the attribute @java::com.diffblue.security.OverlayMethodImplementation; such overlay methods are replaced in the original file with the version found in the last overlay on the classpath. Later definitions can also contain new supporting methods and fields that are merged in.
This will allow insertion of Java methods into library classes to handle, for example, modelling dependency injection.
Includes regression tests
Improvements over earlier version:
  Allows loading of classes such as java.lang.Object from an explicit model
  Prevent attempting to load any class more than once
  Invalid values in the classpath are ignored
  Handles duplicate files appearing in multiple items on the classpath
  Filter loaded class files to remove duplicates or misordered overlays before following links to other classes so as not to add dependencies of duplicate classes

Author: NathanJPhillips

regression/cbmc-java/invalid_classpath/Test.class

@@ -0,0 +1,3 @@
+public class Test {
+    public void main() {}
+}

regression/cbmc-java/invalid_classpath/Test.java

@@ -0,0 +1,10 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--classpath ./NotHere.jar
+^EXIT=6$
+^SIGNAL=0$
+^the program has no entry point$
+^failed to load class `Test'$
+--
+--
+symex-driven lazy loading should emit "the program has no entry point" but currently doesn't

regression/cbmc-java/invalid_classpath/test-jar.desc

@@ -0,0 +1,10 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--classpath ./NotHere
+^EXIT=6$
+^SIGNAL=0$
+^the program has no entry point$
+^failed to load class `Test'$
+--
+--
+symex-driven lazy loading should emit "the program has no entry point" but currently doesn't

regression/cbmc-java/invalid_classpath/test-path.desc

@@ -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/Test.class

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

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

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

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

@@ -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/annotations/com/diffblue/OverlayClassImplementation.java

@@ -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/annotations/com/diffblue/OverlayMethodImplementation.class

@@ -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/annotations/com/diffblue/OverlayMethodImplementation.java

@@ -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/correct-overlay/Test.class

@@ -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/correct-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/correct-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

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

@@ -0,0 +1,33 @@
+package java.lang;
+
+public class Object {
+    public final Class<?> getClass() {
+      return null;
+    }
+
+    public int hashCode() { return 0; }
+
+    public boolean equals(Object obj) { return (this == obj); }
+
+    protected Object clone() throws CloneNotSupportedException {
+      throw new CloneNotSupportedException();
+    }
+
+    public String toString() { return "object"; }
+
+    public final void notify() {}
+
+    public final void notifyAll() {}
+
+    public final void wait(long timeout) throws InterruptedException {
+      throw new InterruptedException();
+    }
+
+    public final void wait(long timeout, int nanos) throws InterruptedException {
+        wait(timeout);
+    }
+
+    public final void wait() throws InterruptedException { wait(0); }
+
+    protected void finalize() throws Throwable { }
+}

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

@@ -0,0 +1,10 @@
+CORE symex-driven-lazy-loading-expected-failure
+java/lang/Object.class
+
+^EXIT=6$
+^SIGNAL=0$
+^the program has no entry point$
+--
+^failed to add class symbol java::java\.lang\.Object$
+--
+symex-driven lazy loading should emit "the program has no entry point" but currently doesn't

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

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