Merge pull request diffblue#2225 from cesaro/extended-java-models

JBMC: Added java-models-library dependency

.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
 

.travis.yml

@@ -238,6 +238,7 @@ jobs:
             name: "diffblue/cbmc"
             description: "Travis build of ${TRAVIS_COMMIT}"
           notification_email: "[email protected]"
+          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"
@@ -264,6 +265,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
@@ -291,4 +293,3 @@ notifications:
     on_start: never
     on_cancel: never
     on_error: always
-

COMPILING.md

@@ -29,15 +29,20 @@ 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
    ```
    On Red Hat/Fedora or derivates, do
    ```
    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
    ```

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

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)

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

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$

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\.\<clinit\>\:\(\)V$

jbmc/src/Makefile

@@ -1,4 +1,5 @@
 DIRS = janalyzer jbmc jdiff java_bytecode miniz
+ROOT = ../
 
 include config.inc
 
@@ -40,11 +41,33 @@ 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 ; \
 
 .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

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)

jbmc/src/java_bytecode/Makefile

@@ -49,18 +49,18 @@ include ../$(CPROVER_DIR)/src/common
 
 CLEANFILES = java_bytecode$(LIBEXT)
 
-all: java_bytecode$(LIBEXT)
+all: library java_bytecode$(LIBEXT)
 
 clean: clean_library
 
 .PHONY: 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)

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -44,7 +44,6 @@ Author: Daniel Kroening, [email protected]
 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"))

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -27,7 +27,6 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/language.h>
 
 #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, [email protected]
   "(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(*) */ \

jbmc/src/java_bytecode/java_class_loader.cpp

@@ -17,15 +17,6 @@ Author: Daniel Kroening, [email protected]
 
 #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<java_bytecode_parse_treet> 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)
   {

jbmc/src/java_bytecode/java_class_loader.h

@@ -36,9 +36,7 @@ class java_class_loadert:public messaget
   typedef std::function<std::vector<irep_idt>(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<std::string> jar_files;
 
-  /// Indicates that the core models should be loaded
-  bool use_core_models;
-
   /// Classes to be explicitly loaded
   std::vector<irep_idt> java_load_classes;
   get_extra_class_refs_functiont get_extra_class_refs;

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 '<PROJECT_ROOT>/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
+                  )

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

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;
 }