manyAux is not tail-recursive

Stream: lean4

[Mario Carneiro]

I'm still not entirely sure I have this correct, but I have a perf report containing a huge stack of calls to docs#Lean.Parser.manyAux when parsing a very long list of commands using a syntax similar to a mutual block. The only reasonable conclusion is that manyAux is not tail-recursive, even though it is written in a style that implies it should be

[Mario Carneiro]

oh and indeed the IR reveals that it is not - one sided if strikes again

def Lean.Parser.manyAux._lambda_2 (x_1 : obj) (x_2 : obj) (x_3 : @& obj) (x_4 : obj) (x_5 : @& obj) : obj :=
  let x_6 : obj := 1;
  let x_7 : obj := Nat.add x_3 x_6;
  let x_8 : obj := Lean.Parser.ParserState.stackSize x_4;
  let x_9 : u8 := Nat.decLt x_7 x_8;
  dec x_8;
  dec x_7;
  case x_9 : u8 of
  Bool.false →
    let x_10 : obj := Lean.Parser.manyAux x_1 x_2 x_4;
    ret x_10
  Bool.true →
    let x_11 : obj := Lean.Parser.optionalFn._closed_2;
    let x_12 : obj := Lean.Parser.ParserState.mkNode x_4 x_11 x_3;
    let x_13 : obj := Lean.Parser.manyAux x_1 x_2 x_12;
    ret x_13
def Lean.Parser.manyAux._lambda_3 (x_1 : obj) (x_2 : obj) (x_3 : @& obj) (x_4 : @& obj) (x_5 : obj) (x_6 : @& obj) : obj :=
  let x_7 : obj := proj[2] x_5;
  inc x_7;
  let x_8 : u8 := Nat.decEq x_4 x_7;
  dec x_7;
  case x_8 : u8 of
  Bool.false →
    let x_9 : obj := ctor_0[PUnit.unit];
    let x_10 : obj := Lean.Parser.manyAux._lambda_2 x_1 x_2 x_3 x_5 x_9;
    ret x_10
  Bool.true →
    dec x_2;
    dec x_1;
    let x_11 : obj := ctor_0[List.nil];
    let x_12 : obj := Lean.Parser.manyAux._lambda_3._closed_1;
    let x_13 : u8 := 1;
    let x_14 : obj := Lean.Parser.ParserState.mkUnexpectedError x_5 x_12 x_11 x_13;
    ret x_14
def Lean.Parser.manyAux (x_1 : obj) (x_2 : obj) (x_3 : obj) : obj :=
  let x_4 : obj := Lean.Parser.ParserState.stackSize x_3;
  let x_5 : obj := proj[2] x_3;
  inc x_5;
  inc x_1;
  inc x_2;
  let x_6 : obj := app x_1 x_2 x_3;
  let x_7 : obj := proj[4] x_6;
  inc x_7;
  let x_8 : obj := ctor_0[Option.none];
  let x_9 : u8 := _private.Init.Data.Option.Basic.0.Option.beqOption.«_@».Init.Data.Option.Basic._hyg.159._at.Lean.Parser.ParserState.hasError._spec_1 x_7 x_8;
  case x_9 : u8 of
  Bool.false →
    dec x_2;
    dec x_1;
    let x_10 : obj := proj[2] x_6;
    inc x_10;
    let x_11 : u8 := Nat.decEq x_5 x_10;
    dec x_10;
    case x_11 : u8 of
    Bool.false →
      dec x_5;
      dec x_4;
      ret x_6
    Bool.true →
      let x_12 : obj := Lean.Parser.ParserState.restore x_6 x_4 x_5;
      dec x_4;
      ret x_12
  Bool.true →
    let x_13 : obj := ctor_0[PUnit.unit];
    let x_14 : obj := Lean.Parser.manyAux._lambda_3 x_1 x_2 x_4 x_5 x_6 x_13;
    dec x_5;
    dec x_4;
    ret x_14

[Mario Carneiro]

This is the code for manyAux:

