%
% (c) The GRASP/AQUA Project, Glasgow University, 19931998
%
\section[SaAbsInt]{Abstract interpreter for strictness analysis}
\begin{code}
#ifndef OLD_STRICTNESS
module SaAbsInt () where
#else
module SaAbsInt (
findStrictness,
findDemand, findDemandAlts,
absEval,
widen,
fixpoint,
isBot
) where
#include "HsVersions.h"
import StaticFlags ( opt_AllStrict, opt_NumbersStrict )
import CoreSyn
import CoreUnfold ( maybeUnfoldingTemplate )
import Id ( Id, idType, idUnfolding, isDataConWorkId_maybe,
idStrictness,
)
import DataCon ( dataConTyCon, splitProductType_maybe, dataConRepArgTys )
import IdInfo ( StrictnessInfo(..) )
import Demand ( Demand(..), wwPrim, wwStrict, wwUnpack, wwLazy,
mkStrictnessInfo, isLazy
)
import SaLib
import TyCon ( isProductTyCon, isRecursiveTyCon )
import Type ( splitTyConApp_maybe,
isUnLiftedType, Type )
import TyCon ( tyConUnique )
import PrelInfo ( numericTyKeys )
import Util ( isIn, nOfThem, zipWithEqual, equalLength )
import Outputable
\end{code}
%************************************************************************
%* *
\subsection[AbsValops]{Operations on @AbsVals@}
%* *
%************************************************************************
Least upper bound, greatest lower bound.
\begin{code}
lub, glb :: AbsVal -> AbsVal -> AbsVal
lub AbsBot val2 = val2
lub val1 AbsBot = val1
lub (AbsProd xs) (AbsProd ys) = AbsProd (zipWithEqual "lub" lub xs ys)
lub _ _ = AbsTop
glb v1 v2
| is_fun v1 || is_fun v2
= if not (anyBot v1) && not (anyBot v2)
then
AbsTop
else
AbsBot
where
is_fun (AbsFun _ _) = True
is_fun (AbsApproxFun _ _) = True
is_fun other = False
glb (AbsProd xs) (AbsProd ys) = AbsProd (zipWithEqual "glb" glb xs ys)
glb AbsTop v2 = v2
glb v1 AbsTop = v1
glb _ _ = AbsBot
\end{code}
@isBot@ returns True if its argument is (a representation of) bottom. The
``representation'' part is because we need to detect the bottom {\em function}
too. To detect the bottom function, bind its args to top, and see if it
returns bottom.
Used only in strictness analysis:
\begin{code}
isBot :: AbsVal -> Bool
isBot AbsBot = True
isBot other = False
\end{code}
Used only in absence analysis:
\begin{code}
anyBot :: AbsVal -> Bool
anyBot AbsBot = True
anyBot AbsTop = False
anyBot (AbsProd vals) = any anyBot vals
anyBot (AbsFun bndr_ty abs_fn) = anyBot (abs_fn AbsTop)
anyBot (AbsApproxFun _ val) = anyBot val
\end{code}
@widen@ takes an @AbsVal@, $val$, and returns and @AbsVal@ which is
approximated by $val$. Furthermore, the result has no @AbsFun@s in
it, so it can be compared for equality by @sameVal@.
\begin{code}
widen :: AnalysisKind -> AbsVal -> AbsVal
widen StrAnal the_fn@(AbsFun bndr_ty _)
= case widened_body of
AbsApproxFun ds val -> AbsApproxFun (d : ds) val
where
d = findRecDemand str_fn abs_fn bndr_ty
str_fn val = isBot (foldl (absApply StrAnal) the_fn
(val : [AbsTop | d <- ds]))
other -> AbsApproxFun [d] widened_body
where
d = findRecDemand str_fn abs_fn bndr_ty
str_fn val = isBot (absApply StrAnal the_fn val)
where
widened_body = widen StrAnal (absApply StrAnal the_fn AbsTop)
abs_fn val = False
widen StrAnal (AbsProd vals) = AbsProd (map (widen StrAnal) vals)
widen StrAnal other_val = other_val
widen AbsAnal the_fn@(AbsFun bndr_ty _)
| anyBot widened_body = AbsBot
| otherwise
= case widened_body of
AbsApproxFun ds val -> AbsApproxFun (d : ds) val
where
d = findRecDemand str_fn abs_fn bndr_ty
abs_fn val = not (anyBot (foldl (absApply AbsAnal) the_fn
(val : [AbsTop | d <- ds])))
other -> AbsApproxFun [d] widened_body
where
d = findRecDemand str_fn abs_fn bndr_ty
abs_fn val = not (anyBot (absApply AbsAnal the_fn val))
where
widened_body = widen AbsAnal (absApply AbsAnal the_fn AbsTop)
str_fn val = True
widen AbsAnal (AbsProd vals) = AbsProd (map (widen AbsAnal) vals)
widen AbsAnal other_val = other_val
\end{code}
@crudeAbsWiden@ is used just for absence analysis, and always
returns AbsTop or AbsBot, so it widens to a twopoint domain
\begin{code}
crudeAbsWiden :: AbsVal -> AbsVal
crudeAbsWiden val = if anyBot val then AbsBot else AbsTop
\end{code}
@sameVal@ compares two abstract values for equality. It can't deal with
@AbsFun@, but that should have been removed earlier in the day by @widen@.
\begin{code}
sameVal :: AbsVal -> AbsVal -> Bool
#ifdef DEBUG
sameVal (AbsFun _ _) _ = panic "sameVal: AbsFun: arg1"
sameVal _ (AbsFun _ _) = panic "sameVal: AbsFun: arg2"
#endif
sameVal AbsBot AbsBot = True
sameVal AbsBot other = False
sameVal AbsTop AbsTop = True
sameVal AbsTop other = False
sameVal (AbsProd vals1) (AbsProd vals2) = and (zipWithEqual "sameVal" sameVal vals1 vals2)
sameVal (AbsProd _) AbsTop = False
sameVal (AbsProd _) AbsBot = False
sameVal (AbsApproxFun str1 v1) (AbsApproxFun str2 v2) = str1 == str2 && sameVal v1 v2
sameVal (AbsApproxFun _ _) AbsTop = False
sameVal (AbsApproxFun _ _) AbsBot = False
sameVal val1 val2 = panic "sameVal: type mismatch or AbsFun encountered"
\end{code}
@evalStrictness@ compares a @Demand@ with an abstract value, returning
@True@ iff the abstract value is {\em less defined} than the demand.
(@True@ is the exciting answer; @False@ is always safe.)
\begin{code}
evalStrictness :: Demand
-> AbsVal
-> Bool
evalStrictness (WwLazy _) _ = False
evalStrictness WwStrict val = isBot val
evalStrictness WwEnum val = isBot val
evalStrictness (WwUnpack _ demand_info) val
= case val of
AbsTop -> False
AbsBot -> True
AbsProd vals
| not (equalLength vals demand_info) -> pprTrace "TELL SIMON: evalStrictness" (ppr demand_info $$ ppr val)
False
| otherwise -> or (zipWithEqual "evalStrictness" evalStrictness demand_info vals)
_ -> pprTrace "evalStrictness?" empty False
evalStrictness WwPrim val
= case val of
AbsTop -> False
AbsBot -> True
other -> pprPanic "evalStrictness: WwPrim:" (ppr other)
\end{code}
For absence analysis, we're interested in whether "poison" in the
argument (ie a bottom therein) can propagate to the result of the
function call; that is, whether the specified demand can {\em
possibly} hit poison.
\begin{code}
evalAbsence (WwLazy True) _ = False
evalAbsence (WwUnpack _ demand_info) val
= case val of
AbsTop -> False
AbsBot -> True
AbsProd vals
| not (equalLength vals demand_info) -> pprTrace "TELL SIMON: evalAbsence" (ppr demand_info $$ ppr val)
True
| otherwise -> or (zipWithEqual "evalAbsence" evalAbsence demand_info vals)
_ -> pprTrace "TELL SIMON: evalAbsence"
(ppr demand_info $$ ppr val)
True
evalAbsence other val = anyBot val
\end{code}
%************************************************************************
%* *
\subsection[absEval]{Evaluate an expression in the abstract domain}
%* *
%************************************************************************
\begin{code}
absId anal var env
= case (lookupAbsValEnv env var,
isDataConWorkId_maybe var,
idStrictness var,
maybeUnfoldingTemplate (idUnfolding var)) of
(Just abs_val, _, _, _) ->
abs_val
(_, Just data_con, _, _) | isProductTyCon tycon &&
not (isRecursiveTyCon tycon)
->
productAbsVal (dataConRepArgTys data_con) []
where
tycon = dataConTyCon data_con
(_, _, NoStrictnessInfo, Just unfolding) ->
absEval anal unfolding env
(_, _, strictness_info, _) ->
absValFromStrictness anal strictness_info
productAbsVal [] rev_abs_args = AbsProd (reverse rev_abs_args)
productAbsVal (arg_ty : arg_tys) rev_abs_args = AbsFun arg_ty (\ abs_arg -> productAbsVal arg_tys (abs_arg : rev_abs_args))
\end{code}
\begin{code}
absEval :: AnalysisKind -> CoreExpr -> AbsValEnv -> AbsVal
absEval anal (Type ty) env = AbsTop
absEval anal (Var var) env = absId anal var env
\end{code}
Discussion about error (following/quoting Lennart): Any expression
'error e' is regarded as bottom (with HBC, with the ffailstrict
flag, on with O).
Regarding it as bottom gives much better strictness properties for
some functions. E.g.
f [x] y = x+y
f (x:xs) y = f xs (x+y)
i.e.
f [] _ = error "no match"
f [x] y = x+y
f (x:xs) y = f xs (x+y)
is strict in y, which you really want. But, it may lead to
transformations that turn a call to \tr{error} into nontermination.
(The odds of this happening aren't good.)
Things are a little different for absence analysis, because we want
to make sure that any poison (?????)
\begin{code}
absEval anal (Lit _) env = AbsTop
\end{code}
\begin{code}
absEval anal (Lam bndr body) env
| isTyVar bndr = absEval anal body env
| otherwise = AbsFun (idType bndr) abs_fn
where
abs_fn arg = absEval anal body (addOneToAbsValEnv env bndr arg)
absEval anal (App expr (Type ty)) env
= absEval anal expr env
absEval anal (App f val_arg) env
= absApply anal (absEval anal f env)
(absEval anal val_arg env)
\end{code}
\begin{code}
absEval anal expr@(Case scrut case_bndr alts) env
= let
scrut_val = absEval anal scrut env
alts_env = addOneToAbsValEnv env case_bndr scrut_val
in
case (scrut_val, alts) of
(AbsBot, _) -> AbsBot
(AbsProd arg_vals, [(con, bndrs, rhs)])
| con /= DEFAULT ->
ASSERT(equalLength arg_vals val_bndrs)
absEval anal rhs rhs_env
where
val_bndrs = filter isId bndrs
rhs_env = growAbsValEnvList alts_env (val_bndrs `zip` arg_vals)
other -> absEvalAlts anal alts alts_env
\end{code}
For @Lets@ we widen the value we get. This is nothing to
do with fixpointing. The reason is so that we don't get an explosion
in the amount of computation. For example, consider:
\begin{verbatim}
let
g a = case a of
q1 -> ...
q2 -> ...
f x = case x of
p1 -> ...g r...
p2 -> ...g s...
in
f e
\end{verbatim}
If we bind @f@ and @g@ to their exact abstract value, then we'll
``execute'' one call to @f@ and {\em two} calls to @g@. This can blow
up exponentially. Widening cuts it off by making a fixed
approximation to @f@ and @g@, so that the bodies of @f@ and @g@ are
not evaluated again at all when they are called.
Of course, this can lose useful joint strictness, which is sad. An
alternative approach would be to try with a certain amount of ``fuel''
and be prepared to bale out.
\begin{code}
absEval anal (Let (NonRec binder e1) e2) env
= let
new_env = addOneToAbsValEnv env binder (widen anal (absEval anal e1 env))
in
absEval anal e2 new_env
absEval anal (Let (Rec pairs) body) env
= let
(binders,rhss) = unzip pairs
rhs_vals = cheapFixpoint anal binders rhss env
new_env = growAbsValEnvList env (binders `zip` rhs_vals)
in
absEval anal body new_env
absEval anal (Note (Coerce _ _) expr) env = AbsTop
absEval anal (Note note expr) env = absEval anal expr env
\end{code}
\begin{code}
absEvalAlts :: AnalysisKind -> [CoreAlt] -> AbsValEnv -> AbsVal
absEvalAlts anal alts env
= combine anal (map go alts)
where
combine StrAnal = foldr1 lub
combine AbsAnal = foldr1 glb
go (con, bndrs, rhs)
= absEval anal rhs rhs_env
where
rhs_env = growAbsValEnvList env (filter isId bndrs `zip` repeat AbsTop)
\end{code}
%************************************************************************
%* *
\subsection[absApply]{Apply an abstract function to an abstract argument}
%* *
%************************************************************************
Easy ones first:
\begin{code}
absApply :: AnalysisKind -> AbsVal -> AbsVal -> AbsVal
absApply anal AbsBot arg = AbsBot
absApply StrAnal AbsTop arg = AbsTop
absApply AbsAnal AbsTop arg = if anyBot arg
then AbsBot
else AbsTop
\end{code}
An @AbsFun@ with only one more argument needed
result. A @Lam@ with two or more args: return another @AbsFun@ with
an augmented environment.
\begin{code}
absApply anal (AbsFun bndr_ty abs_fn) arg = abs_fn arg
\end{code}
\begin{code}
absApply StrAnal (AbsApproxFun (d:ds) val) arg
= case ds of
[] -> val'
other -> AbsApproxFun ds val'
where
val' | evalStrictness d arg = AbsBot
| otherwise = val
absApply AbsAnal (AbsApproxFun (d:ds) val) arg
= if evalAbsence d arg
then AbsBot
else case ds of
[] -> val
other -> AbsApproxFun ds val
#ifdef DEBUG
absApply anal f@(AbsProd _) arg
= pprPanic ("absApply: Duff function: AbsProd." ++ show anal) ((ppr f) <+> (ppr arg))
#endif
\end{code}
%************************************************************************
%* *
\subsection[findStrictness]{Determine some binders' strictness}
%* *
%************************************************************************
\begin{code}
findStrictness :: Id
-> AbsVal
-> AbsVal
-> StrictnessInfo
findStrictness id (AbsApproxFun str_ds str_res) (AbsApproxFun abs_ds _)
= find_strictness id str_ds str_res abs_ds
findStrictness id str_val abs_val
| isBot str_val = mkStrictnessInfo ([], True)
| otherwise = NoStrictnessInfo
find_strictness id orig_str_ds orig_str_res orig_abs_ds
= mkStrictnessInfo (go orig_str_ds orig_abs_ds, res_bot)
where
res_bot = isBot orig_str_res
go str_ds abs_ds = zipWith mk_dmd str_ds (abs_ds ++ repeat wwLazy)
mk_dmd str_dmd (WwLazy True)
= WARN( not (res_bot || isLazy str_dmd),
ppr id <+> ppr orig_str_ds <+> ppr orig_abs_ds )
WwLazy True
mk_dmd (WwUnpack u str_ds)
(WwUnpack _ abs_ds) = WwUnpack u (go str_ds abs_ds)
mk_dmd str_dmd abs_dmd = str_dmd
\end{code}
\begin{code}
findDemand dmd str_env abs_env expr binder
= findRecDemand str_fn abs_fn (idType binder)
where
str_fn val = evalStrictness dmd (absEval StrAnal expr (addOneToAbsValEnv str_env binder val))
abs_fn val = not (evalAbsence dmd (absEval AbsAnal expr (addOneToAbsValEnv abs_env binder val)))
findDemandAlts dmd str_env abs_env alts binder
= findRecDemand str_fn abs_fn (idType binder)
where
str_fn val = evalStrictness dmd (absEvalAlts StrAnal alts (addOneToAbsValEnv str_env binder val))
abs_fn val = not (evalAbsence dmd (absEvalAlts AbsAnal alts (addOneToAbsValEnv abs_env binder val)))
\end{code}
@findRecDemand@ is where we finally convert strictness/absence info
into ``Demands'' which we can pin on Ids (etc.).
NOTE: What do we do if something is {\em both} strict and absent?
Should \tr{f x y z = error "foo"} says that \tr{f}'s arguments are all
strict (because of bottoming effect of \tr{error}) or all absent
(because they're not used)?
Well, for practical reasons, we prefer absence over strictness. In
particular, it makes the ``default defaults'' for class methods (the
ones that say \tr{defm.foo dict = error "I don't exist"}) come out
nicely [saying ``the dict isn't used''], rather than saying it is
strict in every component of the dictionary [massive gratuitious
casing to take the dict apart].
But you could have examples where going for strictness would be better
than absence. Consider:
\begin{verbatim}
let x = something big
in
f x y z + g x
\end{verbatim}
If \tr{x} is marked absent in \tr{f}, but not strict, and \tr{g} is
lazy, then the thunk for \tr{x} will be built. If \tr{f} was strict,
then we'd lettocase it:
\begin{verbatim}
case something big of
x -> f x y z + g x
\end{verbatim}
Ho hum.
\begin{code}
findRecDemand :: (AbsVal -> Bool)
-> (AbsVal -> Bool)
-> Type
-> Demand
findRecDemand str_fn abs_fn ty
= if isUnLiftedType ty then
wwPrim
else if abs_fn AbsBot then
WwLazy True
else if not (opt_AllStrict ||
(opt_NumbersStrict && is_numeric_type ty) ||
str_fn AbsBot) then
WwLazy False
else
case splitProductType_maybe ty of
Nothing -> wwStrict
Just (tycon,_,data_con,cmpnt_tys)
| isRecursiveTyCon tycon
-> wwStrict
| null compt_strict_infos
-> wwStrict
| otherwise
-> wwUnpack compt_strict_infos
where
prod_len = length cmpnt_tys
compt_strict_infos
= [ findRecDemand
(\ cmpnt_val ->
str_fn (mkMainlyTopProd prod_len i cmpnt_val)
)
(\ cmpnt_val ->
abs_fn (mkMainlyTopProd prod_len i cmpnt_val)
)
cmpnt_ty
| (cmpnt_ty, i) <- cmpnt_tys `zip` [1..] ]
where
is_numeric_type ty
= case (splitTyConApp_maybe ty) of
Nothing -> False
Just (tycon, _) -> tyConUnique tycon `is_elem` numericTyKeys
where
is_elem = isIn "is_numeric_type"
mkMainlyTopProd :: Int -> Int -> AbsVal -> AbsVal
mkMainlyTopProd n i val
= let
befores = nOfThem (i1) AbsTop
afters = nOfThem (ni) AbsTop
in
AbsProd (befores ++ (val : afters))
\end{code}
%************************************************************************
%* *
\subsection[fixpoint]{Fixpointer for the strictness analyser}
%* *
%************************************************************************
The @fixpoint@ functions take a list of \tr{(binder, expr)} pairs, an
environment, and returns the abstract value of each binder.
The @cheapFixpoint@ function makes a conservative approximation,
by binding each of the variables to Top in their own right hand sides.
That allows us to make rapid progress, at the cost of a lessthanwonderful
approximation.
\begin{code}
cheapFixpoint :: AnalysisKind -> [Id] -> [CoreExpr] -> AbsValEnv -> [AbsVal]
cheapFixpoint AbsAnal [id] [rhs] env
= [crudeAbsWiden (absEval AbsAnal rhs new_env)]
where
new_env = addOneToAbsValEnv env id AbsTop
cheapFixpoint anal ids rhss env
= [widen anal (absEval anal rhs new_env) | rhs <- rhss]
where
new_env = growAbsValEnvList env [(id,safe_val) | id <- ids]
safe_val
= case anal of
StrAnal -> AbsTop
AbsAnal -> AbsBot
\end{code}
\begin{code}
fixpoint :: AnalysisKind -> [Id] -> [CoreExpr] -> AbsValEnv -> [AbsVal]
fixpoint anal [] _ env = []
fixpoint anal ids rhss env
= fix_loop initial_vals
where
initial_val id
= case anal of
AbsAnal -> AbsTop
StrAnal -> AbsBot
initial_vals = [ initial_val id | id <- ids ]
fix_loop :: [AbsVal] -> [AbsVal]
fix_loop current_widened_vals
= let
new_env = growAbsValEnvList env (ids `zip` current_widened_vals)
new_vals = [ absEval anal rhs new_env | rhs <- rhss ]
new_widened_vals = map (widen anal) new_vals
in
if (and (zipWith sameVal current_widened_vals new_widened_vals)) then
current_widened_vals
else
fix_loop new_widened_vals
\end{code}
For absence analysis, we make do with a very very simple approach:
look for convergence in a twopoint domain.
We used to use just one iteration, starting with the variables bound
to @AbsBot@, which is safe.
Prior to that, we used one iteration starting from @AbsTop@ (which
isn't safe). Why isn't @AbsTop@ safe? Consider:
\begin{verbatim}
letrec
x = ...p..d...
d = (x,y)
in
...
\end{verbatim}
Here, if p is @AbsBot@, then we'd better {\em not} end up with a ``fixed
point'' of @d@ being @(AbsTop, AbsTop)@! An @AbsBot@ initial value is
safe because it gives poison more often than really necessary, and
thus may miss some absence, but will never claim absence when it ain't
so.
Anyway, one iteration starting with everything bound to @AbsBot@ give
bad results for
f = \ x -> ...f...
Here, f would always end up bound to @AbsBot@, which ain't very
clever, because then it would introduce poison whenever it was
applied. Much better to start with f bound to @AbsTop@, and widen it
to @AbsBot@ if any poison shows up. In effect we look for convergence
in the twopoint @AbsTop@/@AbsBot@ domain.
What we miss (compared with the cleverer strictness analysis) is
spotting that in this case
f = \ x y -> ...y...(f x y')...
\tr{x} is actually absent, since it is only passed round the loop, never
used. But who cares about missing that?
NB: despite only having a twopoint domain, we may still have many
iterations, because there are several variables involved at once.
\begin{code}
#endif /* OLD_STRICTNESS */
\end{code}