[nullability] Simplify flow conditions produced when comparing against `nullptr`.
When comparing against `nullptr`, instead of adding three implications to the
flow condition, we can leave the flow condition unchanged and simply use the
nullstate of the operand that isn't `nullptr`, potentially with an added
negation.
Comparing against `nullptr` is the overwhelmingly common case, and simpler flow
conditions help in two ways:
- The SAT solver needs to do less work.
- Flow conditions are easier to interpret when debugging.
The tests in test/comparisons.cc already provide coverage for the new case
distinctions introduced here.
PiperOrigin-RevId: 559659135
Change-Id: I37ad7430654646cd31c3bcd4e69e97010496d6e5
diff --git a/nullability/pointer_nullability_analysis.cc b/nullability/pointer_nullability_analysis.cc
index 344df00..28dc665 100644
--- a/nullability/pointer_nullability_analysis.cc
+++ b/nullability/pointer_nullability_analysis.cc
@@ -323,6 +323,36 @@
const BinaryOperator *BinaryOp, const MatchFinder::MatchResult &result,
TransferState<PointerNullabilityLattice> &State) {
auto &A = State.Env.arena();
+
+ auto *LHS = getPointerValueFromExpr(BinaryOp->getLHS(), State.Env);
+ auto *RHS = getPointerValueFromExpr(BinaryOp->getRHS(), State.Env);
+
+ if (!LHS || !RHS) return;
+ if (!hasPointerNullState(*LHS) || !hasPointerNullState(*RHS)) return;
+
+ BoolValue &LHSNullVal = getPointerNullState(*LHS).second;
+ BoolValue &RHSNullVal = getPointerNullState(*RHS).second;
+ auto &LHSNull = LHSNullVal.formula();
+ auto &RHSNull = RHSNullVal.formula();
+
+ // Special case: Are we comparing against `nullptr`?
+ // We can avoid modifying the flow condition in this case and simply propagate
+ // the nullability of the other operand (potentially with a negation).
+ if (&LHSNull == &A.makeLiteral(true)) {
+ if (BinaryOp->getOpcode() == BO_EQ)
+ State.Env.setValue(*BinaryOp, RHSNullVal);
+ else
+ State.Env.setValue(*BinaryOp, State.Env.makeNot(RHSNullVal));
+ return;
+ }
+ if (&RHSNull == &A.makeLiteral(true)) {
+ if (BinaryOp->getOpcode() == BO_EQ)
+ State.Env.setValue(*BinaryOp, LHSNullVal);
+ else
+ State.Env.setValue(*BinaryOp, State.Env.makeNot(LHSNullVal));
+ return;
+ }
+
// Boolean representing the comparison between the two pointer values,
// automatically created by the dataflow framework.
auto &PointerComparison =
@@ -336,25 +366,15 @@
? A.makeNot(PointerComparison)
: PointerComparison;
- auto *LHS = getPointerValueFromExpr(BinaryOp->getLHS(), State.Env);
- auto *RHS = getPointerValueFromExpr(BinaryOp->getRHS(), State.Env);
-
- if (!LHS || !RHS) return;
-
- auto &LHSNull = getPointerNullState(*LHS).second.formula();
- auto &RHSNull = getPointerNullState(*RHS).second.formula();
- auto &LHSNotNull = A.makeNot(LHSNull);
- auto &RHSNotNull = A.makeNot(RHSNull);
-
// nullptr == nullptr
State.Env.addToFlowCondition(
A.makeImplies(A.makeAnd(LHSNull, RHSNull), PointerEQ));
// nullptr != notnull
State.Env.addToFlowCondition(
- A.makeImplies(A.makeAnd(LHSNull, RHSNotNull), PointerNE));
+ A.makeImplies(A.makeAnd(LHSNull, A.makeNot(RHSNull)), PointerNE));
// notnull != nullptr
State.Env.addToFlowCondition(
- A.makeImplies(A.makeAnd(LHSNotNull, RHSNull), PointerNE));
+ A.makeImplies(A.makeAnd(A.makeNot(LHSNull), RHSNull), PointerNE));
}
void transferFlowSensitiveNullCheckImplicitCastPtrToBool(
