master thesis: Taming Recursion with Three Context-Sensitive Analyses (Callstring, LoopfreeCallstring, Context Gas)

[SchiJoha]

Implementation of three context-sensitive approaches to tame recursion:

• call string approach in the Sharir and Pnueli sense: a call stack tracking the last k function calls is simulated and used as context. As elements on the call stack, the function definitions (classical call string) or the statements (similar to call site) are used. We also enable the choice of k = infinity.
• Loopfree Callstring: similar to call string but with (1) the callee stored in the call stack and (2) loops of the call stack stored in a set. Consequently, the stack elements are function definitions and sets containing function definitions. Overall no function is stored twice in the stack.
• Context Gas: analyzes the first k calls on the call stack context-sensitive. The remaining calls receive no context information.

For the call-sequence main -> f -> g -> f -> g the approaches would have the following context (and gas):

• Callstring: (main)-> (main, f) -> (main, f, g) -> (main, f, g, f) -> (main, f, g, f, g)
• Loopfree: (main)-> (main, f) -> (main, f, g) -> (main, {f, g}) -> (main, {f, g})
• Context Gas (gas = 2): (Some (main-context)) gas 2 -> (Some (f context)) gas 1 -> (None) gas 0 -> (None) gas 0 -> (None) gas 0

[michael-schwarz]

Is this ready for a new review (and merging) or are there still things you're working on?

[SchiJoha]

Is this ready for a new review (and merging) or are there still things you're working on?

Yes! It should be ready for review :)

[michael-schwarz]

@jerhard @DrMichaelPetter do you still want to review this or should we merge it?

[jerhard]

Looks good! I only have some cosmetical suggestions for the code.