Skip to content

Commit 1a0be19

Browse files
committed
Guards: Support integer ranges.
1 parent 5490cfb commit 1a0be19

File tree

1 file changed

+49
-20
lines changed

1 file changed

+49
-20
lines changed

shared/controlflow/codeql/controlflow/Guards.qll

Lines changed: 49 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -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

Comments
 (0)