Remove java_bytecode dependency from remove_instanceof

Author: peterschrammel

src/ansi-c/ansi_c_language.h

@@ -63,6 +63,12 @@ class ansi_c_languaget:public languaget
     exprt &expr,
     const namespacet &ns) override;
 
+  symbol_typet root_base_class_type() override
+  {
+    // does not exist
+    UNREACHABLE;
+  }
+
   std::unique_ptr<languaget> new_language() override
   { return util_make_unique<ansi_c_languaget>(); }
 

src/cpp/cpp_language.h

@@ -75,6 +75,12 @@ class cpp_languaget:public languaget
     exprt &expr,
     const namespacet &ns) override;
 
+  symbol_typet root_base_class_type() override
+  {
+    // TODO: need a synthetic wrapper with a member that holds the type_info
+    UNIMPLEMENTED;
+  }
+
   std::unique_ptr<languaget> new_language() override
   { return util_make_unique<cpp_languaget>(); }
 

src/goto-programs/remove_instanceof.cpp

@@ -14,8 +14,10 @@ Author: Chris Smowton, [email protected]
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/class_identifier.h>
 
+#include <langapi/mode.h>
+#include <langapi/language.h>
+
 #include <util/fresh_symbol.h>
-#include <java_bytecode/java_types.h>
 
 #include <sstream>
 
@@ -100,9 +102,13 @@ std::size_t remove_instanceoft::lower_instanceof(
   // We actually insert the assignment instruction after the existing one.
   // This will briefly be ill-formed (use before def of instanceof_tmp) but the
   // two will subsequently switch places. This makes sure that the inserted
-  // assignement doesn't end up before any labels pointing at this instruction.
-  symbol_typet jlo=to_symbol_type(java_lang_object_type().subtype());
-  exprt object_clsid=get_class_identifier_field(check_ptr, jlo, ns);
+  // assignment doesn't end up before any labels pointing at this instruction.
+  const irep_idt &mode = get_mode_from_identifier(
+    ns, to_symbol_type(target_type).get_identifier());
+  const auto language = get_language_from_mode(mode);
+  CHECK_RETURN(language);
+  exprt object_clsid =
+    get_class_identifier_field(check_ptr, language->root_base_class_type(), ns);
 
   symbolt &newsym = get_fresh_aux_symbol(
     object_clsid.type(),

src/java_bytecode/java_bytecode_language.cpp

@@ -1087,6 +1087,11 @@ bool java_bytecode_languaget::to_expr(
   return true; // fail for now
 }
 
+symbol_typet java_bytecode_languaget::root_base_class_type()
+{
+  return to_symbol_type(java_lang_object_type().subtype());
+}
+
 java_bytecode_languaget::~java_bytecode_languaget()
 {
 }

src/java_bytecode/java_bytecode_language.h

@@ -127,6 +127,8 @@ class java_bytecode_languaget:public languaget
     exprt &expr,
     const namespacet &ns) override;
 
+  symbol_typet root_base_class_type() override;
+
   std::unique_ptr<languaget> new_language() override
   { return util_make_unique<java_bytecode_languaget>(); }
 

src/jsil/jsil_language.h

@@ -60,6 +60,12 @@ class jsil_languaget:public languaget
     exprt &expr,
     const namespacet &ns) override;
 
+  virtual symbol_typet root_base_class_type() override
+  {
+    // unused
+    UNREACHABLE;
+  }
+
   virtual std::unique_ptr<languaget> new_language() override
   { return util_make_unique<jsil_languaget>(); }
 

src/langapi/language.h

@@ -156,6 +156,9 @@ class languaget:public messaget
     exprt &expr,
     const namespacet &ns)=0;
 
+  /// returns the class type that contains RTTI
+  virtual symbol_typet root_base_class_type() = 0;
+
   virtual std::unique_ptr<languaget> new_language()=0;
 
   void set_should_generate_opaque_method_stubs(bool should_generate_stubs);