1 files changed, 155 insertions, 326 deletions

diff --git a/contrib/llvm-project/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp b/contrib/llvm-project/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp
index b0a8667f3fe5..69ac2c2b82cf 100644
--- a/contrib/llvm-project/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp
+++ b/contrib/llvm-project/clang/lib/Analysis/FlowSensitive/Models/UncheckedOptionalAccessModel.cpp
@@ -34,7 +34,6 @@
 #include <memory>
 #include <optional>
 #include <utility>
-#include <vector>
 
 namespace clang {
 namespace dataflow {
@@ -123,12 +122,6 @@ auto nulloptTypeDecl() {
 
 auto hasNulloptType() { return hasType(nulloptTypeDecl()); }
 
-// `optional` or `nullopt_t`
-auto hasAnyOptionalType() {
-  return hasType(hasUnqualifiedDesugaredType(
-      recordType(hasDeclaration(anyOf(nulloptTypeDecl(), optionalClass())))));
-}
-
 auto inPlaceClass() {
   return recordDecl(hasAnyName("std::in_place_t", "absl::in_place_t",
                                "base::in_place_t", "folly::in_place_t"));
@@ -163,11 +156,6 @@ auto isOptionalValueOrConversionAssignment() {
       argumentCountIs(2), hasArgument(1, unless(hasNulloptType())));
 }
 
-auto isNulloptConstructor() {
-  return cxxConstructExpr(hasNulloptType(), argumentCountIs(1),
-                          hasArgument(0, hasNulloptType()));
-}
-
 auto isOptionalNulloptAssignment() {
   return cxxOperatorCallExpr(hasOverloadedOperatorName("="),
                              callee(cxxMethodDecl(ofClass(optionalClass()))),
@@ -238,47 +226,53 @@ auto isComparisonOperatorCall(L lhs_arg_matcher, R rhs_arg_matcher) {
 
 /// Ensures that `Expr` is mapped to a `BoolValue` and returns its formula.
 const Formula &forceBoolValue(Environment &Env, const Expr &Expr) {
-  auto *Value = cast_or_null<BoolValue>(Env.getValue(Expr, SkipPast::None));
+  auto *Value = cast_or_null<BoolValue>(Env.getValue(Expr));
   if (Value != nullptr)
     return Value->formula();
 
-  auto &Loc = Env.createStorageLocation(Expr);
   Value = &Env.makeAtomicBoolValue();
-  Env.setValue(Loc, *Value);
-  Env.setStorageLocation(Expr, Loc);
+  Env.setValue(Expr, *Value);
   return Value->formula();
 }
 
+StorageLocation &locForHasValue(const RecordStorageLocation &OptionalLoc) {
+  return OptionalLoc.getSyntheticField("has_value");
+}
+
+StorageLocation &locForValue(const RecordStorageLocation &OptionalLoc) {
+  return OptionalLoc.getSyntheticField("value");
+}
+
 /// Sets `HasValueVal` as the symbolic value that represents the "has_value"
-/// property of the optional value `OptionalVal`.
-void setHasValue(Value &OptionalVal, BoolValue &HasValueVal) {
-  OptionalVal.setProperty("has_value", HasValueVal);
+/// property of the optional at `OptionalLoc`.
+void setHasValue(RecordStorageLocation &OptionalLoc, BoolValue &HasValueVal,
+                 Environment &Env) {
+  Env.setValue(locForHasValue(OptionalLoc), HasValueVal);
 }
 
 /// Creates a symbolic value for an `optional` value at an existing storage
 /// location. Uses `HasValueVal` as the symbolic value of the "has_value"
 /// property.
-StructValue &createOptionalValue(AggregateStorageLocation &Loc,
+RecordValue &createOptionalValue(RecordStorageLocation &Loc,
                                  BoolValue &HasValueVal, Environment &Env) {
-  auto &OptionalVal = Env.create<StructValue>(Loc);
+  auto &OptionalVal = Env.create<RecordValue>(Loc);
   Env.setValue(Loc, OptionalVal);
-  setHasValue(OptionalVal, HasValueVal);
+  setHasValue(Loc, HasValueVal, Env);
   return OptionalVal;
 }
 
 /// Returns the symbolic value that represents the "has_value" property of the
-/// optional value `OptionalVal`. Returns null if `OptionalVal` is null.
-BoolValue *getHasValue(Environment &Env, Value *OptionalVal) {
-  if (OptionalVal != nullptr) {
-    auto *HasValueVal =
-        cast_or_null<BoolValue>(OptionalVal->getProperty("has_value"));
-    if (HasValueVal == nullptr) {
-      HasValueVal = &Env.makeAtomicBoolValue();
-      OptionalVal->setProperty("has_value", *HasValueVal);
-    }
-    return HasValueVal;
+/// optional at `OptionalLoc`. Returns null if `OptionalLoc` is null.
+BoolValue *getHasValue(Environment &Env, RecordStorageLocation *OptionalLoc) {
+  if (OptionalLoc == nullptr)
+    return nullptr;
+  StorageLocation &HasValueLoc = locForHasValue(*OptionalLoc);
+  auto *HasValueVal = cast_or_null<BoolValue>(Env.getValue(HasValueLoc));
+  if (HasValueVal == nullptr) {
+    HasValueVal = &Env.makeAtomicBoolValue();
+    Env.setValue(HasValueLoc, *HasValueVal);
   }
-  return nullptr;
+  return HasValueVal;
 }
 
 /// Returns true if and only if `Type` is an optional type.
@@ -305,176 +299,47 @@ int countOptionalWrappers(const ASTContext &ASTCtx, QualType Type) {
                      .getDesugaredType(ASTCtx));
 }
 
-/// Tries to initialize the `optional`'s value (that is, contents), and return
-/// its location. Returns nullptr if the value can't be represented.
-StorageLocation *maybeInitializeOptionalValueMember(QualType Q,
-                                                    Value &OptionalVal,
-                                                    Environment &Env) {
-  // The "value" property represents a synthetic field. As such, it needs
-  // `StorageLocation`, like normal fields (and other variables). So, we model
-  // it with a `PointerValue`, since that includes a storage location.  Once
-  // the property is set, it will be shared by all environments that access the
-  // `Value` representing the optional (here, `OptionalVal`).
-  if (auto *ValueProp = OptionalVal.getProperty("value")) {
-    auto *ValuePtr = clang::cast<PointerValue>(ValueProp);
-    auto &ValueLoc = ValuePtr->getPointeeLoc();
-    if (Env.getValue(ValueLoc) != nullptr)
-      return &ValueLoc;
-
-    // The property was previously set, but the value has been lost. This can
-    // happen in various situations, for example:
-    // - Because of an environment merge (where the two environments mapped the
-    //   property to different values, which resulted in them both being
-    //   discarded).
-    // - When two blocks in the CFG, with neither a dominator of the other,
-    //   visit the same optional value. (FIXME: This is something we can and
-    //   should fix -- see also the lengthy FIXME below.)
-    // - Or even when a block is revisited during testing to collect
-    //   per-statement state.
-    // FIXME: This situation means that the optional contents are not shared
-    // between branches and the like. Practically, this lack of sharing
-    // reduces the precision of the model when the contents are relevant to
-    // the check, like another optional or a boolean that influences control
-    // flow.
-    if (ValueLoc.getType()->isRecordType()) {
-      refreshStructValue(cast<AggregateStorageLocation>(ValueLoc), Env);
-      return &ValueLoc;
-    } else {
-      auto *ValueVal = Env.createValue(ValueLoc.getType());
-      if (ValueVal == nullptr)
-        return nullptr;
-      Env.setValue(ValueLoc, *ValueVal);
-      return &ValueLoc;
-    }
-  }
-
-  auto Ty = Q.getNonReferenceType();
-  auto &ValueLoc = Env.createObject(Ty);
-  auto &ValuePtr = Env.create<PointerValue>(ValueLoc);
-  // FIXME:
-  // The change we make to the `value` property below may become visible to
-  // other blocks that aren't successors of the current block and therefore
-  // don't see the change we made above mapping `ValueLoc` to `ValueVal`. For
-  // example:
-  //
-  //   void target(optional<int> oo, bool b) {
-  //     // `oo` is associated with a `StructValue` here, which we will call
-  //     // `OptionalVal`.
-  //
-  //     // The `has_value` property is set on `OptionalVal` (but not the
-  //     // `value` property yet).
-  //     if (!oo.has_value()) return;
-  //
-  //     if (b) {
-  //       // Let's assume we transfer the `if` branch first.
-  //       //
-  //       // This causes us to call `maybeInitializeOptionalValueMember()`,
-  //       // which causes us to set the `value` property on `OptionalVal`
-  //       // (which had not been set until this point). This `value` property
-  //       // refers to a `PointerValue`, which in turn refers to a
-  //       // StorageLocation` that is associated to an `IntegerValue`.
-  //       oo.value();
-  //     } else {
-  //       // Let's assume we transfer the `else` branch after the `if` branch.
-  //       //
-  //       // We see the `value` property that the `if` branch set on
-  //       // `OptionalVal`, but in the environment for this block, the
-  //       // `StorageLocation` in the `PointerValue` is not associated with any
-  //       // `Value`.
-  //       oo.value();
-  //     }
-  //   }
-  //
-  // This situation is currently "saved" by the code above that checks whether
-  // the `value` property is already set, and if, the `ValueLoc` is not
-  // associated with a `ValueVal`, creates a new `ValueVal`.
-  //
-  // However, what we should really do is to make sure that the change to the
-  // `value` property does not "leak" to other blocks that are not successors
-  // of this block. To do this, instead of simply setting the `value` property
-  // on the existing `OptionalVal`, we should create a new `Value` for the
-  // optional, set the property on that, and associate the storage location that
-  // is currently associated with the existing `OptionalVal` with the newly
-  // created `Value` instead.
-  OptionalVal.setProperty("value", ValuePtr);
-  return &ValueLoc;
-}
-
-void initializeOptionalReference(const Expr *OptionalExpr,
-                                 const MatchFinder::MatchResult &,
-                                 LatticeTransferState &State) {
-  if (auto *OptionalVal =
-          State.Env.getValue(*OptionalExpr, SkipPast::Reference)) {
-    if (OptionalVal->getProperty("has_value") == nullptr) {
-      setHasValue(*OptionalVal, State.Env.makeAtomicBoolValue());
-    }
+StorageLocation *getLocBehindPossiblePointer(const Expr &E,
+                                             const Environment &Env) {
+  if (E.isPRValue()) {
+    if (auto *PointerVal = dyn_cast_or_null<PointerValue>(Env.getValue(E)))
+      return &PointerVal->getPointeeLoc();
+    return nullptr;
   }
-}
-
-/// Returns true if and only if `OptionalVal` is initialized and known to be
-/// empty in `Env`.
-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()));
-}
-
-/// 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());
-}
-
-Value *getValueBehindPossiblePointer(const Expr &E, const Environment &Env) {
-  Value *Val = Env.getValue(E, SkipPast::Reference);
-  if (auto *PointerVal = dyn_cast_or_null<PointerValue>(Val))
-    return Env.getValue(PointerVal->getPointeeLoc());
-  return Val;
+  return Env.getStorageLocation(E);
 }
 
 void transferUnwrapCall(const Expr *UnwrapExpr, const Expr *ObjectExpr,
                         LatticeTransferState &State) {
-  if (auto *OptionalVal =
-          getValueBehindPossiblePointer(*ObjectExpr, State.Env)) {
-    if (State.Env.getStorageLocation(*UnwrapExpr, SkipPast::None) == nullptr)
-      if (auto *Loc = maybeInitializeOptionalValueMember(
-              UnwrapExpr->getType(), *OptionalVal, State.Env))
-        State.Env.setStorageLocation(*UnwrapExpr, *Loc);
+  if (auto *OptionalLoc = cast_or_null<RecordStorageLocation>(
+          getLocBehindPossiblePointer(*ObjectExpr, State.Env))) {
+    if (State.Env.getStorageLocation(*UnwrapExpr) == nullptr)
+      State.Env.setStorageLocation(*UnwrapExpr, locForValue(*OptionalLoc));
   }
 }
 
 void transferArrowOpCall(const Expr *UnwrapExpr, const Expr *ObjectExpr,
                          LatticeTransferState &State) {
-  if (auto *OptionalVal =
-          getValueBehindPossiblePointer(*ObjectExpr, State.Env)) {
-    if (auto *Loc = maybeInitializeOptionalValueMember(
-            UnwrapExpr->getType()->getPointeeType(), *OptionalVal, State.Env)) {
-      State.Env.setValueStrict(*UnwrapExpr,
-                               State.Env.create<PointerValue>(*Loc));
-    }
-  }
+  if (auto *OptionalLoc = cast_or_null<RecordStorageLocation>(
+          getLocBehindPossiblePointer(*ObjectExpr, State.Env)))
+    State.Env.setValue(
+        *UnwrapExpr, State.Env.create<PointerValue>(locForValue(*OptionalLoc)));
 }
 
 void transferMakeOptionalCall(const CallExpr *E,
                               const MatchFinder::MatchResult &,
                               LatticeTransferState &State) {
-  createOptionalValue(State.Env.getResultObjectLocation(*E),
-                      State.Env.getBoolLiteralValue(true), State.Env);
+  State.Env.setValue(
+      *E, createOptionalValue(State.Env.getResultObjectLocation(*E),
+                              State.Env.getBoolLiteralValue(true), State.Env));
 }
 
 void transferOptionalHasValueCall(const CXXMemberCallExpr *CallExpr,
                                   const MatchFinder::MatchResult &,
                                   LatticeTransferState &State) {
   if (auto *HasValueVal = getHasValue(
-          State.Env, getValueBehindPossiblePointer(
-                         *CallExpr->getImplicitObjectArgument(), State.Env))) {
-    auto &CallExprLoc = State.Env.createStorageLocation(*CallExpr);
-    State.Env.setValue(CallExprLoc, *HasValueVal);
-    State.Env.setStorageLocation(*CallExpr, CallExprLoc);
+          State.Env, getImplicitObjectLocation(*CallExpr, State.Env))) {
+    State.Env.setValue(*CallExpr, *HasValueVal);
   }
 }
 
@@ -487,17 +352,16 @@ void transferValueOrImpl(
                                 const Formula &HasValueVal)) {
   auto &Env = State.Env;
 
-  const auto *ObjectArgumentExpr =
-      Result.Nodes.getNodeAs<clang::CXXMemberCallExpr>(ValueOrCallID)
-          ->getImplicitObjectArgument();
+  const auto *MCE =
+      Result.Nodes.getNodeAs<clang::CXXMemberCallExpr>(ValueOrCallID);
 
-  auto *HasValueVal = getHasValue(
-      State.Env, getValueBehindPossiblePointer(*ObjectArgumentExpr, State.Env));
+  auto *HasValueVal =
+      getHasValue(State.Env, getImplicitObjectLocation(*MCE, State.Env));
   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,
@@ -535,24 +399,30 @@ void transferValueOrNotEqX(const Expr *ComparisonExpr,
 void transferCallReturningOptional(const CallExpr *E,
                                    const MatchFinder::MatchResult &Result,
                                    LatticeTransferState &State) {
-  if (State.Env.getStorageLocation(*E, SkipPast::None) != nullptr)
+  if (State.Env.getValue(*E) != nullptr)
     return;
 
-  AggregateStorageLocation *Loc = nullptr;
+  RecordStorageLocation *Loc = nullptr;
   if (E->isPRValue()) {
     Loc = &State.Env.getResultObjectLocation(*E);
   } else {
-    Loc = &cast<AggregateStorageLocation>(State.Env.createStorageLocation(*E));
-    State.Env.setStorageLocationStrict(*E, *Loc);
+    Loc = cast_or_null<RecordStorageLocation>(State.Env.getStorageLocation(*E));
+    if (Loc == nullptr) {
+      Loc = &cast<RecordStorageLocation>(State.Env.createStorageLocation(*E));
+      State.Env.setStorageLocation(*E, *Loc);
+    }
   }
 
-  createOptionalValue(*Loc, State.Env.makeAtomicBoolValue(), State.Env);
+  RecordValue &Val =
+      createOptionalValue(*Loc, State.Env.makeAtomicBoolValue(), State.Env);
+  if (E->isPRValue())
+    State.Env.setValue(*E, Val);
 }
 
 void constructOptionalValue(const Expr &E, Environment &Env,
                             BoolValue &HasValueVal) {
-  AggregateStorageLocation &Loc = Env.getResultObjectLocation(E);
-  Env.setValueStrict(E, createOptionalValue(Loc, HasValueVal, Env));
+  RecordStorageLocation &Loc = Env.getResultObjectLocation(E);
+  Env.setValue(E, createOptionalValue(Loc, HasValueVal, Env));
 }
 
 /// Returns a symbolic value for the "has_value" property of an `optional<T>`
@@ -579,8 +449,9 @@ BoolValue &valueOrConversionHasValue(const FunctionDecl &F, const Expr &E,
 
   // This is a constructor/assignment call for `optional<T>` with argument of
   // type `optional<U>` such that `T` is constructible from `U`.
-  if (auto *HasValueVal =
-          getHasValue(State.Env, State.Env.getValue(E, SkipPast::Reference)))
+  auto *Loc =
+      cast_or_null<RecordStorageLocation>(State.Env.getStorageLocation(E));
+  if (auto *HasValueVal = getHasValue(State.Env, Loc))
     return *HasValueVal;
   return State.Env.makeAtomicBoolValue();
 }
@@ -600,12 +471,12 @@ void transferAssignment(const CXXOperatorCallExpr *E, BoolValue &HasValueVal,
                         LatticeTransferState &State) {
   assert(E->getNumArgs() > 0);
 
-  if (auto *Loc = cast<AggregateStorageLocation>(
-          State.Env.getStorageLocationStrict(*E->getArg(0)))) {
+  if (auto *Loc = cast_or_null<RecordStorageLocation>(
+          State.Env.getStorageLocation(*E->getArg(0)))) {
     createOptionalValue(*Loc, HasValueVal, State.Env);
 
     // Assign a storage location for the whole expression.
-    State.Env.setStorageLocationStrict(*E, *Loc);
+    State.Env.setStorageLocation(*E, *Loc);
   }
 }
 
@@ -625,8 +496,8 @@ void transferNulloptAssignment(const CXXOperatorCallExpr *E,
   transferAssignment(E, State.Env.getBoolLiteralValue(false), State);
 }
 
-void transferSwap(AggregateStorageLocation *Loc1,
-                  AggregateStorageLocation *Loc2, Environment &Env) {
+void transferSwap(RecordStorageLocation *Loc1, RecordStorageLocation *Loc2,
+                  Environment &Env) {
   // We account for cases where one or both of the optionals are not modeled,
   // either lacking associated storage locations, or lacking values associated
   // to such storage locations.
@@ -647,11 +518,11 @@ void transferSwap(AggregateStorageLocation *Loc1,
   // allows for local reasoning about the value. To avoid the above, we would
   // need *lazy* value allocation.
   // FIXME: allocate values lazily, instead of just creating a fresh value.
-  BoolValue *BoolVal1 = getHasValue(Env, Env.getValue(*Loc1));
+  BoolValue *BoolVal1 = getHasValue(Env, Loc1);
   if (BoolVal1 == nullptr)
     BoolVal1 = &Env.makeAtomicBoolValue();
 
-  BoolValue *BoolVal2 = getHasValue(Env, Env.getValue(*Loc2));
+  BoolValue *BoolVal2 = getHasValue(Env, Loc2);
   if (BoolVal2 == nullptr)
     BoolVal2 = &Env.makeAtomicBoolValue();
 
@@ -663,18 +534,18 @@ void transferSwapCall(const CXXMemberCallExpr *E,
                       const MatchFinder::MatchResult &,
                       LatticeTransferState &State) {
   assert(E->getNumArgs() == 1);
-  auto *OtherLoc = cast_or_null<AggregateStorageLocation>(
-      State.Env.getStorageLocationStrict(*E->getArg(0)));
+  auto *OtherLoc = cast_or_null<RecordStorageLocation>(
+      State.Env.getStorageLocation(*E->getArg(0)));
   transferSwap(getImplicitObjectLocation(*E, State.Env), OtherLoc, State.Env);
 }
 
 void transferStdSwapCall(const CallExpr *E, const MatchFinder::MatchResult &,
                          LatticeTransferState &State) {
   assert(E->getNumArgs() == 2);
-  auto *Arg0Loc = cast_or_null<AggregateStorageLocation>(
-      State.Env.getStorageLocationStrict(*E->getArg(0)));
-  auto *Arg1Loc = cast_or_null<AggregateStorageLocation>(
-      State.Env.getStorageLocationStrict(*E->getArg(1)));
+  auto *Arg0Loc = cast_or_null<RecordStorageLocation>(
+      State.Env.getStorageLocation(*E->getArg(0)));
+  auto *Arg1Loc = cast_or_null<RecordStorageLocation>(
+      State.Env.getStorageLocation(*E->getArg(1)));
   transferSwap(Arg0Loc, Arg1Loc, State.Env);
 }
 
@@ -682,8 +553,8 @@ void transferStdForwardCall(const CallExpr *E, const MatchFinder::MatchResult &,
                             LatticeTransferState &State) {
   assert(E->getNumArgs() == 1);
 
-  if (auto *Loc = State.Env.getStorageLocationStrict(*E->getArg(0)))
-    State.Env.setStorageLocationStrict(*E, *Loc);
+  if (auto *Loc = State.Env.getStorageLocation(*E->getArg(0)))
+    State.Env.setStorageLocation(*E, *Loc);
 }
 
 const Formula &evaluateEquality(Arena &A, const Formula &EqVal,
@@ -714,29 +585,46 @@ void transferOptionalAndOptionalCmp(const clang::CXXOperatorCallExpr *CmpExpr,
   Environment &Env = State.Env;
   auto &A = Env.arena();
   auto *CmpValue = &forceBoolValue(Env, *CmpExpr);
-  if (auto *LHasVal = getHasValue(
-          Env, Env.getValue(*CmpExpr->getArg(0), SkipPast::Reference)))
-    if (auto *RHasVal = getHasValue(
-            Env, Env.getValue(*CmpExpr->getArg(1), SkipPast::Reference))) {
+  auto *Arg0Loc = cast_or_null<RecordStorageLocation>(
+      Env.getStorageLocation(*CmpExpr->getArg(0)));
+  if (auto *LHasVal = getHasValue(Env, Arg0Loc)) {
+    auto *Arg1Loc = cast_or_null<RecordStorageLocation>(
+        Env.getStorageLocation(*CmpExpr->getArg(1)));
+    if (auto *RHasVal = getHasValue(Env, Arg1Loc)) {
       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()));
     }
+  }
 }
 
 void transferOptionalAndValueCmp(const clang::CXXOperatorCallExpr *CmpExpr,
                                  const clang::Expr *E, Environment &Env) {
   auto &A = Env.arena();
   auto *CmpValue = &forceBoolValue(Env, *CmpExpr);
-  if (auto *HasVal = getHasValue(Env, Env.getValue(*E, SkipPast::Reference))) {
+  auto *Loc = cast_or_null<RecordStorageLocation>(Env.getStorageLocation(*E));
+  if (auto *HasVal = getHasValue(Env, Loc)) {
     if (CmpExpr->getOperator() == clang::OO_ExclaimEqual)
       CmpValue = &A.makeNot(*CmpValue);
-    Env.addToFlowCondition(
+    Env.assume(
         evaluateEquality(A, *CmpValue, HasVal->formula(), A.makeLiteral(true)));
   }
 }
 
+void transferOptionalAndNulloptCmp(const clang::CXXOperatorCallExpr *CmpExpr,
+                                   const clang::Expr *E, Environment &Env) {
+  auto &A = Env.arena();
+  auto *CmpValue = &forceBoolValue(Env, *CmpExpr);
+  auto *Loc = cast_or_null<RecordStorageLocation>(Env.getStorageLocation(*E));
+  if (auto *HasVal = getHasValue(Env, Loc)) {
+    if (CmpExpr->getOperator() == clang::OO_ExclaimEqual)
+      CmpValue = &A.makeNot(*CmpValue);
+    Env.assume(evaluateEquality(A, *CmpValue, HasVal->formula(),
+                                A.makeLiteral(false)));
+  }
+}
+
 std::optional<StatementMatcher>
 ignorableOptional(const UncheckedOptionalAccessModelOptions &Options) {
   if (Options.IgnoreSmartPointerDereference) {
@@ -766,12 +654,6 @@ auto buildTransferMatchSwitch() {
   // lot of duplicated work (e.g. string comparisons), consider providing APIs
   // that avoid it through memoization.
   return CFGMatchSwitchBuilder<LatticeTransferState>()
-      // Attach a symbolic "has_value" state to optional values that we see for
-      // the first time.
-      .CaseOfCFGStmt<Expr>(
-          expr(anyOf(declRefExpr(), memberExpr()), hasOptionalType()),
-          initializeOptionalReference)
-
       // make_optional
       .CaseOfCFGStmt<CallExpr>(isMakeOptionalCall(), transferMakeOptionalCall)
 
@@ -783,14 +665,6 @@ auto buildTransferMatchSwitch() {
             constructOptionalValue(*E, State.Env,
                                    State.Env.getBoolLiteralValue(true));
           })
-      // nullopt_t::nullopt_t
-      .CaseOfCFGStmt<CXXConstructExpr>(
-          isNulloptConstructor(),
-          [](const CXXConstructExpr *E, const MatchFinder::MatchResult &,
-             LatticeTransferState &State) {
-            constructOptionalValue(*E, State.Env,
-                                   State.Env.getBoolLiteralValue(false));
-          })
       // optional::optional(nullopt_t)
       .CaseOfCFGStmt<CXXConstructExpr>(
           isOptionalNulloptConstructor(),
@@ -852,7 +726,7 @@ auto buildTransferMatchSwitch() {
           isOptionalMemberCallWithNameMatcher(hasName("emplace")),
           [](const CXXMemberCallExpr *E, const MatchFinder::MatchResult &,
              LatticeTransferState &State) {
-            if (AggregateStorageLocation *Loc =
+            if (RecordStorageLocation *Loc =
                     getImplicitObjectLocation(*E, State.Env)) {
               createOptionalValue(*Loc, State.Env.getBoolLiteralValue(true),
                                   State.Env);
@@ -864,7 +738,7 @@ auto buildTransferMatchSwitch() {
           isOptionalMemberCallWithNameMatcher(hasName("reset")),
           [](const CXXMemberCallExpr *E, const MatchFinder::MatchResult &,
              LatticeTransferState &State) {
-            if (AggregateStorageLocation *Loc =
+            if (RecordStorageLocation *Loc =
                     getImplicitObjectLocation(*E, State.Env)) {
               createOptionalValue(*Loc, State.Env.getBoolLiteralValue(false),
                                   State.Env);
@@ -891,18 +765,32 @@ auto buildTransferMatchSwitch() {
 
       // Comparisons (==, !=):
       .CaseOfCFGStmt<CXXOperatorCallExpr>(
-          isComparisonOperatorCall(hasAnyOptionalType(), hasAnyOptionalType()),
+          isComparisonOperatorCall(hasOptionalType(), hasOptionalType()),
           transferOptionalAndOptionalCmp)
       .CaseOfCFGStmt<CXXOperatorCallExpr>(
-          isComparisonOperatorCall(hasOptionalType(),
-                                   unless(hasAnyOptionalType())),
+          isComparisonOperatorCall(hasOptionalType(), hasNulloptType()),
+          [](const clang::CXXOperatorCallExpr *Cmp,
+             const MatchFinder::MatchResult &, LatticeTransferState &State) {
+            transferOptionalAndNulloptCmp(Cmp, Cmp->getArg(0), State.Env);
+          })
+      .CaseOfCFGStmt<CXXOperatorCallExpr>(
+          isComparisonOperatorCall(hasNulloptType(), hasOptionalType()),
+          [](const clang::CXXOperatorCallExpr *Cmp,
+             const MatchFinder::MatchResult &, LatticeTransferState &State) {
+            transferOptionalAndNulloptCmp(Cmp, Cmp->getArg(1), State.Env);
+          })
+      .CaseOfCFGStmt<CXXOperatorCallExpr>(
+          isComparisonOperatorCall(
+              hasOptionalType(),
+              unless(anyOf(hasOptionalType(), hasNulloptType()))),
           [](const clang::CXXOperatorCallExpr *Cmp,
              const MatchFinder::MatchResult &, LatticeTransferState &State) {
             transferOptionalAndValueCmp(Cmp, Cmp->getArg(0), State.Env);
           })
       .CaseOfCFGStmt<CXXOperatorCallExpr>(
-          isComparisonOperatorCall(unless(hasAnyOptionalType()),
-                                   hasOptionalType()),
+          isComparisonOperatorCall(
+              unless(anyOf(hasOptionalType(), hasNulloptType())),
+              hasOptionalType()),
           [](const clang::CXXOperatorCallExpr *Cmp,
              const MatchFinder::MatchResult &, LatticeTransferState &State) {
             transferOptionalAndValueCmp(Cmp, Cmp->getArg(1), State.Env);
@@ -915,12 +803,13 @@ auto buildTransferMatchSwitch() {
       .Build();
 }
 
-std::vector<SourceLocation> diagnoseUnwrapCall(const Expr *ObjectExpr,
-                                               const Environment &Env) {
-  if (auto *OptionalVal = getValueBehindPossiblePointer(*ObjectExpr, Env)) {
-    auto *Prop = OptionalVal->getProperty("has_value");
+llvm::SmallVector<SourceLocation> diagnoseUnwrapCall(const Expr *ObjectExpr,
+                                                     const Environment &Env) {
+  if (auto *OptionalLoc = cast_or_null<RecordStorageLocation>(
+          getLocBehindPossiblePointer(*ObjectExpr, Env))) {
+    auto *Prop = Env.getValue(locForHasValue(*OptionalLoc));
     if (auto *HasValueVal = cast_or_null<BoolValue>(Prop)) {
-      if (Env.flowConditionImplies(HasValueVal->formula()))
+      if (Env.proves(HasValueVal->formula()))
         return {};
     }
   }
@@ -937,7 +826,8 @@ auto buildDiagnoseMatchSwitch(
   // lot of duplicated work (e.g. string comparisons), consider providing APIs
   // that avoid it through memoization.
   auto IgnorableOptional = ignorableOptional(Options);
-  return CFGMatchSwitchBuilder<const Environment, std::vector<SourceLocation>>()
+  return CFGMatchSwitchBuilder<const Environment,
+                               llvm::SmallVector<SourceLocation>>()
       // optional::value
       .CaseOfCFGStmt<CXXMemberCallExpr>(
           valueCall(IgnorableOptional),
@@ -963,9 +853,24 @@ UncheckedOptionalAccessModel::optionalClassDecl() {
   return optionalClass();
 }
 
-UncheckedOptionalAccessModel::UncheckedOptionalAccessModel(ASTContext &Ctx)
+static QualType valueTypeFromOptionalType(QualType OptionalTy) {
+  auto *CTSD =
+      cast<ClassTemplateSpecializationDecl>(OptionalTy->getAsCXXRecordDecl());
+  return CTSD->getTemplateArgs()[0].getAsType();
+}
+
+UncheckedOptionalAccessModel::UncheckedOptionalAccessModel(ASTContext &Ctx,
+                                                           Environment &Env)
     : DataflowAnalysis<UncheckedOptionalAccessModel, NoopLattice>(Ctx),
-      TransferMatchSwitch(buildTransferMatchSwitch()) {}
+      TransferMatchSwitch(buildTransferMatchSwitch()) {
+  Env.getDataflowAnalysisContext().setSyntheticFieldCallback(
+      [&Ctx](QualType Ty) -> llvm::StringMap<QualType> {
+        if (!isOptionalType(Ty))
+          return {};
+        return {{"value", valueTypeFromOptionalType(Ty)},
+                {"has_value", Ctx.BoolTy}};
+      });
+}
 
 void UncheckedOptionalAccessModel::transfer(const CFGElement &Elt,
                                             NoopLattice &L, Environment &Env) {
@@ -973,85 +878,9 @@ void UncheckedOptionalAccessModel::transfer(const CFGElement &Elt,
   TransferMatchSwitch(Elt, getASTContext(), State);
 }
 
-ComparisonResult UncheckedOptionalAccessModel::compare(
-    QualType Type, const Value &Val1, const Environment &Env1,
-    const Value &Val2, const Environment &Env2) {
-  if (!isOptionalType(Type))
-    return ComparisonResult::Unknown;
-  bool MustNonEmpty1 = isNonEmptyOptional(Val1, Env1);
-  bool MustNonEmpty2 = isNonEmptyOptional(Val2, Env2);
-  if (MustNonEmpty1 && MustNonEmpty2)
-    return ComparisonResult::Same;
-  // If exactly one is true, then they're different, no reason to check whether
-  // they're definitely empty.
-  if (MustNonEmpty1 || MustNonEmpty2)
-    return ComparisonResult::Different;
-  // Check if they're both definitely empty.
-  return (isEmptyOptional(Val1, Env1) && isEmptyOptional(Val2, Env2))
-             ? ComparisonResult::Same
-             : ComparisonResult::Different;
-}
-
-bool UncheckedOptionalAccessModel::merge(QualType Type, const Value &Val1,
-                                         const Environment &Env1,
-                                         const Value &Val2,
-                                         const Environment &Env2,
-                                         Value &MergedVal,
-                                         Environment &MergedEnv) {
-  if (!isOptionalType(Type))
-    return true;
-  // FIXME: uses same approach as join for `BoolValues`. Requires non-const
-  // values, though, so will require updating the interface.
-  auto &HasValueVal = MergedEnv.makeAtomicBoolValue();
-  bool MustNonEmpty1 = isNonEmptyOptional(Val1, Env1);
-  bool MustNonEmpty2 = isNonEmptyOptional(Val2, Env2);
-  if (MustNonEmpty1 && MustNonEmpty2)
-    MergedEnv.addToFlowCondition(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()));
-  setHasValue(MergedVal, HasValueVal);
-  return true;
-}
-
-Value *UncheckedOptionalAccessModel::widen(QualType Type, Value &Prev,
-                                           const Environment &PrevEnv,
-                                           Value &Current,
-                                           Environment &CurrentEnv) {
-  switch (compare(Type, Prev, PrevEnv, Current, CurrentEnv)) {
-  case ComparisonResult::Same:
-    return &Prev;
-  case ComparisonResult::Different:
-    if (auto *PrevHasVal =
-            cast_or_null<BoolValue>(Prev.getProperty("has_value"))) {
-      if (isa<TopBoolValue>(PrevHasVal))
-        return &Prev;
-    }
-    if (auto *CurrentHasVal =
-            cast_or_null<BoolValue>(Current.getProperty("has_value"))) {
-      if (isa<TopBoolValue>(CurrentHasVal))
-        return &Current;
-    }
-    return &createOptionalValue(cast<StructValue>(Current).getAggregateLoc(),
-                                CurrentEnv.makeTopBoolValue(), CurrentEnv);
-  case ComparisonResult::Unknown:
-    return nullptr;
-  }
-  llvm_unreachable("all cases covered in switch");
-}
-
 UncheckedOptionalAccessDiagnoser::UncheckedOptionalAccessDiagnoser(
     UncheckedOptionalAccessModelOptions Options)
     : DiagnoseMatchSwitch(buildDiagnoseMatchSwitch(Options)) {}
 
-std::vector<SourceLocation> UncheckedOptionalAccessDiagnoser::diagnose(
-    ASTContext &Ctx, const CFGElement *Elt, const Environment &Env) {
-  return DiagnoseMatchSwitch(*Elt, Ctx, Env);
-}
-
 } // namespace dataflow
 } // namespace clang