ivory-opts (empty) → 0.1.0.0
raw patch · 11 files changed
+1771/−0 lines, 11 filesdep +basedep +containersdep +dlistsetup-changed
Dependencies added: base, containers, dlist, fgl, filepath, ivory, monadLib
Files
- LICENSE +28/−0
- Setup.hs +2/−0
- ivory-opts.cabal +41/−0
- src/Ivory/Opts/AssertFold.hs +248/−0
- src/Ivory/Opts/CFG.hs +494/−0
- src/Ivory/Opts/ConstFold.hs +578/−0
- src/Ivory/Opts/DivZero.hs +45/−0
- src/Ivory/Opts/FP.hs +37/−0
- src/Ivory/Opts/Index.hs +72/−0
- src/Ivory/Opts/Overflow.hs +197/−0
- src/Ivory/Opts/Utils.hs +29/−0
+ LICENSE view
@@ -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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ ivory-opts.cabal view
@@ -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
+ src/Ivory/Opts/AssertFold.hs view
@@ -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]++--------------------------------------------------------------------------------
+ src/Ivory/Opts/CFG.hs view
@@ -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)++-}
+ src/Ivory/Opts/ConstFold.hs view
@@ -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
+ src/Ivory/Opts/DivZero.hs view
@@ -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."++--------------------------------------------------------------------------------
+ src/Ivory/Opts/FP.hs view
@@ -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]] ]
+ src/Ivory/Opts/Index.hs view
@@ -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)++--------------------------------------------------------------------------------
+ src/Ivory/Opts/Overflow.hs view
@@ -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)
+ src/Ivory/Opts/Utils.hs view
@@ -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++--------------------------------------------------------------------------------++