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.1 +version: 0.1.0.3 author: Galois, Inc. maintainer: leepike@galois.com category: Language @@ -10,32 +10,40 @@ cabal-version: >= 1.10 synopsis: Ivory compiler optimizations. description: Ivory compiler optimizations as well as compiler insertions. Primarily used by backends. -homepage: http://smaccmpilot.org/languages/ivory-introduction.html +homepage: http://ivorylang.org license: BSD3 license-file: LICENSE source-repository this type: git location: https://github.com/GaloisInc/ivory - tag: hackage-opts-0101 + tag: hackage-opts-0103 library exposed-modules: Ivory.Opts.AssertFold, + Ivory.Opts.BitShift, Ivory.Opts.CFG, + Ivory.Opts.CSE, Ivory.Opts.ConstFold, + Ivory.Opts.ConstFoldComp, Ivory.Opts.DivZero, Ivory.Opts.Index, Ivory.Opts.FP, - Ivory.Opts.Overflow + Ivory.Opts.Overflow, + Ivory.Opts.SanityCheck, + Ivory.Opts.TypeCheck other-modules: Ivory.Opts.Utils - build-depends: base >= 4.6 && < 4.7, - ivory, - monadLib >= 3.7, - filepath, + build-depends: base >= 4.6 && < 5, + base-compat, + containers, + data-reify >=0.6, dlist >= 0.5, fgl >= 5.4.2.4, - containers + filepath, + ivory, + monadLib >= 3.7, + pretty hs-source-dirs: src default-language: Haskell2010 ghc-options: -Wall 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 @@ -5,143 +5,165 @@ -- | Fold over expressions that collect up assertions about the expressions. -module Ivory.Opts.AssertFold where +module Ivory.Opts.AssertFold + ( procFold + , expFoldDefault + , insert + , FolderStmt() + , freshVar + ) where -import MonadLib hiding (collect) -import Data.Monoid +import Prelude () +import Prelude.Compat + +import MonadLib (StateM(..),StateT,Id,runStateT,runId) import qualified Data.DList as D import Ivory.Opts.Utils -import qualified Ivory.Language.Syntax.AST as I -import qualified Ivory.Language.Syntax.Type as I +import qualified Ivory.Language.Array as I +import qualified Ivory.Language.Syntax.AST as I +import qualified Ivory.Language.Syntax.Type as I -------------------------------------------------------------------------------- -- Monad and types. +data St a = St + { dlst :: D.DList a -- ^ State (statements) + , int :: Integer -- ^ Counter for fresh names + , pass :: String -- ^ Base for fresh names + } deriving (Show, Read, Eq) + -- | A monad that holds our transformed program. newtype FolderM a b = FolderM - { unFolderM :: StateT (D.DList a) Id b - } deriving (Functor, Monad) + { unFolderM :: StateT (St a) Id b + } deriving (Functor, Monad, Applicative) -instance StateM (FolderM a) (D.DList a) where +instance StateM (FolderM a) (St a) where get = FolderM get set = FolderM . set +extract :: FolderM a (D.DList a) +extract = do + st <- get + return (dlst st) + insert :: a -> FolderM a () insert a = do st <- get - set (D.snoc st a) + set $ st { dlst = D.snoc (dlst st) a } inserts :: D.DList a -> FolderM a () inserts ds = do st <- get - set (st <++> ds) + set $ st { dlst = dlst st <++> ds } -insertList :: [a] -> FolderM a () -insertList = inserts . D.fromList +runFolderM :: String -> FolderM a b -> D.DList a +runFolderM ps m = + dlst $ snd $ runId $ runStateT st (unFolderM m) + where + st = St D.empty 0 ps -resetState :: FolderM a () -resetState = set D.empty +resetSt :: FolderM a () +resetSt = do + st <- get + set st { dlst = D.empty } -runFolderM :: FolderM a b -> (b, D.DList a) -runFolderM m = runId $ runStateT mempty (unFolderM m) +-- | Create a fresh variable and update the variable store. +freshVar :: FolderM a String +freshVar = do + st <- get + let i = int st + set st { int = i + 1 } + return (pass st ++ show i) -------------------------------------------------------------------------------- -- Specialization for statements -type Stmts = D.DList I.Stmt - type FolderStmt a = FolderM I.Stmt a -- Return a list of assertions from an expression's subexpressions. -type ExpFold = I.Type -> I.Expr -> [I.Expr] - -insertAssert :: I.Expr -> FolderStmt () -insertAssert = insert . I.CompilerAssert - -insertAsserts :: [I.Expr] -> FolderStmt () -insertAsserts = insertList . map I.CompilerAssert - --------------------------------------------------------------------------------- +type ExpFold = I.Type -> I.Expr -> FolderStmt () -runEmptyState :: ExpFold -> [I.Stmt] -> [I.Stmt] -runEmptyState ef stmts = +runEmptyState :: String -> ExpFold -> [I.Stmt] -> [I.Stmt] +runEmptyState ps ef stmts = let m = mapM_ (stmtFold ef) stmts in - D.toList $ snd (runFolderM m) + D.toList (runFolderM ps m) -procFold :: ExpFold -> I.Proc -> I.Proc -procFold ef p = - let body' = runEmptyState ef (I.procBody p) in +-- | Run with fresh statements, returning them, but reseting the statement +-- state. +runFreshStmts :: ExpFold -> [I.Stmt] -> FolderStmt [I.Stmt] +runFreshStmts ef stmts = do + st <- get + set st { dlst = D.empty } + mapM_ (stmtFold ef) stmts + st' <- get + set st' { dlst = dlst st, int = int st' } + return (D.toList (dlst st')) + +-- | Update a procedure's statements with its compiler assertions (and local +-- variable declarations, as needed). +procFold :: String -> ExpFold -> I.Proc -> I.Proc +procFold ps ef p = + let body' = runEmptyState ps ef (I.procBody p) in p { I.procBody = body' } -------------------------------------------------------------------------------- stmtFold :: ExpFold -> I.Stmt -> FolderStmt () stmtFold ef stmt = case stmt of - I.IfTE e b0 b1 -> do insertAsserts (ef I.TyBool e) - let b0' = runEmptyState ef b0 - let b1' = runEmptyState ef b1 + I.IfTE e b0 b1 -> do ef I.TyBool e + b0' <- runFreshStmts ef b0 + b1' <- runFreshStmts ef b1 insert (I.IfTE e b0' b1') - I.Assert e -> do insertAsserts (ef I.TyBool e) + I.Assert e -> do ef I.TyBool e insert stmt - I.CompilerAssert e -> do insertAsserts (ef I.TyBool e) + I.CompilerAssert e -> do ef I.TyBool e insert stmt - I.Assume e -> do insertAsserts (ef I.TyBool e) + I.Assume e -> do ef I.TyBool e insert stmt - I.Return (I.Typed ty e) -> do insertAsserts (ef ty e) + I.Return (I.Typed ty e) -> do ef ty e insert stmt I.ReturnVoid -> insert stmt - I.Deref ty _v e -> do insertAsserts (ef ty e) + I.Deref ty _v e -> do ef ty e insert stmt - I.Store ty ptrExp e -> do insertAsserts (ef (I.TyRef ty) ptrExp) - insertAsserts (ef ty e) + I.Store ty ptrExp e -> do ef (I.TyRef ty) ptrExp + ef ty e insert stmt - I.Assign ty _v e -> do insertAsserts (ef ty e) + I.Assign ty _v e -> do ef ty e insert stmt - I.Call _ty _mv _nm args -> do insertAsserts (concatMap efTyped args) + I.Call _ty _mv _nm args -> do mapM_ efTyped args insert stmt - I.Loop v e incr blk -> do insertAsserts (ef (I.TyInt I.Int32) e) - insertAsserts (efIncr incr) - let blk' = runEmptyState ef blk - insert (I.Loop v e incr blk') + I.Loop m v e incr blk -> do ef (I.ixRep) e + efIncr incr + blk' <- runFreshStmts ef blk + insert (I.Loop m v e incr blk') I.Break -> insert stmt - I.Local _ty _v init' -> do insertAsserts (efInit init') + I.Local _ty _v init' -> do efInit init' insert stmt - I.RefCopy ty e0 e1 -> do insertAsserts (ef ty e0) - insertAsserts (ef ty e1) + I.RefCopy ty e0 e1 -> do ef ty e0 + ef ty e1 insert stmt I.AllocRef{} -> insert stmt - I.Forever blk -> do let blk' = runEmptyState ef blk + I.Forever blk -> do blk' <- runFreshStmts ef blk insert (I.Forever blk') + I.Comment _ -> insert stmt where efTyped (I.Typed ty e) = ef ty e efIncr incr = case incr of I.IncrTo e -> ef ty e I.DecrTo e -> ef ty e - where ty = I.TyInt I.Int32 + where ty = I.ixRep efInit init' = case init' of - I.InitZero -> [] + I.InitZero -> return () I.InitExpr ty e -> ef ty e - I.InitStruct inits -> concatMap (efInit . snd) inits - I.InitArray inits -> concatMap efInit inits - --------------------------------------------------------------------------------- --- Specialization for expressions - -type Exprs = D.DList I.Expr - -type FolderExpr a = FolderM I.Expr a - --- | Default expression folder that performs the recursion for an asserter. -expFoldDefault :: ExpFold -> I.Type -> I.Expr -> [I.Expr] -expFoldDefault ef ty e = - let (_, ds) = runFolderM (expFoldDefault' ef ty e) in - D.toList ds + I.InitStruct inits -> mapM_ (efInit . snd) inits + I.InitArray inits -> mapM_ efInit inits -------------------------------------------------------------------------------- -expFoldDefault' :: ExpFold -> I.Type -> I.Expr -> FolderExpr () -expFoldDefault' asserter ty e = case e of +expFoldDefault :: ExpFold -> I.Type -> I.Expr -> FolderStmt () +expFoldDefault asserter ty e = case e of I.ExpSym{} -> go e + I.ExpExtern{} -> go e I.ExpVar{} -> go e I.ExpLit{} -> go e I.ExpLabel ty' e0 _str -> do go e @@ -157,9 +179,10 @@ expFoldOps asserter ty (op, args) I.ExpAddrOfGlobal{} -> go e I.ExpMaxMin{} -> go e + I.ExpSizeOf{} -> go e where - go = insertList . asserter ty - expFold = expFoldDefault' asserter + go = asserter ty + expFold = expFoldDefault asserter -------------------------------------------------------------------------------- @@ -175,17 +198,18 @@ -- -- x /= 0 ? 3.0/x : 0.0 -- -expFoldOps :: ExpFold -> I.Type -> (I.ExpOp, [I.Expr]) -> FolderExpr () +-- Otherwise, map over the expression with the asserter. +expFoldOps :: ExpFold -> I.Type -> (I.ExpOp, [I.Expr]) -> FolderStmt () expFoldOps asserter ty (op, args) = case (op, args) of (I.ExpCond, [cond, texp, fexp]) -> do fold ty cond - preSt <- get + preSt <- extract tSt <- runBranch cond texp fSt <- runBranch (neg cond) fexp - resetState + resetSt inserts preSt inserts tSt @@ -200,20 +224,19 @@ _ -> mapM_ (fold $ expOpType ty op) args where - fold = expFoldDefault' asserter + fold = expFoldDefault asserter runBranch cond e = do - resetState - fold ty e - withEnv cond - get + resetSt + expFoldDefault (withCond cond asserter) ty e + extract runBool exp0 exp1 f = do - preSt <- get + preSt <- extract st0 <- runCase exp0 st1 <- runBranch (f exp0) exp1 - resetState + resetSt inserts preSt inserts st0 @@ -221,9 +244,9 @@ where runCase e = do - resetState + resetSt fold ty e - get + extract -------------------------------------------------------------------------------- -- Helpers @@ -231,18 +254,15 @@ (<++>) :: Monoid a => a -> a -> a a <++> b = a `mappend` b --- Add a precondition to a conditional expression. -withEnv :: I.Expr -> FolderExpr () -withEnv pre = do - st <- get - let assts = D.map (pre ==>) st - set assts - infixr 0 ==> (==>) :: I.Expr -> I.Expr -> I.Expr (==>) e0 e1 = I.ExpOp I.ExpOr [neg e0, e1] neg :: I.Expr -> I.Expr neg e = I.ExpOp I.ExpNot [e] + +-- | Modify the ExpFold function to take a precondition. +withCond :: I.Expr -> ExpFold -> ExpFold +withCond cond f ty e = f ty (cond ==> e) -------------------------------------------------------------------------------- diff --git a/src/Ivory/Opts/BitShift.hs b/src/Ivory/Opts/BitShift.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Opts/BitShift.hs @@ -0,0 +1,53 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} + +-------------------------------------------------------------------------------- +-- (c) Galois, Inc. 2014. +-- All rights reserved. + +-- | Check for undefined bitshift behavior. Bit-shifts on signed ints are +-- already disallowed. This check is that we bit-shift by strictly less than n +-- for an n-bit value. +-------------------------------------------------------------------------------- + +module Ivory.Opts.BitShift + ( bitShiftFold + ) where + +import Ivory.Opts.AssertFold + +import qualified Ivory.Language.Syntax.AST as I +import qualified Ivory.Language.Syntax.Type as I +import Ivory.Language + +-------------------------------------------------------------------------------- + +bitShiftFold :: I.Proc -> I.Proc +bitShiftFold = procFold "bits" (expFoldDefault bitShiftAssert) + +-------------------------------------------------------------------------------- + +bitShiftAssert :: I.Type -> I.Expr -> FolderStmt () +bitShiftAssert ty e = case e of + I.ExpOp op es -> go op es + _ -> return () + where + go op es = case op of + I.ExpBitShiftL -> assrt + I.ExpBitShiftR -> assrt + _ -> return () + + where + assrt = case ty of + I.TyWord w -> case w of + I.Word8 -> mkAsst (iBitSize (0 :: Uint8)) + I.Word16 -> mkAsst (iBitSize (0 :: Uint16)) + I.Word32 -> mkAsst (iBitSize (0 :: Uint32)) + I.Word64 -> mkAsst (iBitSize (0 :: Uint64)) + _ -> return () + + mkAsst sz = insert $ I.CompilerAssert $ I.ExpOp (I.ExpLt False ty) + [es !! 1, fromIntegral sz] + +-------------------------------------------------------------------------------- diff --git a/src/Ivory/Opts/CFG.hs b/src/Ivory/Opts/CFG.hs --- a/src/Ivory/Opts/CFG.hs +++ b/src/Ivory/Opts/CFG.hs @@ -2,6 +2,7 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE CPP #-} -- {-# LANGUAGE DataKinds #-} -- {-# LANGUAGE TypeOperators #-} @@ -20,16 +21,18 @@ ) where -import qualified Ivory.Language.Syntax.AST as I +import Prelude () +import Prelude.Compat hiding (lookup) + +import qualified Ivory.Language.Array as I +import qualified Ivory.Language.Syntax.AST as I import qualified Ivory.Language.Syntax.Type as I import qualified Data.Graph.Inductive as G -import Prelude hiding (lookup) -import Data.Monoid +import Control.Applicative (liftA2) import System.FilePath import Data.Maybe -import Data.List hiding (lookup) -import Control.Applicative +import Data.List (find,(\\)) import qualified Data.IntMap as M import MonadLib (StateT, get, set, Id, StateM, runM) import MonadLib.Derive (derive_get, derive_set, Iso(..)) @@ -88,7 +91,7 @@ | Word64 deriving (Show,Eq) -data (Show a, Eq a) => Block a +data Block a = Stmt a | Branch [Block a] [Block a] | Loop (Maybe Integer) [Block a] -- If we know how many loops we make, we @@ -130,6 +133,7 @@ I.TyVoid -> TyVoid I.TyInt i -> TyInt (toIntType i) I.TyWord w -> TyWord (toWordType w) + I.TyIndex _n -> toStackType I.ixRep I.TyBool -> TyBool I.TyChar -> TyChar I.TyFloat -> TyFloat @@ -170,9 +174,9 @@ I.IfTE _ blk0 blk1 -> [ Branch (concatMap toAlloc blk0) (concatMap toAlloc blk1) ] -- For the loop variable. - I.Loop _ e _ blk -> - let ty = I.TyInt I.Int32 in - [Stmt (toStackType ty), Loop (getIdx e) (concatMap toAlloc blk)] + I.Loop m _ e _ blk -> + let ty = I.ixRep in + [Stmt (toStackType ty), Loop (Just (loopIdx m e)) (concatMap toAlloc blk)] I.Forever blk -> [Loop Nothing (concatMap toAlloc blk)] _ -> [] @@ -185,11 +189,15 @@ I.Call _ _ nm _ -> case nm of I.NameSym sym -> [Stmt sym] I.NameVar _ -> error $ "XXX need to implement function pointers." - I.Loop _ e _ blk -> [Loop (getIdx e) (concatMap toCall blk)] + I.Loop m _ e _ blk -> [Loop (Just (loopIdx m e)) (concatMap toCall blk)] _ -> [] -getIdx :: I.Expr -> Maybe Integer -getIdx e = case e of +loopIdx :: Integer -> I.Expr -> Integer +loopIdx _ (I.ExpLit (I.LitInteger i)) = i +loopIdx m _ = m + +_getIdx :: I.Expr -> Maybe Integer +_getIdx e = case e of I.ExpLit (I.LitInteger i) -> Just i _ -> Nothing @@ -266,7 +274,7 @@ newtype MaxState a = MaxState { unSt :: StateT MaxMap Id a - } deriving (Functor, Monad) + } deriving (Functor, Monad, Applicative) instance StateM MaxState MaxMap where get = derive_get (Iso MaxState unSt) @@ -406,17 +414,17 @@ -> String graphviz g t = let n = G.labNodes g - e = G.labEdges g - ns = concatMap sn n - es = concatMap se e + e = G.labEdges g + ns = concatMap sn n + es = concatMap se e in "digraph "++t++" {\n" - ++ ns - ++ es - ++"}" - where sn (n, a) | sa == "" = "" - | otherwise = '\t':(show n ++ sa ++ "\n") - where sa = sl a - se (n1, n2, b) = '\t':(show n1 ++ " -> " ++ show n2 ++ sl b ++ "\n") + ++ ns + ++ es + ++"}" + where sn (n, a) | sa == "" = "" + | otherwise = '\t':(show n ++ sa ++ "\n") + where sa = sl a + se (n1, n2, b) = '\t':(show n1 ++ " -> " ++ show n2 ++ sl b ++ "\n") sl :: (Show a) => a -> String sl a = let l = sq (show a) @@ -425,9 +433,9 @@ sq :: String -> String sq s@[_] = s sq ('"':s) | last s == '"' = init s - | otherwise = s + | otherwise = s sq ('\'':s) | last s == '\'' = init s - | otherwise = s + | otherwise = s sq s = s -------------------------------------------------------------------------------- diff --git a/src/Ivory/Opts/CSE.hs b/src/Ivory/Opts/CSE.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Opts/CSE.hs @@ -0,0 +1,387 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +module Ivory.Opts.CSE (cseFold) where + +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 qualified Ivory.Language.Syntax as AST +import MonadLib (WriterT, StateT, Id, get, set, sets, sets_, put, collect, lift, runM) +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 +-- evaluation of an expression earlier than it would have occurred in +-- the source program, which means that sometimes an expression must be +-- re-computed on each of several execution paths. +cseFold :: AST.Proc -> AST.Proc +cseFold def = def + { AST.procBody = reconstruct $ unsafePerformIO $ reifyGraph $ AST.procBody def } + +-- | Variable assignments emitted so far. +data Bindings = Bindings + { availableBindings :: (Map (Unique, AST.Type) Int) + , unusedBindings :: IntSet + , totalBindings :: Int + } + +-- | A monad for emitting both source-level statements as well as +-- assignments that capture common subexpressions. +-- +-- Note that the StateT is outside the WriterT so that we can first run +-- the StateT, getting a set of expressions which shouldn't be assigned +-- to fresh names, and only then decide whether to write out Assign +-- statements. See the comment in `updateFacts`. +type BlockM a = StateT Bindings (WriterT (D.DList AST.Stmt) Id) a + +-- | We perform CSE on expressions but also across all the blocks in a +-- procedure. +data CSE t + = CSEExpr (ExprF t) + | CSEBlock (BlockF t) + deriving (Show, Eq, Ord, Functor) + +-- | During CSE, we replace recursive references to an expression with a +-- unique ID for that expression. +data ExprF t + = ExpSimpleF AST.Expr + -- ^ For expressions that cannot contain any expressions recursively. + | ExpLabelF AST.Type t String + | ExpIndexF AST.Type t AST.Type t + | ExpToIxF t Integer + | ExpSafeCastF AST.Type t + | ExpOpF AST.ExpOp [t] + deriving (Show, Eq, Ord, Foldable, Functor, Traversable) + +instance MuRef AST.Expr where + type DeRef AST.Expr = CSE + mapDeRef child e = CSEExpr <$> case e of + AST.ExpSym{} -> pure $ ExpSimpleF e + AST.ExpExtern{} -> pure $ ExpSimpleF e + AST.ExpVar{} -> pure $ ExpSimpleF e + AST.ExpLit{} -> pure $ ExpSimpleF e + AST.ExpLabel ty ex nm -> ExpLabelF <$> pure ty <*> child ex <*> pure nm + AST.ExpIndex ty1 ex1 ty2 ex2 -> ExpIndexF <$> pure ty1 <*> child ex1 <*> pure ty2 <*> child ex2 + AST.ExpToIx ex bound -> ExpToIxF <$> child ex <*> pure bound + AST.ExpSafeCast ty ex -> ExpSafeCastF ty <$> child ex + AST.ExpOp op args -> ExpOpF op <$> traverse child args + AST.ExpAddrOfGlobal{} -> pure $ ExpSimpleF e + AST.ExpMaxMin{} -> pure $ ExpSimpleF e + AST.ExpSizeOf{} -> pure $ ExpSimpleF e + +-- | Convert a flattened expression back to a real expression. +toExpr :: ExprF AST.Expr -> AST.Expr +toExpr (ExpSimpleF ex) = ex +toExpr (ExpLabelF ty ex nm) = AST.ExpLabel ty ex nm +toExpr (ExpIndexF ty1 ex1 ty2 ex2) = AST.ExpIndex ty1 ex1 ty2 ex2 +toExpr (ExpToIxF ex bound) = AST.ExpToIx ex bound +toExpr (ExpSafeCastF ty ex) = AST.ExpSafeCast ty ex +toExpr (ExpOpF op args) = AST.ExpOp op args + +-- | Wrap the second type in either TyRef or TyConstRef, according to +-- whether the first argument was a constant ref. +copyConst :: AST.Type -> AST.Type -> AST.Type +copyConst (AST.TyRef _) ty = AST.TyRef ty +copyConst (AST.TyConstRef _) ty = AST.TyConstRef ty +copyConst ty _ = error $ "Ivory.Opts.CSE.copyConst: expected a Ref type but got " ++ show ty + +-- | Label all sub-expressions with the type at which they're used, +-- assuming that this expression is used at the given type. +labelTypes :: AST.Type -> ExprF k -> ExprF (k, AST.Type) +labelTypes _ (ExpSimpleF e) = ExpSimpleF e +labelTypes resty (ExpLabelF ty ex nm) = ExpLabelF ty (ex, copyConst resty ty) nm +labelTypes resty (ExpIndexF ty1 ex1 ty2 ex2) = ExpIndexF ty1 (ex1, copyConst resty ty1) ty2 (ex2, ty2) +labelTypes _ (ExpToIxF ex bd) = ExpToIxF (ex, ixRep) bd +labelTypes _ (ExpSafeCastF ty ex) = ExpSafeCastF ty (ex, ty) +labelTypes ty (ExpOpF op args) = ExpOpF op $ case op of + AST.ExpEq t -> map (`atType` t) args + AST.ExpNeq t -> map (`atType` t) args + AST.ExpCond -> let (cond, rest) = splitAt 1 args in map (`atType` AST.TyBool) cond ++ map (`atType` ty) rest + AST.ExpGt _ t -> map (`atType` t) args + AST.ExpLt _ t -> map (`atType` t) args + AST.ExpIsNan t -> map (`atType` t) args + AST.ExpIsInf t -> map (`atType` t) args + _ -> map (`atType` ty) args + where + atType = (,) + +-- | Like ExprF, we replace recursive references to +-- blocks/statements/expressions with unique IDs. +-- +-- Note that we treat statements as a kind of block, because extracting +-- assignments for the common subexpressions in a statement can result +-- in multiple statements, which looks much like a block. +data BlockF t + = StmtSimple AST.Stmt + -- ^ For statements that cannot contain any other statements or expressions. + | StmtIfTE t t t + | StmtAssert t + | StmtCompilerAssert t + | StmtAssume t + | StmtReturn (AST.Typed t) + | StmtDeref AST.Type AST.Var t + | StmtStore AST.Type t t + | StmtAssign AST.Type AST.Var t + | StmtCall AST.Type (Maybe AST.Var) AST.Name [AST.Typed t] + | StmtLocal AST.Type AST.Var (InitF t) + | StmtRefCopy AST.Type t t + | StmtLoop Integer AST.Var t (LoopIncrF t) t + | StmtForever t + | Block [t] + deriving (Show, Eq, Ord, Functor) + +data LoopIncrF t + = IncrTo t + | DecrTo t + deriving (Show, Eq, Ord, Functor) + +data InitF t + = InitZero + | InitExpr AST.Type t + | InitStruct [(String, InitF t)] + | InitArray [InitF t] + deriving (Show, Eq, Ord, Functor) + +instance MuRef AST.Stmt where + type DeRef AST.Stmt = CSE + mapDeRef child stmt = CSEBlock <$> case stmt of + AST.IfTE cond tb fb -> StmtIfTE <$> child cond <*> child tb <*> child fb + AST.Assert cond -> StmtAssert <$> child cond + AST.CompilerAssert cond -> StmtCompilerAssert <$> child cond + AST.Assume cond -> StmtAssume <$> child cond + AST.Return (AST.Typed ty ex) -> StmtReturn <$> (AST.Typed ty <$> child ex) + AST.Deref ty var ex -> StmtDeref ty var <$> child ex + AST.Store ty lhs rhs -> StmtStore ty <$> child lhs <*> child rhs + AST.Assign ty var ex -> StmtAssign ty var <$> child ex + 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.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. + AST.ReturnVoid -> pure $ StmtSimple stmt + AST.AllocRef{} -> pure $ StmtSimple stmt + AST.Break -> pure $ StmtSimple stmt + AST.Comment{} -> pure $ StmtSimple stmt + where + 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 + mapIncr (AST.IncrTo ex) = IncrTo <$> child ex + mapIncr (AST.DecrTo ex) = DecrTo <$> child ex + +instance (MuRef a, DeRef [a] ~ DeRef a) => MuRef [a] where + type DeRef [a] = CSE + mapDeRef child xs = CSEBlock <$> Block <$> traverse child xs + +-- | Convert a flattened statement or block back to a real block. +toBlock :: (k -> AST.Type -> BlockM AST.Expr) -> (k -> BlockM ()) -> BlockF k -> BlockM () +toBlock expr block b = case b of + StmtSimple s -> stmt $ return s + StmtIfTE ex tb fb -> stmt $ AST.IfTE <$> expr ex AST.TyBool <*> genBlock (block tb) <*> genBlock (block fb) + StmtAssert cond -> stmt $ AST.Assert <$> expr cond AST.TyBool + StmtCompilerAssert cond -> stmt $ AST.CompilerAssert <$> expr cond AST.TyBool + StmtAssume cond -> stmt $ AST.Assume <$> expr cond AST.TyBool + StmtReturn (AST.Typed ty ex) -> stmt $ AST.Return <$> (AST.Typed ty <$> expr ex ty) + -- XXX: The AST does not preserve whether the RHS of a deref was for a + -- const ref, but it's safe to assume it's const. + StmtDeref ty var ex -> stmt $ AST.Deref ty var <$> expr ex (AST.TyConstRef ty) + -- XXX: The LHS of a store must not have been const. + StmtStore ty lhs rhs -> stmt $ AST.Store ty <$> expr lhs (AST.TyRef ty) <*> expr rhs ty + StmtAssign ty var ex -> stmt $ AST.Assign ty var <$> expr ex ty + StmtCall ty mv nm args -> stmt $ AST.Call ty mv nm <$> mapM (\ (AST.Typed argTy argEx) -> AST.Typed argTy <$> expr argEx argTy) args + 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) + 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 + where + stmt stmtM = fmap D.singleton stmtM >>= put + 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 + toIncr (IncrTo ex) = AST.IncrTo <$> expr ex ixRep + toIncr (DecrTo ex) = AST.DecrTo <$> expr ex ixRep + +-- | When a statement contains a block, we need to propagate the +-- available expressions into that block. However, on exit from that +-- block, the expressions it made newly-available go out of scope, so we +-- remove them from the available set for subsequent statements. +genBlock :: BlockM () -> BlockM AST.Block +genBlock gen = do + oldBindings <- get + ((), stmts) <- collect gen + sets_ $ \ newBindings -> newBindings { availableBindings = availableBindings oldBindings } + return $ D.toList stmts + +-- | Data to accumulate as we analyze each expression and each +-- block/statement. +type Facts = (IntMap (AST.Type -> BlockM AST.Expr), IntMap (BlockM ())) + +-- | We can only generate code from a DAG, so this function calls +-- `error` if the reified graph has cycles. Because we walk the AST in +-- topo-sorted order, if we haven't already computed the desired fact, +-- then we're trying to follow a back-edge in the graph, and that means +-- the graph has cycles. +getFact :: IntMap v -> Unique -> v +getFact m k = case IntMap.lookup k m of + Nothing -> error "IvoryCSE: cycle detected in expression graph" + Just v -> v + +-- | Walk a reified AST in topo-sorted order, accumulating analysis +-- results. +-- +-- `usedOnce` must be the final value of `unusedBindings` after analysis +-- is complete. +updateFacts :: IntSet -> (Unique, CSE Unique) -> Facts -> Facts +updateFacts _ (ident, CSEBlock block) (exprFacts, blockFacts) = (exprFacts, IntMap.insert ident (toBlock (getFact exprFacts) (getFact blockFacts) block) blockFacts) +updateFacts usedOnce (ident, CSEExpr expr) (exprFacts, blockFacts) = (IntMap.insert ident fact exprFacts, blockFacts) + where + nameOf var = AST.VarName $ "cse" ++ show var + fact = case expr of + ExpSimpleF e -> const $ return e + ex -> \ ty -> do + bindings <- get + case Map.lookup (ident, ty) $ availableBindings bindings of + Just var -> do + set $ bindings { unusedBindings = IntSet.delete var $ unusedBindings bindings } + return $ AST.ExpVar $ nameOf var + Nothing -> do + ex' <- fmap toExpr $ mapM (uncurry $ getFact exprFacts) $ labelTypes ty ex + var <- sets $ \ (Bindings { availableBindings = avail, unusedBindings = unused, totalBindings = maxId}) -> + (maxId, Bindings + { availableBindings = Map.insert (ident, ty) maxId avail + , unusedBindings = IntSet.insert maxId unused + , totalBindings = maxId + 1 + }) + -- Defer a final decision on whether to inline this expression + -- or allocate a variable for it until we've finished running + -- the State monad and can extract the unusedBindings set from + -- there. After that the Writer monad can make decisions based + -- on usedOnce without throwing a <> exception. + lift $ if var `IntSet.member` usedOnce + then return ex' + else do + put $ D.singleton $ AST.Assign ty (nameOf var) ex' + return $ AST.ExpVar $ nameOf var + +-- | Values that we may generate by simplification rules on the reified +-- representation of the graph. +data Constant + = ConstFalse + | ConstTrue + | ConstZero + | ConstTwo + deriving (Bounded, Enum) + +-- | AST implementation for each constant value. +constExpr :: Constant -> CSE Unique +constExpr ConstFalse = CSEExpr $ ExpSimpleF $ AST.ExpLit $ AST.LitBool False +constExpr ConstTrue = CSEExpr $ ExpSimpleF $ AST.ExpLit $ AST.LitBool True +constExpr ConstZero = CSEExpr $ ExpSimpleF $ AST.ExpLit $ AST.LitInteger 0 +constExpr ConstTwo = CSEExpr $ ExpSimpleF $ AST.ExpLit $ AST.LitInteger 2 + +-- | Generate a unique integer for each constant which doesn't collide +-- with any IDs that reifyGraph may generate. +constUnique :: Constant -> Unique +constUnique c = negate $ 1 + fromEnum c + +-- | Wrapper around Facts to track unshared duplicates. +type Dupes = (Map (CSE Unique) Unique, IntMap Unique, Facts) + +-- | Wrapper around updateFacts to remove unshared duplicates. Also, +-- checking for equality of statements or expressions is constant-time +-- in this representation, so apply any simplifications that rely on +-- equality of subtrees here. +dedup :: IntSet -> (Unique, CSE Unique) -> Dupes -> Dupes +dedup usedOnce (ident, expr) (seen, remap, facts) = case expr' of + -- If this operator yields a constant on equal operands, we can + -- rewrite it to that constant. + CSEExpr (ExpOpF (AST.ExpEq ty) [a, b]) | not (isFloat ty) && a == b -> remapTo $ constUnique ConstTrue + CSEExpr (ExpOpF (AST.ExpNeq ty) [a, b]) | not (isFloat ty) && a == b -> remapTo $ constUnique ConstFalse + CSEExpr (ExpOpF (AST.ExpGt isEq ty) [a, b]) | not (isFloat ty) && a == b -> remapTo $ if isEq then constUnique ConstTrue else constUnique ConstFalse + CSEExpr (ExpOpF (AST.ExpLt isEq ty) [a, b]) | not (isFloat ty) && a == b -> remapTo $ if isEq then constUnique ConstTrue else constUnique ConstFalse + CSEExpr (ExpOpF AST.ExpBitXor [a, b]) | a == b -> remapTo $ constUnique ConstZero + -- NOTE: This transformation is not safe for ExpSub on floating-point + -- values, which could be NaN. + + -- If this operator is idempotent and its operands are equal, we can + -- replace it with either operand without changing its meaning. + CSEExpr (ExpOpF AST.ExpAnd [a, b]) | a == b -> remapTo a + CSEExpr (ExpOpF AST.ExpOr [a, b]) | a == b -> remapTo a + CSEExpr (ExpOpF AST.ExpBitAnd [a, b]) | a == b -> remapTo a + CSEExpr (ExpOpF AST.ExpBitOr [a, b]) | a == b -> remapTo a + + -- If both branches of a conditional expression or statement have the + -- same effect, then we don't need to evaluate the condition; we can + -- just replace it with either branch. This is not safe in C because + -- the condition might have side effects, but Ivory expressions never + -- have side effects. + CSEExpr (ExpOpF AST.ExpCond [_, t, f]) | t == f -> remapTo t + -- NOTE: This results in inserting a Block directly into another + -- Block, which can't happen any other way. + CSEBlock (StmtIfTE _ t f) | t == f -> remapTo t + + -- Single-statement blocks generate the same code as the statement. + CSEBlock (Block [s]) -> remapTo s + + -- No equal subtrees, so run with it. + _ -> case Map.lookup expr' seen of + Just ident' -> remapTo ident' + Nothing -> (Map.insert expr' ident seen, remap, updateFacts usedOnce (ident, expr') facts) + where + remapTo ident' = (seen, IntMap.insert ident ident' remap, facts) + expr' = case fmap (\ k -> IntMap.findWithDefault k k remap) expr of + -- Perhaps this operator can be replaced by a simpler one when its + -- operands are equal. + CSEExpr (ExpOpF AST.ExpAdd [a, b]) | a == b -> CSEExpr $ ExpOpF AST.ExpMul $ sort [constUnique ConstTwo, a] + + -- If this operator is commutative, we can put its arguments in any + -- order we want. If we choose the same order every time, more + -- semantically equivalent subexpressions will be factored out. + CSEExpr (ExpOpF op args) | isCommutative op -> CSEExpr $ ExpOpF op $ sort args + asis -> asis + + isFloat AST.TyFloat = True + isFloat AST.TyDouble = True + isFloat _ = False + + isCommutative (AST.ExpEq _) = True + isCommutative (AST.ExpNeq _) = True + isCommutative AST.ExpMul = True + isCommutative AST.ExpAdd = True + isCommutative AST.ExpBitAnd = True + isCommutative AST.ExpBitOr = True + isCommutative AST.ExpBitXor = True + isCommutative _ = False + +-- | Given a reified AST, reconstruct an Ivory AST with all sharing made +-- explicit. +reconstruct :: Graph CSE -> AST.Block +reconstruct (Graph subexprs root) = D.toList rootBlock + where + -- 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] ] + Just rootGen = IntMap.lookup (IntMap.findWithDefault root root remap) blockFacts + (((), 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,139 +1,190 @@ {-# LANGUAGE PatternGuards #-} {-# LANGUAGE Rank2Types #-} +-- +-- Constant folder. +-- +-- Copyright (C) 2014, Galois, Inc. +-- All rights reserved. +-- + module Ivory.Opts.ConstFold ( constFold ) where -import qualified Ivory.Language.Syntax.AST as I -import qualified Ivory.Language.Syntax.Type as I +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 Control.Monad (mzero,msum) +import Control.Arrow (second) +import Data.Map (Map) +import qualified Data.Map as Map import Data.Maybe -import Data.List -import Data.Word -import Data.Int import qualified Data.DList as D +import MonadLib (StateM(..),Id,StateT,runId,runStateT) -------------------------------------------------------------------------------- -- Constant folding --------------------------------------------------------------------------------- -constFold :: I.Proc -> I.Proc -constFold = procFold cf +type CopyMap = Map I.Var I.Expr -- | Expression to expression optimization. -type ExprOpt = I.Type -> I.Expr -> I.Expr - --- | Constant folding. -cf :: ExprOpt -cf ty e = - case e of - I.ExpSym{} -> e - I.ExpVar{} -> e - I.ExpLit{} -> e - - I.ExpOp op args -> cfOp ty op args - - I.ExpLabel t e0 s -> I.ExpLabel t (cf t e0) s - - I.ExpIndex t e0 t1 e1 -> I.ExpIndex t (cf t e0) t1 (cf t e1) - - I.ExpSafeCast t e0 -> - let e0' = cf t e0 - in fromMaybe (I.ExpSafeCast t e0') $ do - _ <- destLit e0' - return e0' - - I.ExpToIx e0 maxSz -> - let ty' = I.TyInt I.Int32 in - let e0' = cf ty' e0 in - case destIntegerLit e0' of - Just i -> I.ExpLit $ I.LitInteger $ i `rem` maxSz - Nothing -> I.ExpToIx e0' maxSz +type ExprOpt = CopyMap -> I.Type -> I.Expr -> I.Expr - I.ExpAddrOfGlobal{} -> e - I.ExpMaxMin{} -> e +constFold :: I.Proc -> I.Proc +constFold = procFold cf procFold :: ExprOpt -> I.Proc -> I.Proc procFold opt proc = let cxt = I.procSym proc - body' = D.toList $ foldl' (stmtFold cxt opt) D.empty (I.procBody proc) + body' = D.toList $ blockFold cxt opt Map.empty $ I.procBody proc in proc { I.procBody = body' } -stmtFold :: String -> ExprOpt -> D.DList I.Stmt -> I.Stmt -> D.DList I.Stmt -stmtFold cxt opt blk stmt = +blockFold :: String -> ExprOpt -> CopyMap -> I.Block -> D.DList I.Stmt +blockFold cxt opt copies = D.concat . fst . runId . runStateT copies . mapM (stmtFold cxt opt) + +stmtFold :: String -> ExprOpt -> I.Stmt -> StateT CopyMap Id (D.DList I.Stmt) +stmtFold cxt opt stmt = case stmt of - I.IfTE e b0 b1 -> - let e' = opt I.TyBool e in - case e' of - I.ExpLit (I.LitBool b) -> if b then blk `D.append` (newFold' b0) - else blk `D.append` (newFold' b1) - _ -> snoc $ I.IfTE e' (newFold b0) (newFold b1) - I.Assert e -> - let e' = opt I.TyBool e in - case e' of + I.IfTE _ [] [] -> return D.empty + I.IfTE e [] b1 -> stmtFold cxt opt $ I.IfTE (I.ExpOp I.ExpNot [e]) b1 [] + I.IfTE e b0 b1 -> do + copies <- get + case opt copies I.TyBool e of + I.ExpLit (I.LitBool b) -> fmap D.concat $ mapM (stmtFold cxt opt) $ if b then b0 else b1 + e' -> return $ D.singleton $ I.IfTE e' (newFold copies b0) (newFold copies b1) + I.Assert e -> do + copies <- get + case opt copies I.TyBool e of I.ExpLit (I.LitBool b) -> - if b then blk + if b then return D.empty else error $ "Constant folding evaluated a False assert()" ++ " in evaluating expression " ++ show e ++ " of function " ++ cxt - _ -> snoc (I.Assert e') - I.CompilerAssert e -> - let e' = opt I.TyBool e in - let go = snoc (I.CompilerAssert e') in - case e' of - I.ExpLit (I.LitBool b) -> - -- It's OK to have false but unreachable compiler asserts. - if b then blk else go - _ -> go - I.Assume e -> - let e' = opt I.TyBool e in - case e' of + e' -> return $ D.singleton (I.Assert e') + I.CompilerAssert e -> do + copies <- get + case opt copies I.TyBool e of + -- It's OK to have false but unreachable compiler asserts. + I.ExpLit (I.LitBool b) | b -> return D.empty + e' -> return $ D.singleton (I.CompilerAssert e') + I.Assume e -> do + copies <- get + case opt copies I.TyBool e of I.ExpLit (I.LitBool b) -> - if b then blk + if b then return D.empty else error $ "Constant folding evaluated a False assume()" ++ " in evaluating expression " ++ show e ++ " of function " ++ cxt - _ -> snoc (I.Assume e') + e' -> return $ D.singleton (I.Assume e') - I.Return e -> snoc $ I.Return (typedFold opt e) - I.ReturnVoid -> snoc I.ReturnVoid - I.Deref t var e -> snoc $ I.Deref t var (opt t e) - I.Store t e0 e1 -> snoc $ I.Store t (opt t e0) (opt t e1) - I.Assign t v e -> snoc $ I.Assign t v (opt t e) - I.Call t mv c tys -> snoc $ I.Call t mv c (map (typedFold opt) tys) - I.Local{} -> snoc stmt - I.RefCopy t e0 e1 -> snoc $ I.RefCopy t (opt t e0) (opt t e1) - I.AllocRef{} -> snoc stmt - I.Loop v e incr blk' -> - let ty = I.TyInt I.Int32 in - case opt ty e of + I.Return e -> do + copies <- get + return $ D.singleton $ I.Return (typedFold opt copies e) + I.ReturnVoid -> return $ D.singleton stmt + I.Deref t var e -> do + copies <- get + return $ D.singleton $ I.Deref t var (opt copies t e) + I.Store t e0 e1 -> do + copies <- get + return $ D.singleton $ I.Store t (opt copies t e0) (opt copies t e1) + + I.Assign t v e -> do + copies <- get + let e' = opt copies t e + let copyProp = set (Map.insert v e' copies) >> return D.empty + case e' of + I.ExpSym{} -> copyProp + I.ExpVar{} -> copyProp + I.ExpLit{} -> copyProp + I.ExpAddrOfGlobal{} -> copyProp + I.ExpMaxMin{} -> copyProp + _ -> return $ D.singleton $ I.Assign t v e' + + I.Call t mv c tys -> do + copies <- get + return $ D.singleton $ I.Call t mv c (map (typedFold opt copies) tys) + I.Local t var i -> do + copies <- get + return $ D.singleton $ I.Local t var $ constFoldInits copies i + I.RefCopy t e0 e1 -> do + copies <- get + return $ D.singleton $ I.RefCopy t (opt copies t e0) (opt copies t e1) + I.AllocRef{} -> return $ D.singleton stmt + I.Loop m v e incr blk' -> do + copies <- get + let ty = I.ixRep + case opt copies ty e of I.ExpLit (I.LitBool b) -> if b then error $ "Constant folding evaluated True expression " ++ "in a loop bound. The loop will never terminate!" else error $ "Constant folding evaluated False expression " ++ "in a loop bound. The loop will never execute!" _ -> - snoc $ I.Loop v (opt ty e) (loopIncrFold (opt ty) incr) - (newFold blk') - I.Break -> snoc I.Break - I.Forever b -> snoc $ I.Forever (newFold b) - where sf = stmtFold cxt opt - newFold' = foldl' sf D.empty - newFold = D.toList . newFold' - snoc = (blk `D.snoc`) + return $ D.singleton $ I.Loop m v (opt copies ty e) (loopIncrFold (opt copies ty) incr) + (newFold copies blk') + I.Break -> return $ D.singleton stmt + I.Forever b -> do + copies <- get + return $ D.singleton $ I.Forever (newFold copies b) + I.Comment{} -> return $ D.singleton stmt + where + newFold copies = D.toList . blockFold cxt opt copies +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 + +-------------------------------------------------------------------------------- +-- Expressions + +-- | Constant folding over expressions. +cf :: ExprOpt +cf copies ty e = + case e of + I.ExpSym{} -> e + I.ExpExtern{} -> e + I.ExpVar v -> Map.findWithDefault e v copies + I.ExpLit{} -> e + + I.ExpOp op args -> liftChoice copies ty op args + + I.ExpLabel t e0 s -> I.ExpLabel t (cf copies t e0) s + + I.ExpIndex t e0 t1 e1 -> I.ExpIndex t (cf copies t e0) t1 (cf copies t1 e1) + + I.ExpSafeCast t e0 -> + let e0' = cf copies t e0 + in fromMaybe (I.ExpSafeCast t e0') $ do + _ <- destLit e0' + return e0' + + I.ExpToIx e0 maxSz -> + let ty' = I.ixRep in + let e0' = cf copies ty' e0 in + case destIntegerLit e0' of + Just i -> I.ExpLit $ I.LitInteger $ i `rem` maxSz + Nothing -> I.ExpToIx e0' maxSz + + I.ExpAddrOfGlobal{} -> e + I.ExpMaxMin{} -> e + I.ExpSizeOf{} -> e + loopIncrFold :: (I.Expr -> I.Expr) -> I.LoopIncr -> I.LoopIncr loopIncrFold opt incr = case incr of I.IncrTo e0 -> I.IncrTo (opt e0) I.DecrTo e0 -> I.DecrTo (opt e0) -typedFold :: ExprOpt -> I.Typed I.Expr -> I.Typed I.Expr -typedFold opt tval@(I.Typed ty val) = tval { I.tValue = opt ty val } +-------------------------------------------------------------------------------- +typedFold :: ExprOpt -> CopyMap -> I.Typed I.Expr -> I.Typed I.Expr +typedFold opt copies tval@(I.Typed ty val) = tval { I.tValue = opt copies ty val } + arg0 :: [a] -> a arg0 = flip (!!) 0 @@ -143,231 +194,282 @@ arg2 :: [a] -> a arg2 = flip (!!) 2 -mkArgs :: I.Type -> [I.Expr] -> [I.Expr] -mkArgs ty = map (cf ty) - -mkCfArgs :: [I.Expr] -> [CfVal] -mkCfArgs = map toCfVal - -mkCfBool :: [I.Expr] -> [Maybe Bool] -mkCfBool = map destBoolLit - -- | Reconstruct an operator, folding away operations when possible. -cfOp :: I.Type -> I.ExpOp -> [I.Expr] -> I.Expr -cfOp ty op args = - case op of - I.ExpEq t -> cfOrd t - I.ExpNeq t -> cfOrd t - I.ExpCond - | Just b <- arg0 goBoolArgs - -> if b then arg1 (toExpr' ty) else arg2 (toExpr' ty) - | otherwise -> noop ty - I.ExpGt orEq t - | orEq -> goOrd t gteCheck args - | otherwise -> goOrd t gtCheck args - I.ExpLt orEq t - | orEq -> goOrd t gteCheck (reverse args) - | otherwise -> goOrd t gtCheck (reverse args) - I.ExpNot - | Just b <- arg0 goBoolArgs - -> I.ExpLit (I.LitBool (not b)) - | otherwise -> noop ty - I.ExpAnd - | Just lb <- arg0 goBoolArgs - , Just rb <- arg1 goBoolArgs - -> I.ExpLit (I.LitBool (lb && rb)) - | Just lb <- arg0 goBoolArgs - -> if lb then arg1 (toExpr' ty) else I.ExpLit (I.LitBool False) - | Just rb <- arg1 goBoolArgs - -> if rb then arg0 (toExpr' ty) else I.ExpLit (I.LitBool False) - | otherwise -> noop ty - I.ExpOr - | Just lb <- arg0 goBoolArgs - , Just rb <- arg1 goBoolArgs - -> I.ExpLit (I.LitBool (lb || rb)) - | Just lb <- arg0 goBoolArgs - -> if lb then I.ExpLit (I.LitBool True) else arg1 (toExpr' ty) - | Just rb <- arg1 goBoolArgs - -> if rb then I.ExpLit (I.LitBool True) else arg0 (toExpr' ty) - | otherwise -> noop ty +cfOp :: CopyMap -> I.Type -> I.ExpOp -> [I.Expr] -> I.Expr +cfOp copies ty op args = cfOp' ty op $ case op of + I.ExpEq t -> cfargs t args + I.ExpNeq t -> cfargs t args + I.ExpCond -> let (cond, rest) = splitAt 1 args in cfargs I.TyBool cond ++ cfargs ty rest + I.ExpGt _ t -> cfargs t args + I.ExpLt _ t -> cfargs t args + I.ExpIsNan t -> cfargs t args + I.ExpIsInf t -> cfargs t args + _ -> cfargs ty args + where + cfargs ty' = mkCfArgs ty' . map (cf copies ty') - I.ExpMul -> goNum - I.ExpAdd -> goNum - I.ExpSub -> goNum - I.ExpNegate -> goNum - I.ExpAbs -> goNum - I.ExpSignum -> goNum +cfOp' :: I.Type -> I.ExpOp -> [CfVal] -> I.Expr +cfOp' ty op args = case op of + I.ExpEq _ -> cfOrd + I.ExpNeq _ -> cfOrd + I.ExpCond + | CfBool b <- arg0 args + -> if b then a1 else a2 + -- If either branch is a boolean literal, reduce to logical AND or OR. + | ty == I.TyBool && arg1 args == CfBool True -> cfOp' ty I.ExpOr [arg0 args, arg2 args] + | ty == I.TyBool && arg1 args == CfBool False -> cfOp' ty I.ExpAnd $ mkCfArgs ty [cfOp' ty I.ExpNot [arg0 args]] ++ [arg2 args] + | ty == I.TyBool && arg2 args == CfBool True -> cfOp' ty I.ExpOr $ mkCfArgs ty [cfOp' ty I.ExpNot [arg0 args]] ++ [arg1 args] + | ty == I.TyBool && arg2 args == CfBool False -> cfOp' ty I.ExpAnd [arg0 args, arg1 args] + -- If both branches have the same result, we dont care about the branch + -- condition. XXX This can be expensive + | a1 == a2 + -> a1 + | otherwise -> noop + where a1 = toExpr $ arg1 args + a2 = toExpr $ arg2 args + I.ExpGt orEq t + | orEq -> goOrd t gteCheck args + | otherwise -> goOrd t gtCheck args + I.ExpLt orEq t + | orEq -> goOrd t gteCheck (reverse args) + | otherwise -> goOrd t gtCheck (reverse args) + I.ExpNot -> case arg0 args of + CfBool b -> I.ExpLit (I.LitBool (not b)) + CfExpr (I.ExpOp (I.ExpEq t) args') -> I.ExpOp (I.ExpNeq t) args' + CfExpr (I.ExpOp (I.ExpNeq t) args') -> I.ExpOp (I.ExpEq t) args' + CfExpr (I.ExpOp (I.ExpGt orEq t) args') -> I.ExpOp (I.ExpLt (not orEq) t) args' + CfExpr (I.ExpOp (I.ExpLt orEq t) args') -> I.ExpOp (I.ExpGt (not orEq) t) args' + _ -> noop + I.ExpAnd + | CfBool lb <- arg0 args + , CfBool rb <- arg1 args + -> I.ExpLit (I.LitBool (lb && rb)) + | CfBool lb <- arg0 args + -> if lb then toExpr $ arg1 args else I.ExpLit (I.LitBool False) + | CfBool rb <- arg1 args + -> if rb then toExpr $ arg0 args else I.ExpLit (I.LitBool False) + | otherwise -> noop + I.ExpOr + | CfBool lb <- arg0 args + , CfBool rb <- arg1 args + -> I.ExpLit (I.LitBool (lb || rb)) + | CfBool lb <- arg0 args + -> if lb then I.ExpLit (I.LitBool True) else toExpr $ arg1 args + | CfBool rb <- arg1 args + -> if rb then I.ExpLit (I.LitBool True) else toExpr $ arg0 args + | otherwise -> noop - I.ExpDiv -> goI2 - I.ExpMod -> goI2 - I.ExpRecip -> goF + I.ExpMul + | isLitValue 0 $ arg0 args -> toExpr $ arg0 args + | isLitValue 1 $ arg0 args -> toExpr $ arg1 args + | isLitValue (-1) $ arg0 args -> cfOp' ty I.ExpNegate [arg1 args] + | CfExpr (I.ExpOp I.ExpNegate [e']) <- arg0 args -> cfOp' ty I.ExpNegate $ mkCfArgs ty [cfOp' ty I.ExpMul $ mkCfArgs ty [e'] ++ [arg1 args]] + | isLitValue 0 $ arg1 args -> toExpr $ arg1 args + | isLitValue 1 $ arg1 args -> toExpr $ arg0 args + | isLitValue (-1) $ arg1 args -> cfOp' ty I.ExpNegate [arg0 args] + | CfExpr (I.ExpOp I.ExpNegate [e']) <- arg1 args -> cfOp' ty I.ExpNegate $ mkCfArgs ty [cfOp' ty I.ExpMul $ arg0 args : mkCfArgs ty [e']] + | otherwise -> goNum - I.ExpIsNan t -> goFB t - I.ExpIsInf t -> goFB t + I.ExpAdd + | isLitValue 0 $ arg0 args -> toExpr $ arg1 args + | isLitValue 0 $ arg1 args -> toExpr $ arg0 args + | CfExpr (I.ExpOp I.ExpNegate [e']) <- arg1 args -> cfOp' ty I.ExpSub $ arg0 args : mkCfArgs ty [e'] + | otherwise -> goNum - I.ExpFExp -> goF - I.ExpFSqrt -> goF - I.ExpFLog -> goF - I.ExpFPow -> goF - I.ExpFLogBase -> goF - I.ExpFSin -> goF - I.ExpFCos -> goF - I.ExpFTan -> goF - I.ExpFAsin -> goF - I.ExpFAcos -> goF - I.ExpFAtan -> goF - I.ExpFSinh -> goF - I.ExpFCosh -> goF - I.ExpFTanh -> goF - I.ExpFAsinh -> goF - I.ExpFAcosh -> goF - I.ExpFAtanh -> goF + I.ExpSub + | isLitValue 0 $ arg0 args -> cfOp' ty I.ExpNegate [arg1 args] + | isLitValue 0 $ arg1 args -> toExpr $ arg0 args + | CfExpr (I.ExpOp I.ExpNegate [e']) <- arg1 args -> cfOp' ty I.ExpAdd $ arg0 args : mkCfArgs ty [e'] + | otherwise -> goNum - I.ExpBitAnd -> toExpr (cfBitAnd ty $ goArgs ty) - I.ExpBitOr -> toExpr (cfBitOr ty $ goArgs ty) + I.ExpNegate -> case arg0 args of + CfExpr (I.ExpOp I.ExpNegate [e']) -> e' + CfExpr (I.ExpOp I.ExpSub [e1, e2]) -> cfOp' ty I.ExpSub $ mkCfArgs ty [e2, e1] + _ -> goNum - -- Unimplemented right now - I.ExpToFloat t -> noop t - I.ExpFromFloat t -> noop t - I.ExpRoundF -> noop ty - I.ExpCeilF -> noop ty - I.ExpFloorF -> noop ty - I.ExpBitXor -> noop ty - I.ExpBitComplement -> noop ty - I.ExpBitShiftL -> noop ty - I.ExpBitShiftR -> noop ty + I.ExpAbs -> goNum + I.ExpSignum -> goNum - where - goArgs ty' = mkCfArgs $ mkArgs ty' args - toExpr' = map toExpr . goArgs - goBoolArgs = mkCfBool $ mkArgs I.TyBool args - noop = I.ExpOp op . map toExpr . goArgs - goI2 = toExpr (cfIntOp2 ty op $ goArgs ty) - goF = toExpr (cfFloating op $ goArgs ty) - goFB ty' = toExpr (cfFloatingB op $ goArgs ty') - cfOrd ty' = toExpr (cfOrd2 op $ goArgs ty') - goOrd ty' chk args' = - let args0 = mkCfArgs $ mkArgs ty' args' in - fromOrdChecks (cfOrd ty') (chk ty' args0) - goNum = toExpr (cfNum ty op $ goArgs ty) + I.ExpDiv -> goI2 + I.ExpMod -> goI2 + I.ExpRecip -> goF + I.ExpIsNan _ -> goFB + I.ExpIsInf _ -> goFB -cfBitAnd :: I.Type -> [CfVal] -> CfVal -cfBitAnd ty [l,r] - | ones ty l = r - | ones ty r = l - | zeros ty l = CfInteger 0 - | zeros ty r = CfInteger 0 - | otherwise = CfExpr (I.ExpOp I.ExpBitAnd [toExpr l, toExpr r]) -cfBitAnd _ _ = err "Wrong number of args to cfBitAnd in constant folder." + I.ExpFExp -> goF + I.ExpFSqrt -> goF + I.ExpFLog -> goF + I.ExpFPow -> goF + I.ExpFLogBase -> goF + I.ExpFSin -> goF + I.ExpFCos -> goF + I.ExpFTan -> goF + I.ExpFAsin -> goF + I.ExpFAcos -> goF + I.ExpFAtan -> goF + I.ExpFAtan2 -> goF + I.ExpFSinh -> goF + I.ExpFCosh -> goF + I.ExpFTanh -> goF + I.ExpFAsinh -> goF + I.ExpFAcosh -> goF + I.ExpFAtanh -> goF -cfBitOr :: I.Type -> [CfVal] -> CfVal -cfBitOr ty [l,r] - | zeros ty l = r - | zeros ty r = l - | ones ty l = CfInteger 1 - | ones ty r = CfInteger 1 - | otherwise = CfExpr (I.ExpOp I.ExpBitOr [toExpr l, toExpr r]) -cfBitOr _ _ = err "Wrong number of args to cfBitOr in constant folder." + I.ExpBitAnd -> toExpr (cfBitAnd ty args) + I.ExpBitOr -> toExpr (cfBitOr ty args) --- Min values for word types. -zeros :: I.Type -> CfVal -> Bool -zeros I.TyWord{} (CfInteger i) = i == 0 -zeros _ _ = False + -- Unimplemented right now + I.ExpRoundF -> noop + I.ExpCeilF -> noop + I.ExpFloorF -> noop + I.ExpBitXor -> noop + I.ExpBitComplement -> noop + I.ExpBitShiftL -> noop + I.ExpBitShiftR -> noop --- Max values for word types. -ones :: I.Type -> CfVal -> Bool -ones ty (CfInteger i) = - case ty of - I.TyWord{} -> maybe False (i ==) (toMaxSize ty) - _ -> False -ones _ _ = False + where + noop = I.ExpOp op $ map toExpr args + goI2 = toExpr (cfIntOp2 ty op args) + goF = toExpr (cfFloating op args) + goFB = toExpr (cfFloatingB op args) + cfOrd = toExpr (cfOrd2 op args) + goOrd ty' chk args' = fromOrdChecks cfOrd (chk ty' args') + goNum = toExpr (cfNum ty op args) --- | Literal expression destructor. -destLit :: I.Expr -> Maybe I.Literal -destLit ex = case ex of - I.ExpLit lit -> return lit - _ -> mzero +-------------------------------------------------------------------------------- --- | Boolean literal destructor. -destBoolLit :: I.Expr -> Maybe Bool -destBoolLit ex = do - I.LitBool b <- destLit ex - return b +-- | Lift nondeterministic choice up see see if we can further optimize. +liftChoice :: CopyMap -> I.Type -> I.ExpOp -> [I.Expr] -> I.Expr +liftChoice copies ty op args = case op of + I.ExpEq{} -> go2 + I.ExpNeq{} -> go2 + -- I.ExpCond --unnecessary + I.ExpGt{} -> go2 + I.ExpLt{} -> go2 --- | Integer literal destructor. -destIntegerLit :: I.Expr -> Maybe Integer -destIntegerLit ex = do - I.LitInteger i <- destLit ex - return i + I.ExpNot{} -> go1 + I.ExpAnd{} -> go2 + I.ExpOr{} -> go2 --- | Float literal destructor. -destFloatLit :: I.Expr -> Maybe Float -destFloatLit ex = do - I.LitFloat i <- destLit ex - return i + I.ExpMul -> go2 + I.ExpAdd -> go2 + I.ExpSub -> go2 + I.ExpNegate -> go1 + I.ExpAbs -> go1 + I.ExpSignum -> go1 --- | Double literal destructor. -destDoubleLit :: I.Expr -> Maybe Double -destDoubleLit ex = do - I.LitDouble i <- destLit ex - return i + -- -- NOT SAFE TO LIFT! + -- I.ExpDiv -> --NO! --- Constant-folded Values ------------------------------------------------------ + -- Unimplemented currently: add as needed + -- I.ExpMod -> + -- I.ExpRecip -> + -- I.ExpIsNan{} -> + -- I.ExpIsInf{} -> + -- I.ExpFExp -> + -- I.ExpFSqrt -> + -- I.ExpFLog -> + -- I.ExpFPow -> + -- I.ExpFLogBase -> + -- I.ExpFSin -> + -- I.ExpFCos -> + -- I.ExpFTan -> + -- I.ExpFAsin -> + -- I.ExpFAcos -> + -- I.ExpFAtan -> + -- I.ExpFAtan2 -> + -- I.ExpFSinh -> + -- I.ExpFCosh -> + -- I.ExpFTanh -> + -- I.ExpFAsinh -> + -- I.ExpFAcosh -> + -- I.ExpFAtanh -> + -- I.ExpBitAnd -> + -- I.ExpBitOr -> + -- -- Unimplemented right now + -- I.ExpRoundF -> + -- I.ExpCeilF -> + -- I.ExpFloorF -> + -- I.ExpBitXor -> + -- I.ExpBitComplement -> + -- I.ExpBitShiftL -> + -- I.ExpBitShiftR -> + _ -> cfOp copies ty op args + where + go1 = unOpLift copies ty op args + go2 = binOpLift copies ty op args --- | Constant-folded values. -data CfVal - = CfBool Bool - | CfInteger Integer - | CfFloat Float - | CfDouble Double - | CfExpr I.Expr - deriving (Show) --- | Convert to a constant-folded value. Picks the one successful lit, if any. -toCfVal :: I.Expr -> CfVal -toCfVal ex = fromMaybe (CfExpr ex) $ msum - [ CfBool `fmap` destBoolLit ex - , CfInteger `fmap` destIntegerLit ex - , CfFloat `fmap` destFloatLit ex - , CfDouble `fmap` destDoubleLit ex - ] +--XXX the equality comparisons below can be expensive. Hashmap? Also, awkward +-- style, but I want sharing of (liftChoice ...) expression in branch condition +-- and result. +unOpLift :: CopyMap -> I.Type -> I.ExpOp -> [I.Expr] -> I.Expr +unOpLift copies ty op args = case a0 of + I.ExpOp I.ExpCond [_,x1,x2] + -> let a = lt x1 in + if a == lt x2 then a else c + _ -> c + where + a0 = arg0 args + lt x = liftChoice copies ty op [x] + c = cfOp copies ty op args --- | Convert back to an expression. -toExpr :: CfVal -> I.Expr -toExpr val = case val of - CfBool b -> I.ExpLit (I.LitBool b) - CfInteger i -> I.ExpLit (I.LitInteger i) - CfFloat f -> I.ExpLit (I.LitFloat f) - CfDouble d -> I.ExpLit (I.LitDouble d) - CfExpr ex -> ex +binOpLift :: CopyMap -> I.Type -> I.ExpOp -> [I.Expr] -> I.Expr +binOpLift copies ty op args = case a0 of + I.ExpOp I.ExpCond [_,x1,x2] + -> let a = lt0 x1 in + if a == lt0 x2 then a else c + _ -> case a1 of + I.ExpOp I.ExpCond [_,x1,x2] + -> let a = lt1 x1 in + if a == lt1 x2 then a else c + _ -> c + where + a0 = arg0 args + a1 = arg1 args + lt0 x = lt x a1 + lt1 x = lt a0 x + lt a b = liftChoice copies ty op [a, b] + c = cfOp copies ty op args +-------------------------------------------------------------------------------- +-- Constant-folded values + -- | Check if we're comparing the max or min bound for >= and optimize. +-- Assumes args are already folded. gteCheck :: I.Type -> [CfVal] -> Maybe Bool gteCheck t [l,r] -- forall a. max >= a - | CfInteger x <- l + | CfInteger _ x <- l , Just s <- toMaxSize t - , x == s = Just True + , x == s + = Just True -- forall a. a >= min - | CfInteger y <- r + | CfInteger _ y <- r , Just s <- toMinSize t - , y == s = Just True - | otherwise = Nothing + , y == s + = Just True + | otherwise + = Nothing gteCheck _ _ = err "wrong number of args to gtCheck." -- | Check if we're comparing the max or min bound for > and optimize. +-- Assumes args are already folded. gtCheck :: I.Type -> [CfVal] -> Maybe Bool gtCheck t [l,r] -- forall a. not (min > a) - | CfInteger x <- l + | CfInteger _ x <- l , Just s <- toMinSize t - , x == s = Just False + , x == s + = Just False -- forall a. not (a > max) - | CfInteger y <- r + | CfInteger _ y <- r , Just s <- toMaxSize t - , y == s = Just False - | otherwise = Nothing + , y == s + = Just False + | otherwise + = Nothing gtCheck _ _ = err "wrong number of args to gtCheck." fromOrdChecks :: I.Expr -> Maybe Bool -> I.Expr @@ -378,10 +480,10 @@ -> [CfVal] -> CfVal cfOrd2 op [l,r] = case (l,r) of - (CfBool x, CfBool y) -> CfBool (op' x y) - (CfInteger x,CfInteger y) -> CfBool (op' x y) - (CfFloat x, CfFloat y) -> CfBool (op' x y) - (CfDouble x, CfDouble y) -> CfBool (op' x y) + (CfBool x, CfBool y) -> CfBool (op' x y) + (CfInteger _ x,CfInteger _ y) -> CfBool (op' x y) + (CfFloat x, CfFloat y) -> CfBool (op' x y) + (CfDouble x, CfDouble y) -> CfBool (op' x y) _ -> CfExpr (I.ExpOp op [toExpr l, toExpr r]) where op' :: Ord a => a -> a -> Bool @@ -397,182 +499,3 @@ _ -> err "bad op to cfOrd2" cfOrd2 _ _ = err "wrong number of args to cfOrd2" --------------------------------------------------------------------------------- - -class Integral a => IntegralOp a where - appI1 :: (a -> a) -> a -> CfVal - appI1 op x = CfInteger $ toInteger $ op x - - appI2 :: (a -> a -> a) -> a -> a -> CfVal - appI2 op x y = CfInteger $ toInteger $ op x y - -instance IntegralOp Int8 -instance IntegralOp Int16 -instance IntegralOp Int32 -instance IntegralOp Int64 -instance IntegralOp Word8 -instance IntegralOp Word16 -instance IntegralOp Word32 -instance IntegralOp Word64 - --------------------------------------------------------------------------------- - -cfNum :: I.Type - -> I.ExpOp - -> [CfVal] - -> CfVal -cfNum ty op args = case args of - [x] -> case x of - CfInteger l -> case ty of - I.TyInt isz -> case isz of - I.Int8 -> appI1 op1 (fromInteger l :: Int8) - I.Int16 -> appI1 op1 (fromInteger l :: Int16) - I.Int32 -> appI1 op1 (fromInteger l :: Int32) - I.Int64 -> appI1 op1 (fromInteger l :: Int64) - I.TyWord isz -> case isz of - I.Word8 -> appI1 op1 (fromInteger l :: Word8) - I.Word16 -> appI1 op1 (fromInteger l :: Word16) - I.Word32 -> appI1 op1 (fromInteger l :: Word32) - I.Word64 -> appI1 op1 (fromInteger l :: Word64) - _ -> err $ "bad type to cfNum loc 1 " - CfFloat l -> CfFloat (op1 l) - CfDouble l -> CfDouble (op1 l) - _ -> CfExpr (I.ExpOp op [toExpr x]) - - [x,y] -> case (x,y) of - (CfInteger l, CfInteger r) -> case ty of - I.TyInt isz -> case isz of - I.Int8 -> appI2 op2 (fromInteger l :: Int8) - (fromInteger r :: Int8) - I.Int16 -> appI2 op2 (fromInteger l :: Int16) - (fromInteger r :: Int16) - I.Int32 -> appI2 op2 (fromInteger l :: Int32) - (fromInteger r :: Int32) - I.Int64 -> appI2 op2 (fromInteger l :: Int64) - (fromInteger r :: Int64) - I.TyWord isz -> case isz of - I.Word8 -> appI2 op2 (fromInteger l :: Word8) - (fromInteger r :: Word8) - I.Word16 -> appI2 op2 (fromInteger l :: Word16) - (fromInteger r :: Word16) - I.Word32 -> appI2 op2 (fromInteger l :: Word32) - (fromInteger r :: Word32) - I.Word64 -> appI2 op2 (fromInteger l :: Word64) - (fromInteger r :: Word64) - _ -> err "bad type to cfNum loc 2" - (CfFloat l, CfFloat r) -> CfFloat (op2 l r) - (CfDouble l, CfDouble r) -> CfDouble (op2 l r) - _ -> CfExpr (I.ExpOp op [toExpr x, toExpr y]) - - _ -> err "wrong num args to cfNum" - where - op2 :: Num a => a -> a -> a - op2 = case op of - I.ExpMul -> (*) - I.ExpAdd -> (+) - I.ExpSub -> (-) - _ -> err "bad op to cfNum loc 3" - op1 :: Num a => a -> a - op1 = case op of - I.ExpNegate -> negate - I.ExpAbs -> abs - I.ExpSignum -> signum - _ -> err "bad op to cfNum loc 4" - -cfIntOp2 :: I.Type -> I.ExpOp -> [CfVal] -> CfVal -cfIntOp2 ty iOp [CfInteger l, CfInteger r] = case ty of - I.TyInt isz -> case isz of - I.Int8 -> appI2 op2 (fromInteger l :: Int8) - (fromInteger r :: Int8) - I.Int16 -> appI2 op2 (fromInteger l :: Int16) - (fromInteger r :: Int16) - I.Int32 -> appI2 op2 (fromInteger l :: Int32) - (fromInteger r :: Int32) - I.Int64 -> appI2 op2 (fromInteger l :: Int64) - (fromInteger r :: Int64) - I.TyWord isz -> case isz of - I.Word8 -> appI2 op2 (fromInteger l :: Word8) - (fromInteger r :: Word8) - I.Word16 -> appI2 op2 (fromInteger l :: Word16) - (fromInteger r :: Word16) - I.Word32 -> appI2 op2 (fromInteger l :: Word32) - (fromInteger r :: Word32) - I.Word64 -> appI2 op2 (fromInteger l :: Word64) - (fromInteger r :: Word64) - _ -> err "bad type to cfIntOp2 loc 1" - - where - op2 :: Integral a => a -> a -> a - op2 = case iOp of - I.ExpDiv -> quot - -- Haskell's `rem` matches C ISO 1999 semantics of the remainder having the - -- same sign as the dividend. - I.ExpMod -> rem - _ -> err "bad op to cfIntOp2" - -cfIntOp2 _ iOp [x, y] = CfExpr (I.ExpOp iOp [toExpr x, toExpr y]) -cfIntOp2 _ _ _ = err "wrong number of args to cfOp2" - --------------------------------------------------------------------------------- - --- | Constant folding for unary operations that require a floating instance. -cfFloating :: I.ExpOp - -> [CfVal] - -> CfVal -cfFloating op args = case args of - [x] -> case x of - CfFloat f -> CfFloat (op1 f) - CfDouble d -> CfDouble (op1 d) - _ -> CfExpr (I.ExpOp op [toExpr x]) - [x,y] -> case (x,y) of - (CfFloat l, CfFloat r) -> CfFloat (op2 l r) - (CfDouble l, CfDouble r) -> CfDouble (op2 l r) - _ -> CfExpr (I.ExpOp op [toExpr x - , toExpr y]) - _ -> err "wrong number of args to cfFloating" - where - op1 :: Floating a => a -> a - op1 = case op of - I.ExpRecip -> recip - I.ExpFExp -> exp - I.ExpFSqrt -> sqrt - I.ExpFLog -> log - I.ExpFSin -> sin - I.ExpFCos -> cos - I.ExpFTan -> tan - I.ExpFAsin -> asin - I.ExpFAcos -> acos - I.ExpFAtan -> atan - I.ExpFSinh -> sinh - I.ExpFCosh -> cosh - I.ExpFTanh -> tanh - I.ExpFAsinh -> asinh - I.ExpFAcosh -> acosh - I.ExpFAtanh -> atanh - _ -> err "wrong op1 to cfFloating" - - op2 :: Floating a => a -> a -> a - op2 = case op of - I.ExpFPow -> (**) - I.ExpFLogBase -> logBase - _ -> err "wrong op2 to cfFloating" - -cfFloatingB :: I.ExpOp - -> [CfVal] - -> CfVal -cfFloatingB op [x] = case x of - CfFloat f -> CfBool (op' f) - CfDouble d -> CfBool (op' d) - _ -> CfExpr (I.ExpOp op [toExpr x]) - where - op' :: RealFloat a => a -> Bool - op' = case op of - I.ExpIsNan _ -> isNaN - I.ExpIsInf _ -> isInfinite - _ -> err "wrong op to cfFloatingB" -cfFloatingB _ _ = err "wrong number of args to cfFloatingB" - --------------------------------------------------------------------------------- - -err :: String -> a -err msg = error $ "Ivory-Opts internal error: " ++ msg diff --git a/src/Ivory/Opts/ConstFoldComp.hs b/src/Ivory/Opts/ConstFoldComp.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Opts/ConstFoldComp.hs @@ -0,0 +1,391 @@ +{-# LANGUAGE ViewPatterns #-} + +-- +-- Constant folding computations in Haskell. +-- +-- Copyright (C) 2014, Galois, Inc. +-- All rights reserved. +-- + +module Ivory.Opts.ConstFoldComp + ( CfVal(..) + , err + , toExpr + , destLit + , destBoolLit + , destIntegerLit + , isLitValue + , mkCfArgs + , cfNum + , cfBitAnd + , cfBitOr + , cfFloating + , cfFloatingB + , cfIntOp2 + ) where + +import qualified Ivory.Language.Syntax.AST as I +import qualified Ivory.Language.Syntax.Type as I +import Ivory.Language.Cast (toMaxSize, toMinSize) + +import Control.Monad (mzero,msum) +import Data.Bits +import Data.Maybe + +import Data.Word +import Data.Int + +-------------------------------------------------------------------------------- + +-- | Constant-folded values. +data CfVal + = CfBool Bool + -- Is this a max or min value for the size type? + | CfInteger MaxMin Integer + | CfFloat Float + | CfDouble Double + | CfExpr I.Expr + deriving (Show, Eq) + +-- | Convert back to an expression. +toExpr :: CfVal -> I.Expr +toExpr val = case val of + CfBool b -> I.ExpLit (I.LitBool b) + CfInteger m i -> case m of + Min -> I.ExpMaxMin False + Max -> I.ExpMaxMin True + None -> I.ExpLit (I.LitInteger i) + CfFloat f -> I.ExpLit (I.LitFloat f) + CfDouble d -> I.ExpLit (I.LitDouble d) + CfExpr ex -> ex + +-------------------------------------------------------------------------------- + +-- | Whether the bounded integer represents a max or min value for its size. +data MaxMin = Max | Min | None deriving (Show, Read, Eq) + +isMaxMin :: I.Type -> Integer -> MaxMin +isMaxMin ty i + | Just m <- toMaxSize ty + , m == i + = Max + | Just m <- toMinSize ty + , m == i + = Min + | otherwise + = None + +toMaxMin :: (Eq a, Bounded a) => a -> MaxMin +toMaxMin r | r == maxBound = Max + | r == minBound = Min + | otherwise = None + +-------------------------------------------------------------------------------- + +mkCfArgs :: I.Type -> [I.Expr] -> [CfVal] +mkCfArgs ty exps = map toCfVal exps + where + -- | Convert to a constant-folded value. Picks the one successful lit, if any. + toCfVal :: I.Expr -> CfVal + toCfVal ex = fromMaybe (CfExpr ex) $ msum + [ CfBool `fmap` destBoolLit ex + , CfFloat `fmap` destFloatLit ex + , CfDouble `fmap` destDoubleLit ex + , (uncurry CfInteger) `fmap` (destMinMaxIntegerLit ex) + ] + + -- | Minimum, maximum, or integer value. + destMinMaxIntegerLit :: I.Expr -> Maybe (MaxMin, Integer) + destMinMaxIntegerLit ex = case ex of + I.ExpMaxMin True -> do s <- toMaxSize ty + return (Max, s) + I.ExpMaxMin False -> do s <- toMinSize ty + return (Min, s) + I.ExpLit (I.LitInteger i) -> Just (isMaxMin ty i, i) + _ -> Nothing + + +cfBitAnd :: I.Type -> [CfVal] -> CfVal +cfBitAnd ty [l, r] = case (ty, l, r) of + (I.TyWord _, CfInteger Min _, _) -> l + (I.TyWord _, CfInteger Max _, _) -> r + (I.TyWord _, _, CfInteger Min _) -> r + (I.TyWord _, _, CfInteger Max _) -> l + _ -> abc (combineBits (.&.)) ty I.ExpBitAnd l r +cfBitAnd _ _ = err "Wrong number of args to cfBitAnd in constant folder." + +cfBitOr :: I.Type -> [CfVal] -> CfVal +cfBitOr ty [l, r] = case (ty, l, r) of + (I.TyWord _, CfInteger Min _, _) -> r + (I.TyWord _, CfInteger Max _, _) -> l + (I.TyWord _, _, CfInteger Min _) -> l + (I.TyWord _, _, CfInteger Max _) -> r + _ -> abc (combineBits (.|.)) ty I.ExpBitOr l r +cfBitOr _ _ = err "Wrong number of args to cfBitOr in constant folder." + + +combineBits :: (Integer -> Integer -> Integer) -> I.ExpOp -> CfVal -> CfVal -> CfVal +combineBits f _ (CfInteger _ x) (CfInteger _ y) = CfInteger None $ f x y +combineBits _ op x y = CfExpr $ I.ExpOp op [toExpr x, toExpr y] + +-------------------------------------------------------------------------------- + +---------------------------------------- +-- Gather constants from an associative/commutative tree of operators + +{- +Rules for normalizing constants in Associative Binary Commutative operators: + +op [const, const]: evaluate the op. (establishes that each op has at least one non-const child) +op [const, var] -> cf op [var, const] (allowed by commutativity; establishes that consts are only right-children) +op [a, op [b, c]] -> cf op [cf op [a, b], c] (allowed by associativity; establishes that right child is not this op, so can't contain more constants) +op [op [var, const], const] -> op [var, cf op [const, const]] (allowed by associativity; establishes that if right-child is const, left-child does not contain any constants) +op [op [var1, const], var2] -> op [op [var1, var2], const] (allowed by associativity and commutativity; establishes that left-child does not contain constants; note that var1 and var2 can't contain constants by these rules) +anything else: unchanged + +These rules assume that the operands have already had these rules +applied bottom-up, and avoid re-doing any work in subtrees that haven't +changed. +-} + +abc :: (I.ExpOp -> CfVal -> CfVal -> CfVal) -> I.Type -> I.ExpOp -> CfVal -> CfVal -> CfVal +abc combine ty op (CfExpr lhs) rhs = case (lhs, rhs) of + (_, CfExpr (I.ExpOp op' (mkCfArgs ty -> [b, c]))) | op == op' -> abc combine ty op (abc combine ty op (CfExpr lhs) b) c + (I.ExpOp _ (_ : (mkCfArgs ty -> [CfExpr _])), _) -> noop + (I.ExpOp op' [a, b], CfExpr c) | op == op' -> CfExpr (I.ExpOp op [I.ExpOp op [a, c], b]) + (I.ExpOp op' (a : (mkCfArgs ty -> [b])), c) | op == op' -> CfExpr (I.ExpOp op [a, toExpr $ combine op b c]) + _ -> noop + where + noop = CfExpr (I.ExpOp op [lhs, toExpr rhs]) +abc combine ty op lhs rhs@(CfExpr _) = abc combine ty op rhs lhs +abc combine _ op lhs rhs = combine op lhs rhs + +-------------------------------------------------------------------------------- + +---------------------------------------- +-- Constant folded Haskell literals + +-- | Literal expression destructor. +destLit :: I.Expr -> Maybe I.Literal +destLit ex = case ex of + I.ExpLit lit -> return lit + _ -> mzero + +-- | Boolean literal destructor. +destBoolLit :: I.Expr -> Maybe Bool +destBoolLit ex = do + I.LitBool b <- destLit ex + return b + +-- | Integer literal destructor. +destIntegerLit :: I.Expr -> Maybe Integer +destIntegerLit ex = do + I.LitInteger i <- destLit ex + return i + +-- | Float literal destructor. +destFloatLit :: I.Expr -> Maybe Float +destFloatLit ex = do + I.LitFloat i <- destLit ex + return i + +-- | Double literal destructor. +destDoubleLit :: I.Expr -> Maybe Double +destDoubleLit ex = do + I.LitDouble i <- destLit ex + return i + +isLitValue :: Integer -> CfVal -> Bool +isLitValue v (CfInteger _ v') = v == v' +isLitValue v (CfFloat v') = fromInteger v == v' +isLitValue v (CfDouble v') = fromInteger v == v' +isLitValue _ _ = False +---------------------------------------- + + +class (Bounded a, Integral a) => IntegralOp a where + appI1 :: (a -> a) -> a -> CfVal + appI1 op x = let r = op x in + CfInteger (toMaxMin r) (toInteger r) + + appI2 :: (a -> a -> a) -> a -> a -> CfVal + appI2 op x y = let r = op x y in + CfInteger (toMaxMin r) (toInteger r) + +instance IntegralOp Int8 +instance IntegralOp Int16 +instance IntegralOp Int32 +instance IntegralOp Int64 +instance IntegralOp Word8 +instance IntegralOp Word16 +instance IntegralOp Word32 +instance IntegralOp Word64 + +-------------------------------------------------------------------------------- + +cfNum :: I.Type + -> I.ExpOp + -> [CfVal] + -> CfVal +cfNum ty op args = case args of + [x] -> case x of + CfInteger _ l -> case ty of + I.TyInt isz -> case isz of + I.Int8 -> appI1 op1 (fromInteger l :: Int8) + I.Int16 -> appI1 op1 (fromInteger l :: Int16) + I.Int32 -> appI1 op1 (fromInteger l :: Int32) + I.Int64 -> appI1 op1 (fromInteger l :: Int64) + I.TyWord isz -> case isz of + I.Word8 -> appI1 op1 (fromInteger l :: Word8) + I.Word16 -> appI1 op1 (fromInteger l :: Word16) + I.Word32 -> appI1 op1 (fromInteger l :: Word32) + I.Word64 -> appI1 op1 (fromInteger l :: Word64) + I.TyIndex _n -> appI1 op1 (fromInteger l :: Int32) + _ -> err $ "bad type to cfNum loc 1 " + CfFloat l -> CfFloat (op1 l) + CfDouble l -> CfDouble (op1 l) + _ -> CfExpr (I.ExpOp op [toExpr x]) + + [x,y] -> case (x,y) of + (CfInteger _ l, CfInteger _ r) -> case ty of + I.TyInt isz -> case isz of + I.Int8 -> appI2 op2 (fromInteger l :: Int8) + (fromInteger r :: Int8) + I.Int16 -> appI2 op2 (fromInteger l :: Int16) + (fromInteger r :: Int16) + I.Int32 -> appI2 op2 (fromInteger l :: Int32) + (fromInteger r :: Int32) + I.Int64 -> appI2 op2 (fromInteger l :: Int64) + (fromInteger r :: Int64) + I.TyWord isz -> case isz of + I.Word8 -> appI2 op2 (fromInteger l :: Word8) + (fromInteger r :: Word8) + I.Word16 -> appI2 op2 (fromInteger l :: Word16) + (fromInteger r :: Word16) + I.Word32 -> appI2 op2 (fromInteger l :: Word32) + (fromInteger r :: Word32) + I.Word64 -> appI2 op2 (fromInteger l :: Word64) + (fromInteger r :: Word64) + I.TyIndex _n -> appI2 op2 (fromInteger l :: Int32) + (fromInteger r :: Int32) + _ -> err "bad type to cfNum loc 2" + (CfFloat l, CfFloat r) -> CfFloat (op2 l r) + (CfDouble l, CfDouble r) -> CfDouble (op2 l r) + _ -> CfExpr (I.ExpOp op [toExpr x, toExpr y]) + + _ -> err "wrong num args to cfNum" + where + op2 :: Num a => a -> a -> a + op2 = case op of + I.ExpMul -> (*) + I.ExpAdd -> (+) + I.ExpSub -> (-) + _ -> err "bad op to cfNum loc 3" + op1 :: Num a => a -> a + op1 = case op of + I.ExpNegate -> negate + I.ExpAbs -> abs + I.ExpSignum -> signum + _ -> err "bad op to cfNum loc 4" + +cfIntOp2 :: I.Type -> I.ExpOp -> [CfVal] -> CfVal +cfIntOp2 ty iOp [CfInteger _ l, CfInteger _ r] = case ty of + I.TyInt isz -> case isz of + I.Int8 -> appI2 op2 (fromInteger l :: Int8) + (fromInteger r :: Int8) + I.Int16 -> appI2 op2 (fromInteger l :: Int16) + (fromInteger r :: Int16) + I.Int32 -> appI2 op2 (fromInteger l :: Int32) + (fromInteger r :: Int32) + I.Int64 -> appI2 op2 (fromInteger l :: Int64) + (fromInteger r :: Int64) + I.TyWord isz -> case isz of + I.Word8 -> appI2 op2 (fromInteger l :: Word8) + (fromInteger r :: Word8) + I.Word16 -> appI2 op2 (fromInteger l :: Word16) + (fromInteger r :: Word16) + I.Word32 -> appI2 op2 (fromInteger l :: Word32) + (fromInteger r :: Word32) + I.Word64 -> appI2 op2 (fromInteger l :: Word64) + (fromInteger r :: Word64) + I.TyIndex _n -> appI2 op2 (fromInteger l :: Int32) + (fromInteger r :: Int32) + _ -> err "bad type to cfIntOp2 loc 1" + + where + op2 :: Integral a => a -> a -> a + op2 = case iOp of + I.ExpDiv -> quot + -- Haskell's `rem` matches C ISO 1999 semantics of the remainder having the + -- same sign as the dividend. + I.ExpMod -> rem + _ -> err "bad op to cfIntOp2" + +cfIntOp2 _ iOp [x, y] = CfExpr (I.ExpOp iOp [toExpr x, toExpr y]) +cfIntOp2 _ _ _ = err "wrong number of args to cfOp2" + +-------------------------------------------------------------------------------- + +-- | Constant folding for unary operations that require a floating instance. +cfFloating :: I.ExpOp + -> [CfVal] + -> CfVal +cfFloating op args = case args of + [x] -> case x of + CfFloat f -> CfFloat (op1 f) + CfDouble d -> CfDouble (op1 d) + _ -> CfExpr (I.ExpOp op [toExpr x]) + [x,y] -> case (x,y) of + (CfFloat l, CfFloat r) -> CfFloat (op2 l r) + (CfDouble l, CfDouble r) -> CfDouble (op2 l r) + _ -> CfExpr (I.ExpOp op [toExpr x + , toExpr y]) + _ -> err "wrong number of args to cfFloating" + where + op1 :: Floating a => a -> a + op1 = case op of + I.ExpRecip -> recip + I.ExpFExp -> exp + I.ExpFSqrt -> sqrt + I.ExpFLog -> log + I.ExpFSin -> sin + I.ExpFCos -> cos + I.ExpFTan -> tan + I.ExpFAsin -> asin + I.ExpFAcos -> acos + I.ExpFAtan -> atan + I.ExpFSinh -> sinh + I.ExpFCosh -> cosh + I.ExpFTanh -> tanh + I.ExpFAsinh -> asinh + I.ExpFAcosh -> acosh + I.ExpFAtanh -> atanh + _ -> err "wrong op1 to cfFloating" + + op2 :: RealFloat a => a -> a -> a + op2 = case op of + I.ExpFPow -> (**) + I.ExpFLogBase -> logBase + I.ExpFAtan2 -> atan2 + _ -> err "wrong op2 to cfFloating" + +cfFloatingB :: I.ExpOp + -> [CfVal] + -> CfVal +cfFloatingB op [x] = case x of + CfFloat f -> CfBool (op' f) + CfDouble d -> CfBool (op' d) + _ -> CfExpr (I.ExpOp op [toExpr x]) + where + op' :: RealFloat a => a -> Bool + op' = case op of + I.ExpIsNan _ -> isNaN + I.ExpIsInf _ -> isInfinite + _ -> err "wrong op to cfFloatingB" +cfFloatingB _ _ = err "wrong number of args to cfFloatingB" + +-------------------------------------------------------------------------------- + +err :: String -> a +err msg = error $ "Ivory-Opts internal error: " ++ msg + diff --git a/src/Ivory/Opts/DivZero.hs b/src/Ivory/Opts/DivZero.hs --- a/src/Ivory/Opts/DivZero.hs +++ b/src/Ivory/Opts/DivZero.hs @@ -8,19 +8,19 @@ import Ivory.Opts.AssertFold -import qualified Ivory.Language.Syntax.AST as I +import qualified Ivory.Language.Syntax.AST as I import qualified Ivory.Language.Syntax.Type as I -------------------------------------------------------------------------------- divZeroFold :: I.Proc -> I.Proc -divZeroFold = procFold (expFoldDefault divAssert) +divZeroFold = procFold "divZ" (expFoldDefault divAssert) -------------------------------------------------------------------------------- -- Claim that the divisor expression cannnot equal zero. If we don't have a -- division-causing expression, return Nothing. -divAssert :: I.Type -> I.Expr -> [I.Expr] +divAssert :: I.Type -> I.Expr -> FolderStmt () divAssert ty e0 = case e0 of I.ExpOp op args -> case (op,args) of @@ -29,14 +29,15 @@ (I.ExpRecip,[e]) -> ma e (I.ExpFLog,[e]) -> ma e (I.ExpFLogBase,[_,r]) -> ma r - _ -> [] - _ -> [] + _ -> return () + _ -> return () where - ma x = [I.ExpOp (I.ExpNeq ty) [x,zeroExp]] + ma x = insert $ I.CompilerAssert $ I.ExpOp (I.ExpNeq ty) [x,zeroExp] zeroExp = case ty of I.TyInt _ -> I.ExpLit (I.LitInteger 0) I.TyWord _ -> I.ExpLit (I.LitInteger 0) + I.TyIndex _-> I.ExpLit (I.LitInteger 0) I.TyFloat -> I.ExpLit (I.LitFloat 0) I.TyDouble -> I.ExpLit (I.LitDouble 0) _ -> error $ diff --git a/src/Ivory/Opts/FP.hs b/src/Ivory/Opts/FP.hs --- a/src/Ivory/Opts/FP.hs +++ b/src/Ivory/Opts/FP.hs @@ -18,20 +18,20 @@ -------------------------------------------------------------------------------- fpFold :: I.Proc -> I.Proc -fpFold = procFold (expFoldDefault fpAssert) +fpFold = procFold "fp" (expFoldDefault fpAssert) -------------------------------------------------------------------------------- -- We're assuming we don't have to check lits---that you'd never actually -- construct a literal inf or NaN value! -fpAssert :: I.Type -> I.Expr -> [I.Expr] +fpAssert :: I.Type -> I.Expr -> FolderStmt () fpAssert ty e = case ty of I.TyFloat -> asst I.TyDouble -> asst - _ -> [] - where asst = [mkAssert ty e] + _ -> return () + where asst = insert (mkAssert ty e) -mkAssert :: I.Type -> I.Expr -> I.Expr -mkAssert ty e = I.ExpOp I.ExpAnd +mkAssert :: I.Type -> I.Expr -> I.Stmt +mkAssert ty e = I.CompilerAssert $ I.ExpOp I.ExpAnd [ I.ExpOp I.ExpNot [I.ExpOp (I.ExpIsNan ty) [e]] , I.ExpOp I.ExpNot [I.ExpOp (I.ExpIsInf ty) [e]] ] diff --git a/src/Ivory/Opts/Index.hs b/src/Ivory/Opts/Index.hs --- a/src/Ivory/Opts/Index.hs +++ b/src/Ivory/Opts/Index.hs @@ -7,62 +7,53 @@ ( ixFold ) where -import qualified Data.DList as D - import Ivory.Opts.AssertFold import Ivory.Opts.Utils -import qualified Ivory.Language.Syntax.AST as I +import qualified Ivory.Language.Array as I +import qualified Ivory.Language.Syntax.AST as I import qualified Ivory.Language.Syntax.Type as I -------------------------------------------------------------------------------- ixFold :: I.Proc -> I.Proc -ixFold = procFold expFold +ixFold = procFold "ix" expFold -------------------------------------------------------------------------------- -- | Default expression folder that performs the recursion for an asserter. -expFold :: I.Type -> I.Expr -> [I.Expr] -expFold ty e = - let (_, ds) = runFolderM (expFold' ty e) in - D.toList ds - --- Here was use a custom folder (and not the expFoldDefault in AssertFold) since +-- Here we use a custom folder (and not the expFoldDefault in AssertFold) since -- the index checks are indepdent of control-flow (from the (x ? y : z) -- expression) and we want to explicitly pattern-match for Ix expressions. -expFold' :: I.Type -> I.Expr -> FolderExpr () -expFold' ty e = case e of +expFold :: I.Type -> I.Expr -> FolderStmt () +expFold ty e = case e of I.ExpSym{} -> return () + I.ExpExtern{} -> return () I.ExpVar{} -> return () I.ExpLit{} -> return () - I.ExpLabel ty' e0 _str -> expFold' ty' e0 - I.ExpIndex tIdx eIdx tArr eArr -> do expFold' tIdx eIdx - expFold' tArr eArr + I.ExpLabel ty' e0 _str -> expFold ty' e0 + I.ExpIndex tIdx eIdx tArr eArr -> do expFold tIdx eIdx + expFold tArr eArr I.ExpToIx e0 maxSz -> do insert (toIxAssert e0 maxSz) - expFold' ixTy e0 - I.ExpSafeCast ty' e0 -> expFold' ty' e0 - I.ExpOp op args -> mapM_ (expFold' $ expOpType ty op) args + expFold I.ixRep e0 + I.ExpSafeCast ty' e0 -> expFold ty' e0 + I.ExpOp op args -> mapM_ (expFold $ expOpType ty op) args I.ExpAddrOfGlobal{} -> return () I.ExpMaxMin{} -> return () + I.ExpSizeOf{} -> return () -------------------------------------------------------------------------------- -- | For toIx e :: Ix maxSz, assert -- @ --- 0 <= e < maxSz && 1 < maxSz +-- 0 <= e < maxSz && 0 < maxSz -- @ -toIxAssert :: I.Expr -> Integer -> I.Expr -toIxAssert e maxSz = I.ExpOp I.ExpAnd - [ I.ExpOp (I.ExpLt True ixTy) [ lit 0, e ] - , I.ExpOp (I.ExpLt False ixTy) [ e, lit maxSz ] - , I.ExpOp (I.ExpLt False ixTy) [ lit 0, lit maxSz ] +toIxAssert :: I.Expr -> Integer -> I.Stmt +toIxAssert e maxSz = I.CompilerAssert $ I.ExpOp I.ExpAnd + [ I.ExpOp (I.ExpLt True I.ixRep) [ lit 0, e ] + , I.ExpOp (I.ExpLt False I.ixRep) [ e, lit maxSz ] + , I.ExpOp (I.ExpLt False I.ixRep) [ lit 0, lit maxSz ] ] - --------------------------------------------------------------------------------- - -ixTy :: I.Type -ixTy = I.TyInt I.Int32 -------------------------------------------------------------------------------- diff --git a/src/Ivory/Opts/Overflow.hs b/src/Ivory/Opts/Overflow.hs --- a/src/Ivory/Opts/Overflow.hs +++ b/src/Ivory/Opts/Overflow.hs @@ -7,15 +7,16 @@ -------------------------------------------------------------------------------- module Ivory.Opts.Overflow - ( overflowFold + ( overflowFold, addBase, subBase, mulBase, divBase, (<+>), ext ) where import Ivory.Opts.AssertFold -import qualified Ivory.Language.Syntax.AST as I -import qualified Ivory.Language.Syntax.Type as I -import qualified Ivory.Language.IBool as T -import qualified Ivory.Language.Type as T +import qualified Ivory.Language.Array as I +import qualified Ivory.Language.Syntax.AST as I +import qualified Ivory.Language.Syntax.Type as I +import qualified Ivory.Language.Syntax.Names as I +import qualified Ivory.Language.Type as T import Ivory.Language import Prelude hiding (max,min) @@ -25,20 +26,20 @@ -------------------------------------------------------------------------------- overflowFold :: I.Proc -> I.Proc -overflowFold = procFold (expFoldDefault arithAssert) +overflowFold = procFold "ovf" (expFoldDefault arithAssert) -------------------------------------------------------------------------------- type Bounds a = (a,a) -arithAssert :: I.Type -> I.Expr -> [I.Expr] +arithAssert :: I.Type -> I.Expr -> FolderStmt () arithAssert ty e = case e of I.ExpLit i -> litAssert ty i -- Should be impossible to fail, if all -- initializers have been accounted for. I.ExpOp op args -> arithAssert' ty op args - _ -> [] + _ -> return () -litAssert :: I.Type -> I.Literal -> [I.Expr] +litAssert :: I.Type -> I.Literal -> FolderStmt () litAssert ty lit = case lit of I.LitInteger i -> case ty of @@ -50,148 +51,133 @@ I.TyInt I.Int16 -> boundLit (minMax :: Bounds Int16) I.TyInt I.Int32 -> boundLit (minMax :: Bounds Int32) I.TyInt I.Int64 -> boundLit (minMax :: Bounds Int64) - _ -> [] + I.TyIndex n -> boundLit (0 :: Integer, n) + _ -> return () where - boundLit (min,max) = fmap T.unwrapExpr $ - if fromIntegral min <= i && i <= fromIntegral max - then [true] - else [false] - _ -> [] + boundLit (min,max) = insert ca + where + ca = I.CompilerAssert (T.unwrapExpr res) + res = if fromIntegral min <= i && i <= fromIntegral max + then true + else false -arithAssert' :: I.Type -> I.ExpOp -> [I.Expr] -> [I.Expr] -arithAssert' ty op args = fmap T.unwrapExpr $ + minMax :: forall t . (Bounded t) => Bounds t + minMax = (minBound :: t, maxBound :: t) + + _ -> return () + +arithAssert' :: I.Type -> I.ExpOp -> [I.Expr] -> FolderStmt () +arithAssert' ty op args = case op of I.ExpAdd -> case ty of - I.TyWord I.Word8 -> sing $ addExprW (minMax :: Bounds Uint8) - I.TyWord I.Word16 -> sing $ addExprW (minMax :: Bounds Uint16) - I.TyWord I.Word32 -> sing $ addExprW (minMax :: Bounds Uint32) - I.TyWord I.Word64 -> sing $ addExprW (minMax :: Bounds Uint64) - I.TyInt I.Int8 -> sing $ addExprI (minMax :: Bounds Sint8) - I.TyInt I.Int16 -> sing $ addExprI (minMax :: Bounds Sint16) - I.TyInt I.Int32 -> sing $ addExprI (minMax :: Bounds Sint32) - I.TyInt I.Int64 -> sing $ addExprI (minMax :: Bounds Sint64) - _ -> [] + I.TyWord I.Word8 -> mkCall addBase ty args + I.TyWord I.Word16 -> mkCall addBase ty args + I.TyWord I.Word32 -> mkCall addBase ty args + I.TyWord I.Word64 -> mkCall addBase ty args + I.TyInt I.Int8 -> mkCall addBase ty args + I.TyInt I.Int16 -> mkCall addBase ty args + I.TyInt I.Int32 -> mkCall addBase ty args + I.TyInt I.Int64 -> mkCall addBase ty args + I.TyIndex _ -> mkCall addBase ty args + _ -> return () I.ExpSub -> case ty of - I.TyWord I.Word8 -> sing $ subExprW (minMax :: Bounds Uint8) - I.TyWord I.Word16 -> sing $ subExprW (minMax :: Bounds Uint16) - I.TyWord I.Word32 -> sing $ subExprW (minMax :: Bounds Uint32) - I.TyWord I.Word64 -> sing $ subExprW (minMax :: Bounds Uint64) - I.TyInt I.Int8 -> sing $ subExprI (minMax :: Bounds Sint8) - I.TyInt I.Int16 -> sing $ subExprI (minMax :: Bounds Sint16) - I.TyInt I.Int32 -> sing $ subExprI (minMax :: Bounds Sint32) - I.TyInt I.Int64 -> sing $ subExprI (minMax :: Bounds Sint64) - _ -> [] + I.TyWord I.Word8 -> mkCall subBase ty args + I.TyWord I.Word16 -> mkCall subBase ty args + I.TyWord I.Word32 -> mkCall subBase ty args + I.TyWord I.Word64 -> mkCall subBase ty args + I.TyInt I.Int8 -> mkCall subBase ty args + I.TyInt I.Int16 -> mkCall subBase ty args + I.TyInt I.Int32 -> mkCall subBase ty args + I.TyInt I.Int64 -> mkCall subBase ty args + I.TyIndex _ -> mkCall subBase ty args + _ -> return () I.ExpMul -> case ty of - I.TyWord I.Word8 -> sing $ mulExprW (minMax :: Bounds Uint8) - I.TyWord I.Word16 -> sing $ mulExprW (minMax :: Bounds Uint16) - I.TyWord I.Word32 -> sing $ mulExprW (minMax :: Bounds Uint32) - I.TyWord I.Word64 -> sing $ mulExprW (minMax :: Bounds Uint64) - I.TyInt I.Int8 -> sing $ mulExprI (minMax :: Bounds Sint8) - I.TyInt I.Int16 -> sing $ mulExprI (minMax :: Bounds Sint16) - I.TyInt I.Int32 -> sing $ mulExprI (minMax :: Bounds Sint32) - I.TyInt I.Int64 -> sing $ mulExprI (minMax :: Bounds Sint64) - _ -> [] + I.TyWord I.Word8 -> mkCall mulBase ty args + I.TyWord I.Word16 -> mkCall mulBase ty args + I.TyWord I.Word32 -> mkCall mulBase ty args + I.TyWord I.Word64 -> mkCall mulBase ty args + I.TyInt I.Int8 -> mkCall mulBase ty args + I.TyInt I.Int16 -> mkCall mulBase ty args + I.TyInt I.Int32 -> mkCall mulBase ty args + I.TyInt I.Int64 -> mkCall mulBase ty args + I.TyIndex _ -> mkCall mulBase ty args + _ -> return () I.ExpDiv -> case ty of - I.TyWord I.Word8 -> sing $ divExpr (minMax :: Bounds Uint8) - I.TyWord I.Word16 -> sing $ divExpr (minMax :: Bounds Uint16) - I.TyWord I.Word32 -> sing $ divExpr (minMax :: Bounds Uint32) - I.TyWord I.Word64 -> sing $ divExpr (minMax :: Bounds Uint64) - I.TyInt I.Int8 -> sing $ divExpr (minMax :: Bounds Sint8) - I.TyInt I.Int16 -> sing $ divExpr (minMax :: Bounds Sint16) - I.TyInt I.Int32 -> sing $ divExpr (minMax :: Bounds Sint32) - I.TyInt I.Int64 -> sing $ divExpr (minMax :: Bounds Sint64) - _ -> [] + I.TyWord I.Word8 -> mkCall divBase ty args + I.TyWord I.Word16 -> mkCall divBase ty args + I.TyWord I.Word32 -> mkCall divBase ty args + I.TyWord I.Word64 -> mkCall divBase ty args + I.TyInt I.Int8 -> mkCall divBase ty args + I.TyInt I.Int16 -> mkCall divBase ty args + I.TyInt I.Int32 -> mkCall divBase ty args + I.TyInt I.Int64 -> mkCall divBase ty args + I.TyIndex _ -> mkCall divBase ty args + _ -> return () I.ExpMod -> case ty of - I.TyWord I.Word8 -> sing $ divExpr (minMax :: Bounds Uint8) - I.TyWord I.Word16 -> sing $ divExpr (minMax :: Bounds Uint16) - I.TyWord I.Word32 -> sing $ divExpr (minMax :: Bounds Uint32) - I.TyWord I.Word64 -> sing $ divExpr (minMax :: Bounds Uint64) - I.TyInt I.Int8 -> sing $ divExpr (minMax :: Bounds Sint8) - I.TyInt I.Int16 -> sing $ divExpr (minMax :: Bounds Sint16) - I.TyInt I.Int32 -> sing $ divExpr (minMax :: Bounds Sint32) - I.TyInt I.Int64 -> sing $ divExpr (minMax :: Bounds Sint64) - _ -> [] - - _ -> [] - - where - (e0, e1) = (args !! 0, args !! 1) - sing = (: []) - - ---------------------------------------------------------- - - addExprI :: forall t . (Num t, IvoryOrd t, T.IvoryExpr t) - => Bounds t -> T.IBool - addExprI (min,max) = - let w :: I.Expr -> t - w = T.wrapExpr in - (w e0 >=? 0 .&& w e1 >=? 0 .&& max - w e0 >=? w e1) - .|| (w e0 <=? 0 .&& w e1 <=? 0 .&& min - w e0 <=? w e1) - .|| (signum (w e0) /=? signum (w e1)) - - addExprW :: forall t. (Num t, IvoryOrd t, T.IvoryExpr t) - => Bounds t -> T.IBool - addExprW (_,max) = do - let w :: I.Expr -> t - w = T.wrapExpr - max - w e0 >=? w e1 - - ---------------------------------------------------------- - - subExprI :: forall t. (Num t, IvoryOrd t, T.IvoryExpr t) - => Bounds t -> T.IBool - subExprI (min,max) = - let w :: I.Expr -> t - w = T.wrapExpr in - (w e0 >=? 0 .&& w e1 <=? 0 .&& max + w e1 >=? w e0) - .|| (w e0 <=? 0 .&& w e1 >=? 0 .&& min + w e1 <=? w e0) - .|| (signum (w e0) ==? signum (w e1)) + I.TyWord I.Word8 -> mkCall divBase ty args + I.TyWord I.Word16 -> mkCall divBase ty args + I.TyWord I.Word32 -> mkCall divBase ty args + I.TyWord I.Word64 -> mkCall divBase ty args + I.TyInt I.Int8 -> mkCall divBase ty args + I.TyInt I.Int16 -> mkCall divBase ty args + I.TyInt I.Int32 -> mkCall divBase ty args + I.TyInt I.Int64 -> mkCall divBase ty args + I.TyIndex _ -> mkCall divBase ty args + _ -> return () - subExprW :: forall t. (Num t, IvoryOrd t, T.IvoryExpr t) - => Bounds t -> T.IBool - subExprW _ = - let w :: I.Expr -> t - w = T.wrapExpr in - (w e0 :: t) >=? w e1 + _ -> return () - ---------------------------------------------------------- +---------------------------------------------------------- - minNegOne :: forall t. (Num t, IvoryIntegral t, IvoryOrd t, T.IvoryExpr t) - => t -> t -> t -> T.IBool - minNegOne min x y = x /=? min .|| y /=? (-1) +-------------------------------------------------------------------------------- +-- Foreign function calls to Ivory standard lib with overflow functions. - mulExprI :: forall t. (Num t, IvoryIntegral t, IvoryOrd t, T.IvoryExpr t) - => Bounds t -> T.IBool - mulExprI (min,max) = - let w :: I.Expr -> t - w = T.wrapExpr in - (minNegOne min (w e0) (w e1) .|| minNegOne min (w e1) (w e0)) - .&& ( w e0 ==? 0 - .|| w e1 ==? 0 - .|| ( max `iDiv` abs (w e0) >=? abs (w e1) - .&& min `iDiv` abs (w e0) <=? abs (w e1))) +mkCall :: String -> I.Type -> [I.Expr] -> FolderStmt () +mkCall f ty args = do + var <- freshVar + let v = I.VarInternal var + insert $ I.Call I.TyBool (Just v) (I.NameSym $ f <+> ext ty) + (map (I.Typed ty) args) + insert $ I.CompilerAssert (I.ExpVar v) - mulExprW :: forall t. (Num t, IvoryIntegral t, IvoryOrd t, T.IvoryExpr t) - => Bounds t -> T.IBool - mulExprW (_,max) = - let w :: I.Expr -> t - w = T.wrapExpr in - (w e0 ==? 0) .|| (max `iDiv` w e0 >=? w e1) +-------------------------------------------------------------------------------- +-- Construct the names of overflow checking functions defined in ivory.h. - ---------------------------------------------------------- +(<+>) :: String -> String -> String +a <+> b = a ++ "_" ++ b - divExpr :: forall t. (Num t, IvoryIntegral t, IvoryOrd t, T.IvoryExpr t) - => Bounds t -> T.IBool - divExpr (min,_) = - let w :: I.Expr -> t - w = T.wrapExpr in - w e1 /=? (0 :: t) .&& minNegOne min (w e0) (w e1) +mkOvf :: String -> String +mkOvf a = a <+> "ovf" ----------------------------------------------------------- +addBase, subBase, mulBase, divBase :: String +addBase = mkOvf "add" +subBase = mkOvf "sub" +mulBase = mkOvf "mul" +divBase = mkOvf "div" -minMax :: forall t . (Bounded t) => Bounds t -minMax = (minBound :: t, maxBound :: t) +ext :: I.Type -> String +ext ty = case ty of + I.TyChar + -> "char" + I.TyFloat + -> "float" + I.TyDouble + -> "double" + I.TyInt i + -> case i of + I.Int8 -> "i8" + I.Int16 -> "i16" + I.Int32 -> "i32" + I.Int64 -> "i64" + I.TyWord w + -> case w of + I.Word8 -> "u8" + I.Word16 -> "u16" + I.Word32 -> "u32" + I.Word64 -> "u64" + I.TyIndex _ -> ext I.ixRep + _ -> error $ "Unexpected type " ++ show ty ++ " in ext." diff --git a/src/Ivory/Opts/SanityCheck.hs b/src/Ivory/Opts/SanityCheck.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Opts/SanityCheck.hs @@ -0,0 +1,331 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE LambdaCase #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- +-- Sanity check to ensure all functions and memory areas are used +-- with the correct type. +-- +-- Copyright (C) 2014, Galois, Inc. +-- All rights reserved. +-- + +module Ivory.Opts.SanityCheck + ( sanityCheck + , showErrors + , existErrors + , Results() + , render + ) where + +import Prelude () +import Prelude.Compat + +import Control.Monad (unless) +import qualified Data.Map as M +import MonadLib + (WriterM(..),StateM(..),sets_,runId,runStateT,runWriterT + ,Id,StateT,WriterT) +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 qualified Ivory.Language.Syntax.Names as I +import qualified Ivory.Language.Syntax.Type as I + +-------------------------------------------------------------------------------- +-- Errors types + +data Error = UnboundValue String + | 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) + +instance Monoid Results where + mempty = Results [] [] + Results a0 b0 `mappend` Results a1 b1 = Results (a0 ++ a1) (b0 ++ b1) + +-- | Are there any errors from typechecking? +existErrors :: Results -> Bool +existErrors = not . null . errors + +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) + +mkOut :: String -> String -> (a -> Doc) -> [a] -> Doc +mkOut _ _ _ [] = empty +mkOut sym kind sh ls = nm $$ nest 4 (vcat (map go ls)) $$ empty + where + go x = text kind <> text ":" <+> sh x + nm = text "*** Procedure" <+> text sym + +-------------------------------------------------------------------------------- +-- Writer Monad + +-- For imported things, we won't require that the string maps to a valid +-- type. For example, we might import `printf` multiple times at multiple +-- types. We'll only check that the key exists (that the symbol isn't +-- unbound). So imported symbols map to `Nothing`. +data MaybeType = Imported | Defined I.Type + deriving (Show, Eq) + +data St = St { loc :: SrcLoc, env :: M.Map String MaybeType } + +newtype SCResults a = SCResults { unTC :: WriterT Results (StateT St Id) a } + deriving (Functor, Applicative, Monad) + +instance WriterM SCResults Results where + put e = SCResults (put e) + +instance StateM SCResults St where + get = SCResults get + set = SCResults . set + +getStLoc :: SCResults SrcLoc +getStLoc = fmap loc get + +setStLoc :: SrcLoc -> SCResults () +setStLoc l = sets_ (\s -> s { loc = l }) + +localEnv :: SCResults a -> SCResults a +localEnv doThis = do + env <- fmap env get + res <- doThis + sets_ (\s -> s { env = env }) + return res + +checkScope :: String -> SCResults () +checkScope name = + lookupType name >>= \case + Nothing -> putError (UnboundValue name) + Just _ -> return () + +lookupType :: String -> SCResults (Maybe MaybeType) +lookupType name = do + env <- fmap env get + return $ M.lookup name env + +hasType :: String -> I.Type -> SCResults () +hasType name ty = sets_ (\s -> s { env = M.insert name (Defined ty) (env s) }) + +putError :: Error -> SCResults () +putError err = do + loc <- getStLoc + put (Results [err `at` loc] []) + +runSCResults :: SCResults a -> (a, Results) +runSCResults tc = fst $ runId $ runStateT (St NoLoc M.empty) $ runWriterT (unTC tc) + +-------------------------------------------------------------------------------- + +varString :: I.Var -> String +varString v = case v of + I.VarName s -> s + I.VarInternal s -> s + I.VarLitName s -> s + +nameString :: I.Name -> String +nameString n = case n of + I.NameSym s -> s + I.NameVar v -> varString v + +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 + where + getVisible v = I.public v ++ I.private v + + topLevel :: M.Map String MaybeType + topLevel = M.fromList + $ concat [ procs m + ++ imports m + ++ externs m + ++ areas m + ++ importAreas m + | m <- this:deps + ] + + 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 ] + +-- | 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 + sets_ (\s -> s { env = env }) + mapM_ (\ (I.Typed t v) -> varString v `hasType` t) procArgs + check procBody + +check :: [I.Stmt] -> SCResults () +check = mapM_ go + where + go stmt = case stmt of + I.Deref t v e + -> checkExpr e >> varString v `hasType` t + I.Store _ e1 e2 + -> checkExpr e1 >> checkExpr e2 + I.Assign t v e + -> checkExpr e >> varString v `hasType` t + I.Call t mv (nameString -> f) args + -> do mapM_ (\ (I.Typed _ e) -> checkExpr e) args + mt <- lookupType f + case mt of + Nothing + -> putError (UnboundValue f) + Just mty + -> case mty of + Imported -> return () + Defined ty -> checkCall f ty args t + case mv of + Nothing -> return () + Just v -> varString v `hasType` t + I.Local t v _ + -> varString v `hasType` t + I.RefCopy _ e1 e2 + -> checkExpr e1 >> checkExpr e2 + I.AllocRef t v _ + -> varString v `hasType` t + I.Loop _ v _ _ stmts + -> localEnv $ do varString v `hasType` I.ixRep + check stmts + I.Forever stmts + -> localEnv $ check stmts + I.IfTE b t f + -> do checkExpr b + localEnv $ check t + localEnv $ check f + I.Comment (I.SourcePos loc) + -> setStLoc loc + _ -> return () + +checkExpr :: I.Expr -> SCResults () +checkExpr expr = case expr of + I.ExpSym v -> checkScope v + I.ExpExtern v -> checkScope (I.externSym v) + I.ExpAddrOfGlobal v -> checkScope v + I.ExpVar v -> checkScope (varString v) + I.ExpLabel _ e _ -> checkExpr e + I.ExpIndex _ e1 _ e2 -> checkExpr e1 >> checkExpr e2 + I.ExpToIx e _ -> checkExpr e + I.ExpSafeCast _ e -> checkExpr e + I.ExpOp _ exprs -> mapM_ checkExpr exprs + _ -> return () + +checkCall :: String -> I.Type -> [I.Typed I.Expr] -> I.Type -> SCResults () +checkCall f ty args retTy = case ty of + I.TyProc r as + -> unless (all eq $ zip (r:as) (retTy : argTys)) + (putError $ TypeError f (I.TyProc r as) (I.TyProc retTy argTys)) + _ -> putError $ TypeError f ty (I.TyProc retTy argTys) + where + argTys = [t | I.Typed t _ <- args] + eq (x,y) = x == y + +instance Pretty I.Type where + pretty ty = case ty of + I.TyVoid + -> text "()" + I.TyInt I.Int8 + -> text "Sint8" + I.TyInt I.Int16 + -> text "Sint16" + I.TyInt I.Int32 + -> text "Sint32" + I.TyInt I.Int64 + -> text "Sint64" + I.TyWord I.Word8 + -> text "Uint8" + I.TyWord I.Word16 + -> text "Uint16" + I.TyWord I.Word32 + -> text "Uint32" + I.TyWord I.Word64 + -> text "Uint64" + I.TyIndex i + -> text "Ix" <+> text (show i) + I.TyBool + -> text "Bool" + I.TyChar + -> text "Char" + I.TyFloat + -> text "Float" + I.TyDouble + -> text "Double" + I.TyProc ret args + -> pretty args <+> text ":->" <+> pretty ret + I.TyRef ref + -> text "Ref" <+> pretty ref + I.TyConstRef ref + -> text "ConstRef" <+> pretty ref + I.TyPtr ptr + -> text "Ptr" <+> pretty ptr + I.TyArr n t + -> text "Array" <+> pretty n <+> pretty t + I.TyStruct s + -> text "Struct" <+> pretty s + I.TyCArray t + -> 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 new file mode 100644 --- /dev/null +++ b/src/Ivory/Opts/TypeCheck.hs @@ -0,0 +1,198 @@ +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE CPP #-} + +-- +-- 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. +-- +-- Copyright (C) 2014, Galois, Inc. +-- All rights reserved. +-- + +module Ivory.Opts.TypeCheck + ( typeCheck + , showErrors + , showWarnings + , existErrors + , Results() + ) where + +import Prelude () +import Prelude.Compat + +import Control.Monad (when,void) +import MonadLib + (WriterM(..),StateM(..),runId,runStateT,runWriterT,Id,StateT,WriterT) +import Data.List (nub) + +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 + +-------------------------------------------------------------------------------- +-- Errors types + +data RetError = RetError String [Error] + deriving (Show, Read, Eq) + +data Warning = IfTEWarn + | LoopWarn + | VoidEmptyBody + deriving (Show, Read, Eq) + +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) + +-- | Are there any errors from typechecking? +existErrors :: Results -> Bool +existErrors = not . null . errs + +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." + +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." + +showWithLoc :: (a -> String) -> Located a -> String +showWithLoc sh (Located loc a) = prettyPrint (pretty loc) ++ ": " ++ sh a + +-- | 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) + +-- | 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) + +mkOut :: String -> String -> (a -> String) -> [a] -> [String] +mkOut _ _ _ [] = [] +mkOut sym kind sh ls = nm : map go ls + where + go x = " " ++ kind ++ ": " ++ sh x + nm = "*** Procedure " ++ sym + +-------------------------------------------------------------------------------- +-- Writer Monad + +newtype TCResults a = TCResults { unTC :: WriterT Results (StateT SrcLoc Id) a } + deriving (Functor, Applicative, Monad) + +instance WriterM TCResults Results where + put e = TCResults (put e) + +instance StateM TCResults SrcLoc where + get = TCResults get + set = TCResults . set + +putError :: Error -> TCResults () +putError err = do + loc <- get + put (Results [err `at` loc] []) + +putWarn :: Warning -> TCResults () +putWarn warn = do + loc <- get + put (Results [] [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) + +-- Sub-block of the prcedure +type SubBlk = Bool +-- Seen a return statement? +type Ret = Bool + +tyChk :: I.Type -> [I.Stmt] -> TCResults () +tyChk I.TyVoid [] = putWarn VoidEmptyBody +tyChk _ [] = putError EmptyBody +tyChk ty stmts = void (tyChk' (False, False) stmts) + where + tyChk' :: (SubBlk, Ret) -> [I.Stmt] -> TCResults Ret + -- Ret and no other statemnts + tyChk' (_, True) ss | all isComment ss + = return True + -- Ret and other statements + tyChk' (sb, True) ss + = putError DeadCode >> tyChk' (sb, False) ss + -- Sub block and no ret seen + tyChk' (True, False) [] + = return False + -- No ret seen, main block: only a problem if non-void type. + tyChk' (False, False) [] + = do when (ty /= I.TyVoid) (putError NoRet) + return False + -- The two return cases + tyChk' (sb, False) (I.ReturnVoid : ss) + = tyChk' (sb, True) ss + tyChk' (sb, False) (I.Return _ : ss) + = tyChk' (sb, True) ss + -- Control flow + tyChk' (sb, False) (I.IfTE _ ss0 ss1 : ss) + = do b0 <- tyChk' (True, False) ss0 + b1 <- tyChk' (True, False) ss1 + if b0 && b1 then tyChk' (sb, True) ss + else do when (b0 `xor` b1) (putWarn IfTEWarn) + tyChk' (sb, False) ss + tyChk' (sb, False) (I.Loop _ _ _ _ ss0 : ss) + = 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 ss + tyChk' b (I.Comment (I.SourcePos src):ss) + = do set src + tyChk' b ss + tyChk' b (_:ss) + = tyChk' b ss + + 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 () + +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 @@ -20,8 +20,6 @@ I.ExpLt _ t1 -> t1 I.ExpIsNan t1 -> t1 I.ExpIsInf t1 -> t1 - I.ExpToFloat t1 -> t1 - I.ExpFromFloat t1 -> t1 _ -> t0 --------------------------------------------------------------------------------