hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-05-26 09:01:22 +02:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #21876 from hvitved/dense-rank-short-circuit

Browse Source 
Util: Short-circuit `rank` usage in dense ranking library
This commit is contained in:
Tom Hvitved
2026-05-22 16:08:45 +02:00
committed by GitHub
parent 3c4e22a8ba 6d6e9c0d47
commit 688695cd57
1 changed files with 73 additions and 9 deletions
Download Patch File Download Diff File Expand all files Collapse all files

82
shared/util/codeql/util/DenseRank.qll
View File

@@ -55,13 +55,33 @@ signature module DenseRankInputSig {
module DenseRank<DenseRankInputSig Input> {
private import Input
private int getARank() { result = getRank(_) }
pragma[noinline]
private int getARankGap() { result = getARank() and not result - 1 = getARank() }
pragma[noinline]
private predicate isDenseFrom(int i) { i = unique( | | getARankGap()) }
pragma[noinline]
private int getRankNeedsDenseRank(Ranked r) { result = getRank(r) and not isDenseFrom(_) }
private int rankRank(Ranked r, int rnk) {
rnk = getRank(r) and
rnk = rank[result](int rnk0 | rnk0 = getRank(_) | rnk0)
rnk = getRankNeedsDenseRank(r) and
rnk = rank[result](int rnk0 | rnk0 = getRankNeedsDenseRank(_) | rnk0)
}
/** Gets the `Ranked` value for which the dense rank is `rnk`. */
Ranked denseRank(int rnk) { rnk = rankRank(result, getRank(result)) }
pragma[nomagic]
Ranked denseRank(int rnk) {
rnk = rankRank(result, getRankNeedsDenseRank(result))
or
exists(int i, int offset |
isDenseFrom(i) and
offset = i - 1 and
rnk = getRank(result) - offset
)
}
}
/** Provides the input to `DenseRank1`. */
@@ -82,16 +102,38 @@ signature module DenseRankInputSig1 {
module DenseRank1<DenseRankInputSig1 Input> {
private import Input
private int getARank(C c) { result = getRank(c, _) }
pragma[noinline]
private int getARankGap(C c) { result = getARank(c) and not result - 1 = getARank(c) }
pragma[noinline]
private predicate isDenseFrom(C c, int i) { i = unique( | | getARankGap(c)) }
pragma[noinline]
private int getRankNeedsDenseRank(C c, Ranked r) {
result = getRank(c, r) and not isDenseFrom(c, _)
}
private int rankRank(C c, Ranked r, int rnk) {
rnk = getRank(c, r) and
rnk = rank[result](int rnk0 | rnk0 = getRank(c, _) | rnk0)
rnk = getRankNeedsDenseRank(c, r) and
rnk = rank[result](int rnk0 | rnk0 = getRankNeedsDenseRank(c, _) | rnk0)
}
/**
* Gets the `Ranked` value for which the dense rank in the context provided by
* `c` is `rnk`.
*/
Ranked denseRank(C c, int rnk) { rnk = rankRank(c, result, getRank(c, result)) }
pragma[nomagic]
Ranked denseRank(C c, int rnk) {
rnk = rankRank(c, result, getRankNeedsDenseRank(c, result))
or
exists(int i, int offset |
isDenseFrom(c, i) and
offset = i - 1 and
rnk = getRank(c, result) - offset
)
}
}
/** Provides the input to `DenseRank2`. */
@@ -116,16 +158,38 @@ signature module DenseRankInputSig2 {
module DenseRank2<DenseRankInputSig2 Input> {
private import Input
private int getARank(C1 c1, C2 c2) { result = getRank(c1, c2, _) }
pragma[noinline]
private int getARankGap(C1 c1, C2 c2) {
result = getARank(c1, c2) and not result - 1 = getARank(c1, c2)
}
pragma[noinline]
private predicate isDenseFrom(C1 c1, C2 c2, int i) { i = unique( | | getARankGap(c1, c2)) }
pragma[noinline]
private int getRankNeedsDenseRank(C1 c1, C2 c2, Ranked r) {
result = getRank(c1, c2, r) and not isDenseFrom(c1, c2, _)
}
private int rankRank(C1 c1, C2 c2, Ranked r, int rnk) {
rnk = getRank(c1, c2, r) and
rnk = rank[result](int rnk0 | rnk0 = getRank(c1, c2, _) | rnk0)
rnk = getRankNeedsDenseRank(c1, c2, r) and
rnk = rank[result](int rnk0 | rnk0 = getRankNeedsDenseRank(c1, c2, _) | rnk0)
}
/**
* Gets the `Ranked` value for which the dense rank in the context provided by
* `c1` and `c2` is `rnk`.
*/
pragma[nomagic]
Ranked denseRank(C1 c1, C2 c2, int rnk) {
rnk = rankRank(c1, c2, result, getRank(c1, c2, result))
rnk = rankRank(c1, c2, result, getRankNeedsDenseRank(c1, c2, result))
or
exists(int i, int offset |
isDenseFrom(c1, c2, i) and
offset = i - 1 and
rnk = getRank(c1, c2, result) - offset
)
}
}