Let/app invariant violations?

[osa1]

Hi all,

This is my first time using HERMIT and I'm not sure if this is a HERMIT-related problem, so apologies if it's not.

After some number of repeated transformations HERMIT is generating a program but GHC's CoreLint pass is rejecting the program with:

*** Core Lint errors : in result of Core plugin:  HERMIT0 ***
<no location info>: Warning:
    In the expression: I# (integerToInt i_a1oG)
    This argument does not satisfy the let/app invariant:
      integerToInt i_a1oG
*** Offending Program ***
... prints huge program ...

So the question is, is this a HERMIT problem or should users make sure their transformations don't violate invariants somehow? I can try to generate a minimal case if this turns out to be a HERMIT problem.

[xich]

I suspect the expression that should be there is:

case integerToInt i_a1oG of w
  _ -> I# w

This most likely happens if an explicit App is used to construct the application, instead of the mkCoreApp function, which checks the invariant and generates a case if necessary. It's possible that some transformation HERMIT provides makes this mistake. Do you have the example code and script that leads to this?

You can also set-auto-corelint True before you run your script... it will run lint after each command, which might catch it earlier. If you are using bash, there is a bash-debug that lints after each step, which is useful to track this stuff down.

@RyanGlScott didn't you run into something like this at some point?

[osa1]

I'm using the HERMIT API and not the language, could it be related with that? I thought that the language commands are directly mapped to HERMIT API rewrite functions so I'm guessing that's not the reason. In any case, I'll try to generate a minimal example.

In case it helps, here are my transformers:

elimLets :: RewriteH LCore
elimLets = tryR $ repeatR $ anybuR $ promoteR letElimR

step :: RewriteH LCore
step =
    repeatR $
      ((onetdR $ promoteR (inlineR <+ betaReduceR <+ caseReduceUnfoldR True))
          >>> elimLets)
      >>> observeR "step"

