remove usage of Java bytecode frontend

Daniel Kroening · chrisr-diffblue · commit 87770c2ffc8f · 2018-05-10T11:27:03.000+01:00
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -63,21 +63,16 @@ set_target_properties(
     goto-instrument-lib
     goto-programs
     goto-symex
-    java_bytecode
-    jbmc
-    jbmc-lib
     jsil
     json
     langapi
     linking
     miniBDD
-    miniz
     mmcc
     pointer-analysis
     solvers
     test-bigint
     testing-utils
-    java-testing-utils
     unit
     util
     xml
diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt
@@ -24,21 +24,15 @@ endmacro(add_test_pl_tests)
 # running tests in parallel, it is important that these directories are
 # listed with decreasing runtimes (i.e. longest running at the top)
 add_subdirectory(cbmc)
-add_subdirectory(cbmc-java)
 add_subdirectory(goto-analyzer)
 add_subdirectory(ansi-c)
-add_subdirectory(jbmc-strings)
 add_subdirectory(goto-instrument)
 add_subdirectory(cpp)
-add_subdirectory(strings-smoke-tests)
 add_subdirectory(cbmc-cover)
 add_subdirectory(goto-instrument-typedef)
 add_subdirectory(strings)
 add_subdirectory(invariants)
-add_subdirectory(goto-diff-java)
 add_subdirectory(test-script)
-add_subdirectory(goto-analyzer-taint)
-add_subdirectory(cbmc-java-inheritance)
 if(NOT WIN32)
   add_subdirectory(goto-gcc)
 endif()
diff --git a/regression/Makefile b/regression/Makefile
@@ -2,22 +2,16 @@
 # running tests in parallel, it is important that these directories are
 # listed with decreasing runtimes (i.e. longest running at the top)
 DIRS = cbmc \
-       cbmc-java \
        goto-analyzer \
        ansi-c \
-       jbmc-strings \
        goto-instrument \
        cpp \
-       strings-smoke-tests \
        cbmc-cover \
        goto-instrument-typedef \
        smt2_solver \
        strings \
        invariants \
-       goto-diff-java \
        test-script \
-       goto-analyzer-taint \
-       cbmc-java-inheritance \
        goto-gcc \
        goto-cc-cbmc \
        cbmc-cpp \
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -96,12 +96,9 @@ add_subdirectory(pointer-analysis)
 add_subdirectory(solvers)
 add_subdirectory(util)
 add_subdirectory(xmllang)
-add_subdirectory(java_bytecode)
-add_subdirectory(miniz)
 add_subdirectory(clobber)
 
 add_subdirectory(cbmc)
-add_subdirectory(jbmc)
 add_subdirectory(goto-cc)
 add_subdirectory(goto-instrument)
 add_subdirectory(goto-analyzer)
diff --git a/src/Makefile b/src/Makefile
@@ -1,10 +1,10 @@
-DIRS = ansi-c big-int cbmc jbmc cpp goto-cc goto-instrument goto-programs \
+DIRS = ansi-c big-int cbmc cpp goto-cc goto-instrument goto-programs \
        goto-symex langapi pointer-analysis solvers util linking xmllang \
-       assembler analyses java_bytecode \
+       assembler analyses \
        json goto-analyzer jsil goto-diff clobber \
-       memory-models miniz
+       memory-models
 
-all: cbmc.dir jbmc.dir goto-cc.dir goto-instrument.dir \
+all: cbmc.dir goto-cc.dir goto-instrument.dir \
      goto-analyzer.dir goto-diff.dir
 
 ###############################################################################
@@ -19,10 +19,8 @@ $(patsubst %, %.dir, $(filter-out big-int util, $(DIRS))): util.dir
 
 cpp.dir: ansi-c.dir linking.dir
 
-java_bytecode.dir: miniz.dir
-
 languages: util.dir langapi.dir \
-           cpp.dir ansi-c.dir xmllang.dir assembler.dir java_bytecode.dir \
+           cpp.dir ansi-c.dir xmllang.dir assembler.dir \
            jsil.dir
 
 solvers.dir: util.dir langapi.dir
@@ -35,8 +33,6 @@ cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \
           pointer-analysis.dir goto-programs.dir linking.dir \
           goto-instrument.dir
 
-jbmc.dir: java_bytecode.dir cbmc.dir
-
 goto-analyzer.dir: languages analyses.dir goto-programs.dir linking.dir \
                    json.dir goto-instrument.dir
 
@@ -88,14 +84,6 @@ glucose-download:
 	@(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch)
 	@rm glucose-syrup.tgz
 
-cprover-jar-build:
-	@echo "Building org.cprover.jar"
-	@(cd java_bytecode/library/; \
-	mkdir -p target; \
-	javac -d target/ `find src/ -name "*.java"`; \
-	cd target; jar cf org.cprover.jar `find . -name "*.class"`; \
-	mv org.cprover.jar ../../../)
-
 ipasir-download:
 	# get the 2016 version of the ipasir package, which contains a few solvers
 	@echo "Download ipasir 2016 package"
diff --git a/src/clobber/Makefile b/src/clobber/Makefile
@@ -17,8 +17,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
        ../goto-symex/rewrite_union$(OBJEXT) \
        ../pointer-analysis/dereference$(OBJEXT) \
        ../goto-instrument/dump_c$(OBJEXT) \
-       ../goto-instrument/goto_program2code$(OBJEXT) \
-       ../miniz/miniz$(OBJEXT)
+       ../goto-instrument/goto_program2code$(OBJEXT)
 
 INCLUDES= -I ..
 
diff --git a/src/goto-analyzer/CMakeLists.txt b/src/goto-analyzer/CMakeLists.txt
@@ -21,7 +21,6 @@ target_link_libraries(goto-analyzer-lib
     util
 )
 
-add_if_library(goto-analyzer-lib java_bytecode)
 add_if_library(goto-analyzer-lib jsil)
 
 # Executable
diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile
@@ -10,7 +10,6 @@ SRC = goto_analyzer_main.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/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -18,7 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <ansi-c/ansi_c_language.h>
 #include <cpp/cpp_language.h>
-#include <java_bytecode/java_bytecode_language.h>
 #include <jsil/jsil_language.h>
 
 #include <goto-programs/initialize_goto_model.h>
@@ -43,9 +42,6 @@ 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>
 
@@ -76,7 +72,6 @@ void goto_analyzer_parse_optionst::register_languages()
 {
   register_language(new_ansi_c_language);
   register_language(new_cpp_language);
-  register_language(new_java_bytecode_language);
   register_language(new_jsil_language);
 }
 
@@ -751,11 +746,6 @@ bool goto_analyzer_parse_optionst::process_goto_program(
       get_message_handler(), goto_model, cmdline.isset("pointer-check"));
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(goto_model);
-    // remove Java throw and catch
-    // This introduces instanceof, so order is important:
-    remove_exceptions(goto_model);
-    // remove rtti
-    remove_instanceof(goto_model);
 
     // do partial inlining
     status() << "Partial Inlining" << eom;
diff --git a/src/goto-cc/CMakeLists.txt b/src/goto-cc/CMakeLists.txt
@@ -17,6 +17,7 @@ target_link_libraries(goto-cc-lib
     xml
     assembler
     langapi
+    json
 )
 
 add_if_library(goto-cc-lib jsil)
diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile
@@ -27,7 +27,6 @@ OBJ += ../big-int/big-int$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
-      ../miniz/miniz$(OBJEXT) \
       ../json/json$(LIBEXT)
 
 INCLUDES= -I ..
diff --git a/src/goto-diff/CMakeLists.txt b/src/goto-diff/CMakeLists.txt
@@ -23,7 +23,6 @@ target_link_libraries(goto-diff-lib
     solvers
 )
 
-add_if_library(goto-diff-lib java_bytecode)
 add_if_library(goto-diff-lib jsil)
 
 # Executable
diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile
@@ -9,7 +9,6 @@ SRC = change_impact.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) \
@@ -32,7 +31,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../util/util$(LIBEXT) \
       ../solvers/solvers$(LIBEXT) \
