TUM Practical Course Summer 2023: Termination Analyses

[Nimmseasy]

Implementation of a sound termination analyses for single-threaded programs.
We handle 2 possible causes for non-termination:

1. loops inside a function: We add a loop-counter variable to the CIL code after any loop head found in the CIL code and check it by assigning it in a special statment to another variable wich then is then locatet by goblints transfer functions. We run the apron analyses (either with polyhedra or octagon domain so far) to get the interval of our loop-counter Variable and see if its bounded => if its bounded we dont have an infinit loop.
   For goto statements we cant proof non termination, if they jump up in the codelines.
2. recursion or call graph cycles: We build a context-sensitive call graph by defining a global invariant
   (callee_function-> (callee-context -> (caller_function, caller_context) and filling it as we analyse the program, and then search
   for cycles in this build callgraph.

If the program gets multithreaded we cant proof non termination.

[sim642]

What's with the test failures in CI?

[sim642]

What's with the test failures in CI?

I see that the test failures are timeouts somehow related to function size. But our regression tests are tiny. Is this termination analysis really that inefficient that it struggles so much on 100-line programs?

[jerhard]

I see that the test failures are timeouts somehow related to function size. But our regression tests are tiny. Is this termination analysis really that inefficient that it struggles so much on 100-line programs?

The analysis relies on our relational analyses, and for most test cases uses polyhedra. The termination analysis introduces one counter variable per loop, so a polyhedra-based termination analysis does not scale well with functions containing multiple loops.

[sim642]

I suppose we'll have to implement variable packing which everyone else has been doing for decades.

If nothing concerning shows up in our own preruns with termination analysis, I think this should be good enough to finally merge.

[jerhard]

I had to make a change so that the termination analysis is activated earlier by the autotuner if the autotuner is active and we have to analyze for termiation, as the termiation analysis needs to be activated before the preprocessing is done (to instrument the program with loop counter variables).

Additionally I had to add a handling if the loop unrolling encounters a all to goblint_bounded (the special function where the boundedness of the loop is checked); now loops that contain such a check are also unrolled.

[jerhard]

I reran this PR with the svcomp.json configuration from this branch on the latest version of sv-comp termination tasks and this yields 567 correct verdicts (and no incorrect ones). The increased number of correct tasks may be due to using more memory (15GB instead of 3GB) and a different configuration (previous runs did not use the autotuner).

Regarding sv-comp: the programs analyzed are contained some artificial loop counters. Since the Termination category is excluded from the validation of correctness witnesses, this should not be a problem, right?

[sim642]

All the non-Apron CI jobs are now failing on master: https://github.com/goblint/analyzer/actions/runs/6917734602. A condition might be missing somewhere.

[michael-schwarz]

Should be fixed, there was a check missing to only run the termination regression tests in configs in which Apron is present.