WIP: Support GHC 9.10

GaloisInc · Feb 13, 2025 · 2eb5a94 · 2eb5a94
1 parent 50d1550
commit 2eb5a94
Show file tree

Hide file tree

Showing 20 changed files with 48 additions and 27 deletions.
diff --git a/.github/Dockerfile-crux-llvm b/.github/Dockerfile-crux-llvm
@@ -1,9 +1,11 @@
 # If you update this version number, make sure to update the value of
 # LINUX_LLVM_VER in .github/ci.sh (in the install_llvm() function).
 ARG LLVM_VER=14
+ARG GHC_VER=9.6.5
 
 FROM ubuntu:22.04 AS build
 ARG LLVM_VER
+ARG GHC_VER
 
 RUN apt-get update && \
     apt-get install -y \
@@ -27,7 +29,7 @@ ADD crux ${CRUX_BUILD_DIR}/crux
 ADD crux-llvm ${CRUX_BUILD_DIR}/crux-llvm
 ADD dependencies ${CRUX_BUILD_DIR}/dependencies
 ADD .github/cabal.project.crux-llvm ${CRUX_BUILD_DIR}/cabal.project
-ADD cabal.GHC-9.4.8.config ${CRUX_BUILD_DIR}/cabal.project.freeze
+ADD cabal.GHC-${GHC_VER}.config ${CRUX_BUILD_DIR}/cabal.project.freeze
 # Workaround until we have a more recent LLVM build available
 RUN cp ${CRUX_BUILD_DIR}/crux-llvm/c-src/libcxx-7.1.0.bc ${CRUX_BUILD_DIR}/crux-llvm/c-src/libcxx-${LLVM_VER}.0.0.bc
 
@@ -56,8 +58,8 @@ RUN mkdir -p /home/crux-llvm/.local/bin && \
 RUN mkdir -p /home/crux-llvm/.ghcup && \
     ghcup --version && \
     ghcup install cabal 3.10.3.0 && \
-    ghcup install ghc 9.4.8 && \
-    ghcup set ghc 9.4.8
+    ghcup install ghc ${GHC_VER} && \
+    ghcup set ghc ${GHC_VER}
 
 WORKDIR ${CRUX_BUILD_DIR}
 RUN cabal v2-update && \

diff --git a/.github/Dockerfile-crux-mir b/.github/Dockerfile-crux-mir
@@ -2,10 +2,12 @@
 # .github/workflows/crux-mir-build.yml
 ARG RUST_TOOLCHAIN="nightly-2023-01-23"
 ARG CRUX_BUILD_DIR=/crux-mir/build
+ARG GHC_VER=9.6.5
 
 FROM ubuntu:22.04 AS build
 ARG RUST_TOOLCHAIN
 ARG CRUX_BUILD_DIR
+ARG GHC_VER
 
 RUN apt-get update && \
     apt-get install -y \
@@ -26,7 +28,7 @@ ADD crux ${CRUX_BUILD_DIR}/crux
 ADD crux-mir ${CRUX_BUILD_DIR}/crux-mir
 ADD dependencies ${CRUX_BUILD_DIR}/dependencies
 ADD .github/cabal.project.crux-mir ${CRUX_BUILD_DIR}/cabal.project
-ADD cabal.GHC-9.4.8.config ${CRUX_BUILD_DIR}/cabal.project.freeze
+ADD cabal.GHC-${GHC_VER}.config ${CRUX_BUILD_DIR}/cabal.project.freeze
 
 RUN useradd -m crux-mir && chown -R crux-mir:crux-mir /crux-mir
 USER crux-mir
@@ -56,8 +58,8 @@ RUN mkdir -p /home/crux-mir/.local/bin && \
 RUN mkdir -p /home/crux-mir/.ghcup && \
     ghcup --version && \
     ghcup install cabal 3.10.3.0 && \
