cbmc: remove dependency on java_bytecode

Author: Daniel Kroening

src/cbmc/CMakeLists.txt

@@ -16,7 +16,6 @@ target_link_libraries(cbmc-lib
     goto-instrument-lib
     goto-programs
     goto-symex
-    java_bytecode
     json
     langapi
     linking

src/cbmc/Makefile

@@ -17,7 +17,6 @@ SRC = all_properties.cpp \
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \
-      ../java_bytecode/java_bytecode$(LIBEXT) \
       ../linking/linking$(LIBEXT) \
       ../big-int/big-int$(LIBEXT) \
       ../goto-programs/goto-programs$(LIBEXT) \

src/cbmc/cbmc_parse_options.cpp

@@ -36,9 +36,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/mm_io.h>
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/remove_function_pointers.h>
-#include <goto-programs/remove_instanceof.h>
 #include <goto-programs/remove_returns.h>
-#include <goto-programs/remove_exceptions.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_asm.h>
@@ -760,8 +758,6 @@ bool cbmc_parse_optionst::process_goto_program(
       log.get_message_handler(),
       goto_model,
       options.get_bool_option("pointer-check"));
-    // remove catch and throw (introduces instanceof)
-    remove_exceptions(goto_model);
 
     mm_io(goto_model);
 

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -25,8 +25,6 @@ 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_exceptions.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>
@@ -45,6 +43,9 @@ Author: Daniel Kroening, [email protected]
 #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>
 

src/goto-diff/goto_diff_parse_options.cpp

@@ -29,9 +29,7 @@ Author: Peter Schrammel
 #include <goto-programs/mm_io.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_exceptions.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_asm.h>
@@ -54,6 +52,8 @@ Author: Peter Schrammel
 #include <pointer-analysis/add_failed_symbols.h>
 
 #include <java_bytecode/java_bytecode_language.h>
+#include <java_bytecode/remove_instanceof.h>
+#include <java_bytecode/remove_exceptions.h>
 
 #include <langapi/mode.h>
 

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -26,8 +26,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/remove_calls_no_body.h>
 #include <goto-programs/remove_function_pointers.h>
 #include <goto-programs/remove_virtual_functions.h>
-#include <goto-programs/remove_exceptions.h>
-#include <goto-programs/remove_instanceof.h>
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/show_properties.h>
@@ -51,6 +49,9 @@ Author: Daniel Kroening, [email protected]
 #include <pointer-analysis/add_failed_symbols.h>
 #include <pointer-analysis/show_value_sets.h>
 
+#include <java_bytecode/remove_exceptions.h>
+#include <java_bytecode/remove_instanceof.h>
+
 #include <analyses/natural_loops.h>
 #include <analyses/global_may_alias.h>
 #include <analyses/local_bitvector_analysis.h>

src/goto-programs/Makefile

@@ -43,9 +43,7 @@ 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/Makefile

@@ -31,6 +31,8 @@ SRC = bytecode_info.cpp \
       java_types.cpp \
       java_utils.cpp \
       mz_zip_archive.cpp \
+      remove_exceptions.cpp \
+      remove_instanceof.cpp \
       select_pointer_type.cpp \
       # Empty last line
 

src/java_bytecode/ci_lazy_methods.cpp

@@ -5,16 +5,17 @@
  Author: Diffblue Ltd.
 
 \*******************************************************************/
+
 #include "ci_lazy_methods.h"
+#include "java_entry_point.h"
+#include "java_class_loader.h"
+#include "java_utils.h"
+#include "java_string_library_preprocess.h"
+#include "remove_exceptions.h"
 
-#include <java_bytecode/java_entry_point.h>
-#include <java_bytecode/java_class_loader.h>
-#include <java_bytecode/java_utils.h>
 #include <util/suffix.h>
-#include <java_bytecode/java_string_library_preprocess.h>
 
 #include <goto-programs/resolve_inherited_component.h>
-#include <goto-programs/remove_exceptions.h>
 
 /// Constructor for lazy-method loading
 /// \param symbol_table: the symbol table to use

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_string_library_preprocess.h"
 #include "java_types.h"
 #include "java_utils.h"
+#include "remove_exceptions.h"
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
@@ -34,7 +35,6 @@ Author: Daniel Kroening, [email protected]
 #include <linking/zero_initializer.h>
 
 #include <goto-programs/cfg.h>
-#include <goto-programs/remove_exceptions.h>
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/resolve_inherited_component.h>
 #include <analyses/cfg_dominators.h>

src/java_bytecode/java_bytecode_internal_additions.cpp

@@ -8,11 +8,12 @@ Author: Daniel Kroening, [email protected]
 
 #include "java_bytecode_internal_additions.h"
 
+// For INFLIGHT_EXCEPTION_VARIABLE_NAME
+#include "remove_exceptions.h"
+
 #include <util/std_types.h>
 #include <util/cprover_prefix.h>
 #include <util/c_types.h>
-// For INFLIGHT_EXCEPTION_VARIABLE_NAME
-#include <goto-programs/remove_exceptions.h>
 
 void java_internal_additions(symbol_table_baset &dest)
 {

src/java_bytecode/java_entry_point.cpp

@@ -29,8 +29,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/string_constant.h>
 #include <util/suffix.h>
 
-#include <goto-programs/remove_exceptions.h>
-
+#include "remove_exceptions.h"
 #include "java_object_factory.h"
 #include "java_types.h"
 #include "java_utils.h"

src/goto-programs/remove_exceptions.cpp renamed to src/java_bytecode/remove_exceptions.cpp

@@ -11,8 +11,8 @@ Date:   December 2016
 /// \file
 /// Remove function exceptional returns
 
-#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_EXCEPTIONS_H
-#define CPROVER_GOTO_PROGRAMS_REMOVE_EXCEPTIONS_H
+#ifndef CPROVER_JAVA_BYTECODE_REMOVE_EXCEPTIONS_H
+#define CPROVER_JAVA_BYTECODE_REMOVE_EXCEPTIONS_H
 
 #include <goto-programs/goto_model.h>
 

src/goto-programs/remove_exceptions.h renamed to src/java_bytecode/remove_exceptions.h

@@ -11,8 +11,8 @@ Author: Chris Smowton, [email protected]
 
 #include "remove_instanceof.h"
 
-#include "class_hierarchy.h"
-#include "class_identifier.h"
+#include <goto-programs/class_hierarchy.h>
+#include <goto-programs/class_identifier.h>
 
 #include <util/fresh_symbol.h>
 #include <java_bytecode/java_types.h>

src/goto-programs/remove_instanceof.cpp renamed to src/java_bytecode/remove_instanceof.cpp

@@ -9,12 +9,13 @@ Author: Chris Smowton, [email protected]
 /// \file
 /// Remove Instance-of Operators
 
-#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_INSTANCEOF_H
-#define CPROVER_GOTO_PROGRAMS_REMOVE_INSTANCEOF_H
+#ifndef CPROVER_JAVA_BYTECODE_REMOVE_INSTANCEOF_H
+#define CPROVER_JAVA_BYTECODE_REMOVE_INSTANCEOF_H
 
 #include <util/symbol_table.h>
-#include "goto_functions.h"
-#include "goto_model.h"
+
+#include <goto-programs/goto_functions.h>
+#include <goto-programs/goto_model.h>
 
 void remove_instanceof(
   goto_programt::targett target,

src/goto-programs/remove_instanceof.h renamed to src/java_bytecode/remove_instanceof.h

@@ -32,9 +32,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/remove_virtual_functions.h>
-#include <goto-programs/remove_instanceof.h>
 #include <goto-programs/remove_returns.h>
-#include <goto-programs/remove_exceptions.h>
 #include <goto-programs/remove_asm.h>
 #include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_skip.h>
@@ -56,6 +54,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_enum_static_init_unwind_handler.h>
+#include <java_bytecode/remove_instanceof.h>
+#include <java_bytecode/remove_exceptions.h>
 
 #include <cbmc/version.h>
 

src/jbmc/jbmc_parse_options.cpp

@@ -12,13 +12,17 @@
 
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/remove_virtual_functions.h>
+#include <goto-programs/remove_returns.h>
+#include <goto-programs/replace_java_nondet.h>
+
+#include <java_bytecode/remove_instanceof.h>
+
 #include <util/config.h>
-#include <goto-instrument/cover.h>
 #include <util/options.h>
+
+#include <goto-instrument/cover.h>
+
 #include <iostream>
-#include <goto-programs/remove_returns.h>
-#include <goto-programs/replace_java_nondet.h>
-#include <goto-programs/remove_instanceof.h>
 
 void validate_method_removal(
   std::list<goto_programt::instructiont> instructions)