{-# LANGUAGE CPP #-} {-# LANGUAGE ImplicitParams, PatternGuards, ScopedTypeVariables #-} module ITransform( -- the transform stage iTransform -- optimize an expression of type Bool , iTransBoolExpr -- optimize an expression of any type , iTransExpr ) where #if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 804) import Prelude hiding ((<>)) #endif import Data.Traversable (forM) import Control.Monad.State hiding (forM) import Data.List((\\)) import Data.Maybe(isJust) import qualified Data.Map as M import IntegerUtil(mask, integerAnd) import Util(log2, itos, appFstM, snd3, makePairs, flattenPairs) import PPrint import IntLit import Position(noPosition, getPosition) import Error(internalError, ErrMsg(..), ErrorHandle, bsErrorUnsafe) import Flags(Flags, optBool) import FStringCompat(mkFString) import Id import Prim import Pragma(DefProp, defPropsHasNoCSE) import ISyntax import ISyntaxUtil import IPrims(doPrimOp) import IInline(iSortDs, iInline) import BExpr -- For boolean opt import Intervals import BoolExp import BoolOpt -- import Util(trace_answer) -- import Debug.Trace(trace, TraceM) -- import Util(traces) ----------------------------------------------------------------------------- -- use the special-purpose boolean optimizer to optimize a boolean expression -- instead of the general-purpose iTransExpr -- will use BDDs for boolean optimization when -opt-bool is set (like optIRule) iTransBoolExpr :: Flags -> IExpr a -> IExpr a iTransBoolExpr flags = optBoolExpr (optBool flags) ----------------------------------------------------------------------------- iTransExpr :: ErrorHandle -> IExpr a -> (IExpr a, Bool) iTransExpr errh = let ?errh = errh in iTransExpr' iTransExpr' :: (?errh :: ErrorHandle) => IExpr a -> (IExpr a, Bool) iTransExpr' (IAps f ts es) = iTrAp emptyCtx f ts es iTransExpr' e = (e, False) {- not really useful external uses only have one-level transformations exposed iTransExprLoop :: IExpr a -> IExpr a iTransExprLoop e = let (e', b') = iTransExpr e in if b' then -- recurse (try transforming more) iTransExprLoop e' else e' -} ----------------------------------------------------------------------------- iTransform :: ErrorHandle -> Flags -> String -> IModule a -> IModule a iTransform errh flags prefix = iInline False . -- XXX only for debug iTransform1 1 errh flags prefix . iSortDs iTransform1 :: Integer -> ErrorHandle -> Flags -> String -> IModule a -> IModule a iTransform1 no errh flags prefix imod@(IModule { imod_state_insts = itvs, imod_local_defs = ds, imod_rules = rs, imod_interface = ifc }) = imod { imod_state_insts = itvs', imod_local_defs = ds', imod_rules = rs', imod_interface = ifc' } where ((itvs', rs', ifc'), ds') = runT errh flags no prefix trMod trMod = do mapM_ iTrDef ds iTransFixupDefNames flags rs' <- iTrRules rs ifc' <- mapM iTrIfc ifc -- clock and reset expressions (in nc and nr) are just wires - do not simplify itvs' <- mapM (\ (i, sv@(IStateVar { isv_iargs = es })) -> do es' <- mapM (iTrExprL emptyCtx []) es return (i, sv { isv_iargs = es' })) itvs return (itvs', rs', ifc') iTrIfc :: IEFace a -> T (IEFace a) a iTrIfc (IEFace i its met mrs wp fi) = do met' <- forM met (appFstM $ iTrExprL emptyCtx []) mrs' <- forM mrs iTrRules return (IEFace i its met' mrs' wp fi) iTrDef :: IDef a -> T () a iTrDef def@(IDef i t e p) = do -- traceM ("iTrDef start " ++ ppReadable def) e' <- iTrExprL emptyCtx [] e -- traceM ("iTrDef process " ++ ppReadable (i, e', expVal e')) addDefT i t e' p iTrRule :: IRule a -> T (IRule a) a iTrRule r = do doBO <- getDoBO let ctx = emptyCtx -- traceM("iTrRule start " ++ ppReadable (irule_name r)) c' <- iTrExprL ctx [] (irule_pred r) let c'' = optBoolExpr doBO c' -- traceM("iTrRule cond " ++ ppReadable (irule_name r, c'')) e' <- iTrExprL (addT c'' ctx) [] (irule_body r) -- traceM("iTrRule body " ++ ppReadable (irule_name r, e')) return $ r { irule_pred = c'', irule_body = e' } iTrRules :: IRules a -> T (IRules a) a iTrRules (IRules sps rs) = do rs' <- mapM iTrRule rs return (IRules sps rs') iTrExprL :: Ctx a -> [(IExpr a, Integer)] -> IExpr a -> T (IExpr a) a iTrExprL ctx idxs e = expandHRef e >>= iTrExpr ctx idxs iTrExpr :: Ctx a -> [(IExpr a, Integer)] -> IExpr a -> T (IExpr a) a iTrExpr ctx idxs (IAps pif@(ICon _ (ICPrim _ PrimIf)) [t] [cnd, thn, els]) = do doBO <- getDoBO cnd1 <- iTrExpr ctx [] (expValShallow cnd) let cnd' = optBoolExpr doBO cnd1 thn' <- iTrExpr (addT cnd' ctx) idxs thn els' <- iTrExpr (addF cnd' ctx) idxs els -- traceM ("IF " ++ ppString (IAps pif [t] [cnd', thn', els']) ++ "\n " ++ ppReadable (cnd, cnd0, cnd1)) iTrExpr' ctx idxs pif [t] [cnd', thn', els'] iTrExpr ctx idxs (IAps pcase@(ICon _ (ICPrim _ PrimCase)) ts@[sz_idx, elem_ty] (idx:dflt:ces)) = do idx' <- iTrExpr ctx [] (expValShallow idx) let foldFn (res_ces, res_ctx) (c,e) = do c' <- iTrExpr ctx [] (expValShallow c) let eq_e = iePrimEQ sz_idx idx' c' e' <- iTrExpr (addT eq_e res_ctx) idxs e return ((c',e'):res_ces, addF eq_e res_ctx) (rev_ces', ctx') <- foldM foldFn ([], ctx) (makePairs ces) let ces' = flattenPairs (reverse rev_ces') dflt' <- iTrExpr ctx' idxs dflt iTrExpr' ctx idxs pcase ts (idx':dflt':ces') iTrExpr ctx idxs (IAps psel@(ICon _ (ICPrim _ PrimArrayDynSelect)) ts@[elem_ty, ITNum sz_idx] [arr, idx]) = do idx' <- iTrExpr ctx [] (expValShallow idx) arr' <- iTrExpr ctx ((idx,sz_idx):idxs) (expValShallow arr) iTrExpr' ctx idxs psel ts [arr', idx'] iTrExpr ctx idxs@((idx,sz_idx):rest_idxs) (IAps pupd@(ICon _ (ICPrim _ PrimArrayDynUpdate)) ts@[elem_ty, ITNum sz_upd_idx] [arr, upd_idx, val]) = do upd_idx' <- iTrExpr ctx [] (expValShallow upd_idx) let mkExtend in_sz out_sz e = let k = out_sz - in_sz ts = [ITNum k, ITNum in_sz, ITNum out_sz] in IAps icPrimZeroExt ts [e] eq_e = let (max_sz, e1, e2) | sz_idx > sz_upd_idx = (sz_idx, idx, mkExtend sz_upd_idx sz_idx upd_idx) | sz_idx < sz_upd_idx = (sz_upd_idx, mkExtend sz_idx sz_upd_idx idx, upd_idx) | otherwise = (sz_upd_idx, idx, upd_idx) in iePrimEQ (ITNum max_sz) e1 e2 val' <- iTrExpr (addT eq_e ctx) idxs (expValShallow val) arr' <- iTrExpr (addF eq_e ctx) idxs (expValShallow arr) iTrExpr' ctx idxs pupd ts [arr', upd_idx', val'] iTrExpr ctx idxs@((idx,sz_idx):rest_idxs) (IAps pbld@(ICon i (ICPrim _ PrimBuildArray)) ts es) = do let foldFn (res_es, res_ctx) (n, e) = do let n_lit = iMkLitAt (getPosition i) (aitBit (ITNum sz_idx)) n let eq_e = iePrimEQ (ITNum sz_idx) idx n_lit e' <- iTrExpr (addT eq_e res_ctx) rest_idxs (expValShallow e) return (e':res_es, addF eq_e res_ctx) (rev_es', _) <- foldM foldFn ([], ctx) (zip [0..] es) iTrExpr' ctx idxs pbld ts (reverse rev_es') iTrExpr ctx idxs (IAps pand@(ICon _ (ICPrim _ PrimBAnd)) ts [e1, e2]) = do e1' <- iTrExpr ctx [] e1 e2'' <- iTrExpr (addT e1' ctx) [] (expValShallow e2) e1'' <- iTrExpr (addT e2'' ctx) [] (expValShallow e1') iTrExpr' ctx idxs pand ts [e1'', e2''] iTrExpr ctx idxs (IAps por@(ICon _ (ICPrim _ PrimBOr)) ts [e1, e2]) = do e1' <- iTrExpr ctx [] e1 e2'' <- iTrExpr (addF e1' ctx) [] (expValShallow e2) e1'' <- iTrExpr (addF e2'' ctx) [] (expValShallow e1') iTrExpr' ctx idxs por ts [e1'', e2''] iTrExpr ctx idxs (IAps f ts es) = do es' <- mapM (iTrExpr ctx []) es iTrExpr' ctx idxs f ts es' -- XXX This makes some conditions simpler, but maybe other things get worse? iTrExpr ctx idxs (ICon _ (ICUndet t _ _)) | t == itAction = return icNoActions iTrExpr ctx idxs (ICon i (ICUndet t k (Just e))) = do e' <- iTrExpr ctx idxs e return (ICon i (ICUndet t k (Just e'))) iTrExpr ctx idxs e = return e expandHRef :: IExpr a -> T (IExpr a) a expandHRef (IAps f ts es) = do f' <- expandHRef f es' <- mapM expandHRef es return (IAps f' ts es') expandHRef e@(ICon i (ICValue { })) = do me <- getDefT i case me of Just e' -> return e' Nothing -> return e -- probably not necessary -- included so we could re-run ITransform if we wanted expandHRef (ICon i (ICUndet t k (Just e))) = do e' <- expandHRef e return (ICon i (ICUndet t k (Just e'))) expandHRef e = return e -- XXX --expandHRef e = internalError ("expandHRef " ++ ppReadable e) iTrExpr' :: Ctx a -> [(IExpr a, Integer)] -> IExpr a -> [IType] -> [IExpr a] -> T (IExpr a) a iTrExpr' ctx idxs f ts es = do errh <- gets errHandle let (et, trans) = let ?errh = errh in iTrAp ctx f ts es if trans then iTrExpr ctx idxs et else do e <- runCSE et let t = iGetType e isBool = t == itBit1 if isBool && isT ctx e then return iTrue else if isBool && isF ctx e then return iFalse else return e runCSE :: IExpr a -> T (IExpr a) a runCSE e@(IAps _ _ _) = do -- This used to recurse on the arguments, but we don't need to do that, -- because "runCSE" is called from iTrExpr, which already recurses on the -- arguments, so runCSE will already have been called on the arguments. let t = iGetType e -- Only CSE applications that are not actions if not (isActionType t) then newExprT t e else return e -- should CSE values boxed by undefined -- they have something to CSE against runCSE (ICon i (ICUndet t k (Just v))) = do v' <- runCSE v let e' = ICon i (ICUndet t k (Just v')) return e' runCSE e = return e -- recursively transform an expression -- noting that a nontrivial transformation has happened {-# INLINE iTrAp2 #-} iTrAp2 :: (?errh :: ErrorHandle) => Ctx a -> IExpr a -> [IType] -> [IExpr a] -> (IExpr a, Bool) iTrAp2 ctx e ts es = (iTrApExp ctx e ts es, True) -- transform an expression, forgetting whether an transformation -- was done or not - used for recursive transformation {-# INLINE iTrApExp #-} iTrApExp :: (?errh :: ErrorHandle) => Ctx a -> IExpr a -> [IType] -> [IExpr a] -> IExpr a iTrApExp ctx e ts es = fst (iTrAp ctx e ts es) -- transform an expression, if it is an application iTrExprIfAp :: (?errh :: ErrorHandle) => Ctx a -> IExpr a -> (IExpr a, Bool) iTrExprIfAp ctx (IAps f ts es) = iTrAp ctx f ts es iTrExprIfAp _ e = (e,False) -- -- Transform an application. -- The arguments need to be unfolded when they are matched against IAps nodes, -- since these are already CSEed. -- Returns a flag indicating whether the expression changed or not iTrAp :: (?errh :: ErrorHandle) => Ctx a -> IExpr a -> [IType] -> [IExpr a] -> (IExpr a, Bool) -- eliminate null actions iTrAp ctx (ICon _ (ICPrim _ PrimJoinActions)) _ [ICon _ (ICPrim _ PrimNoActions), e] = (e, True) iTrAp ctx (ICon _ (ICPrim _ PrimJoinActions)) _ [e, ICon _ (ICPrim _ PrimNoActions)] = (e, True) -- if True t e --> t -- if False t e --> e -- if c t t --> t -- if c True False --> c -- if c True e --> c || e -- if c False True --> not c -- if c False e --> not c && e -- if c t True --> not c || t -- if c t False --> c && t -- if c t _ --> t -- if c _ e --> e iTrAp ctx p@(ICon _ (ICPrim _ PrimIf)) [t] [cnd, thn, els] | isT ctx cnd = (thn, True) | isF ctx cnd = (els, True) | eqE thn els = (thn, True) | otherwise = case (t == itBit1, thn, els) of (True, ICon _ (ICInt { iVal = IntLit { ilValue = 1 } }), ICon _ (ICInt { iVal = IntLit { ilValue = 0 } })) -> (cnd, True) (True, ICon _ (ICInt { iVal = IntLit { ilValue = 1 } }), _ ) -> iTrAp2 ctx iOr [] [cnd, els] (True, ICon _ (ICInt { iVal = IntLit { ilValue = 0 } }), ICon _ (ICInt { iVal = IntLit { ilValue = 1 } })) -> iTrAp2 ctx iNot [] [cnd] (True, ICon _ (ICInt { iVal = IntLit { ilValue = 0 } }), _ ) -> iTrAp2 ctx iAnd [] [iTrApExp ctx iNot [] [cnd], els] (True, _, ICon _ (ICInt { iVal = IntLit { ilValue = 1 } })) -> iTrAp2 ctx iOr [] [iTrApExp ctx iNot [] [cnd], thn] (True, _, ICon _ (ICInt { iVal = IntLit { ilValue = 0 } })) -> iTrAp2 ctx iAnd [] [cnd, thn] (_, _, _ ) -> case (expVal cnd, expVal thn, expVal els) of -- if c1 t (if c2 t e) --> if (c1 || c2) t e (_, _, IAps (ICon _ (ICPrim _ PrimIf)) _ [cnd2, thn2, els2]) | eqE thn thn2 -> iTrAp2 ctx p [t] [ieOr cnd cnd2, thn, els2] {- -- This opt is an improvement, but it triggers too much inlining in some -- examples. I'm reverting it, for backwards compatibility, until we add a -- pass (after ITransform? during VeriQuirks?) that lifts subexpressions -- from defs whose expression is too large. -- if c1 (if c2 t e) e --> if (c1 && c2) t e (_, IAps (ICon _ (ICPrim _ PrimIf)) _ [cnd2, thn2, els2], _) | eqE els els2 -> iTrAp2 ctx p [t] [ieAnd cnd cnd2, thn2, els] -} -- XXX Can this ever be harmful? It removes a constant... -- if (x == k) k e --> if (x == k) x e (cnd', _, _) | (case cnd' of (IAps (ICon _ (ICPrim _ PrimEQ)) _ [x, k@(ICon _ _)]) -> k == thn && thn /= x _ -> False ) -> iTrAp2 ctx p [t] [cnd, x, els] where (IAps _ _ [x, _]) = cnd' -- We used to perform this tagging -- (only for bit-type, not Action, and not in the evaluator) -- if c e _ --> if c e _[e] -- But this could use an ActionValue value outside its scope. -- Also, it appears to be unnecessary (and prematurely picks -- a value. So it has been removed. But the opt also -- included two other opts, which we preserve (and apply even -- in the evaluator: -- if c _ _ --> _ -- XXX This only applies if one of the don't-care has not -- XXX been tagged. Can we ignore tags? Is this opt even used? (_, ICon _ (ICUndet { imVal = Nothing }), ICon _ (ICUndet {})) -> (els, True) (_, ICon _ (ICUndet {}), ICon _ (ICUndet { imVal = Nothing })) -> (thn, True) {- -- This opt was OK when we still had the above optimization for tagging of -- don't-care values. When we remove it, this opt becomes a problem -- (somes modules hang in the transform stage). Until we understand why, -- I'm removing it. -- if c {e1, e2} _ --> if c {e1, e2} {_, _} (_, ICon i (ICUndet { iuKind = u, imVal = Nothing }), IAps c@(ICon _ (ICPrim _ PrimConcat)) ts@[ITNum n, ITNum k, ITNum l] [e1, e2]) -> let t1 = itBitN n t2 = itBitN k thn' = IAps c ts [ICon i (ICUndet t1 u Nothing), ICon i (ICUndet t2 u Nothing)] in iTrAp2 ctx p [t] [cnd, thn', els] (_, IAps c@(ICon _ (ICPrim _ PrimConcat)) ts@[ITNum n, ITNum k, ITNum l] [e1, e2], ICon i (ICUndet { iuKind = u, imVal = Nothing })) -> let t1 = itBitN n t2 = itBitN k els' = IAps c ts [ICon i (ICUndet t1 u Nothing), ICon i (ICUndet t2 u Nothing)] in iTrAp2 ctx p [t] [cnd, thn, els'] -} -- Special case for turning pack.unpack into an identity -- if (select _ l _ e == c) (c ++ select k m _ e) x --> IF k+m == l -- if (select _ l _ e == c) (select _ l _ e ++ select k m _ e) x (IAps (ICon _ (ICPrim _ PrimEQ)) _ [sel1, c], IAps (ICon _ (ICPrim _ PrimConcat)) ts [c', sel2], _) | eqE c c' && (case expVal sel1 of IAps (ICon _ (ICPrim _ PrimSelect)) [_, ITNum ls, _] [e] -> case expVal sel2 of IAps (ICon _ (ICPrim _ PrimSelect)) [ITNum k, ITNum m, _] [e'] -> k + m == ls && eqE e e' ICon _ (ICUndet { imVal = Nothing }) -> True _ -> False _ -> False ) -> iTrAp2 ctx p [t] [cnd, IAps icPrimConcat ts [sel1, sel2], els] -- if c (x1++x2) (x1++y2) --> x1 ++ (if c x2 y2) -- if c (x1++x2) (y1++x2) --> (if c x1 y1) ++ x2 -- check if we make progress to avoid infinite loops (_, IAps pc@(ICon _ (ICPrim _ PrimConcat)) ts@[t1,t2,_] [x1, x2], IAps (ICon _ (ICPrim _ PrimConcat)) ts' [y1, y2] ) | ts == ts', let (e1', opt1) = iTrAp ctx p [aitBit t1] [cnd, x1, y1], let (e2', opt2) = iTrAp ctx p [aitBit t2] [cnd, x2, y2], opt1 || opt2 -> iTrAp2 ctx pc ts [e1', e2'] -- if (not c) t e --> if c e t (IAps (ICon _ (ICPrim _ PrimBNot)) _ [c], _, _) -> iTrAp2 ctx p [t] [c,els,thn] -- if c t e --> if c t[c=True] e[c=False] -- ie. substitute known value of c in sub-exprs XXX: -- This doesn't handle the general case of -- substituting the condition in the sub-exprs, it -- only handles replacing the input expr when it is c -- or !c. There is a worry that general substitution -- could create extra logic in the presence of sharing -- and be computationally expensive due to repeated -- traversal of expressions doing different -- substitutions. (_,_,_) | eqE cnd thn -> iTrAp2 ctx p [t] [cnd,iTrue,els] (_,_,_) | eqE cnd els -> iTrAp2 ctx p [t] [cnd,thn,iFalse] (_,IAps (ICon _ (ICPrim _ PrimBNot)) _ [x],_) | eqE cnd x -> iTrAp2 ctx p [t] [cnd,iFalse,els] (_,_,IAps (ICon _ (ICPrim _ PrimBNot)) _ [x]) | eqE cnd x -> iTrAp2 ctx p [t] [cnd,thn,iTrue] _ -> (IAps p [t] [cnd, thn, els], False) -- Boolean optimization -- False && e --> False -- e && False --> False -- e1 && e2 --> e1 IF e1 IMPLIES e2 -- e2 && e1 --> e2 IF e2 IMPLIES e1 -- these two cases may be logically redundant, but the -- compiler might be able to optimize one path and not the other -- e1 && e2 --> False IF e1 IMPLIES ~e2 -- e2 && e1 --> False IF e2 IMPLIES ~e1 iTrAp ctx p@(ICon _ (ICPrim _ PrimBAnd)) _ [c1, c2] | isF ctx c1 || isF ctx c2 = (iFalse, True) -- fast special case | isUndet c1 || isUndet c2 = (iFalse, True) | implies ctx c1 c2 = (c1, True) | implies ctx c2 c1 = (c2, True) | impliesnot ctx c1 c2 = (iFalse, True) | impliesnot ctx c2 c1 = (iFalse, True) | otherwise = (IAps p [] [c1, c2], False) -- True || e --> True -- e || True --> True -- e1 || e2 --> e1 IF e2 IMPLIES e1 -- e2 || e1 --> e2 IF e1 IMPLIES e2 -- these two cases may be logically redundant, but the -- compiler might be able to optimize one path and not the other -- e1 || e2 --> True IF ~e1 IMPLIES e2 -- e1 || e2 --> True IF ~e2 IMPLIES e1 iTrAp ctx p@(ICon _ (ICPrim _ PrimBOr)) _ [c1, c2] | isT ctx c1 || isT ctx c2 = (iTrue, True) -- fast special case | isUndet c1 || isUndet c2 = (iTrue, True) | implies ctx c2 c1 = (c1, True) | implies ctx c1 c2 = (c2, True) | notimplies ctx c1 c2 = (iTrue, True) | notimplies ctx c2 c1 = (iTrue, True) | otherwise = (IAps p [] [c1, c2], False) -- not True --> False -- not False --> True -- not (not e) --> e -- not (e1 && e2) --> not e1 || not e2 -- not (e1 || e2) --> not e1 && not e2 -- not (e1 RELOP e2) --> e1 (inv RELOP) e2 -- not (if c t e) --> if c (not t) (not e) -- XXX There is no rule for pushing inside dynamic array select/update iTrAp ctx p@(ICon _ (ICPrim _ PrimBNot)) _ [c] | isF ctx c = (iTrue, True) | isT ctx c = (iFalse, True) | otherwise = case expVal c of IAps (ICon _ (ICPrim _ PrimBNot)) _ [e] -> (e, True) IAps (ICon _ (ICPrim _ PrimBAnd)) _ [e1, e2] -> iTrAp2 ctx iOr [] [iTrApExp ctx iNot [] [e1], iTrApExp ctx iNot [] [e2]] IAps (ICon _ (ICPrim _ PrimBOr)) _ [e1, e2] -> iTrAp2 ctx iAnd [] [iTrApExp ctx iNot [] [e1], iTrApExp ctx iNot [] [e2]] IAps i@(ICon _ (ICPrim _ PrimIf)) [t] [e1,e2,e3] -> iTrAp2 ctx i [t] [e1, iTrApExp ctx iNot [] [e2], iTrApExp ctx iNot [] [e3]] u@(ICon i (ICUndet t k Nothing)) -> (u, True) _ -> (IAps p [] [c], False) -- e == e --> True iTrAp ctx (ICon _ (ICPrim _ PrimEQ)) _ [e, e'] | e == e' = (iTrue, True) -- e <= e --> True -- e < e --> False iTrAp ctx (ICon _ (ICPrim _ p)) _ [e, e'] | isLE p, e == e' = (iTrue, True) where isLE = (`elem` [PrimULE, PrimSLE]) iTrAp ctx (ICon _ (ICPrim _ p)) _ [e, e'] | isLT p, e == e' = (iFalse, True) where isLT = (`elem` [PrimULT, PrimSLT]) -- XXX: preserve the _ "kind"? Or treat different _ differently? -- _ == e --> _ iTrAp ctx (ICon _ (ICPrim _ PrimEQ)) _ [e1@(ICon _ (ICUndet {iuKind = u, imVal = Nothing})), e2] = (icUndet itBit1 u, True) -- e == _ --> _ iTrAp ctx (ICon _ (ICPrim _ PrimEQ)) _ [e1, e2@(ICon _ (ICUndet {iuKind = u, imVal = Nothing}))] = (icUndet itBit1 u, True) -- e + c1 == c2 --> e == c2 - c1 -- e - c1 == c2 --> e == c2 + c1 -- This code does not treat other relational operators, because -- the flipped versions are not equivalent in the presence of over- -- and under-flow. -- e ^ c1 == c2 --> e == c2 ^ c1 iTrAp ctx rel_c@(ICon _ (ICPrim _ PrimEQ)) t1@[ITNum i1] [e', c2] | -- app of a PrimEQ with a single type variable (isIConInt c2) && -- c2 is a constant case expVal e' of (IAps (ICon _ (ICPrim _ op)) t2@[ITNum i2] [e, c1]) -> -- app of a prim op with a single type variable (isIConInt c1) && (not (isIConInt e)) && -- c1 is a constant, e is not a constant (to ensure progress) ((op == PrimAdd) || (op == PrimSub) || (op == PrimXor)) && -- op is one of these (i1 == i2) -- the type variables are the same _ -> False = case expVal e' of (IAps opc@(ICon _ (ICPrim _ op)) _ [e, c1]) -> let inv_op = case op of PrimAdd -> PrimSub PrimSub -> PrimAdd PrimXor -> PrimXor _ -> internalError ("ITransform.iTrAp.inv_op: " ++ ppString op) -- c3 == iTrap ctx inv_op t2 [c2,c1] -- do the computation here: c3 = case (doPrimOp (getIExprPosition opc) inv_op t1 [c2,c1]) of Just (Right e) -> e x -> internalError ("iTrAp: doPrimOp: " ++ ppReadable x) in -- any reason to use "icPrimEQ" etc instead of reusing "rel_c"? iTrAp2 ctx rel_c t1 [e, c3] _ -> internalError "ITransform.iTrAp(PrimEQ).expVal e': bad form" -- For these next two, we only want to perform the optimization when we know -- that it leads to an improvement in the expression, otherwise we risk -- preventing case statement reconstruction by obscuring the comparison. -- e1 ++ e2 == e3 => (e1 == e3[0:i1 - 1] && e2 == e3[i1:i3]) iTrAp ctx eq@(ICon ideq (ICPrim _ PrimEQ)) t_eq@[ITNum i_eq] [e_concat@(IAps cat_con@(ICon _ (ICPrim _ PrimConcat)) cat_ty@[ITNum i1, ITNum i2, ITNum i3] cat_args@[e1, e2]), e3] | i3 == i_eq = -- otherwise the comparison is buggy -- try to improve e1_eq and e2_eq let improved x = (x == iTrue) || (x == iFalse) in if ((improved e1_eq) || (improved e2_eq)) then iTrAp2 ctx iAnd [] [e1_eq, e2_eq] else -- no benefit from splitting, so just use the optimized sub-exprs (IAps eq t_eq [cat, e3'], (mod_cat || mod_e3)) where e1_eq = iTrApExp ctx icPrimEQ [ITNum i1] [e1,e3_e1] e2_eq = iTrApExp ctx icPrimEQ [ITNum i2] [e2,e3_e2] e3_e1 = iTrApExp ctx (icSelect (getIdPosition ideq)) [ITNum i1, ITNum i2, ITNum i3] [e3] e3_e2 = iTrApExp ctx (icSelect (getIdPosition ideq)) [ITNum i2, ITNum 0, ITNum i3] [e3] (cat,mod_cat) = iTrAp ctx cat_con cat_ty cat_args (e3',mod_e3) = iTrExprIfAp ctx e3 -- e3 == e1 ++ e2 => (e1 == e3[0:i1 - 1] && e2 == e3[i1:i3]) iTrAp ctx eq@(ICon ideq (ICPrim _ PrimEQ)) t_eq@[ITNum i_eq] [e3, e_concat@(IAps cat_con@(ICon _ (ICPrim _ PrimConcat)) cat_ty@[ITNum i1, ITNum i2, ITNum i3] cat_args@[e1, e2])] | i3 == i_eq = -- otherwise the comparison is buggy let improved x = (x == iTrue) || (x == iFalse) in if ((improved e1_eq) || (improved e2_eq)) then iTrAp2 ctx iAnd [] [e1_eq, e2_eq] else -- no benefit from splitting, so just use the optimized sub-exprs (IAps eq t_eq [e3', cat], (mod_cat || mod_e3)) where e1_eq = iTrApExp ctx icPrimEQ [ITNum i1] [e1,e3_e1] e2_eq = iTrApExp ctx icPrimEQ [ITNum i2] [e2,e3_e2] e3_e1 = iTrApExp ctx (icSelect (getIdPosition ideq)) [ITNum i1, ITNum i2, ITNum i3] [e3] e3_e2 = iTrApExp ctx (icSelect (getIdPosition ideq)) [ITNum i2, ITNum 0, ITNum i3] [e3] (cat,mod_cat) = iTrAp ctx cat_con cat_ty cat_args (e3',mod_e3) = iTrExprIfAp ctx e3 -- select n 0 n e --> e iTrAp ctx (ICon _ (ICPrim _ PrimSelect)) [n, ITNum 0, n'] [e] | n == n' = (e, True) -- select 0 _ _ e --> 0 iTrAp ctx (ICon _ (ICPrim _ PrimSelect)) [t@(ITNum 0), _, _] [_] = (mkZero t, True) -- e * 0 --> 0 -- 0 * e --> 0 iTrAp ctx (ICon _ (ICPrim _ PrimMul)) [_,_,sz] [e,c] | isZero c = (mkZero sz, True) iTrAp ctx (ICon _ (ICPrim _ PrimMul)) [_,_,sz] [c,e] | isZero c = (mkZero sz, True) -- e * 1 --> e -- 1 * e --> e iTrAp ctx (ICon _ (ICPrim _ PrimMul)) [se,sk@(ITNum k_size),sz] [e,c] | isOne c = (e', True) where e' = iTrApExp ctx icPrimConcat [sk,se,sz] [iMkLitSize k_size 0, e] iTrAp ctx (ICon _ (ICPrim _ PrimMul)) [sk@(ITNum k_size),se,sz] [c,e] | isOne c = (e', True) where e' = iTrApExp ctx icPrimConcat [sk,se,sz] [iMkLitSize k_size 0, e] -- e * 2^k --> e << k iTrAp ctx (ICon _ (ICPrim _ PrimMul)) [se,sk@(ITNum k_size),sz] [e, ICon _ (ICInt { iVal = IntLit { ilValue = n } })] | m /= Nothing = iTrAp2 ctx icPrimSL [sz, ITNum 32] [e', iMkLit itNat k] where e' = iTrApExp ctx icPrimConcat [sk, se, sz] [iMkLitSize k_size 0, e] m = iLog2 n Just k = m -- 2^k * e --> e << k iTrAp ctx (ICon _ (ICPrim _ PrimMul)) [sk@(ITNum k_size),se,sz] [ICon _ (ICInt { iVal = IntLit { ilValue = n } }), e] | m /= Nothing = iTrAp2 ctx icPrimSL [sz, ITNum 32] [e', iMkLit itNat k] where e' = iTrApExp ctx icPrimConcat [sk, se, sz] [iMkLitSize k_size 0, e] m = iLog2 n Just k = m -- 0 | e --> e -- 1 | e --> 1 -- 0 & e --> 0 -- 1 & e --> e -- and v.v. (with better granularity) iTrAp ctx p@(ICon _ (ICPrim _ PrimOr)) [ITNum n] [ICon _ (ICInt {iVal = IntLit {ilValue = i}}), e] | n > 0 = case getMaskTail i n of Zeroes l -> let k = n - l -- XXX expression duplication hd = iTrApExp ctx p [ITNum k] [iMkLitSize k (i `div` 2^l), IAps sel [ITNum k, ITNum l, ITNum n] [e]] tl = iTrApExp ctx sel [ITNum l, ITNum 0, ITNum n] [e] in iTrAp2 ctx icPrimConcat [ITNum k, ITNum l, ITNum n] [hd, tl] Ones l -> let k = n - l hd = iTrApExp ctx p [ITNum k] [iMkLitSize k (i `div` 2^l), IAps sel [ITNum k, ITNum l, ITNum n] [e]] tl = iMkLitSize l (2^l - 1) -- all ones in iTrAp2 ctx icPrimConcat [ITNum k, ITNum l, ITNum n] [hd, tl] where sel = icSelect (getIExprPosition p) iTrAp ctx p@(ICon _ (ICPrim _ PrimOr)) t@[ITNum n] [e, c@(ICon _ (ICInt {}))] = iTrAp ctx p t [c, e] iTrAp ctx p@(ICon _ (ICPrim _ PrimAnd)) [ITNum n] [ICon _ (ICInt {iVal = IntLit {ilValue = i}}), e] | n > 0 = case getMaskTail i n of Zeroes l -> let k = n - l hd = iTrApExp ctx p [ITNum k] [iMkLitSize k (i `div` 2^l), IAps sel [ITNum k, ITNum l, ITNum n] [e]] tl = iMkLitSize l 0 -- all zeroes in iTrAp2 ctx icPrimConcat [ITNum k, ITNum l, ITNum n] [hd, tl] Ones l -> let k = n - l -- XXX expression duplication hd = iTrApExp ctx p [ITNum k] [iMkLitSize k (i `div` 2^l), IAps sel [ITNum k, ITNum l, ITNum n] [e]] tl = iTrApExp ctx sel [ITNum l, ITNum 0, ITNum n] [e] in iTrAp2 ctx icPrimConcat [ITNum k, ITNum l, ITNum n] [hd, tl] where sel = icSelect (getIExprPosition p) iTrAp ctx p@(ICon _ (ICPrim _ PrimAnd)) t@[ITNum n] [e, c@(ICon _ (ICInt {}))] = iTrAp ctx p t [c, e] -- 0 ^ e --> e -- 1 ^ e --> ~e -- and v.v. -- with better granularity iTrAp ctx p@(ICon _ (ICPrim _ PrimXor)) [ITNum n] [ICon _ (ICInt {iVal = IntLit {ilValue = i}}), e] | n > 0 = case getMaskTail i n of Zeroes l -> let k = n - l -- XXX expression duplication hd = iTrApExp ctx p [ITNum k] [iMkLitSize k (i `div` 2^l), IAps sel [ITNum k, ITNum l, ITNum n] [e]] tl = iTrApExp ctx sel [ITNum l, ITNum 0, ITNum n] [e] in iTrAp2 ctx icPrimConcat [ITNum k, ITNum l, ITNum n] [hd, tl] Ones l -> let k = n - l -- XXX expression duplication hd = iTrApExp ctx p [ITNum k] [iMkLitSize k (i `div` 2^l), IAps sel [ITNum k, ITNum l, ITNum n] [e]] tl = iTrApExp ctx icPrimInv [ITNum l] [IAps sel [ITNum l, ITNum 0, ITNum n] [e]] in iTrAp2 ctx icPrimConcat [ITNum k, ITNum l, ITNum n] [hd, tl] where sel = icSelect (getIExprPosition p) iTrAp ctx p@(ICon _ (ICPrim _ PrimXor)) t@[ITNum n] [e, c@(ICon _ (ICInt {}))] = iTrAp ctx p t [c, e] {- iTrAp ctx (ICon _ (ICPrim _ PrimOr)) _ [c, e] | isZero c = (e, True) iTrAp ctx (ICon _ (ICPrim _ PrimOr)) _ [e, c] | isZero c = (e, True) iTrAp ctx (ICon _ (ICPrim _ PrimOr)) _ [c, e] | isAllOnes c = (c, True) iTrAp ctx (ICon _ (ICPrim _ PrimOr)) _ [e, c] | isAllOnes c = (c, True) iTrAp ctx (ICon _ (ICPrim _ PrimAnd)) _ [c, e] | isZero c = (c, True) iTrAp ctx (ICon _ (ICPrim _ PrimAnd)) _ [e, c] | isZero c = (c, True) iTrAp ctx (ICon _ (ICPrim _ PrimAnd)) _ [c, e] | isAllOnes c = (e, True) iTrAp ctx (ICon _ (ICPrim _ PrimAnd)) _ [e, c] | isAllOnes c = (e, True) -- 0 ^ e --> e -- e ^ 0 --> e iTrAp ctx (ICon _ (ICPrim _ PrimXor)) _ [c, e] | isZero c = (e, True) iTrAp ctx (ICon _ (ICPrim _ PrimXor)) _ [e, c] | isZero c = (e, True) -- 1 ^ e --> ~e -- e ^ 1 --> ~e iTrAp ctx (ICon _ (ICPrim _ PrimXor)) [t] [c, e] | isAllOnes c = iTrAp2 ctx icPrimInv [t] [e] iTrAp ctx (ICon _ (ICPrim _ PrimXor)) [t] [e, c] | isAllOnes c = iTrAp2 ctx icPrimInv [t] [e] -} -- 0 + e --> e -- e + 0 --> e -- e - 0 --> e iTrAp ctx (ICon _ (ICPrim _ PrimAdd)) _ [c, e] | isZero c = (e, True) iTrAp ctx (ICon _ (ICPrim _ PrimAdd)) _ [e, c] | isZero c = (e, True) iTrAp ctx (ICon _ (ICPrim _ PrimSub)) _ [e, c] | isZero c = (e, True) -- e - e --> 0 iTrAp ctx (ICon _ (ICPrim _ PrimSub)) [t] [e, e'] | e == e' = (mkZero t, True) -- e / 1 --> e iTrAp ctx (ICon _ (ICPrim _ PrimQuot)) _ [e, c] | isOne c = (e, True) -- e / 2^k --> e >> k iTrAp ctx (ICon _ (ICPrim _ PrimQuot)) [se,_] [e, ICon _ (ICInt { iVal = IntLit { ilValue = n } })] | m /= Nothing = iTrAp2 ctx icPrimSRL [se] [e, iMkLit itNat k] where m = iLog2 n Just k = m -- e % 1 --> 0 iTrAp ctx (ICon _ (ICPrim _ PrimRem)) [_,sk] [_,c] | isOne c = (mkZero sk, True) -- e % 2^k --> e[k-1:0] (with optional zero extension) iTrAp ctx (ICon remid (ICPrim _ PrimRem)) [se,sk@(ITNum k_size)] [e, ICon _ (ICInt { iVal = IntLit { ilValue = n } })] | m /= Nothing = if (pad == 0) then (e', True) else iTrAp2 ctx icPrimConcat [ITNum pad, ITNum k, sk] [iMkLitSize pad 0, e'] where e' = iTrApExp ctx (icSelect (getIdPosition remid)) [(ITNum k), ITNum 0, se] [e] m = iLog2 n Just k = m pad = k_size - k -- e < 0 --> False -- e <= 0 --> e == 0 -- e < 1 --> e == 0 -- e <= 0xe --> e /= 0xf -- e < 0xf --> e /= 0xf -- e <= 0xf --> True iTrAp ctx (ICon _ (ICPrim _ PrimULT)) [_] [_, c] | isZero c = (iFalse, True) iTrAp ctx (ICon _ (ICPrim _ PrimULE)) [t] [e, c] | isZero c = iTrAp2 ctx icPrimEQ [t] [e, c] iTrAp ctx (ICon _ (ICPrim _ PrimULT)) [t] [e, c] | isOne c = iTrAp2 ctx icPrimEQ [t] [e, mkZero t] iTrAp ctx (ICon _ (ICPrim _ PrimULE)) [t] [e, c] | isAlmost c = iTrAp2 ctx iNot [] [iTrApExp ctx icPrimEQ [t] [e, inc c]] iTrAp ctx (ICon _ (ICPrim _ PrimULT)) [t] [e, c] | isAllOnes c = iTrAp2 ctx iNot [] [iTrApExp ctx icPrimEQ [t] [e, c]] iTrAp ctx (ICon _ (ICPrim _ PrimULE)) [_] [_, c] | isAllOnes c = (iTrue, True) -- 0xf < e --> False -- 0xf <= e --> e == 0xf -- 0xe < e --> e == 0xf -- 1 <= e --> e /= 0 -- 0 < e --> e /= 0 -- 0 <= e --> True iTrAp ctx (ICon _ (ICPrim _ PrimULT)) [_] [c, _] | isAllOnes c = (iFalse, True) iTrAp ctx (ICon _ (ICPrim _ PrimULE)) [t] [c, e] | isAllOnes c = iTrAp2 ctx icPrimEQ [t] [e, c] iTrAp ctx (ICon _ (ICPrim _ PrimULT)) [t] [c, e] | isAlmost c = iTrAp2 ctx icPrimEQ [t] [e, inc c] iTrAp ctx (ICon _ (ICPrim _ PrimULE)) [t] [c, e] | isOne c = iTrAp2 ctx iNot [] [iTrApExp ctx icPrimEQ [t] [e, mkZero t]] iTrAp ctx (ICon _ (ICPrim _ PrimULT)) [t] [c, e] | isZero c = iTrAp2 ctx iNot [] [iTrApExp ctx icPrimEQ [t] [e, c]] iTrAp ctx (ICon _ (ICPrim _ PrimULE)) [_] [c, _] | isZero c = (iTrue, True) -- e < 0 (signed) ==> sign-bit -- e <= -1 (signed) ==> sign-bit iTrAp ctx (ICon i (ICPrim _ PrimSLT)) [ITNum n] [e, c] | isZero c = iTrAp2 ctx sel [ITNum 1, ITNum (n - 1), ITNum n] [e] where sel = icSelect (getIdPosition i) iTrAp ctx (ICon i (ICPrim _ PrimSLE)) [ITNum n] [e, c] | isAllOnes c = iTrAp2 ctx sel [ITNum 1, ITNum (n - 1), ITNum n] [e] where sel = icSelect (getIdPosition i) -- Bit fields of size 0 always have the value 0. Proceed accordingly. iTrAp ctx (ICon _ (ICPrim _ p)) [ITNum 0] _ | argRes p = (iMkLitSize 0 0, True) where argRes p = p `elem` [PrimAdd, PrimSub, PrimAnd, PrimOr, PrimXor, PrimInv, PrimNeg] -- shifts take two type arguments (the item size and the index size) iTrAp ctx (ICon _ (ICPrim _ p)) [ITNum 0,_] _ | p `elem` [PrimSL, PrimSRL, PrimSRA] = (iMkLitSize 0 0, True) iTrAp ctx (ICon _ (ICPrim _ PrimMul)) [_,_,ITNum 0] _ = (iMkLitSize 0 0, True) -- PrimMul takes three numeric type arguments iTrAp ctx (ICon _ (ICPrim _ p)) [ITNum 0] _ | eqOp p = (iTrue, True) where eqOp p = p `elem` [PrimEQ, PrimULE, PrimSLE] iTrAp ctx (ICon _ (ICPrim _ p)) [ITNum 0] _ | ltOp p = (iFalse, True) where ltOp p = p `elem` [PrimULT, PrimSLT] iTrAp ctx (ICon _ (ICPrim _ PrimSignExt)) [_, ITNum 0, ITNum s] _ = (iMkLitSize s 0, True) -- --e --> e -- ~~e --> e -- - (if c t e) --> if c (-t) (-e) -- ~ (if c t e) --> if c (~t) (~e) -- ~ (a ++ b) -> (~a) ++ (~b) -- - _ -> _ -- ~ _ -> _ iTrAp ctx cneg@(ICon _ (ICPrim _ p)) [ty] [exp] | p == PrimNeg || p == PrimInv = case expVal exp of IAps cneg2@(ICon _ (ICPrim _ p')) [ty] [e] | p' == p -> (e, True) IAps cif@(ICon _ (ICPrim _ PrimIf)) [tif] [c, t, e] | isIConInt t || isIConInt e -> iTrAp2 ctx cif [tif] [c, iTrApExp ctx cneg [ty] [t], iTrApExp ctx cneg [ty] [e]] IAps ccat@(ICon _ (ICPrim _ PrimConcat)) ts@[l, m, _] [e1, e2] | p == PrimInv -> iTrAp2 ctx ccat ts [iTrApExp ctx cneg [l] [e1], iTrApExp ctx cneg [m] [e2]] u@(ICon i (ICUndet t k Nothing)) -> (u, True) _ -> iTrApTail ctx cneg [ty] [exp] -- e >> n --> 0 ++ select (k-n) n k e iTrAp ctx (ICon srl (ICPrim _ PrimSRL)) [t@(ITNum k), _] [e, ICon _ (ICInt { iVal = IntLit { ilValue = n } })] = let z = iMkLitSize n 0 tt = mkNumConT (k-n) tn = mkNumConT n e' = iTrApExp ctx (icSelect (getIdPosition srl)) [tt, tn, t] [e] in if n >= k then (mkZero t, True) else iTrAp2 ctx icPrimConcat [tn, tt, t] [z, e'] -- e << n --> trunc (e ++ 0) iTrAp ctx (ICon sl (ICPrim _ PrimSL)) [t@(ITNum k), _] [e, ICon _ (ICInt { iVal = IntLit { ilValue = n } })] = let z = iMkLitSize n 0 tt = mkNumConT (k-n) tn = mkNumConT n e' = iTrApExp ctx (icSelect (getIdPosition sl)) [tt, mkNumConT 0, t] [e] in if n >= k then (mkZero t, True) else iTrAp2 ctx icPrimConcat [tt, tn, t] [e', z] -- e :: Bit 1 >> x or e :: Bit 1 << x -> if (x == 0) e else 0 --> (x == 0) && e iTrAp ctx (ICon _ (ICPrim _ p)) [ITNum 1, ITNum t] [e, shft] | p `elem` [PrimSL, PrimSRL] = iTrAp2 ctx icIf [itBit1] [isZero, e, mkZero (ITNum 1)] where isZero = IAps icPrimEQ [ITNum t] [shft, mkZero (ITNum t)] -- e :: Bit 1 >> x (arithmetic) --> e -- we rely on looping to recursively simplify e iTrAp ctx (ICon _ (ICPrim _ PrimSRA)) [ITNum 1, ITNum t] [e, shft] = (e, True) -- Associativity and commutativity (for +, &, |) -- (k1 op (k2 op e)) --> (e op (k1 op k2)) -- (k1 op (e op k2)) --> (e op (k1 op k2)) -- ((e op k1) op k2) --> (e op (k1 op k2)) -- ((k1 op e) op k2) --> (e op (k1 op k2)) iTrAp ctx p@(ICon _ (ICPrim _ prim)) [t] [e1,e2] | prim `elem` [PrimAdd, PrimAnd, PrimOr] && (((isIConInt e1) && (isConstExprForPrim prim e2)) || ((isIConInt e2) && (isConstExprForPrim prim e1))) = iTrAp2 ctx p [t] [e,k] where e = if (isIConInt e1) then (nonConstPart e2) else (nonConstPart e1) k1 = if (isIConInt e1) then e1 else (constPart e1) k2 = if (isIConInt e1) then (constPart e2) else e2 k = case (doPrimOp (getIExprPosition p) prim [t] [k1,k2]) of Just (Right res) -> res _ -> internalError("iTrAp: associativity") -- extract n k e h l --> zeroExt (h-l+1) (k-(h-l+1)) k (select (h-l+1) l n e) iTrAp ctx fun@(ICon iext (ICPrim _ PrimExtract)) ts@[tn@(ITNum n), _, ITNum k] es@[e, eh, el] | isIConInt eh && isIConInt el = -- iTrAp ctx icPrimZeroExt [mkNumConT k_sz, mkNumConT sz, mkNumConT k] [exp] iTrAp2 ctx icPrimConcat [mkNumConT k_sz, mkNumConT sz, mkNumConT k] [iMkLitSize k_sz 0, exp] where exp = iTrApExp ctx (icSelect (getIdPosition iext)) [mkNumConT sz, mkNumConT l, tn] [e] ICon _ (ICInt { iVal = IntLit { ilValue = h } }) = eh ICon _ (ICInt { iVal = IntLit { ilValue = l } }) = el sz = mask 32 (h-l+1) -- mask it to allow h == l-1 k_sz = if k < sz then internalError("extraction size (" ++ show sz ++ ") " ++ "is larger than the expected result (" ++ show k ++ "):\n" ++ ppReadable (IAps fun ts es)) else k - sz -- select n k m e --> error, n+k > m iTrAp ctx fun@(ICon sel (ICPrim _ PrimSelect)) ts@[ITNum n, ITNum k, ITNum m] as | n+k > m = bsErrorUnsafe ?errh [(getIdPosition sel, EBitSel (show n) (show k) (show m) (ppString (IAps fun ts as)))] -- select n ? ? _ --> _ iTrAp ctx (ICon sel (ICPrim _ PrimSelect)) [ITNum n, _, _] [ICon _ (ICUndet { iuKind = u, imVal = Nothing })] = (icUndet (itBitN n) u, True) {- -- XXX join with above conApN _ ctx fun@(ICon isel (ICPrim _ PrimSelect)) args@[T (ITNum k), T (ITNum m), T (ITNum n)] | k > n-m || n-m < 0 = compileError ("conApN select: bad bit selection\n" ++ ppReadable (getIdPosition isel) ++ ppReadable (mkAp fun args)) -} {- -- XXX what's this? iTrAp ctx fun@(ICon iext (ICPrim _ PrimExtract)) args@[T tn, T tk, E e, E eh, E el] | eh == el && isNumConT tk && getNumConT tk == 1 = iTrAp ctx icSelect [T (mkNumConT 1), T (mkNumConT 0), T tn, E exp] where exp = IAps icPrimSRL [tn] [e, el] -} -- x::Bit1 == 1 --> x -- x::Bit1 == 0 --> not x iTrAp ctx e0@(ICon _ (ICPrim _ PrimEQ)) [ITNum 1] [e, ICon _ (ICInt { iVal = IntLit { ilValue = i } })] | i == 0 = iTrAp2 ctx iNot [] [e] | i == 1 = (e, True) | otherwise = internalError ("conApN ==") -- (if b1 then c1 else if b2 then c2 else ... cn) == c --> -- if b1 then (c1 == c) else if b2 then (c2 == c) ... (cn == c) -- (other direction is handled by the flip rule below) -- also can be applied to any op which has a 1-bit result -- (and possibly are heuristics for when it's worth applying to other ops) iTrAp ctx rel_c@(ICon _ (ICPrim _ p)) t1@[ITNum i1] [e', c] | -- app of a 1-bit prim with a single type variable (isIConInt c) && -- c is a constant -- XXX can we include other ops? (p `elem` [PrimEQ, PrimULT, PrimULE, PrimSLT, PrimSLE]) && (isIfElseOfIConInt e') = let ap (IAps i@(ICon _ (ICPrim _ PrimIf)) ts [cnd, thn, els]) = -- the result of the "if" is now 1-bit (IAps i [itBit1] [cnd, ap thn, ap els]) ap (ICon _ (ICValue { iValDef = e })) = ap e ap e = iTrApExp ctx rel_c t1 [e, c] in (ap e', True) -- c RELOP x --> x (flip RELOP) c iTrAp ctx e0@(ICon _ (ICPrim _ p)) [t] [e1, e2] | isJust mfp && isIConInt e1 && not (isIConInt e2) = fp [t] [e2, e1] where mfp = flipOp p Just fp = mfp flipOp PrimEQ = Just $ \ ts es -> iTrAp2 ctx icPrimEQ ts es flipOp PrimULT = Just $ \ ts es -> iTrAp2 ctx iNot [] [iTrApExp ctx icPrimULE ts es] flipOp PrimULE = Just $ \ ts es -> iTrAp2 ctx iNot [] [iTrApExp ctx icPrimULT ts es] flipOp PrimSLT = Just $ \ ts es -> iTrAp2 ctx iNot [] [iTrApExp ctx icPrimSLE ts es] flipOp PrimSLE = Just $ \ ts es -> iTrAp2 ctx iNot [] [iTrApExp ctx icPrimSLT ts es] flipOp _ = Nothing iTrAp ctx p@(ICon _ (ICPrim _ PrimConcat)) ts@[s1@(ITNum i1), s2@(ITNum i2), s3@(ITNum i3)] as@[e1, e2] = case map expValConcat as of -- ignore 0 sized args _ | i1 == 0 -> (e2, True) _ | i2 == 0 -> (e1, True) -- _ ++ _ --> _ [ICon _ (ICUndet { imVal = Nothing }), ICon _ (ICUndet { iuKind = u, imVal = Nothing })] -> (icUndet (aitBit s3) u, True) -- c1 ++ (c2 ++ e) --> (c1++c2) ++ e [ICon _ (ICInt { iVal = IntLit { ilValue = c1 } }), IAps (ICon _ (ICPrim _ PrimConcat)) [ITNum isc2, se, _] [ICon _ (ICInt { iVal = IntLit { ilValue = c2 } }), e]] -> iTrAp2 ctx p [mkNumConT isc1c2, se, s3] [iMkLitSize isc1c2 (c1 * 2^isc2 + c2), e] where isc1c2 = i1 + isc2 -- select ? ? ? e1 ++ (select ? ? ? e1 ++ e2) --> (select ? ? ? e1 ++ select ? ? ? e1) ++ e2 -- enables next transform [x1@(IAps ps@(ICon _ (ICPrim _ PrimSelect)) _ [e1]), -- size l (IAps pc@(ICon _ (ICPrim _ PrimConcat)) [s2s@(ITNum s2i), e2s, _] [x2@(IAps (ICon _ (ICPrim _ PrimSelect)) _ [e1']), e2])] | e1 == e1' -> iTrAp2 ctx pc [s12s, e2s, s3] [ss, e2] where ss = iTrApExp ctx pc [s1,s2s,s12s] [x1, x2] s12s = mkNumConT (i1 + s2i) -- select l (m+k) n e ++ select k m n e --> select (l+k) m n e [IAps p@(ICon _ (ICPrim _ PrimSelect)) [ITNum il', ITNum imk, n] [e], IAps (ICon _ (ICPrim _ PrimSelect)) [ITNum ik', m@(ITNum im), n'] [e']] | i1 == il' && i2 == ik' && n == n' && eqE e e' && i3 == i1 + i2 && imk == im + i2 -> iTrAp2 ctx p [s3, m, n] [e] -- (e1 ++ select l (m+k) n e2) ++ select k m n e2 -> (e1 ++ select (l+k) m n e) [x1@(IAps pc@(ICon _ (ICPrim _ PrimConcat)) [e1s@(ITNum e1i), sel1s@(ITNum sel1i), _] [e1, sel1@(IAps (ICon _ (ICPrim _ PrimSelect)) [ITNum il', ITNum imk, n] [e2])]), sel2@(IAps ps@(ICon _ (ICPrim _ PrimSelect)) [ITNum ik', m@(ITNum im), n'] [e2'])] | sel1i == il' && i2 == ik' && n == n' && eqE e2 e2' && i3 == i1 + i2 && imk == im + i2 -> iTrAp2 ctx pc [e1s, s12s, s3] [e1, ss] where ss = iTrApExp ctx pc [sel1s,s2,s12s] [sel1, sel2] s12s = mkNumConT (sel1i + i2) -- _ ++ select k m n e --> select (l+k) m n e IF n-m >= l+k -- _ ++ select k m n e --> _ ++ select (n-m) m n e IF n-m < l+k [ICon _ (ICUndet { iuKind = u, imVal = Nothing }), IAps ps@(ICon _ (ICPrim _ PrimSelect)) [ITNum ik', m@(ITNum im), n@(ITNum inn)] [e]] | i2 == ik' && d /= i1 -> --trace ("_ ++ sel\n" ++ ppReadable (mkAp p as)) $ if d <= 0 then iTrAp2 ctx ps [s3, m, n] [e] else iTrAp2 ctx p [mkNumConT d, tnm, s3] [icUndet (itBitN d) u, iTrApExp ctx ps [tnm, m, n] [e]] where nm = inn - im d = i3 - nm tnm = mkNumConT nm -- select k m n e ++ _ --> select (l+k) (m-l) n e IF m >= l -- select k m n e ++ _ --> select (m+k) 0 n e ++ _ [IAps ps@(ICon _ (ICPrim _ PrimSelect)) [ITNum ik', m@(ITNum im), n@(ITNum inn)] [e], ICon _ (ICUndet { iuKind = u, imVal = Nothing })] | i1 == ik' && (im >= i2 || d /= i2) -> --trace ("sel ++ _\n" ++ ppReadable (mkAp p as, im, i2)) $ if im >= i2 then iTrAp2 ctx ps [s3, mkNumConT (im-i2), n] [e] else iTrAp2 ctx p [tmk, mkNumConT d, s3] [iTrApExp ctx ps [tmk, ITNum 0, n] [e], icUndet (itBitN d) u] where tmk = mkNumConT (im+i1) d = i3 - (im+i1) -- (if c t0 e0) ++ (if c t1 e1) --> if c (t0 ++ t1) (e0 ++ e1) [IAps pif@(ICon _ (ICPrim _ PrimIf)) _ [cnd0, t0, e0], IAps (ICon _ (ICPrim _ PrimIf)) _ [cnd1, t1, e1]] | cnd0 == cnd1 -> iTrAp2 ctx pif [itBitN i3] [cnd0, t', e'] where t' = iTrApExp ctx p ts [t0, t1] e' = iTrApExp ctx p ts [e0, e1] -- (if c thn _) ++ e --> thn ++ e [IAps (ICon _ (ICPrim _ PrimIf)) _ [_, thn, els], e] | isUndet thn && noRefs els -> iTrAp2 ctx p ts [els, e] | isUndet els && noRefs thn -> iTrAp2 ctx p ts [thn, e] -- e ++ (if c thn _) --> e ++ thn [e, IAps (ICon _ (ICPrim _ PrimIf)) _ [_, thn, els]] | isUndet thn && noRefs els -> iTrAp2 ctx p ts [e, els] | isUndet els && noRefs thn -> iTrAp2 ctx p ts [e, thn] _ -> iTrApTail ctx p ts as iTrAp ctx ps@(ICon _ (ICPrim _ PrimSelect)) ts@[k@(ITNum ik), m@(ITNum im), n] [e] = case expVal e of -- select k m n (select n p q e) --> select k (m+p) q e IAps (ICon _ (ICPrim _ PrimSelect)) [n', ITNum ip, q] [e] | n == n' -> iTrAp2 ctx ps [k, mkNumConT (im+ip), q] [e] -- select k 0 n (e1 ++ e2) --> select (k-l2) 0 l1 e1 ++ e2 IF k >= l2 IAps pc@(ICon _ (ICPrim _ PrimConcat)) [l1, l2@(ITNum il2), n'] [e1, e2] | n == n' && im == 0 && ik >= il2 -> iTrAp2 ctx pc [mkNumConT j, l2, k] [sel, e2] where j = ik - il2 sel = iTrApExp ctx ps [mkNumConT j, m, l1] [e1] -- select k m n (e1 ++ e2) --> select k m l2 e2 IF k+m <= l2 -- --> select k (m-l2) l1 e1 IF m >= l2 -- otherwise --> select (k + m - l2) 0 l1 e1 ++ select (l2 - m) m l2 e2 IAps pc@(ICon _ (ICPrim _ PrimConcat)) [l1, l2@(ITNum il2), n'] [e1, e2] | n == n' -> if im >= il2 then iTrAp2 ctx ps [k, mkNumConT (im - il2), l1] [e1] else if (ik + im <= il2) then iTrAp2 ctx ps [k, m, l2] [e2] else iTrAp2 ctx pc [mkNumConT l1', mkNumConT l2', k] [e1', e2'] where e1' = iTrApExp ctx ps [mkNumConT l1', mkNumConT 0, l1] [e1] l1' = ik + im - il2 e2' = iTrApExp ctx ps [mkNumConT l2', m, l2] [e2] l2' = il2 - im {- Disable this fix for bug 1429 because it causes problems with the bug 1490 situation. -- select k m n (if c t e) --> if c (select k m n t) (select k m n e) IAps pif@(ICon _ (ICPrim _ PrimIf)) _ [cnd,thn,els] -> iTrAp2 ctx pif [itBitN ik] [cnd, thn', els'] where thn' = iTrApExp ctx ps ts [thn] els' = iTrApExp ctx ps ts [els] -} _ -> iTrApTail ctx ps ts [e] -- (e1 ++ 0) + (e2 ++ e3) --> (e1+e2) ++ e3 -- XXX only special case so far iTrAp ctx op@(ICon _ (ICPrim _ PrimAdd)) ts as = case map expVal as of [ICon _ (ICInt { iVal = IntLit { ilValue = c } } ), IAps co@(ICon _ (ICPrim _ PrimConcat)) [t1, t2@(ITNum it2), t3] [ICon _ (ICInt { iVal = IntLit { ilValue = c2 } }), e] ] | r == 0 -> iTrAp2 ctx co [t1, t2, t3] [iMkLit (aitBit t1) (q+c2), e] where (q,r) = quotRem c (2^it2) [IAps co@(ICon _ (ICPrim _ PrimConcat)) [t1, t2@(ITNum it2), t3] [e, ICon _ (ICInt { iVal = IntLit { ilValue = 0 } })], ICon _ (ICInt { iVal = IntLit { ilValue = c } } ) ] | q == 0 -> iTrAp2 ctx co [t1, t2, t3] [e, iMkLit (aitBit t2) r] where (q,r) = quotRem c (2^it2) _ -> iTrApTail ctx op ts as -- (e1 ++ e2) `op` (e3 ++ e4) --> (e1 `op` e3) ++ (e2 `op` e4) -- ((e1 ++ e1') ++ e2) `op` (e3 ++ c) --> ((e1 ++ e1') ++ e2) `op` ((e3 ++ c1) ++ c2) -- this doesn't improve things on its own, but can open up other transformations iTrAp ctx op@(ICon _ (ICPrim _ p)) [t@(ITNum it)] as | p `elem` [PrimAnd, PrimOr, PrimXor] = let default_res = iTrApTail ctx op [t] as applyOp (sz, eA, eB) = (sz, iTrApExp ctx op [ITNum sz] [eA, eB]) concatFn (sz, expr) (sz_so_far, expr_so_far) = let sz_total = sz_so_far + sz in (sz_total, iTrApExp ctx icPrimConcat [ITNum sz, ITNum sz_so_far, ITNum sz_total] [expr, expr_so_far]) in case map expVal as of [e1, e2] -> case (findConcatBreaks it e1 e2) of [] -> internalError "iTrAp: findConcatBreaks" [_] -> -- no progress made, so leave as is default_res ps -> let res = snd $ foldr1 concatFn (map applyOp ps) in -- indicate that a transform occurred (res, True) _ -> -- can this happen? default_res -- signExt n n e --> e iTrAp ctx (ICon _ (ICPrim _ PrimSignExt)) [_, t1, t2] [e] | t1 == t2 = (e, True) -- constant folding iTrAp ctx c@(ICon _ (ICPrim _ p)) ts as | canDoOp = (e, True) where (canDoOp, e) = case (doPrimOp (getIExprPosition c) p ts as) of Just (Right res) -> (True, res) _ -> (False, internalError("iTrAp: ICPrim")) iTrAp ctx f ts es = iTrApTail ctx f ts es -- constant folding iTrApTail :: Ctx a -> IExpr a -> [IType] -> [IExpr a] -> (IExpr a, Bool) iTrApTail ctx c@(ICon _ (ICPrim _ p)) ts as | canDoOp = (e, True) where (canDoOp, e) = case (doPrimOp (getIExprPosition c) p ts as) of Just (Right res) -> (True, res) _ -> (False, internalError("iTrapTail: ICPrim")) iTrApTail ctx f ts es = (IAps f ts es, False) expVal :: IExpr a -> IExpr a expVal (ICon _ (ICValue { iValDef = e })) = e expVal e = e -- Like expVal but expands concats one level deeper, so that -- the patterns can match things like ((a ++ (select..)) ++ (select..)) expValConcat :: IExpr a -> IExpr a expValConcat (ICon _ (ICValue { iValDef = e })) = expValConcat e expValConcat (IAps p@(ICon _ (ICPrim _ PrimConcat)) ts es) = IAps p ts (map expVal es) expValConcat e = e ------------------------- findConcatBreaks :: Integer -> IExpr a -> IExpr a -> [(Integer, IExpr a, IExpr a)] findConcatBreaks sz eA@(IAps (ICon _ (ICPrim _ PrimConcat)) [ITNum itA1, ITNum itA2, ITNum itA3] [eA1, eA2]) eB = case (splitConstExpr itA1 itA2 eB) of Nothing -> [(sz, eA, eB)] Just (eB1, eB2) -> findConcatBreaks itA1 eA1 eB1 ++ findConcatBreaks itA2 eA2 eB2 findConcatBreaks sz eA eB@(IAps (ICon _ (ICPrim _ PrimConcat)) [ITNum itB1, ITNum itB2, ITNum itB3] [eB1, eB2]) = case (splitConstExpr itB1 itB2 eA) of Nothing -> [(sz, eA, eB)] Just (eA1, eA2) -> findConcatBreaks itB1 eA1 eB1 ++ findConcatBreaks itB2 eA2 eB2 findConcatBreaks sz eA eB = [(sz, eA, eB)] splitConstExpr :: Integer -> Integer -> IExpr a -> Maybe (IExpr a, IExpr a) splitConstExpr n n2 (ICon _ ic@(ICInt { iVal = IntLit { ilValue = c } })) = let c1 = iMkLit (aitBit (mkNumConT n)) (c `div` 2^n2) c2 = iMkLit (aitBit (mkNumConT n2)) (mask n2 c) in Just (c1, c2) splitConstExpr n n2 (ICon _ (ICUndet { iuKind = u, imVal = Nothing })) = let u1 = icUndet (aitBit (mkNumConT n)) u u2 = icUndet (aitBit (mkNumConT n2)) u in Just (u1, u2) splitConstExpr n n2 e@(IAps (ICon _ (ICPrim _ PrimConcat)) [(ITNum it1), (ITNum it2), (ITNum it3)] [e1, e2]) = case (compare n it1) of EQ -> Just (e1, e2) LT -> let n2' = it1 - n in case (splitConstExpr n n2' e1) of Nothing -> Nothing Just (e1A, e1B) -> let t1' = ITNum n2' -- (it1 - n) t2' = ITNum it2 -- (n2 + n - it1) t3' = ITNum (it3 - n) -- n2 rest = IAps icPrimConcat [t1', t2', t3'] [e1B, e2] in Just (e1A, rest) GT -> let n' = n - it1 in case (splitConstExpr n' n2 e2) of Nothing -> Nothing Just (e2A, e2B) -> let t1' = ITNum it1 t2' = ITNum n' -- (n - it1) t3' = ITNum n -- (it3 - n2) rest = IAps icPrimConcat [t1', t2', t3'] [e1, e2A] in Just (rest, e2B) -- Nothing else is considered a splittable expression splitConstExpr _ _ _ = Nothing ----------------------------------------------------------------------------- addT :: IExpr a -> Ctx a -> Ctx a addT e ctx = --trace ("addT\n" ++ ppReadable (e, ctx, addT' (expValAndOrCmp e) ctx)) $ addT' (expValAndOrCmp e) ctx where addT' e (Ctx vs be) = Ctx (addEqs e vs) (bAdd e be) addEqs (IAps (ICon _ (ICPrim _ PrimEQ)) _ [i, ICon _ (ICInt { iVal = IntLit { ilValue = v } })]) vs = M.insert i v vs -- XXX case for when the const is on the left? -- XXX case for (e1 == e2), when e1 or e2 exists in the set, add the other as the same val addEqs (IAps (ICon _ (ICPrim _ PrimBAnd)) _ [e1, e2]) vs = addEqs e1 (addEqs e2 vs) addEqs (IAps (ICon _ (ICPrim _ PrimBNot)) _ [e]) vs = addNEqs e vs addEqs _ vs = vs -- XXX case for != ? addNEqs (IAps (ICon _ (ICPrim _ PrimBOr)) _ [e1, e2]) vs = addNEqs e1 (addNEqs e2 vs) addNEqs (IAps (ICon _ (ICPrim _ PrimBNot)) _ [e]) vs = addEqs e vs addNEqs _ vs = vs addF :: IExpr a -> Ctx a -> Ctx a addF e ctx = addT (ieNot e) ctx expValAndOrCmp :: IExpr a -> IExpr a expValAndOrCmp (IAps e ts es) = IAps e ts (map expValAndOrCmp es) expValAndOrCmp (ICon _ (ICValue { iValDef = e@(IAps (ICon _ (ICPrim _ p)) _ _ )})) | isAndOrCmp p = expValAndOrCmp e expValAndOrCmp e = e isAndOrCmp :: PrimOp -> Bool isAndOrCmp p = p `elem` [PrimBAnd, PrimBOr, PrimBNot, PrimEQ, PrimULT, PrimULE, PrimSLT, PrimSLE] expValShallow :: IExpr a -> IExpr a expValShallow (IAps e ts es) = IAps e ts (map expValShallow es) expValShallow (ICon _ (ICValue { iValDef = e@(IAps (ICon _ (ICPrim _ p)) _ _ )})) | p == PrimBNot = expValShallow e | isAndOrCmp p = e expValShallow e = e {- expValAndOr :: IExpr a -> IExpr a expValAndOr (IAps e ts es) = IAps e ts (map expValAndOr es) expValAndOr (ICon _ (ICValue { iValDef = e@(IAps (ICon _ (ICPrim _ p)) _ _ )})) | isAndOr p = expValAndOr e where isAndOr p = p `elem` [PrimBAnd, PrimBOr, PrimBNot] expValAndOr e = e -} isT :: Ctx a -> IExpr a -> Bool isT ctx@(Ctx vs be) e = --traces ("isT\n" ++ ppReadable (e, expValAndOrCmp e, ctx, isT' (expValAndOrCmp e))) $ isT' (expValAndOrCmp e) where isT' e = bImplies be e || case e of IAps (ICon _ (ICPrim _ PrimEQ)) _ [i, ICon _ (ICInt { iVal = IntLit { ilValue = v } })] -> -- traces ("isT EQ" ++ ppReadable (i, v, M.toList vs)) $ case M.lookup i vs of Just k -> v == k Nothing -> False IAps (ICon _ (ICPrim _ PrimBNot)) _ [IAps (ICon _ (ICPrim _ PrimEQ)) _ [i, ICon _ (ICInt { iVal = IntLit { ilValue = v } })]] -> -- traces ("isT NE" ++ ppReadable (i, v, M.toList vs)) $ case M.lookup i vs of Just k -> v /= k Nothing -> False _ -> False isF :: Ctx a -> IExpr a -> Bool isF ctx@(Ctx vs be) e = --traces ("isF\n" ++ ppReadable (e, expValAndOrCmp e, ctx, isF' (expValAndOrCmp e))) $ isF' (expValAndOrCmp e) where isF' e = bImplies be (ieNot e) || case e of IAps (ICon _ (ICPrim _ PrimEQ)) _ [i, ICon _ (ICInt { iVal = IntLit { ilValue = v } })] -> case M.lookup i vs of Just k -> v /= k Nothing -> False IAps (ICon _ (ICPrim _ PrimBNot)) _ [IAps (ICon _ (ICPrim _ PrimEQ)) _ [i, ICon _ (ICInt { iVal = IntLit { ilValue = v } })]] -> case M.lookup i vs of Just k -> v == k Nothing -> False _ -> False {- isT :: Ctx a -> IExpr a -> Bool isT _ (ICon _ (ICInt { iVal = IntLit { ilValue = 1 } })) = True isT _ _ = False isF :: Ctx a -> IExpr a -> Bool isF _ (ICon _ (ICInt { iVal = IntLit { ilValue = 0 } })) = True isF _ _ = False -} -- a --> b implies :: Ctx a -> IExpr a -> IExpr a -> Bool implies ctx a b = isT (addT a ctx) b -- ~a --> b notimplies :: Ctx a -> IExpr a -> IExpr a -> Bool notimplies ctx a b = isT (addF a ctx) b -- a --> ~b impliesnot :: Ctx a -> IExpr a -> IExpr a -> Bool impliesnot ctx a b = isF (addT a ctx) b ----------------------------------------------------------------------------- -- The BExpr is a formula of what we know is true data Ctx a = Ctx (M.Map (IExpr a) IValue) (BExpr a) type IValue = Integer emptyCtx :: Ctx a emptyCtx = Ctx M.empty bNothing instance PPrint (Ctx a) where pPrint d p (Ctx es be) = (text "Ctx " $+$ text " ") <> (pPrint d 0 (M.toList es) $+$ pPrint d 0 be) {- bSetLess :: Ctx a -> Ctx a -> Bool bSetLess (Ctx sm e) (Ctx sm' e') = isOrdSubset (M.toList sm) (M.toList sm') && bImpliesB e' e -} ----------------------------------------------------------------------------- data MaskTail = Zeroes Integer | Ones Integer -- this is fast because the GHC libraries (i.e. GMP) do a good job here getMaskTail :: Integer -> Integer -> MaskTail getMaskTail mask size | zeroes_gcd > 1 = let result = log2 zeroes_gcd in if (result > size) then internalError("ITransform.getMaskTail: " ++ ppReadable(mask, size, zeroes_gcd, result)) else Zeroes result | ones_gcd > 1 = let result = log2 ones_gcd in if (result > size) then internalError("ITransform.getMaskTail: " ++ ppReadable(mask, size, ones_gcd, result)) else Ones result | otherwise = internalError ("ITransform.getMaskTail: " ++ ppReadable (mask, size)) where zeroes_gcd = gcd mask power ones_gcd = gcd (mask+1) power power = 2^size isZero :: IExpr a -> Bool isZero (ICon _ (ICInt { iVal = IntLit { ilValue = 0 } })) = True isZero _ = False isOne :: IExpr a -> Bool isOne (ICon _ (ICInt { iVal = IntLit { ilValue = 1 } })) = True isOne _ = False isAllOnes :: IExpr a -> Bool isAllOnes (ICon _ (ICInt { iConType = ITAp b (ITNum i), iVal = IntLit { ilValue = n } })) = b == itBit && 2^i == n+1 isAllOnes _ = False isAlmost :: IExpr a -> Bool isAlmost (ICon _ (ICInt { iConType = ITAp b (ITNum i), iVal = IntLit { ilValue = n } })) = b == itBit && 2^i == n+2 isAlmost _ = False iLog2 :: Integer -> Maybe Integer iLog2 i = if i > 0 && (i `integerAnd` (i-1)) == 0 then Just (log2 i) else Nothing inc :: IExpr a -> IExpr a inc (ICon i c@(ICInt { iVal = il@(IntLit { ilValue = n }) })) = -- GHC emits a warning below because it's forgotten that 'c' must be -- an ICInt ICon i (c { iVal = il { ilValue = n+1 } }) inc iexpr = internalError ("ITransform.inc: " ++ ppString iexpr) mkZero :: IType -> IExpr a mkZero t = iMkLit (aitBit t) 0 -- only match non-chosen undefined values isUndet :: IExpr a -> Bool isUndet (ICon _ (ICUndet { imVal = Nothing })) = True isUndet _ = False -- Guard optimizations that are not valid in the presence of implicit conditions. noRefs :: IExpr a -> Bool noRefs (IRefT {}) = False noRefs (IAps f _ es) = all noRefs (f:es) noRefs _ = True isIfElseOfIConInt :: IExpr a -> Bool isIfElseOfIConInt (IAps (ICon _ (ICPrim _ PrimIf)) [t] [cnd, thn, els]) = isIfElseOfIConInt' thn && isIfElseOfIConInt' els where isIfElseOfIConInt' (IAps (ICon _ (ICPrim _ PrimIf)) [t] [cnd, thn, els]) = isIfElseOfIConInt' thn && isIfElseOfIConInt' els isIfElseOfIConInt' (ICon _ (ICValue { iValDef = e })) = isIfElseOfIConInt' e isIfElseOfIConInt' e = isIConInt e || isUndet e isIfElseOfIConInt (ICon _ (ICValue { iValDef = e })) = isIfElseOfIConInt e isIfElseOfIConInt _ = False isConstExprForPrim :: PrimOp -> IExpr a -> Bool isConstExprForPrim prim (IAps (ICon _ (ICPrim _ p)) _ [e1,e2]) = (p == prim) && ((isIConInt e1) || (isIConInt e2)) isConstExprForPrim _ _ = False constPart :: IExpr a -> IExpr a constPart (IAps (ICon _ (ICPrim _ p)) _ [e1,e2]) | isIConInt e1 = e1 | isIConInt e2 = e2 | otherwise = internalError "constPart: no const part found!" constPart _ = internalError "constPart: expected a binary primitive op" nonConstPart :: IExpr a -> IExpr a nonConstPart (IAps (ICon _ (ICPrim _ p)) _ [e1,e2]) = if (isIConInt e1) then e2 else e1 -- note: e2 may also be a constant! nonConstPart _ = internalError "nonConstPart: expected a binary primitive op" -- More accurate (and faster) equality by ignoring ICValue eqE :: IExpr a -> IExpr a -> Bool eqE (IAps e1 ts1 es1) (IAps e2 ts2 es2) = eqE e1 e2 && ts1 == ts2 && and (zipWith eqE es1 es2) eqE (ICon i1 (ICValue { iValDef = e1 })) (ICon i2 (ICValue { iValDef = e2 })) = i1 == i2 eqE (ICon _ (ICValue { iValDef = e1 })) e2 = eqE e1 e2 eqE e1 (ICon _ (ICValue { iValDef = e2 })) = eqE e1 e2 eqE e1 e2 = e1 == e2 ----------------------------------------------------------------------------- data TState a = TState { errHandle :: ErrorHandle, flags :: Flags, -- Prefix to use for generating new names (resulting from CSE) prefix :: String, -- Source of unique numbers to append to generated names idNo :: Integer, -- A map of package defs. When ICValue is encountered, the def is -- looked up in this map and the assigned expression is inlined. -- The defprops are kept to be used in the fixup step that happens -- between processing defs and processing the rest of the module. def_map :: M.Map Id (IType, IExpr a, [DefProp]), -- A CSE map, from an expr "e" to a tuple of info for the canonical -- def ("defname") to represent it: -- * an expr to use to refer to the def ("ICValue defname") -- * the def ("IDef defname deftype e") -- When the monad is run, because all exprs are inlined and then CSE'd -- back up, the defs for the package will come from this map. cse_map :: M.Map (IExpr a) (IExpr a, IDef a) } type T b a = State (TState a) b runT :: ErrorHandle -> Flags -> Integer -> String -> T b a -> (b, [IDef a]) runT errh flags no prefix xforms = let initState :: TState a initState = TState { errHandle = errh , flags = flags , prefix = prefix , idNo = no , def_map = M.empty , cse_map = M.empty } in case runState xforms initState of (x, ts) -> let defs_from_cse = map (snd . snd) (M.toList (cse_map ts)) non_cse_defs = [ IDef i t e props | (i, (t, e, props)) <- M.toList (def_map ts) , defPropsHasNoCSE props ] defs = defs_from_cse ++ non_cse_defs in (x, defs) getDoBO :: T Bool a getDoBO = do flgs <- gets flags return (optBool flgs) -- Create a CSE def for an expression, returning a reference; -- if a def already exists for this expression, return the existing reference. newExprT :: IType -> IExpr a -> T (IExpr a) a newExprT t e = do ts <- get cmap <- gets cse_map case (M.lookup e cmap) of Just (e', _) -> return e' Nothing -> do n <- gets idNo let i = setBadId $ mkId noPosition (mkFString ((prefix ts) ++ itos n)) e' = ICon i (ICValue t e) d = IDef i t e [] -- props get lost here, but restored in iTransRenameIdsInDef put $ ts { idNo = n+1, cse_map = M.insert e (e', d) cmap } -- traceM ("newExprT " ++ ppString e ++ " -> " ++ ppString (e',d)) return e' addDefT :: Id -> IType -> IExpr a -> [DefProp] -> T () a addDefT i t e p = do -- traceM $ "addDefT " ++ ppString i ++ " " ++ ppString e ts <- get put $ ts {def_map = M.insert i (t,e,p) (def_map ts) } getDefT :: Id -> T (Maybe (IExpr a)) a getDefT i = get >>= (return . fmap snd3 . M.lookup i . def_map) {- we don't need uEq because we use a progress check instead now -- the uEq check is tuned to what we need to do to fix -- concats including undefined values correctly -- things are uEq if: -- - they are directly equal -- - they are equal if you expand chosen undefined values -- - where they are not equal one part is an unchosed undefined value -- as in eqE, we don't go inside ICValue when the names are equal -- this avoids some stack overflows and other nastiness uEq :: IExpr a -> IExpr a -> Bool uEq e1 e2 = {- trace ("uEq: " ++ ppReadable (e1, e2)) $ -} uEq' e1 e2 uEq' (ICon _ (ICUndet { imVal = Nothing })) e = True uEq' e (ICon _ (ICUndet { imVal = Nothing })) = True uEq' e1 (ICon _ (ICUndet { imVal = Just e2 })) = uEq e1 e2 uEq' (ICon _ (ICUndet { imVal = Just e1 })) e2 = uEq e1 e2 uEq' (ICon i1 (ICValue { })) (ICon i2 (ICValue { })) = i1 == i2 uEq' (ICon _ (ICValue _ e1)) e2 = uEq e1 e2 uEq' e1 (ICon _ (ICValue _ e2)) = uEq e1 e2 uEq' (IAps (ICon _ (ICPrim _ PrimIf)) _ [c1,t1,e1]) (IAps (ICon _ (ICPrim _ PrimIf)) _ [c2,t2,e2]) = (c1 `eqE` c2 && t1 `uEq` t2 && e1 `uEq` e2) || (t1 `uEq` e1 && t2 `uEq` e2 && t1 `uEq` t2) uEq' (IAps (ICon _ (ICPrim _ PrimIf)) _ [_,t1,e1]) e2 = t1 `uEq` e2 && e1 `uEq` e2 uEq' e1 (IAps (ICon _ (ICPrim _ PrimIf)) _ [_,t2,e2]) = e1 `uEq` t2 && e1 `uEq` e2 uEq' e1 e2 = e1 == e2 -} ----------------------------------------------------------------------------- optBoolExpr :: Bool -> IExpr a -> IExpr a optBoolExpr moreBoolOpt = optBoolExprN 8 moreBoolOpt optBoolExprN :: Int -> Bool -> IExpr a -> IExpr a optBoolExprN nvars moreBoolOpt = fromBE . (if moreBoolOpt then tryHard nvars else sSimplify) . toBE . (if moreBoolOpt then aOptCmp else sOptCmp) . expValAndOrCmp tryHard :: Int -> BoolExp (IExpr a) -> BoolExp (IExpr a) tryHard nvars e = case optBoolExprQM nvars e of -- Don't try more than 8 variables. Nothing -> {-trace ("tryHard too big " ++ ppReadable e) $ -} aSimplify e Just e' -> {-trace (ppReadable(e, e')) -} e' fromBE :: BoolExp (IExpr a) -> IExpr a fromBE (And e1 e2) = ieAnd (fromBE e1) (fromBE e2) fromBE (Or e1 e2) = ieOr (fromBE e1) (fromBE e2) fromBE (Not e) = ieNot (fromBE e) fromBE (If e1 e2 e3) = ieIf itBit1 (fromBE e1) (fromBE e2) (fromBE e3) fromBE (Var e) = e fromBE TT = iTrue fromBE FF = iFalse toBE :: IExpr a -> BoolExp (IExpr a) toBE (IAps (ICon _ (ICPrim _ PrimBAnd)) _ [e1, e2]) = And (toBE e1) (toBE e2) toBE (IAps (ICon _ (ICPrim _ PrimBOr)) _ [e1, e2]) = Or (toBE e1) (toBE e2) toBE (IAps (ICon _ (ICPrim _ PrimBNot)) _ [e]) = Not (toBE e) toBE (IAps (ICon _ (ICPrim _ PrimIf)) _ [e1,e2,e3]) = If (toBE e1) (toBE e2) (toBE e3) toBE e | e == iTrue = TT | e == iFalse = FF | otherwise = Var e -- A quick hack for optimizing comparisons sOptCmp :: IExpr a -> IExpr a sOptCmp e = let collEQs (IAps (ICon _ (ICPrim _ PrimBAnd)) _ [e1, e2]) = collEQs e1 ++ collEQs e2 collEQs (IAps (ICon _ (ICPrim _ PrimEQ)) _ [v, ICon _ (ICInt { iVal = IntLit { ilValue = i } })]) = [(v, i)] collEQs _ = [] remNE vcs e@(IAps (ICon _ (ICPrim _ PrimEQ)) _ [v, ICon _ (ICInt { iVal = IntLit { ilValue = i } })]) = case lookup v vcs of Just i' | i /= i' -> iFalse _ -> e remNE vcs (IAps f ts es) = IAps f ts (map (remNE vcs) es) remNE vcs e = e collTerms (IAps (ICon _ (ICPrim _ PrimBAnd)) _ [e1, e2]) = collTerms e1 ++ collTerms e2 collTerms e = [e] remAbsurd e (IAps (ICon _ (ICPrim _ PrimBNot)) _ [IAps (ICon _ (ICPrim _ PrimEQ)) _ [v, ICon _ (ICInt { iConType = ITAp bit (ITNum vn), iVal = IntLit { ilValue = i } })]] : es) | bit == itBit && vn <= 8 = loop ([0..2^vn-1] \\ [i]) es where loop [] [] = iFalse loop _ [] = e loop is (IAps (ICon _ (ICPrim _ PrimBNot)) _ [IAps (ICon _ (ICPrim _ PrimEQ)) _ [v', ICon _ (ICInt { iVal = IntLit { ilValue = i } })]] : es) | v == v' = loop (is \\ [i]) es loop is (_:es) = loop is es remAbsurd e (_:es) = remAbsurd e es remAbsurd e [] = e remAbs e = remAbsurd e (collTerms e) in remAbs (remNE (collEQs e) e) aOptCmp :: IExpr a -> IExpr a aOptCmp e = --trace ("optCmp:\n" ++ ppReadable e) $ let (_, e') = optE M.empty e in --(if e/=e' then traces (ppReadable (e, e')) else id) e' optE :: ValMap a -> IExpr a -> (ValMap a, IExpr a) optE m e0@(IAps p@(ICon _ (ICPrim _ PrimBAnd)) ts [e1, e2]) = -- XXX this can't be the best way let (m1, e2') = optE m e2 (m2, e1') = optE m1 e1 in if e1 /= e1' then (m2, IAps p ts [e1', e2']) else let (m1, e1') = optE m e1 (m2, e2') = optE m1 e2 in (m2, IAps p ts [e1', e2']) optE m e@(IAps p@(ICon _ (ICPrim _ cmp)) _ [v, ICon _ (ICInt { iConType = t, iVal = IntLit { ilValue = i } })]) | isCmp cmp && mn /= Nothing = doCmp m e cmp v n i True where mn = getBit t Just n = mn optE m e@(IAps (ICon _ (ICPrim _ PrimBNot)) _ [IAps p@(ICon _ (ICPrim _ cmp)) ts [v, ICon _ (ICInt { iConType = t, iVal = IntLit { ilValue = i } })]]) | isCmp cmp && mn /= Nothing = doCmp m e cmp v n i False where mn = getBit t Just n = mn optE m e = case vsGetSingleton e m of Nothing -> (m, e) Just i -> (m, iMkLit (iGetType e) i) type ValMap a = M.Map (IExpr a) ValueSet vmAdd :: IExpr a -> ValueSet -> ValMap a -> ValMap a vmAdd k vs m = M.insert k vs m vmGet :: IExpr a -> ValMap a -> ValueSet vmGet v m = case M.lookup v m of Just vs -> vs Nothing -> vsUniv v --- type ValueSet = VSetInteger vsUniv :: IExpr a -> ValueSet vsUniv (ICon i (ICValue { iValDef = IAps (ICon _ (ICPrim _ PrimRange)) _ [ICon _ (ICInt { iVal = IntLit { ilValue = lo } }), ICon _ (ICInt { iVal = IntLit { ilValue = hi } }), _] })) = --traces ("interval " ++ ppReadable (i,lo,hi)) $ vFromTo lo hi vsUniv e = --traces ("nointerval " ++ ppReadable e) $ case getBit (iGetType e) of Just n -> vFromTo 0 (2^n-1) Nothing -> internalError "vsUniv" vsGetSingleton :: IExpr a -> ValMap a -> Maybe Integer vsGetSingleton e m = M.lookup e m >>= vGetSing isCmp :: PrimOp -> Bool isCmp PrimEQ = True isCmp PrimULT = True isCmp PrimULE = True isCmp _ = False cmpToVS :: Integer -> Integer -> Bool -> PrimOp -> VSetInteger cmpToVS n i True PrimEQ = vSing i cmpToVS n i True PrimULT = vFromTo 0 (i-1) cmpToVS n i True PrimULE = vFromTo 0 i cmpToVS n i False PrimEQ = vFromTo 0 (i-1) `vUnion` vFromTo (i+1) (2^n-1) cmpToVS n i False PrimULT = vFromTo (i+1) (2^n-1) cmpToVS n i False PrimULE = vFromTo i (2^n-1) cmpToVS _ _ _ prim = internalError ("ITransform.cmpToVS: " ++ ppString prim) doCmp :: ValMap a -> IExpr a -> PrimOp -> IExpr a -> Integer -> Integer -> Bool -> (ValMap a,IExpr a) doCmp m e cmp v n i norm = let vs = vmGet v m tvs = cmpToVS n i norm cmp fvs = cmpToVS n i (not norm) cmp vs' = vs `vIntersect` tvs ivs = vs `vIntersect` fvs m' = vmAdd v vs' m in if vNull ivs && not (vNull vs') then (m', iTrue) else if vNull vs' && not (vNull ivs) then (m', iFalse) else (m', e) getBit :: IType -> Maybe Integer getBit (ITAp b (ITNum n)) | b == itBit = Just n getBit _ = Nothing ----------------------------------------------------------------------------- -- After transforming the defs, with no prior CSE assumptions, -- we digest the resulting CSE info and use that as the assumptions -- when transforming the rest of the module. -- -- We find all the defs that were CSE'd to the same (bad) new name and -- replace it with a good name from one of the defs (if there is one). -- Some of these defs are marked as not-CSE-able, so we keep those defs -- separate. -- iTransFixupDefNames :: forall a . Flags -> T () a iTransFixupDefNames flags = do transform_state <- get let old_defmap = def_map transform_state old_csemap = cse_map transform_state -- A map from (bad) CSE names to the defs that it replaced -- (from those defs, we'll want to pick a good name, to keep) -- (and attempt to preserve the defprops?) cse_ids_map :: M.Map Id [(Id, [DefProp])] cse_ids_map = M.fromListWith (++) $ [ (cse_name, [(def_name, props)]) | (def_name, (_, ICon cse_name value@(ICValue {}), props)) <- M.toList old_defmap ] -- Identify the name to be used, by filtering out the non-CSE defs -- and picking the best name from the remaining (for now, the first) rename_map = let pickId cse_id def_ips = -- filter out the non-CSE defs case (filter (not . defPropsHasNoCSE . snd) def_ips) of -- if they're all non-CSE, keep the bad name [] -> cse_id -- otherwise, take the first def name ((def_id, _):_) -> def_id in M.mapWithKey pickId cse_ids_map -- function to rename ICValue references (to use the new CSE name) rename_expr = iTransRenameIdsInExpr rename_map -- function to rename a CSE def -- XXX defprops from the CSE'd defs are lost rename_def = iTransRenameIdsInDef rename_map -- fixup the CSE Map so that: -- * refs in the expr should refer to the new CSE name -- * the CSE ref should point to the new CSE name -- * the def name and expr are updated new_csemap = M.fromList [ (rename_expr e, (rename_expr ref, rename_def def)) | (e, (ref, def)) <- M.toList old_csemap ] -- fix up the defs to refer to new CSE name in their exprs -- (the def names themselves are unchanged) new_defmap = let mapFn (ty, e, props) = (ty, rename_expr e, props) in M.map mapFn old_defmap new_state :: TState a new_state = transform_state { def_map = new_defmap, cse_map = new_csemap } put new_state -- given a map from old to new identifiers, replace all occurrences -- of the old identifier with the new in a given expression iTransRenameIdsInExpr :: M.Map Id Id -> IExpr a -> IExpr a iTransRenameIdsInExpr rename_map expr@(ICon name value@(ICValue {})) = let renamed_value_def = iTransRenameIdsInExpr rename_map (iValDef value) new_value = value { iValDef = renamed_value_def } in ICon (iTransRenameId rename_map name) new_value iTransRenameIdsInExpr rename_map (IAps func types args) = let renamed_func = iTransRenameIdsInExpr rename_map func renamed_args = [iTransRenameIdsInExpr rename_map arg | arg <- args] in IAps renamed_func types renamed_args iTransRenameIdsInExpr rename_map (ICon i (ICUndet t k (Just v))) = let v' = iTransRenameIdsInExpr rename_map v in ICon i (ICUndet t k (Just v')) iTransRenameIdsInExpr rename_map expr = expr -- given a map from old to new identifiers, replace all occurrences -- of the old identifier with the new in a given definition, -- including the name being defined -- XXX This loses the props. If the name is not renamed, we can keep -- XXX the old props; if it's renamed, we need to be given the new props. iTransRenameIdsInDef :: M.Map Id Id -> IDef a -> IDef a iTransRenameIdsInDef rename_map (IDef name typ expr _) = let renamed_expr = iTransRenameIdsInExpr rename_map expr renamed_name = iTransRenameId rename_map name in IDef renamed_name typ renamed_expr [] -- given a map from old to new identifiers, replace any old id with a new one iTransRenameId :: M.Map Id Id -> Id -> Id iTransRenameId rename_map name = M.findWithDefault name name rename_map -----------------------------------------------------------------------------