Chores

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

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,15 +191,19 @@ 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
         addInvariant (index (intLit ix) tv .== e)
       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

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) })

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

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,(\\))

ivory-opts/src/Ivory/Opts/CSE.hs

@@ -4,14 +4,18 @@
 {-# LANGUAGE DeriveTraversable    #-}
 {-# LANGUAGE FlexibleContexts     #-}
 {-# 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
@@ -20,6 +24,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 +395,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

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,

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 #-}

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

ivory/src/Ivory/Language/String.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE FlexibleContexts #-}
 
 module Ivory.Language.String where