================
@@ -315,6 +328,104 @@ static void transferStatusUpdateCall(const
CXXMemberCallExpr *Expr,
State.Env.setValue(locForOk(*ThisLoc), NewVal);
}
+static BoolValue *evaluateStatusEquality(RecordStorageLocation &LhsStatusLoc,
+ RecordStorageLocation &RhsStatusLoc,
+ Environment &Env) {
+ auto &A = Env.arena();
+ // Logically, a Status object is composed of an error code that could take
one
+ // of multiple possible values, including the "ok" value. We track whether a
+ // Status object has an "ok" value and represent this as an `ok` bit.
Equality
+ // of Status objects compares their error codes. Therefore, merely comparing
+ // the `ok` bits isn't sufficient: when two Status objects are assigned
non-ok
+ // error codes the equality of their respective error codes matters. Since we
+ // only track the `ok` bits, we can't make any conclusions about equality
when
+ // we know that two Status objects have non-ok values.
+
+ auto &LhsOkVal = valForOk(LhsStatusLoc, Env);
+ auto &RhsOkVal = valForOk(RhsStatusLoc, Env);
+
+ auto &Res = Env.makeAtomicBoolValue();
+
+ // lhs && rhs => res (a.k.a. !res => !lhs || !rhs)
+ Env.assume(A.makeImplies(A.makeAnd(LhsOkVal.formula(), RhsOkVal.formula()),
+ Res.formula()));
+ // res => (lhs == rhs)
+ Env.assume(A.makeImplies(
+ Res.formula(), A.makeEquals(LhsOkVal.formula(), RhsOkVal.formula())));
+
+ return &Res;
+}
+
+static BoolValue *
+evaluateStatusOrEquality(RecordStorageLocation &LhsStatusOrLoc,
+ RecordStorageLocation &RhsStatusOrLoc,
+ Environment &Env) {
+ auto &A = Env.arena();
+ // Logically, a StatusOr<T> object is composed of two values - a Status and a
+ // value of type T. Equality of StatusOr objects compares both values.
+ // Therefore, merely comparing the `ok` bits of the Status values isn't
+ // sufficient. When two StatusOr objects are engaged, the equality of their
+ // respective values of type T matters. Similarly, when two StatusOr objects
+ // have Status values that have non-ok error codes, the equality of the error
+ // codes matters. Since we only track the `ok` bits of the Status values, we
+ // can't make any conclusions about equality when we know that two StatusOr
+ // objects are engaged or when their Status values contain non-ok error
codes.
+ auto &LhsOkVal = valForOk(locForStatus(LhsStatusOrLoc), Env);
+ auto &RhsOkVal = valForOk(locForStatus(RhsStatusOrLoc), Env);
+ auto &res = Env.makeAtomicBoolValue();
+
+ // res => (lhs == rhs)
+ Env.assume(A.makeImplies(
+ res.formula(), A.makeEquals(LhsOkVal.formula(), RhsOkVal.formula())));
+ return &res;
+}
+
+static BoolValue *evaluateEquality(const Expr *LhsExpr, const Expr *RhsExpr,
+ Environment &Env) {
+ // Check the type of both sides in case an operator== is added that admits
+ // different types.
+ if (isStatusOrType(LhsExpr->getType()) &&
+ isStatusOrType(RhsExpr->getType())) {
+ auto *LhsStatusOrLoc = Env.get<RecordStorageLocation>(*LhsExpr);
+ if (LhsStatusOrLoc == nullptr)
+ return nullptr;
+ auto *RhsStatusOrLoc = Env.get<RecordStorageLocation>(*RhsExpr);
+ if (RhsStatusOrLoc == nullptr)
+ return nullptr;
+
+ return evaluateStatusOrEquality(*LhsStatusOrLoc, *RhsStatusOrLoc, Env);
+
+ // Check the type of both sides in case an operator== is added that admits
----------------
fmayer wrote:
Actually I don't think we need to repeat this, just removing the second one.
https://github.com/llvm/llvm-project/pull/163871
_______________________________________________
llvm-branch-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-branch-commits
