Generalize passes that require RTTI

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-analyzer/goto_analyzer_parse_options.cpp

@@ -16,52 +16,53 @@ Author: Daniel Kroening, [email protected]
 #include <fstream>
 #include <memory>
 
+#include <analyses/constant_propagator.h>
+#include <analyses/dependence_graph.h>
+#include <analyses/goto_check.h>
+#include <analyses/interval_domain.h>
+#include <analyses/is_threaded.h>
+#include <analyses/local_may_alias.h>
+
 #include <ansi-c/ansi_c_language.h>
+
+#include <cbmc/version.h>
+
 #include <cpp/cpp_language.h>
-#include <java_bytecode/java_bytecode_language.h>
-#include <jsil/jsil_language.h>
 
+#include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_inline.h>
 #include <goto-programs/initialize_goto_model.h>
-#include <goto-programs/set_properties.h>
+#include <goto-programs/link_to_library.h>
+#include <goto-programs/read_goto_binary.h>
+#include <goto-programs/remove_exceptions.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>
 #include <goto-programs/remove_asm.h>
-#include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/set_properties.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/show_symbol_table.h>
-#include <goto-programs/read_goto_binary.h>
-#include <goto-programs/goto_inline.h>
-#include <goto-programs/link_to_library.h>
-
-#include <analyses/is_threaded.h>
-#include <analyses/goto_check.h>
-#include <analyses/local_may_alias.h>
-#include <analyses/constant_propagator.h>
-#include <analyses/dependence_graph.h>
-#include <analyses/interval_domain.h>
 
-#include <java_bytecode/remove_exceptions.h>
-#include <java_bytecode/remove_instanceof.h>
-
-#include <langapi/mode.h>
 #include <langapi/language.h>
+#include <langapi/mode.h>
+
+#include <java_bytecode/java_bytecode_language.h>
+#include <jsil/jsil_language.h>
 
 #include <util/options.h>
 #include <util/config.h>
 #include <util/string2int.h>
 #include <util/unicode.h>
 #include <util/exit_codes.h>
 
-#include <cbmc/version.h>
-
-#include "taint_analysis.h"
-#include "unreachable_instructions.h"
 #include "static_show_domain.h"
 #include "static_simplifier.h"
 #include "static_verifier.h"
+#include "taint_analysis.h"
+#include "unreachable_instructions.h"
 
 goto_analyzer_parse_optionst::goto_analyzer_parse_optionst(
   int argc,

src/goto-diff/goto_diff_parse_options.cpp

@@ -16,53 +16,52 @@ Author: Peter Schrammel
 #include <iostream>
 #include <memory>
 
-#include <util/string2int.h>
-#include <util/config.h>
-#include <util/options.h>
-#include <util/make_unique.h>
-#include <util/exit_codes.h>
-
-#include <langapi/language.h>
+#include <cbmc/version.h>
 
 #include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_inline.h>
 #include <goto-programs/instrument_preconditions.h>
+#include <goto-programs/link_to_library.h>
+#include <goto-programs/loop_ids.h>
 #include <goto-programs/mm_io.h>
+#include <goto-programs/read_goto_binary.h>
+#include <goto-programs/remove_asm.h>
+#include <goto-programs/remove_complex.h>
+#include <goto-programs/remove_exceptions.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_skip.h>
 #include <goto-programs/remove_vector.h>
-#include <goto-programs/remove_complex.h>
-#include <goto-programs/remove_asm.h>
+#include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/remove_unused_functions.h>
-#include <goto-programs/remove_skip.h>
-#include <goto-programs/goto_inline.h>
 #include <goto-programs/show_properties.h>
 #include <goto-programs/set_properties.h>
-#include <goto-programs/read_goto_binary.h>
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
-#include <goto-programs/loop_ids.h>
-#include <goto-programs/link_to_library.h>
-
-#include <goto-symex/rewrite_union.h>
-#include <goto-symex/adjust_float_expressions.h>
 
 #include <goto-instrument/cover.h>
 
-#include <pointer-analysis/add_failed_symbols.h>
+#include <goto-symex/adjust_float_expressions.h>
+#include <goto-symex/rewrite_union.h>
 
 #include <java_bytecode/java_bytecode_language.h>
-#include <java_bytecode/remove_instanceof.h>
-#include <java_bytecode/remove_exceptions.h>
 
+#include <langapi/language.h>
 #include <langapi/mode.h>
 
-#include <cbmc/version.h>
+#include <pointer-analysis/add_failed_symbols.h>
+
+#include <util/config.h>
+#include <util/exit_codes.h>
+#include <util/make_unique.h>
+#include <util/options.h>
+#include <util/string2int.h>
 
+#include "change_impact.h"
 #include "goto_diff.h"
 #include "syntactic_diff.h"
 #include "unified_diff.h"
-#include "change_impact.h"
 
 goto_diff_parse_optionst::goto_diff_parse_optionst(int argc, const char **argv):
   parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv),

src/goto-programs/Makefile

@@ -43,7 +43,9 @@ SRC = basic_blocks.cpp \
       remove_calls_no_body.cpp \
       remove_complex.cpp \
       remove_const_function_pointers.cpp \