(the program is big and I'll post once I can find a smaller program)

[RyanGlScott]

I experienced a similar error when trying to run the factorial HERMIT example on GHC 7.10:

$ hermit Fac.hs
...

module Main where
  (-) ∷ Int → Int → Int
  (*) ∷ Int → Int → Int
  wrap ∷ (Int# → Int#) → Int → Int
  unwrap ∷ (Int → Int) → Int# → Int#
  fac ∷ Int → Int
  main ∷ IO ()
  main ∷ IO ()
hermit<0> set-auto-corelint True
hermit<0> set-pp-type Show
module Main where
  (-) ∷ Int → Int → Int
  (*) ∷ Int → Int → Int
  wrap ∷ (Int# → Int#) → Int → Int
  unwrap ∷ (Int → Int) → Int# → Int#
  fac ∷ Int → Int
  main ∷ IO ()
  main ∷ IO ()
hermit<0> set-fail-hard True
hermit<0> load-and-run "Fac.hss"
Loading "Fac.hss"...
Script "Fac.hss" loaded successfully from "Fac.hss".
fac ∷ Int → Int
fac =
  let f ∷ (Int → Int) → Int → Int
      f = λ fac ds →
        case ds of wild Int
          I# ds →
            case ds of ds Int
              _ → (λ ds → (*) ds (fac ((-) ds (I# 1)))) void#
              0 → I# 1
      rec work ∷ Int# → Int#
          work = unwrap (f (wrap work))
  in wrap work
Error in expression: bash-extended-with [case-elim-inline-scrutinee,inline ['unwrap,'wrap,'*,'-]]
Core Lint Failed:
<no location info>: Warning:
    In the expression: *# x (work_s2zG (-# x 1))
    This argument does not satisfy the let/app invariant:
      work_s2zG (-# x 1)

Exiting HERMIT and aborting GHC compilation.

[roboguy13]

It looks like you can't have unboxed types in a recursive let binding anymore.

If you get rid of the case-elim-inline-scrutinee, it leaves the case in and it looks like it works without warnings. I think this is because the unboxed stuff is happening in a case binding rather than a recursive let (which GHC is okay with).

I also notice that if you use set-auto-corelint True with the original HERMIT script, it will throw the warning before the resume and, as a result, will allow you to finish compiling the program. I don't know if this is a good thing or not, but it might be a way around this issue.

[andygill]

So is our use of unwrap unsound?

[roboguy13]

@andygill I'm not totally sure. The new warning seems like it might be a bit overly general, but I don't know enough about it to be sure.

I think the issue is that let floating a recursive let binding that involves unboxed types can sometimes change the termination properties of a program, which doesn't seem to be a problem in our particular example. There's some more info here.

[roboguy13]

@xich So I'm talking to some people in #ghc and it sounds like the issue is that GHC doesn't like it when an unboxed value is being used directly in a recursive let expression, which is why it is okay with it before the case is eliminated (by case-elim-inline-scrutinee).

Would it make sense to add an error condition to case-elim-inline-scrutinee (or something more general) so that it doesn't eliminate a case if it is surrounded by a recursive let and the scrutinee has an unboxed type (I think I'm using that terminology correctly)? Also, should we remove the case-elim-inline-scrutinee from the factorial example?

[xich]

@roboguy13 Thanks for digging into this. Are you saying the let/app invariant has changed between 7.8 and 7.10 ("anymore")? As far as I know, this restriction has always been in place, and we were just avoiding it before. Perhaps it has only recently been included in Lint checking and we've been lucky to this point?

As for actually fixing it, you're right that modifying case-elim-inline-scrutinee is the solution. GHC provides the following function: needsCaseBinding :: Type -> CoreExpr -> Bool which can be used as a predicate on the scrutinee. If needsCaseBinding returns true, then the case elimination rewrite should fail with the appropriate message.

Case s w ty alts <- idR
guardMsg (needsCaseBinding (exprType s) s) "scrutinee has unlifted type"
...

https://downloads.haskell.org/~ghc/latest/docs/html/libraries/ghc/CoreUtils.html#v:needsCaseBinding

This is the function that GHC uses internally to maintain the invariant.

Also, any other rewrites that eliminate case expressions probably also need to be considered, with this check added.

[roboguy13]

@xich I'm not sure. I was really just assuming that it had changed, but that might not be the case.

Would it be better to add the checks to caseElimR, caseReduceLiteralR, caseReduceDataconR? Those three seem to be used internally by the commands in the two examples here.

[xich]

caseElimR completely eliminates the scrutinee expression, so it shouldn't cause a violation.

The essence of the problem is when the scrutinee gets inlined via the case binder. That is:

case s of w
  ps -> rhss

If the rewrite substitutes s for w in rhss (or binds it as let w = s in ...), then the invariant can be violated. The case reduction rewrites do this substitution, so they will need a check. Another source of the problem will be caseInlineScrutineeR, which is used by many others.

Thinking about it more, perhaps a better solution is to address this in our substitution functions. We currently have:

substCoreExpr :: Var -> CoreExpr -> CoreExpr -> CoreExpr
substCoreExpr v e1 e2 = ...

which replaces v in e2 with e1. Perhaps we add a check to see if needsCaseBinding (exprType e1) e1 and generate a case expression around e2 instead of doing the substitution.

substCoreExpr v e1 e2
    | needsCaseBinding (exprType e1) e1
      && v `elem` freeVarsExpr e2 = Case e1 v (exprType e1) [(DEFAULT, [], e2)]
    | otherwise = ... do the substitution ...

Thoughts?

(My biggest worry is being overly restrictive. It might be the case that some transformation relies on temporarily violating some invariant, as long as it is later restored, though I don't have a concrete example of that.)

[roboguy13]

@xich Would that silently succeed if the rewrite ends up doing nothing as a result? That seems like another possible issue (it seems like most of the time you have a command that does nothing in HERMIT, it gives an error).

This might be a bit more work to implement, but what if we generated an error if the invariant is violated and also provided a command ignore-let/app-inv that takes a list of rewrites and ignores the let/app invariant until all the rewrites in the argument are performed and then checks the invariant at the end?

[xich]

substCoreExpr isn't a rewrite... its an underlying utility function, so isn't required to fail (and by its type, can't really). Though that is a good point. The onus would be on callers to substCoreExpr to detect if something didn't change and then fail. That sounds like a lot of tricky work, so maybe not worth doing.

In the meantime, fixing caseInlineScrutineeR and the two case reduction rewrites will probably squash most issues... and we can review the other case rewrites.

I would hold off on adding the ability to ignore the invariant until we have a concrete case where we need to do so.

[roboguy13]

I tried changing caseInlineScrutineeR to

-- | Inline the case binder as the case scrutinee everywhere in the case alternatives.
caseInlineScrutineeR :: ( ExtendPath c Crumb, ReadPath c Crumb, AddBindings c
                        , ReadBindings c, HasEmptyContext c, MonadCatch m, MonadUnique m )
                     => Rewrite c m CoreExpr
caseInlineScrutineeR = prefixFailMsg "case-inline-scrutinee failed: " $ do
  Case expr _bnds ty _alts <- idR              -- Added lines
  guardMsg (needsCaseBinding ty expr)          --
           "case scrutinee cannot be inlined." --
  caseInlineBinderR Scrutinee

but it is causing the factorial example to fail even sooner. It fails on the ww-split call with the error:

Error in expression: ww-split [| wrap |] [| unwrap |] (ww-AssA-to-AssC WWA)
Rewrite failed:worker/wrapper factorisation failed: verification of worker/wrapper assumption C failed: equality verification failed: Error in script expression: any-bu case-elim-merge-alts
anybuR failed

Did this make the checking too strict? Or maybe this is a concrete case where it is useful to have a way to temporarily ignore the invariant?

[xich]

The call to needsCaseBinding is at the wrong type. The type associated with Case (ty in your code) is the type of the alternatives (the type of the overall case expression, not the scrutinee). The guard should be:

guardMsg (needsCaseBinding (exprType expr) expr) "case scrutinee cannot be inlined because doing so would violate the let/app invariant."

[roboguy13]

Hmm, even with that change it gives the same error on ww-split.