[all-commits] [llvm/llvm-project] d34fbf: [clang][dataflow] In optional model, implement `wi...

Yitzhak Mandelbaum via All-commits all-commits at lists.llvm.org
Thu Jan 12 12:37:04 PST 2023


  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: d34fbf2d9bf4d372d25087d2ded9573b17ce7632
      https://github.com/llvm/llvm-project/commit/d34fbf2d9bf4d372d25087d2ded9573b17ce7632
  Author: Yitzhak Mandelbaum <yitzhakm at google.com>
  Date:   2023-01-12 (Thu, 12 Jan 2023)

  Changed paths:
    M clang/include/clang/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.h
    M clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp
    M clang/unittests/Analysis/FlowSensitive/UncheckedOptionalAccessModelTest.cpp

  Log Message:
  -----------
  [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




More information about the All-commits mailing list