-      ../miniz/miniz$(OBJEXT) \
       ../json/json$(LIBEXT)
 
 INCLUDES= -I ..
diff --git a/src/goto-diff/goto_diff_languages.cpp b/src/goto-diff/goto_diff_languages.cpp
@@ -16,11 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <ansi-c/ansi_c_language.h>
 #include <cpp/cpp_language.h>
 
-#include <java_bytecode/java_bytecode_language.h>
 
 void goto_diff_languagest::register_languages()
 {
   register_language(new_ansi_c_language);
   register_language(new_cpp_language);
-  register_language(new_java_bytecode_language);
 }
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
@@ -51,10 +51,6 @@ 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>
 
 #include <cbmc/version.h>
@@ -422,10 +418,6 @@ bool goto_diff_parse_optionst::process_goto_program(
 
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(goto_model);
-    // remove catch and throw
-    remove_exceptions(goto_model);
-    // Java instanceof -> clsid comparison:
-    remove_instanceof(goto_model);
 
     mm_io(goto_model);
 
@@ -532,8 +524,7 @@ void goto_diff_parse_optionst::help()
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK
     " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
-    "Java Bytecode frontend options:\n"
-    JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
+    "\n"
     "Other options:\n"
     " --version                    show version and exit\n"
     " --json-ui                    use JSON-formatted output\n"
diff --git a/src/goto-instrument/CMakeLists.txt b/src/goto-instrument/CMakeLists.txt
@@ -27,7 +27,6 @@ target_link_libraries(goto-instrument-lib
     solvers
 )
 
-add_if_library(goto-instrument-lib java_bytecode)
 add_if_library(goto-instrument-lib glpk)
 
 # Executable
diff --git a/src/goto-programs/CMakeLists.txt b/src/goto-programs/CMakeLists.txt
@@ -4,4 +4,4 @@ add_library(goto-programs ${sources})
 generic_includes(goto-programs)
 
 target_link_libraries(
-        goto-programs util assembler langapi analyses ansi-c java_bytecode)
+        goto-programs util assembler langapi analyses ansi-c)
diff --git a/src/jbmc/CMakeLists.txt b/src/jbmc/CMakeLists.txt
@@ -17,7 +17,6 @@ target_link_libraries(jbmc-lib
     goto-instrument-lib
     goto-programs
     goto-symex
-    java_bytecode
     json
     langapi
     linking
diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt
@@ -1,10 +1,7 @@
 file(GLOB_RECURSE sources "*.cpp" "*.h")
 
 file(GLOB_RECURSE testing_utils "testing-utils/*.cpp" "testing-utils/*.h")
-
-file(GLOB_RECURSE java_testing_utils
-    "java_bytecode/testing-utils/*.cpp"
-    "java_bytecode/testing-utils/*.h")
+file(GLOB_RECURSE java_tests "java_bytecode/*.cpp" "java_bytecode/*.h")
 
 list(REMOVE_ITEM sources
     # Used in executables
@@ -25,14 +22,29 @@ list(REMOVE_ITEM sources
 
     # Will be built into a separate library and linked
     ${testing_utils}
-    ${java_testing_utils}
+
+    # Java front-end is being remove, so drop all java tests
+    ${java_tests}
+
+    ${goto_program_generics}
+    ${CMAKE_CURRENT_SOURCE_DIR}/analyses/dependence_graph.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/goto-programs/class_hierarchy_output.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/goto-programs/class_hierarchy_graph.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/goto-programs/remove_virtual_functions_without_fallback.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/pointer-analysis/custom_value_set_analysis.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/solvers/refinement/string_refinement/dependency_graph.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/solvers/refinement/string_refinement/string_symbol_resolution.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/util/has_subtype.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/util/parameter_indices.cpp
+    ${CMAKE_CURRENT_SOURCE_DIR}/util/simplify_expr.cpp
+
 
     # Intended to fail to compile
     ${CMAKE_CURRENT_SOURCE_DIR}/util/expr_cast/expr_undefined_casts.cpp
 )
 
 add_subdirectory(testing-utils)
-add_subdirectory(java_bytecode/testing-utils)
 
 add_executable(unit ${sources})
 target_include_directories(unit
@@ -44,10 +56,8 @@ target_include_directories(unit
 target_link_libraries(
         unit
         testing-utils
-        java-testing-utils
         ansi-c
         solvers
-        java_bytecode
         goto-programs
         goto-instrument-lib
         cbmc-lib
diff --git a/unit/Makefile b/unit/Makefile
diff --git a/unit/testing-utils/CMakeLists.txt b/unit/testing-utils/CMakeLists.txt

Original file line number	Diff line number	Diff line change
`@@ -21,7 +21,6 @@ target_link_libraries(goto-analyzer-lib`
`21`	`21`	`util`
`22`	`22`	`)`
`23`	`23`
`24`		`-add_if_library(goto-analyzer-lib java_bytecode)`
`25`	`24`	`add_if_library(goto-analyzer-lib jsil)`
`26`	`25`
`27`	`26`	`# Executable`
Original file line number	Diff line number	Diff line change
`@@ -17,6 +17,7 @@ target_link_libraries(goto-cc-lib`
`17`	`17`	`xml`
`18`	`18`	`assembler`
`19`	`19`	`langapi`
	`20`	`+ json`
`20`	`21`	`)`
`21`	`22`
`22`	`23`	`add_if_library(goto-cc-lib jsil)`