@@ -208,6 +208,11 @@ module Make<
208208
209209 private newtype TGuardValue =
210210 TValue ( TAbstractSingleValue val , Boolean isVal ) or
211+ TIntRange ( int bound , Boolean upper ) {
212+ exists ( ConstantExpr c | c .asIntegerValue ( ) + [ - 1 , 0 , 1 ] = bound ) and
213+ bound != 2147483647 and
214+ bound != - 2147483648
215+ } or
211216 TException ( Boolean throws )
212217
213218 private class AbstractSingleValue extends TAbstractSingleValue {
@@ -238,6 +243,15 @@ module Make<
238243 result = TValue ( val , isVal .booleanNot ( ) )
239244 )
240245 or
246+ exists ( int bound , int d , boolean upper |
247+ upper = true and d = 1
248+ or
249+ upper = false and d = - 1
250+ |
251+ this = TIntRange ( bound , pragma [ only_bind_into ] ( upper ) ) and
252+ result = TIntRange ( bound + d , pragma [ only_bind_into ] ( upper .booleanNot ( ) ) )
253+ )
254+ or
241255 exists ( boolean throws |
242256 this = TException ( throws ) and
243257 result = TException ( throws .booleanNot ( ) )
@@ -262,6 +276,14 @@ module Make<
262276 /** Gets the constant that this value represents, if any. */
263277 ConstantValue asConstantValue ( ) { this = TValue ( TValueConstant ( result ) , true ) }
264278
279+ /**
280+ * Holds if this value represents an integer range.
281+ *
282+ * If `upper = true` the range is `(-infinity, bound]`.
283+ * If `upper = false` the range is `[bound, infinity)`.
284+ */
285+ predicate isIntRange ( int bound , boolean upper ) { this = TIntRange ( bound , upper ) }
286+
265287 /** Holds if this value represents throwing an exception. */
266288 predicate isThrowsException ( ) { this = TException ( true ) }
267289
@@ -275,6 +297,12 @@ module Make<
275297 this = TValue ( val , false ) and result = "not " + val .toString ( )
276298 )
277299 or
300+ exists ( int bound |
301+ this = TIntRange ( bound , true ) and result = "Upper bound " + bound .toString ( )
302+ or
303+ this = TIntRange ( bound , false ) and result = "Lower bound " + bound .toString ( )
304+ )
305+ or
278306 exists ( boolean throws | this = TException ( throws ) |
279307 throws = true and result = "exception"
280308 or
@@ -293,6 +321,24 @@ module Make<
293321 b = TValue ( b1 , true ) and
294322 a1 != b1
295323 )
324+ or
325+ exists ( int upperbound , int lowerbound |
326+ a = TIntRange ( upperbound , true ) and b = TIntRange ( lowerbound , false )
327+ or
328+ b = TIntRange ( upperbound , true ) and a = TIntRange ( lowerbound , false )
329+ |
330+ upperbound < lowerbound
331+ )
332+ or
333+ exists ( int bound , boolean upper , int k |
334+ a = TIntRange ( bound , upper ) and b .asIntValue ( ) = k
335+ or
336+ b = TIntRange ( bound , upper ) and a .asIntValue ( ) = k
337+ |
338+ upper = true and bound < k
339+ or
340+ upper = false and bound > k
341+ )
296342 }
297343
298344 private predicate constantHasValue ( ConstantExpr c , GuardValue v ) {
@@ -681,18 +727,6 @@ module Make<
681727 )
682728 }
683729
684- /** Holds if `e` may take the value `k` */
685- private predicate relevantInt ( Expr e , int k ) {
686- e .( ConstantExpr ) .asIntegerValue ( ) = k
687- or
688- relevantInt ( any ( Expr e1 | valueStep ( e1 , e ) ) , k )
689- or
690- exists ( SsaDefinition def |
691- guardReadsSsaVar ( e , def ) and
692- relevantInt ( getAnUltimateDefinition ( def , _) .( SsaWriteDefinition ) .getDefinition ( ) , k )
693- )
694- }
695-
696730 private predicate impliesStep1 ( Guard g1 , GuardValue v1 , Guard g2 , GuardValue v2 ) {
697731 baseImpliesStep ( g1 , v1 , g2 , v2 )
698732 or
@@ -705,14 +739,9 @@ module Make<
705739 not g2 .directlyValueControls ( g1 .getBasicBlock ( ) , v2 )
706740 )
707741 or
708- exists ( int k1 , int k2 , boolean upper |
709- rangeGuard ( g1 , v1 , g2 , k1 , upper ) and
710- relevantInt ( g2 , k2 ) and
711- v2 = TValue ( TValueInt ( k2 ) , false )
712- |
713- upper = true and k1 < k2 // g2 <= k1 < k2 ==> g2 != k2
714- or
715- upper = false and k1 > k2 // g2 >= k1 > k2 ==> g2 != k2
742+ exists ( int k , boolean upper |
743+ rangeGuard ( g1 , v1 , g2 , k , upper ) and
744+ v2 = TIntRange ( k , upper )
716745 )
717746 or
718747 exists ( boolean isNull |
0 commit comments