Segmentation Fault with mutual, HashMap, and string interpolation

[ericluap]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The code has a segmentation fault when run.

Context

Here is a discussion on Zulip.

Steps to Reproduce

1. lake new test
2. cd test
3. Modify Main.lean to have the following contents

import Lean.Data.HashMap

mutual
inductive Foo
| Foo (bar : Bar)

inductive Bar
| Foo (foo : Foo)
| Baz (baz : String)
end

mutual
def eToString : Foo → String
| Foo.Foo c => cToString c

def cToString : Bar → String
| Bar.Foo e => eToString e
| Bar.Baz c => c

end
instance : ToString Foo := ⟨eToString⟩
instance : ToString Bar := ⟨cToString⟩

def update (_ : Nat × Nat) (_ : Array String) (w : Lean.HashMap (Nat × Nat) (Array String)) :=
  w.insert (0,0) #[]

def test (x : String) (y : Foo) (z : Lean.HashMap (Nat × Nat) (Array String)): Option (String × (Option String) × (Option String) × String × (Lean.HashMap (Nat × Nat) (Array String))) := do
  pure $ (
    ((toString (← (Array.filter (fun _ => true) #[y])[0]?)).split (· = '0')).getD 0 "",
    none,
    "",
    "",
    update (x.length, x.length) #[s!"{x}", s!"{x}"] z
  )


def main : IO Unit := pure ()

4. lake build
5. ./.lake/build/bin/test

Expected behavior: The code should compile and run.

Actual behavior: It produces a segmentation fault.

Versions

"4.10.0" and "4.12.0-nightly-2024-08-27"
macOS Monterey Version 12.4

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[kim-em]

I can reproduce. lldb doesn't give much clue:

% lldb ./.lake/build/bin/test 
(lldb) target create "./.lake/build/bin/test"
Current executable set to '/Users/kim/scratch/test/.lake/build/bin/test' (arm64).
(lldb) run
Process 65953 launched: '/Users/kim/scratch/test/.lake/build/bin/test' (arm64)
Process 65953 stopped
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x2000000000000)
    frame #0: 0x0000000100003238 test`initialize_Main + 544
test`initialize_Main:
->  0x100003238 <+544>: ldr    w8, [x19]
    0x10000323c <+548>: cmp    w8, #0x1
    0x100003240 <+552>: b.lt   0x10000329c               ; <+644>
    0x100003244 <+556>: add    w8, w8, #0x1
Target 0: (test) stopped.
(lldb) bt
* thread #1, queue = 'com.apple.main-thread', stop reason = EXC_BAD_ACCESS (code=1, address=0x2000000000000)
  * frame #0: 0x0000000100003238 test`initialize_Main + 544
    frame #1: 0x00000001000032cc test`main + 32
    frame #2: 0x000000019e3020e0 dyld`start + 2360
(lldb) 

[hargoniX]

Compiling this with -g as leanc args shows that we crash in this function:

static lean_object* _init_l_test___rarg___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; 
x_1 = l_update___rarg___closed__2;
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_array_fget(x_1, x_2);
return x_3;
}

At the fget call. This is because l_update___rarg___closed__2 is initialized with an Array of size 0 as evident by the code:

static lean_object* _init_l_update___rarg___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; 
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}

And the debugger:

(gdb) list
828	_start:
829	{
830	lean_object* x_1; lean_object* x_2; lean_object* x_3;
831	x_1 = l_update___rarg___closed__2;
832	x_2 = lean_unsigned_to_nat(0u);
833	x_3 = lean_array_fget(x_1, x_2);
834	return x_3;
835	}
836	}
837	LEAN_EXPORT lean_object* l_test___rarg(lean_object* x_1, lean_object* x_2) {
(gdb) p ((lean_array_object*)x_1)->m_size
$6 = 0
(gdb) p ((lean_array_object*)x_1)->m_capacity
$7 = 0

[hargoniX]

Looking into the IR the test function contains the following IR prior to closed subterm extraction:

  let _x_4 := Array.mkEmpty _neutral 0;
  let _x_5 := Nat.decLt 0 _x_3;
  Bool.casesOn _x_5
    (let _x_6 := Array.size _neutral _x_4;
    let _x_7 := Nat.decLt 0 _x_6;
    Bool.casesOn _x_7 (none _neutral)
      (let _x_8 := Array.get _neutral _x_4 0;
      @j_1._join _x_8))

What is probably happening here, is that the compiler pulled out Array.get x_4 0 because x_4 is a constant itself. This then gets evaluated in the initialize phase and subsequently crashes. I can offer the following temporary fix:

import Lean.Data.HashMap

mutual
inductive Foo
| Foo (bar : Bar)

inductive Bar
| Foo (foo : Foo)
| Baz (baz : String)
end

mutual
def eToString : Foo → String
| Foo.Foo c => cToString c

def cToString : Bar → String
| Bar.Foo e => eToString e
| Bar.Baz c => c

end
instance : ToString Foo := ⟨eToString⟩
instance : ToString Bar := ⟨cToString⟩

def update (_ : Nat × Nat) (_ : Array String) (w : Lean.HashMap (Nat × Nat) (Array String)) :=
  w.insert (0,0) #[]

set_option compiler.extract_closed false in
def test (x : String) (y : Foo) (z : Lean.HashMap (Nat × Nat) (Array String)): Option (String × (Option String) × (Option String) × String × (Lean.HashMap (Nat × Nat) (Array String))) := do
  pure $ (
    ((toString (← (Array.filter (fun _ => true) #[y])[0]?)).split (· = '0')).getD 0 "",
    none,
    "",
    "",
    update (x.length, x.length) #[s!"{x}", s!"{x}"] z
  )


def main : IO Unit := pure ()