[clang] 01db103 - [clang][dataflow] Add support for correlation of boolean (tracked) values
Yitzhak Mandelbaum via cfe-commits
cfe-commits at lists.llvm.org
Fri Apr 1 10:30:05 PDT 2022
Author: Yitzhak Mandelbaum
Date: 2022-04-01T17:25:49Z
New Revision: 01db10365e935ccca9dc2ed449b23319e170eea0
URL: https://github.com/llvm/llvm-project/commit/01db10365e935ccca9dc2ed449b23319e170eea0
DIFF: https://github.com/llvm/llvm-project/commit/01db10365e935ccca9dc2ed449b23319e170eea0.diff
LOG: [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
Added:
Modified:
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
Removed:
################################################################################
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
index fb7ab70fa4109..68d6e6345f639 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -293,6 +293,10 @@ class Environment {
: makeAnd(makeImplication(LHS, RHS), makeImplication(RHS, LHS));
}
+ const llvm::DenseSet<BoolValue *> &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 79bbfa091f6cb..5b372dde89532 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<BoolValue>(Val1)) {
+ for (BoolValue *Constraint : Env1.getFlowConditionConstraints()) {
+ Expr1 = &Env1.makeAnd(*Expr1, *Constraint);
+ }
+ auto *Expr2 = cast<BoolValue>(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 0e474c84a1b5f..540ed4781aebf 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<std::string, DataflowAnalysisState<NoopLattice>>>
+ 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<BoolValue>(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<BoolValue>(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<BoolValue>(Env.getValue(*CDecl, SkipPast::None));
+ EXPECT_TRUE(Env.flowConditionImplies(CVal));
+ }
+ });
+}
+
} // namespace
More information about the cfe-commits
mailing list