This patch includes two related changes:
- Rewrite compare operation to be sound. Current version checks for equality
of isNonEmptyOptional on both values, judging the values Same when the
results are equal. While that works when both are true, it is problematic when
they are both false, because there are four cases in which that's can occur:
both empty, one empty and one unknown (which is two cases), and both unknown. In
the latter three cases, it is unsound to judge them Same. This patch changes
compare to explicitly check for case of both empty and then judge any other
case Different.
- With the change to compare, a number of common cases will no longer
terminate. So, we also implement widening to properly handle those cases and
recover termination.
Drive-by: improve performance of merge operation.
Of the new tests, the code before the patch fails
- ReassignValueInLoopToSetUnsafe, and
- ReassignValueInLoopToUnknownUnsafe.