Merge pull request diffblue#174 from diffblue/smowton/feature/cbmc_subtree

Switch to git-subtree

Author: smowton

.gitmodules

@@ -1,33 +1,51 @@
 language: cpp
 
-# Disable the default submodule logic
-git:
-  submodules: false
-
 matrix:
   include:
 
+# LOCAL CHANGES: Added CBMC_ALPINE_BUILD so that regression tests (which require Python) can be skipped in this case.
+# We really only care about breaking core cbmc in this case anyhow.
+
+    # Alpine Linux with musl-libc using g++
+    - os: linux
+      sudo: required
+      compiler: gcc
+      cache: ccache
+      services:
+        - docker
+      before_install:
+        - docker pull diffblue/cbmc-builder:alpine-0.0.1
+      env:
+        - PRE_COMMAND="docker run --env CBMC_ALPINE_BUILD=yes -v ${TRAVIS_BUILD_DIR}:/cbmc -v ${HOME}/.ccache:/root/.ccache diffblue/cbmc-builder:alpine-0.0.1"
+        - COMPILER="ccache g++"
+
+# LOCAL CHANGES: Added 'ant' to the OSX package list (needed by security-scanner regression tests)
+
     # OS X using g++
     - os: osx
       sudo: false
       compiler: gcc
       cache: ccache
       before_install:
-        - HOMEBREW_NO_AUTO_UPDATE=1 brew install jq ccache ant
+          #we create symlink to non-ccache gcc, to be used in tests
+        - mkdir bin ; ln -s /usr/bin/gcc bin/gcc
+        - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache ant
         - export PATH=/usr/local/opt/ccache/libexec:$PATH
         - ccache -M 1G
-      env: COMPILER="ccache g++"
+      env: COMPILER=g++
 
     # OS X using clang++
     - os: osx
       sudo: false
       compiler: clang
       cache: ccache
       before_install:
-        - HOMEBREW_NO_AUTO_UPDATE=1 brew install jq ccache ant
+        - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache ant
         - export PATH=/usr/local/opt/ccache/libexec:$PATH
         - ccache -M 1G
-      env: COMPILER="ccache clang++ -Qunused-arguments -fcolor-diagnostics"
+      env:
+        - COMPILER="ccache clang++ -Qunused-arguments -fcolor-diagnostics"
+        - CCACHE_CPP2=yes
 
     # Ubuntu Linux with glibc using g++-5
     - os: linux
@@ -44,7 +62,29 @@ matrix:
             - libubsan0
       before_install:
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
-      env: COMPILER="ccache g++-5"
+      # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
+      env: COMPILER="g++-5"
+
+    # Ubuntu Linux with glibc using g++-5, debug mode
+    - os: linux
+      sudo: false
+      compiler: gcc
+      cache: ccache
+      addons:
+        apt:
+          sources:
+            - ubuntu-toolchain-r-test
+          packages:
+            - libwww-perl
+            - g++-5
+            - libubsan0
+      before_install:
+        - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
+      # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
+      env:
+        - COMPILER="g++-5"
+        - EXTRA_CXXFLAGS="-DDEBUG"
+      script: echo "Not running any tests for a debug build."
 
     # Ubuntu Linux with glibc using clang++-3.7
     - os: linux
@@ -63,59 +103,86 @@ matrix:
             - libubsan0
       before_install:
         - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
+        - export CCACHE_CPP2=yes
+      # env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
       env:
         - COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
         - CCACHE_CPP2=yes
 
-    - env: NAME="CPP-LINT"
+    # Ubuntu Linux with glibc using clang++-3.7, debug mode
+    - os: linux
+      sudo: false
+      compiler: clang
+      cache: ccache
       addons:
         apt:
+          sources:
+            - ubuntu-toolchain-r-test
+            - llvm-toolchain-precise-3.7
           packages:
             - libwww-perl
-      script:
-        - git fetch origin $TRAVIS_BRANCH && git branch $TRAVIS_BRANCH FETCH_HEAD && cbmc/scripts/travis_lint.sh
+            - clang-3.7
+            - libstdc++-5-dev
+            - libubsan0
+      before_install:
+        - mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
+        - export CCACHE_CPP2=yes
+      # env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
+      env:
+        - COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
+        - CCACHE_CPP2=yes
+        - EXTRA_CXXFLAGS="-DDEBUG"
+      script: echo "Not running any tests for a debug build."
+
+# LOCAL CHANGES: added cbmc/ prefix to both these scripts (and the allow_failures entry for cpp-lint)
 
