Merge pull request #2118 from diffblue/remove-jbmc

remove usage of Java bytecode frontend

Author: peterschrammel

.travis.yml

@@ -237,7 +237,7 @@ jobs:
             description: "Travis build of ${TRAVIS_COMMIT}"
           notification_email: "coverity-scan@diffblue.com"
           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:
         - |
@@ -266,12 +266,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

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

appveyor.yml

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

jbmc/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/README.md

@@ -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/CMakeLists.txt

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

jbmc/regression/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 \

jbmc/regression/janalyzer-taint/CMakeLists.txt

@@ -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/goto-analyzer-taint-ansi-c/Makefile renamed to jbmc/regression/janalyzer-taint/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/goto-analyzer-taint/taint-aliasing1/aliasing1.class renamed to jbmc/regression/janalyzer-taint/taint-aliasing1/aliasing1.class

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