Stack overflow in for loops?

Stream: lean4

[Frédéric Dupuis]

I have just failed to solve today's Advent of Code problem with a very strange issue. You can have a look at the full code here. The main loop for Part 2 looks like this:

  let modulo : UInt64 := monkeys.foldl (fun n mon => n * mon.test) 1
  let n := monkeys.size
  let mut monkeyActivity : Array Nat := Array.mkArray n 0
  for rnd in [1:numRounds+1] do
    if rnd % 100 == 0 then dbg_trace s!"Starting round {rnd}, {monkeys.foldl (fun n m => n + m.items.size) 0}"
    for m in [0:n] do
      for i in monkeys[m]!.items do
        monkeyActivity := monkeyActivity.modify m (· + 1)
        let i' := (monkeys[m]!.op i) % modulo
        if i' % monkeys[m]!.test == 0 then
          monkeys := monkeys.modify monkeys[m]!.ifTrue (fun _ => monkeys[monkeys[m]!.ifTrue]!.catchItem i')
        else
          monkeys := monkeys.modify monkeys[m]!.ifFalse (fun _ => monkeys[monkeys[m]!.ifFalse]!.catchItem i')
      monkeys := monkeys.modify m (fun _ => monkeys[m]!.flushItems)

So basically just a few nested for loops whose body should run in constant time (in numRounds). However, what happens when I run this for 10000 rounds is that it progressively gets slower and slower until I get a stack overflow at round ~9200. I have no idea how a stack gets involved here.

@Sebastian Ullrich, maybe you would have a quick answer for this? I see you wrote nearly the same code, except that in your solution the items are not inside the Monkey structure.

[Sebastian Ullrich]

Do you have a stack trace, say with gdb?

[Gabriel Ebner]

My bet would be on the dbg_trace:

#eval dbg_trace s!"{List.range 10000}"; 42 -- stack overflow

[Frédéric Dupuis]

Gabriel Ebner said:

My bet would be on the dbg_trace:

#eval dbg_trace s!"{List.range 10000}"; 42 -- stack overflow

Nope -- removing it doesn't change anything...

[Frédéric Dupuis]

Here's the stack trace from gdb (assuming I did this correctly):

#0  0x0000555558561788 in lean_inc(lean_object*) ()
#1  0x0000555558560f85 in lean_apply_1 ()
#2  0x0000555558560f90 in lean_apply_1 ()
#3  0x0000555558560f90 in lean_apply_1 ()
#4  0x0000555558560f90 in lean_apply_1 ()
#5  0x0000555558560f90 in lean_apply_1 ()
#6  0x0000555558560f90 in lean_apply_1 ()
#7  0x0000555558560f90 in lean_apply_1 ()
#8  0x0000555558560f90 in lean_apply_1 ()
#9  0x0000555558560f90 in lean_apply_1 ()
#10 0x0000555558560f90 in lean_apply_1 ()

and it just keeps going like this forever.

[Frédéric Dupuis]

(This is without the dbg_trace line btw.)

[Gabriel Ebner]

Hmm that is strange. Either way lean4#1944 for the ToString instance.

[Frédéric Dupuis]

Nice -- now I can claim that doing AoC is not 100% procrastination :-)

[Gabriel Ebner]

This is an interesting bug. :smile: Here's an MWE, you can probably spot what's going wrong:

structure Monkey where
  items : Array Nat
  op : Nat → Nat

set_option trace.compiler.ir.result true in
def Monkey.catchItem (item : Nat) (monkey : Monkey) : Monkey :=
  { monkey with items := monkey.items.push item }

def f (n : Nat) : Monkey := Id.run do
  let mut monkey : Monkey := { items := #[], op := (· + 42) }
  for i in [:n] do
    monkey := monkey.catchItem i
  return monkey

#eval (f 10000).op 0 -- stack overflow

[Sebastian Ullrich]

Good thing I started exactly the same way but decided to factor out the mutable field halfway through because I didn't want to deal with the nested update :grimacing: ...

[James Gallicchio]

Is there an issue tracking this? I ran into a similar stack overflow from for loop in my code base, on a relatively recent toolchain.

[James Gallicchio]

ah, nevermind -- the stack overflow was coming from filterMap not being tail recursive

[James Gallicchio]

plot twist, I lied -- even with Std's tailrec filterMap, I get a stackoverflow, and I have a very funky MWE :big_smile:

structure Solver (m : Type → Type v) where
  solve : [Monad m] → m Unit

def DimacsCommand (cmd : String) : Solver IO :=
  ⟨do
  let child ← IO.Process.spawn {
    cmd := cmd
  }
  for _ in [0:10000] do
    IO.println "hi"
  ⟩

def mwe : IO Unit :=
  (DimacsCommand "cadical").solve

#eval mwe

This is on leanprover/lean4:nightly-2023-08-23, let me test it on stable

[James Gallicchio]

yep, still causes stackoverflow or bug on 4.0.0

[Sebastian Ullrich]

Why would you put the Monad argument in the field instead of the structure signature?

[James Gallicchio]

I don't remember :melt: but I remember there being a reason, because it used to be the other way. This is heavily, heavily minimized from LeanSAT.

[James Gallicchio]

(and the eval hangs infinitely instead of stack-overflowing if the monad argument is removed!)

[James Gallicchio]

although you can specialize m:

structure Solver where
  solve : Monad IO → IO Unit

def DimacsCommand (cmd : String) : Solver :=
  ⟨fun _m => do
  let _child ← IO.Process.spawn {
    cmd := cmd
  }
  for _ in [0:10000] do
    IO.println "hi"
  ⟩

#eval (DimacsCommand "ls").solve inferInstance

(also put in a command that most people have...)

[Sebastian Ullrich]

Yes, the problem is not m but the unknown instance