Two Hoopl questions

[Simon Peyton-Jones]

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-bounces at 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 at haskell.org
|  http://www.haskell.org/mailman/listinfo/ghc-devs