remove usage of Java bytecode frontend

.travis.yml

@@ -248,7 +248,7 @@ jobs:
             description: "Travis build of ${TRAVIS_COMMIT}"
           notification_email: "[email protected]"
           build_command_prepend: "make -C src minisat2-download"
-          build_command: "make -C src -j2"
+          build_command: "make -C src -j2; make -C jbmc/src -j2"
           branch_pattern: "develop"
       before_install:
         - |
@@ -277,12 +277,16 @@ install:
   - make -C src/ansi-c library_check
   - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
   - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3 clobber.dir memory-models.dir
+  - make -C jbmc/src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
 
 script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
   - env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
   - make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
   - make -C unit test
+  - env UBSAN_OPTIONS=print_stacktrace=1 make -C jbmc/regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
+  - make -C jbmc/unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
+  - make -C jbmc/unit test
 
 before_cache:
   - ccache -s

CMakeLists.txt

@@ -35,6 +35,7 @@ set(sat_impl "minisat2" CACHE STRING
 )
 
 add_subdirectory(src)
+add_subdirectory(jbmc)
 
 if(${enable_cbmc_tests})
     enable_testing()
@@ -63,15 +64,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
@@ -81,6 +78,17 @@ set_target_properties(
     util
     xml
 
+    java_bytecode
+    jbmc
+    jbmc-lib
+    janalyzer
+    janalyzer-lib
+    jdiff
+    jdiff-lib
+    java-testing-utils
+    java-unit
+    miniz
+
     PROPERTIES
     CXX_STANDARD 11
     CXX_STANDARD_REQUIRED true

COMPILING.md

@@ -28,6 +28,17 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
    yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6 java-1.7.0-openjdk-devel
    ```
    Note that you need g++ version 4.9 or newer.
+
+   To compile JBMC, you additionally need the JDK:
+   On Debian-like distributions, do
+   ```
+   apt-get install openjdk-7-jdk
+   ```
+   On Red Hat/Fedora or derivates, do
+   ```
+   yum install java-1.7.0-openjdk-devel
+   ```
+
 2. As a user, get the CBMC source via
    ```
    git clone https://github.com/diffblue/cbmc cbmc-git
@@ -93,7 +104,11 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
    ```
    pkg install bash gmake git www/p5-libwww patch flex bison openjdk
    ```
-2. As a user, get the CBMC source via
+   To compile JBMC, additionally install
+   ```
+   pkg install openjdk
+   ```
+ 2. As a user, get the CBMC source via
    ```
    git clone https://github.com/diffblue/cbmc cbmc-git
    ```
@@ -183,14 +198,14 @@ require manual modification of build files.
 1. Ensure you have all the build dependencies installed. Build dependencies are
    the same as for the makefile build, but with the addition of CMake version
    3.2 or higher. The installed CMake version can be queried with `cmake
-   --version`. To install all build dependencies:
+   --version`. To install cmake:
    - On Debian-like distributions, do
      ```
-     apt-get install cmake g++ gcc flex bison make git libwww-perl patch openjdk-7-jdk
+     apt-get install cmake
      ```
    - On Red Hat/Fedora or derivates, do
      ```
-     yum install cmake gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6 java-1.7.0-openjdk-devel
+     yum install cmake
      ```
    - On macOS, do
      ```

appveyor.yml

@@ -53,11 +53,11 @@ build_script:
     call "C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\vcvarsall.bat" x64
     sed -i "s/BUILD_ENV[ ]*=.*/BUILD_ENV = MSVC/" src/config.inc
     make -C src -j2
+    make -C jbmc/src -j2
 
 test_script:
 - cmd: |
     cd regression
-
     rem HACK disable failing tests
     rmdir /s /q ansi-c\arch_flags_mcpu_bad
     rmdir /s /q ansi-c\arch_flags_mcpu_good
@@ -90,15 +90,24 @@ test_script:
     rmdir /s /q cpp\nullptr1
     rmdir /s /q cpp\sizeof1
     rmdir /s /q cpp\static_assert1
-    rmdir /s /q cbmc-java\VarLengthArrayTrace1
-    rmdir /s /q cbmc-java\classpath1
-    rmdir /s /q cbmc-java\jar-file3
-    rmdir /s /q cbmc-java\tableswitch2
     rmdir /s /q goto-gcc
     rmdir /s /q goto-instrument\slice08
+    cd ..
 
-    make test
+    make -C regression test
 
-    cd ..
-    make -C unit all
+    make -C unit all -j2
     make -C unit test
+
+    cd jbmc/regression
+    rmdir /s /q jbmc\VarLengthArrayTrace1
+    rmdir /s /q jbmc\classpath1
+    rmdir /s /q jbmc\jar-file3
+    rmdir /s /q jbmc\tableswitch2
+    rmdir /s /q jbmc-concurrency\explicit_thread_blocks
+    cd ../..
+
+    make -C jbmc/regression test
+
+    make -C jbmc/unit all -j2
+    make -C jbmc/unit test

jbmc/CMakeLists.txt

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

jbmc/README.md

@@ -0,0 +1,52 @@
+[![Build Status][travis_img]][travis] [![Build Status][appveyor_img]][appveyor]
+
+About
+=====
+
+JBMC is a Bounded Model Checker for Java programs. It supports
+checking for runtime exceptions and user-definde assertions.
+The verification is performed by unwinding the loops in the program
+and passing the resulting equation to a decision procedure.
+
+[More info...](http://www.cprover.org/jbmc)
+
+Versions
+========
+
+Get the [latest release](https://github.com/diffblue/cbmc/releases)
+* Releases are tested and for production use.
+
+Get the current *develop* version: `git clone https://github.com/diffblue/cbmc.git`
+* Develop versions are not recommended for production use.
+
+Prerequisites
+============
+
+JBMC compiles CBMC as part of its build process and as such has all the pre-requisites of CBMC. These can be viewed at: [diffblue/cbmc:COMPILING](http://github.com/diffblue/cbmc/blob/master/COMPILING)
+
+Compilation
+===========
+
+To compile you need to run the command:
+
+```bash
+make -C jbmc/src
+```
+Output
+======
+
+Compiling produces an executable called `jbmc` which by default can be found in `jbmc/src/jbmc/jbmc`
+
+Reporting bugs and contributing to the code base
+================================================
+
+See [CBMC](https://github.com/diffblue/cbmc/blob/develop/README.md))
+
+License
+=======
+4-clause BSD license, see `LICENSE` file.
+
+[travis]: https://travis-ci.org/diffblue/cbmc
+[travis_img]: https://travis-ci.org/diffblue/cbmc.svg?branch=develop
+[appveyor]: https://ci.appveyor.com/project/diffblue/cbmc/
+[appveyor_img]: https://ci.appveyor.com/api/projects/status/github/diffblue/cbmc?svg=true&branch=develop

jbmc/regression/CMakeLists.txt

@@ -0,0 +1,33 @@
+set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
+
+macro(add_test_pl_profile name cmdline flag profile)
+    add_test(
+        NAME "${name}-${profile}"
+        COMMAND ${test_pl_path} -p -c ${cmdline} ${flag} ${ARGN}
+        WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
+    )
+    set_tests_properties("${name}-${profile}" PROPERTIES
+        LABELS "${profile};CBMC"
+    )
+endmacro(add_test_pl_profile)
+
+macro(add_test_pl_tests cmdline)
+    get_filename_component(TEST_DIR_NAME ${CMAKE_CURRENT_SOURCE_DIR} NAME)
+    message(STATUS "Adding tests in directory: ${TEST_DIR_NAME}")
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -C CORE ${ARGN})
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -T THOROUGH ${ARGN})
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -F FUTURE ${ARGN})
+    add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG ${ARGN})
+endmacro(add_test_pl_tests)
+
+# For the best possible utilisation of multiple cores when
+# running tests in parallel, it is important that these directories are
+# listed with decreasing runtimes (i.e. longest running at the top)
+add_subdirectory(jbmc)
+add_subdirectory(strings-smoke-tests)
+add_subdirectory(jbmc-strings)
+add_subdirectory(jdiff)
+add_subdirectory(janalyzer-taint)
+add_subdirectory(jbmc-concurrency)
+add_subdirectory(jbmc-inheritance)
+add_subdirectory(jbmc-cover)

jbmc/regression/Makefile

@@ -0,0 +1,53 @@
+# For the best possible utilisation of multiple cores when
+# running tests in parallel, it is important that these directories are
+# listed with decreasing runtimes (i.e. longest running at the top)
+DIRS = janalzyer-taint \
+       jbmc \
+       jbmc-concurrency \
+       jbmc-cover \
+       jbmc-inheritance \
+       jbmc-strings \
+       jdiff \
+       string-smoke-tests \
+       # Empty last line
+
+# Tests under goto-gcc cannot be run on Windows, so appveyor.yml unlinks
+# the entire directory under Windows. This variable will contain the list
+# of directories that actually exist on the current platform.
+PLATFORM_DIRS = $(wildcard $(DIRS))
+
+# Run all test directories in sequence
+.PHONY: test
+test:
+	@for dir in $(PLATFORM_DIRS); do \
+		$(MAKE) "$$dir" || exit 1; \
+	done;
+
+# Pattern to execute a single test suite directory
+.PHONY: $(PLATFORM_DIRS)
+$(PLATFORM_DIRS):
+	@echo "Running $@..." ;
+	$(MAKE) -C "$@" test || exit 1;
+
+# Run all test directories using GNU Parallel
+.PHONY: test-parallel
+.NOTPARALLEL: test-parallel
+test-parallel:
+	@echo "Building with $(JOBS) jobs"
+	parallel \
+		--halt soon,fail=1 \
+		--tag \
+		--tagstring '{#}:' \
+		--linebuffer \
+		--jobs $(JOBS) \
+		$(MAKE) "{}" \
+		::: $(PLATFORM_DIRS)
+
+
+.PHONY: clean
+clean:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			$(MAKE) -C "$$dir" clean; \
+		fi; \
+	done;

jbmc/regression/janalyzer-taint/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:goto-analyzer>"
+)

