wyt updated this revision to Diff 439719. wyt marked an inline comment as done. wyt added a comment.
Address comments - improve test clarity by comparing substituted flow condition with an expected value using `equivalentBoolValues` utility. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D128363/new/ 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 @@ -231,4 +231,132 @@ Context.getOrCreateConjunction(X, Context.getOrCreateConjunction(Y, Z)))); } +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 Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp =================================================================== --- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -167,6 +167,76 @@ } } +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; + 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()) { + return getBoolLiteralValue(true); + } + return substituteBoolValue(*ConstraintsIT->second, SubstitutionsCache); +} + } // 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 @@ -195,6 +195,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); @@ -230,6 +245,23 @@ 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.
_______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits