[clang][dataflow] In optional model, implement `widen` and make `compare` sound.
This patch includes two related changes: 1. 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`. 2. 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. Differential Revision: https://reviews.llvm.org/D140344
Loading
Please sign in to comment