[clang][nullability] Use proves() and assume() instead of depreca…

…ted synonyms. (#70297)
llvm · Oct 30, 2023 · 526c9b7 · 526c9b7
1 parent da28c33
commit 526c9b7
Show file tree

Hide file tree

Showing 8 changed files with 149 additions and 161 deletions.
diff --git a/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp b/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
@@ -114,11 +114,10 @@ class ModelDumper {
     // guaranteed true/false here is valuable and hard to determine by hand.
     if (auto *B = llvm::dyn_cast<BoolValue>(&V)) {
       JOS.attribute("formula", llvm::to_string(B->formula()));
-      JOS.attribute(
-          "truth", Env.flowConditionImplies(B->formula()) ? "true"
-                   : Env.flowConditionImplies(Env.arena().makeNot(B->formula()))
-                       ? "false"
-                       : "unknown");
+      JOS.attribute("truth", Env.proves(B->formula()) ? "true"
+                             : Env.proves(Env.arena().makeNot(B->formula()))
+                                 ? "false"
+                                 : "unknown");
     }
   }
   void dump(const StorageLocation &L) {

diff --git a/clang/lib/Analysis/FlowSensitive/Models/ChromiumCheckModel.cpp b/clang/lib/Analysis/FlowSensitive/Models/ChromiumCheckModel.cpp
@@ -59,7 +59,7 @@ bool ChromiumCheckModel::transfer(const CFGElement &Element, Environment &Env) {
     if (const auto *M = dyn_cast<CXXMethodDecl>(Call->getDirectCallee())) {
       if (isCheckLikeMethod(CheckDecls, *M)) {
         // Mark this branch as unreachable.
-        Env.addToFlowCondition(Env.arena().makeLiteral(false));
+        Env.assume(Env.arena().makeLiteral(false));
         return true;
       }
     }

diff --git a/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp b/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp
@@ -413,16 +413,15 @@ bool isEmptyOptional(const Value &OptionalVal, const Environment &Env) {
   auto *HasValueVal =
       cast_or_null<BoolValue>(OptionalVal.getProperty("has_value"));
   return HasValueVal != nullptr &&
-         Env.flowConditionImplies(Env.arena().makeNot(HasValueVal->formula()));
+         Env.proves(Env.arena().makeNot(HasValueVal->formula()));
 }
 
 /// Returns true if and only if `OptionalVal` is initialized and known to be
 /// non-empty in `Env`.
 bool isNonEmptyOptional(const Value &OptionalVal, const Environment &Env) {
   auto *HasValueVal =
       cast_or_null<BoolValue>(OptionalVal.getProperty("has_value"));
-  return HasValueVal != nullptr &&
-         Env.flowConditionImplies(HasValueVal->formula());
+  return HasValueVal != nullptr && Env.proves(HasValueVal->formula());
 }
 
 Value *getValueBehindPossiblePointer(const Expr &E, const Environment &Env) {
@@ -490,8 +489,8 @@ void transferValueOrImpl(
   if (HasValueVal == nullptr)
     return;
 
-  Env.addToFlowCondition(ModelPred(Env, forceBoolValue(Env, *ValueOrPredExpr),
-                                   HasValueVal->formula()));
+  Env.assume(ModelPred(Env, forceBoolValue(Env, *ValueOrPredExpr),
+                       HasValueVal->formula()));
 }
 
 void transferValueOrStringEmptyCall(const clang::Expr *ComparisonExpr,
@@ -717,8 +716,8 @@ void transferOptionalAndOptionalCmp(const clang::CXXOperatorCallExpr *CmpExpr,
     if (auto *RHasVal = getHasValue(Env, Env.getValue(*CmpExpr->getArg(1)))) {
       if (CmpExpr->getOperator() == clang::OO_ExclaimEqual)
         CmpValue = &A.makeNot(*CmpValue);
-      Env.addToFlowCondition(evaluateEquality(A, *CmpValue, LHasVal->formula(),
-                                              RHasVal->formula()));
+      Env.assume(evaluateEquality(A, *CmpValue, LHasVal->formula(),
+                                  RHasVal->formula()));
     }
 }
 
@@ -729,7 +728,7 @@ void transferOptionalAndValueCmp(const clang::CXXOperatorCallExpr *CmpExpr,
   if (auto *HasVal = getHasValue(Env, Env.getValue(*E))) {
     if (CmpExpr->getOperator() == clang::OO_ExclaimEqual)
       CmpValue = &A.makeNot(*CmpValue);
-    Env.addToFlowCondition(
+    Env.assume(
         evaluateEquality(A, *CmpValue, HasVal->formula(), A.makeLiteral(true)));
   }
 }
@@ -917,7 +916,7 @@ llvm::SmallVector<SourceLocation> diagnoseUnwrapCall(const Expr *ObjectExpr,
   if (auto *OptionalVal = getValueBehindPossiblePointer(*ObjectExpr, Env)) {
     auto *Prop = OptionalVal->getProperty("has_value");
     if (auto *HasValueVal = cast_or_null<BoolValue>(Prop)) {
-      if (Env.flowConditionImplies(HasValueVal->formula()))
+      if (Env.proves(HasValueVal->formula()))
         return {};
     }
   }
@@ -1004,14 +1003,13 @@ bool UncheckedOptionalAccessModel::merge(QualType Type, const Value &Val1,
   bool MustNonEmpty1 = isNonEmptyOptional(Val1, Env1);
   bool MustNonEmpty2 = isNonEmptyOptional(Val2, Env2);
   if (MustNonEmpty1 && MustNonEmpty2)
-    MergedEnv.addToFlowCondition(HasValueVal.formula());
+    MergedEnv.assume(HasValueVal.formula());
   else if (
       // Only make the costly calls to `isEmptyOptional` if we got "unknown"
       // (false) for both calls to `isNonEmptyOptional`.
       !MustNonEmpty1 && !MustNonEmpty2 && isEmptyOptional(Val1, Env1) &&
       isEmptyOptional(Val2, Env2))
-    MergedEnv.addToFlowCondition(
-        MergedEnv.arena().makeNot(HasValueVal.formula()));
+    MergedEnv.assume(MergedEnv.arena().makeNot(HasValueVal.formula()));
   setHasValue(MergedVal, HasValueVal);
   return true;
 }

diff --git a/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp b/clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
@@ -148,7 +148,7 @@ class TerminatorVisitor
       ConditionValue = false;
     }
 
-    Env.addToFlowCondition(Val->formula());
+    Env.assume(Val->formula());
     return {&Cond, ConditionValue};
   }
 

diff --git a/clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp b/clang/unittests/Analysis/FlowSensitive/ChromiumCheckModelTest.cpp
@@ -159,7 +159,7 @@ TEST(ChromiumCheckModelTest, CheckSuccessImpliesConditionHolds) {
 
         auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl));
 
-        EXPECT_TRUE(Env.flowConditionImplies(FooVal->formula()));
+        EXPECT_TRUE(Env.proves(FooVal->formula()));
       };
 
   std::string Code = R"(
@@ -190,7 +190,7 @@ TEST(ChromiumCheckModelTest, UnrelatedCheckIgnored) {
 
         auto *FooVal = cast<BoolValue>(Env.getValue(*FooDecl));
 
-        EXPECT_FALSE(Env.flowConditionImplies(FooVal->formula()));
+        EXPECT_FALSE(Env.proves(FooVal->formula()));
       };
 
   std::string Code = R"(

diff --git a/clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp b/clang/unittests/Analysis/FlowSensitive/SignAnalysisTest.cpp
@@ -157,44 +157,44 @@ void transferBinary(const BinaryOperator *BO, const MatchFinder::MatchResult &M,
   switch (BO->getOpcode()) {
   case BO_GT:
     // pos > pos
-    State.Env.addToFlowCondition(
+    State.Env.assume(
         A.makeImplies(*Comp, A.makeImplies(RHSProps.Pos->formula(),
                                            LHSProps.Pos->formula())));
     // pos > zero
-    State.Env.addToFlowCondition(
+    State.Env.assume(
         A.makeImplies(*Comp, A.makeImplies(RHSProps.Zero->formula(),
                                            LHSProps.Pos->formula())));
     break;
   case BO_LT:
     // neg < neg
-    State.Env.addToFlowCondition(
+    State.Env.assume(
         A.makeImplies(*Comp, A.makeImplies(RHSProps.Neg->formula(),
                                            LHSProps.Neg->formula())));
     // neg < zero
-    State.Env.addToFlowCondition(
+    State.Env.assume(
         A.makeImplies(*Comp, A.makeImplies(RHSProps.Zero->formula(),
                                            LHSProps.Neg->formula())));
     break;
   case BO_GE:
     // pos >= pos
-    State.Env.addToFlowCondition(
+    State.Env.assume(
         A.makeImplies(*Comp, A.makeImplies(RHSProps.Pos->formula(),
                                            LHSProps.Pos->formula())));
     break;
   case BO_LE:
     // neg <= neg
-    State.Env.addToFlowCondition(
+    State.Env.assume(
         A.makeImplies(*Comp, A.makeImplies(RHSProps.Neg->formula(),
                                            LHSProps.Neg->formula())));
     break;
   case BO_EQ:
-    State.Env.addToFlowCondition(
+    State.Env.assume(
         A.makeImplies(*Comp, A.makeImplies(RHSProps.Neg->formula(),
                                            LHSProps.Neg->formula())));
-    State.Env.addToFlowCondition(
+    State.Env.assume(
         A.makeImplies(*Comp, A.makeImplies(RHSProps.Zero->formula(),
                                            LHSProps.Zero->formula())));
-    State.Env.addToFlowCondition(
+    State.Env.assume(
         A.makeImplies(*Comp, A.makeImplies(RHSProps.Pos->formula(),
                                            LHSProps.Pos->formula())));
     break;
@@ -215,14 +215,14 @@ void transferUnaryMinus(const UnaryOperator *UO,
     return;
 
   // a is pos ==> -a is neg
-  State.Env.addToFlowCondition(
+  State.Env.assume(
       A.makeImplies(OperandProps.Pos->formula(), UnaryOpProps.Neg->formula()));
   // a is neg ==> -a is pos
-  State.Env.addToFlowCondition(
+  State.Env.assume(
       A.makeImplies(OperandProps.Neg->formula(), UnaryOpProps.Pos->formula()));
   // a is zero ==> -a is zero
-  State.Env.addToFlowCondition(A.makeImplies(OperandProps.Zero->formula(),
-                                             UnaryOpProps.Zero->formula()));
+  State.Env.assume(A.makeImplies(OperandProps.Zero->formula(),
+                                 UnaryOpProps.Zero->formula()));
 }
 
 void transferUnaryNot(const UnaryOperator *UO,
@@ -235,19 +235,19 @@ void transferUnaryNot(const UnaryOperator *UO,
     return;
 
   // a is neg or pos ==> !a is zero
-  State.Env.addToFlowCondition(A.makeImplies(
+  State.Env.assume(A.makeImplies(
       A.makeOr(OperandProps.Pos->formula(), OperandProps.Neg->formula()),
       UnaryOpProps.Zero->formula()));
 
   // FIXME Handle this logic universally, not just for unary not. But Where to
   // put the generic handler, transferExpr maybe?
   if (auto *UOBoolVal = dyn_cast<BoolValue>(UnaryOpValue)) {
     // !a <==> a is zero
-    State.Env.addToFlowCondition(
+    State.Env.assume(
         A.makeEquals(UOBoolVal->formula(), OperandProps.Zero->formula()));
     // !a <==> !a is not zero
-    State.Env.addToFlowCondition(A.makeEquals(
-        UOBoolVal->formula(), A.makeNot(UnaryOpProps.Zero->formula())));
+    State.Env.assume(A.makeEquals(UOBoolVal->formula(),
+                                  A.makeNot(UnaryOpProps.Zero->formula())));
   }
 }
 
@@ -391,11 +391,10 @@ BoolValue &mergeBoolValues(BoolValue &Bool1, const Environment &Env1,
   // path taken - this simplifies the flow condition tracked in `MergedEnv`.
   // Otherwise, information about which path was taken is used to associate
   // `MergedBool` with `Bool1` and `Bool2`.
-  if (Env1.flowConditionImplies(B1) && Env2.flowConditionImplies(B2)) {
-    MergedEnv.addToFlowCondition(MergedBool.formula());
-  } else if (Env1.flowConditionImplies(A.makeNot(B1)) &&
-             Env2.flowConditionImplies(A.makeNot(B2))) {
-    MergedEnv.addToFlowCondition(A.makeNot(MergedBool.formula()));
+  if (Env1.proves(B1) && Env2.proves(B2)) {
+    MergedEnv.assume(MergedBool.formula());
+  } else if (Env1.proves(A.makeNot(B1)) && Env2.proves(A.makeNot(B2))) {
+    MergedEnv.assume(A.makeNot(MergedBool.formula()));
   }
   return MergedBool;
 }
@@ -484,7 +483,7 @@ testing::AssertionResult isPropertyImplied(const Environment &Env,
   if (!Prop)
     return Result;
   auto *BVProp = cast<BoolValue>(Prop);
-  if (Env.flowConditionImplies(BVProp->formula()) != Implies)
+  if (Env.proves(BVProp->formula()) != Implies)
     return testing::AssertionFailure()
            << Property << " is " << (Implies ? "not" : "") << " implied"
            << ", but should " << (Implies ? "" : "not ") << "be";