-  allow_failures:
     - env: NAME="CPP-LINT"
+      install:
+      script: cbmc/scripts/travis_lint.sh
+      before_cache:
+
+    - env: NAME="DOXYGEN-CHECK"
       addons:
         apt:
           packages:
-            - libwww-perl
-      script:
-        - git fetch origin $TRAVIS_BRANCH && git branch $TRAVIS_BRANCH FETCH_HEAD && cbmc/scripts/travis_lint.sh
+            - doxygen
+      install:
+      script: cbmc/scripts/travis_doxygen.sh
+      before_cache:
+
+  allow_failures:
+    - env: NAME="CPP-LINT"
+      install:
+      script: cbmc/scripts/travis_lint.sh
       before_cache:
 
+# LOCAL CHANGES: added cbmc/ prefix to some of the following commands
+# LOCAL CHANGES: added goto-analyzer.dir, goto-diff.dir and goto-cc.dir to the additional build list (needed for CBMC's regression tests, but not by the security-scanner product)
+
 install:
-  - if [ -L bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
-  - |
-    # If this is a PR, CBMC submodule has to refer to 'diffblue/cbmc' not to a fork
-    if [[ ${TRAVIS_PULL_REQUEST} == "false" ]]
-    then
-      # Export list of all contributors to know which forks to pull
-      export USERS=$(curl -H "Authorization: token ${GITHUB_TOKEN}" \
-          https://api.github.com/repos/diffblue/security-scanner/contributors \
-        | jq -r '.[] | .login' \
-        | tr "\n" " ")
-      echo "List of forks to pull >${USERS}<"
-    else
-      echo "List of forks to pull >${USERS}<"
-    fi
-  # Run within host machine to setup CBMC remotes
-  - make setup-cbmc
-
-before_cache: ccache -s
+  - COMMAND="make -C cbmc/src minisat2-download" &&
+    eval ${PRE_COMMAND} ${COMMAND}
+  - COMMAND="make -C cbmc/src boost-download" &&
+    eval ${PRE_COMMAND} ${COMMAND}
+  - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g -DUSE_BOOST $EXTRA_CXXFLAGS\" -j2" &&
+    eval ${PRE_COMMAND} ${COMMAND}
+  - COMMAND="make -C cbmc/src CXX=\"$COMPILER\" CXXFLAGS=\"$FLAGS $EXTRA_CXXFLAGS\" -j2 goto-analyzer.dir goto-cc.dir goto-diff.dir clobber.dir memory-models.dir musketeer.dir" &&
+    eval ${PRE_COMMAND} ${COMMAND}
+
+# LOCAL CHANGES: added cbmc/ prefix to CBMC's test commands and appended security-scanner test commands
 
 script:
-  - |
-    # Compile in host machine/container & run tests in host machine/container
-    if [ -L bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
-    COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare -DUSE_BOOST\"" &&
-    eval ${PRE_COMMAND} ${COMMAND} &&
-    COMMAND="make -C unit test CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare -DUSE_BOOST\"" &&
-    eval ${PRE_COMMAND} ${COMMAND} &&
-    COMMAND="make regression" &&
+  - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
+    COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C cbmc/regression test CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\"" &&
+    eval ${PRE_COMMAND} ${COMMAND}
+  - COMMAND="make -C cbmc/unit CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\" -j2" &&
+    eval ${PRE_COMMAND} ${COMMAND}
+  - COMMAND="make -C cbmc/unit test" &&
+    eval ${PRE_COMMAND} ${COMMAND}
+  - COMMAND="make -C unit test CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g -DUSE_BOOST $EXTRA_CXXFLAGS\"" &&
+    eval ${PRE_COMMAND} ${COMMAND}
+  - COMMAND="scripts/travis_run_regression_tests.sh" &&
     eval ${PRE_COMMAND} ${COMMAND}
 
-notifications:
-  slack:
-    secure: "W/ZrxvFs/OiNYwD9BdtgM5HYMzBL6aBJ62wHwMjF4TKfkbpb05GgYQtwvNRy6cBPOfY4TxECPUzqKiJ6cpGoi4hyST0pye0pCbvZ0CEipT0JkaxtrOkssqmb9ezBpoE7qnPMgQ3eJKpg0DSpP9oE7y5SaUcCajzN7TcY1K4gRnUiyixNyH0fRpCYKLYB8p9Y/RmGMOcmTfWxuGa4TjKLRyI85tS1wZBe6WDkRj4uU7FaRPh88q6zTTFO4AJWBVQsEuP1x4Go0hsZ4r9dsG43hL2OVCVKZtQQVURXRAr7pOAE9mWwJNsAqkoiv/6eriZyJPALUcmEHvvqOJSQWB4iKWrRM+k8aarukcCzr86huLNwnSSWLhMz7Gaq5qe6GihTkCf16j5+6AqfYwIOcECzpNCF/8Sq/5H83/SGSCuT6j9RSpoiGD/fo03zCgp7TXEErUqfmtxJjOHPhBjKp9o0dYj/aBwX2/vBT8PWIrji1GLUoVEd4yGWzbaOk6koVEx3++qHt90SstuerWUQ9ln7n4p1ZLYws+jbJRX1Iadug/7i8mYjElF2/rnA5hqPxcyoF/e1AZ5sktxkSX3wIdEjLa48QaWKhom0mfZb+sIjDKp2GawPGIbN1uVqAmdHiPjIAsn3PxaKzZg/Lm94d+NyVqtzIuxTZJ70T/4Gycry8m0="
+before_cache:
+  - ccache -s

.travis.yml

@@ -8,14 +8,10 @@ clean:
 	$(MAKE) $(MAKEARGS) -C src clean
 
 setup-cbmc:
-  # Configure any extra remotes that are needed before updating the submodule
-	./setup_submodules.sh $(USERS)
-	git submodule update
-
   # To make a single step build, proactively do the dependency downloads:
 	$(MAKE) $(MAKEARGS) -C cbmc/src minisat2-download
 	$(MAKE) $(MAKEARGS) -C cbmc/src boost-download
-	
+
 regression:
 ifndef single
 	python ./benchmarks/evaluator.py

Makefile

@@ -0,0 +1,17 @@
+root = true
+
+[*]
+charset = utf-8
+
+indent_style = space
+indent_size = 2
+
+trim_trailing_whitespace = true
+
+max_line_length = 80
+end_of_line = lf
+insert_final_newline = true
+
+[*patch]
+# Trailing spaces are significant in patch files
+trim_trailing_whitespace = false

cbmc

@@ -0,0 +1,11 @@
+*.cpp text
+*.c text
+*.h text
+*.y text
+*.tex text
+*.shtml text
+*.html text
+*.css text
+*.inc text
+test.desc text
+Makefile text

cbmc/.editorconfig

@@ -0,0 +1,51 @@
+#!/bin/bash
+# Runs scripts/cpplint.py on the modified files
+# Based on https://github.com/s0enke/git-hooks/
+#
+# @author Peter Schrammel <[email protected]>
+
+gitRoot="$(dirname $0)/../.."
+
+# this is the magic:
+# retrieve all files in staging area that are added, modified or renamed
+# but no deletions etc
+files=$(git diff-index --name-only --cached --diff-filter=ACMR HEAD -- )
+
+if [ "$files" == "" ]; then
+    exit 0
+fi
+
+# create temporary copy of staging area and delete upon exit
+cleanup()
+{
+  rm -rf $tmpStaging
+}
+
+trap cleanup EXIT
+
+tmpStaging=$(mktemp -d)
+touch $tmpStaging/.git
+
+# Copy contents of staged version of files to temporary staging area
+# because we only want the staged version that will be commited and not
+# the version in the working directory
+stagedFiles=""
+for file in $files
+do
+  id=$(git diff-index --cached HEAD $file | cut -d " " -f4)
+
+  # create staged version of file in temporary staging area with the same
+  # path as the original file
+  mkdir -p "$tmpStaging/$(dirname $file)"
+  git cat-file blob $id > "$tmpStaging/$file"
+  stagedFiles="$stagedFiles $tmpStaging/$file"
+done
+
+output=$(cd $gitRoot; scripts/cpplint.py $stagedFiles 2>&1)
+retval=$?
+
+if [ $retval -ne 0 ]
+then
+    echo "$output"
+    exit 1
+fi