This revision was automatically updated to reflect the committed changes.
ymandel marked an inline comment as done.
Closed by commit rG01db10365e93: [clang][dataflow] Add support for correlation
of boolean (tracked) values (authored by ymandel).
Changed prior to commit:
https://reviews.llvm.org/D122838?vs=419764&id=419797#toc
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D122838/new/
https://reviews.llvm.org/D122838
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
@@ -35,6 +35,7 @@
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, 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
Index: clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -65,6 +65,49 @@
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 @@
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;
Index: clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -293,6 +293,10 @@
: 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);
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
