From 1bd4f04dbe61914ff0b0a9e340a0191f6251d7ef Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Wed, 23 May 2018 11:24:14 +0100 Subject: [PATCH 1/2] JBMC: Minor fix, removing superfluous padding from converter --- jbmc/src/java_bytecode/library/converter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/library/converter.cpp b/jbmc/src/java_bytecode/library/converter.cpp index 27d083e02dc..fc1e7830436 100644 --- a/jbmc/src/java_bytecode/library/converter.cpp +++ b/jbmc/src/java_bytecode/library/converter.cpp @@ -66,7 +66,7 @@ int main(int argc, char *argv[]) printf("\n"); } - std::cout << "\n#define " << varname << "_SIZE " << size << "\n\n"; + std::cout << "\n#define " << varname << "_SIZE " << size << "\n"; src.close(); return 0; } From c6d2dba8ce4ec5ab3be193eed4f1bd82dd1461f5 Mon Sep 17 00:00:00 2001 From: Kurt Degiorgio Date: Tue, 22 May 2018 16:40:13 +0100 Subject: [PATCH 2/2] JBMC: Added java-models-library dependency This commit adds a dependency to the java-models-library (https://github.com/diffblue/java-models-library). This repository contains models for number of classes derived from the java standard library. These models are needed to support concurrency. This means that the process of building JBMC has changed slightly as one first needs to download the java-models-library. I.E: make -C jbmc/src java-models-library-download make -C jbmc/src Due possible licensing issues, the ability to automatically embed the java core models into JBMC has been removed. Instead, one must explicitly use the '--classpath' option to load the models. Consequently, the '--no-core-models' option and related code was removed as it is no longer relevant. Commit also adds a new make target, 'make dist'. This target in addition to building jbmc will create a 'dist' directory with two sub-folders, bin and lib. Executables will be copied to the former, while 'core-models.jar' will copied to the latter. Note: src/org/cprover/CProver.java has also been removed as this has been superseded by the CProver.java in the java-models-library. --- .gitignore | 9 +- .travis.yml | 3 +- COMPILING.md | 9 +- appveyor.yml | 5 + buildspec.yml | 1 + jbmc/README.md | 2 + .../jbmc-strings/java_append_char/test.desc | 2 +- jbmc/regression/jbmc/coreModels/test.desc | 2 +- jbmc/src/Makefile | 25 ++- jbmc/src/java_bytecode/CMakeLists.txt | 3 - jbmc/src/java_bytecode/Makefile | 8 +- .../java_bytecode/java_bytecode_language.cpp | 1 - .../java_bytecode/java_bytecode_language.h | 3 - jbmc/src/java_bytecode/java_class_loader.cpp | 30 --- jbmc/src/java_bytecode/java_class_loader.h | 11 +- jbmc/src/java_bytecode/library/CMakeLists.txt | 34 ++-- jbmc/src/java_bytecode/library/Makefile | 14 +- .../library/src/org/cprover/CProver.java | 172 ------------------ 18 files changed, 78 insertions(+), 256 deletions(-) delete mode 100644 jbmc/src/java_bytecode/library/src/org/cprover/CProver.java diff --git a/.gitignore b/.gitignore index 87b3c4c28c4..1627be3e149 100644 --- a/.gitignore +++ b/.gitignore @@ -49,7 +49,6 @@ src/ansi-c/gcc_builtin_headers_mips.inc src/ansi-c/gcc_builtin_headers_power.inc src/ansi-c/gcc_builtin_headers_ubsan.inc src/ansi-c/windows_builtin_headers.inc -jbmc/src/java_bytecode/java_core_models.inc # regression/test files *.out @@ -122,9 +121,13 @@ src/ansi-c/file_converter src/ansi-c/file_converter.exe src/ansi-c/library/converter src/ansi-c/library/converter.exe -jbmc/src/java_bytecode/converter -jbmc/src/java_bytecode/converter.exe +jbmc/src/java_bytecode/library/converter.exe +jbmc/src/java_bytecode/library/converter +jbmc/src/java_bytecode/library/core-models.jar +jbmc/src/java_bytecode/library/classes +jbmc/src/java_bytecode/library/src build/ +dist/ *.pyc diff --git a/.travis.yml b/.travis.yml index 71e19f029aa..8fd293fdeb2 100644 --- a/.travis.yml +++ b/.travis.yml @@ -233,6 +233,7 @@ jobs: name: "diffblue/cbmc" description: "Travis build of ${TRAVIS_COMMIT}" notification_email: "coverity-scan@diffblue.com" + build_command_prepend: "make -C jbmc/src java-models-library-download" build_command_prepend: "make -C src minisat2-download" build_command: "make -C src -j2; make -C jbmc/src -j2" branch_pattern: "develop" @@ -259,6 +260,7 @@ jobs: install: - ccache -z - ccache --max-size=1G + - make -C jbmc/src java-models-library-download - make -C src minisat2-download - make -C src/ansi-c library_check - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3 @@ -286,4 +288,3 @@ notifications: on_start: never on_cancel: never on_error: always - diff --git a/COMPILING.md b/COMPILING.md index 92ec5012536..79460e73341 100644 --- a/COMPILING.md +++ b/COMPILING.md @@ -29,8 +29,9 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution. ``` Note that you need g++ version 4.9 or newer. - To compile JBMC, you additionally need the JDK: - On Debian-like distributions, do + To compile JBMC, you additionally need the JDK and the java-models-library. + + For the JDK, on Debian-like distributions, do ``` apt-get install openjdk-7-jdk ``` @@ -38,6 +39,10 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution. ``` yum install java-1.7.0-openjdk-devel ``` + For the models library, do + ``` + make -C jbmc/src java-models-library-download + ``` 2. As a user, get the CBMC source via ``` diff --git a/appveyor.yml b/appveyor.yml index 64b0b0a7119..1574fb57f0a 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -42,12 +42,17 @@ install: & 7z x minisat2_2.2.1.orig.tar.gz &7z x minisat2_2.2.1.orig.tar } + if (!(Test-Path jml)) { + & appveyor downloadfile https://github.com/diffblue/java-models-library/archive/master.zip -FileName jml.zip + & 7z x jml.zip + } cd .. cache: deps build_script: - cmd: | + cp -r deps/java-models-library-master/src jbmc/src/java_bytecode/library cp -r deps/minisat2-2.2.1 minisat-2.2.1 patch -d minisat-2.2.1 -p1 < scripts/minisat-2.2.1-patch call "C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\vcvarsall.bat" x64 diff --git a/buildspec.yml b/buildspec.yml index e027e933048..2860371953f 100644 --- a/buildspec.yml +++ b/buildspec.yml @@ -13,6 +13,7 @@ phases: build: commands: - echo Build started on `date` + - make -C jbmc/src java-models-library-download - (cd src ; make minisat2-download) - (cd src ; make CXX="ccache g++" -j2) - (cd regression ; make test) diff --git a/jbmc/README.md b/jbmc/README.md index b4605b7dcaf..db3d8182657 100644 --- a/jbmc/README.md +++ b/jbmc/README.md @@ -30,8 +30,10 @@ Compilation To compile you need to run the command: ```bash +make -C jbmc/src java-models-library-download make -C jbmc/src ``` + Output ====== diff --git a/jbmc/regression/jbmc-strings/java_append_char/test.desc b/jbmc/regression/jbmc-strings/java_append_char/test.desc index efe6c611b39..5eba917c237 100644 --- a/jbmc/regression/jbmc-strings/java_append_char/test.desc +++ b/jbmc/regression/jbmc-strings/java_append_char/test.desc @@ -1,6 +1,6 @@ CORE test_append_char.class ---refine-strings --string-max-length 1000 --no-core-models --function test_append_char.main +--refine-strings --string-max-length 1000 --function test_append_char.main ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc/coreModels/test.desc b/jbmc/regression/jbmc/coreModels/test.desc index 22f3976f5d0..4d3f33bf979 100644 --- a/jbmc/regression/jbmc/coreModels/test.desc +++ b/jbmc/regression/jbmc/coreModels/test.desc @@ -1,6 +1,6 @@ CORE test.class ---show-symbol-table +--show-symbol-table --cp ../../../src/java_bytecode/library/core-models.jar:. ^EXIT=0$ ^SIGNAL=0$ ^Symbol\s*\.*\: java\:\:org\.cprover\.CProver\.\\:\(\)V$ diff --git a/jbmc/src/Makefile b/jbmc/src/Makefile index 169f77b0943..bfa0c692b5c 100644 --- a/jbmc/src/Makefile +++ b/jbmc/src/Makefile @@ -1,4 +1,5 @@ DIRS = janalyzer jbmc jdiff java_bytecode miniz +ROOT = ../ include config.inc @@ -40,7 +41,7 @@ generated_files: $(patsubst %, %_generated_files, $(DIRS)) # cleaning .PHONY: clean -clean: $(patsubst %, %_clean, $(DIRS)) cprover_clean +clean: $(patsubst %, %_clean, $(DIRS)) cprover_clean dist_clean $(patsubst %, %_clean, $(DIRS)): $(MAKE) $(MAKEARGS) -C $(patsubst %_clean, %, $@) clean ; \ @@ -48,3 +49,25 @@ $(patsubst %, %_clean, $(DIRS)): .PHONY: cprover_clean cprover_clean: $(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/src clean + +.PHONY: dist_clean +dist_clean: + rm -rf $(ROOT)dist + +# extended JBMC models download, for your convenience +java-models-library-download: + @echo "Downloading java models library" + @wget https://github.com/diffblue/java-models-library/archive/master.zip -O java-models-library.zip + @unzip java-models-library.zip + @rm java-models-library.zip + @cp -r java-models-library-master/src java_bytecode/library + @rm -r java-models-library-master + +.PHONY: dist +dist: java-models-library-download all + mkdir -p $(ROOT)dist/lib + cp java_bytecode/library/core-models.jar $(ROOT)dist/lib + mkdir -p $(ROOT)dist/bin + cp jbmc/jbmc $(ROOT)dist/bin + cp janalyzer/janalyzer $(ROOT)dist/bin + cp jdiff/jdiff $(ROOT)dist/bin diff --git a/jbmc/src/java_bytecode/CMakeLists.txt b/jbmc/src/java_bytecode/CMakeLists.txt index 99f4094ad3c..6fd4d77a666 100644 --- a/jbmc/src/java_bytecode/CMakeLists.txt +++ b/jbmc/src/java_bytecode/CMakeLists.txt @@ -10,9 +10,6 @@ add_library(java_bytecode ${sources} ${headers}) # targets wishing to depend on the target 'java_bytecode' may want to use generic_includes(java_bytecode) -# target 'java-core-models-inc' is defined in library/ -add_dependencies(java_bytecode java-core-models-inc) - # if you link java_bytecode.a in, then you also need to link other .a libraries # in target_link_libraries(java_bytecode util goto-programs miniz json) diff --git a/jbmc/src/java_bytecode/Makefile b/jbmc/src/java_bytecode/Makefile index 71c3e45b898..83d465fd379 100644 --- a/jbmc/src/java_bytecode/Makefile +++ b/jbmc/src/java_bytecode/Makefile @@ -49,7 +49,7 @@ include ../$(CPROVER_DIR)/src/common CLEANFILES = java_bytecode$(LIBEXT) -all: java_bytecode$(LIBEXT) +all: library java_bytecode$(LIBEXT) clean: clean_library @@ -57,10 +57,10 @@ clean: clean_library clean_library: $(MAKE) clean -C library -library/java_core_models.inc: - $(MAKE) -C library java_core_models.inc +.PHONY: library +library: + $(MAKE) -C library -java_class_loader$(OBJEXT): library/java_core_models.inc ############################################################################### java_bytecode$(LIBEXT): $(OBJ) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index a3130545edb..aae80a1778b 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -44,7 +44,6 @@ Author: Daniel Kroening, kroening@kroening.com void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) { assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null"); - java_class_loader.set_use_core_models(!cmd.isset("no-core-models")); string_refinement_enabled=cmd.isset("refine-strings"); throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions"); if(cmd.isset("java-max-input-array-length")) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index 0aabc7afc14..f7c0ac17020 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -27,7 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \ - "(no-core-models)" \ "(java-assume-inputs-non-null)" \ "(java-throw-runtime-exceptions)" \ "(java-max-input-array-length):" \ @@ -40,8 +39,6 @@ Author: Daniel Kroening, kroening@kroening.com "(java-no-load-class):" #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \ - " --no-core-models don't load internally provided models for core classes in\n"/* NOLINT(*) */ \ - " the Java Class Library\n" /* NOLINT(*) */ \ " --java-assume-inputs-non-null never initialize reference-typed parameter to the\n" /* NOLINT(*) */ \ " entry point with null\n" /* NOLINT(*) */ \ " --java-throw-runtime-exceptions make implicit runtime exceptions explicit\n" /* NOLINT(*) */ \ diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index 3104c52e084..cfe64958a2d 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/jbmc/src/java_bytecode/java_class_loader.cpp @@ -17,15 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_bytecode_parser.h" -#include "library/java_core_models.inc" - -/// This variable stores the data of the file core-models.jar. The macro -/// JAVA_CORE_MODELS_SIZE is defined in the header java_core_models.inc, which -/// gets generated at compile time by running a small utility (converter.cpp) on -/// actual .jar file. The number of bytes in the variable is -/// JAVA_CORE_MODELS_SIZE, another macro defined in java_core_models.inc. -unsigned char java_core_models[] = { JAVA_CORE_MODELS_DATA }; - java_class_loadert::parse_tree_with_overlayst &java_class_loadert::operator()( const irep_idt &class_name) { @@ -137,27 +128,6 @@ java_class_loadert::get_parse_tree( parse_trees.emplace_back(std::move(*parse_tree)); } - // Then add core models - if(use_core_models) - { - // Add internal jar file. The name is used to load it once only and - // reference it later. - std::string core_models = "core-models.jar"; - jar_pool( - class_loader_limit, core_models, java_core_models, JAVA_CORE_MODELS_SIZE); - - // This does not read from the jar file but from the jar_filet object we - // just created - jar_index_optcreft index = read_jar_file(class_loader_limit, core_models); - if(index) - { - optionalt parse_tree = - get_class_from_jar(class_name, core_models, *index, class_loader_limit); - if(parse_tree) - parse_trees.emplace_back(std::move(*parse_tree)); - } - } - // Then add everything on the class path for(const auto &cp_entry : config.java.classpath) { diff --git a/jbmc/src/java_bytecode/java_class_loader.h b/jbmc/src/java_bytecode/java_class_loader.h index 6634172da93..2f9634bb182 100644 --- a/jbmc/src/java_bytecode/java_class_loader.h +++ b/jbmc/src/java_bytecode/java_class_loader.h @@ -36,9 +36,7 @@ class java_class_loadert:public messaget typedef std::function(const irep_idt &)> get_extra_class_refs_functiont; - // Default constructor does not use core models - // for backward compatibility of unit tests - java_class_loadert() : use_core_models(true) + java_class_loadert() { } @@ -79,10 +77,6 @@ class java_class_loadert:public messaget { jar_files.push_back(f); } - void set_use_core_models(bool use_core_models) - { - this->use_core_models = use_core_models; - } static std::string file_to_class_name(const std::string &); static std::string class_name_to_file(const irep_idt &); @@ -137,9 +131,6 @@ class java_class_loadert:public messaget /// get_parse_tree). std::list jar_files; - /// Indicates that the core models should be loaded - bool use_core_models; - /// Classes to be explicitly loaded std::vector java_load_classes; get_extra_class_refs_functiont get_extra_class_refs; diff --git a/jbmc/src/java_bytecode/library/CMakeLists.txt b/jbmc/src/java_bytecode/library/CMakeLists.txt index 4a62176fac9..cfb3e4983b4 100644 --- a/jbmc/src/java_bytecode/library/CMakeLists.txt +++ b/jbmc/src/java_bytecode/library/CMakeLists.txt @@ -1,5 +1,18 @@ +message(STATUS "Downloading java-models-library...") +include("${CBMC_SOURCE_DIR}/../cmake/DownloadProject.cmake") + +# Note: 'PATCH_COMMAND' is being used instead of 'COMMAND' as +# 'download_project' does not work as expected if called without +# 'PATCH_COMMAND'. +download_project(PROJ java_models_library + URL https://github.com/diffblue/java-models-library/archive/master.zip + PATCH_COMMAND cmake -E copy_directory "${CMAKE_BINARY_DIR}/java_models_library-src/src" + "${JBMC_SOURCE_DIR}/java_bytecode/library/src" +) + find_package(Java REQUIRED) include(UseJava) + set(CMAKE_JAVA_COMPILE_FLAGS -sourcepath "src" -d "classes" -XDignore.symbol.file) # create a target for the executable performing the .jar -> .inc conversion @@ -9,16 +22,11 @@ add_executable(java-converter converter.cpp) file(GLOB_RECURSE java_sources "src/*.java") add_jar("core-models" ${java_sources}) -# define a cmake variable with the full path of the .inc file -set(JAVA_CORE_MODELS_INC "${CMAKE_CURRENT_BINARY_DIR}/java_core_models.inc") - -# define a rule telling cmake how to generate the file ${JAVA_CORE_MODELS_INC} from -# the .jar file by running the java-converter; the output file depends on the -# .jar file but also on the converter (!) -add_custom_command(OUTPUT ${JAVA_CORE_MODELS_INC} - COMMAND java-converter "JAVA_CORE_MODELS" "core-models.jar" > ${JAVA_CORE_MODELS_INC} - DEPENDS "core-models.jar" java-converter) - -# create a target 'core-models-inc' that depends on the .inc file -add_custom_target(java-core-models-inc - DEPENDS ${JAVA_CORE_MODELS_INC}) +# copy 'core-models.jar' to '/jbmc/src/java_bytecode/library'. +# This is needed to deal with unit tests that make use of the core-models +# library. So that they can find the 'core-models.jar' in the same place as +# if the project had been compiled with 'make'. +add_custom_command(TARGET core-models + POST_BUILD + COMMAND ${CMAKE_COMMAND} -E copy "core-models.jar" ${PROJECT_SOURCE_DIR}/java_bytecode/library + ) diff --git a/jbmc/src/java_bytecode/library/Makefile b/jbmc/src/java_bytecode/library/Makefile index 94b8ddd611e..b3c1db689f6 100644 --- a/jbmc/src/java_bytecode/library/Makefile +++ b/jbmc/src/java_bytecode/library/Makefile @@ -2,13 +2,11 @@ #javac compiles multiple classes for each source as it will compile dependent sources. #Thus we do not allow the make to run concurrently. -SRC = converter.cpp - include ../../config.inc include ../../$(CPROVER_DIR)/src/config.inc include ../../$(CPROVER_DIR)/src/common -SOURCE_DIR := src +SOURCE_DIR := src/main/java BINARY_DIR := classes FIND := find @@ -35,17 +33,11 @@ JARFLAGS := -cf core-models.jar: $(ALL_CLASSES) $(JAR) $(JARFLAGS) $@ -C $(BINARY_DIR) . -CLEANFILES = core-models.jar converter$(EXEEXT) java_core_models.inc +CLEANFILES = core-models.jar -all: java_core_models.inc +all: core-models.jar clean: clean_ clean_: $(RM) -Rf $(BINARY_DIR) - -converter$(EXEEXT): converter.cpp - $(LINKNATIVE) - -java_core_models.inc: converter$(EXEEXT) core-models.jar - ./converter$(EXEEXT) JAVA_CORE_MODELS core-models.jar > $@ diff --git a/jbmc/src/java_bytecode/library/src/org/cprover/CProver.java b/jbmc/src/java_bytecode/library/src/org/cprover/CProver.java deleted file mode 100644 index a040d29f1e5..00000000000 --- a/jbmc/src/java_bytecode/library/src/org/cprover/CProver.java +++ /dev/null @@ -1,172 +0,0 @@ -package org.cprover; - -public final class CProver -{ - public static boolean enableAssume=true; - public static boolean enableNondet=true; - public static boolean enableConcurrency=true; - - public static boolean nondetBoolean() - { - if (enableNondet) - { - throw new RuntimeException( - "Cannot execute program with CProver.nondetBoolean()"); - } - - return false; - } - - public static byte nondetByte() - { - if (enableNondet) - { - throw new RuntimeException( - "Cannot execute program with CProver.nondetByte()"); - } - - return 0; - } - - public static char nondetChar() - { - if (enableNondet) - { - throw new RuntimeException( - "Cannot execute program with CProver.nondetChar()"); - } - - return '\0'; - } - - public static short nondetShort() - { - if (enableNondet) - { - throw new RuntimeException( - "Cannot execute program with CProver.nondetShort()"); - } - - return 0; - } - - public static int nondetInt() - { - if (enableNondet) - { - throw new RuntimeException( - "Cannot execute program with CProver.nondetInt()"); - } - - return 0; - } - - public static long nondetLong() - { - if (enableNondet) - { - throw new RuntimeException( - "Cannot execute program with CProver.nondetLong()"); - } - - return 0; - } - - public static float nondetFloat() - { - if (enableNondet) - { - throw new RuntimeException( - "Cannot execute program with CProver.nondetFloat()"); - } - - return 0; - } - - public static double nondetDouble() - { - if (enableNondet) - { - throw new RuntimeException( - "Cannot execute program with CProver.nondetDouble()"); - } - - return 0; - } - - public static T nondetWithNull() - { - if (enableNondet) - { - throw new RuntimeException( - "Cannot execute program with CProver.nondetWithNull(T)"); - } - - return null; - } - - public static T nondetWithoutNull() - { - if (enableNondet) - { - throw new RuntimeException( - "Cannot execute program with CProver.nondetWithoutNull(T)"); - } - - return null; - } - - public static void startThread(int id) - { - if(enableConcurrency) - { - throw new RuntimeException( - "Cannot execute program with CProver.startThread()"); - } - } - - public static void endThread(int id) - { - if(enableConcurrency) - { - throw new RuntimeException( - "Cannot execute program with CProver.endThread()"); - } - } - - public static void atomicBegin() - { - if(enableConcurrency) - { - throw new RuntimeException( - "Cannot execute program with CProver.atomicBegin()"); - } - } - - public static void atomicEnd() - { - if(enableConcurrency) - { - throw new RuntimeException( - "Cannot execute program with CProver.atomicEnd()"); - } - } - - public static int getCurrentThreadID() - { - if(enableConcurrency) - { - throw new RuntimeException( - "Cannot execute program with CProver.getCurrentThreadID()"); - } - return 0; - } - - public static void assume(boolean condition) - { - if(enableAssume && !condition) - { - throw new RuntimeException("CProver.assume() predicate is false"); - } - } -}