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/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; } 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"); - } - } -}