================
@@ -6177,6 +6212,102 @@ TEST(TransferTest, ConditionalOperatorLocation) {
});
}
+TEST(TransferTest, ConditionalOperatorValuesTested) {
+ // Even though the LHS and the RHS of the conditional operator have different
+ // StorageLocations, we get constraints from the condition that the values
+ // must be equal to B1 for JoinDifferentIsB1, or B2 for JoinDifferentIsB2.
+ std::string Code = R"(
+ void target(bool B1, bool B2) {
+ bool JoinDifferentIsB1 = (B1 == B2) ? B2 : B1;
+ bool JoinDifferentIsB2 = (B1 == B2) ? B1 : B2;
+ // [[p]]
+ }
+ )";
+ runDataflow(
+ Code,
+ [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+ ASTContext &ASTCtx) {
+ Environment Env = getEnvironmentAtAnnotation(Results, "p").fork();
+
+ auto &B1 = getValueForDecl<BoolValue>(ASTCtx, Env, "B1");
+ auto &B2 = getValueForDecl<BoolValue>(ASTCtx, Env, "B2");
+ auto &JoinDifferentIsB1 =
+ getValueForDecl<BoolValue>(ASTCtx, Env, "JoinDifferentIsB1");
+ auto &JoinDifferentIsB2 =
+ getValueForDecl<BoolValue>(ASTCtx, Env, "JoinDifferentIsB2");
+
+ const Formula &JoinDifferentIsB1EqB1 =
+ Env.arena().makeEquals(JoinDifferentIsB1.formula(), B1.formula());
+ EXPECT_TRUE(Env.allows(JoinDifferentIsB1EqB1));
+ EXPECT_TRUE(Env.proves(JoinDifferentIsB1EqB1));
+
+ const Formula &JoinDifferentIsB2EqB2 =
+ Env.arena().makeEquals(JoinDifferentIsB2.formula(), B2.formula());
+ EXPECT_TRUE(Env.allows(JoinDifferentIsB2EqB2));
+ EXPECT_TRUE(Env.proves(JoinDifferentIsB2EqB2));
+ });
+}
+
+TEST(TransferTest, ConditionalOperatorLocationUpdatedAfter) {
+ // We don't currently model a Conditional Operator with an LValue result
+ // as having aliases to the LHS and RHS (if it isn't just the same LValue
+ // on both sides). We also don't model that the update "may" happen
+ // (a weak update). So, we don't consider the LHS and RHS as being weakly
+ // updated at [[after_diff]].
+ std::string Code = R"(
+ void target(bool Cond, bool B1, bool B2) {
+ (void)0;
+ // [[before_same]]
+ (Cond ? B1 : B1) = !B1;
+ // [[after_same]]
+ (Cond ? B1 : B2) = !B1;
+ // [[after_diff]]
+ }
+ )";
+ runDataflow(
+ Code,
+ [](const llvm::StringMap<DataflowAnalysisState<NoopLattice>> &Results,
+ ASTContext &ASTCtx) {
+ Environment BeforeSameEnv =
+ getEnvironmentAtAnnotation(Results, "before_same").fork();
+ Environment AfterSameEnv =
+ getEnvironmentAtAnnotation(Results, "after_same").fork();
+ Environment AfterDiffEnv =
+ getEnvironmentAtAnnotation(Results, "after_diff").fork();
+
+ auto &BeforeSameB1 =
+ getValueForDecl<BoolValue>(ASTCtx, BeforeSameEnv, "B1");
+ auto &AfterSameB1 =
+ getValueForDecl<BoolValue>(ASTCtx, AfterSameEnv, "B1");
+ auto &AfterDiffB1 =
+ getValueForDecl<BoolValue>(ASTCtx, AfterDiffEnv, "B1");
+
+ EXPECT_NE(&BeforeSameB1, &AfterSameB1);
+ EXPECT_NE(&BeforeSameB1, &AfterDiffB1);
+ // FIXME: The formula for AfterSameB1 should be different from
+ // AfterDiffB1 to reflect that B1 may be updated.
+ EXPECT_EQ(&AfterSameB1, &AfterDiffB1);
+
+ // The value of B1 is definitely different from before_same vs
+ // after_same.
+ const Formula &B1ChangedForSame =
+ AfterSameEnv.arena().makeNot(AfterSameEnv.arena().makeEquals(
+ AfterSameB1.formula(), BeforeSameB1.formula()));
+ EXPECT_TRUE(AfterSameEnv.allows(B1ChangedForSame));
+ EXPECT_TRUE(AfterSameEnv.proves(B1ChangedForSame));
+
+ // FIXME: It should be possible that B1 *may* be updated, so it may be
----------------
bazuzi wrote:
It would more clear to me that only the `allows` expectation needs to change if
this comment were moved to precede that line, after this decl.
https://github.com/llvm/llvm-project/pull/168994
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
