Bug 1430582 - Add Cryptol/SAW runs to Taskcluster r=franziskus

Reviewers: franziskus

Reviewed By: franziskus

Bug #: 1430582

Differential Revision: https://phabricator.services.mozilla.com/D388

automation/saw/bmul.cry

@@ -0,0 +1,8 @@
+/* This Source Code Form is subject to the terms of the Mozilla Public
+ * License, v. 2.0. If a copy of the MPL was not distributed with this
+ * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
+
+bmul : {n,m} (fin n, n >= 1, m == n*2 - 1) => [n] -> [n] -> ([n], [n])
+bmul a b = (take`{n} prod, drop`{n} prod)
+    where prod = pad (pmult a b : [m])
+          pad x = zero # x

automation/saw/bmul.saw

@@ -0,0 +1,26 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+
+import "bmul.cry";
+
+print "Loading LLVM bitcode...";
+m <- llvm_load_module "../../../dist/Debug/lib/libfreeblpriv3.so.bc";
+
+let SpecBinaryMul n = do {
+  x <- llvm_var "x" (llvm_int n);
+  y <- llvm_var "y" (llvm_int n);
+  llvm_ptr "r_high" (llvm_int n);
+  r_high <- llvm_var "*r_high" (llvm_int n);
+  llvm_ptr "r_low" (llvm_int n);
+  r_low <- llvm_var "*r_low" (llvm_int n);
+
+  let res = {{ bmul x y }};
+  llvm_ensure_eq "*r_high" {{ res.0 }};
+  llvm_ensure_eq "*r_low" {{ res.1 }};
+
+  llvm_verify_tactic abc;
+};
+
+print "Proving equality for 32-bit bmul()...";
+time (llvm_verify m "bmul32" [] (SpecBinaryMul 32));

automation/saw/chacha20.saw

@@ -0,0 +1,40 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+
+import "chacha20.cry" as chacha20;
+
+print "Proving ChaCha20 spec...";
+prove_print abc {{ chacha20::allTestsPass }};
+
+print "Loading LLVM bitcode...";
+m <- llvm_load_module "../../../dist/Debug/lib/libfreeblpriv3.so.bc";
+
+let SpecChaCha20 n = do {
+  llvm_ptr "output" (llvm_array n (llvm_int 8));
+  output <- llvm_var "*output" (llvm_array n (llvm_int 8));
+
+  llvm_ptr "plain" (llvm_array n (llvm_int 8));
+  plain <- llvm_var "*plain" (llvm_array n (llvm_int 8));
+
+  len <- llvm_var "len" (llvm_int 32);
+  llvm_assert_eq "len" {{ `n : [32] }};
+
+  llvm_ptr "k" (llvm_array 32 (llvm_int 8));
+  k <- llvm_var "*k" (llvm_array 32 (llvm_int 8));
+
+  llvm_ptr "n1" (llvm_array 12 (llvm_int 8));
+  n1 <- llvm_var "*n1" (llvm_array 12 (llvm_int 8));
+
+  ctr <- llvm_var "ctr" (llvm_int 32);
+
+  llvm_ensure_eq "*output" {{ chacha20::encrypt k ctr n1 plain }};
+
+  llvm_verify_tactic abc;
+};
+
+print "Proving equality for a single block...";
+time (llvm_verify m "Hacl_Chacha20_chacha20" [] (SpecChaCha20 64));
+
+print "Proving equality for multiple blocks...";
+time (llvm_verify m "Hacl_Chacha20_chacha20" [] (SpecChaCha20 256));

automation/taskcluster/docker-saw/Dockerfile

@@ -0,0 +1,42 @@
+FROM ubuntu:17.04
+MAINTAINER Tim Taubert <ttaubert@mozilla.com>
+
+RUN useradd -d /home/worker -s /bin/bash -m worker
+WORKDIR /home/worker
+
+ENV DEBIAN_FRONTEND noninteractive
+
+RUN apt-get update && apt-get install -y \
+    binutils \
+    build-essential \
+    bzip2 \
+    clang-3.8 \
+    curl \
+    gcc-multilib \
+    g++-multilib \
+    gyp \
+    lib32z1-dev \
+    mercurial \
+    ninja-build \
+    unzip \
+    zlib1g-dev
+
+# Install SAW/Cryptol.
+RUN curl -LO https://saw.galois.com/builds/nightly/saw-0.2-2018-01-14-Ubuntu14.04-64.tar.gz && \
+    tar xzvf saw-*.tar.gz -C /usr/local --strip-components=1 && \
+    rm saw-*.tar.gz
+
+# Install Z3.
+RUN curl -LO https://github.com/Z3Prover/z3/releases/download/z3-4.6.0/z3-4.6.0-x64-ubuntu-16.04.zip && \
+    unzip z3*.zip && \
+    cp -r z3*/* /usr/local/ && \
+    rm -fr z3*
+
+ADD bin /home/worker/bin
+RUN chmod +x /home/worker/bin/*
+
+# Change user.
+USER worker
+
+# Set a default command useful for debugging
+CMD ["/bin/bash", "--login"]

automation/taskcluster/docker-saw/bin/checkout.sh

@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+
+set -v -e -x
+
+# Default values for testing.
+REVISION=${NSS_HEAD_REVISION:-default}
+REPOSITORY=${NSS_HEAD_REPOSITORY:-https://hg.mozilla.org/projects/nss}
+
+# Clone NSS.
+for i in 0 2 5; do
+    sleep $i
+    hg clone -r $REVISION $REPOSITORY nss && exit 0
+    rm -rf nss
+done
+exit 1

automation/taskcluster/graph/src/extend.js

@@ -30,6 +30,11 @@ const HACL_GEN_IMAGE = {
   path: "automation/taskcluster/docker-hacl"
 };
 
+const SAW_IMAGE = {
+  name: "saw",
+  path: "automation/taskcluster/docker-saw"
+};
+
 const WINDOWS_CHECKOUT_CMD =
   "bash -c \"hg clone -r $NSS_HEAD_REVISION $NSS_HEAD_REPOSITORY nss || " +
     "(sleep 2; hg clone -r $NSS_HEAD_REVISION $NSS_HEAD_REPOSITORY nss) || " +
@@ -991,5 +996,56 @@ async function scheduleTools() {
     ]
   }));
 
+  let task_saw = queue.scheduleTask(merge(base, {
+    symbol: "B",
+    group: "SAW",
+    name: "LLVM bitcode build (32 bit)",
+    image: SAW_IMAGE,
+    kind: "build",
+    env: {
+      AR: "llvm-ar-3.8",
+      CC: "clang-3.8",
+      CCC: "clang++-3.8"
+    },
+    artifacts: {
+      public: {
+        expires: 24 * 7,
+        type: "directory",
+        path: "/home/worker/artifacts"
+      }
+    },
+    command: [
+      "/bin/bash",
+      "-c",
+      "bin/checkout.sh && nss/automation/taskcluster/scripts/build_gyp.sh --disable-tests --emit-llvm -m32"
+    ]
+  }));
+
+  queue.scheduleTask(merge(base, {
+    parent: task_saw,
+    symbol: "bmul",
+    group: "SAW",
+    name: "bmul.saw",
+    image: SAW_IMAGE,
+    command: [
+      "/bin/bash",
+      "-c",
+      "bin/checkout.sh && nss/automation/taskcluster/scripts/run_saw.sh bmul"
+    ]
+  }));
+
+  queue.scheduleTask(merge(base, {
+    parent: task_saw,
+    symbol: "ChaCha20",
+    group: "SAW",
+    name: "chacha20.saw",
+    image: SAW_IMAGE,
+    command: [
+      "/bin/bash",
+      "-c",
+      "bin/checkout.sh && nss/automation/taskcluster/scripts/run_saw.sh chacha20"
+    ]
+  }));
+
   return queue.submit();
 }

automation/taskcluster/graph/src/image_builder.js

@@ -30,7 +30,7 @@ export async function buildTask({name, path}) {
   let ns = `docker.images.v1.${process.env.TC_PROJECT}.${name}.hash.${hash}`;
 
   return {
-    name: "Image Builder",
+    name: `Image Builder (${name})`,
     image: "nssdev/image_builder:0.1.5",
     routes: ["index." + ns],
     env: {

automation/taskcluster/graph/src/try_syntax.js

@@ -51,7 +51,7 @@ function parseOptions(opts) {
   }
 
   // Parse tools.
-  let allTools = ["clang-format", "scan-build", "hacl"];
+  let allTools = ["clang-format", "scan-build", "hacl", "saw"];
   let tools = intersect(opts.tools.split(/\s*,\s*/), allTools);
 
   // If the given value is "all" run all tools.
