`isExclusiveUnsafe` crashes (SIGSEGV) on scalar arguments such as a small `Nat`
Maintainers usually reply within 1 day
Nobody has claimed this yet.
Assessment
- Difficulty
- 2/5
- Estimated time
- 1-3 hours
- Newbie friendliness
- 76/100
Research direction
The crash comes from lean_is_exclusive and lean_is_exclusive_obj in src/include/lean/lean.h (around lines 776-786), which read the reference count through lean_is_st without first checking lean_is_scalar. Look at how lean_dbg_trace_if_shared in src/runtime/object.cpp handles scalars and mirror that guard. Done when the repro's ./Repro small, ./Repro bool, and ./Repro unit print false and exit 0, and the interpreter run also succeeds.
Written by the indexing model from the issue text.
Description
Prerequisites
- 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
isExclusiveUnsafe {α : Type u} (a : @& α) : Bool accepts any type, but a scalar argument (a small
Nat, Bool, Unit, an enum, ...) is a tagged pointer (lean_box(5) == 0xb), not a heap object.
lean_is_exclusive dereferences it through lean_is_st without a lean_is_scalar test, so the
process dies with SIGSEGV. A scalar is not a heap object, hence the expected answer is false.
Context
Deciding whether a value is uniquely referenced, e.g. to mutate in place or copy. α is arbitrary, so
scalars are legitimate inputs. The safe wrapper proposed in RFC #15235 / PR #15323 also calls
isExclusiveUnsafe a, so it would crash on scalar arguments too.
Steps to Reproduce
Repro.lean:
unsafe def main (args : List String) : IO UInt32 := do
match args.head? with
| some "heap" => IO.println (isExclusiveUnsafe (2 ^ 70 : Nat)); return 0
| some "small" => IO.println (isExclusiveUnsafe (5 : Nat)); return 0
| some "bool" => IO.println (isExclusiveUnsafe (true : Bool)); return 0
| some "unit" => IO.println (isExclusiveUnsafe (() : Unit)); return 0
| _ => IO.println "usage: Repro <heap|small|bool|unit>"; return 1
lean Repro.lean -c Repro.c && leanc -O1 -o Repro Repro.c, then./Repro heap,./Repro small,
./Repro bool,./Repro unit. (lean --run Repro.lean smallcrashes in the interpreter as well.)
Expected behavior: every run prints a Bool and exits 0 — false for the scalar cases.
Actual behavior:
$ ./Repro heap
false
$ ./Repro small
Segmentation fault (core dumped) # exit 139; same for bool, unit, and the interpreter
Versions
Lean (version 4.36.0-nightly-2026-10-13, x86_64-unknown-linux-gnu, commit b7725c34da98e6e2f6323d7f382448ddf31477fb, Release)
Linux 7.0.0-38-generic (x86_64)
Additional Information
lean_is_exclusive (lean.h:776-782) reads o->m_rc through lean_is_st (lean.h:635-637) without a lean_is_scalar (lean.h:361) test; it reaches isExclusiveUnsafe via lean_is_exclusive_obj (lean.h:784-786, Init/Util.lean:98-99).
Fix — test for a scalar first, as lean_dbg_trace_if_shared already does (object.cpp:2872-2877):
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
- Dominant language
- Lean
- Stars
- 9.6k
- Forks
- 1.1k
- Avg merge
- 1d 17m
- Merged PRs (30d)
- 296
Getting set up
- No Dockerfile or Docker Compose file
- Has a pull request template
- Read the contributing guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from leanprover/lean4
-
`IO.appPath` fails when `/proc` belongs to another PID namespacePossibly taken @treiher claimed this 6 days ago. Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/lean4#15692 · 3 reactions ·
Maintainers usually reply within 1 day
-
`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 66/100
leanprover/lean4#15683 ·
Maintainers usually reply within 1 day
-
`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
leanprover/lean4#15681 ·
Maintainers usually reply within 1 day
-
`Child.takeStdin` loses `setsid`, so `Child.kill` only signals the child, not its process groupOpenbug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/lean4#15674 ·
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 82/100
leanprover/lean4#15626 ·
Maintainers usually reply within 1 day
All issues in leanprover/lean4
Similar issues
-
Slang input: int8_t4_packed and uint8_t4_packed are copied into CrossGLPossibly taken @ninglinLiu claimed this 1 day ago. Openarea:frontend backend:slang bug direction:input
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
CrossGL/crosstl#2801 · 1 comment ·
Maintainers usually reply within 1 day
-
Decompiler: convertCharRef() in xml.y overflows its int4 accumulator on long character referencesPossibly taken @kaayzouee claimed this 1 day ago. Open
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
NationalSecurityAgency/ghidra#10009 ·
Maintainers usually reply within 2 days
-
Difficulty 2/5 Under an hour Newbie friendliness 85/100
MoonshotAI/kimi-code#4367 ·
Maintainers usually reply within 1 day
-
clang:frontend code-cleanup HLSL
Difficulty 2/5 1-3 hours Newbie friendliness 74/100
llvm/llvm-project#235100 · 1 comment ·
Maintainers usually reply within 1 day
-
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
paritytech/polkavm#442 ·