-fhpc inteferes/prevents rewrite rules from firing

[dons]

Use case:

I'm writing tests for rewrite rules, and using HPC to determine if rules were fired (and their code exercised). HPC is quite cool here, since it lets us see which rules fired, without needing to explicitly export functions to test.

However, -fhpc seems to prevent many rules from firing (likely due to ticks getting in the way?)

For example:

import qualified  Data.ByteString.Char8 as C

main = print (C.pack "literal")

When compiled normally, triggers a nice rewrite rule:

$ ghc -O2 A.hs -ddump-simpl-stats A.hs -c

    1 ByteString pack/packAddress

Now with -fhpc:

2 RuleFired
    1 unpack
    1 unpack-list

What's the best way to ensure the same code is exercised with and without -fhpc here? (I'd quite like to get this working, since rewrite rules benefit from testing.)

[AndyGill]

I'm not sure what to do here. To match code that contains ticks, and rewrite them requires either

• removing ticks - generally a bad idea!
• recreating the ticks, which is hard/impossible to do in some cases.

I suppose we could have an option to ignore ticks in rules, but this leads to false positives.

Also consider:

  {-# RULES
    "pack/packAddress" forall s . pack (unpackCString# s) = B.packAddress s
   #-}

pack and unpackCString are strict, so we have tick equivalence!

    tick<1>pack(tick<2>unpackCString# (tick<3> s))

is the same as

   tick<1,2,3>pack(unpackCString# s)

The tick lifting has given us the original match.

[simonpj]

In general, coverage testing is incompatible with optimisation, although it seems surprising (to me) robust:

  f x = g (h x)
  g x = x
  h x = x

then if we inline busily we'll get

  f x = x

and in fact this does happen, but none of the relevant ticks are lost. In effect, the optimiser knows how to commute stuff with ticks, because ticks get encoded as case expressions. There's a paper in here, actually, because the code does get shaken around quite a bit, despite the ticks littering it. (Mind you, we don't yet have an operational semantics to tell us what ticks should do, though that would not be hard to write. That too should be in the paper.)

But this robustness breaks down for rewrite rules, because they inspect the structure of terms, and that's messed up by the ticks. For a composition of strict functions, matters are more straightforward, as Andy says, because all the ticks float to the outside. To take his example, if we have

  f x = ...(pack (unpack s))...

after tick decoration it'll look like

  f x = ...(tick <a> (pack (tick <b> (unpack s)))...

then the tick around the (unpack s) will float out (since pack is strict), so we'll end up with something like

  f x = ...(tick <a> (tick <b> (pack (unpack s)))...

So if we simply did not tick-ify the LHS of a rule you'd think the rule would work. And it seems to: try this with -fhpc -O.

module Foo where

f g x = g x

{-# NOINLINE g #-}
g x = x

{-# NOINLINE h #-}
h x = x

foo y = f g (h y)

{-# RULES "gh" forall x.  g (h x) = g x #-}

(NB: The rule gh doesn't fire until after strictness analysis has told us that g is strict; and that late firing definitely could be a problem.)

Conclusion: we aren't decorating RULES with ticks anyway, and that must be the Right Thing for the LHS of the rule. (We almost certainly should decorate their right-hand sides -- that's a bug.)

The problem, I guess, comes with lazy functions, where the ticks don't float. And indeed, if f is lazy, so does not provably consume its argument, what would you like to happen for

  RULE "f"  forall x. f (g x) = x

In an expression ...(f (tick <a> (g x)))..., what do you want to happen to the <a> tick? Do you want to show (g x) as covered? Or not?

The most plausible answer is, I think, that we'd like to show (g x) as covered, so we'd like to do the following rewrite

   ...(f (tick <a> (g x)))...  ==>   ....(tick <a> x)....

That is, the tick should not get in the way of matching, but should not be discarded either. Instead it should be saved up and wrapped around the result.

Interesting. This is very like what happens for let-expressions. See Section 4.1 of the  call-pattern specialisation paper, and Note [Matching lets] in specialise/Rules.lhs. So I speculate that, if this is the semantics we want, we could adjust the rule matcher to ignore-but-accumulate ticks, just as it does lets.

Andy if you want to pursue this, I can guide you to the right place.

Simon

[simonmar]

Replying to simonpj:

In general, coverage testing is incompatible with optimisation, although it seems surprising (to me) robust: {{{ f x = g (h x) g x = x h x = x }}} then if we inline busily we'll get {{{ f x = x }}} and in fact this does happen, but none of the relevant ticks are lost. In effect, the optimiser knows how to commute stuff with ticks, because ticks get encoded as case expressions. There's a paper in here, actually, because the code does get shaken around quite a bit, despite the ticks littering it. (Mind you, we don't yet have an operational semantics to tell us what ticks should do, though that would not be hard to write. That too should be in the paper.)

We said a little about this in the GHCi debugger paper, although I agree a formal treatment would be useful. You may remember the basic idea is that we tell the simplifier that the tick has side effects. The principle we want the simplifier to preserve is that the tick in case tick of _ -> e should be evaluated if and only if e would be evaluated by the standard lazy operational semantics. We don't care about ordering: the simplifier can re-order two ticks, as long as it can be sure that both expressions would have been evaluated according to the semantics. (in the debugger you'll see the effect of reordering, but HPC doesn't care).