Opened 6 months ago

Closed 6 months ago

#15110 closed bug (fixed)

Exitification abstracts over shadowed variables

Reported by: nomeata Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.5
Keywords: JoinPoints Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Simon did some code review of Exitify.hs in https://ghc.haskell.org/trac/ghc/ticket/14152#comment:36 and he was onto something; the code is wrong after all:

Consider this core term

  joinrec j (x :: Bool) (x :: Int) =
    if x == 0
    then foo x
    else jump j True (x - 1)
  in …

where the two parameters x and x are different variables, but shadow each other (i.e. have the same unique). This is legal Core!

But Exitification chooses the variables to abstract over in this line:

        -- The possible arguments of this exit join point
        -- No need for `sortQuantVars`, `captured` is already in dependency order
        abs_vars = map zap $ filter (`elemVarSet` fvs) captured

where captured = [x::Bool,x::Int] in this case, which would yield this code

  join exit (x :: Bool) (x :: Int) = foo x in
  joinrec j (x :: Bool) (x :: Int) =
    if x == 0
    then jump exit (x::Bool) (x::Int)
    else jump j True (x - 1)
  in …

which is no longer type correct (or even “scope-correct”) any more, as it passes the Int-typed x as the Bool argument to exit.

The conditions where this happens, i.e. such shadowing, is rather obscure so I did not even try to produce a lint error here. It also means that this is rather low severity, but I’ll still go and fix it.

An application of reverseNub seems to be in order – or simply switching to keeping captured in a DVarSet rather than a list (in which case sortQuantVars would be required…)

Change History (4)

comment:1 Changed 6 months ago by simonpj

Ha, quite true -- although you give me too much credit for spotting it.

NB: in your explanation (which should end up in a Note, be sure to point out that Core distinguishes variables by their Unique so their OccName is irrelevant. What you write should be understood to mean that the two x's are variable with the same Unique, rather than with the same OccName. It's difficult to make this happen, and the Simplifier removes such shadowing, but yes, it's valid.

Easy fix:

abs_vars = map zap proto_abs_vars
(proto_abs_vars, _) = foldr add ([], fvs) captured
add v (acc, fvs) = (acc', fvs `delVarSet` b)
  where
    acc' | v `elemVarSet` fvs = v : acc
         | otherwise          = acc

comment:2 Changed 6 months ago by simonpj

Keywords: JoinPoints added

comment:3 Changed 6 months ago by Joachim Breitner <mail@…>

In 60f9e46/ghc:

Exitify: Do not trip over shadowing (fixes #15110)

comment:4 Changed 6 months ago by nomeata

Resolution: fixed
Status: newclosed
Note: See TracTickets for help on using tickets.