partial def manyAux (p : ParserFn) : ParserFn := fun c s => Id.run do
  let iniSz  := s.stackSize
  let iniPos := s.pos
  let mut s  := p c s
  if s.hasError then
    return if iniPos == s.pos then s.restore iniSz iniPos else s
  if iniPos == s.pos then
    return s.mkUnexpectedError "invalid 'many' parser combinator application, parser did not consume anything"
  if s.stackSize > iniSz + 1 then
    s := s.mkNode nullKind iniSz
  manyAux p c s

I have seen this issue before, the fix is to avoid early return in this kind of code because it generates lambdas for the join points that become part of a mutual tail recursion, which the code generator does not support

partial def manyAux (p : ParserFn) : ParserFn := fun c s => Id.run do
  let iniSz  := s.stackSize
  let iniPos := s.pos
  let mut s  := p c s
  if s.hasError then
    return if iniPos == s.pos then s.restore iniSz iniPos else s
  else if iniPos == s.pos then
    return s.mkUnexpectedError "invalid 'many' parser combinator application, parser did not consume anything"
  else if s.stackSize > iniSz + 1 then
    s := s.mkNode nullKind iniSz
  manyAux p c s

[Mario Carneiro]

cc: @Sebastian Ullrich

[Marc Huisinga]

I came across this when optimizing the JSON parser a bit as well (lean4#4900), though the effect there was mostly just slower code.

[Mario Carneiro]

I did not get a stack overflow, but parsing was suspiciously slow (like, minutes)

[Joachim Breitner]

yup, ran into this issue with early return braking tail recursion as well recently.

[Kim Morrison]

Do we have an issue tracking this?

[Yury G. Kudryashov]

Should we have a linter that flags recursive but not tail-recursive functions? Is it possible to figure out in a linter?

[Yury G. Kudryashov]

IMHO, having to explicitly say "yes, I know that this function isn't tail-recursive" is a low price for avoiding footguns (but I don't know if such a linter is possible).

[Damiano Testa]

What does tail recursive mean?

[Henrik Böving]

Yury G. Kudryashov said:

IMHO, having to explicitly say "yes, I know that this function isn't tail-recursive" is a low price for avoiding footguns (but I don't know if such a linter is possible).

The linter would have to inspect the IR not the surface level code. But yes its possible to do such things. However I'd say it should only check whether the function is TR if explicitly asked so, there are lots of non tail rec functions and lots of valid reasons to write them in Lean

[Henrik Böving]

Damiano Testa said:

What does tail recursive mean?

That the recursive call of a function is the last thing that happens, that allows a sufficiently smart compiler to turn the function into a loop instead of consuming stack space.

[Damiano Testa]

Ok, checking that the last line is a call to the function itself and that no call to the function happened earlier should be relatively easy. Is that really all that there is to it, or are there other issues?

[Henrik Böving]

As you can see in this thread no that's not at all enough. You have to inspect the IR for this.

[Henrik Böving]

And again this should not be a default thing that runs on all functions, there is plenty of valid reasons to write non tail rec functions in lean

[Damiano Testa]

Ok, so would it be enough that the function is never called before the last line of all the declarations that are generated by the given one?

[Henrik Böving]

If you want to make absolutely sure something like that for looking at the closure of IR declarations generated by the function in question would probably work yes.

[Henrik Böving]

Though that's quite an over approximation given that there is lots of specialization happening so it will perform sub optimally on large code bases

[Damiano Testa]

Are IR declaration just regular declarations that are added to the environment, just some you would usually never inspect?

[Henrik Böving]

No they are fundamentally different. They're stored in an environment extension using a custom IR type. Leans IR is different (though not very different) from Expr or Syntax.

[Damiano Testa]

Ok, I would need to learn about that. It is a regular environment extension and it will have its underlying inductive, right? This is what I gather from your message.

[Henrik Böving]

Yes, there's also 3 different stages stored in the environment, you most likely only want to check the last

[Damiano Testa]

Ah, these are the declarations that I sometimes see ending in stageN?

[Henrik Böving]

But again, this should not be a check enabled by default, there are many valid reasons to have non tail rec functions. It should be an on demand check.

[Damiano Testa]

Yes, I understand. However, before the check is not enabled by default, it should exist! :smile: