From 6ff1eec0eecf7bb9dda805268d73e2b84e14eef8 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Tue, 17 Apr 2018 15:33:09 +0100
Subject: [PATCH] cbmc: remove dependency on java_bytecode

---
 src/cbmc/CMakeLists.txt                              |  1 -
 src/cbmc/Makefile                                    |  1 -
 src/cbmc/cbmc_parse_options.cpp                      |  4 ----
 src/goto-analyzer/goto_analyzer_parse_options.cpp    |  5 +++--
 src/goto-diff/goto_diff_parse_options.cpp            |  4 ++--
 .../goto_instrument_parse_options.cpp                |  5 +++--
 src/goto-programs/Makefile                           |  2 --
 src/java_bytecode/Makefile                           |  2 ++
 src/java_bytecode/ci_lazy_methods.cpp                | 11 ++++++-----
 src/java_bytecode/java_bytecode_convert_method.cpp   |  2 +-
 .../java_bytecode_internal_additions.cpp             |  5 +++--
 src/java_bytecode/java_entry_point.cpp               |  3 +--
 .../remove_exceptions.cpp                            |  0
 .../remove_exceptions.h                              |  4 ++--
 .../remove_instanceof.cpp                            |  4 ++--
 .../remove_instanceof.h                              |  9 +++++----
 src/jbmc/jbmc_parse_options.cpp                      |  4 ++--
 .../java_replace_nondet/replace_nondet.cpp           | 12 ++++++++----
 18 files changed, 40 insertions(+), 38 deletions(-)
 rename src/{goto-programs => java_bytecode}/remove_exceptions.cpp (100%)
 rename src/{goto-programs => java_bytecode}/remove_exceptions.h (91%)
 rename src/{goto-programs => java_bytecode}/remove_instanceof.cpp (98%)
 rename src/{goto-programs => java_bytecode}/remove_instanceof.h (79%)

diff --git a/src/cbmc/CMakeLists.txt b/src/cbmc/CMakeLists.txt
index cf0034f5484..b1cae0f8b01 100644
--- a/src/cbmc/CMakeLists.txt
+++ b/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
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
index c1d88efa6be..9da2d96efc2 100644
--- a/src/cbmc/Makefile
+++ b/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) \
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index c3b88a93bd7..5962d65ecc9 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -36,9 +36,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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);
 
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 2e7cddeb793..4df96cddc3e 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -25,8 +25,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #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, kroening@kroening.com
 #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>
 
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index 232ebf029b3..c2b7bbb34ca 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/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>
 
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index a628391a106..61c5f1265ca 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -26,8 +26,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #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, kroening@kroening.com
 #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>
diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile
index 378bb4694f8..35f5c01050e 100644
--- a/src/goto-programs/Makefile
+++ b/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 \
diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile
index f42ce024d7f..e07faa26343 100644
--- a/src/java_bytecode/Makefile
+++ b/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
 
diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp
index 30f5deacf10..6d34d869e8e 100644
--- a/src/java_bytecode/ci_lazy_methods.cpp
+++ b/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
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index e535620a535..cdc75bad6dd 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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, kroening@kroening.com
 #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>
diff --git a/src/java_bytecode/java_bytecode_internal_additions.cpp b/src/java_bytecode/java_bytecode_internal_additions.cpp
index a8968756587..106cd0fb642 100644
--- a/src/java_bytecode/java_bytecode_internal_additions.cpp
+++ b/src/java_bytecode/java_bytecode_internal_additions.cpp
@@ -8,11 +8,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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)
 {
diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp
index 53d81c5b78e..5c3beafc357 100644
--- a/src/java_bytecode/java_entry_point.cpp
+++ b/src/java_bytecode/java_entry_point.cpp
@@ -29,8 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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"
diff --git a/src/goto-programs/remove_exceptions.cpp b/src/java_bytecode/remove_exceptions.cpp
similarity index 100%
rename from src/goto-programs/remove_exceptions.cpp
rename to src/java_bytecode/remove_exceptions.cpp
diff --git a/src/goto-programs/remove_exceptions.h b/src/java_bytecode/remove_exceptions.h
similarity index 91%
rename from src/goto-programs/remove_exceptions.h
rename to src/java_bytecode/remove_exceptions.h
index 20d83f93807..76358c640cc 100644
--- a/src/goto-programs/remove_exceptions.h
+++ b/src/java_bytecode/remove_exceptions.h
@@ -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>
 
diff --git a/src/goto-programs/remove_instanceof.cpp b/src/java_bytecode/remove_instanceof.cpp
similarity index 98%
rename from src/goto-programs/remove_instanceof.cpp
rename to src/java_bytecode/remove_instanceof.cpp
index ad62322e90a..37cb8cc3094 100644
--- a/src/goto-programs/remove_instanceof.cpp
+++ b/src/java_bytecode/remove_instanceof.cpp
@@ -11,8 +11,8 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 
 #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>
diff --git a/src/goto-programs/remove_instanceof.h b/src/java_bytecode/remove_instanceof.h
similarity index 79%
rename from src/goto-programs/remove_instanceof.h
rename to src/java_bytecode/remove_instanceof.h
index b492de5dc6b..8ff3da10328 100644
--- a/src/goto-programs/remove_instanceof.h
+++ b/src/java_bytecode/remove_instanceof.h
@@ -9,12 +9,13 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 /// \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,
diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp
index 25cce4cacd1..93306e74a03 100644
--- a/src/jbmc/jbmc_parse_options.cpp
+++ b/src/jbmc/jbmc_parse_options.cpp
@@ -32,9 +32,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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, kroening@kroening.com
 
 #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>
 
diff --git a/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp b/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
index d78dba970fa..5995ce9a288 100644
--- a/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
+++ b/unit/java_bytecode/java_replace_nondet/replace_nondet.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)