[SEC-180] Overlay classes

regression/cbmc-java/invalid_classpath/Test.java

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

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

@@ -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-path.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/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

regression/cbmc-java/provide_object_implementation/java/lang/Object.java

@@ -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/provide_object_implementation/test.desc

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

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