[clang] [dataflow] Add global condition to DataflowAnalysisContext (PR #65949)
Yitzhak Mandelbaum via cfe-commits
cfe-commits at lists.llvm.org
Wed Sep 13 07:02:02 PDT 2023
================
@@ -172,27 +179,33 @@ bool DataflowAnalysisContext::equivalentFormulas(const Formula &Val1,
}
void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
- Atom Token, llvm::SetVector<const Formula *> &Constraints,
- llvm::DenseSet<Atom> &VisitedTokens) {
- auto Res = VisitedTokens.insert(Token);
- if (!Res.second)
- return;
-
- auto ConstraintsIt = FlowConditionConstraints.find(Token);
- if (ConstraintsIt == FlowConditionConstraints.end()) {
- Constraints.insert(&arena().makeAtomRef(Token));
- } else {
- // Bind flow condition token via `iff` to its set of constraints:
- // FC <=> (C1 ^ C2 ^ ...), where Ci are constraints
- Constraints.insert(&arena().makeEquals(arena().makeAtomRef(Token),
- *ConstraintsIt->second));
- }
+ Atom Token, llvm::SetVector<const Formula *> &Constraints) {
+ llvm::DenseSet<Atom> AddedTokens;
+ std::vector<Atom> Remaining = {Token};
+
+ if (GlobalConstraints)
+ Constraints.insert(GlobalConstraints);
+ // Define all the flow conditions that might be referenced in constraints.
+ while (!Remaining.empty()) {
+ auto Token = Remaining.back();
+ Remaining.pop_back();
+ if (!AddedTokens.insert(Token).second)
+ continue;
+
+ auto ConstraintsIt = FlowConditionConstraints.find(Token);
+ if (ConstraintsIt == FlowConditionConstraints.end()) {
+ Constraints.insert(&arena().makeAtomRef(Token));
+ } else {
+ // Bind flow condition token via `iff` to its set of constraints:
+ // FC <=> (C1 ^ C2 ^ ...), where Ci are constraints
+ Constraints.insert(&arena().makeEquals(arena().makeAtomRef(Token),
+ *ConstraintsIt->second));
+ }
- auto DepsIt = FlowConditionDeps.find(Token);
- if (DepsIt != FlowConditionDeps.end()) {
- for (Atom DepToken : DepsIt->second) {
- addTransitiveFlowConditionConstraints(DepToken, Constraints,
- VisitedTokens);
+ if (auto DepsIt = FlowConditionDeps.find(Token);
+ DepsIt != FlowConditionDeps.end()) {
+ for (Atom A : DepsIt->second)
+ Remaining.push_back(A);
----------------
ymand wrote:
Sounds good.
https://github.com/llvm/llvm-project/pull/65949
More information about the cfe-commits
mailing list