diff --git a/README.md b/README.md index 9aed46475a..b701a747e6 100644 --- a/README.md +++ b/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: . 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 diff --git a/deps/language-sally b/deps/language-sally index de4f979032..a217a9f661 160000 --- a/deps/language-sally +++ b/deps/language-sally @@ -1 +1 @@ -Subproject commit de4f979032396b2c8fa1b5d05603c47dd96874e2 +Subproject commit a217a9f661caabd7858a17c2b556217fc39a946e diff --git a/deps/what4 b/deps/what4 index 4af08d1762..6f5e0fe9be 160000 --- a/deps/what4 +++ b/deps/what4 @@ -1 +1 @@ -Subproject commit 4af08d1762a60ff4d36adf6a98481fe5910a72d6 +Subproject commit 6f5e0fe9bef58234603ccf6914c32ea1ba2f9766 diff --git a/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs b/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs index bd52c55aa6..3a160c88dd 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs +++ b/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 diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs index 7c9177fa5b..a064e5a316 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs +++ b/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,6 +3053,7 @@ 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 @@ -3060,6 +3061,8 @@ nthPermExpr (PExprs_Cons args _) (Member_Step 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 diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs index cb87f38c86..5aaea81968 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs +++ b/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 -> diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs b/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs index 7c07886b64..6aaa2b862d 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs +++ b/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) -> diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs index e41414db15..60c7c617c9 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SAWModule.hs +++ b/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 diff --git a/saw-core-sbv/saw-core-sbv.cabal b/saw-core-sbv/saw-core-sbv.cabal index bc2cb9c205..1cc5448ab4 100644 --- a/saw-core-sbv/saw-core-sbv.cabal +++ b/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 diff --git a/saw-core/saw-core.cabal b/saw-core/saw-core.cabal index 82b90875a7..9e6d9d77d9 100644 --- a/saw-core/saw-core.cabal +++ b/saw-core/saw-core.cabal @@ -24,7 +24,7 @@ library happy >= 1.9.6 build-depends: - base == 4.*, + base >= 4.8, array, bytestring, containers, diff --git a/saw-core/src/Verifier/SAW/Change.hs b/saw-core/src/Verifier/SAW/Change.hs index aa7a4e51bb..d2af8fb388 100644 --- a/saw-core/src/Verifier/SAW/Change.hs +++ b/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) diff --git a/saw-core/src/Verifier/SAW/Conversion.hs b/saw-core/src/Verifier/SAW/Conversion.hs index 2d6e2615d4..c8b647c83c 100644 --- a/saw-core/src/Verifier/SAW/Conversion.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs index b9596827df..fe34ad88d6 100644 --- a/saw-core/src/Verifier/SAW/Rewriter.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/TermNet.hs b/saw-core/src/Verifier/SAW/TermNet.hs index 3c7a6dd101..50e112ff73 100644 --- a/saw-core/src/Verifier/SAW/TermNet.hs +++ b/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] diff --git a/saw-core/src/Verifier/SAW/UnionFind.hs b/saw-core/src/Verifier/SAW/UnionFind.hs index 1615bf1da5..6ab5da2589 100644 --- a/saw-core/src/Verifier/SAW/UnionFind.hs +++ b/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) } - diff --git a/saw-remote-api/saw-remote-api.cabal b/saw-remote-api/saw-remote-api.cabal index a903c5b63f..7cdf6084f3 100644 --- a/saw-remote-api/saw-remote-api.cabal +++ b/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, diff --git a/saw-script.cabal b/saw-script.cabal index 5f739f5146..c3e726c100 100644 --- a/saw-script.cabal +++ b/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 diff --git a/saw/SAWScript/REPL/Command.hs b/saw/SAWScript/REPL/Command.hs index df278eb073..ee9cf6f40e 100644 --- a/saw/SAWScript/REPL/Command.hs +++ b/saw/SAWScript/REPL/Command.hs @@ -8,6 +8,8 @@ Stability : provisional {-# LANGUAGE CPP, PatternGuards, FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE ViewPatterns #-} +-- TODO RGS: Do better (or at least comment why we do this) +{-# OPTIONS_GHC -fno-warn-incomplete-uni-patterns #-} module SAWScript.REPL.Command ( -- * Commands diff --git a/saw/SAWScript/REPL/Monad.hs b/saw/SAWScript/REPL/Monad.hs index 74e5b03638..294ea88e60 100644 --- a/saw/SAWScript/REPL/Monad.hs +++ b/saw/SAWScript/REPL/Monad.hs @@ -193,7 +193,7 @@ instance Functor REPL where instance Monad REPL where {-# INLINE return #-} - return x = REPL (\_ -> return x) + return = pure {-# INLINE (>>=) #-} m >>= f = REPL $ \ref -> do @@ -210,7 +210,7 @@ instance Fail.MonadFail REPL where instance Applicative REPL where {-# INLINE pure #-} - pure = return + pure x = REPL (\_ -> pure x) {-# INLINE (<*>) #-} (<*>) = ap diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 732401b9f8..aa8591b13a 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -945,7 +945,10 @@ verifyPrestate opts cc mspec globals = liftIO $ W4.setCurrentProgramLoc sym prestateLoc let lvar = Crucible.llvmMemVar (ccLLVMContext cc) - let Just mem = Crucible.lookupGlobal lvar globals + mem <- + case Crucible.lookupGlobal lvar globals of + Nothing -> fail "internal error: LLVM Memory global not found" + Just mem -> pure mem -- Allocate LLVM memory for each 'llvm_alloc' (env, mem') <- runStateT diff --git a/src/SAWScript/Lexer.x b/src/SAWScript/Lexer.x index a0814e8a43..23a02cc3f4 100644 --- a/src/SAWScript/Lexer.x +++ b/src/SAWScript/Lexer.x @@ -17,7 +17,7 @@ import SAWScript.Token import SAWScript.Position import SAWScript.Utils -import Numeric +import Numeric (readInt) import Data.List } diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs index 44ae0a8765..fc15b024fb 100644 --- a/src/SAWScript/Prover/MRSolver/Monad.hs +++ b/src/SAWScript/Prover/MRSolver/Monad.hs @@ -92,7 +92,7 @@ pattern TermsNotEq t1 t2 = TermsNotRel False t1 t2 pattern TypesNotEq :: Type -> Type -> MRFailure pattern TypesNotEq t1 t2 = TypesNotRel False t1 t2 --- | Remove the context from a 'MRFailure', i.e. remove all applications of the +-- | Remove the context from a 'MRFailure', i.e. remove all applications of the -- 'MRFailureLocalVar' and 'MRFailureCtx' constructors mrFailureWithoutCtx :: MRFailure -> MRFailure mrFailureWithoutCtx (MRFailureLocalVar x err) = @@ -259,7 +259,7 @@ coIndHypWithVar (CoIndHyp ctx f1 f2 args1 args2 invar1 invar2) nm tp = let ctx' = mrVarCtxAppend (singletonMRVarCtx nm tp) ctx (args1', args2') <- liftTermLike 0 1 (args1, args2) return (CoIndHyp ctx' f1 f2 args1' args2' invar1 invar2, var) - + -- | A map from pairs of function names to co-inductive hypotheses over those -- names type CoIndHyps = Map (FunName, FunName) CoIndHyp @@ -286,7 +286,7 @@ data DataTypeAssump deriving (Generic, Show, TermLike) instance PrettyInCtx DataTypeAssump where - prettyInCtx (IsLeft x) = prettyInCtx x >>= ppWithPrefix "Left _ _" + prettyInCtx (IsLeft x) = prettyInCtx x >>= ppWithPrefix "Left _ _" prettyInCtx (IsRight x) = prettyInCtx x >>= ppWithPrefix "Right _ _" prettyInCtx (IsNum x) = prettyInCtx x >>= ppWithPrefix "TCNum" prettyInCtx IsInf = return "TCInf" @@ -479,14 +479,14 @@ mrErrorTerm a str = liftSC2 scGlobalApply "Prelude.error" [a, err_str] -- | Create a term representing an application of @Prelude.genBVVecFromVec@, --- where the default value argument is @Prelude.error@ of the given 'T.Text' +-- where the default value argument is @Prelude.error@ of the given 'T.Text' mrGenBVVecFromVec :: Term -> Term -> Term -> T.Text -> Term -> Term -> MRM Term mrGenBVVecFromVec m a v def_err_str n len = do err_tm <- mrErrorTerm a def_err_str liftSC2 scGlobalApply "Prelude.genBVVecFromVec" [m, a, v, err_tm, n, len] -- | Create a term representing an application of @Prelude.genFromBVVec@, --- where the default value argument is @Prelude.error@ of the given 'T.Text' +-- where the default value argument is @Prelude.error@ of the given 'T.Text' mrGenFromBVVec :: Term -> Term -> Term -> Term -> T.Text -> Term -> MRM Term mrGenFromBVVec n len a v def_err_str m = do err_tm <- mrErrorTerm a def_err_str @@ -623,7 +623,9 @@ mrLambdaLift ctx t f = -- variable, which is passed as a 'Term' to the sub-computation. Note that any -- assumptions made in the sub-computation will be lost when it completes. withUVar :: LocalName -> Type -> (Term -> MRM a) -> MRM a -withUVar nm tp m = withUVars (singletonMRVarCtx nm tp) (\[v] -> m v) +withUVar nm tp m = withUVars (singletonMRVarCtx nm tp) $ \case + [v] -> m v + _ -> error "withUVar: impossible" -- | Run a MR Solver computation in a context extended with a universal variable -- and pass it the lifting (in the sense of 'incVars') of an MR Solver term diff --git a/src/SAWScript/SBVParser.hs b/src/SAWScript/SBVParser.hs index 8f16083c79..3aef0a3277 100644 --- a/src/SAWScript/SBVParser.hs +++ b/src/SAWScript/SBVParser.hs @@ -131,7 +131,10 @@ parseSBVExpr opts sc unint nodes size (SBV.SBVApp operator sbvs) = scGlobalDef sc (mkIdent preludeName (Text.pack name)) args <- mapM (parseSBV sc nodes) sbvs let inSizes = map fst args - (TFun inTyp outTyp) = typ + (inTyp, outTyp) <- + case typ of + TFun inTyp outTyp -> pure (inTyp, outTyp) + _ -> fail "parseSBVExpr: expected function type" unless (sum (typSizes inTyp) == sum (map fromIntegral inSizes)) $ do printOutLn opts Error ("ERROR parseSBVPgm: input size mismatch in " ++ name) printOutFn opts Error (show inTyp) @@ -333,7 +336,10 @@ combineOutputs sc ty xs0 = parseSBVPgm :: Options -> SharedContext -> UnintMap -> SBV.SBVPgm -> IO Term parseSBVPgm opts sc unint (SBV.SBVPgm (_version, irtype, revcmds, _vcs, _warnings, _uninterps)) = - do let (TFun inTyp outTyp) = parseIRType irtype + do (inTyp, outTyp) <- + case parseIRType irtype of + TFun inTyp outTyp -> pure (inTyp, outTyp) + _ -> fail "parseSBVPgm: expected function type" let cmds = reverse revcmds let (assigns, inputs, outputs) = partitionSBVCommands cmds let inSizes = [ size | SBVInput size _ <- inputs ] diff --git a/src/SAWScript/VerificationSummary.hs b/src/SAWScript/VerificationSummary.hs index 7a687f1396..0caae341e7 100644 --- a/src/SAWScript/VerificationSummary.hs +++ b/src/SAWScript/VerificationSummary.hs @@ -18,10 +18,10 @@ module SAWScript.VerificationSummary import Control.Lens ((^.)) import qualified Data.Map as Map import qualified Data.Set as Set -import Data.Text (Text) import Data.String import Prettyprinter import Data.Aeson (encode, (.=), Value(..), object, toJSON) +import Data.Aeson.Key (Key) import qualified Data.ByteString.Lazy.UTF8 as BLU import Data.Parameterized.Nonce @@ -111,7 +111,7 @@ thmToJSON thm = object ([ Just ploc -> [("ploc" .= plocToJSON ploc)] ) -theoremStatus :: TheoremSummary -> [(Text,Value)] +theoremStatus :: TheoremSummary -> [(Key,Value)] theoremStatus summary = case summary of ProvedTheorem stats -> [ ("status" .= ("verified" :: String)) diff --git a/src/SAWScript/X86Spec.hs b/src/SAWScript/X86Spec.hs index d11e3ef2ae..e066fd3569 100644 --- a/src/SAWScript/X86Spec.hs +++ b/src/SAWScript/X86Spec.hs @@ -1107,7 +1107,9 @@ setupGlobals opts gs fs s let alignment = noAlignment -- default to byte-aligned (FIXME, see #338) (p,mem) <- doMalloc bak GlobalAlloc Immutable "Globals" (stateMem s) sz alignment - let Just base = asNat (fst (llvmPointerView p)) + base <- case asNat (fst (llvmPointerView p)) of + Just base -> pure base + Nothing -> error "[setupGlobals] Expected concrete block number from doMalloc" mem1 <- foldM (writeGlob p) mem gs let gMap = mkGlobalMap (Map.singleton 0 p) @@ -1194,7 +1196,9 @@ debugPPReg :: (ToCrucibleType mt ~ LLVMPointerType w) => X86Reg mt -> State -> IO () debugPPReg r s = - do let Just (RV v) = lookupX86Reg r (stateRegs s) + do RV v <- case lookupX86Reg r (stateRegs s) of + Just rv -> pure rv + Nothing -> error $ "[debugPPReg] Could not find register: " ++ show r putStrLn (show r ++ " = " ++ show (ppPtr v)) _debugDumpGoals :: Opts -> IO () @@ -1282,9 +1286,16 @@ overrideMode spec opts s = -- of the stack, as it shold be, so we don't know the correct value. -- It looks like things work, if keep the orignal value instead. - let Just ip0 = lookupX86Reg X86_IP (stateRegs s) - let Just finalRegs = updateX86Reg X86_IP (const ip0) (stateRegs sf) + ip0 <- case lookupX86Reg X86_IP (stateRegs s) of + Just ip0 -> pure ip0 + Nothing -> noIPError + finalRegs <- case updateX86Reg X86_IP (const ip0) (stateRegs sf) of + Just finalRegs -> pure finalRegs + Nothing -> noIPError return sf { stateRegs = finalRegs } + where + noIPError :: a + noIPError = error "[overrideMode] Could not find instruction pointer"