Merge pull request #1019 from cristina-david/feature/refactor-exception-instrumentation

Refactor runtime exception instrumentation

Author: smowton

regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class

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

regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.java

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

regression/cbmc-java/ArrayIndexOutOfBoundsException1/test.desc

@@ -0,0 +1,13 @@
+public class ClassCastExceptionTest {
+  public static void main(String args[]) {
+      try {
+          Object x = new Integer(0);
+          String y = (String)x;
+          throw new RuntimeException();
+      }
+      catch (ClassCastException exc) {
+          assert false;
+      }
+    
+  }
+}

regression/cbmc-java/ClassCastException1/A.class

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

regression/cbmc-java/ClassCastException1/B.class

@@ -0,0 +1,21 @@
+class A {}
+
+class B extends A {}
+
+class C extends B {}
+
+public class ClassCastExceptionTest {
+  public static void main(String args[]) {
+      try {
+          A c = new C();
+          B b = (B)c;
+          // TODO: an explicit throw is currently needed in order
+          // for CBMC to convert the exception handler
+          throw new RuntimeException();
+      }
+      catch (ClassCastException exc) {
+          assert false;
+      }
+    
+  }
+}

regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.class

@@ -0,0 +1,8 @@
+CORE
+ClassCastExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java

@@ -0,0 +1,20 @@
+class B extends RuntimeException {}
+
+class A {
+    int i;
+}
+
+public class Test {
+    public static void main(String args[]) {
+        A a=null;
+        try {
+            a.i=0;
+            // TODO: an explicit throw is currently needed in order
+            // for CBMC to convert the exception handler
+            throw new B();
+        }
+        catch (NullPointerException exc) {
+            assert false;
+        }
+    }
+}

regression/cbmc-java/ClassCastException1/test.desc

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

regression/cbmc-java/ClassCastException2/A.class

@@ -0,0 +1,20 @@
+class B extends RuntimeException {}
+
+class A {
+    int i;
+}
+
+public class Test {
+    public static void main(String args[]) {
+        A a=null;
+        try {
+            int i=a.i;
+            // TODO: an explicit throw is currently needed in order
+            // for CBMC to convert the exception handler
+            throw new B();
+        }
+        catch (NullPointerException exc) {
+            assert false;
+        }
+    }
+}

regression/cbmc-java/ClassCastException2/B.class

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

regression/cbmc-java/ClassCastException2/C.class

@@ -1070,6 +1070,7 @@ void cbmc_parse_optionst::help()
     // NOLINTNEXTLINE(whitespace/line_length)
     " --java-max-vla-length        limit the length of user-code-created arrays\n"
     // NOLINTNEXTLINE(whitespace/line_length)
+    " --java-throw-runtime-exceptions Make implicit runtime exceptions explicit"
     " --java-cp-include-files      regexp or JSON list of files to load (with '@' prefix)\n"
     " --java-unwind-enum-static    try to unwind loops in static initialization of enums\n"
     "\n"

regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.class

@@ -65,6 +65,7 @@ class optionst;
   "(graphml-witness):" \
   "(java-max-vla-length):(java-unwind-enum-static)" \
   "(java-cp-include-files):" \
+  "(java-throw-runtime-exceptions)" \
   "(localize-faults)(localize-faults-method):" \
   "(lazy-methods)" \
   "(test-invariant-failure)" \

regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.java

@@ -5,6 +5,7 @@ SRC = bytecode_info.cpp \
       jar_file.cpp \
       java_bytecode_convert_class.cpp \
       java_bytecode_convert_method.cpp \
+      java_bytecode_instrument.cpp \
       java_bytecode_internal_additions.cpp \
       java_bytecode_language.cpp \
       java_bytecode_parse_tree.cpp \

regression/cbmc-java/ClassCastException2/test.desc

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_types.h"
 #include "java_bytecode_convert_method.h"
 #include "java_bytecode_language.h"
+#include "java_utils.h"
 
 #include <util/arith_tools.h>
 #include <util/namespace.h>
@@ -56,7 +57,10 @@ class java_bytecode_convert_classt:public messaget
       string_preprocess.add_string_type(
         parse_tree.parsed_class.name, symbol_table);
     else if(!loading_success)
-      generate_class_stub(parse_tree.parsed_class.name);
+      generate_class_stub(
+        parse_tree.parsed_class.name,
+        symbol_table,
+        get_message_handler());
   }
 
   typedef java_bytecode_parse_treet::classt classt;
@@ -73,7 +77,6 @@ class java_bytecode_convert_classt:public messaget
   void convert(const classt &c);
   void convert(symbolt &class_symbol, const fieldt &f);
 
-  void generate_class_stub(const irep_idt &class_name);
   void add_array_types();
 };
 
@@ -171,40 +174,6 @@ void java_bytecode_convert_classt::convert(const classt &c)
     java_root_class(*class_symbol);
 }
 
-void java_bytecode_convert_classt::generate_class_stub(
-  const irep_idt &class_name)
-{
-  class_typet class_type;
-
-  class_type.set_tag(class_name);
-  class_type.set(ID_base_name, class_name);
-
-  class_type.set(ID_incomplete_class, true);
-
-  // produce class symbol
-  symbolt new_symbol;
-  new_symbol.base_name=class_name;
-  new_symbol.pretty_name=class_name;
-  new_symbol.name="java::"+id2string(class_name);
-  class_type.set(ID_name, new_symbol.name);
-  new_symbol.type=class_type;
-  new_symbol.mode=ID_java;
-  new_symbol.is_type=true;
-
-  symbolt *class_symbol;
-
-  if(symbol_table.move(new_symbol, class_symbol))
-  {
-    warning() << "stub class symbol " << new_symbol.name
-              << " already exists" << eom;
-  }
-  else
-  {
-    // create the class identifier etc
-    java_root_class(*class_symbol);
-  }
-}
-
 void java_bytecode_convert_classt::convert(
   symbolt &class_symbol,
   const fieldt &f)