Draft: Support GHC 9.2

This contains a variety of minor changes needed to make `saw` and its
supporting libraries compile with GHC 9.2:

* One place in `heapster-saw` matches on a GADT using a `let` binding, which no
  longer typechecks in GHC 9.2. While somewhat mysterious, using `let` bindings
  to match on GADTs is fragile anyway, so I opted to simply replace this with a
  monadic `do` match, which does not exhibit the same fragility.
* GHC now includes `-Wincomplete-uni-patterns` in `-Wall` as of 9.2, so much
  of this patch is dedicated to silencing these sorts of warnings, usually by
  adding explicit fall-through cases for partial pattern matches.
* GHC now inclues `-Wnoncanonical-monad-instances` in `-Wall` as of 9.2, so I
  had to refactor some `Applicative`/`Monad` instances to fix these warnings.
* GHC 9.2 now defines `readBin` in `Numeric`, which clashes with a function of
  the same name in `SAWScript.Lexer`. Using explicit imports avoids this.
* GHC's pattern-match coverage checker is smarter in 9.2 (see
  [here](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.2?version_id=63085dd8a5b56370571bda428848e7098765f7f8#improved-pattern-match-coverage-checker)),
  so I had to use `EmptyCase` to silence some of the new
  `-Wincomplete-patterns` warnings that were uncovered in `heapster-saw`.
* The `language-sally` submodule dependency has been bumped to bring in changes
  from GaloisInc/language-sally#11. This requires bumping the `what4` submodule
  as a knock-on consequence.

This is still a draft because:

* [ ] There are various `-Wincomplete-uni-patterns` warnings in `saw` and
      `heapster-saw` that I have not yet had time to address. (See also a
      `TODO RGS` in `exe:saw` that should be fixed.)

      Also this one in `saw-remote-api`:

   ```
   src/SAWServer/Yosys.hs:113:11: warning: [-Wincomplete-uni-patterns]
       Pattern match(es) are non-exhaustive
       In a pattern binding:
           Patterns of type ‘Maybe
                               Verifier.SAW.TypedTerm.TypedTerm’ not matched:
               Nothing
       |
   113 |       let Just modTerm = Map.lookup (yosysVerifyModule params) imp
       |           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   ```
* [ ] Need to fix this warning (maybe?):

   ```
   src/Verifier/SAW/Heapster/Permissions.hs:8387:47: warning: [-Wstar-is-type]
       Using ‘*’ (or its Unicode variant) to mean ‘Data.Kind.Type’
       relies on the StarIsType extension, which will become
       deprecated in the future.
       Suggested fix: use ‘Type’ from ‘Data.Kind’ instead.
        |
   8387 | newtype SeenDetVarsClauses :: CrucibleType -> * where
        |                                               ^
   ```

[ci skip]

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, 8.10, or 9.0.
+    Cabal 3.4 or newer, and GHC 8.8, 8.10, 9.0, or 9.2.
 
   * Ensure that you have the C libraries and header files for
     `terminfo`, which generally comes as part of `ncurses` on most

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

@@ -1,3 +1,4 @@
+{-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE QuasiQuotes #-}
@@ -737,6 +738,7 @@ cruCtxLen (CruCtxCons ctx _) = 1 + cruCtxLen ctx
 
 -- | Look up a type in a 'CruCtx'
 cruCtxLookup :: CruCtx ctx -> Member ctx a -> TypeRepr a
+cruCtxLookup CruCtxNil m = case m of {}
 cruCtxLookup (CruCtxCons _ tp) Member_Base = tp
 cruCtxLookup (CruCtxCons ctx _) (Member_Step memb) = cruCtxLookup ctx memb
 

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

@@ -2206,7 +2206,7 @@ mbRangeFTDelete
     bvRangeDelete rng1 rng2
 mbRangeFTDelete mb_rng _ = [mb_rng]
 
--- | Delete all ranges in any of a list of ranges from 
+-- | Delete all ranges in any of a list of ranges from
 mbRangeFTsDelete :: [MbRangeForType a] -> [MbRangeForType a] ->
                     [MbRangeForType a]
 mbRangeFTsDelete rngs_l rngs_r =
@@ -3053,13 +3053,16 @@ addPermOffsets (LLVMPermOffset off1) (LLVMPermOffset off2) =
 
 -- | Get the @n@th expression in a 'PermExprs' list
 nthPermExpr :: PermExprs args -> Member args a -> PermExpr a
+nthPermExpr PExprs_Nil m = case m of {}
 nthPermExpr (PExprs_Cons _ arg) Member_Base = arg
 nthPermExpr (PExprs_Cons args _) (Member_Step memb) =
   nthPermExpr args memb
 
 -- | Set the @n@th expression in a 'PermExprs' list
 setNthPermExpr :: PermExprs args -> Member args a -> PermExpr a ->
                   PermExprs args
+setNthPermExpr PExprs_Nil m _ =
+  case m of {}
 setNthPermExpr (PExprs_Cons args _) Member_Base a =
   PExprs_Cons args a
 setNthPermExpr (PExprs_Cons args arg) (Member_Step memb) a =
@@ -7088,6 +7091,7 @@ permVarSubstToNames PermVarSubst_Nil = MNil
 permVarSubstToNames (PermVarSubst_Cons s n) = permVarSubstToNames s :>: n
 
 varSubstLookup :: PermVarSubst ctx -> Member ctx a -> ExprVar a
+varSubstLookup PermVarSubst_Nil m = case m of {}
 varSubstLookup (PermVarSubst_Cons _ x) Member_Base = x
 varSubstLookup (PermVarSubst_Cons s _) (Member_Step memb) =
   varSubstLookup s memb

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

@@ -2941,7 +2941,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
        let prxs2 = mbRAssignProxies ps2
        let prxs_in = RL.append prxs1 prxs2 :>: Proxy
        pctx <- itiPermStack <$> ask
-       let (pctx_ps, pctx12 :>: ptrans_l) = RL.split ps0 prxs_in pctx
+       (pctx_ps, pctx12 :>: ptrans_l) <- pure $ RL.split ps0 prxs_in pctx
        let (pctx1, pctx2) = RL.split prxs1 prxs2 pctx12
 
        -- Also split out the input variables and replace them with the ps_out vars
@@ -2955,10 +2955,10 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
        let fromJustOrError (Just x) = x
            fromJustOrError Nothing = error "translateSimplImpl: SImpl_MapLifetime"
            ps_in'_vars =
-             RL.map (translateVar . getCompose) $ mbRAssign $ 
+             RL.map (translateVar . getCompose) $ mbRAssign $
              fmap (fromJustOrError . exprPermsVars) ps_in'
            ps_out_vars =
-             RL.map (translateVar . getCompose) $ mbRAssign $ 
+             RL.map (translateVar . getCompose) $ mbRAssign $
              fmap (fromJustOrError . exprPermsVars) ps_out
        impl_in_tm <-
          translateCurryLocalPermImpl "Error mapping lifetime input perms:" impl_in
@@ -4946,7 +4946,7 @@ tcTranslateAddCFGs sc mod_name env checks endianness dlevel cfgs_and_perms =
        applyOpenTerm (globalOpenTerm "Prelude.lrtTupleType") lrts
      tup_fun_tm <- completeNormOpenTerm sc $
        applyOpenTermMulti (globalOpenTerm "Prelude.multiFixM") [lrts, tup_fun]
-     scInsertDef sc mod_name tup_fun_ident tup_fun_tp tup_fun_tm 
+     scInsertDef sc mod_name tup_fun_ident tup_fun_tp tup_fun_tm
      new_entries <-
        zipWithM
        (\cfg_and_perm i ->

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

@@ -117,11 +117,11 @@ instance Functor (PolyContT r m) where
   fmap f m = m >>= return . f
 
 instance Applicative (PolyContT r m) where
-  pure = return
+  pure x = PolyContT $ \k -> k x
   (<*>) = ap
 
 instance Monad (PolyContT r m) where
-  return x = PolyContT $ \k -> k x
+  return = pure
   (PolyContT m) >>= f =
     PolyContT $ \k -> m $ \a -> runPolyContT (f a) k
 
@@ -454,7 +454,7 @@ widenExprs (CruCtxCons tps tp) (es1 :>: e1) (es2 :>: e2) =
 
 
 -- | Widen two bitvector offsets by trying to widen them additively
--- ('widenBVsAddy'), or if that is not possible, by widening them 
+-- ('widenBVsAddy'), or if that is not possible, by widening them
 -- multiplicatively ('widenBVsMulty')
 widenOffsets :: (1 <= w, KnownNat w) => TypeRepr (BVType w) ->
                 PermOffset (LLVMPointerType w) ->

saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs

@@ -96,7 +96,20 @@ translateDataType (DataType {..}) =
         liftTermTranslationMonad $ do
         ps <- TermTranslation.translateParams dtParams
         ixs <- TermTranslation.translateParams dtIndices
-        return (ps, map (\(Coq.Binder s (Just t)) -> Coq.PiBinder (Just s) t) ixs)
+        -- Translating the indices of a data type should never yield
+        -- Inhabited constraints, so the result of calling
+        -- `translateParams dtIndices` above should only return Binders and not
+        -- any ImplicitBinders. Moreover, `translateParams` always returns
+        -- Binders where the second field is `Just t`, where `t` is the type.
+        let errorBecause msg = error $ "translateDataType.translateNamed: " ++ msg
+        let bs = map (\case Coq.Binder s (Just t) ->
+                              Coq.PiBinder (Just s) t
+                            Coq.Binder _ Nothing ->
+                              errorBecause "encountered a Binder without a Type"
+                            Coq.ImplicitBinder{} ->
+                              errorBecause "encountered an implicit binder")
+                     ixs
+        return (ps, bs)
       let inductiveSort = TermTranslation.translateSort dtSort
       inductiveConstructors <- mapM (translateCtor inductiveParameters) dtCtors
       return $ Coq.InductiveDecl $ Coq.Inductive

saw-core-sbv/saw-core-sbv.cabal

@@ -20,7 +20,7 @@ library
     lens,
     mtl,
     saw-core,
-    sbv >= 8.10 && < 8.16,
+    sbv >= 8.10 && < 9.1,
     text,
     transformers,
     vector

saw-core/saw-core.cabal

@@ -24,7 +24,7 @@ library
     happy >= 1.9.6
 
   build-depends:
-    base == 4.*,
+    base >= 4.8,
     array,
     bytestring,
     containers,

saw-core/src/Verifier/SAW/Change.hs

@@ -1,4 +1,3 @@
-{-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -25,10 +24,8 @@ module Verifier.SAW.Change
   , flatten
   ) where
 
-#if !MIN_VERSION_base(4,8,0)
-import Control.Applicative
-#endif
-import Control.Monad (liftM, liftM2)
+import Control.Applicative (liftA2)
+import Control.Monad (liftM)
 import Control.Monad.Trans
 
 ----------------------------------------------------------------------
@@ -84,7 +81,7 @@ instance Applicative Change where
   Modified f <*> Modified x = Modified (f x)
 
 instance Monad Change where
-  return x = Original x
+  return = pure
   Original x >>= k = k x
   Modified x >>= k = taint (k x)
 
@@ -108,15 +105,15 @@ commitChange (Modified x) = x
 
 newtype ChangeT m a = ChangeT { runChangeT :: m (Change a) }
 
-instance Monad m => Functor (ChangeT m) where
-  fmap f (ChangeT m) = ChangeT (liftM (fmap f) m)
+instance Functor m => Functor (ChangeT m) where
+  fmap f (ChangeT m) = ChangeT (fmap (fmap f) m)
 
-instance Monad m => Applicative (ChangeT m) where
-  pure x = ChangeT (return (Original x))
-  ChangeT m1 <*> ChangeT m2 = ChangeT (liftM2 (<*>) m1 m2)
+instance Applicative m => Applicative (ChangeT m) where
+  pure x = ChangeT (pure (Original x))
+  ChangeT m1 <*> ChangeT m2 = ChangeT (liftA2 (<*>) m1 m2)
 
 instance Monad m => Monad (ChangeT m) where
-  return x = ChangeT (return (Original x))
+  return = pure
   ChangeT m >>= k = ChangeT (m >>= f)
     where f (Original x) = runChangeT (k x)
           f (Modified x) = runChangeT (k x) >>= (return . taint)

saw-core/src/Verifier/SAW/Conversion.hs

@@ -361,13 +361,13 @@ instance Monad TermBuilder where
   m >>= h = TermBuilder $ \mg mk -> do
     r <- runTermBuilder m mg mk
     runTermBuilder (h r) mg mk
-  return v = TermBuilder $ \_ _ -> return v
+  return = pure
 
 instance Functor TermBuilder where
     fmap = liftM
 
 instance Applicative TermBuilder where
-    pure = return
+    pure v = TermBuilder $ \_ _ -> pure v
     (<*>) = ap
 
 mkTermF :: TermF Term -> TermBuilder Term

saw-core/src/Verifier/SAW/Rewriter.hs

@@ -248,7 +248,11 @@ scMatch sc pat term =
              guard (fvy `unionBitSets` fvj == fvj)
              let fixVar t (nm, ty) =
                    do v <- scFreshGlobal sc nm ty
-                      let Just ec = R.asExtCns v
+                      -- asExtCns should always return Just here because
+                      -- scFreshGlobal always returns an ExtCns.
+                      ec <- case R.asExtCns v of
+                              Just ec -> pure ec
+                              Nothing -> error "scMatch.match: impossible"
                       t' <- instantiateVar sc 0 v t
                       return (t', ec)
              let fixVars t [] = return (t, [])
@@ -958,10 +962,13 @@ doHoistIfs sc ss hoistCache itePat = go
        top :: Term -> TermF Term -> IO (HoistIfs s)
        top t tf
           | Just inst <- first_order_match itePat t = do
-               let Just branch_tp   = Map.lookup 0 inst
-               let Just cond        = Map.lookup 1 inst
-               let Just then_branch = Map.lookup 2 inst
-               let Just else_branch = Map.lookup 3 inst
+               -- All of these Map lookups should be safe due to the term
+               -- structure of an if-then-else expression.
+               let err = error "doHoistIfs.top: impossible"
+               let branch_tp   = Map.findWithDefault err 0 inst
+               let cond        = Map.findWithDefault err 1 inst
+               let then_branch = Map.findWithDefault err 2 inst
+               let else_branch = Map.findWithDefault err 3 inst
 
                (then_branch',conds1) <- go then_branch
                (else_branch',conds2) <- go else_branch

saw-core/src/Verifier/SAW/TermNet.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE RecordWildCards #-}
@@ -250,8 +251,11 @@ matching unif = match
         Var       -> nets
         App t1 t2 -> foldr (match t2) nets (rands t1 comb [])
 
+{- Invariant: Each list entry must be a Leaf. -}
 extract_leaves :: [Net a] -> [a]
-extract_leaves = concatMap (\(Leaf xs) -> xs)
+extract_leaves = concatMap $ \case
+  Leaf xs -> xs
+  Net{}   -> error "extract_leaves: Unexpected Net node"
 
 {-return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL-}
 match_term :: Pattern t => Net a -> t -> [a]

saw-core/src/Verifier/SAW/UnionFind.hs

@@ -85,6 +85,26 @@ classRep (Class r) = UF $ do
             return (Class i)
   impl r []
 
+-- | Look up an equivalence class in a union find structure's map. This checks
+-- the invariant that the index of the class exists in the map and is associated
+-- with a 'Rep', not a 'NonRep'. If this invariant is violated, this function
+-- will throw an error.
+lookupClassRep :: Class d -> UnionFind d -> ([ClassIndex], Int, d)
+lookupClassRep (Class rC) uf =
+  case Map.lookup rC (ufsMap uf) of
+    Just (Rep ne sz d) ->
+      (ne, sz, d)
+    Just (NonRep i) ->
+      errorBecause $ unlines
+        [ "not associated with a class representative,"
+        , "but rather an element with index " ++ show i
+        ]
+    Nothing ->
+      errorBecause "not found in map"
+  where
+    errorBecause msg = error $
+      "lookupClassRep: Equivalence class index " ++ show rC ++ " " ++ msg
+
 -- | Creates a new class with the given descriptor.
 freshClass :: d -> Action d (Class d)
 freshClass d = UF $ do
@@ -118,14 +138,14 @@ setEqual :: Class d
          -> d -- ^ Descriptor for union class.
          -> Action d AssertResult
 setEqual x y d = do
-  Class xr <- classRep x
-  Class yr <- classRep y
+  xc@(Class xr) <- classRep x
+  yc@(Class yr) <- classRep y
   if xr == yr
     then return AssertRedundant
     else do
-      m <- UF $ gets ufsMap
-      let Rep xne xsz _xd = m Map.! xr
-      let Rep yne ysz _yd = m Map.! yr
+      uf <- UF get
+      let (xne, xsz, _xd) = lookupClassRep xc uf
+      let (yne, ysz, _yd) = lookupClassRep yc uf
       xElts <- fmap (map toClassIdx) $ mapM classRep (map Class xne)
       yElts <- fmap (map toClassIdx) $ mapM classRep (map Class yne)
       if xr `elem` yElts || yr `elem` xElts
@@ -151,14 +171,14 @@ setEqual x y d = do
 -- previously set equal.
 setUnequal :: Class d -> Class d -> Action d AssertResult
 setUnequal x y = do
-  Class xr <- classRep x
-  Class yr <- classRep y
+  xc@(Class xr) <- classRep x
+  yc@(Class yr) <- classRep y
   if xr == yr
     then return AssertFailed
     else do
-      m <- UF $ gets ufsMap
-      let Rep xne xsz xd = m Map.! xr
-      let Rep yne _ _ = m Map.! yr
+      uf <- UF get
+      let (xne, xsz, xd) = lookupClassRep xc uf
+      let (yne, _,   _)  = lookupClassRep yc uf
       xElts <- fmap (map toClassIdx) $ mapM classRep (map Class xne)
       yElts <- fmap (map toClassIdx) $ mapM classRep (map Class yne)
       if xr `elem` yElts || yr `elem` xElts
@@ -172,24 +192,23 @@ setUnequal x y = do
 -- | Get a class description
 readClassDesc :: Class d -> Action d d
 readClassDesc c = do
-  Class rC <- classRep c
-  m <- UF $ gets ufsMap
-  let Rep _ _ desc = m Map.! rC
+  rCls <- classRep c
+  s <- UF get
+  let (_, _, desc) = lookupClassRep rCls s
   return desc
 
 -- | Set a class description
 writeClassDesc :: Class d -> d -> Action d ()
 writeClassDesc c d = do
-  Class rC <- classRep c
+  rCls@(Class rC) <- classRep c
   UF $ modify $ \s ->
-    let Rep dis sz _ = (ufsMap s) Map.! rC
+    let (dis, sz, _) = lookupClassRep rCls s
      in s { ufsMap = Map.insert rC (Rep dis sz d) (ufsMap s) }
 
 -- | Modify a class description
 modifyClassDesc :: Class d -> (d -> d) -> Action d ()
 modifyClassDesc c fn = do
-  Class rC <- classRep c
+  rCls@(Class rC) <- classRep c
   UF $ modify $ \s ->
-    let Rep dis sz desc = (ufsMap s) Map.! rC
+    let (dis, sz, desc) = lookupClassRep rCls s
      in s { ufsMap = Map.insert rC (Rep dis sz (fn desc)) (ufsMap s) }
-

saw-remote-api/saw-remote-api.cabal

@@ -34,8 +34,8 @@ common errors
     -Werror=overlapping-patterns
 
 common deps
-  build-depends: base >=4.11.1.0 && <4.16,
-                 aeson >= 1.4.2 && < 2.0,
+  build-depends: base >=4.11.1.0 && <4.17,
+                 aeson >= 1.4.2 && < 2.1,
                  aig,
                  argo,
                  base64-bytestring,

saw-script.cabal

@@ -22,8 +22,8 @@ custom-setup
 library
   default-language: Haskell2010
   build-depends:
-      base >= 4
-    , aeson >= 1.4.2 && < 2.0
+      base >= 4.9
+    , aeson >= 2.0 && < 2.1
     , aig
     , array
     , binary
@@ -80,7 +80,7 @@ library
     , saw-core-coq
     , saw-core-sbv
     , saw-core-what4
-    , sbv >= 8.10 && < 8.16
+    , sbv >= 8.10 && < 9.1
     , split
     , temporary
     , template-haskell