Fix address domain widening creating duplicates

[sim642]

Closes #554.

In the problematic widen {a[def_exc:1], a} {a[def_exc:Not {0}([0,7])]}, previously it iterated over the two elements of the old set and widened those with the single element of the new set. Those inner widenings gave identical results and both remained.

Now it iterates over the single element of the new set and widening that with the two elements just yields one element, avoiding the duplicate.

None of HoarePO contains explicit logic for avoiding duplicates though, it just uses lists for the buckets. So I cannot be fully sure that there aren't some other weird cases possible, where it can still break.

[michael-schwarz]

Is the issue not even earlier, namely that widen {a[def_exc:1], a} {a[def_exc:Not {0}([0,7])]} violates the rule that the first argument of a widen needs to be less or equal to its second argument?

Edit: Apparently {a[def_exc:1], a} leq {a[def_exc:Not {0}([0,7])]} does hold. Maybe it is just me, but it is this not a bit questionable? Why is a set that contains a without offset leq a set where a[0] is explicitly excluded?

[michael-schwarz]

If this property is violated here, this would result in loosing all elements in the left argument that are incomparable with all elements in the right set, right?

[michael-schwarz]

But it does fix the issue we had for openSSL (and not just the reduced example).

[sim642]

Apparently {a[def_exc:1], a} leq {a[def_exc:Not {0}([0,7])]} does hold. Maybe it is just me, but it is this not a bit questionable? Why is a set that contains a without offset leq a set where a[0] is explicitly excluded?

That's a good point. I didn't really think about it and just thought that's due to some special address domain thing. So there might be more wrong here indeed.

Also, I suspect the join might be wrong too then because the right argument of widen already has the left one joined in, so a should've been joined into something, but apparently not?

If this property is violated here, this would result in loosing all elements in the left argument that are incomparable with all elements in the right set, right?

Hmm, I think due to the right argument being a join, all the addresses from the left should be contained and thus comparable with something on the right, so nothing should disappear.

[sim642]

I added some unit tests for the lval domain used for the elements of address domain and there's an even more fundamental issue I guess:

• a is equal to a[0],
• a[0] join a[1] is equal to a[top],
• a join a[1] is not equal to a[top], because the join raises Uncomparable instead.

I'm not completely sure anymore, what the intended semantics is supposed to be. Are a and a[0] supposed to be different representations of the same thing? Having multiple representations is always a pain to deal with.

[sim642]

Apparently {a[def_exc:1], a} leq {a[def_exc:Not {0}([0,7])]} does hold. Maybe it is just me, but it is this not a bit questionable? Why is a set that contains a without offset leq a set where a[0] is explicitly excluded?

I looked into this and the problem was that a is leq than a[not 0], which it should not be. Turns out this was due to a bug in DefExc.equal_to with an exclusion set, which caused wrong results from some of the offset lattice operations dealing with offsets of differing length. This should be fixed according to the tests I added.

[michael-schwarz]

Does not solve all the strange things going on here, but at least the ones where we are clear on how to solve them. I'd advocate merging.