Fix/region

[vogler]

Using solver wpoint, two functions in one of the region tests are dead (but should not be):

Testing 09/23 regions/evilcollapse_rc	 Status: 3 (verify)
  ...
  - Fixpoint not reached at entry state of list_add (23-evilcollapse_rc.c:22)
  - Fixpoint not reached at entry state of INIT_LIST_HEAD (23-evilcollapse_rc.c:11)

With --disable exp.region-offsets instead, they are somehow not dead. The solver works fine with all other tests.

[michael-schwarz]

@sim642 @vesalvojdani Is this something we should merge? or close?

[sim642]

Probably needs to be assessed as part of #107.

[sim642]

I merged master into this to see what's the state of this.

The test case no longer runs because there's no wpoint solver, but:

1. wpoint solver was renamed to space in e2ba38341cb5341fe505083d0348669703d346ad. That doesn't exist anymore either.
2. space solver was removed in 25f8eb4eb39438e3bee23618d8a9724d1a320069.
3. Restoring the space solver and fixing the interfaces, indeed the two functions are found to be dead. But that doesn't seem to depend on exp.region-offsets anymore.
4. That removed solver was "Top down solver that only keeps values at widening points and restores other values afterwards". Configuring the current TD3 in the same way gives sound results.
5. I tried all of the remaining solvers: topdown_term and topdown_space_cache_term and also have the dead code issue.

So part of the issue at least appears to simply be old solvers whose modern version for whatever reason has been fixed. I didn't debug enough to understand what the fix could've been.

---

Other than that, since we recently removed blessed/unique types on master, part of these changes has already been made. The three changes to region domain lattice operations is something I'm still looking into to see if they make sense or matter at all (I suspect they might even not).

[sim642]

The three changes to region domain lattice operations is something I'm still looking into to see if they make sense or matter at all (I suspect they might even not).

It seems like they change code which should never be triggered anyway:

1. The region domain defines collapse such that bullet is not collapsible with a non-bullet, so there should be no attempt to ever join them anyway. Seems like there's something similar to DisjointDomain.PairwiseSet here.
2. The partition set is never involved in a meet. A sound implementation is probably possible, but not necessary at this point.

I replaced these things with exceptions and ran it on sv-benchmarks where we use region by default. These never failed there (nor on our regression suite), so these assumptions seem to hold.