[PATCH] D140344: [clang][dataflow] In optional model, implement `widen` and make `compare` sound.

[Yitzhak Mandelbaum via Phabricator via cfe-commits]

ymandel created this revision.
ymandel added reviewers: xazax.hun, gribozavr2, kinu, sgatev.
Herald added subscribers: martong, rnkovacs.
Herald added a reviewer: NoQ.
Herald added a project: All.
ymandel requested review of this revision.
Herald added a project: clang.

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.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D140344

Files:
  clang/include/clang/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.h
  clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp
  clang/unittests/Analysis/FlowSensitive/UncheckedOptionalAccessModelTest.cpp

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D140344.484047.patch
Type: text/x-patch
Size: 7253 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20221219/71683133/attachment.bin>