Implement delayed widening

[RonaldJudin]

This implements standard widening delay in-domain as suggested by #1442 (comment) and #1442 (comment).
The two separate options and analysis lifters allow different delays to be used for locally and globally. Moreover, local widening delays are applied per-path, which is not possible at the solver level at all.

The domain functor WideningDelay.Dom is generic and could be used as fine-grained as desired. For example, a specific analysis could only apply it to its own local or global abstract values, not for all analyses simultaneously. It could even be applied to only some parts of composed abstract domains.
It lives in a completely separate file, not to clutter any existing solvers, domains or analysis lifters.

TODO

• Merge master.
• Separate options and lifters for D and G?

[michael-schwarz]

This is indeed an interesting approach, thanks for the PR @RonaldJudin!

@jerhard and I considered it for a while, and made the following (perhaps obvious to you) observations:

• The gas is reset at every transfer function (which should be highlighted in the comment so this is more obvious).
• This, as we had discussed in Munich previously, avoids propagating high gas values outside of loops, which might lead to precision loss.
• Widening is only applied after the solver detects things as wpoints and thereby relies on the solver performing a widening between the previous value and the new one, rather than, e.g., performing widening between contributions from incoming edges.

As such, we presume the effect of this to be largely similar to #1442, but of course experiments are needed to confirm this suspicion.

What irks us a little is that this somehow mashes together the question of specifying the constraint system of interest with the process of computing (post-)solutions, which is evidenced by the fact that the gas components are not checked when performing leq checks. This information thus strikes us more to be a self-observation of the solver than something that ought to be reflected in the specification. To go to extremes to make the point clear, putting stable or point into the constraint system, would - while technically possible - be a questionable choice.

With our student, we are considering submitting a paper on widening, narrowing and related issues for side-effecting constraint systems, which will likely include #1442. As this may be quite similar, we might align at GobCon on how to proceed.

[sim642]

• This, as we had discussed in Munich previously, avoids propagating high gas values outside of loops, which might lead to precision loss.

Was the precision loss about high gas values outside of loops or their avoidance (which is the opposite)?

• Widening is only applied after the solver detects things as wpoints and thereby relies on the solver performing a widening between the previous value and the new one, rather than, e.g., performing widening between contributions from incoming edges.

What do you mean by widening between incoming edges? #1442 is in the solver and doesn't even know about different incoming edges, it can only see the joined values, so what's the difference?

What irks us a little is that this somehow mashes together the question of specifying the constraint system of interest with the process of computing (post-)solutions, which is evidenced by the fact that the gas components are not checked when performing leq checks. This information thus strikes us more to be a self-observation of the solver than something that ought to be reflected in the specification.

It's not the specification though. The lifted abstract values behave exactly as the unlifted ones, which is why leq shouldn't be affected. Widening by its very concept is something that affects the computation process, rather than its soundness, etc, so this isn't putting anything new in there. By that logic widenings shouldn't be in domains at all.

To go to extremes to make the point clear, putting stable or point into the constraint system, would - while technically possible - be a questionable choice.

To go to the other extreme, putting widen into the constraint system is also a questionable choice. But we aren't going to either extremity here, so that's really besides the point.
By the way, this questionable choice has been proposed from TUM before: https://link.springer.com/chapter/10.1007/978-3-642-38088-4_12.

---

I have to emphasize, this is the standard way to implement widening delays. It's precisely what Astree does:

We now use a local solution. Each piece of abstract information (such as an interval, an octagon, a filter predicate, etc.) is fitted with a freshness counter that allows regulating when this piece of information is widened.
[...]
The main advantage of freshness counters is that each piece of abstract information is dealt with separately and they are not necessarily widened at the same time. This is very important to analyze some variables that depend on each others.
[...]
It is also possible to select the widening frequency on a per abstract domain basis.

In an earlier paper, they explicitly mention switching to this as opposed to some more global counting strategy:

The following approach supersedes the previous one: Each abstract property (or set of abstract properties) is fitted with a freshness indicator.

This is also what Frama-C does: https://git.frama-c.com/pub/frama-c/-/blob/fe41a5490c3933fe18b9dbd4075f2f03f926714a/src/plugins/eva/partitioning/trace_partitioning.ml#L63.

This and #1442 aren't mutually exclusive. This just adds to Goblint what everyone else already has and has it completely in a separate file, not bothering any existing solver, domain or analysis code to do so.

---

This implementation is very much in alignment how various things in Goblint already are:

• LimitLifter lifts an analysis to flat-out crash after dbg.limit.widen widenings at a node (regardless of context!). And it uses mutable global state within the specification, which is far worse than doing it functionally.
• LevelSliceLifter lifts an analysis to similar domain with counters in second components.
• WidenContextLifterSide lifts an analysis to also make its computation terminate with recursive contexts, which isn't needed for the sound specification of the analysis.

[michael-schwarz]

Was the precision loss about high gas values outside of loops or their avoidance (which is the opposite)?

The consideration was that not resetting the counter would lead to precision loss at the code fragments located after a widening point.

What do you mean by widening between incoming edges? #1442 is in the solver and doesn't even know about different incoming edges, it can only see the joined values, so what's the difference?

This observation was not about a difference between #1442 and this. Rather it was an observation about what the solvers need to be fulfill for this to work (which TD3 does, but not necessarily all solvers must do). #1442 is integrated into one specific solver, so the question about what a solver must be like for it to work doesn't pose itself there.

[michael-schwarz]

@Red-Panda64 has some benchmarks here, where this seems to be worse when it comes to performance then #1442. Those might be of interest.

[Red-Panda64]

Well, yes, widening delay seems to be a bit slower. It times out 141 times where #1442 does not. Conversely, #1442 times out 10 times where widening delay does not.
Here are the plots comparing the unreach-call and valid-memsafety categories, where the majority of the difference was found.
#1442 is on the x-axis, #1483 on the y-axis.

unreach-call:

valid-memsafety:

The benchmarks ran on the same machine with specs:
Intel Xeon Platinum 8260 CPU @ 2.40GHz, cores: 96, frequency: 3900 MHz, Turbo Boost: enabled; RAM: 540649 MB
However, @stilscher said that bench-exec was slightly differently configured.

Anyway, it is good to see that both implementations agree on everything and produce the same new true results.

[michael-schwarz]

@jerhard: You promised a review on this until 2024-11-26 in the Gobcon. Do you have an estimate when you will be able to provide a review?