6 Commits

Author SHA1 Message Date
Wei Yi Tee
1e9cd04d7b [clang][dataflow] Refactor boolean creation as a test utility.
Differential Revision: https://reviews.llvm.org/D129546
2022-07-13 10:35:17 +00:00
Wei Yi Tee
632de855a0 [clang][dataflow] Refactor boolean creation as a test utility.
Differential Revision: https://reviews.llvm.org/D129546
2022-07-13 10:15:06 +00:00
Wei Yi Tee
81e6400d8c [clang][dataflow] Return a solution from the solver when Constraints are Satisfiable.
Differential Revision: https://reviews.llvm.org/D129180
2022-07-07 20:21:19 +00:00
Dmitri Gribenko
63fac424e6 Revert "[clang][dataflow] Return a solution from the solver when Constraints are Satisfiable."
This reverts commit 19e21887eb18aa019000c2384ea7f2c91d937489. I
accidentally landed the non-final version of the patch that used
decomposition declarations (not yet usable in LLVM/Clang source).
2022-07-07 21:50:52 +02:00
Wei Yi Tee
19e21887eb [clang][dataflow] Return a solution from the solver when Constraints are Satisfiable.
A truth assignment to atomic boolean values which satisfy `Constraints` will be returned if found by the solver.
This gives us more information which can be helpful for debugging or constructing warning messages.

Reviewed By: hlopko, gribozavr2, sgatev

Differential Revision: https://reviews.llvm.org/D129180
2022-07-07 20:53:47 +02:00
Stanislav Gatev
53dcd9efd1 [clang][dataflow] Add SAT solver interface and implementation
This is part of the implementation of the dataflow analysis framework.
See "[RFC] A dataflow analysis framework for Clang AST" on cfe-dev.

Reviewed-by: ymandel, xazax.hun

Differential Revision: https://reviews.llvm.org/D120289
2022-02-25 14:46:52 +00:00