Skip to content
Draft
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
82 changes: 73 additions & 9 deletions shared/util/codeql/util/DenseRank.qll
Original file line number Diff line number Diff line change
Expand Up @@ -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`. */
Expand All @@ -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`. */
Expand All @@ -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
)
}
}
Loading