wyt updated this revision to Diff 439714.
wyt marked 3 inline comments as done.
wyt added a comment.
Address comments.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D128357/new/
https://reviews.llvm.org/D128357
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -66,19 +66,16 @@
}
AtomicBoolValue &DataflowAnalysisContext::makeFlowConditionToken() {
- AtomicBoolValue &Token = createAtomicBoolValue();
- FlowConditionRemainingConjuncts[&Token] = {};
- FlowConditionFirstConjuncts[&Token] = &Token;
- return Token;
+ return createAtomicBoolValue();
}
void DataflowAnalysisContext::addFlowConditionConstraint(
AtomicBoolValue &Token, BoolValue &Constraint) {
- FlowConditionRemainingConjuncts[&Token].insert(&getOrCreateDisjunctionValue(
- Constraint, getOrCreateNegationValue(Token)));
- FlowConditionFirstConjuncts[&Token] =
- &getOrCreateDisjunctionValue(*FlowConditionFirstConjuncts[&Token],
- getOrCreateNegationValue(Constraint));
+ auto Res = FlowConditionConstraints.try_emplace(&Token, &Constraint);
+ if (!Res.second) {
+ Res.first->second =
+ &getOrCreateConjunctionValue(*Res.first->second, Constraint);
+ }
}
AtomicBoolValue &
@@ -133,24 +130,30 @@
void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
- llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) const {
+ llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) {
auto Res = VisitedTokens.insert(&Token);
if (!Res.second)
return;
- auto FirstConjunctIT = FlowConditionFirstConjuncts.find(&Token);
- if (FirstConjunctIT != FlowConditionFirstConjuncts.end())
- Constraints.insert(FirstConjunctIT->second);
- auto RemainingConjunctsIT = FlowConditionRemainingConjuncts.find(&Token);
- if (RemainingConjunctsIT != FlowConditionRemainingConjuncts.end())
- Constraints.insert(RemainingConjunctsIT->second.begin(),
- RemainingConjunctsIT->second.end());
+ auto ConstraintsIT = FlowConditionConstraints.find(&Token);
+ if (ConstraintsIT == FlowConditionConstraints.end()) {
+ Constraints.insert(&Token);
+ } else {
+ // Bind flow condition token via `iff` to its set of constraints:
+ // FC <=> (C1 ^ C2 ^ ...), where Ci are constraints
+ Constraints.insert(&getOrCreateConjunctionValue(
+ getOrCreateDisjunctionValue(
+ Token, getOrCreateNegationValue(*ConstraintsIT->second)),
+ getOrCreateDisjunctionValue(getOrCreateNegationValue(Token),
+ *ConstraintsIT->second)));
+ }
auto DepsIT = FlowConditionDeps.find(&Token);
if (DepsIT != FlowConditionDeps.end()) {
- for (AtomicBoolValue *DepToken : DepsIT->second)
+ for (AtomicBoolValue *DepToken : DepsIT->second) {
addTransitiveFlowConditionConstraints(*DepToken, Constraints,
VisitedTokens);
+ }
}
}
Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -198,7 +198,7 @@
/// calls.
void addTransitiveFlowConditionConstraints(
AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
- llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) const;
+ llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);
std::unique_ptr<Solver> S;
@@ -232,21 +232,16 @@
// defines the flow condition. Conceptually, each binding corresponds to an
// "iff" of the form `FC <=> (C1 ^ C2 ^ ...)` where `FC` is a flow condition
// token (an atomic boolean) and `Ci`s are the set of constraints in the flow
- // flow condition clause. Internally, we do not record the formula directly as
- // an "iff". Instead, a flow condition clause is encoded as conjuncts of the
- // form `(FC v !C1 v !C2 v ...) ^ (C1 v !FC) ^ (C2 v !FC) ^ ...`. The first
- // conjuct is stored in the `FlowConditionFirstConjuncts` map and the set of
- // remaining conjuncts are stored in the `FlowConditionRemainingConjuncts`
- // map, both keyed by the token of the flow condition.
+ // flow condition clause. The set of constraints (C1 ^ C2 ^ ...) are stored in
+ // the `FlowConditionConstraints` map, keyed by the token of the flow
+ // condition.
//
// Flow conditions depend on other flow conditions if they are created using
// `forkFlowCondition` or `joinFlowConditions`. The graph of flow condition
// dependencies is stored in the `FlowConditionDeps` map.
llvm::DenseMap<AtomicBoolValue *, llvm::DenseSet<AtomicBoolValue *>>
FlowConditionDeps;
- llvm::DenseMap<AtomicBoolValue *, BoolValue *> FlowConditionFirstConjuncts;
- llvm::DenseMap<AtomicBoolValue *, llvm::DenseSet<BoolValue *>>
- FlowConditionRemainingConjuncts;
+ llvm::DenseMap<AtomicBoolValue *, BoolValue *> FlowConditionConstraints;
};
} // namespace dataflow
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
