This will allow us to statically allocate stack space with a tighter bound. The Hafnium codebase uses bounded recursion, so we might have to do this in two steps:

• Compute maximum stack size on the assumption that the recursion bounds hold.
• Actually prove the recursion bounds.

sashabu@ said: I don't think I'll have time to work on this.

dbrazdil@ said: This is a nice-to-have. I'll leave it open so it can be suggested to Arm but not critical to Hafnium's functionality.
I've previously experimented with clang to get an upper bound (tricky because it doesn't cover intrinsics) and a script in the Linux tree which looks at the assembly (very conservative). Neither seemed good enough for production.

(Migrated from b/119558941.)