Support building with GHC 9.0

This contains a variety of fixes needed to make the packages in the
`saw-script` repo compile with GHC 9.0:

* GHC 9.0 implements simplified subsumption (see
  [here](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0?version_id=5fcd0a50e0872efb3c38a32db140506da8310d87#simplified-subsumption)).
  This requires manually eta expanding some function applications to
  accommodate (see, for instance, the expansions of `getAllLLVM` in
  `SAWScript.Crucible.LLVM.MethodSpecIR`.
* GHC's constraint solver now solves constraints in each top-level group
  sooner (see
  [here](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0?version_id=5fcd0a50e0872efb3c38a32db140506da8310d87#the-order-of-th-splices-is-more-important)).
  This affects `heapster-saw`, as it uses declaration splices extensively. I
  did some fairly involved rearranging of data type declarations and
  TH-generated instances to make everything typecheck. It's not exactly pretty,
  but it gets the job done.
* GHC 9.0 now enables `-Wstar-is-type` in `-Wall`, so this patch replaces some
  uses of `*` with `Data.Kind.Type` in `saw-core-what4` and `crux-mir-comp`.
  `Data.Kind` requires the use of GHC 8.0 or later, so this patch also updates
  the lower bounds on `base` to `>= 4.9` in the appropriate `.cabal` files.
  (I'm fairly certain that this requirement was already present implicity, but
  better to be explicit about it.)
* The upper version bounds on `base` in `saw-remote-api` were raised to allow
  it to build with `base-4.15.*`, which is bundled with GHC 9.0.
* The `cryptol` submodule was bumped to incorporate the changes from
  GaloisInc/cryptol#1233, which allow it to build with GHC 9.0.

Author: RyanGlScott

README.md

@@ -42,7 +42,7 @@ To build SAWScript and related utilities from source:
   * Ensure that you have the `cabal` and `ghc` executables in your
     `PATH`. If you don't already have them, we recommend using `ghcup`
     to install them: <https://www.haskell.org/ghcup/>. We recommend
-    Cabal 3.4 or newer, and GHC 8.8 or 8.10.
+    Cabal 3.4 or newer, and GHC 8.8, 8.10, or 9.0.
 
   * Ensure that you have the C libraries and header files for
     `terminfo`, which generally comes as part of `ncurses` on most

crux-mir-comp/crux-mir-comp.cabal

@@ -19,7 +19,7 @@ extra-source-files:  README.md
 
 library
   default-language: Haskell2010
-  build-depends: base >= 4.7 && < 5,
+  build-depends: base >= 4.9 && < 5,
                  text,
                  prettyprinter >= 1.7.0,
                  crucible,

crux-mir-comp/src/Mir/Compositional/Override.hs

@@ -66,7 +66,7 @@ import Mir.Compositional.MethodSpec
 type MirOverrideMatcher sym a = forall p rorw rtp args ret.
     MS.OverrideMatcher' sym MIR rorw (OverrideSim (p sym) sym MIR rtp args ret) a
 
-data MethodSpec = MethodSpec 
+data MethodSpec = MethodSpec
     { _msCollectionState :: CollectionState
     , _msSpec :: MIRMethodSpec
     }
@@ -244,7 +244,7 @@ runSpec cs mh ms = ovrWithBackend $ \bak ->
         -- TODO: see if we need any other assertions from LLVM OverrideMatcher
 
 
-        -- Handle preconditions and postconditions.  
+        -- Handle preconditions and postconditions.
 
         -- Convert preconditions to `osAsserts`
         forM_ (ms ^. MS.csPreState . MS.csConditions) $ \cond -> do
@@ -379,7 +379,7 @@ matchArg sym sc eval allocSpecs shp rv sv = go shp rv sv
                         ""
     go (TupleShape _ _ flds) rvs (MS.SetupStruct () False svs) = goFields flds rvs svs
     go (ArrayShape _ _ shp) vec (MS.SetupArray () svs) = case vec of
-        MirVector_Vector v -> zipWithM_ (go shp) (toList v) svs
+        MirVector_Vector v -> zipWithM_ (\x y -> go shp x y) (toList v) svs
         MirVector_PartialVector pv -> forM_ (zip (toList pv) svs) $ \(p, sv) -> do
             rv <- liftIO $ readMaybeType sym "vector element" (shapeType shp) p
             go shp rv sv

crux-mir-comp/src/Mir/Cryptol.hs

@@ -19,6 +19,7 @@ import Control.Monad.IO.Class
 import qualified Data.ByteString as BS
 import Data.Functor.Const
 import Data.IORef
+import qualified Data.Kind as Kind
 import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.String (fromString)
@@ -241,10 +242,10 @@ loadCryptolFunc col sig modulePath name = do
         cryptolRun sc (Text.unpack fnName) argShps retShp (SAW.ttTerm tt)
 
   where
-    listToCtx :: forall k (f :: k -> *). [Some f] -> Some (Assignment f)
+    listToCtx :: forall k (f :: k -> Kind.Type). [Some f] -> Some (Assignment f)
     listToCtx xs = go xs (Some Empty)
       where
-        go :: forall k (f :: k -> *). [Some f] -> Some (Assignment f) -> Some (Assignment f)
+        go :: forall k (f :: k -> Kind.Type). [Some f] -> Some (Assignment f) -> Some (Assignment f)
         go [] acc = acc
         go (Some x : xs) (Some acc) = go xs (Some $ acc :> x)
 

deps/cryptol

@@ -38,6 +38,7 @@ library
     filepath,
     language-rust,
     hobbits ^>= 1.4,
+    extra,
   hs-source-dirs: src
   build-tool-depends:
     alex:alex,

heapster-saw/heapster-saw.cabal

@@ -371,8 +371,8 @@ $(mkNuMatching [t| UB.PtrComparisonOperator |])
 $(mkNuMatching [t| forall v. NuMatching v => StorageTypeF v |])
 $(mkNuMatching [t| StorageType |])
 
-$(mkNuMatching [t| forall f. NuMatchingAny1 f => UB.UndefinedBehavior f |])
 $(mkNuMatching [t| forall f. NuMatchingAny1 f => Poison.Poison f |])
+$(mkNuMatching [t| forall f. NuMatchingAny1 f => UB.UndefinedBehavior f |])
 -- $(mkNuMatching [t| forall f. NuMatchingAny1 f => BadBehavior f |])
 -- $(mkNuMatching [t| forall f. NuMatchingAny1 f => LLVMSafetyAssertion f |])
 $(mkNuMatching [t| forall f. NuMatchingAny1 f => LLVMSideCondition f |])
@@ -390,17 +390,6 @@ instance NuMatchingAny1 (EmptyExprExtension f) where
 
 $(mkNuMatching [t| AVXOp1 |])
 $(mkNuMatching [t| forall f tp. NuMatchingAny1 f => ExtX86 f tp |])
-$(mkNuMatching [t| forall f tp. NuMatchingAny1 f =>
-                LLVMExtensionExpr f tp |])
-
-instance NuMatchingAny1 f => NuMatchingAny1 (LLVMExtensionExpr f) where
-  nuMatchingAny1Proof = nuMatchingProof
-
-{-
-$(mkNuMatching [t| forall w f tp. NuMatchingAny1 f => LLVMStmt w f tp |])
--}
-
-$(mkNuMatching [t| forall tp. GlobalVar tp |])
 
 instance NuMatching (Nonce s tp) where
   nuMatchingProof = unsafeMbTypeRepr
@@ -411,6 +400,17 @@ instance Closable (Nonce s tp) where
 instance Liftable (Nonce s tp) where
   mbLift = unClosed . mbLift . fmap toClosed
 
+$(mkNuMatching [t| forall tp. GlobalVar tp |])
+$(mkNuMatching [t| forall f tp. NuMatchingAny1 f =>
+                LLVMExtensionExpr f tp |])
+
+instance NuMatchingAny1 f => NuMatchingAny1 (LLVMExtensionExpr f) where
+  nuMatchingAny1Proof = nuMatchingProof
+
+{-
+$(mkNuMatching [t| forall w f tp. NuMatchingAny1 f => LLVMStmt w f tp |])
+-}
+
 instance Closable (BV.BV w) where
   toClosed = unsafeClose
 

heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs

@@ -37,6 +37,7 @@ import qualified Data.BitVector.Sized as BV
 import GHC.TypeLits
 import Control.Lens hiding ((:>), ix)
 import Control.Applicative
+import Control.Monad.Extra (concatMapM)
 import Control.Monad.State.Strict hiding (ap)
 
 import qualified Data.Type.RList as RL
@@ -1512,22 +1513,40 @@ idLocalPermImpl = LocalPermImpl $ PermImpl_Done $ LocalImplRet Refl
 
 -- type IsLLVMPointerTypeList w ps = RAssign ((:~:) (LLVMPointerType w)) ps
 
-$(mkNuMatching [t| forall a. EqPerm a |])
-$(mkNuMatching [t| forall ps a. NuMatching a => EqProofStep ps a |])
-$(mkNuMatching [t| forall ps a. NuMatching a => EqProof ps a |])
-$(mkNuMatching [t| forall ps_in ps_out. SimplImpl ps_in ps_out |])
-$(mkNuMatching [t| forall ps_in ps_outs. PermImpl1 ps_in ps_outs |])
-$(mkNuMatching [t| forall r bs_pss. NuMatchingAny1 r => MbPermImpls r bs_pss |])
-$(mkNuMatching [t| forall r ps. NuMatchingAny1 r => PermImpl r ps |])
-$(mkNuMatching [t| forall ps_in ps_out. LocalPermImpl ps_in ps_out |])
-$(mkNuMatching [t| forall ps ps'. LocalImplRet ps ps' |])
-
 instance NuMatchingAny1 EqPerm where
   nuMatchingAny1Proof = nuMatchingProof
 
 instance NuMatchingAny1 (LocalImplRet ps) where
   nuMatchingAny1Proof = nuMatchingProof
 
+-- Many of these types are mutually recursive. Moreover, Template Haskell
+-- declaration splices strictly separate top-level groups, so if we were to
+-- write each $(mkNuMatching [t| ... |]) splice individually, the splices
+-- involving mutually recursive types would not typecheck. As a result, we
+-- must put everything into a single splice so that it forms a single top-level
+-- group.
+$(concatMapM mkNuMatching
+  [ [t| forall a. EqPerm a |]
+  , [t| forall ps a. NuMatching a => EqProofStep ps a |]
+  , [t| forall ps a. NuMatching a => EqProof ps a |]
+  , [t| forall ps_in ps_out. SimplImpl ps_in ps_out |]
+  , [t| forall ps_in ps_outs. PermImpl1 ps_in ps_outs |]
+  , [t| forall r bs_pss. NuMatchingAny1 r => MbPermImpls r bs_pss |]
+  , [t| forall r ps. NuMatchingAny1 r => PermImpl r ps |]
+  , [t| forall ps_in ps_out. LocalPermImpl ps_in ps_out |]
+  , [t| forall ps ps'. LocalImplRet ps ps' |]
+  ])
+
+-- | A splitting of an existential list of permissions into a prefix, a single
+-- variable plus permission, and then a suffix
+data DistPermsSplit ps where
+  DistPermsSplit :: RAssign Proxy ps1 -> RAssign Proxy ps2 ->
+                    DistPerms (ps1 :++: ps2) ->
+                    ExprVar a -> ValuePerm a ->
+                    DistPermsSplit (ps1 :> a :++: ps2)
+
+$(mkNuMatching [t| forall ps. DistPermsSplit ps |])
+
 
 -- | Compile-time flag for whether to prune failure branches in 'implCatchM'
 pruneFailingBranches :: Bool
@@ -6245,7 +6264,7 @@ proveVarLLVMArrayH x first_p _ ps mb_ap =
 
 -- | Prove an array permission by proving its first cell and then its remaining
 -- cells and appending them together
-proveVarLLVMArray_FromHead :: 
+proveVarLLVMArray_FromHead ::
   (1 <= w, KnownNat w, NuMatchingAny1 r) =>
   ExprVar (LLVMPointerType w) -> Mb vars (LLVMArrayPerm w) ->
   ImplM vars s r (ps :> LLVMPointerType w) ps ()
@@ -7063,7 +7082,7 @@ proveVarLLVMBlocks2 x ps psubst mb_bp mb_sh mb_bps
     -- Prove the corresponding field permission
     proveVarImplInt x (mbValPerm_LLVMField mb_fp) >>>
     getTopDistPerm x >>>= \(ValPerm_LLVMField fp) ->
-    
+
     -- Finally, convert the field perm to a block and move it into position
     implSimplM Proxy (SImpl_IntroLLVMBlockField x fp) >>>
     implSwapInsertConjM x (Perm_LLVMBlock $ llvmFieldPermToBlock fp) ps' 0
@@ -7081,7 +7100,7 @@ proveVarLLVMBlocks2 x ps psubst mb_bp mb_sh mb_bps
     proveVarImplInt x (mbMapCl $(mkClosed [| ValPerm_LLVMArray . fromJust .
                                              llvmBlockPermToArray |]) mb_bp) >>>
     getTopDistPerm x >>>= \(ValPerm_LLVMArray ap) ->
-    
+
     -- Finally, convert the array perm to a block and move it into position
     implSimplM Proxy (SImpl_IntroLLVMBlockArray x ap) >>>
     implSwapInsertConjM x (Perm_LLVMBlock $ fromJust $
@@ -7124,7 +7143,7 @@ proveVarLLVMBlocks2 x ps psubst mb_bp mb_sh mb_bps
 
 
 -- If proving a tagged union shape, first prove an equality permission for the
--- tag and then use that equality permission to 
+-- tag and then use that equality permission to
 proveVarLLVMBlocks2 x ps psubst mb_bp _ mb_bps
   | Just [nuP| SomeTaggedUnionShape mb_tag_u |] <- mbLLVMBlockToTaggedUnion mb_bp
   , mb_shs <- mbTaggedUnionDisjs mb_tag_u
@@ -8125,14 +8144,6 @@ funPermExDistIns fun_perm args =
   fmap (varSubst (permVarSubstOfNames args)) $ mbSeparate args $
   mbValuePermsToDistPerms $ funPermIns fun_perm
 
--- | A splitting of an existential list of permissions into a prefix, a single
--- variable plus permission, and then a suffix
-data DistPermsSplit ps where
-  DistPermsSplit :: RAssign Proxy ps1 -> RAssign Proxy ps2 ->
-                    DistPerms (ps1 :++: ps2) ->
-                    ExprVar a -> ValuePerm a ->
-                    DistPermsSplit (ps1 :> a :++: ps2)
-
 -- | Make a "base case" 'DistPermsSplit' where the split is at the end
 baseDistPermsSplit :: DistPerms ps -> ExprVar a -> ValuePerm a ->
                       DistPermsSplit (ps :> a)
@@ -8418,5 +8429,3 @@ proveVarsImplVarEVars mb_ps =
 proveVarImpl :: NuMatchingAny1 r => ExprVar a -> Mb vars (ValuePerm a) ->
                 ImplM vars s r (ps :> a) ps ()
 proveVarImpl x mb_p = proveVarsImplAppend $ fmap (distPerms1 x) mb_p
-
-$(mkNuMatching [t| forall ps. DistPermsSplit ps |])