Lazy methods: mark JVM-generated exceptions as always available (fixes TG-774)

regression/cbmc-java/ArithmeticException7/ArithmeticExceptionTest.java

@@ -0,0 +1,11 @@
+public class ArithmeticExceptionTest {
+    public static void  main(String args[]) {
+        try {
+            int i=0;
+            int j=10/i;
+        }
+        catch(Exception exc) {
+            assert false;
+        }
+    }
+}

regression/cbmc-java/ArithmeticException7/java/lang/ArithmeticException.java

@@ -0,0 +1,4 @@
+package java.lang;
+
+public class ArithmeticException extends RuntimeException {
+}

regression/cbmc-java/ArithmeticException7/java/lang/RuntimeException.java

@@ -0,0 +1,4 @@
+package java.lang;
+
+public class RuntimeException extends Exception {
+}

regression/cbmc-java/ArithmeticException7/test.desc

@@ -0,0 +1,9 @@
+CORE
+ArithmeticExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$
+^VERIFICATION FAILED
+--
+^warning: ignoring

regression/cbmc-java/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.java

@@ -0,0 +1,11 @@
+public class ArrayIndexOutOfBoundsExceptionTest {
+  public static void main(String args[]) {
+      try {
+          int[] a=new int[4];
+          a[4]=0;
+      }
+      catch (Exception exc) {
+          assert false;
+      }
+  }
+}

regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.java

@@ -0,0 +1,4 @@
+package java.lang;
+
+public class ArrayIndexOutOfBoundsException extends IndexOutOfBoundsException {
+}

regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.java

@@ -0,0 +1,4 @@
+package java.lang;
+
+public class IndexOutOfBoundsException extends RuntimeException {
+}

regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.java

@@ -0,0 +1,4 @@
+package java.lang;
+
+public class RuntimeException extends Exception {
+}

regression/cbmc-java/ArrayIndexOutOfBoundsException3/test.desc

@@ -0,0 +1,9 @@
+CORE
+ArrayIndexOutOfBoundsExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/ClassCastException3/ClassCastExceptionTest.java

@@ -0,0 +1,15 @@
+class A {}
+
+class B {}
+
+public class ClassCastExceptionTest {
+  public static void main(String args[]) {
+      try {
+          Object a = new A();
+          B b = (B)a;
+      }
+      catch (Exception exc) {
+          assert false;
+      }
+  }
+}

regression/cbmc-java/ClassCastException3/java/lang/ClassCastException.java

@@ -0,0 +1,4 @@
+package java.lang;
+
+public class ClassCastException extends RuntimeException {
+}

regression/cbmc-java/ClassCastException3/java/lang/RuntimeException.java

@@ -0,0 +1,4 @@
+package java.lang;
+
+public class RuntimeException extends Exception {
+}

regression/cbmc-java/ClassCastException3/test.desc

@@ -0,0 +1,9 @@
+CORE
+ClassCastExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file ClassCastExceptionTest.java line 12 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/NegativeArraySizeException2/NegativeArraySizeExceptionTest.java

@@ -0,0 +1,10 @@
+public class NegativeArraySizeExceptionTest {
+  public static void main(String args[]) {
+      try {
+          int a[]=new int[-1];
+      }
+      catch (Exception exc) {
+          assert false;
+      }
+  }
+}

regression/cbmc-java/NegativeArraySizeException2/java/lang/NegativeArraySizeException.java

@@ -0,0 +1,4 @@
+package java.lang;
+
+public class NegativeArraySizeException extends RuntimeException {
+}

regression/cbmc-java/NegativeArraySizeException2/java/lang/RuntimeException.java

@@ -0,0 +1,4 @@
+package java.lang;
+
+public class RuntimeException extends Exception {
+}

regression/cbmc-java/NegativeArraySizeException2/test.desc

@@ -0,0 +1,9 @@
+CORE
+NegativeArraySizeExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file NegativeArraySizeExceptionTest.java line 7 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/NullPointerException4/Test.java

@@ -0,0 +1,15 @@
+class A {
+    int i;
+}
+
+public class Test {
+    public static void main(String args[]) {
+        A a=null;
+        try {
+            a.i=0;
+        }
+        catch (Exception exc) {
+            assert false;
+        }
+    }
+}

regression/cbmc-java/NullPointerException4/java/lang/NullPointerException.java

@@ -0,0 +1,4 @@
+package java.lang;
+
+public class NullPointerException extends RuntimeException {
+}

regression/cbmc-java/NullPointerException4/java/lang/RuntimeException.java

@@ -0,0 +1,4 @@
+package java.lang;
+
+public class RuntimeException extends Exception {
+}

regression/cbmc-java/NullPointerException4/test.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file Test.java line 12 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/java_bytecode/java_bytecode_instrument.cpp

@@ -8,6 +8,8 @@ Date:   June 2017
 
 \*******************************************************************/
 
+#include "java_bytecode_instrument.h"
+
 #include <util/arith_tools.h>
 #include <util/fresh_symbol.h>
 #include <util/std_code.h>
@@ -18,7 +20,6 @@ Date:   June 2017
 #include <goto-programs/goto_functions.h>
 
 #include "java_bytecode_convert_class.h"
-#include "java_bytecode_instrument.h"
 #include "java_entry_point.h"
 #include "java_root_class.h"
 #include "java_types.h"
@@ -79,6 +80,15 @@ class java_bytecode_instrumentt:public messaget
 };
 
 
+const std::vector<irep_idt> exception_needed_classes =
+{
+  "java.lang.ArithmeticException",
+  "java.lang.ArrayIndexOutOfBoundsException",
+  "java.lang.ClassCastException",
+  "java.lang.NegativeArraySizeException",
+  "java.lang.NullPointerException"
+};
+
 /// Creates a class stub for exc_name and generates a
 ///  conditional GOTO such that exc_name is thrown when
 ///  cond is met.

src/java_bytecode/java_bytecode_instrument.h

@@ -11,6 +11,10 @@ Date:   June 2017
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H
 
+#include <util/symbol_table.h>
+#include <util/message.h>
+#include <util/irep.h>
+
 void java_bytecode_instrument_symbol(
   symbol_table_baset &symbol_table,
   symbolt &symbol,
@@ -22,4 +26,6 @@ void java_bytecode_instrument(
   const bool throw_runtime_exceptions,
   message_handlert &_message_handler);
 
+extern const std::vector<irep_idt> exception_needed_classes;
+
 #endif

src/java_bytecode/java_bytecode_language.cpp

@@ -61,10 +61,19 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
   else
     lazy_methods_mode=LAZY_METHODS_MODE_EAGER;
 
+  if(cmd.isset("java-throw-runtime-exceptions"))
+  {
+    throw_runtime_exceptions = true;
+    java_load_classes.insert(
+        java_load_classes.end(),
+        exception_needed_classes.begin(),
+        exception_needed_classes.end());
+  }
   if(cmd.isset("java-load-class"))
   {
-    for(const auto &c : cmd.get_values("java-load-class"))
-      java_load_classes.push_back(c);
+    const auto &values = cmd.get_values("java-load-class");
+    java_load_classes.insert(
+        java_load_classes.end(), values.begin(), values.end());
   }
 
   const std::list<std::string> &extra_entry_points=