fix: make the stack handling more robust to sanitizers and `-O3`

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.75k stars 427 forks source link

Closed eric-wieser closed 6 days ago

eric-wieser commented 1 week ago

This PR should make lean better-behaved around sanitizers, per https://github.com/google/sanitizers/issues/1688. As far as I can tell, https://github.com/google/sanitizers/wiki/AddressSanitizerUseAfterReturn#algorithm replaces local variables with heap allocations, and so taking the address of a local is not effective at producing a monotonic measure of stack usage.

The approach used here is the same as the one used by clang.

leanprover-community-bot commented 1 week ago

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b30903d1fcae504013d493c8d15f368a62e0e89e --onto 4600bb16fcded0356d20ae232e7f8580c56a5955. (2024-11-20 22:14:43)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b30903d1fcae504013d493c8d15f368a62e0e89e --onto 7fbe8e3b36faabc9cfcc45e65a4b7ef042c0b068. (2024-11-21 10:17:47)

eric-wieser commented 1 week ago

I guess this should be changelog-other?

Kha commented 6 days ago

changelog-compiler mentions "runtime", let's go with that :)