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

[SchiJoha]

Implementation of three context-sensitive approaches to tam recursion:

• call string approach in the Sharir and Pnueli sense: a call stack tracking the last k function calls is 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.
• The context gas analyses 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]

We probably should tag a branch with the version used for the experiments and make a pre-release akin to what we did for longjmp[1] and a lightweight artifact as well. Not sure if we one cut a pre-release from a branch on a fork.

If not, we might have to pull this over to a branch on this repo.

1: https://github.com/goblint/analyzer/releases/tag/v2.1.0-longjmp

[sim642]

No need to overcomplicate the tagging: git is distributed after all. The tag can be created and pushed to the branch in the fork. If this PR is merged, the same commit will exist in this repo's history, so the very same tag can also be pushed here.

The most important thing is to just know the commit where the experiments are made (which is always in goblint --version). So the tag can even be recreated if need be.

[michael-schwarz]

Thanks for the reviews @sim642, we are currently in a bit of a time crunch to make it for SOAP, but we're factoring in some places where the intent of our approach was unclear, and will address the comments in detail some time after the deadline :smile:

(And when I say we will answer I mostly mean @SchiJoha probably :stuck_out_tongue:)

[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?