Merge pull request diffblue#188 from diffblue/pull-support-20170908

Pull security-scanner-support into subtree

Author: smowton

.travis.yml

@@ -1,28 +1,68 @@
 language: cpp
 
-matrix:
+jobs:
   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.
+# LOCAL CHANGES: added cbmc/ prefix to both these scripts
+
+    - &linter-stage
+      stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
+      env: NAME="CPP-LINT"
+      install:
+      script: cbmc/scripts/travis_lint.sh
+      before_cache:
+
+    - &doxygen-stage
+      stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
+      env: NAME="DOXYGEN-CHECK"
+      addons:
+        apt:
+          packages:
+            - doxygen
+      install:
+      script: cbmc/scripts/travis_doxygen.sh
+      before_cache:
+
+    # Ubuntu Linux with glibc using g++-5
+    - stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
+      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="ccache g++-5"
+
+# LOCAL CHANGES: Upgraded to diffblue-builder:alpine-0.0.4 because it includes Python
 
     # Alpine Linux with musl-libc using g++
-    - os: linux
+    - stage: Test different OS/CXX/Flags
+      os: linux
       sudo: required
       compiler: gcc
       cache: ccache
       services:
         - docker
       before_install:
-        - docker pull diffblue/cbmc-builder:alpine-0.0.1
+        - docker pull diffblue/diffblue-builder:alpine-0.0.4
       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"
+        - PRE_COMMAND="docker run -v ${TRAVIS_BUILD_DIR}:/cbmc -v ${HOME}/.ccache:/root/.ccache diffblue/diffblue-builder:alpine-0.0.4"
         - COMPILER="ccache g++"
 
 # LOCAL CHANGES: Added 'ant' to the OSX package list (needed by security-scanner regression tests)
 
     # OS X using g++
-    - os: osx
+    - stage: Test different OS/CXX/Flags
+      os: osx
       sudo: false
       compiler: gcc
       cache: ccache
@@ -31,42 +71,24 @@ matrix:
         - 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=g++
+      env: COMPILER="ccache g++"
 
     # OS X using clang++
-    - os: osx
+    - stage: Test different OS/CXX/Flags
+      os: osx
       sudo: false
       compiler: clang
       cache: ccache
       before_install:
         - 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"
         - CCACHE_CPP2=yes
 
-    # Ubuntu Linux with glibc using g++-5
-    - 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"
-
     # Ubuntu Linux with glibc using g++-5, debug mode
-    - os: linux
+    - stage: Test different OS/CXX/Flags
+      os: linux
       sudo: false
       compiler: gcc
       cache: ccache
@@ -82,12 +104,13 @@ matrix:
         - 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"
+        - COMPILER="ccache 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
+    - stage: Test different OS/CXX/Flags
+      os: linux
       sudo: false
       compiler: clang
       cache: ccache
@@ -110,7 +133,8 @@ matrix:
         - CCACHE_CPP2=yes
 
     # Ubuntu Linux with glibc using clang++-3.7, debug mode
-    - os: linux
+    - stage: Test different OS/CXX/Flags
+      os: linux
       sudo: false
       compiler: clang
       cache: ccache
@@ -134,42 +158,27 @@ matrix:
         - 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)
-
-    - env: NAME="CPP-LINT"
-      install:
-      script: cbmc/scripts/travis_lint.sh
-      before_cache:
-
-    - env: NAME="DOXYGEN-CHECK"
-      addons:
-        apt:
-          packages:
-            - 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:
+    - <<: *linter-stage
+    - <<: *doxygen-stage
 
 # 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:
+  - ccache --max-size=1G
   - 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 cbmc/src/ansi-c library_check" &&
+    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
+# LOCAL CHANGES: Added cbmc/ prefix, and added unit and regression tests to the end of the list.
 
 script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;

benchmarks/TRAINING/diffblue/taint_traces_05/AssignmentAction.java

@@ -1,4 +1,3 @@
-import java.util.HashMap;
 import java.util.List;
 import java.io.InputStream;
 import java.io.IOException;
@@ -10,16 +9,16 @@ public void doUpload_all(RunData data) {
     FileItem fileFromUpload = null;
     fileFromUpload = params.getFileItem("file");
     InputStream fileContentStream = fileFromUpload.getInputStream();
-    HashMap submissionTable = new HashMap();
+    StringMap submissionTable = new StringMap();
     List submissions = null;
     submissions = AssignmentService.getSubmissions("some_param");
     submissionTable = uploadAll_parseZipFile(fileContentStream,submissionTable);
     uploadAll_updateSubmissions(submissionTable,submissions);
   }
 
