Segfault from code that doesn't even get executed

Stream: lean4

[Frédéric Dupuis]

I hit a very bizarre bug today: the following innocuous-looking code segfaults when attempting to run the compiled version:

import Parser.Char

def foobar : TrivialParser Substring Char (Option Char) := do
  let foo ← Parser.sepBy (Parser.Char.chars " ") Parser.anyToken
  if h : foo.size < 1 then return none
  else return some foo[0]

def main : IO Unit :=
  IO.println s!"Hello!"

This only happens when running the compiled code, everything looks fine in VSCode. It also goes away if one uses foo[0]! instead of the proof with h in foobar. Note that the offending code doesn't even get executed here -- it just sits there.

The Parser library above is @François G. Dorais's parser library; unfortunately I haven't managed to get an MWE without this dependency (I tried switching to different monads and so on, to no avail).

In any case, the bug can be reproduced on a fresh new Lean repo on version 4.15.0-rc1, with the above in Main.lean, and the following in lakefile.lean:

import Lake
open Lake DSL

package «mwe» where
  -- add package configuration options here

@[default_target]
lean_lib «Mwe» where

@[default_target]
lean_exe mwe where
  root := `Main
  -- Enables the use of the Lean interpreter by the executable (e.g.,
  -- `runFrontend`) at the expense of increased binary size on Linux.
  -- Remove this line if you do not need such functionality.
  --supportInterpreter := true

require Parser from git "https://github.com/fgdorais/lean4-parser" @ "main"

I can work around it of course, but I thought I would report this here.

[François G. Dorais]

Looks like a compiler error. The C output has a couple of suspicious things but I haven't been able to pinpoint the issue.

[Frédéric Dupuis]

Yeah, that's what it looks like.

[François G. Dorais]

I'll try some debugging but this is likely over my head. The import might be necessary for a MWE (though not this specific import :smile:). My guess is that since the import is not actually used, some parts of initialization get optimized out and later init code unexpectedly tries to access an invalid memory location.

[Mario Carneiro]

the symptoms sound similar to lean4#1965