-    ghcup install ghc 9.4.8 && \
-    ghcup set ghc 9.4.8
+    ghcup install ghc ${GHC_VER} && \
+    ghcup set ghc ${GHC_VER}
 
 WORKDIR ${CRUX_BUILD_DIR}/crux-mir
 RUN ./translate_libs.sh

diff --git a/.github/workflows/crucible-go-build.yml b/.github/workflows/crucible-go-build.yml
@@ -28,14 +28,14 @@ jobs:
       matrix:
         os: [ubuntu-22.04]
         cabal: ["3.10.3.0"]
-        ghc: ["9.4.8", "9.6.5", "9.8.2"]
+        ghc: ["9.6.5", "9.8.2", "9.10.1"]
         include:
           - os: macos-14
             cabal: 3.10.3.0
-            ghc: 9.8.2
+            ghc: 9.10.1
           - os: windows-2019
             cabal: 3.10.3.0
-            ghc: 9.8.2
+            ghc: 9.10.1
     name: crucible-go - GHC v${{ matrix.ghc }} - ${{ matrix.os }}
     steps:
       - uses: actions/checkout@v4
@@ -93,6 +93,7 @@ jobs:
             9.4.8) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
             9.6.5) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
             9.8.2) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
+            9.10.1) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
             *)     GHC_NIXPKGS=github:nixos/nixpkgs/21.11 ;;
           esac
           echo NS="nix shell ${GHC_NIXPKGS}#cabal-install ${GHC_NIXPKGS}#${GHC} nixpkgs#gmp nixpkgs#zlib nixpkgs#zlib.dev" >> $GITHUB_ENV

diff --git a/.github/workflows/crucible-jvm-build.yml b/.github/workflows/crucible-jvm-build.yml
@@ -28,14 +28,14 @@ jobs:
       matrix:
         os: [ubuntu-22.04]
         cabal: ["3.10.3.0"]
-        ghc: ["9.4.8", "9.6.5", "9.8.2"]
+        ghc: ["9.6.5", "9.8.2", "9.10.1"]
         include:
           - os: macos-14
             cabal: 3.10.3.0
-            ghc: 9.8.2
+            ghc: 9.10.1
           - os: windows-2019
             cabal: 3.10.3.0
-            ghc: 9.8.2
+            ghc: 9.10.1
     name: crucible-jvm - GHC v${{ matrix.ghc }} - ${{ matrix.os }}
     steps:
       - uses: actions/checkout@v4
@@ -93,6 +93,7 @@ jobs:
             9.4.8) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
             9.6.5) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
             9.8.2) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
+            9.10.1) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
             *)     GHC_NIXPKGS=github:nixos/nixpkgs/21.11 ;;
           esac
           echo NS="nix shell ${GHC_NIXPKGS}#cabal-install ${GHC_NIXPKGS}#${GHC} nixpkgs#gmp nixpkgs#zlib nixpkgs#zlib.dev" >> $GITHUB_ENV

diff --git a/.github/workflows/crucible-wasm-build.yml b/.github/workflows/crucible-wasm-build.yml
@@ -28,14 +28,14 @@ jobs:
       matrix:
         os: [ubuntu-22.04]
         cabal: ["3.10.3.0"]
-        ghc: ["9.4.8", "9.6.5", "9.8.2"]
+        ghc: ["9.6.5", "9.8.2", "9.10.1"]
         include:
           - os: macos-14
             cabal: 3.10.3.0
-            ghc: 9.8.2
+            ghc: 9.10.1
           - os: windows-2019
             cabal: 3.10.3.0
-            ghc: 9.8.2
+            ghc: 9.10.1
     name: crucible-wasm - GHC v${{ matrix.ghc }} - ${{ matrix.os }}
     steps:
       - uses: actions/checkout@v4
@@ -90,9 +90,9 @@ jobs:
         run: |
           GHC=haskell.compiler.ghc$(echo ${{ matrix.ghc }} | sed -e s,\\.,,g)
           case ${{ matrix.ghc }} in
-            9.4.8) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
             9.6.5) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
             9.8.2) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
+            9.10.1) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
             *)     GHC_NIXPKGS=github:nixos/nixpkgs/21.11 ;;
           esac
           echo NS="nix shell ${GHC_NIXPKGS}#cabal-install ${GHC_NIXPKGS}#${GHC} nixpkgs#gmp nixpkgs#zlib nixpkgs#zlib.dev" >> $GITHUB_ENV

diff --git a/.github/workflows/crux-llvm-build.yml b/.github/workflows/crux-llvm-build.yml
@@ -65,17 +65,17 @@ jobs:
       matrix:
         os: [ubuntu-22.04]
         cabal: ["3.10.3.0"]
-        ghc: ["9.4.8", "9.6.5", "9.8.2"]
+        ghc: ["9.6.5", "9.8.2", "9.10.1"]
         include:
           - os: ubuntu-20.04
             cabal: 3.10.3.0
-            ghc: 9.4.8
+            ghc: 9.10.1
           - os: macos-14
             cabal: 3.10.3.0
-            ghc: 9.4.8
+            ghc: 9.10.1
           - os: windows-2019
             cabal: 3.10.3.0
-            ghc: 9.4.8
+            ghc: 9.10.1
     name: crux-llvm - GHC v${{ matrix.ghc }} - ${{ matrix.os }}
     steps:
       - uses: actions/checkout@v4
@@ -133,6 +133,7 @@ jobs:
             9.4.8) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
             9.6.5) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
             9.8.2) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
+            9.10.1) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
             *)     GHC_NIXPKGS=github:nixos/nixpkgs/21.11 ;;
           esac
           echo NS="nix shell ${GHC_NIXPKGS}#cabal-install ${GHC_NIXPKGS}#${GHC} nixpkgs#gmp nixpkgs#zlib nixpkgs#zlib.dev" >> $GITHUB_ENV

diff --git a/.github/workflows/crux-mir-build.yml b/.github/workflows/crux-mir-build.yml
@@ -139,6 +139,7 @@ jobs:
             9.4.8) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
             9.6.5) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
             9.8.2) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
+            9.10.1) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
             *)     GHC_NIXPKGS=github:nixos/nixpkgs/21.11 ;;
           esac
           echo NS="nix shell ${GHC_NIXPKGS}#cabal-install ${GHC_NIXPKGS}#${GHC} nixpkgs#gmp nixpkgs#zlib nixpkgs#zlib.dev" >> $GITHUB_ENV

diff --git a/cabal.project b/cabal.project
@@ -4,6 +4,10 @@
 --
 -- export PATH=$PWD/dist-newstyle/build/x86_64-linux/ghc-7.10.3/hpb-0.1.1/c/hpb/build/hpb:$PATH
 
+-- TODO: https://github.com/travitch/itanium-abi/pull/15
+allow-newer: itanium-abi:text
+allow-newer: boomerang:template-haskell
+
 packages:
   crucible/
   crucible-cli/

diff --git a/crucible-llvm/CHANGELOG.md b/crucible-llvm/CHANGELOG.md
@@ -1,5 +1,6 @@
 # next -- TBA
 
+* Add support for GHC 9.10
 * Fix a bug in which the memory model would panic when attempting to unpack
   constant string literals.
 

diff --git a/crucible-llvm/crucible-llvm.cabal b/crucible-llvm/crucible-llvm.cabal
@@ -33,7 +33,7 @@ common bldflags
 library
   import: bldflags
   build-depends:
-    base >= 4.13 && < 4.20,
+    base >= 4.13 && < 4.21,
     attoparsec,
     bv-sized >= 1.0.0,
     bytestring,

diff --git a/crucible-symio/CHANGELOG.md b/crucible-symio/CHANGELOG.md
@@ -1,5 +1,9 @@
 # Revision history for crucible-symio
 
