Commit 6a7bcd3
Lines changed: 23 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
@@ -4,6 +4,12 @@ | |||
| 4 | 4 | * variable), and `v` is an integer in the range `[0 .. m-1]`. | |
| 5 | 5 | */ | |
| 6 | 6 | ||
| 7 | + /* | ||
| 8 | + * The main recursion has base cases in both `ssaModulus` (for guarded reads) and `semExprModulus` | ||
| 9 | + * (for constant values). The most interesting recursive case is `phiModulusRankStep`, which | ||
| 10 | + * handles phi inputs. | ||
| 11 | + */ | ||
| 12 | + | ||
| 7 | 13 | private import ModulusAnalysisSpecific::Private | |
| 8 | 14 | private import experimental.semmle.code.cpp.semantic.Semantic | |
| 9 | 15 | private import ConstantAnalysis | |
@@ -162,20 +168,37 @@ private predicate phiModulusInit(SemSsaPhiNode phi, SemBound b, int val, int mod | |||
| 162 | 168 | */ | |
| 163 | 169 | pragma[nomagic] | |
| 164 | 170 | private predicate phiModulusRankStep(SemSsaPhiNode phi, SemBound b, int val, int mod, int rix) { | |
| 171 | + /* | ||
| 172 | + * base case. If any phi input is equal to `b + val` modulo `mod`, that's a potential congruence | ||
| 173 | + * class for the phi node. | ||
| 174 | + */ | ||
| 175 | + | ||
| 165 | 176 | rix = 0 and | |
| 166 | 177 | phiModulusInit(phi, b, val, mod) | |
| 167 | 178 | or | |
| 168 | 179 | exists(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int v1, int m1 | | |
| 169 | 180 | mod != 1 and | |
| 170 | 181 | val = remainder(v1, mod) | |
| 171 | 182 | | | |
| 183 | + /* | ||
| 184 | + * Recursive case. If `inp` = `b + v2` mod `m2`, we combine that with the preceding potential | ||
| 185 | + * congruence class `b + v1` mod `m1`. The result will be the congruence class of `v1` modulo | ||
| 186 | + * the greatest common denominator of `m1`, `m2`, and `v1 - v2`. | ||
| 187 | + */ | ||
| 188 | + | ||
| 172 | 189 | exists(int v2, int m2 | | |
| 173 | 190 | rankedPhiInput(pragma[only_bind_out](phi), inp, edge, rix) and | |
| 174 | 191 | phiModulusRankStep(phi, b, v1, m1, rix - 1) and | |
| 175 | 192 | ssaModulus(inp, edge, b, v2, m2) and | |
| 176 | 193 | mod = m1.gcd(m2).gcd(v1 - v2) | |
| 177 | 194 | ) | |
| 178 | 195 | or | |
| 196 | + /* | ||
| 197 | + * Recursive case. If `inp` = `phi` mod `m2`, we combine that with the preceding potential | ||
| 198 | + * congruence class `b + v1` mod `m1`. The result will be a congruence class modulo the greatest | ||
| 199 | + * common denominator of `m1` and `m2`. | ||
| 200 | + */ | ||
| 201 | + | ||
| 179 | 202 | exists(int m2 | | |
| 180 | 203 | rankedPhiInput(phi, inp, edge, rix) and | |
| 181 | 204 | phiModulusRankStep(phi, b, v1, m1, rix - 1) and | |
0 commit comments