[clang][dataflow] In optional model, implement `widen` and make `compare` sound.
authorYitzhak Mandelbaum <yitzhakm@google.com>
Thu, 15 Dec 2022 15:11:21 +0000 (15:11 +0000)
committerYitzhak Mandelbaum <yitzhakm@google.com>
Thu, 12 Jan 2023 20:36:37 +0000 (20:36 +0000)
commitd34fbf2d9bf4d372d25087d2ded9573b17ce7632
tree276bbf0bcf7307491abce2c29633bdd4876f88b0
parent97156ba7bcc91b1449925df95128c36680549a4d
[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
clang/include/clang/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.h
clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp
clang/unittests/Analysis/FlowSensitive/UncheckedOptionalAccessModelTest.cpp