[all-commits] [llvm/llvm-project] 5bd643: [clang][dataflow] Strengthen widening of boolean v...

[martinboehme via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: 5bd643e1456bd2acc53ac0bf594d285be89a44fe
      https://github.com/llvm/llvm-project/commit/5bd643e1456bd2acc53ac0bf594d285be89a44fe
  Author: martinboehme <mboehme at google.com>
  Date:   2023-11-27 (Mon, 27 Nov 2023)

  Changed paths:
    M clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
    M clang/unittests/Analysis/FlowSensitive/TransferTest.cpp

  Log Message:
  -----------
  [clang][dataflow] Strengthen widening of boolean values. (#73484)

Before we widen to top, we now check if both values can be proved either
true or
false in their respective environments; if so, widening returns a true
or false
literal. The idea is that we avoid losing information if posssible.

This patch includes a test that fails without this change to widening.

This change does mean that we call the SAT solver in more places, but
this seems
acceptable given the additional precision we gain.

In tests on an internal codebase, the number of SAT solver timeouts we
observe
with Crubit's nullability checker does increase by about 25%. They can
be
brought back to the previous level by doubling the SAT solver work
limit.