ivory-opts 0.1.0.3 → 0.1.0.4
raw patch · 7 files changed
+344/−223 lines, 7 filesdep ~basedep ~ivory
Dependency ranges changed: base, ivory
Files
- ivory-opts.cabal +3/−3
- src/Ivory/Opts/AssertFold.hs +14/−11
- src/Ivory/Opts/CSE.hs +34/−26
- src/Ivory/Opts/ConstFold.hs +21/−14
- src/Ivory/Opts/SanityCheck.hs +92/−86
- src/Ivory/Opts/TypeCheck.hs +137/−81
- src/Ivory/Opts/Utils.hs +43/−2
ivory-opts.cabal view
@@ -2,7 +2,7 @@ -- see http://haskell.org/cabal/users-guide/ name: ivory-opts-version: 0.1.0.3+version: 0.1.0.4 author: Galois, Inc. maintainer: leepike@galois.com category: Language@@ -16,7 +16,7 @@ source-repository this type: git location: https://github.com/GaloisInc/ivory- tag: hackage-opts-0103+ tag: hackage-0.1.0.4 library exposed-modules: Ivory.Opts.AssertFold,@@ -34,7 +34,7 @@ other-modules: Ivory.Opts.Utils - build-depends: base >= 4.6 && < 5,+ build-depends: base >= 4.7 && < 5, base-compat, containers, data-reify >=0.6,
src/Ivory/Opts/AssertFold.hs view
@@ -1,7 +1,7 @@+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE TypeSynonymInstances #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeSynonymInstances #-} -- | Fold over expressions that collect up assertions about the expressions. @@ -13,15 +13,16 @@ , freshVar ) where -import Prelude ()-import Prelude.Compat+import Prelude ()+import Prelude.Compat -import MonadLib (StateM(..),StateT,Id,runStateT,runId)-import qualified Data.DList as D+import qualified Data.DList as D+import qualified Ivory.Language.Array as I+import qualified Ivory.Language.Syntax.AST as I+import qualified Ivory.Language.Syntax.Type as I import Ivory.Opts.Utils-import qualified Ivory.Language.Array as I-import qualified Ivory.Language.Syntax.AST as I-import qualified Ivory.Language.Syntax.Type as I+import MonadLib (Id, StateM (..), StateT, runId,+ runStateT) -------------------------------------------------------------------------------- -- Monad and types.@@ -142,6 +143,8 @@ I.RefCopy ty e0 e1 -> do ef ty e0 ef ty e1 insert stmt+ I.RefZero ty e0 -> do ef ty e0+ insert stmt I.AllocRef{} -> insert stmt I.Forever blk -> do blk' <- runFreshStmts ef blk insert (I.Forever blk')@@ -156,7 +159,7 @@ I.InitZero -> return () I.InitExpr ty e -> ef ty e I.InitStruct inits -> mapM_ (efInit . snd) inits- I.InitArray inits -> mapM_ efInit inits+ I.InitArray inits _ -> mapM_ efInit inits --------------------------------------------------------------------------------
src/Ivory/Opts/CSE.hs view
@@ -1,29 +1,31 @@ {-# OPTIONS_GHC -fno-warn-orphans #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE DeriveFoldable #-}-{-# LANGUAGE DeriveFunctor #-}-{-# LANGUAGE DeriveTraversable #-}-{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} module Ivory.Opts.CSE (cseFold) where -import Prelude ()-import Prelude.Compat+import Prelude ()+import Prelude.Compat -import qualified Data.DList as D-import Data.IntMap.Strict (IntMap)-import qualified Data.IntMap.Strict as IntMap-import Data.IntSet (IntSet)-import qualified Data.IntSet as IntSet-import Data.List (sort)-import Data.Map.Strict (Map)-import qualified Data.Map.Strict as Map-import Data.Reify-import Ivory.Language.Array (ixRep)+import Control.Applicative (liftA2)+import qualified Data.DList as D+import Data.IntMap.Strict (IntMap)+import qualified Data.IntMap.Strict as IntMap+import Data.IntSet (IntSet)+import qualified Data.IntSet as IntSet+import Data.List (sort)+import Data.Map.Strict (Map)+import qualified Data.Map.Strict as Map+import Data.Reify+import Ivory.Language.Array (ixRep) import qualified Ivory.Language.Syntax as AST-import MonadLib (WriterT, StateT, Id, get, set, sets, sets_, put, collect, lift, runM)-import System.IO.Unsafe (unsafePerformIO)+import MonadLib (Id, StateT, WriterT, collect, get, lift,+ put, runM, set, sets, sets_)+import System.IO.Unsafe (unsafePerformIO) -- | Find each common sub-expression and extract it to a new variable, -- making any sharing explicit. However, this function should never move@@ -37,8 +39,8 @@ -- | Variable assignments emitted so far. data Bindings = Bindings { availableBindings :: (Map (Unique, AST.Type) Int)- , unusedBindings :: IntSet- , totalBindings :: Int+ , unusedBindings :: IntSet+ , totalBindings :: Int } -- | A monad for emitting both source-level statements as well as@@ -141,6 +143,7 @@ | StmtCall AST.Type (Maybe AST.Var) AST.Name [AST.Typed t] | StmtLocal AST.Type AST.Var (InitF t) | StmtRefCopy AST.Type t t+ | StmtRefZero AST.Type t | StmtLoop Integer AST.Var t (LoopIncrF t) t | StmtForever t | Block [t]@@ -155,7 +158,7 @@ = InitZero | InitExpr AST.Type t | InitStruct [(String, InitF t)]- | InitArray [InitF t]+ | InitArray [InitF t] Bool deriving (Show, Eq, Ord, Functor) instance MuRef AST.Stmt where@@ -172,6 +175,7 @@ AST.Call ty mv nm args -> StmtCall ty mv nm <$> traverse (\ (AST.Typed argTy argEx) -> AST.Typed argTy <$> child argEx) args AST.Local ty var initex -> StmtLocal ty var <$> mapInit initex AST.RefCopy ty dst src -> StmtRefCopy ty <$> child dst <*> child src+ AST.RefZero ty dst -> StmtRefZero ty <$> child dst AST.Loop m var ex incr lb -> StmtLoop m var <$> child ex <*> mapIncr incr <*> child lb AST.Forever lb -> StmtForever <$> child lb -- These kinds of statements can't contain other statements or expressions.@@ -183,7 +187,7 @@ mapInit AST.InitZero = pure InitZero mapInit (AST.InitExpr ty ex) = InitExpr ty <$> child ex mapInit (AST.InitStruct fields) = InitStruct <$> traverse (\ (nm, i) -> (,) nm <$> mapInit i) fields- mapInit (AST.InitArray elements) = InitArray <$> traverse mapInit elements+ mapInit (AST.InitArray elements b) = liftA2 InitArray (traverse mapInit elements) (pure b) mapIncr (AST.IncrTo ex) = IncrTo <$> child ex mapIncr (AST.DecrTo ex) = DecrTo <$> child ex @@ -210,6 +214,7 @@ StmtLocal ty var initex -> stmt $ AST.Local ty var <$> toInit initex -- XXX: See deref and store comments above. StmtRefCopy ty dst src -> stmt $ AST.RefCopy ty <$> expr dst (AST.TyRef ty) <*> expr src (AST.TyConstRef ty)+ StmtRefZero ty dst -> stmt $ AST.RefZero ty <$> expr dst (AST.TyRef ty) StmtLoop m var ex incr lb -> stmt $ AST.Loop m var <$> expr ex ixRep <*> toIncr incr <*> genBlock (block lb) StmtForever lb -> stmt $ AST.Forever <$> genBlock (block lb) Block stmts -> mapM_ block stmts@@ -218,7 +223,7 @@ toInit InitZero = pure AST.InitZero toInit (InitExpr ty ex) = AST.InitExpr ty <$> expr ex ty toInit (InitStruct fields) = AST.InitStruct <$> traverse (\ (nm, i) -> (,) nm <$> toInit i) fields- toInit (InitArray elements) = AST.InitArray <$> traverse toInit elements+ toInit (InitArray elements b') = liftA2 AST.InitArray (traverse toInit elements) (pure b') toIncr (IncrTo ex) = AST.IncrTo <$> expr ex ixRep toIncr (DecrTo ex) = AST.DecrTo <$> expr ex ixRep @@ -382,6 +387,9 @@ -- NOTE: `dedup` needs to merge the constants in first, which means -- that as long as this is a `foldr`, they need to be appended after -- `subexprs`. Don't try to optimize this by re-ordering the list.- (_, remap, (_, blockFacts)) = foldr (dedup usedOnce) mempty $ subexprs ++ [ (constUnique c, constExpr c) | c <- [minBound..maxBound] ]+ (_, remap, (_, blockFacts)) =+ foldr (dedup usedOnce) mempty+ $ subexprs ++ [ (constUnique c, constExpr c) | c <- [minBound..maxBound] ] Just rootGen = IntMap.lookup (IntMap.findWithDefault root root remap) blockFacts- (((), Bindings { unusedBindings = usedOnce }), rootBlock) = runM rootGen $ Bindings Map.empty IntSet.empty 0+ (((), Bindings { unusedBindings = usedOnce }), rootBlock) =+ runM rootGen $ Bindings Map.empty IntSet.empty 0
src/Ivory/Opts/ConstFold.hs view
@@ -1,5 +1,5 @@ {-# LANGUAGE PatternGuards #-}-{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE Rank2Types #-} -- -- Constant folder.@@ -12,18 +12,19 @@ ( constFold ) where -import Ivory.Opts.ConstFoldComp+import Ivory.Opts.ConstFoldComp -import qualified Ivory.Language.Array as I-import qualified Ivory.Language.Syntax as I-import Ivory.Language.Cast (toMaxSize, toMinSize)+import qualified Ivory.Language.Array as I+import Ivory.Language.Cast (toMaxSize, toMinSize)+import qualified Ivory.Language.Syntax as I -import Control.Arrow (second)-import Data.Map (Map)-import qualified Data.Map as Map-import Data.Maybe-import qualified Data.DList as D-import MonadLib (StateM(..),Id,StateT,runId,runStateT)+import Control.Arrow (second)+import qualified Data.DList as D+import Data.Map (Map)+import qualified Data.Map as Map+import Data.Maybe+import MonadLib (Id, StateM (..), StateT, runId,+ runStateT) -------------------------------------------------------------------------------- -- Constant folding@@ -112,6 +113,9 @@ I.RefCopy t e0 e1 -> do copies <- get return $ D.singleton $ I.RefCopy t (opt copies t e0) (opt copies t e1)+ I.RefZero t e0 -> do+ copies <- get+ return $ D.singleton $ I.RefZero t (opt copies t e0) I.AllocRef{} -> return $ D.singleton stmt I.Loop m v e incr blk' -> do copies <- get@@ -135,9 +139,12 @@ constFoldInits :: CopyMap -> I.Init -> I.Init constFoldInits _ I.InitZero = I.InitZero-constFoldInits copies (I.InitExpr ty expr) = I.InitExpr ty $ cf copies ty expr-constFoldInits copies (I.InitStruct i) = I.InitStruct $ map (second (constFoldInits copies)) i-constFoldInits copies (I.InitArray i) = I.InitArray $ map (constFoldInits copies) i+constFoldInits copies (I.InitExpr ty expr) =+ I.InitExpr ty $ cf copies ty expr+constFoldInits copies (I.InitStruct i) =+ I.InitStruct $ map (second (constFoldInits copies)) i+constFoldInits copies (I.InitArray i b) =+ I.InitArray (map (constFoldInits copies) i) b -------------------------------------------------------------------------------- -- Expressions
src/Ivory/Opts/SanityCheck.hs view
@@ -1,9 +1,9 @@-{-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE ViewPatterns #-}-{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -fno-warn-orphans #-} @@ -17,28 +17,34 @@ module Ivory.Opts.SanityCheck ( sanityCheck- , showErrors+ , showSanityChkModule , existErrors- , Results()- , render+ , dupDefs+ , showDupDefs ) where -import Prelude ()-import Prelude.Compat+import Prelude ()+import Prelude.Compat -import Control.Monad (unless)+import System.IO (hPutStrLn, stderr)++import Control.Monad (unless)+import qualified Data.List as L import qualified Data.Map as M-import MonadLib- (WriterM(..),StateM(..),sets_,runId,runStateT,runWriterT- ,Id,StateT,WriterT)+import MonadLib (Id, StateM (..),+ StateT, WriterM (..),+ WriterT, runId,+ runStateT, runWriterT,+ sets_) import Text.PrettyPrint -import Ivory.Language.Syntax.Concrete.Location-import Ivory.Language.Syntax.Concrete.Pretty import qualified Ivory.Language.Array as I import qualified Ivory.Language.Syntax.AST as I+import Ivory.Language.Syntax.Concrete.Location+import Ivory.Language.Syntax.Concrete.Pretty import qualified Ivory.Language.Syntax.Names as I import qualified Ivory.Language.Syntax.Type as I+import Ivory.Opts.Utils -------------------------------------------------------------------------------- -- Errors types@@ -47,50 +53,31 @@ | TypeError String I.Type I.Type deriving (Show, Eq) -data Warning = TypeWarning String I.Type I.Type- deriving (Show, Eq)--data Results = Results- { errors :: [Located Error]- , _warnings :: [Located Warning]- } deriving (Show, Eq)+type Result = Located Error -instance Monoid Results where- mempty = Results [] []- Results a0 b0 `mappend` Results a1 b1 = Results (a0 ++ a1) (b0 ++ b1)+type Results = [Located Error] -- | Are there any errors from typechecking?-existErrors :: Results -> Bool-existErrors = not . null . errors+existErrors :: ModResult Result -> Bool+existErrors (ModResult _ ls) = or (map go ls)+ where+ go (SymResult _ res) = not (null res) showError :: Error -> Doc showError err = case err of UnboundValue x -> text "Unbound value:" <+> quotes (text x) TypeError x actual expected- -> typeMsg x actual expected--typeMsg :: String -> I.Type -> I.Type -> Doc-typeMsg x actual expected =- quotes (text x) <+> text "has type:"- $$ nest 4 (quotes (pretty actual))- $$ text "but is used with type:"- $$ nest 4 (quotes (pretty expected))--showWithLoc :: (a -> Doc) -> Located a -> Doc-showWithLoc sh (Located loc a) = pretty loc <> text ":" $$ nest 2 (sh a)---- | Given a procedure name, show all the typechecking results for that procedure.-showErrors :: String -> Results -> Doc-showErrors procName res- = mkOut procName "ERROR" (showWithLoc showError) (errors res)+ -> quotes (text x) <+> text "has type:"+ $$ nest 4 (quotes (pretty actual))+ $$ text "but is used with type:"+ $$ nest 4 (quotes (pretty expected)) -mkOut :: String -> String -> (a -> Doc) -> [a] -> Doc-mkOut _ _ _ [] = empty-mkOut sym kind sh ls = nm $$ nest 4 (vcat (map go ls)) $$ empty+showSanityChkModule :: ModResult Result -> IO ()+showSanityChkModule res = showModErrs go res where- go x = text kind <> text ":" <+> sh x- nm = text "*** Procedure" <+> text sym+ go :: Result -> Doc+ go = showWithLoc showError -------------------------------------------------------------------------------- -- Writer Monad@@ -144,7 +131,7 @@ putError :: Error -> SCResults () putError err = do loc <- getStLoc- put (Results [err `at` loc] [])+ put [err `at` loc] runSCResults :: SCResults a -> (a, Results) runSCResults tc = fst $ runId $ runStateT (St NoLoc M.empty) $ runWriterT (unTC tc)@@ -165,33 +152,68 @@ getType :: I.Typed a -> I.Type getType (I.Typed t _) = t -sanityCheck :: [I.Module] -> I.Module -> Results-sanityCheck deps this@(I.Module {..})- = mconcat $ map (sanityCheckProc topLevel) $ getVisible modProcs+sanityCheck :: [I.Module] -> [ModResult Result]+sanityCheck ms = map goMod ms where- getVisible v = I.public v ++ I.private v+ goMod m =+ ModResult (I.modName m)+ (concatMap goProc (getVisible I.modProcs m)) + goProc p =+ let scp = sanityCheckProc topLevel p in+ if null scp then [] else [SymResult (I.procSym p) scp]+ topLevel :: M.Map String MaybeType- topLevel = M.fromList- $ concat [ procs m+ topLevel = M.fromList $+ concat [ procs m ++ imports m ++ externs m ++ areas m ++ importAreas m- | m <- this:deps+ | m <- ms ] - procs m = [ (procSym, Defined $ I.TyProc procRetTy (map getType procArgs) )- | I.Proc {..} <- getVisible $ I.modProcs m ]- imports m = [ (importSym, Imported)- | I.Import {..} <- I.modImports m ]- externs m = [ (externSym, Defined externType)- | I.Extern {..} <- I.modExterns m ]- areas m = [ (areaSym, Defined areaType)- | I.Area {..} <- getVisible $ I.modAreas m ]- importAreas m = [ (aiSym, Imported)- | I.AreaImport {..} <- I.modAreaImports m ]+showDupDefs :: [String] -> IO ()+showDupDefs dups =+ if null dups then return ()+ else hPutStrLn stderr $ render (vcat (map docDups dups) $$ empty)+ where+ docDups x = text "*** WARNING"+ <> colon+ <+> quotes (text x)+ <+> text "has multiple definitions." +-- Are there any duplicated definitions?+dupDefs :: [I.Module] -> [String]+dupDefs ms = map fst dups+ where+ dups :: [(String, MaybeType)]+ -- XXX doesn't guarantee that there are multiply defined defs, but at+ -- least sanity checks it.+ dups = defs L.\\ (L.nubBy (\a b -> (fst a == fst b) && (snd a /= snd b))) defs+ where+ defs = concat [ procs m ++ areas m ++ structs m | m <- ms ]++getVisible :: (t -> I.Visible a) -> t -> [a]+getVisible acc m =+ let ps = acc m in+ I.public ps ++ I.private ps++procs, areas, imports, externs, importAreas, structs :: I.Module -> [(I.Sym, MaybeType)]+procs m = [ (procSym, Defined $ I.TyProc procRetTy (map getType procArgs) )+ | I.Proc {..} <- getVisible I.modProcs m ]+areas m = [ (areaSym, Defined areaType)+ | I.Area {..} <- getVisible I.modAreas m ]+imports m = [ (importSym, Imported)+ | I.Import {..} <- I.modImports m ]+externs m = [ (externSym, Defined externType)+ | I.Extern {..} <- I.modExterns m ]+importAreas m = [ (aiSym, Imported)+ | I.AreaImport {..} <- I.modAreaImports m ]+-- Not an imported type, but we don't need hte type here.+structs m = [ (nm, Imported)+ | (I.Struct nm _) <- getVisible I.modStructs m ]+ -- | Sanity Check a procedure. Check for unbound and ill-typed values sanityCheckProc :: M.Map String MaybeType -> I.Proc -> Results sanityCheckProc env (I.Proc {..}) = snd $ runSCResults $ do@@ -222,10 +244,12 @@ case mv of Nothing -> return () Just v -> varString v `hasType` t- I.Local t v _+ I.Local t v _init -> varString v `hasType` t I.RefCopy _ e1 e2 -> checkExpr e1 >> checkExpr e2+ I.RefZero _ e1+ -> checkExpr e1 I.AllocRef t v _ -> varString v `hasType` t I.Loop _ v _ _ stmts@@ -310,22 +334,4 @@ -> text "CArray" <+> pretty t I.TyOpaque -> text "Opaque"------------------------------------------------------------------------------------- Unused for now.---- showWarning :: Warning -> Doc--- showWarning w = case w of--- TypeWarning x actual expected--- -> typeMsg x actual expected---- -- | Given a procedure name, show all the typechecking results for that procedure.--- showWarnings :: String -> Results -> Doc--- showWarnings procName res--- = mkOut procName "WARNING" (showWithLoc showWarning) (warnings res)---- putWarn :: Warning -> SCResults ()--- putWarn warn = do--- loc <- getStLoc--- put (Results [] [warn `at` loc])
src/Ivory/Opts/TypeCheck.hs view
@@ -1,12 +1,13 @@-{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE CPP #-}+{-# LANGUAGE MultiParamTypeClasses #-} -- -- Type check to ensure there are no empty blocks in procedures, for non-void -- procedures, a value is returned, there is no dead code (code after a return--- statement), no field in a struct is initialized twice.+-- statement), no field in a struct is initialized twice, and that arrays have+-- the right number of elements initialized. -- -- Copyright (C) 2014, Galois, Inc. -- All rights reserved.@@ -14,24 +15,26 @@ module Ivory.Opts.TypeCheck ( typeCheck- , showErrors- , showWarnings+ , showTyChkModule+ , existWarnOrErrors , existErrors- , Results() ) where -import Prelude ()-import Prelude.Compat+import Prelude ()+import Prelude.Compat hiding (init) -import Control.Monad (when,void)-import MonadLib- (WriterM(..),StateM(..),runId,runStateT,runWriterT,Id,StateT,WriterT)-import Data.List (nub)+import Control.Monad (unless, void, when)+import Data.List (nub)+import MonadLib (Id, StateM (..),+ StateT, WriterM (..),+ WriterT, runId,+ runStateT, runWriterT)+import Text.PrettyPrint -import Ivory.Language.Syntax.Concrete.Location-import Ivory.Language.Syntax.Concrete.Pretty-import qualified Ivory.Language.Syntax.AST as I-import qualified Ivory.Language.Syntax.Type as I+import qualified Ivory.Language.Syntax.AST as I+import Ivory.Language.Syntax.Concrete.Location+import qualified Ivory.Language.Syntax.Type as I+import Ivory.Opts.Utils -------------------------------------------------------------------------------- -- Errors types@@ -39,65 +42,81 @@ data RetError = RetError String [Error] deriving (Show, Read, Eq) -data Warning = IfTEWarn- | LoopWarn- | VoidEmptyBody+data Warning =+ IfTEWarn+ | LoopWarn+ | VoidEmptyBody+ | ArrayInitUnusedWarning+ | ArrayInitPartialWarning deriving (Show, Read, Eq) -data Error = EmptyBody- | NoRet- | DeadCode- | DoubleInit+data Error =+ EmptyBody+ | NoRet+ | DeadCode+ | DoubleInit deriving (Show, Read, Eq) -data Results = Results- { errs :: [Located Error]- , warnings :: [Located Warning]- } deriving (Show, Read, Eq)--instance Monoid Results where- mempty = Results [] []- Results a0 b0 `mappend` Results a1 b1 = Results (a0 ++ a1) (b0 ++ b1)+data Result =+ LocError (Located Error)+ | LocWarn (Located Warning)+ deriving (Show, Read, Eq) --- | Are there any errors from typechecking?-existErrors :: Results -> Bool-existErrors = not . null . errs+type Results = [Result] -showError :: Error -> String-showError err = case err of- EmptyBody -> "Procedure contains no statements!"- NoRet -> "No return statment and procedure has a non-void type."- DeadCode -> "Unreachable statements after a return."- DoubleInit -> "Repeated initialization of a struct field."+allResults :: ModResult Result -> [Result]+allResults (ModResult _ ls) = concatMap go ls+ where+ go (SymResult _ res) = res -showWarning :: Warning -> String-showWarning w = case w of- IfTEWarn- -> "One branch of an if-then-else statement contains a return statement.\nStatements after the if-the-else block are not reachable on all control paths."- LoopWarn- -> "Statements after the loop may be unreachable due to a return statement within the loop."- VoidEmptyBody- -> "Procedure with void return type has no statements."+-- | Are there any errors from typechecking the module?+existErrors :: ModResult Result -> Bool+existErrors m =+ not (null (f (allResults m)))+ where+ f = filter (\a -> case a of LocError{} -> True; LocWarn{} -> False) -showWithLoc :: (a -> String) -> Located a -> String-showWithLoc sh (Located loc a) = prettyPrint (pretty loc) ++ ": " ++ sh a+-- | Are there any errors or warnings from typechecking the module?+existWarnOrErrors :: ModResult Result -> Bool+existWarnOrErrors m = not (null (allResults m)) --- | Given a procedure name, show all the typechecking results for that procedure.-showErrors :: String -> Results -> [String]-showErrors procName res- = mkOut procName "ERROR" (showWithLoc showError) (errs res)+showError :: Error -> Doc+showError err =+ text "ERROR"+ <+> text (case err of+ EmptyBody+ -> "Procedure contains no statements!"+ NoRet+ -> "No return statement and procedure has a non-void type."+ DeadCode+ -> "Unreachable statements after a return."+ DoubleInit+ -> "Repeated initialization of a struct field."+ ) --- | Given a procedure name, show all the typechecking results for that procedure.-showWarnings :: String -> Results -> [String]-showWarnings procName res- = mkOut procName "WARNING" (showWithLoc showWarning) (warnings res)+showWarning :: Warning -> Doc+showWarning w =+ text "WARNING"+ <+> text (case w of+ IfTEWarn+ -> "One branch of an if-then-else statement contains a return statement. Statements after the if-the-else block are not reachable on all control paths."+ LoopWarn+ -> "Statements after the loop may be unreachable due to a return statement within the loop."+ VoidEmptyBody+ -> "Procedure with void return type has no statements."+ ArrayInitPartialWarning+ -> "Array partially initialized."+ ArrayInitUnusedWarning+ -> "Array contains unused initializers."+ ) -mkOut :: String -> String -> (a -> String) -> [a] -> [String]-mkOut _ _ _ [] = []-mkOut sym kind sh ls = nm : map go ls+-- Boolean says whether to show warnings (True) or not.+showTyChkModule :: Bool -> ModResult Result -> IO ()+showTyChkModule b res = showModErrs go res where- go x = " " ++ kind ++ ": " ++ sh x- nm = "*** Procedure " ++ sym+ go :: Result -> Doc+ go (LocError e) = showWithLoc showError e+ go (LocWarn w) = if b then showWithLoc showWarning w else empty -------------------------------------------------------------------------------- -- Writer Monad@@ -115,22 +134,37 @@ putError :: Error -> TCResults () putError err = do loc <- get- put (Results [err `at` loc] [])+ put [LocError (err `at` loc)] putWarn :: Warning -> TCResults () putWarn warn = do loc <- get- put (Results [] [warn `at` loc])+ put [LocWarn (warn `at` loc)] runTCResults :: TCResults a -> (a, Results) runTCResults tc = fst $ runId $ runStateT NoLoc $ runWriterT (unTC tc) -------------------------------------------------------------------------------- --- | Type Check a procedure.-typeCheck :: I.Proc -> Results-typeCheck p = snd $ runTCResults $ tyChk (I.procRetTy p) (I.procBody p)+-- | Type Check a module.+typeCheck :: I.Module -> ModResult Result+typeCheck m =+ ModResult (I.modName m)+ (concatMap procTC allProcs ++ concatMap areaTC allAreas) + where+ allProcs = let ps = I.modProcs m in I.public ps ++ I.private ps+ procTC p =+ if null res then [] else [SymResult (I.procSym p) res]+ where+ res = snd $ runTCResults $ tyChk (I.procRetTy p) (I.procBody p)++ allAreas = let as = I.modAreas m in I.public as ++ I.private as+ areaTC a =+ if null res then [] else [SymResult (I.areaSym a) res]+ where+ res = snd $ runTCResults $ checkInit (Just (I.areaType a)) (I.areaInit a)+ -- Sub-block of the prcedure type SubBlk = Bool -- Seen a return statement?@@ -171,8 +205,8 @@ = do b <- tyChk' (True, False) ss0 when b (putWarn LoopWarn) tyChk' (sb, False) ss- tyChk' b (I.Local _t _v init' : ss)- = do checkInit init'+ tyChk' b (I.Local t _v init' : ss)+ = do checkInit (Just t) init' tyChk' b ss tyChk' b (I.Comment (I.SourcePos src):ss) = do set src@@ -183,16 +217,38 @@ isComment (I.Comment _) = True isComment _ = False - checkInit (I.InitStruct fis)- = do mapM_ (checkInit . snd) fis- let fs = map fst fis- when (fs /= nub fs) $- putError DoubleInit- return ()- checkInit (I.InitArray is)- = mapM_ checkInit is- checkInit _- = return ()+-- XXX We don't check array lengths for substructural arrays (e.g., arrays that+-- are a field of a struct) because we don't have the typing information with+-- the array length in the AST; it's not part of the initializer. We could add it, though.+checkInit :: Maybe I.Type -> I.Init -> TCResults ()+checkInit mty init =+ case init of+ I.InitZero+ -> return ()+ I.InitExpr{}+ -> return ()+ I.InitStruct ls+ -> do+ mapM_ (checkInit Nothing . snd) ls+ let fs = map fst ls+ when (fs /= nub fs) (putError DoubleInit)+ I.InitArray inits b+ -> do+ mapM_ (checkInit Nothing) inits+ unless b (putWarn ArrayInitUnusedWarning)+ let mlen = getArrayLen <$> mty+ case mlen of+ Nothing -> return ()+ -- Assume default initialization if zero inits+ Just len -> when (not (null inits) && length inits < len)+ (putWarn ArrayInitPartialWarning)++getArrayLen :: I.Type -> Int+getArrayLen ty = case ty of+ I.TyArr i _+ -> i+ _ -> error $ "Error in TypeChecking: the impossible happened. "+ ++ "Expected an array type but saw " ++ show ty ++ "." xor :: Bool -> Bool -> Bool xor a b = (not a && b) || (a && not b)
src/Ivory/Opts/Utils.hs view
@@ -6,9 +6,15 @@ where -import qualified Ivory.Language.Syntax.AST as I-import qualified Ivory.Language.Syntax.Type as I+import Text.PrettyPrint +import qualified Ivory.Language.Syntax.AST as I+import Ivory.Language.Syntax.Concrete.Location+import Ivory.Language.Syntax.Concrete.Pretty (pretty, prettyPrint)+import qualified Ivory.Language.Syntax.Type as I++import System.IO (hPutStrLn, stderr)+ -------------------------------------------------------------------------------- -- | Type of the expression's arguments.@@ -23,5 +29,40 @@ _ -> t0 --------------------------------------------------------------------------------+-- PrettyPrinting +-- Results for a symbol, with the symbol name.+data SymResult a = SymResult String [a]+ deriving (Show, Read, Eq) +-- Results for a module, with the module name.+data ModResult a = ModResult String [SymResult a]+ deriving (Show, Read, Eq)++-- Show the errors for a module.+showModErrs :: Show a => (a -> Doc) -> ModResult a -> IO ()+showModErrs doc (ModResult m errs) =+ case errs of+ [] -> return ()+ _ ->+ hPutStrLn stderr+ $ render+ $ text "***" <+> text "Module" <+> text m <> colon+ $$ nest 2 (vcat (map (showSymErrs doc) errs))+ $$ empty++-- Show the errors for a symbol (area or procedure).+showSymErrs :: (a -> Doc) -> SymResult a -> Doc+showSymErrs doc (SymResult sym errs) =+ case errs of+ [] -> empty+ _ ->+ text "***" <+> text "Symbol" <+> text sym <> colon+ $$ nest 2 (vcat (map doc errs))+ $$ empty++showWithLoc :: (a -> Doc) -> Located a -> Doc+showWithLoc sh (Located loc a) =+ case loc of+ NoLoc -> sh a+ _ -> text (prettyPrint (pretty loc)) <> colon <+> sh a