Merge pull request diffblue#431 from diffblue/CBMC_merge_2018-05-30

Cbmc merge 2018-05-30

Author: owen-jones-diffblue

cbmc/.gitignore

@@ -49,13 +49,15 @@ 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
-src/java_bytecode/java_core_models.inc
+jbmc/src/java_bytecode/java_core_models.inc
 
 # regression/test files
 *.out
 regression/**/tests.log
 regression/**/*.gb
 regression/**/*.smt2
+jbmc/regression/**/tests.log
+jbmc/regression/**/tests-symex-driven-loading.log
 
 # regression/coverage file
 /regression/coverage_**
@@ -64,8 +66,6 @@ regression/**/*.smt2
 *~
 
 # libs downloaded by make [name]-download
-libzip/
-zlib/
 minisat*/
 glucose-syrup/
 boost-include/
@@ -96,38 +96,35 @@ src/memory-models/mm_y.tab.h
 # binaries
 src/cbmc/cbmc
 src/cbmc/cbmc.exe
-src/cegis/cegis
-src/cegis/cegis.exe
 src/goto-analyzer/goto-analyzer
 src/goto-analyzer/goto-analyzer.exe
 src/goto-cc/goto-cc
 src/goto-cc/goto-cc.exe
 src/goto-cc/goto-cl.exe
 src/goto-instrument/goto-instrument
 src/goto-instrument/goto-instrument.exe
-src/jbmc/jbmc
-src/musketeer/musketeer
-src/musketeer/musketeer.exe
 src/solvers/smt2_solver
 src/solvers/smt2_solver.exe
-src/symex/symex
-src/symex/symex.exe
 src/goto-diff/goto-diff
 src/goto-diff/goto-diff.exe
 src/clobber/clobber
 src/clobber/clobber.exe
 src/big-int/test-bigint
 src/big-int/test-bigint.exe
+jbmc/src/jbmc/janalyzer
+jbmc/src/jbmc/janalyzer.exe
+jbmc/src/jbmc/jdiff
+jbmc/src/jbmc/jdiff.exe
+jbmc/src/jbmc/jbmc
+jbmc/src/jbmc/jbmc.exe
 
 # build tools
 src/ansi-c/file_converter
 src/ansi-c/file_converter.exe
 src/ansi-c/library/converter
 src/ansi-c/library/converter.exe
-src/java_bytecode/converter
-src/java_bytecode/converter.exe
-src/util/irep_ids_convert
-src/util/irep_ids_convert.exe
+jbmc/src/java_bytecode/converter
+jbmc/src/java_bytecode/converter.exe
 build/
 
 *.pyc

cbmc/.travis.yml

@@ -99,10 +99,7 @@ jobs:
       before_install:
         - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache parallel
         - export PATH=$PATH:/usr/local/opt/ccache/libexec
-      env:
-        - COMPILER="ccache clang++"
-        - EXTRA_CXXFLAGS="-Qunused-arguments -fcolor-diagnostics"
-        - CCACHE_CPP2=yes
+      env: COMPILER="ccache clang++"
 
     # Ubuntu Linux with glibc using g++-5, debug mode
     - stage: Test different OS/CXX/Flags
@@ -237,7 +234,7 @@ jobs:
             description: "Travis build of ${TRAVIS_COMMIT}"
           notification_email: "[email protected]"
           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:
         - |
@@ -267,12 +264,16 @@ install:
   - make -C src/ansi-c library_check
   - make -C src "CXX=${COMPILER} -DUSE_BOOST ${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

cbmc/CMakeLists.txt

@@ -37,13 +37,15 @@ set(sat_impl "minisat2" CACHE STRING
     "This setting controls the SAT library which is used. Valid values are 'minisat2' and 'glucose'"
 )
 
-add_subdirectory(src)
-
 if(${enable_cbmc_tests})
     enable_testing()
 endif()
-add_subdirectory(unit)
+
+add_subdirectory(src)
 add_subdirectory(regression)
