diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,28 @@ +Copyright (c)2013, Galois, Inc + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Galois, Inc nor the names of its contributors + may be used to endorse or promote products derived from this software + without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/ivory-opts.cabal b/ivory-opts.cabal new file mode 100644 --- /dev/null +++ b/ivory-opts.cabal @@ -0,0 +1,41 @@ +-- Initial ivory.cabal generated by cabal init. For further documentation, +-- see http://haskell.org/cabal/users-guide/ + +name: ivory-opts +version: 0.1.0.0 +author: Galois, Inc. +maintainer: leepike@galois.com +category: Language +build-type: Simple +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 +license: BSD3 +license-file: LICENSE +source-repository this + type: git + location: https://github.com/GaloisInc/ivory-opts + tag: hackage-opts-0100a + +library + exposed-modules: Ivory.Opts.AssertFold, + Ivory.Opts.CFG, + Ivory.Opts.ConstFold, + Ivory.Opts.DivZero, + Ivory.Opts.Index, + Ivory.Opts.FP, + Ivory.Opts.Overflow + + other-modules: Ivory.Opts.Utils + + build-depends: base >= 4.6 && < 4.7, + ivory, + monadLib >= 3.7, + filepath, + dlist >= 0.5, + fgl >= 5.4.2.4, + containers + hs-source-dirs: src + default-language: Haskell2010 + ghc-options: -Wall diff --git a/src/Ivory/Opts/AssertFold.hs b/src/Ivory/Opts/AssertFold.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Opts/AssertFold.hs @@ -0,0 +1,248 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +-- | Fold over expressions that collect up assertions about the expressions. + +module Ivory.Opts.AssertFold where + +import MonadLib hiding (collect) +import Data.Monoid +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 + +-------------------------------------------------------------------------------- +-- Monad and types. + +-- | A monad that holds our transformed program. +newtype FolderM a b = FolderM + { unFolderM :: StateT (D.DList a) Id b + } deriving (Functor, Monad) + +instance StateM (FolderM a) (D.DList a) where + get = FolderM get + set = FolderM . set + +insert :: a -> FolderM a () +insert a = do + st <- get + set (D.snoc st a) + +inserts :: D.DList a -> FolderM a () +inserts ds = do + st <- get + set (st <++> ds) + +insertList :: [a] -> FolderM a () +insertList = inserts . D.fromList + +resetState :: FolderM a () +resetState = set D.empty + +runFolderM :: FolderM a b -> (b, D.DList a) +runFolderM m = runId $ runStateT mempty (unFolderM m) + +-------------------------------------------------------------------------------- +-- 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 + +-------------------------------------------------------------------------------- + +runEmptyState :: ExpFold -> [I.Stmt] -> [I.Stmt] +runEmptyState ef stmts = + let m = mapM_ (stmtFold ef) stmts in + D.toList $ snd (runFolderM m) + +procFold :: ExpFold -> I.Proc -> I.Proc +procFold ef p = + let body' = runEmptyState 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 + insert (I.IfTE e b0' b1') + I.Assert e -> do insertAsserts (ef I.TyBool e) + insert stmt + I.CompilerAssert e -> do insertAsserts (ef I.TyBool e) + insert stmt + I.Assume e -> do insertAsserts (ef I.TyBool e) + insert stmt + I.Return (I.Typed ty e) -> do insertAsserts (ef ty e) + insert stmt + I.ReturnVoid -> insert stmt + I.Deref ty _v e -> do insertAsserts (ef ty e) + insert stmt + I.Store ty ptrExp e -> do insertAsserts (ef (I.TyRef ty) ptrExp) + insertAsserts (ef ty e) + insert stmt + I.Assign ty _v e -> do insertAsserts (ef ty e) + insert stmt + I.Call _ty _mv _nm args -> do insertAsserts (concatMap 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.Break -> insert stmt + I.Local _ty _v init' -> do insertAsserts (efInit init') + insert stmt + I.RefCopy ty e0 e1 -> do insertAsserts (ef ty e0) + insertAsserts (ef ty e1) + insert stmt + I.AllocRef{} -> insert stmt + I.Forever blk -> do let blk' = runEmptyState ef blk + insert (I.Forever blk') + 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 + efInit init' = case init' of + I.InitZero -> [] + 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 + +-------------------------------------------------------------------------------- + +expFoldDefault' :: ExpFold -> I.Type -> I.Expr -> FolderExpr () +expFoldDefault' asserter ty e = case e of + I.ExpSym{} -> go e + I.ExpVar{} -> go e + I.ExpLit{} -> go e + I.ExpLabel ty' e0 _str -> do go e + expFold ty' e0 + I.ExpIndex tIdx eIdx tArr eArr -> do go e + expFold tIdx eIdx + expFold tArr eArr + I.ExpToIx e0 _i -> do go e + expFold ty e0 + I.ExpSafeCast ty' e0 -> do go e + expFold ty' e0 + I.ExpOp op args -> do go e + expFoldOps asserter ty (op, args) + I.ExpAddrOfGlobal{} -> go e + I.ExpMaxMin{} -> go e + where + go = insertList . asserter ty + expFold = expFoldDefault' asserter + +-------------------------------------------------------------------------------- + +-- We need a special case for expressions that may affect control flow: +-- +-- ExpCond +-- ExpOr +-- ExpAnd +-- +-- (The later two can introduce shortcutting.) ExpCond is in the spirit of an +-- expression by implementing control-flow. We need a pre-condition here, since +-- we might have expressions like +-- +-- x /= 0 ? 3.0/x : 0.0 +-- +expFoldOps :: ExpFold -> I.Type -> (I.ExpOp, [I.Expr]) -> FolderExpr () +expFoldOps asserter ty (op, args) = case (op, args) of + + (I.ExpCond, [cond, texp, fexp]) + -> do + fold ty cond + preSt <- get + + tSt <- runBranch cond texp + fSt <- runBranch (neg cond) fexp + resetState + + inserts preSt + inserts tSt + inserts fSt + + (I.ExpAnd, [exp0, exp1]) + -> runBool exp0 exp1 id + + (I.ExpOr, [exp0, exp1]) + -> runBool exp0 exp1 neg + + _ -> mapM_ (fold $ expOpType ty op) args + + where + fold = expFoldDefault' asserter + + runBranch cond e = do + resetState + fold ty e + withEnv cond + get + + runBool exp0 exp1 f = do + preSt <- get + + st0 <- runCase exp0 + st1 <- runBranch (f exp0) exp1 + resetState + + inserts preSt + inserts st0 + inserts st1 + + where + runCase e = do + resetState + fold ty e + get + +-------------------------------------------------------------------------------- +-- Helpers + +(<++>) :: 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] + +-------------------------------------------------------------------------------- diff --git a/src/Ivory/Opts/CFG.hs b/src/Ivory/Opts/CFG.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Opts/CFG.hs @@ -0,0 +1,494 @@ +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleInstances #-} + +-- {-# LANGUAGE DataKinds #-} +-- {-# LANGUAGE TypeOperators #-} + +module Ivory.Opts.CFG + ( callGraphDot + -- ** Generate a dot file of the control flow for a program. + , SizeMap(..) + -- ** Implementation-defined size map for stack elements. + , defaultSizeMap + , hasLoop + -- ** Does the control-flow graph contain a loop? + , WithTop + , maxStack + -- ** What is the maximum stack size of the program? + ) + where + +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 System.FilePath +import Data.Maybe +import Data.List hiding (lookup) +import Control.Applicative +import qualified Data.IntMap as M +import MonadLib (StateT, get, set, Id, StateM, runM) +import MonadLib.Derive (derive_get, derive_set, Iso(..)) + +-- import Ivory.Language hiding (Top) + +-------------------------------------------------------------------------------- +-- Types + +-- | Add Top to a type. +data WithTop a = Top | Val a + deriving (Eq, Functor) + +instance Show a => Show (WithTop a) where + show Top = "Top" + show (Val a) = show a + +instance Ord a => Ord (WithTop a) where + compare Top (Val _) = GT + compare (Val _) Top = LT + compare Top Top = EQ + compare (Val a) (Val b) = compare a b + +instance Applicative WithTop where + pure a = Val a + Val _ <*> Top = Top + Val f <*> (Val a) = Val (f a) + _ <*> _ = Top + +type Size = Integer +type CallNm = String + +-- | We track those objects for which the size might be +-- implementation-dependent. +data StackType = TyStruct String -- ^ Name of struct + | TyArr StackType Size -- ^ Array and size + | Ptr -- ^ Pointer or ref type + | TyVoid + | TyInt IntSize + | TyWord WordSize + | TyBool + | TyChar + | TyFloat + | TyDouble + deriving (Show, Eq) + +data IntSize = Int8 + | Int16 + | Int32 + | Int64 + deriving (Show,Eq) + +data WordSize = Word8 + | Word16 + | Word32 + | Word64 + deriving (Show,Eq) + +data (Show a, Eq a) => Block a + = Stmt a + | Branch [Block a] [Block a] + | Loop (Maybe Integer) [Block a] -- If we know how many loops we make, we + -- store it. Otherwise, `Nothing`. + deriving (Show, Eq) + +type Control = Block CallNm -- ^ Name of function being called +type Alloc = Block StackType -- ^ Memory being allocated + +-- | Describes the CFG and memory usage for a single procedure. +data ProcInfo = ProcInfo + { procSym :: CallNm + , params :: [StackType] + -- ^ Parameters pushed onto the stack. + , alloc :: [Alloc] + -- ^ Allocated elements. + , calls :: [Control] + } deriving (Show, Eq) + +data ModuleInfo = ModuleInfo + { modName :: String + , procs :: [ProcInfo] + } deriving (Show, Eq) + +-------------------------------------------------------------------------------- +-- Procedure Analysis + +toStackTyped :: I.Typed a -> StackType +toStackTyped ty = toStackType (I.tType ty) + +toStackType :: I.Type -> StackType +toStackType ty = + case ty of + I.TyStruct nm -> TyStruct nm + I.TyArr i t -> TyArr (toStackType t) (fromIntegral i) + I.TyRef{} -> Ptr + I.TyConstRef{} -> Ptr + I.TyPtr{} -> Ptr + I.TyVoid -> TyVoid + I.TyInt i -> TyInt (toIntType i) + I.TyWord w -> TyWord (toWordType w) + I.TyBool -> TyBool + I.TyChar -> TyChar + I.TyFloat -> TyFloat + I.TyDouble -> TyDouble + t -> error $ "Unhandled stack type: " ++ show t + +toIntType :: I.IntSize -> IntSize +toIntType i = + case i of + I.Int8 -> Int8 + I.Int16 -> Int16 + I.Int32 -> Int32 + I.Int64 -> Int64 + +toWordType :: I.WordSize -> WordSize +toWordType i = + case i of + I.Word8 -> Word8 + I.Word16 -> Word16 + I.Word32 -> Word32 + I.Word64 -> Word64 + +cfgProc :: I.Proc -> ProcInfo +cfgProc proc = ProcInfo + { procSym = I.procSym proc + , params = map toStackTyped (I.procArgs proc) + , alloc = concatMap toAlloc (I.procBody proc) + , calls = concatMap toCall (I.procBody proc) + } + +toAlloc :: I.Stmt -> [Alloc] +toAlloc stmt = + case stmt of + I.Assign ty _ _ -> [Stmt $ toStackType ty] + I.AllocRef ty _ _ -> [Stmt $ toStackType ty] + I.Deref ty _ _ -> [Stmt $ toStackType ty] + -- Descend into blocks + 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.Forever blk -> + [Loop Nothing (concatMap toAlloc blk)] + _ -> [] + +toCall :: I.Stmt -> [Control] +toCall stmt = + case stmt of + I.IfTE _ blk0 blk1 -> [ Branch (concatMap toCall blk0) + (concatMap toCall blk1) ] + 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)] + _ -> [] + +getIdx :: I.Expr -> Maybe Integer +getIdx e = case e of + I.ExpLit (I.LitInteger i) -> Just i + _ -> Nothing + +-------------------------------------------------------------------------------- +-- Call-graph construction from a module. + +-- type Node = G.LNode ProcInfo + +-- | A call graph is a graph in which nodes are labeled by their procedure info +-- and edges are unlabeled. +type CFG = G.Gr ProcInfo () + +flattenControl :: Control -> [CallNm] +flattenControl ctrl = + case ctrl of + Stmt str -> [str] + Branch ctrl0 ctrl1 -> + concatMap flattenControl ctrl0 ++ concatMap flattenControl ctrl1 + Loop _ ctrl0 -> concatMap flattenControl ctrl0 + +cfgModule :: I.Module -> ModuleInfo +cfgModule m = ModuleInfo + { modName = I.modName m + , procs = map cfgProc ps + } + where ps = I.public (I.modProcs m) ++ I.private (I.modProcs m) + +-- | Construct a control-flow graph from an Ivory module. +cfg :: I.Module -> CFG +cfg m = G.insEdges (concatMap go nodes) $ G.insNodes nodes G.empty + where + nodes :: [G.LNode ProcInfo] + nodes = zip [0,1..] (procs $ cfgModule m) + + go :: (Int, ProcInfo) -> [G.LEdge ()] + go (i,p) = + let outCalls = concatMap flattenControl (calls p) in + let outIdxs = catMaybes (map (lookup nodes) outCalls) in + zip3 (repeat i) outIdxs (repeat ()) -- outboud edges + + lookup ls sym | [] <- ls = Nothing + | ((i,p):_) <- ls + , procSym p == sym = Just i + | (_:ls') <- ls = lookup ls' sym + | otherwise = error "Unreachable in cfg" -- To make GHC happy. + +-- | Just label the nodes with the function names. +procSymGraph :: CFG -> G.Gr CallNm () +procSymGraph = G.nmap procSym + +-- | Does the program have a loop in it? +hasLoop :: CFG -> Bool +hasLoop = G.hasLoop + +-------------------------------------------------------------------------------- +-- Stack usage analysis. + +data SizeMap = SizeMap + { stackElemMap :: StackType -> Size -- ^ Mapping from `StackType` to their + -- implementation-dependent size. + , retSize :: Size -- ^ Size of a return address. + } + + +-- | Maps everything to being size 1. Useful for testing. +defaultSizeMap :: SizeMap +defaultSizeMap = SizeMap + { stackElemMap = const 1 + , retSize = 1 + } + +-- A mapping from `Node` (Ints) to the maximum stack usage for that function. +type MaxMap = M.IntMap Size + +newtype MaxState a = MaxState + { unSt :: StateT MaxMap Id a + } deriving (Functor, Monad) + +instance StateM MaxState MaxMap where + get = derive_get (Iso MaxState unSt) + set = derive_set (Iso MaxState unSt) + +emptyMaxSt :: MaxMap +emptyMaxSt = M.empty + +getMaxMap :: MaxState MaxMap +getMaxMap = return =<< get + +-- | Takes a procedure name, a control-flow graph, and a `SizeMap` and produces +-- the maximum stack usage starting at the procedure give. Returns `Top` if +-- there is an unanalyzable loop in the program (ie., non-constant loop) and +-- @Val max@ otherwise. +maxStack :: CallNm -> CFG -> SizeMap -> WithTop Size +maxStack proc cf szmap = go proc + where + go p = fst $ runM (unSt (maxStack' cf szmap [] (findNode cf p))) emptyMaxSt + +-- Get the node from it's name. +findNode :: CFG -> CallNm -> G.Node +findNode cf proc = fst $ + fromMaybe (error $ "Proc " ++ proc ++ " is not in the graph!") + (find ((== proc) . procSym . snd) (G.labNodes cf)) + +maxStack' :: CFG -> SizeMap -> [G.Node] -> G.Node -> MaxState (WithTop Size) +maxStack' cf szmap visited curr + | curr `elem` visited = return Top -- A loop is detected. + | otherwise = maxStackNode + where + -- Process the max stack for a single node. + maxStackNode :: MaxState (WithTop Size) + maxStackNode = do + blkMax <- goBlks cf szmap visited curr alloc' calls' + let sz = (topAllocSz + paramsSz + retSize szmap +) <$> blkMax + return sz + + where + cxt = G.context cf curr + procInfo = G.lab' cxt + + alloc' = alloc procInfo + calls' = calls procInfo + + -- Top-level allocation + topAllocSz :: Size + topAllocSz = getSize szmap (getBlock alloc') + + paramsSz :: Size + paramsSz = getSize szmap (params procInfo) + +goBlks :: CFG -> SizeMap -> [G.Node] -> G.Node + -> [Alloc] -> [Control] -> MaxState (WithTop Size) +goBlks cf szmap visited curr acs cns = + case (acs, cns) of + -- Done with all blocks/statements in this function. + ([] ,[]) -> return (Val 0) + (Branch a0 a1:acs', Branch c0 c1:cns') -> do + sz0 <- goBlks' a0 c0 + sz1 <- goBlks' a1 c1 + sz2 <- goBlks' acs' cns' + return (liftA2 max sz0 sz1 <+> sz2) + -- There's no new loop allocation, just assignments. So we assume that on + -- each iteration, the stack usage doesn't change. + (Loop _ a:acs', Loop _ c:cns') -> do + sz0 <- goBlks' a c + sz1 <- goBlks' acs' cns' + return (sz0 <+> sz1) + + -- case idx of + -- -- Unknown loop bound. + -- Nothing -> if sz0 == Val 0 then return sz1 + + -- else return Top -- Did some allocation in the loop, so + -- -- can't compute. + -- Just _ -> + -- There is either a straight-line call or assignment. + _ -> do + sz0 <- goBlk cf szmap visited curr (getBlock acs) (getBlock cns) + sz1 <- goBlks' (nxtBlock acs) (nxtBlock cns) + return (sz0 <+> sz1) + where goBlks' = goBlks cf szmap visited curr + +goBlk :: CFG -> SizeMap -> [G.Node] -> G.Node -> [StackType] + -> [CallNm] -> MaxState (WithTop Size) +goBlk cf szmap visited curr acs cns = do + maxMp <- getMaxMap + let localAlloc = getSize szmap acs + let callNodes = map (findNode cf) cns + let allCalls = zip callNodes (map (flip M.lookup $ maxMp) callNodes) + newMaxs <- mapM cachedCalls allCalls + return $ Val localAlloc <+> if null newMaxs then Val 0 + -- Depends on Top being >= all vals. + else maximum newMaxs + + where + cachedCalls :: (G.Node, Maybe Size) -> MaxState (WithTop Size) + cachedCalls (n, msz) | Just sz <- msz = return (Val sz) + | otherwise = + maxStack' cf szmap (curr:visited) n + +(<+>) :: Num a => WithTop a -> WithTop a -> WithTop a +(<+>) = liftA2 (+) + +-- Get the cumulative sizes of allocated things. +getSize :: SizeMap -> [StackType] -> Size +getSize szmap = sum . map (stackElemMap szmap) + +-- Get the prefix of a list of @[Block a] in the current block. +getBlock :: (Show a, Eq a) => [Block a] -> [a] +getBlock bls | (Stmt b:bs) <- bls = b : getBlock bs + | otherwise = [] + +nxtBlock :: (Show a, Eq a) => [Block a] -> [Block a] +nxtBlock bls | (Stmt _:bs) <- bls = nxtBlock bs + | otherwise = bls + +-- | Call-graph output. Takes a start function foo, a filepath, and emits the +-- graph named "foo.dot" in the filepath. +callGraphDot :: CallNm -> FilePath -> [I.Module] -> IO CFG +callGraphDot proc path mods = + writeFile (path proc `addExtension` "dot") grOut >> return graph + where + m = mconcat mods + grOut = graphviz filterG (I.modName m) + filterG :: G.Gr CallNm () + filterG = let closure = G.reachable (findNode graph proc) graph in + G.delNodes (G.nodes graph \\ closure) (procSymGraph graph) + graph = cfg m + +-------------------------------------------------------------------------------- +-- Adapted from fgl (BSD3) to remove sizing info. +graphviz :: (G.Graph g, Show a, Show b) + => g a b -- ^ The graph to format + -> String -- ^ The title of the graph + -> String +graphviz g t = + let n = G.labNodes g + 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") + +sl :: (Show a) => a -> String +sl a = let l = sq (show a) + in if (l /= "()") then (" [label = \""++l++"\"]") else "" + +sq :: String -> String +sq s@[_] = s +sq ('"':s) | last s == '"' = init s + | otherwise = s +sq ('\'':s) | last s == '\'' = init s + | otherwise = s +sq s = s + +-------------------------------------------------------------------------------- +-- Testing + +{- + +fibCFG :: CFG +fibCFG = cfg fibMod + +outGraph = writeFile "fib.dot" gr + where + gr = G.graphviz (procSymGraph fibCFG) "fib" (4,4) (4,4) G.Portrait +---------------------- + +fibMod :: Module +fibMod = package "fib" $ do + incl fib + incl fib_aux + +fib :: Def ('[Uint32] :-> Uint64) +fib = proc "fib" (\n -> body (ret =<< call fib_aux 0 1 n)) + +fib_aux :: Def ('[Uint32,Uint32,Uint32] :-> Uint64) +fib_aux = proc "fib_aux" $ \ a b n -> body $ do + ifte_ (n ==? 0) + (ret (safeCast a)) + (ret . safeCast =<< call fib_aux b (a + b) (n - 1)) + +fibSz = SizeMap + { stackElemMap = \_ -> 1 + , retSize = 1 } + +------------------------------------- + +x :: G.Gr Int () +x = G.insEdges edges gr + where + edges = [(0,1,()), (0,2,()), (2,1,()), (2,3,())] + gr = G.insNodes nodes G.empty + nodes = zip [0,1 ..] [2,3,4,1] + +y :: G.Gr Int () +y = G.insEdges edges gr + where + edges = [(0,1,()), (0,2,()), (2,1,()), (1,3,())] + gr = G.insNodes nodes G.empty + nodes = zip [0,1 ..] [1,4,5,8] + +maxf :: G.Gr Int () -> G.Node -> Maybe Int +maxf g n = maxf' [] n + where + maxf' :: [G.Node] -> G.Node -> Maybe Int + maxf' visited curr + | curr `elem` visited = Nothing -- We made a loop on this path! That's Top. + | otherwise = liftA2 (+) (Just $ G.lab' cxt) go + where + cxt = G.context g curr + res = map (maxf' (G.node' cxt : visited)) (G.suc' cxt) + go | null (G.suc' cxt) = Just 0 -- No more successors to try + | Nothing `elem` res = Nothing + | otherwise = Just $ maximum (catMaybes res) + +-} diff --git a/src/Ivory/Opts/ConstFold.hs b/src/Ivory/Opts/ConstFold.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Opts/ConstFold.hs @@ -0,0 +1,578 @@ +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE Rank2Types #-} + +module Ivory.Opts.ConstFold + ( constFold + ) 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.Maybe +import Data.List +import Data.Word +import Data.Int +import qualified Data.DList as D + +-------------------------------------------------------------------------------- +-- Constant folding +-------------------------------------------------------------------------------- + +constFold :: I.Proc -> I.Proc +constFold = procFold cf + +-- | 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 + + I.ExpAddrOfGlobal{} -> e + I.ExpMaxMin{} -> e + +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) + in proc { I.procBody = body' } + +stmtFold :: String -> ExprOpt -> D.DList I.Stmt -> I.Stmt -> D.DList I.Stmt +stmtFold cxt opt blk 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.ExpLit (I.LitBool b) -> + if b then blk + 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 + I.ExpLit (I.LitBool b) -> + if b then blk + else error $ "Constant folding evaluated a False assume()" + ++ " in evaluating expression " ++ show e + ++ " of function " ++ cxt + _ -> snoc (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.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`) + +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 } + +arg0 :: [a] -> a +arg0 = flip (!!) 0 + +arg1 :: [a] -> a +arg1 = flip (!!) 1 + +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 + + I.ExpMul -> goNum + I.ExpAdd -> goNum + I.ExpSub -> goNum + I.ExpNegate -> goNum + I.ExpAbs -> goNum + I.ExpSignum -> goNum + + I.ExpDiv -> goI2 + I.ExpMod -> goI2 + I.ExpRecip -> goF + + I.ExpIsNan t -> goFB t + I.ExpIsInf t -> goFB t + + 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.ExpBitAnd -> toExpr (cfBitAnd ty $ goArgs ty) + I.ExpBitOr -> toExpr (cfBitOr ty $ goArgs ty) + + -- 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 + + 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) + + +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." + +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." + +-- Min values for word types. +zeros :: I.Type -> CfVal -> Bool +zeros I.TyWord{} (CfInteger i) = i == 0 +zeros _ _ = False + +-- 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 + +-- | 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 + +-- Constant-folded Values ------------------------------------------------------ + +-- | 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 + ] + +-- | 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 + +-- | Check if we're comparing the max or min bound for >= and optimize. +gteCheck :: I.Type -> [CfVal] -> Maybe Bool +gteCheck t [l,r] + -- forall a. max >= a + | CfInteger x <- l + , Just s <- toMaxSize t + , x == s = Just True + -- forall a. a >= min + | CfInteger y <- r + , Just s <- toMinSize t + , 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. +gtCheck :: I.Type -> [CfVal] -> Maybe Bool +gtCheck t [l,r] + -- forall a. not (min > a) + | CfInteger x <- l + , Just s <- toMinSize t + , x == s = Just False + -- forall a. not (a > max) + | CfInteger y <- r + , Just s <- toMaxSize t + , y == s = Just False + | otherwise = Nothing +gtCheck _ _ = err "wrong number of args to gtCheck." + +fromOrdChecks :: I.Expr -> Maybe Bool -> I.Expr +fromOrdChecks expr = maybe expr (toExpr . CfBool) + +-- | Apply a binary operation that requires an ord instance. +cfOrd2 :: I.ExpOp + -> [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) + _ -> CfExpr (I.ExpOp op [toExpr l, toExpr r]) + where + op' :: Ord a => a -> a -> Bool + op' = case op of + I.ExpEq _ -> (==) + I.ExpNeq _ -> (/=) + I.ExpGt orEq _ + | orEq -> (>=) + | otherwise -> (>) + I.ExpLt orEq _ + | orEq -> (<=) + | otherwise -> (<) + _ -> 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/DivZero.hs b/src/Ivory/Opts/DivZero.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Opts/DivZero.hs @@ -0,0 +1,45 @@ +-------------------------------------------------------------------------------- +-- | Division by zero checks. +-------------------------------------------------------------------------------- + +module Ivory.Opts.DivZero + ( divZeroFold + ) where + +import Ivory.Opts.AssertFold + +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) + +-------------------------------------------------------------------------------- + +-- 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 ty e0 = case e0 of + I.ExpOp op args -> + case (op,args) of + (I.ExpDiv,[_,r]) -> ma r + (I.ExpMod,[_,r]) -> ma r + (I.ExpRecip,[e]) -> ma e + (I.ExpFLog,[e]) -> ma e + (I.ExpFLogBase,[_,r]) -> ma r + _ -> [] + _ -> [] + + where + ma x = [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.TyFloat -> I.ExpLit (I.LitFloat 0) + I.TyDouble -> I.ExpLit (I.LitDouble 0) + _ -> error $ + "ivory opts: unrecognized expression in Div by zero checking." + +-------------------------------------------------------------------------------- diff --git a/src/Ivory/Opts/FP.hs b/src/Ivory/Opts/FP.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Opts/FP.hs @@ -0,0 +1,37 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} + +-------------------------------------------------------------------------------- +-- | Assert folding: add asserts expression NaN and Infinite floats. +-------------------------------------------------------------------------------- + +module Ivory.Opts.FP + ( fpFold + ) where + +import Ivory.Opts.AssertFold + +import qualified Ivory.Language.Syntax.AST as I +import qualified Ivory.Language.Syntax.Type as I + +-------------------------------------------------------------------------------- + +fpFold :: I.Proc -> I.Proc +fpFold = procFold (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 ty e = case ty of + I.TyFloat -> asst + I.TyDouble -> asst + _ -> [] + where asst = [mkAssert ty e] + +mkAssert :: I.Type -> I.Expr -> I.Expr +mkAssert ty e = 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 new file mode 100644 --- /dev/null +++ b/src/Ivory/Opts/Index.hs @@ -0,0 +1,72 @@ + +-------------------------------------------------------------------------------- +-- | Assert folding: add asserts expression for converting to and using indexes. +-------------------------------------------------------------------------------- + +module Ivory.Opts.Index + ( 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.Syntax.Type as I + +-------------------------------------------------------------------------------- + +ixFold :: I.Proc -> I.Proc +ixFold = procFold 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 +-- 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 + I.ExpSym{} -> 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.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 + I.ExpAddrOfGlobal{} -> return () + I.ExpMaxMin{} -> return () + +-------------------------------------------------------------------------------- + +-- | For toIx e :: Ix maxSz, assert +-- @ +-- 0 <= e < maxSz && 1 < 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 ] + ] + +-------------------------------------------------------------------------------- + +ixTy :: I.Type +ixTy = I.TyInt I.Int32 + +-------------------------------------------------------------------------------- + +lit :: Integer -> I.Expr +lit i = I.ExpLit (I.LitInteger i) + +-------------------------------------------------------------------------------- diff --git a/src/Ivory/Opts/Overflow.hs b/src/Ivory/Opts/Overflow.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Opts/Overflow.hs @@ -0,0 +1,197 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} + +-------------------------------------------------------------------------------- +-- | Assert folding: add asserts expression overflow/underflow. +-------------------------------------------------------------------------------- + +module Ivory.Opts.Overflow + ( overflowFold + ) 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 Ivory.Language + +import Prelude hiding (max,min) +import Data.Word +import Data.Int + +-------------------------------------------------------------------------------- + +overflowFold :: I.Proc -> I.Proc +overflowFold = procFold (expFoldDefault arithAssert) + +-------------------------------------------------------------------------------- + +type Bounds a = (a,a) + +arithAssert :: I.Type -> I.Expr -> [I.Expr] +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 + _ -> [] + +litAssert :: I.Type -> I.Literal -> [I.Expr] +litAssert ty lit = case lit of + I.LitInteger i -> + case ty of + I.TyWord I.Word8 -> boundLit (minMax :: Bounds Word8) + I.TyWord I.Word16 -> boundLit (minMax :: Bounds Word16) + I.TyWord I.Word32 -> boundLit (minMax :: Bounds Word32) + I.TyWord I.Word64 -> boundLit (minMax :: Bounds Word64) + I.TyInt I.Int8 -> boundLit (minMax :: Bounds Int8) + I.TyInt I.Int16 -> boundLit (minMax :: Bounds Int16) + I.TyInt I.Int32 -> boundLit (minMax :: Bounds Int32) + I.TyInt I.Int64 -> boundLit (minMax :: Bounds Int64) + _ -> [] + where + boundLit (min,max) = fmap T.unwrapExpr $ + 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 $ + 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.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.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.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.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)) + + 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 + + ---------------------------------------------------------- + + 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) + + 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))) + + 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) + + ---------------------------------------------------------- + + 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) + +---------------------------------------------------------- + +minMax :: forall t . (Bounded t) => Bounds t +minMax = (minBound :: t, maxBound :: t) diff --git a/src/Ivory/Opts/Utils.hs b/src/Ivory/Opts/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Opts/Utils.hs @@ -0,0 +1,29 @@ +-------------------------------------------------------------------------------- +-- | Utilities. +-------------------------------------------------------------------------------- + +module Ivory.Opts.Utils + +where + +import qualified Ivory.Language.Syntax.AST as I +import qualified Ivory.Language.Syntax.Type as I + +-------------------------------------------------------------------------------- + +-- | Type of the expression's arguments. +expOpType :: I.Type -> I.ExpOp -> I.Type +expOpType t0 op = case op of + I.ExpEq t1 -> t1 + I.ExpNeq t1 -> t1 + I.ExpGt _ t1 -> t1 + I.ExpLt _ t1 -> t1 + I.ExpIsNan t1 -> t1 + I.ExpIsInf t1 -> t1 + I.ExpToFloat t1 -> t1 + I.ExpFromFloat t1 -> t1 + _ -> t0 + +-------------------------------------------------------------------------------- + +