From 97cb9e28ae9cb9b937ad2278349f54c5264b640a Mon Sep 17 00:00:00 2001 From: sorki Date: Fri, 15 Dec 2023 16:11:28 +0100 Subject: [PATCH 1/9] ivory: allow newer th-abstraction --- ivory/ivory.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ivory/ivory.cabal b/ivory/ivory.cabal index f466bd90..ca287a03 100644 --- a/ivory/ivory.cabal +++ b/ivory/ivory.cabal @@ -87,7 +87,7 @@ library containers >= 0.5, monadLib >= 3.7, template-haskell >= 2.8 && <3, - th-abstraction >=0.3 && <0.5, + th-abstraction >=0.3, filepath, text, dlist >= 0.5, From ad62670f0a301fdd883520f5592adca5a63aed47 Mon Sep 17 00:00:00 2001 From: sorki Date: Fri, 15 Dec 2023 16:35:34 +0100 Subject: [PATCH 2/9] ivory-backend-c: shave off incomplete uni pattern --- ivory-backend-c/src/Ivory/Compile/C/CmdlineFrontend.hs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/ivory-backend-c/src/Ivory/Compile/C/CmdlineFrontend.hs b/ivory-backend-c/src/Ivory/Compile/C/CmdlineFrontend.hs index 4f903587..b4e58c65 100644 --- a/ivory-backend-c/src/Ivory/Compile/C/CmdlineFrontend.hs +++ b/ivory-backend-c/src/Ivory/Compile/C/CmdlineFrontend.hs @@ -37,6 +37,8 @@ import System.Directory (createDirectoryIfMissi import System.Environment (getArgs) import System.FilePath (addExtension, ()) +import qualified Data.Maybe + -- Code Generation Front End --------------------------------------------------- compile :: [Module] -> [Located Artifact] -> IO () @@ -73,7 +75,10 @@ stdoutmodules cmodules = outputmodules :: Opts -> [C.CompileUnits] -> [Located Artifact] -> IO () outputmodules opts cmodules user_artifacts = do -- Irrrefutable pattern checked above - let Just srcdir = outDir opts + let srcdir = + Data.Maybe.fromMaybe + (error "Impossible") + $ outDir opts let incldir = hdrDir srcdir let rootdir = rootDir srcdir createDirectoryIfMissing True rootdir From a3dd1b83184f28c8ab292c3d8549391bfb80eefb Mon Sep 17 00:00:00 2001 From: sorki Date: Fri, 15 Dec 2023 16:35:54 +0100 Subject: [PATCH 3/9] ivory-opts: shave off incomplete uni pattern, add TypeOperators --- ivory-opts/src/Ivory/Opts/CSE.hs | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/ivory-opts/src/Ivory/Opts/CSE.hs b/ivory-opts/src/Ivory/Opts/CSE.hs index b9ed1dfd..177b6156 100644 --- a/ivory-opts/src/Ivory/Opts/CSE.hs +++ b/ivory-opts/src/Ivory/Opts/CSE.hs @@ -4,6 +4,7 @@ {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Ivory.Opts.CSE (cseFold) where @@ -20,6 +21,7 @@ import qualified Data.IntSet as IntSet import Data.List (sort) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map +import qualified Data.Maybe import Data.Reify import Ivory.Language.Array (ixRep) import qualified Ivory.Language.Syntax as AST @@ -390,6 +392,11 @@ reconstruct (Graph subexprs root) = D.toList rootBlock (_, remap, (_, blockFacts)) = foldr (dedup usedOnce) mempty $ subexprs ++ [ (constUnique c, constExpr c) | c <- [minBound..maxBound] ] - Just rootGen = IntMap.lookup (IntMap.findWithDefault root root remap) blockFacts + rootGen = + Data.Maybe.fromMaybe + (error "No root found") + $ IntMap.lookup + (IntMap.findWithDefault root root remap) + blockFacts (((), Bindings { unusedBindings = usedOnce }), rootBlock) = runM rootGen $ Bindings Map.empty IntSet.empty 0 From 2248ef9365e39b935f2e52b5210f47ffae78e456 Mon Sep 17 00:00:00 2001 From: sorki Date: Fri, 15 Dec 2023 16:36:20 +0100 Subject: [PATCH 4/9] ivory: TypeOperators for Language.String --- ivory/src/Ivory/Language/String.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/ivory/src/Ivory/Language/String.hs b/ivory/src/Ivory/Language/String.hs index 33dabf73..382d05d3 100644 --- a/ivory/src/Ivory/Language/String.hs +++ b/ivory/src/Ivory/Language/String.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} {-# LANGUAGE FlexibleContexts #-} module Ivory.Language.String where From 04e8f8b232136da7e571eaf8a715607b262eaa06 Mon Sep 17 00:00:00 2001 From: sorki Date: Fri, 15 Dec 2023 16:43:22 +0100 Subject: [PATCH 5/9] ivory: shave off all Coroutine warnings --- ivory/src/Ivory/Language/Coroutine.hs | 65 ++++++++++++++++++++------- 1 file changed, 48 insertions(+), 17 deletions(-) diff --git a/ivory/src/Ivory/Language/Coroutine.hs b/ivory/src/Ivory/Language/Coroutine.hs index d28a858e..a4fb3397 100644 --- a/ivory/src/Ivory/Language/Coroutine.hs +++ b/ivory/src/Ivory/Language/Coroutine.hs @@ -37,6 +37,7 @@ import Control.Monad.Fix (mfix) import qualified Data.DList as D import qualified Data.IntMap as IntMap import qualified Data.Map as Map +import qualified Data.Maybe import Ivory.Language.Area import Ivory.Language.Array import Ivory.Language.Effects @@ -215,10 +216,12 @@ stateType :: AST.Type stateType = AST.TyWord AST.Word32 data BasicBlock = BasicBlock AST.Block Terminator + deriving Show type Goto = Int data Terminator = BranchTo Bool Goto | CondBranchTo AST.Expr BasicBlock BasicBlock + deriving Show joinTerminators :: BasicBlock -> BasicBlock joinTerminators (BasicBlock b (CondBranchTo cond t f)) = @@ -230,7 +233,17 @@ joinTerminators bb = bb doInline :: Goto -> [(Goto, BasicBlock)] -> [(Goto, BasicBlock)] doInline inlineLabel blocks = do - let Just (BasicBlock newStmts tgt) = lookup inlineLabel blocks + let (BasicBlock newStmts tgt) = + Data.Maybe.fromMaybe + ( error + $ "No BasicBlock found for inline label " + <> show inlineLabel + <> " in blocks " + <> show blocks + ) + $ lookup + inlineLabel + blocks let inlineBlock (BasicBlock b (BranchTo False dst)) | dst == inlineLabel = BasicBlock (b ++ newStmts) tgt inlineBlock (BasicBlock b (CondBranchTo cond tb fb)) @@ -247,8 +260,17 @@ keepUsedBlocks root blocks = sweep $ snd $ MonadLib.runM (mark root >> ref root) seen <- MonadLib.get ref label unless (label `IntMap.member` seen) $ do - let Just b = lookup label blocks - markBlock b + markBlock + $ Data.Maybe.fromMaybe + ( error + $ "Can't lookup label " + <> show label + <> " in blocks " + <> show blocks + ) + $ lookup + label + blocks ref label = MonadLib.sets_ $ IntMap.insertWith (+) label 1 markBlock (BasicBlock _ (BranchTo suspend label)) = do mark label @@ -314,9 +336,8 @@ extractLocals (AST.Call ty mvar name args) rest -- 'yieldName' is the pseudo-function call which we handle specially at this -- point using 'addYield': | name == AST.NameSym yieldName = do - -- XXX: yield takes no arguments and always returns something - let (Just var, []) = (mvar, args) - addYield ty var rest + when (args /= mempty) $ error "Coroutine yield takes no arguments" + addYield ty mvar rest | otherwise = do -- All other function calls pass through normally, but have their -- arguments run through 'updateTypedExpr' and have their results saved @@ -331,7 +352,10 @@ extractLocals (AST.Call ty mvar name args) rest rest extractLocals (AST.Local ty var initex) rest = do cont <- addLocal ty var - let AST.VarName varStr = var + let varStr = + case var of + AST.VarName n -> n + x -> error $ "Expected VarName but got " <> show x let ref = AST.VarName $ varStr ++ "_ref" initex' <- runUpdateExpr $ updateInit initex stmts @@ -347,7 +371,11 @@ extractLocals (AST.RefZero ty ref) rest = (runUpdateExpr $ AST.RefZero ty <$> updateExpr ref) >>= stmt >> rest extractLocals (AST.AllocRef _ty refvar name) rest = do - let AST.NameVar var = name -- XXX: AFAICT, AllocRef can't have a NameSym argument. + -- XXX: AFAICT, AllocRef can't have a NameSym argument. + let var = + case name of + AST.NameVar n -> n + x -> error $ "Expected NameVar but got " <> show x refvar `rewriteTo` contRef var rest extractLocals (AST.Loop _ var initEx incr b) rest = do @@ -404,13 +432,12 @@ resumeAt :: Goto -> CoroutineMonad Terminator resumeAt = return . BranchTo True contRef :: AST.Var -> CoroutineMonad AST.Expr -contRef var = do - let AST.VarName varStr = var +contRef (AST.VarName varStr) = do MonadLib.asks getCont <*> pure varStr +contRef x = error $ "Expected VarName but got " <> show x addLocal :: AST.Type -> AST.Var -> CoroutineMonad AST.Expr -addLocal ty var = do - let AST.VarName varStr = var +addLocal ty var@(AST.VarName varStr) = do MonadLib.lift $ MonadLib.put (D.singleton $ AST.Typed ty varStr, mempty) cont <- contRef var var `rewriteTo` do @@ -420,13 +447,15 @@ addLocal ty var = do stmt $ AST.Deref ty var' cont return $ AST.ExpVar var' return cont +addLocal _ty var = error $ "Expected VarName but got " <> show var -- | Generate the code to turn a @yield@ pseudo-call to a suspend and resume. -addYield :: AST.Type -> AST.Var -> CoroutineMonad Terminator -> - CoroutineMonad Terminator -addYield ty var rest = do - let AST.TyRef derefTy = ty - AST.VarName varStr = var +addYield + :: AST.Type + -> Maybe AST.Var + -> CoroutineMonad Terminator + -> CoroutineMonad Terminator +addYield (AST.TyRef derefTy) (Just var@(AST.VarName varStr)) rest = do MonadLib.lift $ MonadLib.put (D.singleton $ AST.Typed derefTy varStr, mempty) cont <- contRef var @@ -435,6 +464,8 @@ addYield ty var rest = do let resume arg = [AST.RefCopy derefTy cont arg] MonadLib.lift $ MonadLib.put (mempty, Map.singleton after resume) resumeAt after +addYield _ Nothing _ = error "Coroutine yield always returns something" +addYield t _ _ = error $ "Got wrong type as input for addYield: " <> show t setBreakLabel :: Terminator -> CoroutineMonad a -> CoroutineMonad a setBreakLabel label m = do From 53dca612c4ff49fb6d11da9ded9422564599d2fe Mon Sep 17 00:00:00 2001 From: sorki Date: Fri, 15 Dec 2023 17:15:11 +0100 Subject: [PATCH 6/9] ivory-opts: guard Control.Applicative imports using CPP, MIN_VERSION_base(4,18,0) --- ivory-opts/src/Ivory/Opts/CFG.hs | 2 ++ ivory-opts/src/Ivory/Opts/CSE.hs | 3 +++ 2 files changed, 5 insertions(+) diff --git a/ivory-opts/src/Ivory/Opts/CFG.hs b/ivory-opts/src/Ivory/Opts/CFG.hs index 80b55b31..bf81d274 100644 --- a/ivory-opts/src/Ivory/Opts/CFG.hs +++ b/ivory-opts/src/Ivory/Opts/CFG.hs @@ -29,7 +29,9 @@ import qualified Ivory.Language.Syntax.AST as I import qualified Ivory.Language.Syntax.Type as I import qualified Data.Graph.Inductive as G +#if !MIN_VERSION_base(4,18,0) import Control.Applicative (liftA2) +#endif import System.FilePath import Data.Maybe import Data.List (find,(\\)) diff --git a/ivory-opts/src/Ivory/Opts/CSE.hs b/ivory-opts/src/Ivory/Opts/CSE.hs index 177b6156..dd71379f 100644 --- a/ivory-opts/src/Ivory/Opts/CSE.hs +++ b/ivory-opts/src/Ivory/Opts/CSE.hs @@ -6,13 +6,16 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE CPP #-} module Ivory.Opts.CSE (cseFold) where import Prelude () import Prelude.Compat +#if !MIN_VERSION_base(4,18,0) import Control.Applicative (liftA2) +#endif import qualified Data.DList as D import Data.IntMap.Strict (IntMap) import qualified Data.IntMap.Strict as IntMap From dd74230b0793596ce51fdd01e4ab6f771e4d9249 Mon Sep 17 00:00:00 2001 From: sorki Date: Fri, 15 Dec 2023 18:32:10 +0100 Subject: [PATCH 7/9] ivory-model-check: shave off incomplete uni patterns --- .../src/Ivory/ModelCheck/Ivory2CVC4.hs | 20 ++++++++++++------- .../src/Ivory/ModelCheck/Monad.hs | 8 +++++--- 2 files changed, 18 insertions(+), 10 deletions(-) diff --git a/ivory-model-check/src/Ivory/ModelCheck/Ivory2CVC4.hs b/ivory-model-check/src/Ivory/ModelCheck/Ivory2CVC4.hs index 3c642f2b..036b98b7 100644 --- a/ivory-model-check/src/Ivory/ModelCheck/Ivory2CVC4.hs +++ b/ivory-model-check/src/Ivory/ModelCheck/Ivory2CVC4.hs @@ -13,7 +13,7 @@ import Prelude () import Prelude.Compat hiding (exp) -import Control.Monad (forM, forM_, void, when) +import Control.Monad (forM, forM_, void) import Data.List (nub) import qualified Data.Map as M import Data.Maybe @@ -191,7 +191,9 @@ toInit ty init = _ -> return $ intLit 0 I.InitExpr t exp -> toExpr t exp I.InitArray is _ -> do - let (I.TyArr k t) = ty + let (k, t) = case ty of + I.TyArr k t -> (k, t) + x -> error $ "Expected I.TyArr but got " <> show x tv <- fmap var $ incReservedVar =<< toType ty forM_ (zip [0..] is) $ \ (ix,i) -> do e <- toInit t i @@ -199,7 +201,9 @@ toInit ty init = return tv I.InitStruct fs -> do tv <- fmap var $ incReservedVar =<< toType ty - let (I.TyStruct s) = ty + let s = case ty of + I.TyStruct s -> s + x -> error $ "Expected I.TyStruct but got " <> show x forM_ fs $ \ (f, i) -> do structs <- getStructs case M.lookup s structs >>= lookupField f of @@ -309,10 +313,12 @@ toIfTE ens cond blk0 blk1 = do trs <- runBranch b blk0 frs <- runBranch (not' b) blk1 forM_ (M.toList (M.unionWith (++) trs frs)) $ \ ((t, r), nub -> vs) -> do - when (length vs == 2) $ do - r' <- addEnvVar t r - let [tv,fv] = vs - addInvariant $ (b .=> (var r' .== var tv)) .&& (not' b .=> (var r' .== var fv)) + case vs of + [tv, fv] -> do + r' <- addEnvVar t r + let [tv,fv] = vs + addInvariant $ (b .=> (var r' .== var tv)) .&& (not' b .=> (var r' .== var fv)) + _ -> pure () where runBranch b blk = withLocalRefs $ inBranch b $ do mapM_ (toBody ens) blk -- Body under the invariant diff --git a/ivory-model-check/src/Ivory/ModelCheck/Monad.hs b/ivory-model-check/src/Ivory/ModelCheck/Monad.hs index 2c5542eb..a0183320 100644 --- a/ivory-model-check/src/Ivory/ModelCheck/Monad.hs +++ b/ivory-model-check/src/Ivory/ModelCheck/Monad.hs @@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} @@ -214,8 +215,9 @@ snapshotRefs :: ModelCheck () snapshotRefs = do rs <- getRefs b <- symCond <$> get - forM_ (M.toList rs) $ \ ((t,r),[v]) -> - updateStReturnRef t r b v + forM_ (M.toList rs) $ \case + ((t,r),[v]) -> updateStReturnRef t r b v + x -> error $ "Expected ((t, r), [v]) but got " <> show x getStructs :: ModelCheck (M.Map I.Sym I.Struct) getStructs = do @@ -230,7 +232,7 @@ addStruct s = do I.Abstract n _ -> n let st' = st { symStructs = M.insert nm s (symStructs st) } set st' - + updateStRef :: I.Type -> Var -> Var -> ModelCheck () updateStRef t v v' = sets_ (\st -> st { symRefs = M.insert (t,v) [v'] (symRefs st) }) From 701e6dfb80c313c31bad18a1576e84657e3f40f1 Mon Sep 17 00:00:00 2001 From: sorki Date: Fri, 15 Dec 2023 18:32:51 +0100 Subject: [PATCH 8/9] ivory: TypeOperators for BitData --- ivory/src/Ivory/Language/BitData/BitData.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/ivory/src/Ivory/Language/BitData/BitData.hs b/ivory/src/Ivory/Language/BitData/BitData.hs index 0e1a2536..5cc24bf0 100644 --- a/ivory/src/Ivory/Language/BitData/BitData.hs +++ b/ivory/src/Ivory/Language/BitData/BitData.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ConstraintKinds #-} From e9c572a1004625abb36912983f0f508aa4903168 Mon Sep 17 00:00:00 2001 From: sorki Date: Fri, 15 Dec 2023 18:40:54 +0100 Subject: [PATCH 9/9] ivory-model-check: shave off incomplete uni patterns in tests --- ivory-model-check/test/Test.hs | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/ivory-model-check/test/Test.hs b/ivory-model-check/test/Test.hs index 4e8e78fb..06665ab5 100644 --- a/ivory-model-check/test/Test.hs +++ b/ivory-model-check/test/Test.hs @@ -79,32 +79,36 @@ testArgs :: Args testArgs = initArgs { printQuery = False, printEnv = False } mkSuccess :: Def p -> [Module] -> TestTree -mkSuccess d@(~(I.DefProc p)) mods = testCase (I.procSym p) $ do +mkSuccess d@(I.DefProc p) mods = testCase (I.procSym p) $ do r <- modelCheck testArgs mods d let msg = printf "Expected: Safe\nActual: %s" (showResult r) assertBool msg (isSafe r) +mkSuccess _ _ = error "Absurd" mkSuccessInline :: Def p -> [Module] -> TestTree -mkSuccessInline d@(~(I.DefProc p)) mods = testCase (I.procSym p) $ do +mkSuccessInline d@(I.DefProc p) mods = testCase (I.procSym p) $ do r <- modelCheck (testArgs { inlineCall = True }) mods d let msg = printf "Expected: Safe\nActual: %s" (showResult r) assertBool msg (isSafe r) +mkSuccessInline _ _ = error "Absurd" mkFailure :: Def p -> [Module] -> TestTree -mkFailure d@(~(I.DefProc p)) mods = testCase (I.procSym p) $ do +mkFailure d@(I.DefProc p) mods = testCase (I.procSym p) $ do r <- modelCheck testArgs mods d let msg = printf "Expected: Unsafe\nActual: %s" (showResult r) assertBool msg (isUnsafe r) +mkFailure _ _ = error "Absurd" mkNotError :: Def p -> [Module] -> TestTree -mkNotError d@(~(I.DefProc p)) mods = testCase (I.procSym p) $ do +mkNotError d@(I.DefProc p) mods = testCase (I.procSym p) $ do r <- modelCheck testArgs mods d let msg = printf "Expected: anything but Error\nActual: %s" (showResult r) assertBool msg (not $ isError r) +mkNotError _ _ = error "Absurd" -------------------------------------------------------------------------------- -- test modules