Use remove_instanceof in driver programs

This adds a remove_instanceof call wherever there was an existing remove_virtual_functions call.

Author: smowton

src/cbmc/cbmc_parse_options.cpp

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

src/goto-analyzer/goto_analyzer_parse_options.cpp

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

src/goto-programs/remove_instanceof.cpp

@@ -276,3 +276,9 @@ void remove_instanceof(
   remove_instanceoft rem(symbol_table, goto_functions);
   rem.lower_instanceof();
 }
+
+void remove_instanceof(goto_modelt &goto_model)
+{
+  remove_instanceof(
+    goto_model.symbol_table, goto_model.goto_functions);
+}

src/goto-programs/remove_instanceof.h

@@ -11,10 +11,12 @@ Author: Chris Smowton, [email protected]
 
 #include <util/symbol_table.h>
 #include "goto_functions.h"
+#include "goto_model.h"
 
 void remove_instanceof(
   symbol_tablet &symbol_table,
   goto_functionst &goto_functions);
 
+void remove_instanceof(goto_modelt &model);
 
 #endif

src/symex/symex_parse_options.cpp

@@ -32,6 +32,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_virtual_functions.h>
+#include <goto-programs/remove_instanceof.h>
 
 #include <goto-symex/rewrite_union.h>
 #include <goto-symex/adjust_float_expressions.h>
@@ -361,7 +362,10 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
     // remove stuff
     remove_complex(goto_model);
     remove_vector(goto_model);
+    // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(goto_model);
+    // Java instanceof -> clsid comparison:
+    remove_instanceof(goto_model);
     rewrite_union(goto_model);
     adjust_float_expressions(goto_model);