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/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 d05b6f99ed..2bbecd6093 100644 --- a/s2nTests/docker/awslc.dockerfile +++ b/s2nTests/docker/awslc.dockerfile @@ -1,7 +1,10 @@ -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 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 931d9c2725..f2442720eb 100644 --- a/s2nTests/docker/blst.dockerfile +++ b/s2nTests/docker/blst.dockerfile @@ -1,7 +1,10 @@ -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 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 82b7af20c8..947f1c7131 100644 --- a/s2nTests/docker/s2n.dockerfile +++ b/s2nTests/docker/s2n.dockerfile @@ -1,18 +1,36 @@ -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 \ curl \ gcc \ + g++ \ git \ - llvm-3.9 \ 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 && \ @@ -25,4 +43,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 deleted file mode 100644 index 4eb83bf9d4..0000000000 --- a/s2nTests/docker/saw.dockerfile +++ /dev/null @@ -1,70 +0,0 @@ -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 -USER root -RUN apt-get update && apt-get install -y wget libncurses-dev 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 -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 -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 -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/blst-entrypoint.sh b/s2nTests/scripts/blst-entrypoint.sh index 2a1ba1dfb0..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-20210917/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/* 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 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