History log of /llvm-project/clang/lib/Analysis/FlowSensitive/SimplifyConstraints.cpp (Results 1 – 3 of 3)
Revision (<<< Hide revision tags) (Show revision tags >>>) Date Author Comments
Revision tags: llvmorg-18.1.8, llvmorg-18.1.7, llvmorg-18.1.6, llvmorg-18.1.5, llvmorg-18.1.4, llvmorg-18.1.3, llvmorg-18.1.2, llvmorg-18.1.1, llvmorg-18.1.0, llvmorg-18.1.0-rc4, llvmorg-18.1.0-rc3, llvmorg-18.1.0-rc2, llvmorg-18.1.0-rc1, llvmorg-19-init
# 1b1b5251 18-Jan-2024 martinboehme <mboehme@google.com>

[clang][dataflow] Use `Formula::isLiteral()` in a couple more places. (#78404)


Revision tags: llvmorg-17.0.6, llvmorg-17.0.5
# 24060db3 07-Nov-2023 Aaron Ballman <aaron@aaronballman.com>

Silence diagnostics about not all control paths returning a value; NFC


# 7c636728 07-Nov-2023 martinboehme <mboehme@google.com>

[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 th

[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)
```

show more ...