4 ms·
If hard realtime and stack space are part of your constraints, then recursive constructions are in fact always harder to reason about.
by AnimalMuppet 2y ago
If hard realtime and stack space are part of your constraints, then recursive constructions are in fact always harder to reason about.
- ajross 2y agoTo clarify: it's not stack "space" that's at issue. It's the requirement that the lack of stack overflow at runtime be formally verified. If functions exist in a static call tree[1] you can do this with a little disassembly wizardry and a few hundred lines of python. If you allow them to call themselves recursively, or even to indirect through a function pointer, it becomes undecidable. [1] There are some other related rules like "no alloca()".
- rcxdude 2y agoFunction pointers are possible to deal with, with varying levels of automation. You can detect when pointers to functions are taken, and tie them to call sides with type information or some manual work (I have a static analysis tool which allows function pointers for callbacks by linking functions passed into one function to the list of possible destinations for a given callsite). Recursion is harder but it's still possible in principle to prove a bound in a lot of cases, given a proof framework. Not something I'd encourage, though.