regression/goto-analyzer-taint-ansi-c/Makefile → jbmc/regression/janalyzer-taint/Makefile

@@ -1,10 +1,12 @@
 default: tests.log
 
+include ../../src/config.inc
+
 test:
-	@../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/janalyzer/janalyzer
 
-tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer
+tests.log: ../$(CPROVER_DIR)/regression/test.pl
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/janalyzer/janalyzer
 
 show:
 	@for dir in *; do \

regression/cbmc-java-concurrency/Makefile → jbmc/regression/jbmc-concurrency/Makefile

@@ -1,10 +1,12 @@
 default: tests.log
 
+include ../../src/config.inc
+
 test:
-	@../test.pl -p -c ../../../src/jbmc/jbmc
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
 
-tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/jbmc/jbmc
+tests.log: ../$(CPROVER_DIR)/regression/test.pl
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
 
 show:
 	@for dir in *; do \

regression/cbmc-java-inheritance/Makefile → jbmc/regression/jbmc-cover/Makefile

@@ -1,10 +1,12 @@
 default: tests.log
 
+include ../../src/config.inc
+
 test:
-	@../test.pl -p -c ../../../src/jbmc/jbmc
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
 
-tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/jbmc/jbmc
+tests.log: ../$(CPROVER_DIR)/regression/test.pl
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
 
 show:
 	@for dir in *; do \

regression/cbmc-java/Makefile → jbmc/regression/jbmc-inheritance/Makefile

@@ -1,12 +1,12 @@
 default: tests.log
 
+include ../../src/config.inc
+
 test:
-	@../test.pl -p -c ../../../src/jbmc/jbmc
-	@../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
 
-tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/jbmc/jbmc
-	@../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
+tests.log: ../$(CPROVER_DIR)/regression/test.pl
+	@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
 
 show:
 	@for dir in *; do \