Author: Wei Yi Tee Date: 2022-06-24T21:52:16+02:00 New Revision: fb88ea62602c90f8f7c80560fd6a14f1c8c6d520
URL: https://github.com/llvm/llvm-project/commit/fb88ea62602c90f8f7c80560fd6a14f1c8c6d520 DIFF: https://github.com/llvm/llvm-project/commit/fb88ea62602c90f8f7c80560fd6a14f1c8c6d520.diff LOG: [clang][dataflow] Store flow condition constraints in a single `FlowConditionConstraints` map. A flow condition is represented with an atomic boolean token, and it is bound to a set of constraints: `(FC <=> C1 ^ C2 ^ ...)`. \ This was internally represented as `(FC v !C1 v !C2 v ...) ^ (C1 v !FC) ^ (C2 v !FC) ^ ...` and tracked by 2 maps: - `FlowConditionFirstConjunct` stores the first conjunct `(FC v !C1 v !C2 v ...)` - `FlowConditionRemainingConjuncts` stores the remaining conjuncts `(C1 v !FC) ^ (C2 v !FC) ^ ...` This patch simplifies the tracking of the constraints by using a single `FlowConditionConstraints` map which stores `(C1 ^ C2 ^ ...)`, eliminating the use of two maps. Reviewed By: gribozavr2, sgatev, xazax.hun Differential Revision: https://reviews.llvm.org/D128357 Added: Modified: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp Removed: ################################################################################ diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h index e2820fcb55655..48d0eedc49dde 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h @@ -198,7 +198,7 @@ class DataflowAnalysisContext { /// 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 @@ class DataflowAnalysisContext { // 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 diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp index 81e37e6e6905a..ffd552b1fdc72 100644 --- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -66,19 +66,16 @@ BoolValue &DataflowAnalysisContext::getOrCreateNegationValue(BoolValue &Val) { } 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 @@ bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) { 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); + } } } _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
