From 0d6e81070349955167fb39d7692cd18acb7462dc Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 26 Mar 2025 21:44:00 -0400 Subject: [PATCH 1/9] Move Ubuntu versions: mostly 22.04 / some 20.04 -> mostly 24.04 / some 22.04. Update the what4-solvers snapshot to get Ubuntu 24.04 bins. Note that GitHub Actions support for 20.04 is about to disappear. Leave heapster.dockerfile alone as it isn't being used and will need further attention to not break it. --- .github/workflows/ci.yml | 40 ++++++++++++++++---------------- exercises/Dockerfile | 2 +- s2nTests/README.md | 2 +- s2nTests/docker/awslc.dockerfile | 2 +- s2nTests/docker/blst.dockerfile | 2 +- s2nTests/docker/s2n.dockerfile | 2 +- saw-remote-api/Dockerfile | 6 ++--- saw/Dockerfile | 6 ++--- 8 files changed, 31 insertions(+), 31 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7ba35e61aa..aac2aaed40 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,7 +1,7 @@ # Overall configuration notes: # - Artifact uploads for binaries are from GHC 9.4.8 -# - Builds for Ubuntu happen on 22.04. We also include a single configuration -# for 20.04 to increase our Linux coverage. +# - Builds for Ubuntu happen on 24.04. We also include a single configuration +# for 22.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. @@ -33,11 +33,11 @@ env: # Solver package snapshot date - also update in the following locations: # ./saw/Dockerfile # ./saw-remote-api/Dockerfile - SOLVER_PKG_VERSION: "snapshot-20250227" + SOLVER_PKG_VERSION: "snapshot-20250326" jobs: config: - runs-on: ubuntu-22.04 + runs-on: ubuntu-24.04 outputs: name: ${{ steps.config.outputs.name }} version: ${{ steps.config.outputs.version }} @@ -74,7 +74,7 @@ jobs: strategy: fail-fast: false matrix: - os: [ubuntu-22.04] + os: [ubuntu-24.04] cabal: ["3.10.3.0"] ghc: ["9.4.8", "9.6.6", "9.8.2"] haddock: [true] @@ -84,14 +84,14 @@ jobs: # We include one job from an older Ubuntu LTS release to increase our # coverage of possible Linux configurations. Since we already run the # tests with the newest LTS release, we won't bother testing this one. - - os: ubuntu-20.04 + - os: ubuntu-22.04 ghc: "9.4.8" cabal: "3.10.3.0" haddock: false run-tests: false hpc: false # Include one job with HPC enabled - - os: ubuntu-22.04 + - os: ubuntu-24.04 ghc: "9.4.8" cabal: "3.10.3.0" haddock: false @@ -298,7 +298,7 @@ jobs: runs-on: ${{ matrix.os }} strategy: matrix: - os: [ubuntu-22.04] + os: [ubuntu-24.04] steps: - name: Check out repository (no submodules) uses: actions/checkout@v4 @@ -351,7 +351,7 @@ jobs: if: github.event_name == 'push' && needs.config.outputs.release == 'false' && github.repository_owner == 'GaloisInc' strategy: matrix: - os: [ubuntu-22.04] + os: [ubuntu-24.04] steps: - name: Check out repository (no submodules) uses: actions/checkout@v4 @@ -390,7 +390,7 @@ jobs: runs-on: ${{ matrix.os }} strategy: matrix: - os: [ubuntu-22.04] + os: [ubuntu-24.04] steps: - name: Check out gh-pages uses: actions/checkout@v4 @@ -430,7 +430,7 @@ jobs: strategy: fail-fast: false matrix: - os: [ubuntu-22.04, macos-14] + os: [ubuntu-24.04, macos-14] runs-on: ${{ matrix.os }} steps: - uses: actions/checkout@v4 @@ -465,7 +465,7 @@ jobs: strategy: fail-fast: false matrix: - os: [ubuntu-22.04, macos-14] + os: [ubuntu-24.04, macos-14] runs-on: ${{ matrix.os }} steps: - uses: actions/checkout@v4 @@ -522,7 +522,7 @@ jobs: include: - name: Install and test test: saw-remote-api/scripts/run_rpc_tests.sh - os: ubuntu-22.04 + os: ubuntu-24.04 # TODO: saw-remote-api unit tests are disabled pending a fix for #1699 - name: Install on MacOS test: | @@ -533,7 +533,7 @@ jobs: os: macos-14 - name: Check docs test: saw-remote-api/scripts/check_docs.sh - os: ubuntu-22.04 + os: ubuntu-24.04 steps: - uses: actions/checkout@v4 with: @@ -580,7 +580,7 @@ jobs: fail-fast: false matrix: suite: ${{ fromJson(needs.build.outputs.cabal-test-suites-json) }} - os: [ubuntu-22.04] + os: [ubuntu-24.04] continue-on-error: [false] include: - suite: integration_tests @@ -682,7 +682,7 @@ jobs: strategy: matrix: suite: ['integration_tests'] - os: [ubuntu-22.04] + os: [ubuntu-24.04] steps: # Need a copy of the source to generate coverage HTML - uses: actions/checkout@v4 @@ -775,7 +775,7 @@ jobs: keep_files: false build-push-image: - runs-on: ubuntu-22.04 + runs-on: ubuntu-24.04 needs: [config] # Restrict this to the main repository where the needed secrets # will be available. As noted above, scheduled runs also happen in @@ -887,7 +887,7 @@ jobs: - hmac-failure - awslc - blst - os: [ubuntu-22.04] + os: [ubuntu-24.04] ghc: ["9.4.8"] steps: - uses: actions/checkout@v4 @@ -941,7 +941,7 @@ jobs: runs-on: ${{ matrix.os }} strategy: matrix: - os: [ubuntu-22.04] + os: [ubuntu-24.04] ghc: ["9.4.8"] steps: - uses: actions/checkout@v4 @@ -973,7 +973,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-22.04 + runs-on: ubuntu-24.04 needs: - build - heapster-tests diff --git a/exercises/Dockerfile b/exercises/Dockerfile index 53667ba1ca..04a5e1b601 100644 --- a/exercises/Dockerfile +++ b/exercises/Dockerfile @@ -1,4 +1,4 @@ -FROM ubuntu:22.04 +FROM ubuntu:24.04 RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections RUN apt-get update && apt-get install -y clang-12 make diff --git a/s2nTests/README.md b/s2nTests/README.md index baf64ee823..d2a0234d2b 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 22.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 24.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/awslc.dockerfile b/s2nTests/docker/awslc.dockerfile index e52340a4b5..1839a83b39 100644 --- a/s2nTests/docker/awslc.dockerfile +++ b/s2nTests/docker/awslc.dockerfile @@ -1,4 +1,4 @@ -FROM ubuntu:22.04 +FROM ubuntu:24.04 RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections 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 diff --git a/s2nTests/docker/blst.dockerfile b/s2nTests/docker/blst.dockerfile index 1dc00f6be5..adf37bf24b 100644 --- a/s2nTests/docker/blst.dockerfile +++ b/s2nTests/docker/blst.dockerfile @@ -1,4 +1,4 @@ -FROM ubuntu:22.04 +FROM ubuntu:24.04 RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections 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 diff --git a/s2nTests/docker/s2n.dockerfile b/s2nTests/docker/s2n.dockerfile index 947f1c7131..c2d4a4659d 100644 --- a/s2nTests/docker/s2n.dockerfile +++ b/s2nTests/docker/s2n.dockerfile @@ -1,4 +1,4 @@ -FROM ubuntu:22.04 +FROM ubuntu:24.04 RUN apt-get update -y -q && \ apt-get install -y software-properties-common && \ diff --git a/saw-remote-api/Dockerfile b/saw-remote-api/Dockerfile index bd2a93a328..11d00b66c0 100644 --- a/saw-remote-api/Dockerfile +++ b/saw-remote-api/Dockerfile @@ -1,4 +1,4 @@ -FROM ubuntu:22.04 AS build +FROM ubuntu:24.04 AS build USER root RUN apt-get update && \ apt-get install -y \ @@ -32,12 +32,12 @@ WORKDIR /home/saw//rootfs/usr/local/bin # BUILD_TARGET_ARCH in `.github/workflow/ci.yml`, but specialized to x86-64 # Ubuntu. # If updating the snapshot version, update ci.yml and saw/Dockerfile too. -RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20250227/ubuntu-22.04-X64-bin.zip" +RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20250326/ubuntu-24.04-X64-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 +FROM ubuntu:24.04 RUN apt-get update && \ apt-get install -y libgmp10 libgomp1 libffi8 wget libncurses6 unzip libreadline-dev openjdk-11-jdk-headless zlib1g COPY --from=build /home/saw/rootfs / diff --git a/saw/Dockerfile b/saw/Dockerfile index 3276a13512..6c45b8523d 100644 --- a/saw/Dockerfile +++ b/saw/Dockerfile @@ -1,4 +1,4 @@ -FROM ubuntu:22.04 AS build +FROM ubuntu:24.04 AS build USER root RUN apt-get update && \ apt-get install -y \ @@ -33,12 +33,12 @@ WORKDIR /home/saw//rootfs/usr/local/bin # BUILD_TARGET_ARCH in `.github/workflow/ci.yml`, but specialized to x86-64 # Ubuntu. # If updating the snapshot version, update ci.yml and saw-remote-api/Dockerfile too. -RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20250227/ubuntu-22.04-X64-bin.zip" +RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20250326/ubuntu-24.04-X64-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 +FROM ubuntu:24.04 RUN apt-get update && \ apt-get install -y libgmp10 libgomp1 libffi8 wget libncurses6 libreadline-dev unzip zlib1g COPY --from=build /home/saw/rootfs / From 8cda5c5f6d6fac936acaca08c0fc8e84861df722 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 27 Mar 2025 15:12:14 -0400 Subject: [PATCH 2/9] exercises: bump clang in the docker image to clang-14 clang-12 is no longer available on ubuntu 24.04. also, rearrange the logic that symlinks clang -> clang-14 (and update it to 14) --- exercises/Dockerfile | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/exercises/Dockerfile b/exercises/Dockerfile index 04a5e1b601..10ae103b0d 100644 --- a/exercises/Dockerfile +++ b/exercises/Dockerfile @@ -1,9 +1,10 @@ FROM ubuntu:24.04 RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections -RUN apt-get update && apt-get install -y clang-12 make +RUN apt-get update && apt-get install -y clang-14 make -RUN find /usr/bin/ -name "*-12" -exec basename {} \; | sed "s/\-12//" | xargs -I{} ln -s /usr/bin/'{}'-12 /usr/bin/'{}' +# symlink clang -> clang-14 for all the clang bins +RUN (cd /usr/bin && ls *-14 | sed 's/-14$//' | awk '{ printf "ln -s %s-14 %s\n", $1, $1 }' | sh) COPY . /workdir From df6383c736408064360f0170cceada0fbff857c3 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 27 Mar 2025 15:12:47 -0400 Subject: [PATCH 3/9] s2ntests: use ncurses 6 in the docker images, drop ncurses 5 ncurses 5 is no longer available in ubuntu 24.04. If there's an ancient binary somewhere using it, we'll have to regen. We aren't running a museum here... --- s2nTests/docker/awslc.dockerfile | 2 +- s2nTests/docker/blst.dockerfile | 2 +- s2nTests/docker/s2n.dockerfile | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/s2nTests/docker/awslc.dockerfile b/s2nTests/docker/awslc.dockerfile index 1839a83b39..279c05482f 100644 --- a/s2nTests/docker/awslc.dockerfile +++ b/s2nTests/docker/awslc.dockerfile @@ -1,6 +1,6 @@ FROM ubuntu:24.04 RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections -RUN apt-get update && apt-get install -y curl wget unzip git cmake golang python3-pip libncurses6 libncurses5 libtinfo-dev quilt file +RUN apt-get update && apt-get install -y curl wget unzip git cmake golang python3-pip libncurses6 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 && \ diff --git a/s2nTests/docker/blst.dockerfile b/s2nTests/docker/blst.dockerfile index adf37bf24b..d7b643ee48 100644 --- a/s2nTests/docker/blst.dockerfile +++ b/s2nTests/docker/blst.dockerfile @@ -1,6 +1,6 @@ FROM ubuntu:24.04 RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections -RUN apt-get update && apt-get install -y curl wget unzip git cmake golang python3-pip libncurses6 libncurses5 libtinfo-dev quilt file +RUN apt-get update && apt-get install -y curl wget unzip git cmake golang python3-pip libncurses6 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 && \ diff --git a/s2nTests/docker/s2n.dockerfile b/s2nTests/docker/s2n.dockerfile index c2d4a4659d..d65eeeaeaf 100644 --- a/s2nTests/docker/s2n.dockerfile +++ b/s2nTests/docker/s2n.dockerfile @@ -24,7 +24,7 @@ RUN apt-get update -y -q && \ zlib1g-dev \ python3-pip \ tox \ - libncurses5 \ + libncurses6 \ libtinfo-dev \ && \ rm -rf /var/lib/apt/lists/* From 60c7dd9dc24c285229149e4228ba6c025ac162e4 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 27 Mar 2025 16:10:42 -0400 Subject: [PATCH 4/9] s2ntests: install wllvm with pip --break-system-packages This is apparently now required as a workaround to use pip (rather than apt) to install system-wide packages. --- s2nTests/docker/awslc.dockerfile | 6 +++++- s2nTests/docker/blst.dockerfile | 6 +++++- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/s2nTests/docker/awslc.dockerfile b/s2nTests/docker/awslc.dockerfile index 279c05482f..4458052aa0 100644 --- a/s2nTests/docker/awslc.dockerfile +++ b/s2nTests/docker/awslc.dockerfile @@ -1,7 +1,11 @@ FROM ubuntu:24.04 RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections RUN apt-get update && apt-get install -y curl wget unzip git cmake golang python3-pip libncurses6 libtinfo-dev quilt file -RUN pip3 install wllvm +# FUTURE: Apparently you're now supposed to install a venv and not try +# to use pip to install system-wide packages. --break-system-packages +# is probably ok as a workaround here but it wouldn't surprise me if +# it disappeared after a while. +RUN pip3 install --break-system-packages 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 diff --git a/s2nTests/docker/blst.dockerfile b/s2nTests/docker/blst.dockerfile index d7b643ee48..25a9dbfc0d 100644 --- a/s2nTests/docker/blst.dockerfile +++ b/s2nTests/docker/blst.dockerfile @@ -1,7 +1,11 @@ FROM ubuntu:24.04 RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections RUN apt-get update && apt-get install -y curl wget unzip git cmake golang python3-pip libncurses6 libtinfo-dev quilt file -RUN pip3 install wllvm +# FUTURE: Apparently you're now supposed to install a venv and not try +# to use pip to install system-wide packages. --break-system-packages +# is probably ok as a workaround here but it wouldn't surprise me if +# it disappeared after a while. +RUN pip3 install --break-system-packages 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 From 51bbe14101e64805136dd5c956bc3de99f81198d Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 27 Mar 2025 15:15:56 -0400 Subject: [PATCH 5/9] CI: move to setup-ocaml@v3 to work around problem on ubuntu 24.04 v2 tries to install darcs, which is not available on the ubuntu 24.04 runners. Changes are from #2153, which failed mysteriously when it was filed but might work better now. --- .github/workflows/ci.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index aac2aaed40..dca6715b32 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -489,9 +489,9 @@ jobs: chmod +x dist/bin/* echo $GITHUB_WORKSPACE/dist/bin >> $GITHUB_PATH - - uses: ocaml/setup-ocaml@v2 + - uses: ocaml/setup-ocaml@v3 with: - ocaml-compiler: 4.14.x + ocaml-compiler: "4.14" - run: opam repo add coq-released https://coq.inria.fr/opam/released From 62d80d4c099b02f39fab1816fb51e45027accf35 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 27 Mar 2025 17:48:08 -0400 Subject: [PATCH 6/9] s2ntests: Tell the s2n infrastructure not to install saw. This prevents it from downloading and trying to run an ancient binary that no longer runs on Ubuntu 24.04. Downside of this is that this also turns off fetching yices and z3, so instead copy in the yices and z3 we already have. This may or may not work since they're probably quite a bit newer than the ones expected, but if they do it's probably for the best. The tls and hmac proofs apparently need yices-smt2, so add that to the bits provided by docker-compose. This also may not be the way we want to do this, but if it works it avoids needing to change the s2n tree. --- s2nTests/docker-compose.yml | 2 +- s2nTests/scripts/s2n-entrypoint.sh | 14 +++++++++++++- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/s2nTests/docker-compose.yml b/s2nTests/docker-compose.yml index 0b39a4c8ed..8e778993b4 100644 --- a/s2nTests/docker-compose.yml +++ b/s2nTests/docker-compose.yml @@ -3,7 +3,7 @@ services: build: context: .. dockerfile: ${PWD:-.}/../saw/Dockerfile - entrypoint: ["cp", "/usr/local/bin/saw", "/usr/local/bin/abc", "/usr/local/bin/yices", "/usr/local/bin/z3-4.8.8", "/saw-bin"] + entrypoint: ["cp", "/usr/local/bin/saw", "/usr/local/bin/abc", "/usr/local/bin/yices", "/usr/local/bin/yices-smt2", "/usr/local/bin/z3-4.8.8", "/saw-bin"] user: root volumes: - ${PWD:-}/bin:/saw-bin:rw diff --git a/s2nTests/scripts/s2n-entrypoint.sh b/s2nTests/scripts/s2n-entrypoint.sh index 971a147d8d..54b77b6ba3 100755 --- a/s2nTests/scripts/s2n-entrypoint.sh +++ b/s2nTests/scripts/s2n-entrypoint.sh @@ -9,10 +9,22 @@ 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/install_default_dependencies.sh + +# override SAW_INSTALL_DIR so the downloaded saw goes somewhere else +SAW=false SAW_INSTALL_DIR=tmp-saw ./codebuild/bin/install_default_dependencies.sh + +# These copies use the SAW_INSTALL_DIR from s2n_setup_env.sh. +# The /saw-bin they copy from is provided by ../docker-compose.yml. cp /saw-bin/saw "$SAW_INSTALL_DIR"/bin/saw cp /saw-bin/abc "$SAW_INSTALL_DIR"/bin/abc +cp /saw-bin/yices "$SAW_INSTALL_DIR"/bin/yices +cp /saw-bin/yices-smt2 "$SAW_INSTALL_DIR"/bin/yices-smt2 +cp /saw-bin/z3-4.8.8 "$SAW_INSTALL_DIR"/bin/z3 "$SAW_INSTALL_DIR"/bin/saw --version +"$SAW_INSTALL_DIR"/bin/abc -h || true # exits 1 on -h, sigh +"$SAW_INSTALL_DIR"/bin/yices --version +"$SAW_INSTALL_DIR"/bin/z3 --version + export CFLAGS=-Wno-error=array-parameter export CLANG=clang export LLVMLINK=llvm-link From 38c738319633ef01e7bea307d820fd062ce13d99 Mon Sep 17 00:00:00 2001 From: David Holland Date: Fri, 28 Mar 2025 00:03:02 +0000 Subject: [PATCH 7/9] s2ntests: use ubuntu clang-14 instead of an LLVM 10 binary The binary distribution seems to be linked against ncurses 5, which is no longer available in ubuntu 24.04. Why a compiler needs to be linked against curses, IDK. Applies to the awslc and blst containers, but not (yet?) the default s2n container as that uses a different clang that might or might not be runnable. Provisional. --- s2nTests/docker/awslc.dockerfile | 16 ++++++++++++---- s2nTests/docker/blst.dockerfile | 16 ++++++++++++---- 2 files changed, 24 insertions(+), 8 deletions(-) diff --git a/s2nTests/docker/awslc.dockerfile b/s2nTests/docker/awslc.dockerfile index 4458052aa0..b0b7420f85 100644 --- a/s2nTests/docker/awslc.dockerfile +++ b/s2nTests/docker/awslc.dockerfile @@ -1,14 +1,22 @@ FROM ubuntu:24.04 RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections -RUN apt-get update && apt-get install -y curl wget unzip git cmake golang python3-pip libncurses6 libtinfo-dev quilt file +RUN apt-get update && apt-get install -y curl wget unzip git cmake golang python3-pip libncurses6 libtinfo-dev quilt file clang-14 # FUTURE: Apparently you're now supposed to install a venv and not try # to use pip to install system-wide packages. --break-system-packages # is probably ok as a workaround here but it wouldn't surprise me if # it disappeared after a while. RUN pip3 install --break-system-packages 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 + +# This doesn't run any more on ubuntu 24.04 (it's linked to ncurses 5) +# so we're going to install clang-14 (the oldest in said ubuntu) instead +# and hope it works. +# +#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 + +# symlink clang -> clang-14 for all the clang bins +RUN (cd /usr/bin && ls *-14 | sed 's/-14$//' | awk '{ printf "ln -s %s-14 %s\n", $1, $1 }' | sh) # The commit we check out is now the head of the saw-test-runs branch, # because we added that commit (and branch) specifically to fix up diff --git a/s2nTests/docker/blst.dockerfile b/s2nTests/docker/blst.dockerfile index 25a9dbfc0d..bdfe997fcc 100644 --- a/s2nTests/docker/blst.dockerfile +++ b/s2nTests/docker/blst.dockerfile @@ -1,14 +1,22 @@ FROM ubuntu:24.04 RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections -RUN apt-get update && apt-get install -y curl wget unzip git cmake golang python3-pip libncurses6 libtinfo-dev quilt file +RUN apt-get update && apt-get install -y curl wget unzip git cmake golang python3-pip libncurses6 libtinfo-dev quilt file clang-14 # FUTURE: Apparently you're now supposed to install a venv and not try # to use pip to install system-wide packages. --break-system-packages # is probably ok as a workaround here but it wouldn't surprise me if # it disappeared after a while. RUN pip3 install --break-system-packages 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 + +# This doesn't run any more on ubuntu 24.04 (it's linked to ncurses 5) +# so we're going to install clang-14 (the oldest in said ubuntu) instead +# and hope it works. +# +#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 + +# symlink clang -> clang-14 for all the clang bins +RUN (cd /usr/bin && ls *-14 | sed 's/-14$//' | awk '{ printf "ln -s %s-14 %s\n", $1, $1 }' | sh) # The commit we check out is the head of the main branch. # From 09d90872bde823196a5adcb050cc9aaaf2d9e050 Mon Sep 17 00:00:00 2001 From: David Holland Date: Fri, 28 Mar 2025 18:32:28 -0400 Subject: [PATCH 8/9] CI: disable the awslc run. See #2273 and #1094. --- .github/workflows/ci.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index dca6715b32..4f4fe3812b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -885,7 +885,8 @@ jobs: - bike - tls - hmac-failure - - awslc + # 20250328: disabled temporarily because it now tickles #1094 (see #2273) + # - awslc - blst os: [ubuntu-24.04] ghc: ["9.4.8"] From a6aea1ca8f67151470d95c570929aaf2ae42faea Mon Sep 17 00:00:00 2001 From: David Holland Date: Mon, 31 Mar 2025 17:31:36 -0400 Subject: [PATCH 9/9] s2ntests: note in README that awslc is currently disabled in the CI. While passing through, note a couple of the other recent maintenance concerns as well. --- s2nTests/README.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/s2nTests/README.md b/s2nTests/README.md index d2a0234d2b..01e6b15a37 100644 --- a/s2nTests/README.md +++ b/s2nTests/README.md @@ -17,3 +17,16 @@ Running `make ` on one of the following targets will use the `saw` binar - `blst` `make` alone with no targets will run all of the proofs. + +## Ongoing maintenance concerns + +- Currently the awslc proof fails because it tickles #1094. + It's consequently disabled in the CI run until that gets fixed; see #2273. + +- Currently the tls proof contains invalid SAWScript that is accepted with a + warning in SAW 1.3 but will be rejected eventually. + This will need to be fixed. + See #2169. + +- The pending deprecation of llvm_struct per #2159 will eventually require + upstream updates to a number of the proofs.