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

@@ -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/library/converter.exe
-jbmc/src/java_bytecode/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

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

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:
+   To compile JBMC, you additionally need the JDK and the java-models-library.
-   On Debian-like distributions, do
+
+   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
    ```

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

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,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:
+.PHONY: library
-	$(MAKE) -C library java_core_models.inc
+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, 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"))

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -27,7 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #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, 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(*) */ \

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<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 @@ public:
   typedef std::function<std::vector<irep_idt>(const irep_idt &)>
     get_extra_class_refs_functiont;
 
-  // Default constructor does not use core models
+  java_class_loadert()
-  // for backward compatibility of unit tests
-  java_class_loadert() : use_core_models(true)
   {
   }
 
@@ -79,10 +77,6 @@ public:
   {
     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 @@ private:
   /// 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
+# copy 'core-models.jar' to '<PROJECT_ROOT>/jbmc/src/java_bytecode/library'.
-set(JAVA_CORE_MODELS_INC "${CMAKE_CURRENT_BINARY_DIR}/java_core_models.inc")
+# 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
-# define a rule telling cmake how to generate the file ${JAVA_CORE_MODELS_INC} from
+# if the project had been compiled with 'make'.
-# the .jar file by running the java-converter; the output file depends on the
+add_custom_command(TARGET core-models
-# .jar file but also on the converter (!)
+                   POST_BUILD
-add_custom_command(OUTPUT ${JAVA_CORE_MODELS_INC}
+                   COMMAND ${CMAKE_COMMAND} -E copy "core-models.jar" ${PROJECT_SOURCE_DIR}/java_bytecode/library
-    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})

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/src/org/cprover/CProver.java

@@ -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> T nondetWithNull()
-  {
-    if (enableNondet)
-    {
-      throw new RuntimeException(
-          "Cannot execute program with CProver.nondetWithNull<T>(T)");
-    }
-
-    return null;
-  }
-
-  public static <T> T nondetWithoutNull()
-  {
-    if (enableNondet)
-    {
-      throw new RuntimeException(
-          "Cannot execute program with CProver.nondetWithoutNull<T>(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");
-    }
-  }
-}