Merge pull request #490 from smowton/use_remove_instanceof

Use remove instanceof

Author: Daniel Kroening

regression/cbmc-java/instanceof1/instanceof1.class

@@ -2,18 +2,6 @@ class instanceof1
 {
   public static void main(String[] args)
   {
-    // absolutely everything is an Object
     assert args instanceof Object;
-    assert int.class instanceof Object;
-    
-    // args is an array
-    assert args instanceof Object[];
-    
-    // string literals are strings
-    assert "" instanceof String;
-
-    // need a negative example, too
-    Object o=new Object();
-    assert ! (o instanceof String);
   }
 };

regression/cbmc-java/instanceof1/instanceof1.java

@@ -0,0 +1,7 @@
+class instanceof2
+{
+  public static void main(String[] args)
+  {
+    assert int.class instanceof Object;
+  }
+};

regression/cbmc-java/instanceof2/instanceof2.class

@@ -0,0 +1,8 @@
+KNOWNBUG
+instanceof2.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/instanceof2/instanceof2.java

@@ -0,0 +1,7 @@
+class instanceof3
+{
+  public static void main(String[] args)
+  {
+    assert args instanceof Object[];
+  }
+};

regression/cbmc-java/instanceof2/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+instanceof3.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/instanceof3/instanceof3.class

@@ -0,0 +1,7 @@
+class instanceof4
+{
+  public static void main(String[] args)
+  {
+    assert "" instanceof String;
+  }
+};

regression/cbmc-java/instanceof3/instanceof3.java

@@ -0,0 +1,8 @@
+CORE
+instanceof4.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/instanceof3/test.desc

@@ -0,0 +1,8 @@
+class instanceof5
+{
+  public static void main(String[] args)
+  {
+    Object o=new Object();
+    assert ! (o instanceof String);
+  }
+};

regression/cbmc-java/instanceof4/instanceof4.class

@@ -0,0 +1,8 @@
+CORE
+instanceof5.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/instanceof4/instanceof4.java

@@ -0,0 +1,15 @@
+class instanceof6
+{
+  public static void main(String[] args)
+  {
+    A[] as = { new A(), new B() };
+    assert(as[0] instanceof A);
+    assert(as[1] instanceof A);
+  }
+};
+
+class A {
+}
+
+class B extends A {
+}

regression/cbmc-java/instanceof4/test.desc

@@ -0,0 +1,8 @@
+CORE
+instanceof6.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/instanceof5/instanceof5.class

@@ -0,0 +1,15 @@
+class instanceof7
+{
+  public static void main(String[] args)
+  {
+    A[] as = { new A(), new B() };
+    assert(!(as[0] instanceof B));
+    assert(as[1] instanceof B);
+  }
+};
+
+class A {
+}
+
+class B extends A {
+}

regression/cbmc-java/instanceof5/instanceof5.java

@@ -0,0 +1,8 @@
+CORE
+instanceof7.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/instanceof5/test.desc

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_virtual_functions.h>
+#include <goto-programs/remove_instanceof.h>
 #include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_complex.h>
@@ -884,7 +885,10 @@ bool cbmc_parse_optionst::process_goto_program(
       symbol_table,
       goto_functions,
       cmdline.isset("pointer-check"));
+    // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(symbol_table, goto_functions);
+    // Java instanceof -> clsid comparison:
+    remove_instanceof(symbol_table, goto_functions);
 
     // full slice?
     if(cmdline.isset("full-slice"))

regression/cbmc-java/instanceof6/A.class

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/set_properties.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_virtual_functions.h>
+#include <goto-programs/remove_instanceof.h>
 #include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_complex.h>
@@ -380,7 +381,10 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     // remove function pointers
     status() << "Removing function pointers and virtual functions" << eom;
     remove_function_pointers(goto_model, cmdline.isset("pointer-check"));
+    // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(goto_model);
+    // Java instanceof -> clsid comparison:
+    remove_instanceof(goto_model);
 
     // do partial inlining
     status() << "Partial Inlining" << eom;