From 21ab252f972cd810888636c106bfa88a18f72572 Mon Sep 17 00:00:00 2001 From: Sam McCall Date: Thu, 14 Sep 2023 19:30:04 +0200 Subject: [dataflow] Add global invariant condition to DataflowAnalysisContext (#65949) This records facts that are not sensitive to the current flow condition, and should apply to all environments. The motivating case is recording information about where a Value originated, such as nullability: - we may see the same Value for multiple expressions (e.g. reads of the same field) in multiple environments (multiple blocks or iterations) - we want to record information only when we first see the Value (e.g. Nullability annotations on fields only add information if we don't know where the value came from) - this information should be expressible as a SAT condition - we must add this SAT condition to every environment where the Value may appear We solve this by recording the information in the global condition. This doesn't seem particularly elegant, but solves the problem and is a fairly small and natural extension of the Environment. Alternatives considered: - store the constraint directly as a property on the Value. But it's more composable for such properties to always be variables (AtomicBoolValue), and constrain them with SAT conditions. - add a hook whenever values are created, giving the analysis the chance to populate them. However the framework relies on/provides the ability to construct values in arbitrary places without providing the context such a hook would need, this would be a very invasive change. --- .../FlowSensitive/DataflowAnalysisContext.cpp | 63 ++++++++++++---------- 1 file changed, 36 insertions(+), 27 deletions(-) (limited to 'clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp') diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp index 47a994f..e81048c 100644 --- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -104,6 +104,13 @@ DataflowAnalysisContext::getOrCreateNullPointerValue(QualType PointeeType) { return *Res.first->second; } +void DataflowAnalysisContext::addInvariant(const Formula &Constraint) { + if (Invariant == nullptr) + Invariant = &Constraint; + else + Invariant = &arena().makeAnd(*Invariant, Constraint); +} + void DataflowAnalysisContext::addFlowConditionConstraint( Atom Token, const Formula &Constraint) { auto Res = FlowConditionConstraints.try_emplace(Token, &Constraint); @@ -149,8 +156,7 @@ bool DataflowAnalysisContext::flowConditionImplies(Atom Token, llvm::SetVector Constraints; Constraints.insert(&arena().makeAtomRef(Token)); Constraints.insert(&arena().makeNot(Val)); - llvm::DenseSet VisitedTokens; - addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); + addTransitiveFlowConditionConstraints(Token, Constraints); return isUnsatisfiable(std::move(Constraints)); } @@ -159,8 +165,7 @@ bool DataflowAnalysisContext::flowConditionIsTautology(Atom Token) { // ever be false. llvm::SetVector Constraints; Constraints.insert(&arena().makeNot(arena().makeAtomRef(Token))); - llvm::DenseSet VisitedTokens; - addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); + addTransitiveFlowConditionConstraints(Token, Constraints); return isUnsatisfiable(std::move(Constraints)); } @@ -172,28 +177,33 @@ bool DataflowAnalysisContext::equivalentFormulas(const Formula &Val1, } void DataflowAnalysisContext::addTransitiveFlowConditionConstraints( - Atom Token, llvm::SetVector &Constraints, - llvm::DenseSet &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)); - } - - auto DepsIt = FlowConditionDeps.find(Token); - if (DepsIt != FlowConditionDeps.end()) { - for (Atom DepToken : DepsIt->second) { - addTransitiveFlowConditionConstraints(DepToken, Constraints, - VisitedTokens); + Atom Token, llvm::SetVector &Constraints) { + llvm::DenseSet AddedTokens; + std::vector Remaining = {Token}; + + if (Invariant) + Constraints.insert(Invariant); + // 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)); } + + if (auto DepsIt = FlowConditionDeps.find(Token); + DepsIt != FlowConditionDeps.end()) + for (Atom A : DepsIt->second) + Remaining.push_back(A); } } @@ -201,8 +211,7 @@ void DataflowAnalysisContext::dumpFlowCondition(Atom Token, llvm::raw_ostream &OS) { llvm::SetVector Constraints; Constraints.insert(&arena().makeAtomRef(Token)); - llvm::DenseSet VisitedTokens; - addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); + addTransitiveFlowConditionConstraints(Token, Constraints); // TODO: have formulas know about true/false directly instead Atom True = arena().makeLiteral(true).getAtom(); -- cgit v1.1