@@ -77,7 +77,8 @@ function filter(opts) {
     // are not affected by platform or build type selectors.
     if (task.platform == "nss-tools") {
       return opts.tools.some(tool => {
-        return task.symbol.toLowerCase().startsWith(tool);
+        return task.symbol.toLowerCase().startsWith(tool) ||
+               (task.group && task.group.toLowerCase().startsWith(tool));
       });
     }
 

automation/taskcluster/scripts/run_saw.sh

@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+source $(dirname "$0")/tools.sh
+
+# Fetch artifact if needed.
+fetch_dist
+
+# Run SAW.
+saw "nss/automation/saw/$1.saw"

build.sh

@@ -91,6 +91,7 @@ while [ $# -gt 0 ]; do
         --sancov=?*) enable_sancov "${1#*=}" ;;
         --pprof) gyp_params+=(-Duse_pprof=1) ;;
         --ct-verif) gyp_params+=(-Dct_verif=1) ;;
+        --emit-llvm) gyp_params+=(-Demit_llvm=1 -Dsign_libs=0) ;;
         --disable-tests) gyp_params+=(-Ddisable_tests=1) ;;
         --no-zdefs) gyp_params+=(-Dno_zdefs=1) ;;
         --system-sqlite) gyp_params+=(-Duse_system_sqlite=1) ;;

coreconf/config.gypi

@@ -431,6 +431,10 @@
               'LIBRARY_SEARCH_PATHS': ['/usr/lib <(sanitizer_flags)'],
             },
           }],
+          [ 'emit_llvm==1', {
+            'cflags': ['-flto'],
+            'ldflags': ['-flto', '-fuse-ld=gold', '-Wl,-plugin-opt=save-temps'],
+          }],
           [ 'OS=="android" and mozilla_client==0', {
             'defines': [
               'NO_SYSINFO',

help.txt

@@ -37,6 +37,8 @@ NSS build tool options:
     --msan           do an msan build
     --sancov         do sanitize coverage builds
                      --sancov=func sets coverage to function level for example
+    --emit-llvm      emit LLVM bitcode while building
+                     (requires the gold linker, use clang-3.8 for SAW)
     --disable-tests  don't build tests and corresponding cmdline utils
     --system-sqlite  use system sqlite
     --no-zdefs       don't set -Wl,-z,defs