@@ -2180,29 +2180,56 @@ func (ft *factsTable) detectSubRelations(v *Value) {
21802180
21812181 // Check if we might wrap around. If so, give up.
21822182 width := uint (v .Type .Size ()) * 8
2183- if _ , ok := safeSub (xLim .min , yLim .max , width ); ! ok {
2184- return // x-y might underflow
2185- }
2186- if _ , ok := safeSub (xLim .max , yLim .min , width ); ! ok {
2187- return // x-y might overflow
2183+
2184+ // v >= 1 in the signed domain?
2185+ var vSignedMinOne bool
2186+
2187+ // Signed optimizations
2188+ if _ , ok := safeSub (xLim .min , yLim .max , width ); ok {
2189+ // Large abs negative y can also overflow
2190+ if _ , ok := safeSub (xLim .max , yLim .min , width ); ok {
2191+ // x-y won't overflow
2192+
2193+ // Subtracting a positive non-zero number only makes
2194+ // things smaller. If it's positive or zero, it might
2195+ // also do nothing (x-0 == v).
2196+ if yLim .min > 0 {
2197+ ft .update (v .Block , v , x , signed , lt )
2198+ } else if yLim .min == 0 {
2199+ ft .update (v .Block , v , x , signed , lt | eq )
2200+ }
2201+
2202+ // Subtracting a number from a bigger one
2203+ // can't go below 1. If the numbers might be
2204+ // equal, then it can't go below 0.
2205+ //
2206+ // This requires the overflow checks because
2207+ // large negative y can cause an overflow.
2208+ if ft .orderS .Ordered (y , x ) {
2209+ ft .signedMin (v , 1 )
2210+ vSignedMinOne = true
2211+ } else if ft .orderS .OrderedOrEqual (y , x ) {
2212+ ft .setNonNegative (v )
2213+ }
2214+ }
21882215 }
21892216
2190- // Subtracting a positive non-zero number only makes
2191- // things smaller. If it's positive or zero, it might
2192- // also do nothing (x-0 == v).
2193- if yLim . min > 0 {
2194- ft . update ( v . Block , v , x , signed , lt )
2195- } else if yLim . min == 0 {
2196- ft . update ( v . Block , v , x , signed , lt | eq )
2217+ // Unsigned optimizations
2218+ if _ , ok := safeSubU ( xLim . umin , yLim . umax , width ); ok {
2219+ if yLim . umin > 0 {
2220+ ft . update ( v . Block , v , x , unsigned , lt )
2221+ } else {
2222+ ft . update ( v . Block , v , x , unsigned , lt | eq )
2223+ }
21972224 }
21982225
2199- // Subtracting a number from a bigger one
2200- // can't go below 1. If the numbers might be
2201- // equal, then it can't go below 0.
2202- if ft . orderS . Ordered ( y , x ) {
2203- ft . signedMin ( v , 1 )
2204- } else if ft .orderS . OrderedOrEqual (y , x ) {
2205- ft .setNonNegative ( v )
2226+ // Proving v >= 1 in the signed domain automatically
2227+ // proves it in the unsigned domain, so we can skip it.
2228+ //
2229+ // We don't need overflow checks here, since if y < x,
2230+ // then x-y can never overflow for uint.
2231+ if ! vSignedMinOne && ft .orderU . Ordered (y , x ) {
2232+ ft .unsignedMin ( v , 1 )
22062233 }
22072234}
22082235
0 commit comments