|
Revision tags: llvmorg-20.1.0, llvmorg-20.1.0-rc3, llvmorg-20.1.0-rc2, llvmorg-20.1.0-rc1, llvmorg-21-init, llvmorg-19.1.7, llvmorg-19.1.6, llvmorg-19.1.5, llvmorg-19.1.4, llvmorg-19.1.3, llvmorg-19.1.2, llvmorg-19.1.1, llvmorg-19.1.0, llvmorg-19.1.0-rc4, llvmorg-19.1.0-rc3, llvmorg-19.1.0-rc2, llvmorg-19.1.0-rc1, llvmorg-20-init, 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, llvmorg-17.0.6, llvmorg-17.0.5, llvmorg-17.0.4, llvmorg-17.0.3, llvmorg-17.0.2, llvmorg-17.0.1, llvmorg-17.0.0, llvmorg-17.0.0-rc4, llvmorg-17.0.0-rc3, llvmorg-17.0.0-rc2, llvmorg-17.0.0-rc1, llvmorg-18-init, llvmorg-16.0.6, llvmorg-16.0.5, llvmorg-16.0.4, llvmorg-16.0.3, llvmorg-16.0.2, llvmorg-16.0.1, llvmorg-16.0.0, llvmorg-16.0.0-rc4, llvmorg-16.0.0-rc3, llvmorg-16.0.0-rc2, llvmorg-16.0.0-rc1, llvmorg-17-init, llvmorg-15.0.7, llvmorg-15.0.6, llvmorg-15.0.5, llvmorg-15.0.4, llvmorg-15.0.3, llvmorg-15.0.2, llvmorg-15.0.1, llvmorg-15.0.0, llvmorg-15.0.0-rc3, llvmorg-15.0.0-rc2, llvmorg-15.0.0-rc1, llvmorg-16-init |
|
| #
b5e3dac3 |
| 26-Jul-2022 |
Dmitri Gribenko <[email protected]> |
[clang][dataflow] Add explicit "AST" nodes for implications and iff
Previously we used to desugar implications and biconditionals into
equivalent CNF/DNF as soon as possible. However, this desugarin
[clang][dataflow] Add explicit "AST" nodes for implications and iff
Previously we used to desugar implications and biconditionals into
equivalent CNF/DNF as soon as possible. However, this desugaring makes
debug output (Environment::dump()) less readable than it could be.
Therefore, it makes sense to keep the sugared representation of a
boolean formula, and desugar it in the solver.
Reviewed By: sgatev, xazax.hun, wyt
Differential Revision: https://reviews.llvm.org/D130519
show more ...
|
| #
3281138a |
| 26-Jul-2022 |
Dmitri Gribenko <[email protected]> |
[clang][dataflow] Fix SAT solver crashes on `X ^ X` and `X v X`
BooleanFormula::addClause has an invariant that a clause has no duplicated
literals. When the solver was desugaring a formula into CNF
[clang][dataflow] Fix SAT solver crashes on `X ^ X` and `X v X`
BooleanFormula::addClause has an invariant that a clause has no duplicated
literals. When the solver was desugaring a formula into CNF clauses, it
could construct a clause with such duplicated literals in two cases.
Reviewed By: sgatev, ymandel, xazax.hun
Differential Revision: https://reviews.llvm.org/D130522
show more ...
|
| #
81e6400d |
| 07-Jul-2022 |
Wei Yi Tee <[email protected]> |
[clang][dataflow] Return a solution from the solver when `Constraints` are `Satisfiable`.
Differential Revision: https://reviews.llvm.org/D129180
|
| #
63fac424 |
| 07-Jul-2022 |
Dmitri Gribenko <[email protected]> |
Revert "[clang][dataflow] Return a solution from the solver when `Constraints` are `Satisfiable`."
This reverts commit 19e21887eb18aa019000c2384ea7f2c91d937489. I
accidentally landed the non-final v
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).
show more ...
|
| #
19e21887 |
| 07-Jul-2022 |
Wei Yi Tee <[email protected]> |
[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 sol
[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
show more ...
|
|
Revision tags: llvmorg-14.0.6, llvmorg-14.0.5, llvmorg-14.0.4, llvmorg-14.0.3, llvmorg-14.0.2, llvmorg-14.0.1, llvmorg-14.0.0, llvmorg-14.0.0-rc4, llvmorg-14.0.0-rc3, llvmorg-14.0.0-rc2 |
|
| #
53dcd9ef |
| 21-Feb-2022 |
Stanislav Gatev <[email protected]> |
[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-de
[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
show more ...
|