+# next
+
+* Add support for GHC 9.10
+
 ## 0.1.1 -- 2024-08-30
 
 * Add support for GHC 9.8

diff --git a/crucible-symio/crucible-symio.cabal b/crucible-symio/crucible-symio.cabal
@@ -21,7 +21,7 @@ source-repository head
   subdir:   crucible-symio
 
 common shared
-  build-depends:       base >=4.12 && <4.20,
+  build-depends:       base >=4.12 && <4.21,
                        aeson,
                        bv-sized,
                        bytestring,

diff --git a/crucible/CHANGELOG.md b/crucible/CHANGELOG.md
@@ -1,5 +1,6 @@
 # next -- TBA
 
+* Add support for GHC 9.10
 * Add support for Bitwuzla as an online SMT solver backend.
 * Add a function `ppTypeRepr` to `Lang.Crucible.Types` for pretty-printing
   `TypeRepr`s. Modify the `Pretty` instance to use this function.

diff --git a/crucible/crucible.cabal b/crucible/crucible.cabal
@@ -45,7 +45,7 @@ library
   import: bldflags
   build-depends:
     async,
-    base >= 4.13 && < 4.20,
+    base >= 4.13 && < 4.21,
     bimap,
     bv-sized >= 1.0.0 && < 1.1,
     containers >= 0.5.9.0,

diff --git a/crucible/src/Lang/Crucible/Utils/BitSet.hs b/crucible/src/Lang/Crucible/Utils/BitSet.hs
@@ -35,7 +35,7 @@ import Data.Bits
 import Data.Word
 import Data.Hashable
 import qualified Data.List as List
-import Prelude hiding (null, foldr, foldl)
+import Prelude hiding (null, foldr, foldl, foldl')
 
 newtype BitSet a = BitSet { getBits :: Integer }
  deriving (Show, Eq, Ord)

diff --git a/crux-llvm/CHANGELOG.md b/crux-llvm/CHANGELOG.md
@@ -1,5 +1,6 @@
 # next -- TBA
 
+* Add support for GHC 9.10.
 * Add support for the Bitwuzla SMT solver in the test suite.
 * Add `--debug` option for starting the Crucible debugger.
 

diff --git a/crux-llvm/crux-llvm.cabal b/crux-llvm/crux-llvm.cabal
@@ -55,7 +55,7 @@ common bldflags
                -Wincomplete-uni-patterns
   ghc-prof-options: -O2
   default-language: Haskell2010
-  build-depends:    base >= 4.8 && < 4.20
+  build-depends:    base >= 4.8 && < 4.21
                   , bytestring
                   , containers
                   , crucible

diff --git a/crux-mir/CHANGELOG.md b/crux-mir/CHANGELOG.md
@@ -1,5 +1,6 @@
 # next -- TBA
 
+* Add support for GHC 9.10
 * Add `--debug` option for starting the Crucible debugger.
 
 # 0.9 -- 2024-08-30

diff --git a/crux/CHANGELOG.md b/crux/CHANGELOG.md
@@ -1,5 +1,6 @@
 # next -- TBA
 
+* Add support for GHC 9.10
 * Add support for the Bitwuzla SMT solver.
 * Add `--debug` option for starting the Crucible debugger.
 * For the sake of the `--debug` flag, Crux now depends on the

diff --git a/uc-crux-llvm/uc-crux-llvm.cabal b/uc-crux-llvm/uc-crux-llvm.cabal
@@ -185,7 +185,7 @@ library
   build-depends:
     aeson,
     async,
-    base >= 4.8 && < 4.20,
+    base >= 4.8 && < 4.21,
     bv-sized,
     bytestring,
     containers,
@@ -217,7 +217,7 @@ executable uc-crux-llvm
   hs-source-dirs: exe
 
   build-depends:
-    base >= 4.8 && < 4.20,
+    base >= 4.8 && < 4.21,
     uc-crux-llvm
 
   ghc-options: -threaded