From 5e4ad816bf100b0325ed45ab1cfea18deb3ab3d1 Mon Sep 17 00:00:00 2001 From: Sam McCall Date: Wed, 21 Jun 2023 18:59:01 +0200 Subject: [dataflow] Replace most BoolValue subclasses with references to Formula (and AtomicBoolValue => Atom and BoolValue => Formula where appropriate) This properly frees the Value hierarchy from managing boolean formulas. We still distinguish AtomicBoolValue; this type is used in client code. However we expect to convert such uses to BoolValue (where the distinction is not needed) or Atom (where atomic identity is intended), and then fold AtomicBoolValue into FormulaBoolValue. We also distinguish TopBoolValue; this has distinct rules for widen/join/equivalence, and top-ness is not represented in Formula. It'd be nice to find a cleaner representation (e.g. the absence of a formula), but no immediate plans. For now, BoolValues with the same Formula are deduplicated. This doesn't seem desirable, as Values are mutable by their creators (properties). We can probably drop this for FormulaBoolValue immediately (not in this patch, to isolate changes). For AtomicBoolValue we first need to update clients to stop using value pointers for atom identity. The data structures around flow conditions are updated: - flow condition tokens are Atom, rather than AtomicBoolValue* - conditions are Formula, rather than BoolValue Most APIs were changed directly, some with many clients had a new version added and the existing one deprecated. The factories for BoolValues in Environment keep their existing signatures for now (e.g. makeOr(BoolValue, BoolValue) => BoolValue) and are not deprecated. These have very many clients and finding the most ergonomic API & migration path still needs some thought. Differential Revision: https://reviews.llvm.org/D153469 --- .../FlowSensitive/DataflowAnalysisContext.cpp | 97 +++++++++++----------- 1 file changed, 47 insertions(+), 50 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 42cc6d4..a807ef8 100644 --- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -102,115 +102,112 @@ DataflowAnalysisContext::getOrCreateNullPointerValue(QualType PointeeType) { } void DataflowAnalysisContext::addFlowConditionConstraint( - AtomicBoolValue &Token, BoolValue &Constraint) { - auto Res = FlowConditionConstraints.try_emplace(&Token, &Constraint); + Atom Token, const Formula &Constraint) { + auto Res = FlowConditionConstraints.try_emplace(Token, &Constraint); if (!Res.second) { Res.first->second = &arena().makeAnd(*Res.first->second, Constraint); } } -AtomicBoolValue & -DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) { - auto &ForkToken = arena().makeFlowConditionToken(); - FlowConditionDeps[&ForkToken].insert(&Token); - addFlowConditionConstraint(ForkToken, Token); +Atom DataflowAnalysisContext::forkFlowCondition(Atom Token) { + Atom ForkToken = arena().makeFlowConditionToken(); + FlowConditionDeps[ForkToken].insert(Token); + addFlowConditionConstraint(ForkToken, arena().makeAtomRef(Token)); return ForkToken; } -AtomicBoolValue & -DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken, - AtomicBoolValue &SecondToken) { - auto &Token = arena().makeFlowConditionToken(); - FlowConditionDeps[&Token].insert(&FirstToken); - FlowConditionDeps[&Token].insert(&SecondToken); - addFlowConditionConstraint( - Token, arena().makeOr(FirstToken, SecondToken)); +Atom +DataflowAnalysisContext::joinFlowConditions(Atom FirstToken, + Atom SecondToken) { + Atom Token = arena().makeFlowConditionToken(); + FlowConditionDeps[Token].insert(FirstToken); + FlowConditionDeps[Token].insert(SecondToken); + addFlowConditionConstraint(Token, + arena().makeOr(arena().makeAtomRef(FirstToken), + arena().makeAtomRef(SecondToken))); return Token; } -Solver::Result -DataflowAnalysisContext::querySolver(llvm::SetVector Constraints) { +Solver::Result DataflowAnalysisContext::querySolver( + llvm::SetVector Constraints) { Constraints.insert(&arena().makeLiteral(true)); Constraints.insert(&arena().makeNot(arena().makeLiteral(false))); - std::vector Formulas; - for (const BoolValue *Constraint : Constraints) - Formulas.push_back(&arena().getFormula(*Constraint)); - return S->solve(Formulas); + return S->solve(Constraints.getArrayRef()); } -bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token, - BoolValue &Val) { +bool DataflowAnalysisContext::flowConditionImplies(Atom Token, + const Formula &Val) { // Returns true if and only if truth assignment of the flow condition implies // that `Val` is also true. We prove whether or not this property holds by // reducing the problem to satisfiability checking. In other words, we attempt // to show that assuming `Val` is false makes the constraints induced by the // flow condition unsatisfiable. - llvm::SetVector Constraints; - Constraints.insert(&Token); + llvm::SetVector Constraints; + Constraints.insert(&arena().makeAtomRef(Token)); Constraints.insert(&arena().makeNot(Val)); - llvm::DenseSet VisitedTokens; + llvm::DenseSet VisitedTokens; addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); return isUnsatisfiable(std::move(Constraints)); } -bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) { +bool DataflowAnalysisContext::flowConditionIsTautology(Atom Token) { // Returns true if and only if we cannot prove that the flow condition can // ever be false. - llvm::SetVector Constraints; - Constraints.insert(&arena().makeNot(Token)); - llvm::DenseSet VisitedTokens; + llvm::SetVector Constraints; + Constraints.insert(&arena().makeNot(arena().makeAtomRef(Token))); + llvm::DenseSet VisitedTokens; addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); return isUnsatisfiable(std::move(Constraints)); } -bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1, - BoolValue &Val2) { - llvm::SetVector Constraints; +bool DataflowAnalysisContext::equivalentFormulas(const Formula &Val1, + const Formula &Val2) { + llvm::SetVector Constraints; Constraints.insert(&arena().makeNot(arena().makeEquals(Val1, Val2))); return isUnsatisfiable(std::move(Constraints)); } void DataflowAnalysisContext::addTransitiveFlowConditionConstraints( - AtomicBoolValue &Token, llvm::SetVector &Constraints, - llvm::DenseSet &VisitedTokens) { - auto Res = VisitedTokens.insert(&Token); + Atom Token, llvm::SetVector &Constraints, + llvm::DenseSet &VisitedTokens) { + auto Res = VisitedTokens.insert(Token); if (!Res.second) return; - auto ConstraintsIt = FlowConditionConstraints.find(&Token); + auto ConstraintsIt = FlowConditionConstraints.find(Token); if (ConstraintsIt == FlowConditionConstraints.end()) { - Constraints.insert(&Token); + 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(Token, *ConstraintsIt->second)); + Constraints.insert(&arena().makeEquals(arena().makeAtomRef(Token), + *ConstraintsIt->second)); } - auto DepsIt = FlowConditionDeps.find(&Token); + auto DepsIt = FlowConditionDeps.find(Token); if (DepsIt != FlowConditionDeps.end()) { - for (AtomicBoolValue *DepToken : DepsIt->second) { - addTransitiveFlowConditionConstraints(*DepToken, Constraints, + for (Atom DepToken : DepsIt->second) { + addTransitiveFlowConditionConstraints(DepToken, Constraints, VisitedTokens); } } } -void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token, +void DataflowAnalysisContext::dumpFlowCondition(Atom Token, llvm::raw_ostream &OS) { - // TODO: accumulate formulas directly instead - llvm::SetVector Constraints; - Constraints.insert(&Token); - llvm::DenseSet VisitedTokens; + llvm::SetVector Constraints; + Constraints.insert(&arena().makeAtomRef(Token)); + llvm::DenseSet VisitedTokens; addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); // TODO: have formulas know about true/false directly instead - Atom True = arena().getFormula(arena().makeLiteral(true)).getAtom(); - Atom False = arena().getFormula(arena().makeLiteral(false)).getAtom(); + Atom True = arena().makeLiteral(true).getAtom(); + Atom False = arena().makeLiteral(false).getAtom(); Formula::AtomNames Names = {{False, "false"}, {True, "true"}}; for (const auto *Constraint : Constraints) { - arena().getFormula(*Constraint).print(OS, &Names); + Constraint->print(OS, &Names); OS << "\n"; } } -- cgit v1.1