Make flow condition implications regardless of is_known properties. Whether a type was annotated to be null/nonnull or not, if we have compared it to nullptr, we can use that information in the flow conditions of the affected blocks. The is_known property doesn't make the comparison less valid. PiperOrigin-RevId: 539115610
diff --git a/nullability/formal_methods/gradual_nullability_code_synthesis.smt2 b/nullability/formal_methods/gradual_nullability_code_synthesis.smt2 index 0c2544b..b0366d8 100644 --- a/nullability/formal_methods/gradual_nullability_code_synthesis.smt2 +++ b/nullability/formal_methods/gradual_nullability_code_synthesis.smt2
@@ -63,6 +63,8 @@ (declare-fun fc-conj--ptr-is-unknown (PointerValue) Bool) (declare-fun fc-conj--ptr-is-nonnull (PointerValue) Bool) (declare-fun fc-conj--ptr-is-nullable (PointerValue) Bool) +(declare-fun fc-conj--ptr-is-maybe-unknown-but-nonnull (PointerValue) Bool) +(declare-fun fc-conj--ptr-is-maybe-unknown-but-null (PointerValue) Bool) ;; Flow condition conjunct that constrains the result of comparing two ;; pointers for equality. @@ -116,19 +118,33 @@ (= p (make-PointerValue true true))))))) (assert (=> enable-solution-s1 + (forall ((p PointerValue)) + (= (fc-conj--ptr-is-maybe-unknown-but-nonnull p) + (or + (= p (make-PointerValue true true)) + (= p (make-PointerValue false true))))))) + +(assert (=> enable-solution-s1 + (forall ((p PointerValue)) + (= (fc-conj--ptr-is-maybe-unknown-but-null p) + (or + (= p (make-PointerValue true false)) + (= p (make-PointerValue false false))))))) + +(assert (=> enable-solution-s1 (forall ((lhs PointerValue) (rhs PointerValue) (eq Bool)) (= (fc-conj--ptrs-were-compared lhs rhs eq) (and ;; nullptr == nullptr - (=> (and (fc-conj--ptr-is-null lhs) (fc-conj--ptr-is-null rhs)) + (=> (and (fc-conj--ptr-is-maybe-unknown-but-null lhs) (fc-conj--ptr-is-maybe-unknown-but-null rhs)) eq) ;; nullptr != nonnull - (=> (and (fc-conj--ptr-is-null lhs) (fc-conj--ptr-is-nonnull rhs)) + (=> (and (fc-conj--ptr-is-maybe-unknown-but-null lhs) (fc-conj--ptr-is-maybe-unknown-but-nonnull rhs)) (not eq)) ;; nonnull != nullptr - (=> (and (fc-conj--ptr-is-nonnull lhs) (fc-conj--ptr-is-null rhs)) + (=> (and (fc-conj--ptr-is-maybe-unknown-but-nonnull lhs) (fc-conj--ptr-is-maybe-unknown-but-null rhs)) (not eq))))))) (assert (=> enable-solution-s1 @@ -219,26 +235,13 @@ ;; Transitivity for fc-conj--ptrs-were-compared. (assert - (=> - ;; Transitivity does not hold in S1. - ;; Consider (nonnull == unknown), (unknown == null). - ;; However (nonnull == null) never holds. - ;; ``` - ;; void target(int * _NonNull x, int *y) { - ;; if (x == y && y == nullptr) { - ;; // dead code that we can't detect - ;; } - ;; } - ;; ``` - ;; TODO: How big of a problem is it? - (not enable-solution-s1) - (forall ((p1 PointerValue) (p2 PointerValue) (p3 PointerValue)) - (=> (and (is-valid-pointer p1) - (is-valid-pointer p2) - (is-valid-pointer p3) - (fc-conj--ptrs-were-compared p1 p2 true) - (fc-conj--ptrs-were-compared p2 p3 true)) - (fc-conj--ptrs-were-compared p1 p3 true))))) + (forall ((p1 PointerValue) (p2 PointerValue) (p3 PointerValue)) + (=> (and (is-valid-pointer p1) + (is-valid-pointer p2) + (is-valid-pointer p3) + (fc-conj--ptrs-were-compared p1 p2 true) + (fc-conj--ptrs-were-compared p2 p3 true)) + (fc-conj--ptrs-were-compared p1 p3 true)))) ;; Symmetry for fc-conj--join-ptr with regards to pointers. (assert
diff --git a/nullability/pointer_nullability_analysis.cc b/nullability/pointer_nullability_analysis.cc index a2f9690..4343199 100644 --- a/nullability/pointer_nullability_analysis.cc +++ b/nullability/pointer_nullability_analysis.cc
@@ -297,24 +297,20 @@ if (!LHS || !RHS) return; - auto [LHSKnown, LHSNull] = getPointerNullState(*LHS); - auto [RHSKnown, RHSNull] = getPointerNullState(*RHS); - auto& LHSKnownNotNull = - State.Env.makeAnd(LHSKnown, State.Env.makeNot(LHSNull)); - auto& RHSKnownNotNull = - State.Env.makeAnd(RHSKnown, State.Env.makeNot(RHSNull)); - auto& LHSKnownNull = State.Env.makeAnd(LHSKnown, LHSNull); - auto& RHSKnownNull = State.Env.makeAnd(RHSKnown, RHSNull); + auto& LHSNull = getPointerNullState(*LHS).second; + auto& RHSNull = getPointerNullState(*RHS).second; + auto& LHSNotNull = State.Env.makeNot(LHSNull); + auto& RHSNotNull = State.Env.makeNot(RHSNull); // nullptr == nullptr State.Env.addToFlowCondition(State.Env.makeImplication( - State.Env.makeAnd(LHSKnownNull, RHSKnownNull), PointerEQ)); + State.Env.makeAnd(LHSNull, RHSNull), PointerEQ)); // nullptr != notnull State.Env.addToFlowCondition(State.Env.makeImplication( - State.Env.makeAnd(LHSKnownNull, RHSKnownNotNull), PointerNE)); + State.Env.makeAnd(LHSNull, RHSNotNull), PointerNE)); // notnull != nullptr State.Env.addToFlowCondition(State.Env.makeImplication( - State.Env.makeAnd(LHSKnownNotNull, RHSKnownNull), PointerNE)); + State.Env.makeAnd(LHSNotNull, RHSNull), PointerNE)); } void transferFlowSensitiveNullCheckImplicitCastPtrToBool(
diff --git a/nullability/test/comparisons.cc b/nullability/test/comparisons.cc index ee60aca..f881513 100644 --- a/nullability/test/comparisons.cc +++ b/nullability/test/comparisons.cc
@@ -283,7 +283,7 @@ if (x == nullptr) { unknown(x); // TODO: nullable } else { - unknown(x); // TODO: nonnull + nonnull(x); } unknown(x); // TODO: nullable } @@ -292,14 +292,14 @@ if (nullptr == x) { unknown(x); // TODO: nullable } else { - unknown(x); // TODO: nonnull + nonnull(x); } unknown(x); // TODO: nullable } TEST void unknownNotEqualsNullptr(int* x) { unknown(x); // TODO: nullable if (x != nullptr) { - unknown(x); // TODO: nonnull + nonnull(x); } else { unknown(x); // TODO: nullable } @@ -308,7 +308,7 @@ TEST void nullptrNotEqualsUnknown(int* x) { unknown(x); // TODO: nullable if (nullptr != x) { - unknown(x); // TODO: nonnull + nonnull(x); } else { unknown(x); // TODO: nullable } @@ -320,7 +320,7 @@ unknown(x); nonnull(y); if (x == y) { - unknown(x); // TODO: nonnull + nonnull(x); nonnull(y); } else { unknown(x); @@ -333,7 +333,7 @@ unknown(x); nonnull(y); if (y == x) { - unknown(x); // TODO: nonnull + nonnull(x); nonnull(y); } else { unknown(x); @@ -349,7 +349,7 @@ unknown(x); nonnull(y); } else { - unknown(x); // TODO: nonnull + nonnull(x); nonnull(y); } unknown(x); @@ -362,7 +362,7 @@ unknown(x); nonnull(y); } else { - unknown(x); // TODO: nonnull + nonnull(x); nonnull(y); } unknown(x);