From 01db10365e935ccca9dc2ed449b23319e170eea0 Mon Sep 17 00:00:00 2001 From: Yitzhak Mandelbaum Date: Mon, 28 Mar 2022 15:38:17 +0000 Subject: [PATCH] [clang][dataflow] Add support for correlation of boolean (tracked) values This patch extends the join logic for environments to explicitly handle boolean values. It creates the disjunction of both source values, guarded by the respective flow conditions from each input environment. This change allows the framework to reason about boolean correlations across multiple branches (and subsequent joins). Differential Revision: https://reviews.llvm.org/D122838 --- .../Analysis/FlowSensitive/DataflowEnvironment.h | 4 ++ .../Analysis/FlowSensitive/DataflowEnvironment.cpp | 53 ++++++++++++++++++--- .../Analysis/FlowSensitive/TransferTest.cpp | 55 ++++++++++++++++++++++ 3 files changed, 105 insertions(+), 7 deletions(-) diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h index fb7ab70..68d6e63 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h @@ -293,6 +293,10 @@ public: : makeAnd(makeImplication(LHS, RHS), makeImplication(RHS, LHS)); } + const llvm::DenseSet &getFlowConditionConstraints() const { + return FlowConditionConstraints; + } + /// Adds `Val` to the set of clauses that constitute the flow condition. void addToFlowCondition(BoolValue &Val); diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp index 79bbfa0..5b372dd 100644 --- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp @@ -65,6 +65,49 @@ static bool equivalentValues(QualType Type, Value *Val1, return Model.compareEquivalent(Type, *Val1, Env1, *Val2, Env2); } +/// Attempts to merge distinct values `Val1` and `Val1` in `Env1` and `Env2`, +/// respectively, of the same type `Type`. Merging generally produces a single +/// value that (soundly) approximates the two inputs, although the actual +/// meaning depends on `Model`. +static Value *mergeDistinctValues(QualType Type, Value *Val1, Environment &Env1, + Value *Val2, const Environment &Env2, + Environment::ValueModel &Model) { + // Join distinct boolean values preserving information about the constraints + // in the respective path conditions. Note: this construction can, in + // principle, result in exponential growth in the size of boolean values. + // Potential optimizations may be worth considering. For example, represent + // the flow condition of each environment using a bool atom and store, in + // `DataflowAnalysisContext`, a mapping of bi-conditionals between flow + // condition atoms and flow condition constraints. Something like: + // \code + // FC1 <=> C1 ^ C2 + // FC2 <=> C2 ^ C3 ^ C4 + // FC3 <=> (FC1 v FC2) ^ C5 + // \code + // Then, we can track dependencies between flow conditions (e.g. above `FC3` + // depends on `FC1` and `FC2`) and modify `flowConditionImplies` to construct + // a formula that includes the bi-conditionals for all flow condition atoms in + // the transitive set, before invoking the solver. + if (auto *Expr1 = dyn_cast(Val1)) { + for (BoolValue *Constraint : Env1.getFlowConditionConstraints()) { + Expr1 = &Env1.makeAnd(*Expr1, *Constraint); + } + auto *Expr2 = cast(Val2); + for (BoolValue *Constraint : Env2.getFlowConditionConstraints()) { + Expr2 = &Env1.makeAnd(*Expr2, *Constraint); + } + return &Env1.makeOr(*Expr1, *Expr2); + } + + // FIXME: Consider destroying `MergedValue` immediately if `ValueModel::merge` + // returns false to avoid storing unneeded values in `DACtx`. + if (Value *MergedVal = Env1.createValue(Type)) + if (Model.merge(Type, *Val1, Env1, *Val2, Env2, *MergedVal, Env1)) + return MergedVal; + + return nullptr; +} + /// Initializes a global storage value. static void initGlobalVar(const VarDecl &D, Environment &Env) { if (!D.hasGlobalStorage() || @@ -309,13 +352,9 @@ LatticeJoinEffect Environment::join(const Environment &Other, continue; } - // FIXME: Consider destroying `MergedValue` immediately if - // `ValueModel::merge` returns false to avoid storing unneeded values in - // `DACtx`. - if (Value *MergedVal = createValue(Loc->getType())) - if (Model.merge(Loc->getType(), *Val, *this, *It->second, Other, - *MergedVal, *this)) - LocToVal.insert({Loc, MergedVal}); + if (Value *MergedVal = mergeDistinctValues(Loc->getType(), Val, *this, + It->second, Other, Model)) + LocToVal.insert({Loc, MergedVal}); } if (OldLocToVal.size() != LocToVal.size()) Effect = LatticeJoinEffect::Changed; diff --git a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp index 0e474c8..540ed47 100644 --- a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp @@ -35,6 +35,7 @@ using ::testing::ElementsAre; using ::testing::IsNull; using ::testing::NotNull; using ::testing::Pair; +using ::testing::SizeIs; class TransferTest : public ::testing::Test { protected: @@ -2648,4 +2649,58 @@ TEST_F(TransferTest, BooleanInequality) { }); } +TEST_F(TransferTest, CorrelatedBranches) { + std::string Code = R"( + void target(bool B, bool C) { + if (B) { + return; + } + (void)0; + /*[[p0]]*/ + if (C) { + B = true; + /*[[p1]]*/ + } + if (B) { + (void)0; + /*[[p2]]*/ + } + } + )"; + runDataflow( + Code, [](llvm::ArrayRef< + std::pair>> + Results, + ASTContext &ASTCtx) { + ASSERT_THAT(Results, SizeIs(3)); + + const ValueDecl *CDecl = findValueDecl(ASTCtx, "C"); + ASSERT_THAT(CDecl, NotNull()); + + { + ASSERT_THAT(Results[2], Pair("p0", _)); + const Environment &Env = Results[2].second.Env; + const ValueDecl *BDecl = findValueDecl(ASTCtx, "B"); + ASSERT_THAT(BDecl, NotNull()); + auto &BVal = *cast(Env.getValue(*BDecl, SkipPast::None)); + + EXPECT_TRUE(Env.flowConditionImplies(Env.makeNot(BVal))); + } + + { + ASSERT_THAT(Results[1], Pair("p1", _)); + const Environment &Env = Results[1].second.Env; + auto &CVal = *cast(Env.getValue(*CDecl, SkipPast::None)); + EXPECT_TRUE(Env.flowConditionImplies(CVal)); + } + + { + ASSERT_THAT(Results[0], Pair("p2", _)); + const Environment &Env = Results[0].second.Env; + auto &CVal = *cast(Env.getValue(*CDecl, SkipPast::None)); + EXPECT_TRUE(Env.flowConditionImplies(CVal)); + } + }); +} + } // namespace -- 2.7.4