Bug 1395549 - CI integration for HACL*, r=mt

Summary:
This is the description for the new docker image, used to generate HACL* C code and compare it to existing code in NSS.

Differential Revision: https://nss-review.dev.mozaws.net/D411

--HG--
rename : automation/taskcluster/docker/bin/checkout.sh => automation/taskcluster/docker-hacl/bin/checkout.sh
extra : rebase_source : 57e67531d24557239b6cc6ea5914f59f584f6b62

automation/taskcluster/docker-hacl/Dockerfile

@@ -0,0 +1,70 @@
+FROM ubuntu:xenial
+
+MAINTAINER Franziskus Kiefer <franziskuskiefer@gmail.com>
+# Based on the HACL* image from Benjamin Beurdouche and
+# the original F* formula with Daniel Fabian
+
+# Pinned versions of HaCl* (F* and KreMLin are pinned as submodules)
+ENV haclrepo https://github.com/mitls/hacl-star.git
+
+# Define versions of dependencies
+ENV opamv 4.04.2
+ENV z3v 4.5.1.1f29cebd4df6-x64-ubuntu-14.04
+ENV haclversion 0030539598cde15d1a0e5f93b32e121f7b7b5a1c
+ENV haclbranch production-nss
+
+# Install required packages and set versions
+RUN apt-get -qq update
+RUN apt-get install --yes sudo libssl-dev libsqlite3-dev g++-5 gcc-5 m4 make opam pkg-config python libgmp3-dev cmake curl libtool-bin autoconf
+RUN update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 200
+RUN update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 200
+
+# Create user
+RUN useradd -ms /bin/bash worker
+RUN echo "worker ALL=(ALL:ALL) NOPASSWD:ALL" >> /etc/sudoers
+WORKDIR /home/worker
+
+# Add build and test scripts.
+ADD bin /home/worker/bin
+RUN chmod +x /home/worker/bin/*
+USER worker
+
+# Add "known-good" version of Z3
+RUN curl -LO https://github.com/FStarLang/binaries/raw/master/z3-tested/z3-${z3v}.zip
+RUN unzip z3-${z3v}.zip
+RUN rm z3-${z3v}.zip
+RUN mv z3-${z3v} z3
+ENV PATH "/home/worker/z3/bin:$PATH"
+
+# Prepare build (OCaml packages)
+ENV OPAMYES true
+RUN opam init
+RUN echo ". /home/worker/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true" >> .bashrc
+RUN opam switch -v ${opamv}
+RUN opam install ocamlfind batteries sqlite3 fileutils yojson ppx_deriving_yojson zarith pprint menhir ulex process fix wasm stdint
+
+# Get the HaCl* code
+RUN git clone ${haclrepo} hacl-star
+RUN git -C hacl-star checkout ${haclversion}
+
+# Prepare submodules, and build, verify, test, and extract c code
+# This caches the extracted c code (pins the HaCl* version). All we need to do
+# on CI now is comparing the code in this docker image with the one in NSS.
+RUN opam config exec -- make -C hacl-star nss -j$(nproc)
+
+# Get clang-format-3.9
+RUN curl -LO http://releases.llvm.org/3.9.1/clang+llvm-3.9.1-x86_64-linux-gnu-ubuntu-16.04.tar.xz
+RUN curl -LO http://releases.llvm.org/3.9.1/clang+llvm-3.9.1-x86_64-linux-gnu-ubuntu-16.04.tar.xz.sig
+# Verify the signature.
+RUN gpg --keyserver pool.sks-keyservers.net --recv-keys B6C8F98282B944E3B0D5C2530FC3042E345AD05D
+RUN gpg --verify *.tar.xz.sig
+# Install into /usr/local/.
+RUN sudo tar xJvf *.tar.xz -C /usr/local --strip-components=1
+# Cleanup.
+RUN rm *.tar.xz*
+
+# Cleanup
+RUN rm -rf ~/.ccache ~/.cache
+RUN sudo apt-get autoremove -y
+RUN sudo apt-get clean
+RUN sudo apt-get autoclean

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

@@ -0,0 +1,20 @@
+#!/usr/bin/env bash
+
+set -v -e -x
+
+if [ $(id -u) = 0 ]; then
+    # Drop privileges by re-running this script.
+    exec su worker $0
+fi
+
+# 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

@@ -20,6 +20,11 @@ const FUZZ_IMAGE = {
   path: "automation/taskcluster/docker-fuzz"
 };
 
+const HACL_GEN_IMAGE = {
+  name: "hacl",
+  path: "automation/taskcluster/docker-hacl"
+};
+
 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) || " +
@@ -934,5 +939,16 @@ async function scheduleTools() {
     ]
   }));
 
+  queue.scheduleTask(merge(base, {
+    symbol: "hacl",
+    name: "hacl",
+    image: HACL_GEN_IMAGE,
+    command: [
+      "/bin/bash",
+      "-c",
+      "bin/checkout.sh && nss/automation/taskcluster/scripts/run_hacl.sh"
+    ]
+  }));
+
   return queue.submit();
 }

automation/taskcluster/graph/src/try_syntax.js

@@ -51,7 +51,7 @@ function parseOptions(opts) {
   }
 
   // Parse tools.
-  let allTools = ["clang-format", "scan-build"];
+  let allTools = ["clang-format", "scan-build", "hacl"];
   let tools = intersect(opts.tools.split(/\s*,\s*/), allTools);
 
   // If the given value is "all" run all tools.

automation/taskcluster/scripts/run_hacl.sh

@@ -0,0 +1,24 @@
+#!/usr/bin/env bash
+
+if [[ $(id -u) -eq 0 ]]; then
+    # Drop privileges by re-running this script.
+    # Note: this mangles arguments, better to avoid running scripts as root.
+    exec su worker -c "$0 $*"
+fi
+
+set -e -x -v
+
+# The docker image this is running in has the HACL* and NSS sources.
+# The extracted C code from HACL* is already generated and the HACL* tests were
+# successfully executed.
+
+# Format the extracted C code.
+cd ~/hacl-star/snapshots/nss-production
+cp ~/nss/.clang-format .
+find . -type f -name '*.[ch]' -exec clang-format -i {} \+
+
+# These diff commands will return 1 if there are differences and stop the script.
+files=($(find ~/nss/lib/freebl/verified/ -type f -name '*.[ch]'))
+for f in "${files[@]}"; do
+    diff $f $(basename "$f")
+done