`longjmp` in abstract call graph/ARG

[sim642]

The termination analysis uses an abstract call graph to detect cycles from recursion. As far as I know, this graph does not contain edges corresponding to longjmp flows. Instead, the termination analysis gives up on any longjmp and considers the program as possibly non-terminating.

I wonder if it would be possible to have longjmp-aware termination analysis if the abstract call graph also indicated these flows in some way.
It's possible to have longjmp-based loops, but these are artificially constructed examples. I imagine realistic longjmp usage wouldn't do such things.

Even if this isn't enough to improve termination analysis, these flows could still make sense for some usability things. The (abstract) call graph reflects what calls what and conversely normal returns. In that sense it would make sense to also indicate the abnormal returns via longjmp.

(It would be even better to have them in the ARG for abstract debugging but that might not be so simple because both longjmp and ARG construction are separate Spec lifters.)

[michael-schwarz]

I think the reason why we didn't consider it so far is because Goblint's termination analysis suffers from more obvious shortcomings: Such issues are, e.g., meaningful support for discovering that some recursive functions always terminate (requiring some relational analyses about entry and exist states). Supporting the termination analysis of programs using setjmp/longjmp seemed low prio.

Simply adding such an edge to the context-enhanced callgraphs is not helpful here: Inside the call graph all program points are collapsed, so as soon as longjmp occurs (say back into f from g), you will have a cycle f->g->f.

To be helpful, these context-enhanced callgraphs would need to distinguish the parts of f based on the return value of setjmp. Alternatively you could track a bit may come after return via longjmp for all program points reached after a return into the function via longjmp, and the somehow disregard edges where this bit is not set when doing cycle detection.

While doable, this sounds quite exotic --- even more than our first longjmp paper. Not sure if one can write a paper about it...

[michael-schwarz]

Come to think of it, maybe non-termination due to sj/lj is better understood in terms of our termination analysis of loops:

The question is whether the setjmp forms part of a loop and whether that loop can be bounded. The fact that the return happens via longjmp is only relevant in the sense that execution continues somewhere else than the invocation of the function (transitively) doing the longjmp, but the framework does that for us.

I'm starting to suspect that the only thing that is needed is some instrumentation à la:

volatile unsigned int  longjmp__bounded;

if(!setjmp(buff,val)) {
    longjmp__bounded++;
    goblint__check_bounded(longjmp__bounded);

   ....

}
....

[sim642]

Simply adding such an edge to the context-enhanced callgraphs is not helpful here: Inside the call graph all program points are collapsed, so as soon as longjmp occurs (say back into f from g), you will have a cycle f->g->f.

To be helpful, these context-enhanced callgraphs would need to distinguish the parts of f based on the return value of setjmp. Alternatively you could track a bit may come after return via longjmp for all program points reached after a return into the function via longjmp, and the somehow disregard edges where this bit is not set when doing cycle detection.

Indeed, these flows might make more sense in the ARG.
On the other hand, we could also do the recursion detection with the ARG, not its abstraction to a call graph. In that case it might also help. Not sure if it helps in any other case though.

Come to think of it, maybe non-termination due to sj/lj is better understood in terms of our termination analysis of loops:

Perhaps. I only started thinking about why longjmp isn't in any of our abstract graphs and then what that could be useful for (termination). But the termination thing might be easier improved in different ways.

[michael-schwarz]

On the other hand, we could also do the recursion detection with the ARG, not its abstraction to a call graph.

Iirc, ARG construction at some point was an insane amount of overhead. Has this changed?

[sim642]

I think most of the overhead should be after solving when generating the GraphML witness, which requires ARG nodes to be lifted with call stacks. Just collecting the data for ARG construction does not do that.
For example, the abstract debugger uses the ARG directly without that lifting and does its own stack reconstruction on the fly (just to have a call stack view).

Also, in SV-COMP we have it enabled anyway.