[all-commits] [llvm/llvm-project] 7c6367: [clang][dataflow] Simplify flow conditions display...

[martinboehme via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: 7c636728c0fc18fc79831bfc3cdf41841b9b517c
      https://github.com/llvm/llvm-project/commit/7c636728c0fc18fc79831bfc3cdf41841b9b517c
  Author: martinboehme <mboehme at google.com>
  Date:   2023-11-07 (Tue, 07 Nov 2023)

  Changed paths:
    A clang/include/clang/Analysis/FlowSensitive/SimplifyConstraints.h
    M clang/lib/Analysis/FlowSensitive/CMakeLists.txt
    M clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
    M clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
    A clang/lib/Analysis/FlowSensitive/SimplifyConstraints.cpp
    M clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
    A clang/unittests/Analysis/FlowSensitive/SimplifyConstraintsTest.cpp
    M llvm/utils/gn/secondary/clang/lib/Analysis/FlowSensitive/BUILD.gn
    M llvm/utils/gn/secondary/clang/unittests/Analysis/FlowSensitive/BUILD.gn

  Log Message:
  -----------
  [clang][dataflow] Simplify flow conditions displayed in HTMLLogger. (#70848)

This can make the flow condition significantly easier to interpret; see
below
for an example.

I had hoped that adding the simplification as a preprocessing step
before the
SAT solver (in `DataflowAnalysisContext::querySolver()`) would also
speed up SAT
solving and maybe even eliminate SAT solver timeouts, but in my testing,
this
actually turns out to be a pessimization. It appears that these
simplifications
are easy enough for the SAT solver to perform itself.

Nevertheless, the improvement in debugging alone makes this a worthwhile
change.

Example of flow condition output with these changes:

```
Flow condition token: V37
Constraints:
(V16 = (((V15 & (V19 = V12)) & V22) & V25))
(V15 = ((V12 & ((V14 = V9) | (V14 = V4))) & (V13 = V14)))
True atoms: (V0, V1, V2, V5, V6, V7, V29, V30, V32, V34, V35, V37)
False atoms: (V3, V8, V17)
Equivalent atoms:
(V11, V15)

Flow condition constraints before simplification:
V37
((!V3 & !V8) & !V17)
(V37 = V34)
(V34 = (V29 & (V35 = V30)))
(V29 = (((V16 | V2) & V32) & (V30 = V32)))
(V16 = (((V15 & (V19 = V12)) & V22) & V25))
(V15 = V11)
(V11 = ((((V7 | V2) & V12) & ((V7 & (V14 = V9)) | (V2 & (V14 = V4)))) & (V13 = V14)))
(V2 = V1)
(V1 = V0)
V0
(V7 = V6)
(V6 = V5)
(V5 = V2)
```