From cf30702f86ebaa4c9d225219508b93fd9d707f46 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sat, 13 Aug 2022 11:43:58 -0400 Subject: [PATCH 1/5] CI: Use Ubuntu 22.04, drop 18.04 GitHub Actions has deprecated its Ubuntu 18.04 runners, and they will be removed by December 1, 2022. Moreover, GitHub Actions now offers Ubuntu 22.04 runners. It seems like a good time to upgrade our CI accordingly. Somewhat annoyingly, the `haskell` Docker images that we use in our Dockerfiles use such an old version of Debian that their version of `glibc` is incompatible with any of the `what4-solvers` built for Ubuntu 20.04 or 22.04. As a result, I switched them from the `haskell` Docker image to the `ubuntu` one. This required some minor tweaks to how dependencies are installed, but nothing too serious. Fixes #1741. By upgrading the version of the solvers being used, this also fixes #1744. --- .dockerignore | 1 + .github/workflows/ci.yml | 43 +++++++++++++++++------------ s2nTests/README.md | 2 +- s2nTests/scripts/blst-entrypoint.sh | 2 +- saw-remote-api/Dockerfile | 28 +++++++++++++++---- saw/Dockerfile | 28 +++++++++++++++---- 6 files changed, 73 insertions(+), 31 deletions(-) diff --git a/.dockerignore b/.dockerignore index b3bbde6d36..dd1881b6ed 100644 --- a/.dockerignore +++ b/.dockerignore @@ -3,6 +3,7 @@ .DS_Store .cabal-sandbox cabal.sandbox.config +cabal.project.local .ghc.environment.x86_64-darwin-* s2nTests diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7f17eedea2..3a634279e0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,6 +1,7 @@ # Overall configuration notes: # - Artifact uploads for binaries are from GHC 8.10.7 -# - Builds for Ubuntu happen on 18.04 (would like to include 20.04, in addition) +# - Builds for Ubuntu happen on 22.04. We also include a single configuration +# for 20.04 to increase our Linux coverage. # - Docker builds happen nightly, on manual invocation, and on release branch commits # Please update this comment as those details change. @@ -23,13 +24,13 @@ env: # ./saw-remote-api/Dockerfile # ./s2nTests/scripts/blst-entrypoint.sh # ./s2nTests/docker/saw.dockerfile - SOLVER_PKG_VERSION: "snapshot-20220721" + SOLVER_PKG_VERSION: "snapshot-20220902" OCAML_VERSION: 4.09.x jobs: config: - runs-on: ubuntu-latest + runs-on: ubuntu-22.04 outputs: name: ${{ steps.config.outputs.name }} version: ${{ steps.config.outputs.version }} @@ -66,20 +67,28 @@ jobs: strategy: fail-fast: false matrix: - os: [ubuntu-18.04, macos-12, windows-latest] + os: [ubuntu-22.04, macos-12, windows-latest] ghc: ["8.8.4", "8.10.7", "9.0.2"] + run-tests: [true] + include: + - os: ubuntu-20.04 + ghc: "8.10.7" + run-tests: false exclude: # Exclude 8.8 on macOS 12 due to # https://gitlab.haskell.org/ghc/ghc/-/issues/18446 - os: macos-12 ghc: "8.8.4" + run-tests: true - os: windows-latest ghc: "8.8.4" + run-tests: true # Exclude 9.0 on Windows for now until # https://github.com/commercialhaskell/stackage/issues/6400 # is resolved - os: windows-latest ghc: "9.0.2" + run-tests: false outputs: cabal-test-suites-json: ${{ steps.cabal-test-suites.outputs.targets-json }} steps: @@ -91,9 +100,9 @@ jobs: - id: config shell: bash run: | - NAME="${{ needs.config.outputs.name }}-${{ runner.os }}-x86_64" + NAME="${{ needs.config.outputs.name }}-${{ matrix.os }}-x86_64" .github/ci.sh output name $NAME - echo "NAME=${{ needs.config.outputs.name }}-${{ runner.os }}-x86_64" >> $GITHUB_ENV + echo "NAME=${{ needs.config.outputs.name }}-${{ matrix.os }}-x86_64" >> $GITHUB_ENV - uses: haskell/actions/setup@v1 id: setup-haskell @@ -119,9 +128,9 @@ jobs: path: | ${{ steps.setup-haskell.outputs.cabal-store }} dist-newstyle - key: ${{ env.CACHE_VERSION }}-cabal-${{ runner.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}-${{ github.sha }} + key: ${{ env.CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}-${{ github.sha }} restore-keys: | - ${{ env.CACHE_VERSION }}-cabal-${{ runner.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}- + ${{ env.CACHE_VERSION }}-cabal-${{ matrix.os }}-${{ matrix.ghc }}-${{ hashFiles(format('cabal.GHC-{0}.config', matrix.ghc)) }}- - if: needs.config.outputs.release == 'true' shell: bash @@ -198,7 +207,7 @@ jobs: if-no-files-found: error retention-days: ${{ needs.config.outputs.retention-days }} - - if: "matrix.ghc == '8.10.7'" + - if: matrix.ghc == '8.10.7' && matrix.run-tests uses: actions/upload-artifact@v2 with: path: dist/bin @@ -209,7 +218,7 @@ jobs: strategy: fail-fast: false matrix: - os: [ubuntu-latest, macos-12] + os: [ubuntu-22.04, macos-12] runs-on: ${{ matrix.os }} steps: - uses: actions/checkout@v2 @@ -243,7 +252,7 @@ jobs: strategy: fail-fast: false matrix: - os: [ubuntu-latest, macos-12] + os: [ubuntu-22.04, macos-12] runs-on: ${{ matrix.os }} steps: - uses: actions/checkout@v2 @@ -295,7 +304,7 @@ jobs: include: - name: Install and test test: saw-remote-api/scripts/run_rpc_tests.sh - os: ubuntu-18.04 + os: ubuntu-22.04 # TODO: saw-remote-api unit tests are disabled pending a fix for #1699 - name: Install on MacOS test: | @@ -306,7 +315,7 @@ jobs: os: macos-12 - name: Check docs test: saw-remote-api/scripts/check_docs.sh - os: ubuntu-18.04 + os: ubuntu-22.04 steps: - uses: actions/checkout@v2 with: @@ -350,7 +359,7 @@ jobs: fail-fast: false matrix: suite: ${{ fromJson(needs.build.outputs.cabal-test-suites-json) }} - os: [ubuntu-18.04] + os: [ubuntu-22.04] continue-on-error: [false] include: - suite: integration_tests @@ -414,7 +423,7 @@ jobs: dist-tests/${{ matrix.suite }} build-push-image: - runs-on: ubuntu-latest + runs-on: ubuntu-22.04 needs: [config] if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' || needs.config.outputs.release == 'true' strategy: @@ -516,7 +525,7 @@ jobs: name: "Test s2n proofs" timeout-minutes: 120 needs: build - runs-on: ubuntu-18.04 + runs-on: ubuntu-22.04 strategy: fail-fast: false matrix: @@ -569,7 +578,7 @@ jobs: # - changes to jobs or job instances don't require a mergify config update # - dependencies through `needs:` are validated, CI will fail if it's invalid mergify: - runs-on: ubuntu-latest + runs-on: ubuntu-22.04 needs: - build - heapster-tests diff --git a/s2nTests/README.md b/s2nTests/README.md index 82703c925f..baf64ee823 100644 --- a/s2nTests/README.md +++ b/s2nTests/README.md @@ -3,7 +3,7 @@ This directory contains Docker configurations for running some more complex cryp (These are the same configurations used in our GitHub Actions CI.) ## Building SAWScript -Running `make saw-script` will build SAWScript from the current working tree and place the resulting `saw` binary in `bin/`. This is useful if you develop on a system that isn't binary-compatible with Ubuntu 18.04 (e.g. macOS or NixOS). +Running `make saw-script` will build SAWScript from the current working tree and place the resulting `saw` binary in `bin/`. This is useful if you develop on a system that isn't binary-compatible with Ubuntu 22.04 (e.g. macOS or NixOS). ## Running tests Running `make ` on one of the following targets will use the `saw` binary in `bin/` to run the respective proof: diff --git a/s2nTests/scripts/blst-entrypoint.sh b/s2nTests/scripts/blst-entrypoint.sh index 2a1ba1dfb0..e306a1724e 100755 --- a/s2nTests/scripts/blst-entrypoint.sh +++ b/s2nTests/scripts/blst-entrypoint.sh @@ -5,7 +5,7 @@ cd /workdir ./scripts/install.sh cp /saw-bin/saw bin/saw -wget --quiet -O solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20210917/ubuntu-20.04-bin.zip" +wget --quiet -O solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220902/ubuntu-20.04-bin.zip" (cd bin && unzip -o ../solvers.zip) chmod +x bin/* diff --git a/saw-remote-api/Dockerfile b/saw-remote-api/Dockerfile index 35b8e92805..81ab9c3354 100644 --- a/saw-remote-api/Dockerfile +++ b/saw-remote-api/Dockerfile @@ -1,6 +1,13 @@ -FROM haskell:8.8.4 AS build +FROM ubuntu:22.04 AS build USER root -RUN apt-get update && apt-get install -y wget libncurses-dev unzip +RUN apt-get update && \ + apt-get install -y \ + # ghcup requirements + build-essential curl libffi-dev libffi8 libgmp-dev libgmp10 libncurses-dev libncurses6 libtinfo6 \ + # SAW dependencies + zlib1g-dev \ + # Miscellaneous + git wget unzip RUN useradd -m saw COPY --chown=saw:saw . /home/saw USER saw @@ -8,18 +15,27 @@ WORKDIR /home/saw ENV LANG=C.UTF-8 \ LC_ALL=C.UTF-8 COPY cabal.GHC-8.8.4.config cabal.project.freeze +ENV PATH=/home/saw/ghcup-download/bin:/home/saw/.ghcup/bin:$PATH +RUN mkdir -p /home/saw/ghcup-download/bin && \ + curl -L https://downloads.haskell.org/~ghcup/0.1.17.7/x86_64-linux-ghcup-0.1.17.7 -o /home/saw/ghcup-download/bin/ghcup && \ + chmod +x /home/saw/ghcup-download/bin/ghcup +RUN mkdir -p /home/saw/.ghcup && \ + ghcup --version && \ + ghcup install cabal 3.6.2.0 && \ + ghcup install ghc 8.8.4 && \ + ghcup set ghc 8.8.4 RUN cabal v2-update && cabal v2-build -j exe:saw-remote-api RUN mkdir -p /home/saw/rootfs/usr/local/bin RUN cp $(cabal v2-exec which saw-remote-api) /home/saw/rootfs/usr/local/bin/saw-remote-api WORKDIR /home/saw//rootfs/usr/local/bin -RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20210917/ubuntu-18.04-bin.zip" +RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220902/ubuntu-22.04-bin.zip" RUN unzip solvers.zip && rm solvers.zip && chmod +x * USER root RUN chown -R root:root /home/saw/rootfs -FROM debian:buster-slim -RUN apt-get update \ - && apt-get install -y libgmp10 libgomp1 libffi6 wget libncurses5 unzip libreadline-dev openjdk-11-jdk-headless +FROM ubuntu:22.04 +RUN apt-get update && \ + apt-get install -y libgmp10 libgomp1 libffi8 wget libncurses6 unzip libreadline-dev openjdk-11-jdk-headless COPY --from=build /home/saw/rootfs / RUN useradd -m saw && chown -R saw:saw /home/saw USER saw diff --git a/saw/Dockerfile b/saw/Dockerfile index 1ea90c4aaf..a61edafeb7 100644 --- a/saw/Dockerfile +++ b/saw/Dockerfile @@ -1,6 +1,13 @@ -FROM haskell:8.8.4 AS build +FROM ubuntu:22.04 AS build USER root -RUN apt-get update && apt-get install -y wget libncurses-dev unzip +RUN apt-get update && \ + apt-get install -y \ + # ghcup requirements + build-essential curl libffi-dev libffi8 libgmp-dev libgmp10 libncurses-dev libncurses6 libtinfo6 \ + # SAW dependencies + zlib1g-dev \ + # Miscellaneous + git wget unzip RUN useradd -m saw COPY --chown=saw:saw . /home/saw USER saw @@ -8,19 +15,28 @@ WORKDIR /home/saw ENV LANG=C.UTF-8 \ LC_ALL=C.UTF-8 COPY cabal.GHC-8.8.4.config cabal.project.freeze +ENV PATH=/home/saw/ghcup-download/bin:/home/saw/.ghcup/bin:$PATH +RUN mkdir -p /home/saw/ghcup-download/bin && \ + curl -L https://downloads.haskell.org/~ghcup/0.1.17.7/x86_64-linux-ghcup-0.1.17.7 -o /home/saw/ghcup-download/bin/ghcup && \ + chmod +x /home/saw/ghcup-download/bin/ghcup +RUN mkdir -p /home/saw/.ghcup && \ + ghcup --version && \ + ghcup install cabal 3.6.2.0 && \ + ghcup install ghc 8.8.4 && \ + ghcup set ghc 8.8.4 RUN cabal v2-update RUN cabal v2-build RUN mkdir -p /home/saw/rootfs/usr/local/bin RUN cp $(cabal v2-exec which saw) /home/saw/rootfs/usr/local/bin/saw WORKDIR /home/saw//rootfs/usr/local/bin -RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20210917/ubuntu-18.04-bin.zip" +RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220902/ubuntu-22.04-bin.zip" RUN unzip solvers.zip && rm solvers.zip && chmod +x * USER root RUN chown -R root:root /home/saw/rootfs -FROM debian:buster-slim -RUN apt-get update \ - && apt-get install -y libgmp10 libgomp1 libffi6 wget libncurses5 libreadline-dev unzip +FROM ubuntu:22.04 +RUN apt-get update && \ + apt-get install -y libgmp10 libgomp1 libffi8 wget libncurses6 libreadline-dev unzip COPY --from=build /home/saw/rootfs / RUN useradd -m saw && chown -R saw:saw /home/saw USER saw From 3c833d79aa0e0d1df931b500775680fb182bc2ab Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 10 Oct 2022 15:22:00 -0400 Subject: [PATCH 2/5] Port s2nTests over to Ubuntu 22.04 --- s2nTests/docker/awslc.dockerfile | 4 +- s2nTests/docker/blst.dockerfile | 4 +- s2nTests/docker/s2n.dockerfile | 8 ++-- s2nTests/docker/saw.dockerfile | 69 +++++++++++--------------------- 4 files changed, 31 insertions(+), 54 deletions(-) diff --git a/s2nTests/docker/awslc.dockerfile b/s2nTests/docker/awslc.dockerfile index d05b6f99ed..f4d5727ce9 100644 --- a/s2nTests/docker/awslc.dockerfile +++ b/s2nTests/docker/awslc.dockerfile @@ -1,6 +1,6 @@ -FROM ubuntu:20.04 +FROM ubuntu:22.04 RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections -RUN apt-get update && apt-get install -y wget unzip git cmake clang llvm golang python3-pip libncurses5 quilt +RUN apt-get update && apt-get install -y wget unzip git cmake clang llvm golang python3-pip libncurses6 quilt RUN pip3 install wllvm WORKDIR /saw-script diff --git a/s2nTests/docker/blst.dockerfile b/s2nTests/docker/blst.dockerfile index 931d9c2725..8f6cf37b7c 100644 --- a/s2nTests/docker/blst.dockerfile +++ b/s2nTests/docker/blst.dockerfile @@ -1,6 +1,6 @@ -FROM ubuntu:20.04 +FROM ubuntu:22.04 RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections -RUN apt-get update && apt-get install -y wget unzip git cmake clang llvm golang python3-pip libncurses5 quilt +RUN apt-get update && apt-get install -y wget unzip git cmake clang llvm golang python3-pip libncurses6 quilt RUN pip3 install wllvm RUN git clone https://github.com/GaloisInc/blst-verification.git /workdir && \ diff --git a/s2nTests/docker/s2n.dockerfile b/s2nTests/docker/s2n.dockerfile index 82b7af20c8..d47be0956d 100644 --- a/s2nTests/docker/s2n.dockerfile +++ b/s2nTests/docker/s2n.dockerfile @@ -1,14 +1,14 @@ -FROM ubuntu:18.04 +FROM ubuntu:22.04 RUN apt-get update -y -q && \ apt-get install -y software-properties-common && \ apt-get update -q -y && \ apt install -y \ - clang-3.9 \ + clang-12 \ curl \ gcc \ git \ - llvm-3.9 \ + llvm-12 \ make \ sudo \ && \ @@ -25,4 +25,4 @@ RUN mkdir -p /saw-script && \ COPY scripts/s2n-entrypoint.sh /entrypoint.sh ENTRYPOINT [ "/entrypoint.sh" ] -CMD [ "/bin/bash" ] \ No newline at end of file +CMD [ "/bin/bash" ] diff --git a/s2nTests/docker/saw.dockerfile b/s2nTests/docker/saw.dockerfile index 4eb83bf9d4..d97fc4319c 100644 --- a/s2nTests/docker/saw.dockerfile +++ b/s2nTests/docker/saw.dockerfile @@ -1,47 +1,13 @@ -FROM debian:stretch AS solvers - -# Install needed packages for building -RUN apt-get update \ - && apt-get install -y curl cmake gcc g++ git libreadline-dev unzip -RUN useradd -m user -RUN install -d -o user -g user /solvers -USER user -WORKDIR /solvers -RUN mkdir -p rootfs/usr/local/bin - -# Get Z3 4.8.10 from GitHub -RUN curl -L https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-ubuntu-18.04.zip --output z3.zip -RUN unzip z3.zip -RUN mv z3-*/bin/z3 rootfs/usr/local/bin - -# Build abc from GitHub. (Latest version.) -RUN git clone https://github.com/berkeley-abc/abc.git -RUN cd abc && make -j$(nproc) -RUN cp abc/abc rootfs/usr/local/bin - -# Build Boolector release 3.2.1 from source -RUN curl -L https://github.com/Boolector/boolector/archive/3.2.1.tar.gz | tar xz -RUN cd boolector* && ./contrib/setup-lingeling.sh && ./contrib/setup-btor2tools.sh && ./configure.sh && cd build && make -j$(nproc) -RUN cp boolector*/build/bin/boolector rootfs/usr/local/bin - -# Install Yices 2.6.2 -RUN curl -L https://yices.csl.sri.com/releases/2.6.2/yices-2.6.2-x86_64-pc-linux-gnu-static-gmp.tar.gz | tar xz -RUN cp yices*/bin/yices-smt2 rootfs/usr/local/bin \ - && cp yices*/bin/yices rootfs/usr/local/bin - -# Install CVC4 1.8 -RUN curl -L https://github.com/CVC4/CVC4/releases/download/1.8/cvc4-1.8-x86_64-linux-opt --output rootfs/usr/local/bin/cvc4 - -# Install MathSAT 5.6.3 - Uncomment if you are in compliance with MathSAT's license. -# RUN curl -L https://mathsat.fbk.eu/download.php?file=mathsat-5.6.3-linux-x86_64.tar.gz | tar xz -# RUN cp mathsat-5.6.3-linux-x86_64/bin/mathsat rootfs/usr/local/bin - -# Set executable and run tests -RUN chmod +x rootfs/usr/local/bin/* - -FROM haskell:8.8.4-stretch AS build +FROM ubuntu:22.04 AS build USER root -RUN apt-get update && apt-get install -y wget libncurses-dev unzip +RUN apt-get update && \ + apt-get install -y \ + # ghcup requirements + build-essential curl libffi-dev libffi8 libgmp-dev libgmp10 libncurses-dev libncurses6 libtinfo6 \ + # SAW dependencies + zlib1g-dev \ + # Miscellaneous + git wget unzip COPY --from=solvers /solvers/rootfs / RUN useradd -m saw COPY --chown=saw:saw . /home/saw @@ -50,17 +16,28 @@ WORKDIR /home/saw ENV LANG=C.UTF-8 \ LC_ALL=C.UTF-8 COPY cabal.GHC-8.8.4.config cabal.project.freeze +ENV PATH=/home/saw/ghcup-download/bin:/home/saw/.ghcup/bin:$PATH +RUN mkdir -p /home/saw/ghcup-download/bin && \ + curl -L https://downloads.haskell.org/~ghcup/0.1.17.7/x86_64-linux-ghcup-0.1.17.7 -o /home/saw/ghcup-download/bin/ghcup && \ + chmod +x /home/saw/ghcup-download/bin/ghcup +RUN mkdir -p /home/saw/.ghcup && \ + ghcup --version && \ + ghcup install cabal 3.6.2.0 && \ + ghcup install ghc 8.8.4 && \ + ghcup set ghc 8.8.4 RUN cabal v2-update RUN cabal v2-build RUN mkdir -p /home/saw/rootfs/usr/local/bin RUN cp $(cabal v2-exec which saw) /home/saw/rootfs/usr/local/bin/saw WORKDIR /home/saw +RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220902/ubuntu-22.04-bin.zip" +RUN unzip solvers.zip && rm solvers.zip && chmod +x * USER root RUN chown -R root:root /home/saw/rootfs -FROM debian:stretch-slim -RUN apt-get update \ - && apt-get install -y libgmp10 libgomp1 libffi6 wget libncurses5 unzip +FROM ubuntu:22.04 +RUN apt-get update && \ + apt-get install -y libgmp10 libgomp1 libffi8 wget libncurses6 libreadline-dev unzip COPY --from=build /home/saw/rootfs / COPY --from=solvers /solvers/rootfs / RUN useradd -m saw && chown -R saw:saw /home/saw From 8b3f02e8fd0d4ce057165001f7116a7d03b52263 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Sat, 15 Oct 2022 23:42:35 -0400 Subject: [PATCH 3/5] Ensure s2nTests all run on Ubuntu 22.04 Also, delete the redundant saw.dockerfile --- s2nTests/docker-compose.yml | 4 +-- s2nTests/docker/awslc.dockerfile | 5 +++- s2nTests/docker/blst.dockerfile | 5 +++- s2nTests/docker/s2n.dockerfile | 22 ++++++++++++-- s2nTests/docker/saw.dockerfile | 47 ------------------------------ s2nTests/scripts/s2n-entrypoint.sh | 5 +++- 6 files changed, 34 insertions(+), 54 deletions(-) delete mode 100644 s2nTests/docker/saw.dockerfile diff --git a/s2nTests/docker-compose.yml b/s2nTests/docker-compose.yml index 64b1e1aa80..7fcd4ab12b 100644 --- a/s2nTests/docker-compose.yml +++ b/s2nTests/docker-compose.yml @@ -3,8 +3,8 @@ services: saw-script: build: context: .. - dockerfile: ${PWD:-.}/docker/saw.dockerfile - entrypoint: ["cp", "/usr/local/bin/saw", "/saw-bin"] + dockerfile: ${PWD:-.}/../saw/Dockerfile + entrypoint: ["cp", "/usr/local/bin/saw", "/usr/local/bin/abc", "/saw-bin"] user: root volumes: - ${PWD:-}/bin:/saw-bin:rw diff --git a/s2nTests/docker/awslc.dockerfile b/s2nTests/docker/awslc.dockerfile index f4d5727ce9..2bbecd6093 100644 --- a/s2nTests/docker/awslc.dockerfile +++ b/s2nTests/docker/awslc.dockerfile @@ -1,7 +1,10 @@ FROM ubuntu:22.04 RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections -RUN apt-get update && apt-get install -y wget unzip git cmake clang llvm golang python3-pip libncurses6 quilt +RUN apt-get update && apt-get install -y curl wget unzip git cmake golang python3-pip libncurses6 libncurses5 libtinfo-dev quilt file RUN pip3 install wllvm +RUN curl -OL https://github.com/llvm/llvm-project/releases/download/llvmorg-10.0.0/clang+llvm-10.0.0-x86_64-linux-gnu-ubuntu-18.04.tar.xz && \ + tar xf clang+llvm-10.0.0-x86_64-linux-gnu-ubuntu-18.04.tar.xz && \ + cp -r clang+llvm-10.0.0-x86_64-linux-gnu-ubuntu-18.04/* /usr WORKDIR /saw-script RUN mkdir -p /saw-script && \ diff --git a/s2nTests/docker/blst.dockerfile b/s2nTests/docker/blst.dockerfile index 8f6cf37b7c..f2442720eb 100644 --- a/s2nTests/docker/blst.dockerfile +++ b/s2nTests/docker/blst.dockerfile @@ -1,7 +1,10 @@ FROM ubuntu:22.04 RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections -RUN apt-get update && apt-get install -y wget unzip git cmake clang llvm golang python3-pip libncurses6 quilt +RUN apt-get update && apt-get install -y curl wget unzip git cmake golang python3-pip libncurses6 libncurses5 libtinfo-dev quilt file RUN pip3 install wllvm +RUN curl -OL https://github.com/llvm/llvm-project/releases/download/llvmorg-10.0.0/clang+llvm-10.0.0-x86_64-linux-gnu-ubuntu-18.04.tar.xz && \ + tar xf clang+llvm-10.0.0-x86_64-linux-gnu-ubuntu-18.04.tar.xz && \ + cp -r clang+llvm-10.0.0-x86_64-linux-gnu-ubuntu-18.04/* /usr RUN git clone https://github.com/GaloisInc/blst-verification.git /workdir && \ cd /workdir && \ diff --git a/s2nTests/docker/s2n.dockerfile b/s2nTests/docker/s2n.dockerfile index d47be0956d..947f1c7131 100644 --- a/s2nTests/docker/s2n.dockerfile +++ b/s2nTests/docker/s2n.dockerfile @@ -4,15 +4,33 @@ RUN apt-get update -y -q && \ apt-get install -y software-properties-common && \ apt-get update -q -y && \ apt install -y \ - clang-12 \ curl \ gcc \ + g++ \ git \ - llvm-12 \ make \ sudo \ + unzip \ + indent \ + kwstyle \ + libssl-dev \ + tcpdump \ + valgrind \ + lcov \ + m4 \ + nettle-dev \ + nettle-bin \ + pkg-config \ + zlib1g-dev \ + python3-pip \ + tox \ + libncurses5 \ + libtinfo-dev \ && \ rm -rf /var/lib/apt/lists/* +RUN curl -OL https://releases.llvm.org/3.9.0/clang+llvm-3.9.0-x86_64-linux-gnu-ubuntu-16.04.tar.xz && \ + tar xf clang+llvm-3.9.0-x86_64-linux-gnu-ubuntu-16.04.tar.xz && \ + cp -r clang+llvm-3.9.0-x86_64-linux-gnu-ubuntu-16.04/* /usr WORKDIR /saw-script RUN mkdir -p /saw-script && \ diff --git a/s2nTests/docker/saw.dockerfile b/s2nTests/docker/saw.dockerfile deleted file mode 100644 index d97fc4319c..0000000000 --- a/s2nTests/docker/saw.dockerfile +++ /dev/null @@ -1,47 +0,0 @@ -FROM ubuntu:22.04 AS build -USER root -RUN apt-get update && \ - apt-get install -y \ - # ghcup requirements - build-essential curl libffi-dev libffi8 libgmp-dev libgmp10 libncurses-dev libncurses6 libtinfo6 \ - # SAW dependencies - zlib1g-dev \ - # Miscellaneous - git wget unzip -COPY --from=solvers /solvers/rootfs / -RUN useradd -m saw -COPY --chown=saw:saw . /home/saw -USER saw -WORKDIR /home/saw -ENV LANG=C.UTF-8 \ - LC_ALL=C.UTF-8 -COPY cabal.GHC-8.8.4.config cabal.project.freeze -ENV PATH=/home/saw/ghcup-download/bin:/home/saw/.ghcup/bin:$PATH -RUN mkdir -p /home/saw/ghcup-download/bin && \ - curl -L https://downloads.haskell.org/~ghcup/0.1.17.7/x86_64-linux-ghcup-0.1.17.7 -o /home/saw/ghcup-download/bin/ghcup && \ - chmod +x /home/saw/ghcup-download/bin/ghcup -RUN mkdir -p /home/saw/.ghcup && \ - ghcup --version && \ - ghcup install cabal 3.6.2.0 && \ - ghcup install ghc 8.8.4 && \ - ghcup set ghc 8.8.4 -RUN cabal v2-update -RUN cabal v2-build -RUN mkdir -p /home/saw/rootfs/usr/local/bin -RUN cp $(cabal v2-exec which saw) /home/saw/rootfs/usr/local/bin/saw -WORKDIR /home/saw -RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220902/ubuntu-22.04-bin.zip" -RUN unzip solvers.zip && rm solvers.zip && chmod +x * -USER root -RUN chown -R root:root /home/saw/rootfs - -FROM ubuntu:22.04 -RUN apt-get update && \ - apt-get install -y libgmp10 libgomp1 libffi8 wget libncurses6 libreadline-dev unzip -COPY --from=build /home/saw/rootfs / -COPY --from=solvers /solvers/rootfs / -RUN useradd -m saw && chown -R saw:saw /home/saw -USER saw -ENV LANG=C.UTF-8 \ - LC_ALL=C.UTF-8 -ENTRYPOINT ["/usr/local/bin/saw"] diff --git a/s2nTests/scripts/s2n-entrypoint.sh b/s2nTests/scripts/s2n-entrypoint.sh index 48a0d807f3..5680df62ab 100755 --- a/s2nTests/scripts/s2n-entrypoint.sh +++ b/s2nTests/scripts/s2n-entrypoint.sh @@ -9,8 +9,11 @@ fi cd /saw-script/s2n echo 'JOBS=1' >> codebuild/bin/jobs.sh source codebuild/bin/s2n_setup_env.sh -SAW=true SAW_INSTALL_DIR=tmp-saw codebuild/bin/s2n_install_test_dependencies.sh +SAW=true SAW_INSTALL_DIR=tmp-saw ./codebuild/bin/install_default_dependencies.sh cp /saw-bin/saw "$SAW_INSTALL_DIR"/bin/saw cp /saw-bin/abc "$SAW_INSTALL_DIR"/bin/abc "$SAW_INSTALL_DIR"/bin/saw --version +export CFLAGS=-Wno-error=array-parameter +export CLANG=clang +export LLVMLINK=llvm-link exec codebuild/bin/s2n_codebuild.sh From 47e8ece194acd485dbd60c27b3d09d26d135efe2 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Mon, 21 Nov 2022 12:20:53 -0500 Subject: [PATCH 4/5] Test CI on older solver version --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3a634279e0..db6d1d04ea 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -24,7 +24,7 @@ env: # ./saw-remote-api/Dockerfile # ./s2nTests/scripts/blst-entrypoint.sh # ./s2nTests/docker/saw.dockerfile - SOLVER_PKG_VERSION: "snapshot-20220902" + SOLVER_PKG_VERSION: "snapshot-20210917" OCAML_VERSION: 4.09.x From 8095d01d5a8e0cc21508e641bee812177d552e35 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Mon, 21 Nov 2022 13:14:02 -0500 Subject: [PATCH 5/5] Try 22.04 binaries in BLST proof --- .github/workflows/ci.yml | 2 +- s2nTests/scripts/blst-entrypoint.sh | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index db6d1d04ea..3a634279e0 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -24,7 +24,7 @@ env: # ./saw-remote-api/Dockerfile # ./s2nTests/scripts/blst-entrypoint.sh # ./s2nTests/docker/saw.dockerfile - SOLVER_PKG_VERSION: "snapshot-20210917" + SOLVER_PKG_VERSION: "snapshot-20220902" OCAML_VERSION: 4.09.x diff --git a/s2nTests/scripts/blst-entrypoint.sh b/s2nTests/scripts/blst-entrypoint.sh index e306a1724e..4d8035b702 100755 --- a/s2nTests/scripts/blst-entrypoint.sh +++ b/s2nTests/scripts/blst-entrypoint.sh @@ -5,7 +5,7 @@ cd /workdir ./scripts/install.sh cp /saw-bin/saw bin/saw -wget --quiet -O solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220902/ubuntu-20.04-bin.zip" +wget --quiet -O solvers.zip "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220902/ubuntu-22.04-bin.zip" (cd bin && unzip -o ../solvers.zip) chmod +x bin/*