Merge pull request diffblue#455 from diffblue/smowton/merge/develop-2018-06-13

SEC-461: Merge from develop, 2018-06-13

Author: smowton

cbmc/.gitignore

@@ -49,7 +49,7 @@ 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
+src/cpp/cprover_library.inc
 
 # regression/test files
 *.out
@@ -123,9 +123,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
 

cbmc/.travis.yml

@@ -46,17 +46,35 @@ jobs:
       before_cache:
 
     - stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
-      env: NAME="DOXYGEN-CHECK"
+      env:
+        NAME: "DOXYGEN-CHECK"
+        DOXYGEN_VERSION: "1.8.14"
       addons:
         apt:
           sources:
             - sourceline: 'deb http://packages.cloud.google.com/apt cloud-sdk-trusty main'
               key_url: 'https://packages.cloud.google.com/apt/doc/apt-key.gpg'
           packages:
-            - doxygen
+            - cmake
             - google-cloud-sdk
+      cache:
+        directories:
+          - ${TRAVIS_BUILD_DIR}/doxygen/build/bin
       install:
-      script: scripts/travis_doxygen.sh
+        - |
+          # Build doxygen if it is not in Travis cache
+          if ! [ -x doxygen/build/bin/doxygen ]
+          then
+            mkdir -p doxygen/build \
+            && wget http://ftp.stack.nl/pub/users/dimitri/doxygen-${DOXYGEN_VERSION}.src.tar.gz -O- | tar -xz --strip-components=1 --directory doxygen \
+            && ( cd doxygen/build && cmake .. ) \
+            && make -j4 -C doxygen/build
+          fi
+        - export PATH="$PATH:${TRAVIS_BUILD_DIR}/doxygen/build/bin"
+      script:
+        - echo $PATH
+        - doxygen --version
+        - scripts/travis_doxygen.sh
       before_cache:
       after_success:
         # Google Cloud Integration
@@ -222,8 +240,9 @@ jobs:
 
     # Run Coverity
     - stage: Test different OS/CXX/Flags
+      if: type = cron
       os: linux
-      sudo: required
+      sudo: false
       compiler: gcc
       cache: ccache
       addons:
@@ -238,16 +257,11 @@ 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"
       before_install:
-        - |
-          if [[ "${TRAVIS_EVENT_TYPE}" != "cron" ]]
-          then
-            echo "This is not a cron build and build is not needed."
-            travis_terminate 0
-          fi
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
         - sudo update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 90
         - g++ --version
@@ -264,10 +278,12 @@ jobs:
 install:
   - ccache -z
   - ccache --max-size=1G
+  - make -C jbmc/src java-models-library-download
   - make -C src minisat2-download
   - make -C src boost-download
   - make -C src/ansi-c library_check
-  - make -C src "CXX=${COMPILER} -DUSE_BOOST ${EXTRA_CXXFLAGS}" -j3
+  - make -C src/cpp library_check
+  - make -C src "CXX=${COMPILER} ${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
 
@@ -287,9 +303,9 @@ notifications:
   webhooks:
     urls:
       - http://dashboard.diffblue.com/api/travis-webhooks
+      - https://us-central1-dev-user-joelallred.cloudfunctions.net/trigger-testgen-from-cbmc
     on_success: always
     on_failure: always
     on_start: never
     on_cancel: never
     on_error: always
-    

cbmc/COMPILING.md

@@ -27,17 +27,22 @@ 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.
+   Note that you need g++ version 5.0 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
    ```
@@ -95,7 +100,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
    ```
    That should do it. To run, you will need
    ```
-   export LD_LIBRARY_PATH=/usr/gcc/4.9/lib
+   export LD_LIBRARY_PATH=/usr/gcc/5.0/lib
    ```
 
 # COMPILATION ON FREEBSD 11

