remove usage of Java bytecode frontend

Author: Daniel Kroening

CMakeLists.txt

@@ -63,15 +63,11 @@ 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

regression/CMakeLists.txt

@@ -24,21 +24,16 @@ 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)
 add_subdirectory(test-script)
-add_subdirectory(goto-analyzer-taint)
-add_subdirectory(cbmc-java-inheritance)
 if(NOT WIN32)
   add_subdirectory(goto-gcc)
 endif()

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 \
        test-script \
-       goto-analyzer-taint \
-       cbmc-java-inheritance \
        goto-gcc \
        goto-cc-cbmc \
        cbmc-cpp \

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)

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"

src/clobber/CMakeLists.txt

@@ -25,9 +25,6 @@ target_link_libraries(clobber-lib
 )
 
 add_if_library(clobber-lib bv_refinement)
-add_if_library(clobber-lib java_bytecode)
-add_if_library(clobber-lib specc)
-add_if_library(clobber-lib php)
 
 # Executable
 add_executable(clobber clobber_main.cpp)

src/clobber/Makefile

@@ -3,7 +3,6 @@ SRC = clobber_main.cpp \
       # Empty last line
 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) \
@@ -17,8 +16,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 ..
 
@@ -31,16 +29,6 @@ CLEANFILES = clobber$(EXEEXT)
 
 all: clobber$(EXEEXT)
 
-ifneq ($(wildcard ../specc/Makefile),)
-  OBJ += ../specc/specc$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_SPECC
-endif
-
-ifneq ($(wildcard ../php/Makefile),)
-  OBJ += ../php/php$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_PHP
-endif
-
 ###############################################################################
 
 clobber$(EXEEXT): $(OBJ)

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) \

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;

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 ..

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 ..

src/goto-diff/goto_diff_languages.cpp

@@ -20,8 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <specc/specc_language.h>
 #endif
 
-#include <java_bytecode/java_bytecode_language.h>
-
 void goto_diff_languagest::register_languages()
 {
   register_language(new_ansi_c_language);
@@ -30,6 +28,4 @@ void goto_diff_languagest::register_languages()
   #ifdef HAVE_SPECC
   register_language(new_specc_language);
   #endif
-
-  register_language(new_java_bytecode_language);
 }

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"

unit/CMakeLists.txt

@@ -40,7 +40,6 @@ target_link_libraries(
         testing-utils
         ansi-c
         solvers
-        java_bytecode
         goto-programs
         goto-instrument-lib
 )

unit/Makefile

@@ -13,47 +13,26 @@ SRC += unit_tests.cpp \
        analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
        goto-programs/goto_trace_output.cpp \
-       goto-programs/class_hierarchy_output.cpp \
-       goto-programs/class_hierarchy_graph.cpp \
-       goto-programs/remove_virtual_functions_without_fallback.cpp \
-       java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \
-       java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp \
-       java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \
-       java_bytecode/java_object_factory/gen_nondet_string_init.cpp \
-       java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \
-       java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \
        miniBDD_new.cpp \
-       java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \
-       java_bytecode/java_utils_test.cpp \
-       java_bytecode/inherited_static_fields/inherited_static_fields.cpp \
-       pointer-analysis/custom_value_set_analysis.cpp \
        sharing_node.cpp \
        solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \
        solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \
        solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \
-       solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \
        solvers/refinement/string_refinement/concretize_array.cpp \
-       solvers/refinement/string_refinement/dependency_graph.cpp \
        solvers/refinement/string_refinement/substitute_array_list.cpp \
-       solvers/refinement/string_refinement/string_symbol_resolution.cpp \
        solvers/refinement/string_refinement/sparse_array.cpp \
        solvers/refinement/string_refinement/union_find_replace.cpp \
        util/expr_cast/expr_cast.cpp \
        util/expr_iterator.cpp \
-       util/has_subtype.cpp \
        util/irep.cpp \
        util/irep_sharing.cpp \
        util/message.cpp \
        util/optional.cpp \
-       util/parameter_indices.cpp \
-       util/simplify_expr.cpp \
        util/small_shared_two_way_ptr.cpp \
        util/string_utils/split_string.cpp \
        util/string_utils/strip_string.cpp \
        util/symbol_table.cpp \
        catch_example.cpp \
-       java_bytecode/java_virtual_functions/virtual_functions.cpp \
-       java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp \
        # Empty last line
 
 INCLUDES= -I ../src/ -I.
@@ -67,8 +46,7 @@ cprover.dir:
 testing-utils.dir:
 	$(MAKE) $(MAKEARGS) -C testing-utils
 
-CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
-              ../src/miniz/miniz$(OBJEXT) \
+CPROVER_LIBS =../src/miniz/miniz$(OBJEXT) \
               ../src/ansi-c/ansi-c$(LIBEXT) \
               ../src/cpp/cpp$(LIBEXT) \
               ../src/json/json$(LIBEXT) \

unit/testing-utils/Makefile

@@ -1,7 +1,6 @@
 SRC = \
   c_to_expr.cpp \
   free_form_cmdline.cpp \
-  load_java_class.cpp \
   require_expr.cpp \
   require_goto_statements.cpp \
   require_parse_tree.cpp \