a tactic to induce a crash?

Stream: general

[Scott Morrison]

I recently wanted to induce crashes in the Lean server, to test interactions with VS Code. I wrote the following tactic that causes the server the crash. If anyone else would find it useful:

@[user_attribute]
meta def sigbus_attribute : user_attribute unit unit := {
  name := `sigbus,
  descr := "An attribute to help generate SIGBUS crashes, for debugging IDE interactions.",
  cache_cfg :=
   { mk_cache := λ ls, sigbus_attribute.get_cache,
     dependencies := [] }
}

meta def sigbus : tactic unit := sigbus_attribute.get_cache

-- run_cmd sigbus

[Scott Morrison]

(Actually --- does mathlib even want this?)

[Mario Carneiro]

what?

[Mario Carneiro]

is this a bug in lean, or a documented API?

[Mario Carneiro]

I don't see what's supposed to cause the crash

[Scott Morrison]

Sorry. :-) Maybe this is dumb. It's an "inevitable" bug --- we call the attribute cache, which calls itself ad infinitum, causing a crash.

[Mario Carneiro]

why would that cause a crash? That sounds like a stack overflow or something

[Scott Morrison]

It was just the first reproducible crash I could think of.

[Mario Carneiro]

and it should certainly not take the server down

[Mario Carneiro]

it's a bit worrisome that lean has a plethora of bug conditions ready for exploitation

[Scott Morrison]

Ok. maybe this is just a random bug that will never be fixed, then. I found it useful while fixing elan installation from VS Code today. :-)

[Scott Morrison]

There are certainly some parser related crashes still around, although I haven't found a reproducible one in a while. Something in structure parser is wonky, I think.

[Keeley Hoek]

I get a SIGSEGV on linux with that. I don't think these kind of compiler bugs fall into the realm of a security vulnerability though, since if an attacker had control of a source file being compiled they could execute arbitrary code anyway