+add_subdirectory(unit)
+
+add_subdirectory(jbmc)
 
 set_target_properties(
     analyses
@@ -66,15 +68,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
@@ -84,6 +82,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

cbmc/CODEOWNERS

@@ -21,7 +21,7 @@ src/solvers/miniBDD @tautschnig @kroening
 src/solvers/prop @martin-cs @kroening @tautschnig @peterschrammel
 src/solvers/sat @martin-cs @kroening @tautschnig @peterschrammel
 src/solvers/smt2 @martin-cs @tautschnig @peterschrammel
-src/miniz/ @smowton @mgudemann @peterschrammel
+jbmc/src/miniz/ @smowton @mgudemann @peterschrammel
 
 
 # These files change frequently and changes are high-risk
@@ -30,7 +30,7 @@ src/cbmc/ @smowton @kroening @tautschnig @peterschrammel
 src/goto-programs/ @smowton @kroening @tautschnig @peterschrammel @pkesseli
 src/util/ @smowton @kroening @tautschnig @peterschrammel @pkesseli
 src/solvers/refinement @martin-cs @romainbrenguier @peterschrammel
-src/java_bytecode/ @smowton @mgudemann @thk123 @cristina-david @cesaro @pkesseli @NathanJPhillips @peterschrammel
+jbmc/src/java_bytecode/ @smowton @mgudemann @thk123 @cristina-david @cesaro @pkesseli @NathanJPhillips @peterschrammel
 src/analyses/ @martin-cs @peterschrammel @chrisr-diffblue @thk123 @smowton
 src/pointer-analysis/ @martin-cs @peterschrammel @chrisr-diffblue @smowton
 
@@ -40,7 +40,9 @@ src/pointer-analysis/ @martin-cs @peterschrammel @chrisr-diffblue @smowton
 src/goto-analyzer/ @martin-cs @chrisr-diffblue @peterschrammel
 src/goto-instrument/ @martin-cs @chrisr-diffblue @peterschrammel
 src/goto-diff/ @tautschnig @peterschrammel
-src/jbmc/ @smowton @mgudemann @cristina-david @cesaro @pkesseli @peterschrammel
+jbmc/src/jbmc/ @smowton @mgudemann @cristina-david @cesaro @pkesseli @peterschrammel
+jbmc/src/janalyzer/ @smowton @mgudemann @cristina-david @cesaro @pkesseli @peterschrammel
+jbmc/src/jdiff/ @smowton @mgudemann @cristina-david @cesaro @pkesseli @peterschrammel
 src/cpp/ @kroening @tautschnig @peterschrammel
 
 
@@ -50,6 +52,8 @@ src/util/irep_ids.def @diffblue/cbmc-developers
 
 unit/ @diffblue/cbmc-developers
 regression/ @diffblue/cbmc-developers
+jbmc/unit/ @diffblue/cbmc-developers
+jbmc/regression/ @diffblue/cbmc-developers
 
 scripts/ @diffblue/devops @thk123 @forejtv @peterschrammel
 .travis.yml @diffblue/devops @thk123 @forejtv @peterschrammel

cbmc/CODING_STANDARD.md

@@ -156,7 +156,7 @@ Formatting is enforced using clang-format. For more information about this, see
 - Make references `const` whenever possible
 - Make member functions `const` whenever possible
 - Do not hide base class functions
-- You are encouraged to use `override`
+- When overriding a virtual function, use `override` (without `virtual`)
 - Single argument constructors must be `explicit`
 - Avoid implicit conversions
 - Avoid `friend` declarations

cbmc/COMPILING.md

@@ -28,6 +28,17 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
    yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6 java-1.7.0-openjdk-devel
    ```
    Note that you need g++ version 4.9 or newer.
+
+   To compile JBMC, you additionally need 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
+   ```
+
 2. As a user, get the CBMC source via
    ```
    git clone https://github.com/diffblue/cbmc cbmc-git
@@ -93,7 +104,11 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
    ```
    pkg install bash gmake git www/p5-libwww patch flex bison openjdk
    ```
-2. As a user, get the CBMC source via
+   To compile JBMC, additionally install
+   ```
+   pkg install openjdk
+   ```
+ 2. As a user, get the CBMC source via
    ```
    git clone https://github.com/diffblue/cbmc cbmc-git
    ```
@@ -183,14 +198,14 @@ require manual modification of build files.
 1. Ensure you have all the build dependencies installed. Build dependencies are
    the same as for the makefile build, but with the addition of CMake version
    3.2 or higher. The installed CMake version can be queried with `cmake
-   --version`. To install all build dependencies:
+   --version`. To install cmake:
    - On Debian-like distributions, do
      ```
-     apt-get install cmake g++ gcc flex bison make git libwww-perl patch openjdk-7-jdk
+     apt-get install cmake
      ```
    - On Red Hat/Fedora or derivates, do
      ```
-     yum install cmake gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6 java-1.7.0-openjdk-devel
+     yum install cmake
      ```
    - On macOS, do
      ```

cbmc/appveyor.yml

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

cbmc/doc/cbmc-user-manual.md

@@ -2193,8 +2193,8 @@ section on [Assumptions and Assertions](modeling-assertions.shtml).
 #### \_\_CPROVER\_same\_object, \_\_CPROVER\_POINTER\_OBJECT, \_\_CPROVER\_POINTER\_OFFSET, \_\_CPROVER\_DYNAMIC\_OBJECT
 
     _Bool __CPROVER_same_object(const void *, const void *);
-    unsigned __CPROVER_POINTER_OBJECT(const void *p);
-    signed __CPROVER_POINTER_OFFSET(const void *p);
+    __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *p);
+    __CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *p);
     _Bool __CPROVER_DYNAMIC_OBJECT(const void *p);
 
 The function **\_\_CPROVER\_same\_object** returns true if the two

cbmc/jbmc/CMakeLists.txt

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

cbmc/jbmc/README.md

@@ -0,0 +1,52 @@
+[![Build Status][travis_img]][travis] [![Build Status][appveyor_img]][appveyor]
+
+About
+=====
+
+JBMC is a Bounded Model Checker for Java programs. It supports
+checking for runtime exceptions and user-definde assertions.
+The verification is performed by unwinding the loops in the program
+and passing the resulting equation to a decision procedure.
+
+[More info...](http://www.cprover.org/jbmc)
+
+Versions
+========
+
+Get the [latest release](https://github.com/diffblue/cbmc/releases)
+* Releases are tested and for production use.
+
+Get the current *develop* version: `git clone https://github.com/diffblue/cbmc.git`
+* Develop versions are not recommended for production use.
+
+Prerequisites
+============
+
+JBMC compiles CBMC as part of its build process and as such has all the pre-requisites of CBMC. These can be viewed at: [diffblue/cbmc:COMPILING](http://github.com/diffblue/cbmc/blob/master/COMPILING)
+
+Compilation
+===========
+
+To compile you need to run the command:
+
+```bash
+make -C jbmc/src
+```
+Output
+======
+
+Compiling produces an executable called `jbmc` which by default can be found in `jbmc/src/jbmc/jbmc`
+
+Reporting bugs and contributing to the code base
+================================================
+
+See [CBMC](https://github.com/diffblue/cbmc/blob/develop/README.md))
+
+License
+=======
+4-clause BSD license, see `LICENSE` file.
+
+[travis]: https://travis-ci.org/diffblue/cbmc
+[travis_img]: https://travis-ci.org/diffblue/cbmc.svg?branch=develop
+[appveyor]: https://ci.appveyor.com/project/diffblue/cbmc/
+[appveyor_img]: https://ci.appveyor.com/api/projects/status/github/diffblue/cbmc?svg=true&branch=develop

cbmc/jbmc/regression/CMakeLists.txt

@@ -0,0 +1,13 @@
+set(test_pl_path "${CBMC_SOURCE_DIR}/../regression/test.pl")
+
+# 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)