It's easy to get confused, but in fact the bedrock issues are quite simple.
As Edward says, a function f is monotonic iff
x <= y implies f(x) <= f(y)
Monotonicity does NOT mean that x <= f(x)!!!
The transfer function, and the 'join' function, must all be monotonic. It's
that simple.
=======
I would *not* mess with the rewrite fuel. It's not used at all for analysis,
only for rewrites, and it's the analysis that is going bad on you.
Instead, simply arrange give an extra "fuel" counter to function 'loop' line
603 of Compiler.Hoopl.Dataflow. If you run out of fuel, print some information
about blocks left in the to-do list and the next few iterations. You can give
enough fuel for (say) 100 passes through each block. Do this if DEBUG is
defined. In this way you'll get much more information than non-termination.
==========
For the constant-prop stuff, you want to know what each fact means. Something
like
x -> BOT "I have no information about x"
x -> val "x always has value val, on all the control flow paths I
have seen so far"
x -> NAC "x can have more than one value depending on the control
flow path
that reaches this point"
Now the transfer functions in your email make perfect sense.
Simon
| -----Original Message-----
| From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of Jan
Stolarek
| Sent: 26 July 2013 22:48
| To: Edward Z. Yang
| Cc: ghc-devs
| Subject: Re: Two Hoopl questions
|
| Thank you Edward. I am aware of these requirements - my problem is writing
the
| code in which these
| will always hold (I'm optimizing Cmm and hand-written Cmm files tend to cause
| many problems that
| don't appear in automatically generated Cmm). Having a debugging tool in
form of
| Fuel would be
| helpful for me, because instead of getting a freeze and seeing no output
from -
| ddump-cmm I would
| see incorrectly transformed Cmm that would allow me to track bugs more
easily.
|
| > > • The transfer function must be monotonic: given a more infor-
| > > mative fact in, it must produce a more informative fact out.
| I spent some considerable time thinking about this. Consider a simple
example of
| copy propagation.
| Let's assume that { x = NAC }, i.e. we know that x has been defined earlier
but is
| Not-A-Constant
| and so we cannot rewrite it. Now we have something llike this:
|
| x := 3;
| y := x;
|
| Here we are allowed to rewrite y := x with y := 3, because after first
statement we
| learn that { x
| = 3 }. Now consider this:
|
| x := 3;
| x := very_unsafe_stg_call();
| y := x;
|
| Here, after the first statement we learn that { x = 3 }, but after the
second one
| we learn once
| again that x is NAC and so we are not allowed to rewrite statement y := x.
So the
| value of x can
| change from NAC to a constant and from constant to a NAC. Is such a transfer
| function monotonic?
|
| Janek
|
| _______________________________________________
| ghc-devs mailing list
| ghc-devs@haskell.org
| http://www.haskell.org/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
