wyt created this revision.
Herald added subscribers: martong, tschuett, xazax.hun.
Herald added a project: All.
wyt requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
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 <https://reviews.llvm.org/D128357>
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D128363
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -169,4 +169,54 @@
EXPECT_TRUE(Context.flowConditionIsTautology(FC5));
}
+// FIXME: Consider implementing pretty print feature for values for clarity of
+// testing
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionEmptyFC) {
+ auto &FC = Context.makeFlowConditionToken();
+ auto &X = Context.createAtomicBoolValue();
+
+ auto XTrue = llvm::DenseMap<AtomicBoolValue *, BoolValue *>(
+ {{&X, &Context.getBoolLiteralValue(true)}});
+ auto &FCWithXTrue = Context.buildAndSubstituteFlowCondition(FC, XTrue);
+
+ auto XFalse = llvm::DenseMap<AtomicBoolValue *, BoolValue *>(
+ {{&X, &Context.getBoolLiteralValue(false)}});
+ auto &FCWithXFalse = Context.buildAndSubstituteFlowCondition(FC, XFalse);
+
+ auto &FCIndependentOfX =
+ Context.getOrCreateConjunctionValue(FCWithXTrue, FCWithXFalse);
+
+ // FC = {}
+ // Empty flow condition holds regardless of value of boolean X
+ EXPECT_TRUE(Context.flowConditionImplies(FC, FCIndependentOfX));
+}
+
+TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsDisjunctiveFC1) {
+ auto &FC = Context.makeFlowConditionToken();
+ auto &B = Context.createAtomicBoolValue();
+ auto &X = Context.createAtomicBoolValue();
+ Context.addFlowConditionConstraint(
+ FC, Context.getOrCreateDisjunctionValue(
+ Context.getOrCreateNegationValue(B),
+ Context.getOrCreateConjunctionValue(B, X)));
+
+ auto XTrue = llvm::DenseMap<AtomicBoolValue *, BoolValue *>(
+ {{&X, &Context.getBoolLiteralValue(true)}});
+ auto &FCWithXTrue = Context.buildAndSubstituteFlowCondition(FC, XTrue);
+
+ auto XFalse = llvm::DenseMap<AtomicBoolValue *, BoolValue *>(
+ {{&X, &Context.getBoolLiteralValue(false)}});
+ auto &FCWithXFalse = Context.buildAndSubstituteFlowCondition(FC, XFalse);
+
+ auto &FCIndependentOfX =
+ Context.getOrCreateConjunctionValue(FCWithXTrue, FCWithXFalse);
+
+ // FC = (!B) || (B && X)
+ // The flow condition holds when
+ // 1. B is false, independent of value of X
+ // 2. B is true, and X is true
+ EXPECT_TRUE(Context.flowConditionImplies(
+ FC, Context.getOrCreateDisjunctionValue(FCIndependentOfX, B)));
+}
+
} // namespace
Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -158,6 +158,77 @@
}
}
+BoolValue &DataflowAnalysisContext::substituteBoolVal(
+ 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 = substituteBoolVal(Negation.getSubVal(), SubstitutionsCache);
+ Result = &getOrCreateNegationValue(Sub);
+ break;
+ }
+ case Value::Kind::Disjunction: {
+ auto &Disjunct = *cast<DisjunctionValue>(&Val);
+ auto &LeftSub =
+ substituteBoolVal(Disjunct.getLeftSubValue(), SubstitutionsCache);
+ auto &RightSub =
+ substituteBoolVal(Disjunct.getRightSubValue(), SubstitutionsCache);
+ Result = &getOrCreateDisjunctionValue(LeftSub, RightSub);
+ break;
+ }
+ case Value::Kind::Conjunction: {
+ auto &Conjunct = *cast<ConjunctionValue>(&Val);
+ auto &LeftSub =
+ substituteBoolVal(Conjunct.getLeftSubValue(), SubstitutionsCache);
+ auto &RightSub =
+ substituteBoolVal(Conjunct.getRightSubValue(), SubstitutionsCache);
+ Result = &getOrCreateConjunctionValue(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;
+ SubstitutionsCache.insert(Substitutions.begin(), Substitutions.end());
+ return buildAndSubstituteFlowConditionWithCache(Token, SubstitutionsCache);
+}
+
+BoolValue &DataflowAnalysisContext::buildAndSubstituteFlowConditionWithCache(
+ AtomicBoolValue &Token,
+ llvm::DenseMap<BoolValue *, BoolValue *> &SubstitutionsCache) {
+ auto DepsIt = FlowConditionDeps.find(&Token);
+ if (DepsIt != FlowConditionDeps.end()) {
+ for (AtomicBoolValue *DepToken : DepsIt->second) {
+ auto &NewDep = buildAndSubstituteFlowConditionWithCache(
+ *DepToken, SubstitutionsCache);
+ SubstitutionsCache[DepToken] = &NewDep;
+ }
+ }
+ auto ConstraintsIt = FlowConditionConstraints.find(&Token);
+ if (ConstraintsIt != FlowConditionConstraints.end()) {
+ auto &Constraints = *ConstraintsIt->second;
+ return substituteBoolVal(Constraints, SubstitutionsCache);
+ }
+ return getBoolLiteralValue(true);
+}
+
} // namespace dataflow
} // namespace clang
Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -183,6 +183,21 @@
AtomicBoolValue &joinFlowConditions(AtomicBoolValue &FirstToken,
AtomicBoolValue &SecondToken);
+ // FIXME: This function returns the flow condition expressed directly as its
+ // constraints: (C1 AND C2 AND ...). This differs 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.
+ 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);
@@ -200,6 +215,23 @@
AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);
+ /// 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 &substituteBoolVal(
+ 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.
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