+      remove_exceptions.cpp \
       remove_function_pointers.cpp \
+      remove_instanceof.cpp \
       remove_returns.cpp \
       remove_skip.cpp \
       remove_unreachable.cpp \

src/java_bytecode/remove_instanceof.cpp → 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/goto-programs/remove_virtual_functions.cpp

@@ -12,8 +12,14 @@ Author: Daniel Kroening, [email protected]
 
 #include <algorithm>
 
+#include <langapi/language.h>
+#include <langapi/mode.h>
+
+#include <util/c_types.h>
+#include <util/prefix.h>
 #include <util/type_eq.h>
 
+#include "class_hierarchy.h"
 #include "class_identifier.h"
 #include "goto_model.h"
 #include "resolve_inherited_component.h"
@@ -315,6 +321,10 @@ void remove_virtual_functionst::get_child_functions_rec(
   if(findit==class_hierarchy.class_map.end())
     return;
 
+  const auto language = get_language_from_identifier(ns, this_id);
+  CHECK_RETURN(language);
+  const irep_idt root_base_class_type_name =
+    language->root_base_class_type().get_identifier();
   for(const auto &child : findit->second.children)
   {
     // Skip if we have already visited this and we found a function call that
@@ -324,7 +334,7 @@ void remove_virtual_functionst::get_child_functions_rec(
       it != entry_map.end() &&
       !has_prefix(
         id2string(it->second.symbol_expr.get_identifier()),
-        "java::java.lang.Object"))
+        id2string(root_base_class_type_name)))
     {
       continue;
     }

src/java_bytecode/Makefile

@@ -31,8 +31,6 @@ SRC = bytecode_info.cpp \
       java_types.cpp \
       java_utils.cpp \
       mz_zip_archive.cpp \
-      remove_exceptions.cpp \
-      remove_instanceof.cpp \
       remove_java_new.cpp \
       replace_java_nondet.cpp \
       select_pointer_type.cpp \

src/java_bytecode/ci_lazy_methods.cpp

@@ -11,11 +11,11 @@
 #include "java_class_loader.h"
 #include "java_utils.h"
 #include "java_string_library_preprocess.h"
-#include "remove_exceptions.h"
 
+#include <goto-programs/remove_exceptions.h>
+#include <goto-programs/resolve_inherited_component.h>
 #include <util/suffix.h>
 
-#include <goto-programs/resolve_inherited_component.h>
 
 /// Constructor for lazy-method loading
 /// \param symbol_table: the symbol table to use

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -13,14 +13,22 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #endif
 
+#include "bytecode_info.h"
 #include "java_bytecode_convert_method.h"
 #include "java_bytecode_convert_method_class.h"
-#include "bytecode_info.h"
 #include "java_static_initializers.h"
 #include "java_string_library_preprocess.h"
 #include "java_types.h"
 #include "java_utils.h"
-#include "remove_exceptions.h"
+
+#include <analyses/cfg_dominators.h>
+
+#include <goto-programs/cfg.h>
+#include <goto-programs/class_hierarchy.h>
+#include <goto-programs/remove_exceptions.h>
+#include <goto-programs/resolve_inherited_component.h>
+
+#include <linking/zero_initializer.h>
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
@@ -32,18 +40,11 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/string2int.h>
 
-#include <linking/zero_initializer.h>
-
-#include <goto-programs/cfg.h>
-#include <goto-programs/class_hierarchy.h>
-#include <goto-programs/resolve_inherited_component.h>
-#include <analyses/cfg_dominators.h>
-
-#include <limits>
 #include <algorithm>
 #include <functional>
-#include <unordered_set>
+#include <limits>
 #include <regex>
+#include <unordered_set>
 
 /// Given a string of the format '?blah?', will return true when compared
 /// against a string that matches appart from any characters that are '?'

src/java_bytecode/java_bytecode_internal_additions.cpp

@@ -9,7 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_bytecode_internal_additions.h"
 
 // For INFLIGHT_EXCEPTION_VARIABLE_NAME
-#include "remove_exceptions.h"
+#include <goto-programs/remove_exceptions.h>
 
 #include <util/std_types.h>
 #include <util/cprover_prefix.h>

src/java_bytecode/java_bytecode_language.cpp

@@ -1091,6 +1091,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/java_bytecode/java_entry_point.cpp

@@ -8,15 +8,30 @@ Author: Daniel Kroening, [email protected]
 
 #include "java_entry_point.h"
 
-#include <util/config.h>
-#include <util/string_constant.h>
-#include <util/suffix.h>
+#include <algorithm>
+#include <set>
+#include <unordered_set>
 
-#include <goto-programs/goto_functions.h>
+#include <goto-programs/remove_exceptions.h>
 
 #include <linking/static_lifetime_init.h>
 
+#include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/config.h>
+#include <util/cprover_prefix.h>
+#include <util/message.h>
+#include <util/namespace.h>
+#include <util/pointer_offset_size.h>
+#include <util/prefix.h>
+#include <util/std_code.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
+#include <util/string_constant.h>
+#include <util/suffix.h>
+
 #include "java_object_factory.h"
+#include "java_types.h"
 #include "java_utils.h"
 
 static void create_initialize(symbol_table_baset &symbol_table)