structure inline in rec functions

Stream: lean4

[James Gallicchio]

there's a pretty common pattern in String code of inlining the fields of Substring in the implementations of certain functions, presumably because it avoids the cost of constructing and deconstructing the structures. But this manual inlining is a bit of a pain and makes it harder to prove anything about their behavior... do we think this is a reasonable future optimization for the compiler to perform? it doesn't seem too complicated in the common case.

[Sebastian Ullrich]

If the Substring is stack-allocated by an escape analysis, LLVM should do the destructuring itself I think. Or maybe it only does if the symbol is internal

[James Gallicchio]

oh cool!

[James Gallicchio]

Then maybe I should stop manually inlining these substrings and do some tests instead :joy:

[Mario Carneiro]

Don't worry, I will do it if you don't

[Sebastian Ullrich]

Note that I said "an escape analysis", we don't have one yet :)

[James Gallicchio]

I assume LLVM has an escape analysis on llvm ir, maybe the llvm backend of the compiler is sufficient to get this optimization automatically??

[Mario Carneiro]

I am fairly pessimistic about LLVM's ability to remove lean allocations

[Mario Carneiro]

looking at the code, lean_alloc_small isn't even an LLVM approved malloc, so LLVM would be duty-bound to preserve any effects on the local allocator caused by the allocation function

[Sebastian Ullrich]

I believe this would require use of the alloc-family LLVM IR annotation (e.g.), which doesn't seem to be exposed by clang. So it would need to happen in the LLVM backend /cc @Siddharth Bhat @Tobias Grosser