diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h index b23bdad6469..628c5bab08c 100644 --- a/src/ansi-c/ansi_c_language.h +++ b/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 new_language() override { return util_make_unique(); } diff --git a/src/cpp/cpp_language.h b/src/cpp/cpp_language.h index 3f474005f15..a3db8124f44 100644 --- a/src/cpp/cpp_language.h +++ b/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 new_language() override { return util_make_unique(); } diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 4df96cddc3e..8540991bc94 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -16,38 +16,41 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#include +#include +#include +#include +#include + #include + +#include + #include -#include -#include +#include +#include #include -#include +#include +#include +#include #include #include +#include #include #include #include #include -#include +#include #include #include -#include -#include -#include - -#include -#include -#include -#include -#include -#include -#include -#include - -#include #include +#include + +#include +#include #include #include @@ -55,13 +58,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - -#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, diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index c2b7bbb34ca..27601f421f8 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -16,53 +16,52 @@ Author: Peter Schrammel #include #include -#include -#include -#include -#include -#include - -#include +#include #include +#include #include +#include +#include #include +#include +#include +#include +#include #include -#include +#include #include +#include #include -#include -#include +#include #include -#include -#include #include #include -#include #include #include -#include -#include - -#include -#include #include -#include +#include +#include #include -#include -#include +#include #include -#include +#include + +#include +#include +#include +#include +#include +#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), diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index c16ba9f9ae0..40b86a50f29 100644 --- a/src/goto-programs/Makefile +++ b/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 \ diff --git a/src/java_bytecode/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp similarity index 100% rename from src/java_bytecode/remove_exceptions.cpp rename to src/goto-programs/remove_exceptions.cpp diff --git a/src/java_bytecode/remove_exceptions.h b/src/goto-programs/remove_exceptions.h similarity index 100% rename from src/java_bytecode/remove_exceptions.h rename to src/goto-programs/remove_exceptions.h diff --git a/src/java_bytecode/remove_instanceof.cpp b/src/goto-programs/remove_instanceof.cpp similarity index 94% rename from src/java_bytecode/remove_instanceof.cpp rename to src/goto-programs/remove_instanceof.cpp index cb93fcbbb98..02e998eeb9b 100644 --- a/src/java_bytecode/remove_instanceof.cpp +++ b/src/goto-programs/remove_instanceof.cpp @@ -14,8 +14,10 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include +#include +#include + #include -#include #include @@ -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(), diff --git a/src/java_bytecode/remove_instanceof.h b/src/goto-programs/remove_instanceof.h similarity index 100% rename from src/java_bytecode/remove_instanceof.h rename to src/goto-programs/remove_instanceof.h diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index a242577e8cd..64d091e12c6 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -12,8 +12,14 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include +#include + +#include +#include #include +#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; } diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index 13aa8e6c2ca..3fa30f99a32 100644 --- a/src/java_bytecode/Makefile +++ b/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 \ diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp index ccb892a296c..62c03ad2a85 100644 --- a/src/java_bytecode/ci_lazy_methods.cpp +++ b/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 +#include #include -#include /// Constructor for lazy-method loading /// \param symbol_table: the symbol table to use diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 9b221d4298c..fd0eb17e9a4 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -13,14 +13,22 @@ Author: Daniel Kroening, kroening@kroening.com #include #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 + +#include +#include +#include +#include + +#include #include #include @@ -32,18 +40,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - -#include -#include -#include -#include - -#include #include #include -#include +#include #include +#include /// Given a string of the format '?blah?', will return true when compared /// against a string that matches appart from any characters that are '?' diff --git a/src/java_bytecode/java_bytecode_internal_additions.cpp b/src/java_bytecode/java_bytecode_internal_additions.cpp index 106cd0fb642..9229aab3fec 100644 --- a/src/java_bytecode/java_bytecode_internal_additions.cpp +++ b/src/java_bytecode/java_bytecode_internal_additions.cpp @@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_bytecode_internal_additions.h" // For INFLIGHT_EXCEPTION_VARIABLE_NAME -#include "remove_exceptions.h" +#include #include #include diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index cfcb797cc40..3e7aeb5f90c 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/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() { } diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index 47d5fb69d82..268c5256fe2 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/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 new_language() override { return util_make_unique(); } diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 2556ee4d7e9..a8aaa7bdccd 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -8,15 +8,30 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_entry_point.h" -#include -#include -#include +#include +#include +#include -#include +#include #include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + #include "java_object_factory.h" +#include "java_types.h" #include "java_utils.h" static void create_initialize(symbol_table_baset &symbol_table) diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 031d7aec587..8a30327613f 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -16,49 +16,48 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include -#include -#include - -#include - #include +#include + #include #include #include #include #include #include -#include -#include #include -#include +#include +#include +#include #include +#include +#include #include #include #include #include -#include - #include #include #include -#include - -#include +#include #include #include -#include -#include -#include #include +#include -#include +#include +#include + +#include + +#include +#include +#include +#include jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv): parse_options_baset(JBMC_OPTIONS, argc, argv), diff --git a/src/jsil/jsil_language.h b/src/jsil/jsil_language.h index 8b902b86ded..b1419f5a9f7 100644 --- a/src/jsil/jsil_language.h +++ b/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 new_language() override { return util_make_unique(); } diff --git a/src/langapi/language.h b/src/langapi/language.h index 9e35daa17c9..6a7c5cecec5 100644 --- a/src/langapi/language.h +++ b/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 new_language()=0; void set_should_generate_opaque_method_stubs(bool should_generate_stubs);