diff --git a/ivory-opts.cabal b/ivory-opts.cabal --- a/ivory-opts.cabal +++ b/ivory-opts.cabal @@ -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, diff --git a/src/Ivory/Opts/AssertFold.hs b/src/Ivory/Opts/AssertFold.hs --- a/src/Ivory/Opts/AssertFold.hs +++ b/src/Ivory/Opts/AssertFold.hs @@ -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 -------------------------------------------------------------------------------- diff --git a/src/Ivory/Opts/CSE.hs b/src/Ivory/Opts/CSE.hs --- a/src/Ivory/Opts/CSE.hs +++ b/src/Ivory/Opts/CSE.hs @@ -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 diff --git a/src/Ivory/Opts/ConstFold.hs b/src/Ivory/Opts/ConstFold.hs --- a/src/Ivory/Opts/ConstFold.hs +++ b/src/Ivory/Opts/ConstFold.hs @@ -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 diff --git a/src/Ivory/Opts/SanityCheck.hs b/src/Ivory/Opts/SanityCheck.hs --- a/src/Ivory/Opts/SanityCheck.hs +++ b/src/Ivory/Opts/SanityCheck.hs @@ -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]) diff --git a/src/Ivory/Opts/TypeCheck.hs b/src/Ivory/Opts/TypeCheck.hs --- a/src/Ivory/Opts/TypeCheck.hs +++ b/src/Ivory/Opts/TypeCheck.hs @@ -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) diff --git a/src/Ivory/Opts/Utils.hs b/src/Ivory/Opts/Utils.hs --- a/src/Ivory/Opts/Utils.hs +++ b/src/Ivory/Opts/Utils.hs @@ -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