ymandel created this revision.
ymandel added reviewers: xazax.hun, sgatev.
Herald added subscribers: tschuett, steakhal, rnkovacs.
Herald added a project: All.
ymandel requested review of this revision.
Herald added a project: clang.
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).
Repository:
rG LLVM Github Monorepo
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:
@@ -2410,4 +2411,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,35 @@
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.
+ 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() ||
@@ -273,13 +302,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