cbmc/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 java-models-library-master\.gitignore)) {
+     & 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
@@ -59,18 +64,9 @@ 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
-    rmdir /s /q ansi-c\arch_flags_mthumb_bad
-    rmdir /s /q ansi-c\arch_flags_mthumb_good
     rmdir /s /q ansi-c\Forward_Declaration2
     rmdir /s /q ansi-c\Incomplete_Type1
-    rmdir /s /q ansi-c\Union_Padding1
     rmdir /s /q ansi-c\Universal_characters1
-    rmdir /s /q ansi-c\function_return1
-    rmdir /s /q ansi-c\gcc_attributes7
-    rmdir /s /q ansi-c\struct6
-    rmdir /s /q ansi-c\struct7
     rmdir /s /q cbmc\Malloc23
     rmdir /s /q cbmc\byte_update2
     rmdir /s /q cbmc\byte_update3
@@ -80,16 +76,6 @@ test_script:
     rmdir /s /q cbmc\byte_update7
     rmdir /s /q cbmc\pipe1
     rmdir /s /q cbmc\unsigned___int128
-    rmdir /s /q cbmc-cpp
-    rmdir /s /q cpp\Decltype1
-    rmdir /s /q cpp\Decltype2
-    rmdir /s /q cpp\Function_Overloading1
-    rmdir /s /q cpp\enum2
-    rmdir /s /q cpp\enum7
-    rmdir /s /q cpp\enum8
-    rmdir /s /q cpp\nullptr1
-    rmdir /s /q cpp\sizeof1
-    rmdir /s /q cpp\static_assert1
     rmdir /s /q goto-gcc
     rmdir /s /q goto-instrument\slice08
     cd ..

cbmc/buildspec-windows.yml

@@ -0,0 +1,70 @@
+version: 0.2
+
+phases:
+  install:
+    commands:
+      - choco install cyg-get -y --no-progress
+      - cyg-get bash patch bison flex make wget perl
+
+  build:
+    commands:
+      - 'C:\tools\cygwin\bin\sed -i "s/BUILD_ENV[ ]*=.*/BUILD_ENV = MSVC/" src/config.inc'
+      - |
+        $env:Path = "C:\tools\cygwin\bin;$env:Path"
+        C:\tools\cygwin\bin\bash -c "make -C src minisat2-download DOWNLOADER=wget"
+
+      - |
+        $env:Path = "C:\tools\cygwin\bin;$env:Path"
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C src" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C unit all" '
+
+      - |
+        $env:Path = "C:\tools\cygwin\bin;$env:Path"
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/src" '
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -j4 -C jbmc/unit all ; exit 0" '
+
+  post_build:
+    commands:
+      - |
+        cd regression
+        # HACK disable failing tests
+        Remove-Item ansi-c\Forward_Declaration2 -Force -Recurse
+        Remove-Item ansi-c\Incomplete_Type1 -Force -Recurse
+        Remove-Item cbmc\Malloc23 -Force -Recurse
+        Remove-Item cbmc\byte_update2 -Force -Recurse
+        Remove-Item cbmc\byte_update3 -Force -Recurse
+        Remove-Item cbmc\byte_update4 -Force -Recurse
+        Remove-Item cbmc\byte_update5 -Force -Recurse
+        Remove-Item cbmc\byte_update6 -Force -Recurse
+        Remove-Item cbmc\byte_update7 -Force -Recurse
+        Remove-Item cbmc\pipe1 -Force -Recurse
+        Remove-Item cbmc\unsigned___int128 -Force -Recurse
+        Remove-Item cpp -Force -Recurse
+        Remove-Item cbmc-cpp -Force -Recurse
+        Remove-Item goto-gcc -Force -Recurse
+        Remove-Item systemc -Force -Recurse
+        Remove-Item goto-instrument\slice08 -Force -Recurse
+        Remove-Item goto-analyzer/constant_propagation_nondet_rounding_mode -Force -Recurse
+        cd ..
+
+      - |
+        $env:Path = "C:\tools\cygwin\bin;$env:Path"
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression test" '
+
+      - |
+        $env:Path = "C:\tools\cygwin\bin;$env:Path"
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C unit test" '
+
+      - |
+        $env:Path = "C:\tools\cygwin\bin;$env:Path"
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/regression test ; exit 0" '
+
+      - |
+        $env:Path = "C:\tools\cygwin\bin;$env:Path"
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/unit test ; exit 0" '
+
+artifacts:
+  files:
+
+cache:
+  paths:

cbmc/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)

cbmc/jbmc/README.md

@@ -4,7 +4,7 @@ About
 =====
 
 JBMC is a Bounded Model Checker for Java programs. It supports
-checking for runtime exceptions and user-definde assertions.
+checking for runtime exceptions and user-defined assertions.
 The verification is performed by unwinding the loops in the program
 and passing the resulting equation to a decision procedure.
 
@@ -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
 ======
 

cbmc/jbmc/regression/jbmc-strings/StartsWith/Test.class

@@ -0,0 +1,72 @@
+// Must be compiled with CProverString:
+// javac Test.java ../cprover/CProverString.java
+public class Test {
+
+    // Reference implementation
+    public static boolean referenceStartsWith(String s, String prefix, int offset) {
+        if (offset < 0 || offset > s.length() - prefix.length()) {
+            return false;
+        }
+
+        for (int i = 0; i < prefix.length(); i++) {
+            if (org.cprover.CProverString.charAt(s, offset + i)
+                    != org.cprover.CProverString.charAt(prefix, i)) {
+                return false;
+            }
+        }
+        return true;
+    }
+
+    public static boolean check(String s, String t, int offset) {
+        // Filter out null strings
+        if(s == null || t == null) {
+            return false;
+        }
+
+        // Act
+        final boolean result = s.startsWith(t, offset);
+
+        // Assert
+        final boolean referenceResult = referenceStartsWith(s, t, offset);
+        assert(result == referenceResult);
+
+        // Check reachability
+        assert(result == false);
+        return result;
+    }
+
+    public static boolean checkDet() {
+        boolean result = false;
+        result = "foo".startsWith("foo", 0);
+        assert(result);
+        result = "foo".startsWith("f", -1);
+        assert(!result);
+        result = "foo".startsWith("oo", 1);
+        assert(result);
+        result = "foo".startsWith("f", 1);
+        assert(!result);
+        result = "foo".startsWith("bar", 0);
+        assert(!result);
+        result = "foo".startsWith("oo", 2);
+        assert(!result);
+        assert(false);
+        return result;
+    }
+
+    public static boolean checkNonDet(String s) {
+        // Filter
+        if (s == null) {
+            return false;
+        }
+
+        // Act
+        final boolean result = s.startsWith(s, 1);
+
+        // Assert
+        assert(!result);
+
+        // Check reachability
+        assert(false);
+        return result;
+    }
+}

cbmc/jbmc/regression/jbmc-strings/StartsWith/Test.java

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--refine-strings --string-max-input-length 10 --unwind 10 --function Test.check
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 31 .*: SUCCESS
+assertion at file Test.java line 34 .*: FAILURE
+--