Switch to widen which doesn't require leq on arguments

[sim642]

Arguments for this approach are given here: https://link.springer.com/chapter/10.1007/978-981-19-9601-6_4.

This currently just pushes the join down into the domains, so it currently doesn't achieve much.
The goal would be to avoid all such intermediate joins when they're actually not needed and only have the necessary ones in "leaf" domains.

This pushes the join from the solver down into the domains, as far as possible, ideally to the "leaf" domains.
And in that case the join can often be inlined and integrated into widen to lift the leq assumption without needing to actually construct the intermediate joined value.
There are a couple of places where there's still a join at an intermediate domain: specifically the various HoareDomain and set-based struct domains. The whole widening situation there is quite tricky and for the most part we don't use those domains, so the main bottlenecks should be avoided already.

This should improve performance on large programs like rsync: #1967 (comment). And it finally should allow #1484 to be integrated without global state hacks.

TODO

• widen_with_fct
• smart_widen
• sv-benchmarks
  • Investigate OUT OF MEMORY → TIMEOUT changes: Switch to widen which doesn't require leq on arguments #2081 (comment)
• rsync
• Revert 4734724 after Fix ArrayDomain.Partitioned.make returning non-normalized values #2112

[sim642]

In sv-benchmarks level01 60s 1GB comparisons, there's no verdict differences: https://goblint.cs.ut.ee/results/380-all-level01-pr-2081-after-2/.
In the difference table, there's just two suspicious cases that go from OUT OF MEMORY to TIMEOUT:

• ldv-commit-tester/m0_drivers-media-video-cx88-cx88-blackbird-ko--32_7a--d47b389 w/ unreach-call
• ldv-commit-tester/m0_drivers-media-video-cx88-cx88-blackbird-ko--32_7a--d47b389-1 w/ unreach-call

In those cases, before this PR:

[Info] runtime: 00:00:10.421
[Info] vars: 20434, evals: 16784

[Info] runtime: 00:00:20.654
[Info] vars: 40192, evals: 33068

After this PR:

[Info] runtime: 00:00:10.299
[Info] vars: 4040, evals: 17473

[Info] runtime: 00:00:20.328
[Info] vars: 4040, evals: 36421

[...]

So there is something possibly suspicious happening that it gets stuck at the same number of vars.

In overall performance, there's sadly no difference either.
The only notable exception is recursified_loop-simple/recursified_nested_6 (and similar) w/ unreach-call which become 1.5× faster.

I'm still running the rsync comparison to see if it makes a difference there, because the initial hope was based on rsync profiling.

[sim642]

So there is something possibly suspicious happening that it gets stuck at the same number of vars.

I traced this with sol_max (and then sol) to find out where it's getting stuck. One of the looping updates is the following.
Old value

vargs ->   (partitioned array:Array: Array (no part.): (Array (no part.): Unknown, 1), IntDomLifter(intdomtuple):1)

Right-hand side value and new (widened?) value:

vargs ->   (partitioned array:Array: Array (part. by 0): ((Array (part. by 0): (Unknown -- Unknown -- Unknown), 1) -- (Array (no part.): Unknown, 1) -- (Array (no part.): Unknown, 1)), IntDomLifter(intdomtuple):1)

I guess this might've gone back and forth infinitely (?), I didn't actually check: the log file is impossibly large to interact with.

I then had another look at the widening changes of partitioned arrays and found out that I had mistakenly not adapted the various smart_widen functions appropriately to do the smart_join in the second argument.
I don't really understand why it's necessary because both of them delegate to a common smart_op implementation, which then should at least compute the upper bound (and only differ in what's applied to the inner elements).

EDIT: The real culprit seems to be #2112 (comment). So my latest commit here should probably get reverted then.

[sim642]

I'm still running the rsync comparison to see if it makes a difference there, because the initial hope was based on rsync profiling.

The speedup on rsync is huge: from ~7h 16 min to "just" ~5h. That's a 31% speedup!
All warnings, vars count and evals count are the same, so they should really be equivalent (I should've marshaled the runs to be able to compare the solutions, but oh well.)

[michael-schwarz]

The speedup on rsync is huge: from ~7h 16 min to "just" ~5h. That's a 31% speedup!

I am a bit skeptical. Why would we see such a huge speedup here? Is it the removed asserts?

[sim642]

Here are screenshots of the corresponding perf profiles, with Td3.side highlighted in both, which is where the difference is most prominent.
The savings are in two places:

1. The removal of assert_valid_widen, which is a couple of frames higher in the flame graph. There are other places deeper in the domains, which also assert the same (for good measure), but they didn't stand out.
2. The removal of join itself makes the bigger difference than the assertions. This essentially fuses the two map2-like passes on the abstract element into one. So 2 traversals are replaced with 1, and 2 result constructions are replaced with 1 (the intermediate join result element isn't allocated). And on top of that, it reduces GC time because there's so much less to collect.

It is true that by just pushing the join deep into widen just makes each leaf widen do slightly more work (which is why Td3.side runtime isn't fully halved).
But in many cases, the join can be inlined into the widen at the leaf domain. For example, for intervals it's a 2 character change: https://github.com/goblint/analyzer/pull/2081/changes#diff-2d56354faf2bc9035056389107dd30ed9bf45dec5421db67a885139ed26ec3a6. So interval widen without the assumption is just as efficient as the one we had before.

Out of all of our domains, intervals are one of the few that actually have an interesting widen. (Actually, this rsync conf doesn't even use intervals.)
There were many-many domains with let widen = join, which was unnecessary before and caused an inefficiency by doing the join twice (for no reason at all).

Before

Td3.side is 43% of runtime.

After

Td3.side is 26% of runtime.

[michael-schwarz]

Thank you for the detailed writeup!