|
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 ...
|
| #
fa34210f |
| 27-Jun-2022 |
Wei Yi Tee <[email protected]> |
[clang][dataflow] Do not allow substitution of true/false boolean literals in `buildAndSubstituteFlowCondition`
Reviewed By: gribozavr2, xazax.hun
Differential Revision: https://reviews.llvm.org/D1
[clang][dataflow] Do not allow substitution of true/false boolean literals in `buildAndSubstituteFlowCondition`
Reviewed By: gribozavr2, xazax.hun
Differential Revision: https://reviews.llvm.org/D128658
show more ...
|
| #
bdfe556d |
| 27-Jun-2022 |
Wei Yi Tee <[email protected]> |
[clang][dataflow] Implement functionality for flow condition variable substitution.
This patch introduces `buildAndSubstituteFlowCondition` - given a flow condition token, this function returns the
[clang][dataflow] Implement functionality for flow condition variable substitution.
This patch introduces `buildAndSubstituteFlowCondition` - given a flow condition token, this function returns the expression of constraints defining the flow condition, with values substituted where specified.
As an example:
Say we have tokens `FC1`, `FC2`, `FC3`:
```
FlowConditionConstraints: {
FC1: C1,
FC2: C2,
FC3: (FC1 v FC2) ^ C3,
}
```
`buildAndSubstituteFlowCondition(FC3, /*Substitutions:*/{{C1 -> C1'}})`
returns a value corresponding to `(C1' v C2) ^ C3`.
Note:
This function returns the flow condition expressed directly as its constraints, which differs to how we currently represent the flow condition as a token bound to a set of constraints and dependencies. Making the representation consistent may be an option to consider in the future.
Depends On D128357
Reviewed By: gribozavr2, xazax.hun
Differential Revision: https://reviews.llvm.org/D128363
show more ...
|
| #
0f65a3e6 |
| 24-Jun-2022 |
Wei Yi Tee <[email protected]> |
[clang][dataflow] Implement functionality to compare if two boolean values are equivalent.
`equivalentBoolValues` compares equivalence between two booleans. The current implementation does not consi
[clang][dataflow] Implement functionality to compare if two boolean values are equivalent.
`equivalentBoolValues` compares equivalence between two booleans. The current implementation does not consider constraints imposed by flow conditions on the booleans and its subvalues.
Depends On D128520
Reviewed By: gribozavr2, xazax.hun
Differential Revision: https://reviews.llvm.org/D128521
show more ...
|
| #
00e9d534 |
| 24-Jun-2022 |
Wei Yi Tee <[email protected]> |
[clang][dataflow] Move logic for creating implication and iff expressions into `DataflowAnalysisContext` from `DataflowEnvironment`.
To keep functionality of creating boolean expressions in a consis
[clang][dataflow] Move logic for creating implication and iff expressions into `DataflowAnalysisContext` from `DataflowEnvironment`.
To keep functionality of creating boolean expressions in a consistent location.
Depends On D128357
Reviewed By: gribozavr2, sgatev, xazax.hun
Differential Revision: https://reviews.llvm.org/D128519
show more ...
|
|
Revision tags: llvmorg-14.0.6, llvmorg-14.0.5, llvmorg-14.0.4 |
|
| #
58abe36a |
| 04-May-2022 |
Eric Li <[email protected]> |
[clang][dataflow] Add flowConditionIsTautology function
Provide a way for users to check if a flow condition is
unconditionally true.
Differential Revision: https://reviews.llvm.org/D124943
|
|
Revision tags: llvmorg-14.0.3, llvmorg-14.0.2 |
|
| #
955a05a2 |
| 25-Apr-2022 |
Stanislav Gatev <[email protected]> |
[clang][dataflow] Optimize flow condition representation
Enable efficient implementation of context-aware joining of distinct
boolean values. It can be used to join distinct boolean values while
pre
[clang][dataflow] Optimize flow condition representation
Enable efficient implementation of context-aware joining of distinct
boolean values. It can be used to join distinct boolean values while
preserving flow condition information.
Flow conditions are represented as Token <=> Clause iff formulas. To
perform context-aware joining, one can simply add the tokens of flow
conditions to the formula when joining distinct boolean values, e.g:
`makeOr(makeAnd(FC1, Val1), makeAnd(FC2, Val2))`. This significantly
simplifies the implementation of `Environment::join`.
This patch removes the `DataflowAnalysisContext::getSolver` method.
The `DataflowAnalysisContext::flowConditionImplies` method should be
used instead.
Reviewed-by: ymandel, xazax.hun
Differential Revision: https://reviews.llvm.org/D124395
show more ...
|
|
Revision tags: llvmorg-14.0.1, llvmorg-14.0.0, llvmorg-14.0.0-rc4, llvmorg-14.0.0-rc3, llvmorg-14.0.0-rc2 |
|
| #
ae60884d |
| 01-Mar-2022 |
Stanislav Gatev <[email protected]> |
[clang][dataflow] Add flow condition constraints to Environment
This is part of the implementation of the dataflow analysis framework.
See "[RFC] A dataflow analysis framework for Clang AST" on cfe-
[clang][dataflow] Add flow condition constraints to Environment
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/D120711
show more ...
|