-  private HashMap uploadAll_parseZipFile(
+  private StringMap uploadAll_parseZipFile(
         InputStream fileContentStream,
-        HashMap submissionTable
+        StringMap submissionTable
         ) {
     // If we do not load the class java.util.zip.ZipInputStream, then we
     // loose the class hierarchy => our rules stop working correctly. The
@@ -30,16 +29,16 @@ private HashMap uploadAll_parseZipFile(
     submissionTable.put("some_key",comment);
     return submissionTable;
   }
-  
+
   private void uploadAll_updateSubmissions(
-        HashMap submissionTable,
+        StringMap submissionTable,
         List submissions
         ) {
     if (submissions == null)
       return;
     AssignmentSubmissionEdit sEdit = editSubmission();
     if (sEdit != null)
-      sEdit.setSubmittedText((String)submissionTable.get("some_key"));
+      sEdit.setSubmittedText(submissionTable.get("some_key"));
   }
 
   private AssignmentSubmissionEdit editSubmission() {
@@ -63,4 +62,3 @@ private String readIntoString(InputStream zin) {
     return buffer.toString();
   }
 }
-

benchmarks/TRAINING/diffblue/taint_traces_05/StringMap.java

@@ -0,0 +1,25 @@
+
+// This is a dumb map-like container to replace HashMap, because when HashMap's
+// method bodies are unavailable cbmc will assume that generic Object-returning
+// methods actually return an Object, not a subclass, and hence using it to store
+// Strings fails when downcasting the result of HashMap.get(...)
+
+// This isn't actually a functional map, but is complex enough to exercise taint analysis.
+
+public class StringMap {
+
+  private String[] store;
+
+  public StringMap() {
+    store = new String[1];
+  }
+
+  public void put(Object key, String value) {
+    store[0] = value;
+  }
+
+  public String get(Object key) {
+    return store[0];
+  }
+
+}

benchmarks/TRAINING/diffblue/taint_traces_05_rules.json

@@ -98,27 +98,27 @@
         }
       },
       {
-        "comment": "Inserting a potentially tainted string into a HashMap container. Making the container tainted.",
-        "id": "HashMap.put(*,String)->*",
-        "class": "java.util.HashMap",
-        "method": "put:(Ljava/lang/Object;Ljava/lang/Object;)Ljava/lang/Object;",
+        "comment": "Inserting a potentially tainted string into a StringMap container. Making the container tainted.",
+        "id": "StringMap.put(*,String)->*",
+        "class": "StringMap",
+        "method": "put:(Ljava/lang/Object;Ljava/lang/String;)Ljava/lang/Object;",
         "input": {
           "location": "arg2",
           "taint": "<toString(TaintedInputStream.read@byte[])@String>"
         },
         "result": {
           "location": "arg0",
-          "taint": "<HashMap.put(toString(TaintedInputStream.read@byte[]))@HashMap>"
+          "taint": "<StringMap.put(toString(TaintedInputStream.read@byte[]))@StringMap>"
         }
       },
       {
-        "comment": "Retrieving a potentially tainted string from a HashMap container.",
-        "id": "HashMap.get(HashMap,*)->String",
-        "class": "java.util.HashMap",
-        "method": "get:(Ljava/lang/Object;)Ljava/lang/Object;",
+        "comment": "Retrieving a potentially tainted string from a StringMap container.",
+        "id": "StringMap.get(StringMap,*)->String",
+        "class": "StringMap",
+        "method": "get:(Ljava/lang/Object;)Ljava/lang/String;",
         "input": {
           "location": "arg0",
-          "taint": "<HashMap.put(toString(TaintedInputStream.read@byte[]))@HashMap>"
+          "taint": "<StringMap.put(toString(TaintedInputStream.read@byte[]))@StringMap>"
         },
         "result": {
           "location": "return_value",

benchmarks/evaluator.py

@@ -143,6 +143,7 @@ def __evaluate_benchmark(record):
         "--name \"" + record["name"] + "\" " +
         record["custom-options-for-security-scanner"]
         )
+    print(command)
     os.system(command)
 
     # And finally, we check whether the computed results match the expected ones.