Move java_bytecode, jbmc and miniz to jbmc/src

Author: peterschrammel

CMakeLists.txt

@@ -35,6 +35,7 @@ set(sat_impl "minisat2" CACHE STRING
 )
 
 add_subdirectory(src)
+add_subdirectory(jbmc)
 
 if(${enable_cbmc_tests})
     enable_testing()
@@ -81,6 +82,13 @@ set_target_properties(
     util
     xml
 
+    java_bytecode
+    jbmc
+    jbmc-lib
+    java-testing-utils
+    java-unit
+    miniz
+
     PROPERTIES
     CXX_STANDARD 11
     CXX_STANDARD_REQUIRED true

jbmc/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_subdirectory(regression)
+add_subdirectory(src)
+add_subdirectory(unit)

jbmc/src/CMakeLists.txt

@@ -0,0 +1,18 @@
+project(JBMC)
+
+#   Set the public include locations for a target.
+macro(generic_includes name)
+    target_include_directories(${name}
+        PUBLIC
+        ${JBMC_BINARY_DIR}
+        ${JBMC_SOURCE_DIR}
+        ${CBMC_BINARY_DIR}
+        ${CBMC_SOURCE_DIR}
+        ${CMAKE_CURRENT_BINARY_DIR}
+        ${CMAKE_CURRENT_SOURCE_DIR}
+    )
+endmacro(generic_includes)
+
+add_subdirectory(miniz)
+add_subdirectory(java_bytecode)
+add_subdirectory(jbmc)

jbmc/src/Makefile

@@ -0,0 +1,44 @@
+DIRS = jbmc java_bytecode miniz
+
+include config.inc
+
+.PHONY: all
+all: jbmc.dir
+
+# building cbmc proper
+.PHONY: cprover.dir
+cprover.dir:
+	$(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/src
+
+.PHONY: java_bytecode.dir
+java_bytecode.dir: miniz.dir
+
+.PHONY: jbmc.dir
+jbmc.dir: java_bytecode.dir cprover.dir
+
+.PHONY: miniz.dir
+miniz.dir:
+
+$(patsubst %, %.dir, $(DIRS)):
+	## Entering $(basename $@)
+	$(MAKE) $(MAKEARGS) -C $(basename $@)
+
+# generate source files
+
+$(patsubst %, %_generated_files, $(DIRS)):
+	$(MAKE) $(MAKEARGS) -C $(patsubst %_generated_files, %, $@) generated_files
+
+.PHONY: generated_files
+generated_files: $(patsubst %, %_generated_files, $(DIRS))
+
+# cleaning
+
+.PHONY: clean
+clean: $(patsubst %, %_clean, $(DIRS)) cprover_clean
+
+$(patsubst %, %_clean, $(DIRS)):
+	$(MAKE) $(MAKEARGS) -C $(patsubst %_clean, %, $@) clean ; \
+
+.PHONY: cprover_clean
+cprover_clean:
+	$(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/src clean

jbmc/src/config.inc

@@ -0,0 +1 @@
+CPROVER_DIR ?= ../..

src/java_bytecode/CMakeLists.txt renamed to jbmc/src/java_bytecode/CMakeLists.txt

@@ -41,10 +41,11 @@ SRC = bytecode_info.cpp \
       simple_method_stubbing.cpp \
       # Empty last line
 
-INCLUDES= -I ..
+INCLUDES= -I .. -I ../$(CPROVER_DIR)/src
 
 include ../config.inc
-include ../common
+include ../$(CPROVER_DIR)/src/config.inc
+include ../$(CPROVER_DIR)/src/common
 
 CLEANFILES = java_bytecode$(LIBEXT)
 

src/java_bytecode/Makefile renamed to jbmc/src/java_bytecode/Makefile

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "bytecode_info.h"
 
+// clang-format off
 struct bytecode_infot const bytecode_info[]=
 {
 { "aaload",         0x32, ' ', 2, 1, ' ' }, // arrayref, index → value; load onto the stack a reference from an array  NOLINT(*)
@@ -221,3 +222,4 @@ struct bytecode_infot const bytecode_info[]=
 { "wide",           0xc4, ' ', 0, 0, ' ' }, // modifier for others  NOLINT(*)
 { nullptr,          0x00, '\0',0, 0, '\0'}, // zero-initialized NOLINT (*)
 };
+// clang-format on

src/java_bytecode/README.md renamed to jbmc/src/java_bytecode/README.md

@@ -34,7 +34,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_string_literals.h"
 #include "java_static_initializers.h"
 #include "java_utils.h"
-#include <java_bytecode/ci_lazy_methods.h>
+#include "ci_lazy_methods.h"
 
 #include "expr2java.h"
 
@@ -124,7 +124,10 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
       // add jars from JSON config file to classpath
       for(const jsont &file_entry : include_files.array)
       {
-        assert(file_entry.is_string() && has_suffix(file_entry.value, ".jar"));
+        DATA_INVARIANT(
+          file_entry.is_string() && has_suffix(file_entry.value, ".jar"),
+          "classpath entry must be jar filename, but '" + file_entry.value +
+          "' found");
         config.java.classpath.push_back(file_entry.value);
       }
     }

src/java_bytecode/bytecode_info.cpp renamed to jbmc/src/java_bytecode/bytecode_info.cpp

@@ -5,7 +5,8 @@
 SRC = converter.cpp
 
 include ../../config.inc
-include ../../common
+include ../../$(CPROVER_DIR)/src/config.inc
+include ../../$(CPROVER_DIR)/src/common
 
 SOURCE_DIR := src
 BINARY_DIR := classes

src/java_bytecode/bytecode_info.h renamed to jbmc/src/java_bytecode/bytecode_info.h

@@ -10,26 +10,22 @@ generic_includes(jbmc-lib)
 target_link_libraries(jbmc-lib
     analyses
     ansi-c
-    assembler
     big-int
     cbmc-lib
-    cpp
     goto-instrument-lib
     goto-programs
     goto-symex
     java_bytecode
     json
     langapi
     linking
+    miniz
     pointer-analysis
     solvers
     util
     xml
 )
 
-add_if_library(jbmc-lib bv_refinement)
-add_if_library(jbmc-lib jsil)
-
 # Executable
 add_executable(jbmc jbmc_main.cpp)
 target_link_libraries(jbmc jbmc-lib)

src/java_bytecode/character_refine_preprocess.cpp renamed to jbmc/src/java_bytecode/character_refine_preprocess.cpp

@@ -0,0 +1,74 @@
+SRC = jbmc_main.cpp \
+      jbmc_parse_options.cpp \
+      # Empty last line
+
+OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
+      ../java_bytecode/java_bytecode$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/linking/linking$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/goto-programs/goto-programs$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/goto-symex/goto-symex$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/pointer-analysis/value_set$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/pointer-analysis/value_set_analysis_fi$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/pointer-analysis/value_set_domain_fi$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/pointer-analysis/value_set_fi$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/pointer-analysis/value_set_dereference$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/pointer-analysis/dereference_callback$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/pointer-analysis/add_failed_symbols$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/pointer-analysis/rewrite_index$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/pointer-analysis/goto_program_dereference$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-instrument/full_slicer$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-instrument/reachability_slicer$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-instrument/nondet_static$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-instrument/cover$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-instrument/cover_basic_blocks$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-instrument/cover_filter$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_branch$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_condition$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_decision$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_location$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_mcdc$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_other$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-instrument/cover_util$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/goto-instrument/unwindset$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/xmllang/xmllang$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/solvers/solvers$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/util/util$(LIBEXT) \
+      ../miniz/miniz$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/json/json$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/cbmc/bmc_cover$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/cbmc/bv_cbmc$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/cbmc/cbmc_dimacs$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/cbmc/cbmc_solvers$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/cbmc/counterexample_beautification$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/cbmc/fault_localization$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/cbmc/show_vcc$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/cbmc/symex_bmc$(OBJEXT) \
+      ../$(CPROVER_DIR)/src/cbmc/symex_coverage$(OBJEXT) \
+      # Empty last line
+
+INCLUDES= -I .. -I ../$(CPROVER_DIR)/src
+
+LIBS =
+
+include ../config.inc
+include ../$(CPROVER_DIR)/src/config.inc
+include ../$(CPROVER_DIR)/src/common
+
+CLEANFILES = jbmc$(EXEEXT)
+
+all: jbmc$(EXEEXT)
+
+###############################################################################
+
+jbmc$(EXEEXT): $(OBJ)
+	$(LINKBIN)
+
+.PHONY: jbmc-mac-signed
+
+jbmc-mac-signed: jbmc$(EXEEXT)
+	strip jbmc$(EXEEXT) ; codesign -v -s $(OSX_IDENTITY) jbmc$(EXEEXT)

src/java_bytecode/character_refine_preprocess.h renamed to jbmc/src/java_bytecode/character_refine_preprocess.h

@@ -1,9 +1,11 @@
 SRC = miniz.cpp \
       # Empty last line
+
 INCLUDES= -I ..
 
 include ../config.inc
-include ../common
+include ../$(CPROVER_DIR)/src/config.inc
+include ../$(CPROVER_DIR)/src/common
 
 CLEANFILES = miniz$(OBJEXT)
 

src/java_bytecode/ci_lazy_methods.cpp renamed to jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -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/java_bytecode/ci_lazy_methods.h renamed to jbmc/src/java_bytecode/ci_lazy_methods.h

@@ -1,11 +1,33 @@
-DIRS = ansi-c big-int cbmc jbmc cpp goto-cc goto-instrument goto-programs \
-       goto-symex langapi pointer-analysis solvers util linking xmllang \
-       assembler analyses java_bytecode \
-       json goto-analyzer jsil goto-diff clobber \
-       memory-models miniz
-
-all: cbmc.dir jbmc.dir goto-cc.dir goto-instrument.dir \
-     goto-analyzer.dir goto-diff.dir
+DIRS = analyses \
+       ansi-c \
+       assembler \
+       big-int \
+       cbmc \
+       clobber \
+       cpp \
+       goto-analyzer \
+       goto-cc \
+       goto-diff \
+       goto-instrument \
+       goto-programs \
+       goto-symex \
+       jsil \
+       json \
+       langapi \
+       linking \
+       memory-models \
+       pointer-analysis \
+       solvers \
+       util \
+       xmllang \
+       # Empty last line
+
+all: cbmc.dir \
+     goto-analyzer.dir \
+     goto-cc.dir \
+     goto-diff.dir \
+     goto-instrument.dir \
+     # Empty last line
 
 ###############################################################################
 
@@ -19,10 +41,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 +55,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 +106,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"
@@ -121,4 +131,4 @@ cadical-download:
 doc :
 	doxygen
 
-.PHONY: ipasir-build minisat2-download glucose-download cprover-jar-build
+.PHONY: ipasir-build minisat2-download glucose-download

src/java_bytecode/ci_lazy_methods_needed.cpp renamed to jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp

@@ -17,7 +17,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
        ../pointer-analysis/dereference$(OBJEXT) \
        ../goto-instrument/dump_c$(OBJEXT) \
        ../goto-instrument/goto_program2code$(OBJEXT) \
-       ../miniz/miniz$(OBJEXT)
+       # Empty last line
 
 INCLUDES= -I ..
 

src/java_bytecode/ci_lazy_methods_needed.h renamed to jbmc/src/java_bytecode/ci_lazy_methods_needed.h

@@ -415,8 +415,6 @@ void clobber_parse_optionst::help()
     " --round-to-minus-inf         IEEE floating point rounding mode\n"
     " --round-to-zero              IEEE floating point rounding mode\n"
     "\n"
-    JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
-    "\n"
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK
     " --show-properties            show the properties\n"

src/java_bytecode/convert_java_nondet.cpp renamed to jbmc/src/java_bytecode/convert_java_nondet.cpp

@@ -21,8 +21,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 
-#include <java_bytecode/java_bytecode_language.h>
-
 class goto_functionst;
 class optionst;
 
@@ -38,7 +36,6 @@ class optionst;
   "(string-abstraction)" \
   "(show-locs)(show-vcc)(show-trace)" \
   "(property):" \
-  JAVA_BYTECODE_LANGUAGE_OPTIONS
 // clang-format on
 
 class clobber_parse_optionst: