[all-commits] [llvm/llvm-project] fc9821: Reland "[dataflow] Add dedicated representation of...

[Sam McCall via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: fc9821a877d4e1443603d67539e4369b3ec72890
      https://github.com/llvm/llvm-project/commit/fc9821a877d4e1443603d67539e4369b3ec72890
  Author: Sam McCall <sam.mccall at gmail.com>
  Date:   2023-07-07 (Fri, 07 Jul 2023)

  Changed paths:
    M clang/include/clang/Analysis/FlowSensitive/Arena.h
    M clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
    M clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
    M clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
    A clang/include/clang/Analysis/FlowSensitive/Formula.h
    M clang/include/clang/Analysis/FlowSensitive/Solver.h
    M clang/include/clang/Analysis/FlowSensitive/Value.h
    M clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
    M clang/lib/Analysis/FlowSensitive/Arena.cpp
    M clang/lib/Analysis/FlowSensitive/CMakeLists.txt
    M clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
    M clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
    M clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
    A clang/lib/Analysis/FlowSensitive/Formula.cpp
    M clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
    M clang/lib/Analysis/FlowSensitive/Transfer.cpp
    M clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
    M clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
    M clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
    M clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
    M clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
    M clang/unittests/Analysis/FlowSensitive/TestingSupport.h
    M clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
    M clang/unittests/Analysis/FlowSensitive/ValueTest.cpp

  Log Message:
  -----------
  Reland "[dataflow] Add dedicated representation of boolean formulas"

This reverts commit 7a72ce98224be76d9328e65eee472381f7c8e7fe.

Test problems were due to unspecified order of function arg evaluation.

Reland "[dataflow] Replace most BoolValue subclasses with references to Formula (and AtomicBoolValue => Atom and BoolValue => Formula where appropriate)"

This properly frees the Value hierarchy from managing boolean formulas.

We still distinguish AtomicBoolValue; this type is used in client code.
However we expect to convert such uses to BoolValue (where the
distinction is not needed) or Atom (where atomic identity is intended),
and then fold AtomicBoolValue into FormulaBoolValue.

We also distinguish TopBoolValue; this has distinct rules for
widen/join/equivalence, and top-ness is not represented in Formula.
It'd be nice to find a cleaner representation (e.g. the absence of a
formula), but no immediate plans.

For now, BoolValues with the same Formula are deduplicated. This doesn't
seem desirable, as Values are mutable by their creators (properties).
We can probably drop this for FormulaBoolValue immediately (not in this
patch, to isolate changes). For AtomicBoolValue we first need to update
clients to stop using value pointers for atom identity.

The data structures around flow conditions are updated:
- flow condition tokens are Atom, rather than AtomicBoolValue*
- conditions are Formula, rather than BoolValue
Most APIs were changed directly, some with many clients had a
new version added and the existing one deprecated.

The factories for BoolValues in Environment keep their existing
signatures for now (e.g. makeOr(BoolValue, BoolValue) => BoolValue)
and are not deprecated. These have very many clients and finding the
most ergonomic API & migration path still needs some thought.

Differential Revision: https://reviews.llvm.org/D153469