#
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 ...
|