Initial portion of GHC 9.10 and 9.12 support

.github/workflows/ci.yml

@@ -85,7 +85,7 @@ jobs:
       fail-fast: false
       matrix:
         os: [ubuntu-24.04]
-        cabal: ["3.10.3.0"]
+        cabal: ["3.14.1.0"]
         ghc: ["9.4.8", "9.6.7", "9.8.4"]
         haddock: [true]
         run-tests: [true]
@@ -96,14 +96,14 @@ jobs:
           # tests with the newest LTS release, we won't bother testing this one.
           - os: ubuntu-22.04
             ghc: "9.6.7"
-            cabal: "3.10.3.0"
+            cabal: "3.14.1.0"
             haddock: false
             run-tests: false
             hpc: false
           # Include one job with HPC enabled
           - os: ubuntu-24.04
             ghc: "9.6.7"
-            cabal: "3.10.3.0"
+            cabal: "3.14.1.0"
             haddock: false
             run-tests: true
             hpc: true

compute-coverage.sh

@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-set -Eeuxo pipefail
+set -uo pipefail
 
 # This script generates an HTML coverage report for any tests run within the
 # saw-script repo. It uses HPC, which is a tool in the standard GHC
@@ -16,9 +16,18 @@ set -Eeuxo pipefail
 # Combine .tix files
 # Avoid tripping on an existing all.tix from a prior run
 SUM_TIX="all.tix"
+TIXFILES=$(find . ! -path ./all.tix -name "*.tix" -print | sort)
+
+echo "Running: hpc sum --output=$SUM_TIX ..."
 hpc sum --output=$SUM_TIX --union --exclude=Main \
         --exclude=SAWVersion.GitRev --exclude=SAWVersion.GitRevAux \
-        $(find . ! -path ./all.tix -name "*.tix" -print)
+        $TIXFILES
+if [ $? != 0 ]; then
+    echo "TIXFILES was:"
+    echo "$TIXFILES" | awk '{ printf "   %s\n", $0 }'
+    echo "Failed. Help?" 1>&2
+    exit 1
+fi
 
 # Find the HPC dir, and don't trip on old versions after a version bump.
 # See saw-script #2114.
@@ -30,6 +39,11 @@ hpc sum --output=$SUM_TIX --union --exclude=Main \
 # -v0 (verbosity 0) prevents cabal from accidentally including extraneous
 # data (see saw-script #2103)
 SAW=$(cabal list-bin -v0 exe:saw)
+if [ $? != 0 ]; then
+    echo "cabal list-bin failed? help..." 1>&2
+    exit 1
+fi
+echo "SAW: $SAW"
 
 # Now what we want is the top-level build dir for the saw package.
 # As of when #2114 was merged, the path we were getting was:
@@ -61,6 +75,7 @@ SAW=$(cabal list-bin -v0 exe:saw)
 # difficult or fragile. Trying to figure $TARGET or $GHC would be
 # messy, but we still wouldn't need to do that.)
 BUILDDIR=$(echo "$SAW" | sed 's,/build/saw/saw$,,;s,/x/saw$,,')
+echo "BUILDDIR: $BUILDDIR"
 
 case "$BUILDDIR" in
     */saw-*.*) ;;
@@ -91,20 +106,31 @@ esac
 # hpc/vanilla/mix. The previous version of this code looked for a
 # single 'hpc' dir and then iterated through its hpc/vanilla/mix; here
 # what we'll do is just find all hpc/vanilla/mix/* dirs.
+#
+# As of #3252, we have moved to a newer Cabal version and that seems
+# to change the way hpc finds the mix files. The old Cabal version
+# wanted every top-level subdir of every hpc/vanilla/mix dir. The new
+# one wants just the hpc/vanilla/mix dirs. This is quite a bit simpler
+# to extract.  (I don't entirely understand why changing the Cabal
+# version changes the hpc behavior, but I guess hpc must be linked to
+# the Cabal library. Anyway, if the behavior ever changes back,
+# consider fishing the older version of this logic out of the
+# history.)
+HPCDIRS=$(find "$BUILDDIR" -path '*/hpc/vanilla/mix' -type d -print | sort)
 
