Merge branch 'master' into sygus2

GaloisInc · Feb 18, 2024 · 7617969 · 7617969
2 parents 08b51b6 + c5dc719
commit 7617969
Show file tree

Hide file tree

Showing 72 changed files with 577 additions and 760 deletions.
diff --git a/.github/Dockerfile-crux-llvm b/.github/Dockerfile-crux-llvm
@@ -17,7 +17,10 @@ ENV LANGUAGE en_US:en
 ENV LC_ALL en_US.UTF-8
 
 WORKDIR /usr/local/bin
-RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220902/ubuntu-22.04-bin.zip"
+# The URL here is based on the same logic used to specify BUILD_TARGET_OS and
+# BUILD_TARGET_ARCH in `.github/workflow/crux-llvm-build.yml`, but specialized
+# to x86-64 Ubuntu.
+RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20240212/ubuntu-22.04-X64-bin.zip"
 RUN unzip solvers.zip && rm solvers.zip && chmod +x *
 
 ENV PATH=/root/ghcup-download/bin:/root/.ghcup/bin:$PATH

diff --git a/.github/Dockerfile-crux-mir b/.github/Dockerfile-crux-mir
@@ -27,7 +27,10 @@ RUN apt-get update && \
 COPY --from=mir_json /usr/local/cargo /usr/local/cargo
 COPY --from=mir_json /usr/local/rustup /usr/local/rustup
 WORKDIR /usr/local/bin
-RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20220902/ubuntu-22.04-bin.zip"
+# The URL here is based on the same logic used to specify BUILD_TARGET_OS and
+# BUILD_TARGET_ARCH in `.github/workflow/crux-mir-build.yml`, but specialized
+# to x86-64 Ubuntu.
+RUN curl -o solvers.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20240212/ubuntu-22.04-X64-bin.zip"
 RUN unzip solvers.zip && rm solvers.zip && chmod +x *
 
 ENV CARGO_HOME=/usr/local/cargo

