GaloisInc · sauclovian-g · Mar 31, 2025 · Mar 27, 2025 · Mar 27, 2025 · Mar 27, 2025
diff --git 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
@@ -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
 
@@ -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
@@ -885,9 +885,10 @@ jobs:
           - bike
           - tls
           - hmac-failure
-          - awslc
+          # 20250328: disabled temporarily because it now tickles #1094 (see #2273)
+          # - awslc
           - blst
-        os: [ubuntu-22.04]
+        os: [ubuntu-24.04]
         ghc: ["9.4.8"]
     steps:
       - uses: actions/checkout@v4
@@ -941,7 +942,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 +974,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
@@ -1,9 +1,10 @@
-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
+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
 

diff --git 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 <target>` on one of the following targets will use the `saw` binary in `bin/` to run the respective proof:
@@ -17,3 +17,16 @@ Running `make <target>` 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.
diff --git 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/docker/awslc.dockerfile b/s2nTests/docker/awslc.dockerfile
@@ -1,10 +1,22 @@
-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
-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 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
+
+# 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
@@ -1,10 +1,22 @@
-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
-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 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
+
+# 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.
 #

diff --git 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 && \
@@ -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/*

diff --git 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

diff --git 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
@@ -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 /