[clang] bdfe556 - [clang][dataflow] Implement functionality for flow condition variable substitution.
Dmitri Gribenko via cfe-commits
cfe-commits at lists.llvm.org
Mon Jun 27 02:37:53 PDT 2022
Author: Wei Yi Tee
Date: 2022-06-27T11:37:46+02:00
New Revision: bdfe556dd837007c5671f33384d26e9ea315db53
URL: https://github.com/llvm/llvm-project/commit/bdfe556dd837007c5671f33384d26e9ea315db53
DIFF: https://github.com/llvm/llvm-project/commit/bdfe556dd837007c5671f33384d26e9ea315db53.diff
LOG: [clang][dataflow] Implement functionality for flow condition variable substitution.
This patch introduces `buildAndSubstituteFlowCondition` - given a flow condition token, this function returns the expression of constraints defining the flow condition, with values substituted where specified.
As an example:
Say we have tokens `FC1`, `FC2`, `FC3`:
```
FlowConditionConstraints: {
FC1: C1,
FC2: C2,
FC3: (FC1 v FC2) ^ C3,
}
```
`buildAndSubstituteFlowCondition(FC3, /*Substitutions:*/{{C1 -> C1'}})`
returns a value corresponding to `(C1' v C2) ^ C3`.
Note:
This function returns the flow condition expressed directly as its constraints, which differs to how we currently represent the flow condition as a token bound to a set of constraints and dependencies. Making the representation consistent may be an option to consider in the future.
Depends On D128357
Reviewed By: gribozavr2, xazax.hun
Differential Revision: https://reviews.llvm.org/D128363
Added:
Modified:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
Removed:
################################################################################
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
index 58acd5639c436..2e6b8ea7b0da0 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -211,6 +211,27 @@ class DataflowAnalysisContext {
AtomicBoolValue &joinFlowConditions(AtomicBoolValue &FirstToken,
AtomicBoolValue &SecondToken);
+ // FIXME: This function returns the flow condition expressed directly as its
+ // constraints: (C1 AND C2 AND ...). This
diff ers from the general approach in
+ // the framework where a flow condition is represented as a token (an atomic
+ // boolean) with dependencies and constraints tracked in `FlowConditionDeps`
+ // and `FlowConditionConstraints`: (FC <=> C1 AND C2 AND ...).
+ // Consider if we should make the representation of flow condition consistent,
+ // returning an atomic boolean token with separate constraints instead.
+ //
+ /// Builds and returns the logical formula defining the flow condition
+ /// identified by `Token`. If a value in the formula is present as a key in
+ /// `Substitutions`, it will be substituted with the value it maps to.
+ /// As an example, say we have flow condition tokens FC1, FC2, FC3 and
+ /// FlowConditionConstraints: { FC1: C1,
+ /// FC2: C2,
+ /// FC3: (FC1 v FC2) ^ C3 }
+ /// buildAndSubstituteFlowCondition(FC3, {{C1 -> C1'}}) will return a value
+ /// corresponding to (C1' v C2) ^ C3.
+ BoolValue &buildAndSubstituteFlowCondition(
+ AtomicBoolValue &Token,
+ llvm::DenseMap<AtomicBoolValue *, BoolValue *> Substitutions);
+
/// Returns true if and only if the constraints of the flow condition
/// identified by `Token` imply that `Val` is true.
bool flowConditionImplies(AtomicBoolValue &Token, BoolValue &Val);
@@ -246,6 +267,23 @@ class DataflowAnalysisContext {
return querySolver(std::move(Constraints)) == Solver::Result::Unsatisfiable;
}
+ /// Returns a boolean value as a result of substituting `Val` and its sub
+ /// values based on entries in `SubstitutionsCache`. Intermediate results are
+ /// stored in `SubstitutionsCache` to avoid reprocessing values that have
+ /// already been visited.
+ BoolValue &substituteBoolValue(
+ BoolValue &Val,
+ llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache);
+
+ /// Builds and returns the logical formula defining the flow condition
+ /// identified by `Token`, sub values may be substituted based on entries in
+ /// `SubstitutionsCache`. Intermediate results are stored in
+ /// `SubstitutionsCache` to avoid reprocessing values that have already been
+ /// visited.
+ BoolValue &buildAndSubstituteFlowConditionWithCache(
+ AtomicBoolValue &Token,
+ llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache);
+
std::unique_ptr<Solver> S;
// Storage for the state of a program.
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 9e4b03e36bb70..de48fd71b065b 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -202,6 +202,76 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
}
}
+BoolValue &DataflowAnalysisContext::substituteBoolValue(
+ BoolValue &Val,
+ llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache) {
+ auto IT = SubstitutionsCache.find(&Val);
+ if (IT != SubstitutionsCache.end()) {
+ return *IT->second;
+ }
+ BoolValue *Result;
+ switch (Val.getKind()) {
+ case Value::Kind::AtomicBool: {
+ Result = &Val;
+ break;
+ }
+ case Value::Kind::Negation: {
+ auto &Negation = *cast<NegationValue>(&Val);
+ auto &Sub = substituteBoolValue(Negation.getSubVal(), SubstitutionsCache);
+ Result = &getOrCreateNegation(Sub);
+ break;
+ }
+ case Value::Kind::Disjunction: {
+ auto &Disjunct = *cast<DisjunctionValue>(&Val);
+ auto &LeftSub =
+ substituteBoolValue(Disjunct.getLeftSubValue(), SubstitutionsCache);
+ auto &RightSub =
+ substituteBoolValue(Disjunct.getRightSubValue(), SubstitutionsCache);
+ Result = &getOrCreateDisjunction(LeftSub, RightSub);
+ break;
+ }
+ case Value::Kind::Conjunction: {
+ auto &Conjunct = *cast<ConjunctionValue>(&Val);
+ auto &LeftSub =
+ substituteBoolValue(Conjunct.getLeftSubValue(), SubstitutionsCache);
+ auto &RightSub =
+ substituteBoolValue(Conjunct.getRightSubValue(), SubstitutionsCache);
+ Result = &getOrCreateConjunction(LeftSub, RightSub);
+ break;
+ }
+ default:
+ llvm_unreachable("Unhandled Value Kind");
+ }
+ SubstitutionsCache[&Val] = Result;
+ return *Result;
+}
+
+BoolValue &DataflowAnalysisContext::buildAndSubstituteFlowCondition(
+ AtomicBoolValue &Token,
+ llvm::DenseMap<AtomicBoolValue *, BoolValue *> Substitutions) {
+ llvm::DenseMap<BoolValue *, BoolValue *> SubstitutionsCache(
+ Substitutions.begin(), Substitutions.end());
+ return buildAndSubstituteFlowConditionWithCache(Token, SubstitutionsCache);
+}
+
+BoolValue &DataflowAnalysisContext::buildAndSubstituteFlowConditionWithCache(
+ AtomicBoolValue &Token,
+ llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache) {
+ auto ConstraintsIT = FlowConditionConstraints.find(&Token);
+ if (ConstraintsIT == FlowConditionConstraints.end()) {
+ return getBoolLiteralValue(true);
+ }
+ auto DepsIT = FlowConditionDeps.find(&Token);
+ if (DepsIT != FlowConditionDeps.end()) {
+ for (AtomicBoolValue *DepToken : DepsIT->second) {
+ auto &NewDep = buildAndSubstituteFlowConditionWithCache(
+ *DepToken, SubstitutionsCache);
+ SubstitutionsCache[DepToken] = &NewDep;
+ }
+ }
+ return substituteBoolValue(*ConstraintsIT->second, SubstitutionsCache);
+}
+
} // namespace dataflow
} // namespace clang
diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
index 1f0116cdbf2ef..26bc37bda617b 100644
--- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -276,4 +276,172 @@ TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
Context.getOrCreateConjunction(X, Context.getOrCreateConjunction(Y, Z))));
}
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsAtomicFC) {
+ auto &X = Context.createAtomicBoolValue();
+ auto &True = Context.getBoolLiteralValue(true);
+ auto &False = Context.getBoolLiteralValue(false);
+
+ // FC = X
+ auto &FC = Context.makeFlowConditionToken();
+ Context.addFlowConditionConstraint(FC, X);
+
+ // If X is true in FC, FC = X must be true
+ auto &FCWithXTrue =
+ Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
+ EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True));
+
+ // If X is false in FC, FC = X must be false
+ auto &FC1WithXFalse =
+ Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
+ EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, False));
+}
+
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsNegatedFC) {
+ auto &X = Context.createAtomicBoolValue();
+ auto &True = Context.getBoolLiteralValue(true);
+ auto &False = Context.getBoolLiteralValue(false);
+
+ // FC = !X
+ auto &FC = Context.makeFlowConditionToken();
+ Context.addFlowConditionConstraint(FC, Context.getOrCreateNegation(X));
+
+ // If X is true in FC, FC = !X must be false
+ auto &FCWithXTrue =
+ Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
+ EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, False));
+
+ // If X is false in FC, FC = !X must be true
+ auto &FC1WithXFalse =
+ Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
+ EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, True));
+}
+
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsDisjunctiveFC) {
+ auto &X = Context.createAtomicBoolValue();
+ auto &Y = Context.createAtomicBoolValue();
+ auto &True = Context.getBoolLiteralValue(true);
+ auto &False = Context.getBoolLiteralValue(false);
+
+ // FC = X || Y
+ auto &FC = Context.makeFlowConditionToken();
+ Context.addFlowConditionConstraint(FC, Context.getOrCreateDisjunction(X, Y));
+
+ // If X is true in FC, FC = X || Y must be true
+ auto &FCWithXTrue =
+ Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
+ EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True));
+
+ // If X is false in FC, FC = X || Y is equivalent to evaluating Y
+ auto &FC1WithXFalse =
+ Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
+ EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, Y));
+}
+
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsConjunctiveFC) {
+ auto &X = Context.createAtomicBoolValue();
+ auto &Y = Context.createAtomicBoolValue();
+ auto &True = Context.getBoolLiteralValue(true);
+ auto &False = Context.getBoolLiteralValue(false);
+
+ // FC = X && Y
+ auto &FC = Context.makeFlowConditionToken();
+ Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y));
+
+ // If X is true in FC, FC = X && Y is equivalent to evaluating Y
+ auto &FCWithXTrue =
+ Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}});
+ EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y));
+
+ // If X is false in FC, FC = X && Y must be false
+ auto &FCWithXFalse =
+ Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}});
+ EXPECT_TRUE(Context.equivalentBoolValues(FCWithXFalse, False));
+}
+
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsForkedFC) {
+ auto &X = Context.createAtomicBoolValue();
+ auto &Y = Context.createAtomicBoolValue();
+ auto &Z = Context.createAtomicBoolValue();
+ auto &True = Context.getBoolLiteralValue(true);
+ auto &False = Context.getBoolLiteralValue(false);
+
+ // FC = X && Y
+ auto &FC = Context.makeFlowConditionToken();
+ Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y));
+ // ForkedFC = FC && Z = X && Y && Z
+ auto &ForkedFC = Context.forkFlowCondition(FC);
+ Context.addFlowConditionConstraint(ForkedFC, Z);
+
+ // If any of X,Y,Z is true in ForkedFC, ForkedFC = X && Y && Z is equivalent
+ // to evaluating the conjunction of the remaining values
+ auto &ForkedFCWithZTrue =
+ Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &True}});
+ EXPECT_TRUE(Context.equivalentBoolValues(
+ ForkedFCWithZTrue, Context.getOrCreateConjunction(X, Y)));
+ auto &ForkedFCWithYAndZTrue = Context.buildAndSubstituteFlowCondition(
+ ForkedFC, {{&Y, &True}, {&Z, &True}});
+ EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYAndZTrue, X));
+
+ // If any of X,Y,Z is false in ForkedFC, ForkedFC = X && Y && Z must be false
+ auto &ForkedFCWithXFalse =
+ Context.buildAndSubstituteFlowCondition(ForkedFC, {{&X, &False}});
+ auto &ForkedFCWithYFalse =
+ Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Y, &False}});
+ auto &ForkedFCWithZFalse =
+ Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &False}});
+ EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithXFalse, False));
+ EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYFalse, False));
+ EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithZFalse, False));
+}
+
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsJoinedFC) {
+ auto &X = Context.createAtomicBoolValue();
+ auto &Y = Context.createAtomicBoolValue();
+ auto &Z = Context.createAtomicBoolValue();
+ auto &True = Context.getBoolLiteralValue(true);
+ auto &False = Context.getBoolLiteralValue(false);
+
+ // FC1 = X
+ auto &FC1 = Context.makeFlowConditionToken();
+ Context.addFlowConditionConstraint(FC1, X);
+ // FC2 = Y
+ auto &FC2 = Context.makeFlowConditionToken();
+ Context.addFlowConditionConstraint(FC2, Y);
+ // JoinedFC = (FC1 || FC2) && Z = (X || Y) && Z
+ auto &JoinedFC = Context.joinFlowConditions(FC1, FC2);
+ Context.addFlowConditionConstraint(JoinedFC, Z);
+
+ // If any of X, Y is true in JoinedFC, JoinedFC = (X || Y) && Z is equivalent
+ // to evaluating the remaining Z
+ auto &JoinedFCWithXTrue =
+ Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &True}});
+ auto &JoinedFCWithYTrue =
+ Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &True}});
+ EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithXTrue, Z));
+ EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithYTrue, Z));
+
+ // If Z is true in JoinedFC, JoinedFC = (X || Y) && Z is equivalent to
+ // evaluating the remaining disjunction (X || Y)
+ auto &JoinedFCWithZTrue =
+ Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &True}});
+ EXPECT_TRUE(Context.equivalentBoolValues(
+ JoinedFCWithZTrue, Context.getOrCreateDisjunction(X, Y)));
+
+ // If any of X, Y is false in JoinedFC, JoinedFC = (X || Y) && Z is equivalent
+ // to evaluating the conjunction of the other value and Z
+ auto &JoinedFCWithXFalse =
+ Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &False}});
+ auto &JoinedFCWithYFalse =
+ Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &False}});
+ EXPECT_TRUE(Context.equivalentBoolValues(
+ JoinedFCWithXFalse, Context.getOrCreateConjunction(Y, Z)));
+ EXPECT_TRUE(Context.equivalentBoolValues(
+ JoinedFCWithYFalse, Context.getOrCreateConjunction(X, Z)));
+
+ // If Z is false in JoinedFC, JoinedFC = (X || Y) && Z must be false
+ auto &JoinedFCWithZFalse =
+ Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &False}});
+ EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithZFalse, False));
+}
+
} // namespace
More information about the cfe-commits
mailing list