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