Author: martinboehme Date: 2024-01-16T08:25:21+01:00 New Revision: af1463d403182720ae0e3fab07634817dd0f41be
URL: https://github.com/llvm/llvm-project/commit/af1463d403182720ae0e3fab07634817dd0f41be DIFF: https://github.com/llvm/llvm-project/commit/af1463d403182720ae0e3fab07634817dd0f41be.diff LOG: [clang][dataflow] Add an early-out to `flowConditionImplies()` / `flowConditionAllows()`. (#78172) This saves having to assemble the set of constraints and run the SAT solver in the trivial case of `flowConditionImplies(true)` or `flowConditionAllows(false)`. This is an update / reland of my previous reverted [#77453](https://github.com/llvm/llvm-project/pull/77453). That PR contained a logic bug -- the early-out for `flowConditionAllows()` was wrong because my intuition about the logic was wrong. (In particular, note that `flowConditionImplies(F)` does not imply `flowConditionAllows(F)`, even though this may run counter to intuition.) I've now done what I should have done on the first iteration and added more tests. These pass both with and without my early-outs. This patch is a performance win on the benchmarks for the Crubit nullability checker, except for one slight regression on a relatively short benchmark: ``` name old cpu/op new cpu/op delta BM_PointerAnalysisCopyPointer 68.5µs ± 7% 67.6µs ± 4% ~ (p=0.159 n=18+19) BM_PointerAnalysisIntLoop 173µs ± 3% 162µs ± 4% -6.40% (p=0.000 n=19+20) BM_PointerAnalysisPointerLoop 307µs ± 2% 312µs ± 4% +1.56% (p=0.013 n=18+20) BM_PointerAnalysisBranch 199µs ± 4% 181µs ± 4% -8.81% (p=0.000 n=20+20) BM_PointerAnalysisLoopAndBranch 503µs ± 3% 508µs ± 2% ~ (p=0.081 n=18+19) BM_PointerAnalysisTwoLoops 304µs ± 4% 286µs ± 2% -6.04% (p=0.000 n=19+20) BM_PointerAnalysisJoinFilePath 4.78ms ± 3% 4.54ms ± 4% -4.97% (p=0.000 n=20+20) BM_PointerAnalysisCallInLoop 3.05ms ± 3% 2.90ms ± 4% -5.05% (p=0.000 n=19+20) ``` When running clang-tidy on real-world code, the results are less clear. In three runs, averaged, on an arbitrarily chosen input file, I get 11.60 s of user time without this patch and 11.40 s with it, though with considerable measurement noise (I'm seeing up to 0.2 s of variation between runs). Still, this is a very simple change, and it is a clear win in benchmarks, so I think it is worth making. Added: Modified: clang/include/clang/Analysis/FlowSensitive/Formula.h clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp Removed: ################################################################################ diff --git a/clang/include/clang/Analysis/FlowSensitive/Formula.h b/clang/include/clang/Analysis/FlowSensitive/Formula.h index 982e400c1deff1..0e6352403a832f 100644 --- a/clang/include/clang/Analysis/FlowSensitive/Formula.h +++ b/clang/include/clang/Analysis/FlowSensitive/Formula.h @@ -75,6 +75,10 @@ class alignas(const Formula *) Formula { return static_cast<bool>(Value); } + bool isLiteral(bool b) const { + return kind() == Literal && static_cast<bool>(Value) == b; + } + ArrayRef<const Formula *> operands() const { return ArrayRef(reinterpret_cast<Formula *const *>(this + 1), numOperands(kind())); diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp index fa114979c8e326..d95b3324ef6b2a 100644 --- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -174,6 +174,9 @@ Solver::Result DataflowAnalysisContext::querySolver( bool DataflowAnalysisContext::flowConditionImplies(Atom Token, const Formula &F) { + if (F.isLiteral(true)) + return true; + // Returns true if and only if truth assignment of the flow condition implies // that `F` is also true. We prove whether or not this property holds by // reducing the problem to satisfiability checking. In other words, we attempt @@ -188,6 +191,9 @@ bool DataflowAnalysisContext::flowConditionImplies(Atom Token, bool DataflowAnalysisContext::flowConditionAllows(Atom Token, const Formula &F) { + if (F.isLiteral(false)) + return false; + llvm::SetVector<const Formula *> Constraints; Constraints.insert(&arena().makeAtomRef(Token)); Constraints.insert(&F); diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp index 88eb11045b9e9f..4f7a72c502ccfe 100644 --- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp @@ -33,10 +33,34 @@ TEST_F(DataflowAnalysisContextTest, DistinctTopsNotEquivalent) { EXPECT_FALSE(Context.equivalentFormulas(X.formula(), Y.formula())); } -TEST_F(DataflowAnalysisContextTest, EmptyFlowCondition) { +TEST_F(DataflowAnalysisContextTest, TautologicalFlowConditionImplies) { Atom FC = A.makeFlowConditionToken(); - auto &C = A.makeAtomRef(A.makeAtom()); - EXPECT_FALSE(Context.flowConditionImplies(FC, C)); + EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeLiteral(true))); + EXPECT_FALSE(Context.flowConditionImplies(FC, A.makeLiteral(false))); + EXPECT_FALSE(Context.flowConditionImplies(FC, A.makeAtomRef(A.makeAtom()))); +} + +TEST_F(DataflowAnalysisContextTest, TautologicalFlowConditionAllows) { + Atom FC = A.makeFlowConditionToken(); + EXPECT_TRUE(Context.flowConditionAllows(FC, A.makeLiteral(true))); + EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeLiteral(false))); + EXPECT_TRUE(Context.flowConditionAllows(FC, A.makeAtomRef(A.makeAtom()))); +} + +TEST_F(DataflowAnalysisContextTest, ContradictoryFlowConditionImpliesAnything) { + Atom FC = A.makeFlowConditionToken(); + Context.addFlowConditionConstraint(FC, A.makeLiteral(false)); + EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeLiteral(true))); + EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeLiteral(false))); + EXPECT_TRUE(Context.flowConditionImplies(FC, A.makeAtomRef(A.makeAtom()))); +} + +TEST_F(DataflowAnalysisContextTest, ContradictoryFlowConditionAllowsNothing) { + Atom FC = A.makeFlowConditionToken(); + Context.addFlowConditionConstraint(FC, A.makeLiteral(false)); + EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeLiteral(true))); + EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeLiteral(false))); + EXPECT_FALSE(Context.flowConditionAllows(FC, A.makeAtomRef(A.makeAtom()))); } TEST_F(DataflowAnalysisContextTest, AddFlowConditionConstraint) { _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