diff --git a/.github/ci.sh b/.github/ci.sh
@@ -65,8 +65,12 @@ test() {
 install_llvm() {
   if [[ "$RUNNER_OS" = "Linux" ]]; then
     sudo apt-get update -q && sudo apt-get install -y clang-12 llvm-12-tools
+    echo "LLVM_LINK=llvm-link-12" >> "$GITHUB_ENV"
+    echo "LLVM_AS=llvm-as-12" >> "$GITHUB_ENV"
+    echo "CLANG=clang-12" >> "$GITHUB_ENV"
   elif [[ "$RUNNER_OS" = "macOS" ]]; then
     brew install llvm@12
+    echo "$(brew --prefix)/opt/llvm@12/bin" >> "$GITHUB_PATH"
   elif [[ "$RUNNER_OS" = "Windows" ]]; then
     choco install llvm
   else
@@ -76,7 +80,7 @@ install_llvm() {
 }
 
 install_solvers() {
-  (cd $BIN && curl -o bins.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/$SOLVER_PKG_VERSION/$BUILD_TARGET_OS-bin.zip" && unzip -o bins.zip && rm bins.zip)
+  (cd $BIN && curl -o bins.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/$SOLVER_PKG_VERSION/$BUILD_TARGET_OS-$BUILD_TARGET_ARCH-bin.zip" && unzip -o bins.zip && rm bins.zip)
   cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT
   chmod +x $BIN/*
   export PATH=$BIN:$PATH
@@ -111,7 +115,7 @@ setup_dist() {
 
 zip_dist() {
   : "${VERSION?VERSION is required as an environment variable}"
-  pkgname="${pkgname:-"$1-$VERSION-$OS_TAG-x86_64"}"
+  pkgname="${pkgname:-"$1-$VERSION-$OS_TAG-$ARCH_TAG"}"
   mv dist "$pkgname"
   tar -czf "$pkgname".tar.gz "$pkgname"
   rm -rf dist

diff --git a/.github/workflows/README.md b/.github/workflows/README.md
@@ -5,16 +5,19 @@ on CI, whose CI configurations are located here. We use the following
 conventions when picking with operating systems to test:
 
 * For each project, we test the latest LTS release of Ubuntu on the three most
-  recent stable releases of GHC. In the case of `crux-llvm-build.yml`, we also
-  test some older versions of GHC.
+  recent stable releases of GHC.
 * In addition, we also test the previous LTS release of Ubuntu on the
-  `crux-llvm-build.yml` workflow, but only using the latest supported version
-  of GHC.
-* For each project, we test macOS and Windows only using the latest
-  supported version of GHC. This is because the turnaround time for macOS and
-  Windows builders on GitHub Actions is longer, so we try to avoid
-  bottlenecking CI workflows on these operating systems.
+  `crux-llvm-build.yml` and `crux-mir-build.yml` workflows, but only using a
+  single version of GHC.
+* For each project, we test macOS and Windows only using a single version of
+  GHC. This is because the turnaround time for macOS and Windows builders on
+  GitHub Actions is longer, so we try to avoid bottlenecking CI workflows on
+  these operating systems.
 
-  Note that we do not currently run LLVM-related tests on Windows as it is not
-  straightforward to obtain Windows builds of LLVM that include all of the
-  developer tools that we need, such as `llvm-link` and `llvm-as`.
+  Note that:
+
+  * We do not currently run LLVM-related tests on Windows, as it is not
+    straightforward to obtain Windows builds of LLVM that include all of the
+    developer tools that we need, such as `llvm-link` and `llvm-as`.
+  * We do not currently run MIR-related tests on Windows, as it is not
+    straightforward to install `mir-json` on Windows.
diff --git a/.github/workflows/crucible-go-build.yml b/.github/workflows/crucible-go-build.yml
@@ -42,7 +42,7 @@ jobs:
         with:
           submodules: true
 
-      - uses: haskell/actions/setup@v2
+      - uses: haskell-actions/setup@v2
         id: setup-haskell
         with:
           ghc-version: ${{ matrix.ghc }}
@@ -78,8 +78,9 @@ jobs:
       - shell: bash
         run: .github/ci.sh install_system_deps
         env:
-          SOLVER_PKG_VERSION: "snapshot-20220902"
+          SOLVER_PKG_VERSION: "snapshot-20240212"
           BUILD_TARGET_OS: ${{ matrix.os }}
+          BUILD_TARGET_ARCH: ${{ runner.arch }}
 
       - name: Setup Environment Vars
         if: runner.os == 'Linux'

diff --git a/.github/workflows/crucible-jvm-build.yml b/.github/workflows/crucible-jvm-build.yml
@@ -42,7 +42,7 @@ jobs:
         with:
           submodules: true
 
-      - uses: haskell/actions/setup@v2
+      - uses: haskell-actions/setup@v2
         id: setup-haskell
         with:
           ghc-version: ${{ matrix.ghc }}
@@ -78,8 +78,9 @@ jobs:
       - shell: bash
         run: .github/ci.sh install_system_deps
         env:
-          SOLVER_PKG_VERSION: "snapshot-20220902"
+          SOLVER_PKG_VERSION: "snapshot-20240212"
           BUILD_TARGET_OS: ${{ matrix.os }}
+          BUILD_TARGET_ARCH: ${{ runner.arch }}
 
       - name: Setup Environment Vars
         if: runner.os == 'Linux'

diff --git a/.github/workflows/crucible-wasm-build.yml b/.github/workflows/crucible-wasm-build.yml
@@ -42,7 +42,7 @@ jobs:
         with:
           submodules: true
 
-      - uses: haskell/actions/setup@v2
+      - uses: haskell-actions/setup@v2
         id: setup-haskell
         with:
           ghc-version: ${{ matrix.ghc }}
@@ -78,8 +78,9 @@ jobs:
       - shell: bash
         run: .github/ci.sh install_system_deps
         env:
-          SOLVER_PKG_VERSION: "snapshot-20220902"
+          SOLVER_PKG_VERSION: "snapshot-20240212"
           BUILD_TARGET_OS: ${{ matrix.os }}
+          BUILD_TARGET_ARCH: ${{ runner.arch }}
 
       - name: Setup Environment Vars
         if: runner.os == 'Linux'

diff --git a/.github/workflows/crux-llvm-build.yml b/.github/workflows/crux-llvm-build.yml
@@ -31,7 +31,7 @@ jobs:
       event-tag: ${{ steps.config.outputs.tag }}
       event-schedule: ${{ steps.config.outputs.schedule }}
       publish: ${{ steps.config.outputs.publish }}
-      release: ${{ steps.env.outputs.release }}
+      release: ${{ steps.config.outputs.release }}
       retention-days: ${{ steps.config.outputs.retention-days }}
     steps:
       - uses: actions/checkout@v2
@@ -52,7 +52,7 @@ jobs:
           .github/ci.sh output tag $EVENT_TAG
           .github/ci.sh output schedule $EVENT_SCHEDULE
           .github/ci.sh output publish $({ $EVENT_TAG || $EVENT_SCHEDULE; } && echo true || echo false)
-          .github/ci.sh output release $([[ "refs/heads/release-$(.github/ci.sh crux_llvm_ver)" == "${{ github.event.ref }}" ]] && echo true || echo false)
+          .github/ci.sh output release $([[ "refs/heads/release-crux-$(.github/ci.sh crux_llvm_ver)" == "${{ github.event.ref }}" ]] && echo true || echo false)
           .github/ci.sh output retention-days $($RELEASE && echo 90 || echo 5)
 
   build:
@@ -67,13 +67,10 @@ jobs:
         cabal: ["3.10.1.0"]
         ghc: ["9.2.8", "9.4.5", "9.6.2"]
         include:
-          - os: ubuntu-22.04
-            cabal: 3.10.1.0
-            ghc: 8.10.7
           - os: ubuntu-20.04
             cabal: 3.10.1.0
-            ghc: 9.6.2
-          - os: macos-12
+            ghc: 9.2.8
+          - os: macos-14
             cabal: 3.10.1.0
             ghc: 9.2.8
           - os: windows-2019
@@ -85,7 +82,7 @@ jobs:
         with:
           submodules: true
 
-      - uses: haskell/actions/setup@v2
+      - uses: haskell-actions/setup@v2
         id: setup-haskell
         with:
           ghc-version: ${{ matrix.ghc }}
@@ -121,8 +118,9 @@ jobs:
       - shell: bash
         run: .github/ci.sh install_system_deps
         env:
-          SOLVER_PKG_VERSION: "snapshot-20220902"
+          SOLVER_PKG_VERSION: "snapshot-20240212"
           BUILD_TARGET_OS: ${{ matrix.os }}
+          BUILD_TARGET_ARCH: ${{ runner.arch }}
 
       - name: Setup Environment Vars
         if: runner.os == 'Linux'
@@ -186,93 +184,45 @@ jobs:
         run: .github/ci.sh test crucible-cli
 
       - shell: bash
-        name: Test crucible-symio (Linux)
+        name: Test crucible-symio
         run: cabal test pkg:crucible-symio
         if: runner.os == 'Linux'
 
       - shell: bash
-        name: Test crucible-llvm (Linux)
+        name: Test crucible-llvm
         run: .github/ci.sh test crucible-llvm
-        if: runner.os == 'Linux'
-        env:
-          LLVM_LINK: "llvm-link-12"
-          LLVM_AS: "llvm-as-12"
-          CLANG: "clang-12"
+        if: runner.os == 'Linux' || runner.os == 'macOS'
 
       - shell: bash
-        name: Test crucible-llvm-syntax (Linux)
+        name: Test crucible-llvm-syntax
         run: .github/ci.sh test crucible-llvm-syntax
         if: runner.os == 'Linux'
 
       - shell: bash
-        name: Test crucible-llvm-cli (Linux)
+        name: Test crucible-llvm-cli
         run: .github/ci.sh test crucible-llvm-cli
         if: runner.os == 'Linux'
 
       - shell: bash
-        name: Test crux-llvm (Linux)
+        name: Test crux-llvm
         run: .github/ci.sh test crux-llvm
-        if: runner.os == 'Linux'
-        env:
-          LLVM_LINK: "llvm-link-12"
-          CLANG: "clang-12"
+        if: runner.os == 'Linux' || runner.os == 'macOS'
 
       - shell: bash
         name: Test uc-crux-llvm (Linux)
         run: .github/ci.sh test uc-crux-llvm
         if: matrix.os == 'ubuntu-22.04'
-        env:
-          LLVM_LINK: "llvm-link-12"
-          CLANG: "clang-12"
-
-      - shell: bash
-        name: Install LLVM-11 for MacOS
-        if: runner.os == 'macOS'
-        run: |
-          LLVM_TAR=https://github.com/llvm/llvm-project/releases/download/llvmorg-11.0.0/clang+llvm-11.0.0-x86_64-apple-darwin.tar.xz
-          curl -sSL $LLVM_TAR -o llvm.tar.xz && tar xzf llvm.tar.xz && mv clang+llvm-* llvm
-          echo "#!/usr/bin/env bash" > llvm/bin/clang-withIncl
-          echo "clang -I${{ github.workspace }}/llvm/include -I${{ github.workspace }}/llvm/include/c++/v1" >> llvm/bin/clang-withIncl
-          chmod +x llvm/bin/clang-withIncl
-          echo "$PWD/llvm/bin" >> $GITHUB_PATH
-
-      - uses: actions/cache@v2
-        name: Cache LLVM-11
-        if: runner.os == 'macOS'
-        with:
-          path: ${{ github.workspace }}/llvm
-          key: llvm-11.0.0
-          restore-keys: llvm-11.0.0
-
-      - shell: bash
-        name: Test crucible-llvm (macOS)
-        run: .github/ci.sh test crucible-llvm
-        if: runner.os == 'macOS'
-        env:
-          LLVM_LINK: "${{ github.workspace }}/llvm/bin/llvm-link"
-          LLVM_AS: "${{ github.workspace }}/llvm/bin/llvm-as"
-          CLANG: "${{ github.workspace }}/llvm/bin/clang"
-
-        # We disable the crux-llvm test suite on macOS due to
-        # https://github.com/GaloisInc/crucible/issues/885 and
-        # https://github.com/GaloisInc/crucible/issues/999
-      - shell: bash
-        name: Test crux-llvm (macOS)
-        run: .github/ci.sh test crux-llvm
-        if: runner.os == 'macOS' && false
-        env:
-          LLVM_LINK: "${{ github.workspace }}/llvm/bin/llvm-link"
-          CLANG: "${{ github.workspace }}/llvm/bin/clang-withIncl"
 
       - name: Create binary artifact
         shell: bash
         run: |
-          NAME="crux-llvm-${{ needs.config.outputs.crux-llvm-version }}-${{ matrix.os }}-x86_64"
+          NAME="crux-llvm-${{ needs.config.outputs.crux-llvm-version }}-${{ matrix.os }}-${{ runner.arch }}"
           echo "NAME=$NAME" >> $GITHUB_ENV
           .github/ci.sh bundle_crux_llvm_files
         if: github.repository == 'GaloisInc/crucible'
         env:
           OS_TAG: ${{ matrix.os }}
+          ARCH_TAG: ${{ runner.arch }}
           VERSION: ${{ needs.config.outputs.crux-llvm-version }}
 
       - name: Sign binary artifact
@@ -369,9 +319,9 @@ jobs:
           docker push ${{ matrix.image }}:nightly
 
       - if: needs.config.outputs.release == 'true'
-        name: ${{ matrix.image }}:${{ needs.config.outputs.version }}
+        name: ${{ matrix.image }}:${{ needs.config.outputs.crux-llvm-version }}
         run: |
-          docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:${{ needs.config.outputs.version }}
-          docker push ${{ matrix.image }}:${{ needs.config.outputs.version }}
+          docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:${{ needs.config.outputs.crux-llvm-version }}
+          docker push ${{ matrix.image }}:${{ needs.config.outputs.crux-llvm-version }}
           docker tag ${{ matrix.image }}:$COMMON_TAG ${{ matrix.image }}:latest
           docker push ${{ matrix.image }}:latest