-HPC_ARGS=""
-for d1 in $(find "$BUILDDIR" -path '*/hpc/vanilla/mix' -type d -print); do
-    for d2 in "$d1"/*; do
-        if [ "$d2" = "$d1/*" ]; then
-            continue
-        fi
-        HPC_ARGS="${HPC_ARGS} --hpcdir=${d2}"
-    done
-done
+# Print what we found. Back-substitute BUILDDIR; the paths are
+# enormous and it's hard enough to read this way.
+echo "HPCDIRS:"
+echo "$HPCDIRS" | awk '
+    {
+        gsub(builddir, "$BUILDDIR", $0);
+        for (i=1;i<=NF;i++) printf "   %s\n", $i;
+    }
+' "builddir=$BUILDDIR"
 
 # Check if we actually found stuff, in case we didn't, and bail with
 # an error message instead of generating hpc's usage message.
-if [ "x$HPC_ARGS" = x ]; then
+if [ "x$HPCDIRS" = x ]; then
     echo "$0: Found no paths matching hpc/vanilla/mix/* in $BUILDDIR" 1>&2
     echo "$0: There are the following hpc dirs:" 1>&2
     find "$BUILDDIR" -type d -name hpc -print 1>&2
@@ -113,5 +139,35 @@ if [ "x$HPC_ARGS" = x ]; then
     echo "$0: ...help?" 1>&2
     exit 1
 fi
-
+
+# Now stick --hpcdir= in front of each one. I separated this out to
+# improve the legibility of the prints above during one of the rounds
+# of mysterious failures.
+HPC_ARGS=$(echo "$HPCDIRS" |\
+              awk '{ for (i=1;i<=NF;i++) printf " --hpcdir=%s", $i; printf "\n"; }')
+
+echo "Running:"
+echo "   hpc markup --destdir=hpc-html <<HPC_ARGS>> ${SUM_TIX}"
 hpc markup --destdir=hpc-html ${HPC_ARGS} ${SUM_TIX}
+if [ $? != 0 ]; then
+    (
+        echo "Failed."
+        echo "HPC_ARGS:"
+        echo "$HPC_ARGS" | awk '
+            {
+                gsub(builddir, "$BUILDDIR", $0);
+                for (i=1;i<=NF;i++) printf "   %s\n", $i;
+            }
+        ' "builddir=$BUILDDIR"
+
+        echo "Files in HPCDIRS:"
+        find $HPCDIRS -type f | sort | awk '
+            {
+                gsub(builddir, "$BUILDDIR", $0);
+                printf "   %s\n", $0
+            }
+        ' "builddir=$BUILDDIR"
+        echo "Help!!"
+    ) 1>&2
+    exit 1
+fi

crux-mir-comp/Dockerfile

@@ -49,7 +49,7 @@ RUN case ${TARGETPLATFORM} in \
     chmod +x /home/crux-mir-comp/ghcup-download/bin/ghcup
 RUN mkdir -p /home/crux-mir-comp/.ghcup && \
     ghcup --version && \
-    ghcup install cabal 3.10.3.0 && \
+    ghcup install cabal 3.14.1.0 && \
     ghcup install ghc 9.6.7 && \
     ghcup set ghc 9.6.7
 

cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs

@@ -1829,20 +1829,40 @@ importName cnm =
               qn = cryptolQualName [] [] shortNm (Just (C.nameUnique cnm))
            in pure (mkImportedName qn)
 
-      | otherwise ->
+      | otherwise -> do
           let (topMod, nested) = C.modPathSplit (C.ogModule og)
               topChunks = C.modNameChunksText topMod
               nestedNms = map C.identText nested
-              -- If the name came from a module parameter, add the module
-              -- parameter identifier to distinguish between names that have the
-              -- same identifier but come from different module parameters (see
-              -- #1892)
-              ifaceNms  = case C.ogFromParam og of
-                            Just i  -> [C.identText i]
-                            Nothing -> []
               shortNm   = C.identText (C.nameIdent cnm)
-              qn        = cryptolQualName topChunks (nestedNms ++ ifaceNms) shortNm Nothing
-           in pure (mkImportedName qn)
+              qn        = cryptolQualName topChunks nestedNms shortNm Nothing
+
+          -- As of May 2026 and Cryptol #2059 (possibly earlier),
+          -- the `C.ogFromParam` field that says if a name came
+          -- from a module parameter is only supposed to be
+          -- present in interfaces, which we can't import
+          -- directly, or unapplied functors, which we don't
+          -- support. If it appears nonempty, fail. (This should
+          -- maybe be a panic; it isn't clear if an unsupported
+          -- import will fail upstream or make it to here and then
+          -- need to fail in a user-facing way.)
+          --
+          -- Prior to this point we'd take the name and append it
+          -- to `nestedNms`, because it used to be possible to get
+          -- duplicate names in applied functors that had multiple
+          -- instances of the same interface argument. See #1892.
+          -- If necessary, we can do that again in the future. If
+          -- mucking with this, be sure to run test1892, and also
+          -- test3000.
+          --
+          -- Note if making this a panic: be sure it actually gets
+          -- evaluated.
+          case C.ogFromParam og of
+              Nothing -> pure ()
+              Just i  ->
+                  fail $ Text.unpack $ "Unexpected/unsupported module " <>
+                                       "parameter name " <> C.identText i <>
+                                       " in Cryptol name " <> QN.ppQualName qn
+          pure (mkImportedName qn)
 
 -- | Map 'bindName' over a list of names and signatures, returning an updated
 -- 'CryptolEnv' and a list of fresh SAWCore variables.

otherTests/saw-core-rocq/test_cryptol_module_sha512.log.good

@@ -11,7 +11,7 @@ Malformed term: let { L@free : Num;
                     }
  in fix x`6
       (\(hash : x`6) ->
-         ecCat x`1 L@free x`3 [|:SHA__parameter::H0]
+         ecCat x`1 L@free x`3 [|:Parameter::H0]
            (coerce (seq x`7 x`3) (seq L@free x`3)
               (seq_cong1 x`7 L@free x`3 (unsafeAssert Num x`7 L@free))
               (seqMap #(x`3, x`4) x`3 x`7

saw-central/src/SAWCentral/Crucible/LLVM/Setup/Value.hs

@@ -15,6 +15,7 @@ The printing code for the types in this module lives in
 (apart from LLVMModule, since we don't export its contents)
 -}
 
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE OverloadedStrings #-}

saw-core-what4/src/SAWCoreWhat4/Uninterp.hs

@@ -123,6 +123,7 @@ uninterpreted functions, there's a special case for terms that started as
 SAW Core *variables* rather than SAW Core *constant*, and don't have any
 arguments---these use `bindSAWTerm` instead of `sawRegisterSymFunInterp`.
 -}
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}

saw-core/src/SAWCore/Fingerprint.hs

@@ -15,14 +15,19 @@ module SAWCore.Fingerprint
   ( fingerprintSATQuery
   ) where
 
+-- FUTURE: this and the explicit import from Data.Foldable can be
+-- dropped once we no longer support building with GHC 9.8 or earlier
+-- (base 4.19 and earlier).
+import Prelude hiding (Foldable(..))
+
 import Control.Monad.Reader (ReaderT, MonadReader, runReaderT, ask)
 import Control.Monad.State.Strict (State, MonadState, state, gets, modify', evalState)
 import qualified Crypto.Hash.SHA256 as SHA256
 import Data.Binary (encode)
 import qualified Data.ByteString as BS
 import qualified Data.ByteString.Builder as BS
 import Data.ByteString.Lazy (ByteString, singleton)
-import Data.Foldable (foldl')
+import Data.Foldable (Foldable(..)) -- for foldl'
 import Data.IntMap.Strict (IntMap)
 import qualified Data.IntMap.Strict as IntMap
 import qualified Data.Map.Strict as Map

saw-remote-api/Dockerfile

@@ -41,7 +41,7 @@ RUN case ${TARGETPLATFORM} in \
     chmod +x /home/saw/ghcup-download/bin/ghcup
 RUN mkdir -p /home/saw/.ghcup && \
     ghcup --version && \
-    ghcup install cabal 3.10.3.0 && \
+    ghcup install cabal 3.14.1.0 && \
     ghcup install ghc 9.6.7 && \
     ghcup set ghc 9.6.7
 

saw.cabal

@@ -718,11 +718,11 @@ library saw-server
 
   build-depends:
     -- upstream packages from hackage
-    base >=4.11.1.0 && <4.20,
+    base >=4.11.1.0 && <4.22,
     aeson >= 1.4.2 && < 2.3,
     base64-bytestring,
     bytestring,
-    containers >= 0.6 && < 0.7,
+    containers >= 0.6 && < 0.8,
     cryptonite,
     cryptonite-conduit,
     directory,
@@ -830,11 +830,11 @@ executable saw-remote-api
 
   build-depends:
     -- upstream packages from hackage
-    base >=4.11.1.0 && <4.20,
+    base >=4.11.1.0 && <4.22,
     aeson >= 1.4.2 && < 2.3,
     base64-bytestring,
     bytestring,
-    containers >= 0.6 && < 0.7,
+    containers >= 0.6 && < 0.8,
     cryptonite,
     cryptonite-conduit,
     directory,

saw/Dockerfile

@@ -41,7 +41,7 @@ RUN case ${TARGETPLATFORM} in \
     chmod +x /home/saw/ghcup-download/bin/ghcup
 RUN mkdir -p /home/saw/.ghcup && \
     ghcup --version && \
-    ghcup install cabal 3.10.3.0 && \
+    ghcup install cabal 3.14.1.0 && \
     ghcup install ghc 9.6.7 && \
     ghcup set ghc 9.6.7
 RUN cabal v2-update