|
| 1 | +/** |
| 2 | + * Provides the implementation of a summary type tracker, that is type tracking through flow summaries. |
| 3 | + * To use this, you must implement the `Input` signature. You can then use the predicates in the `Output` |
| 4 | + * signature to implement the predicates of the same names inside `TypeTrackerSpecific.qll`. |
| 5 | + */ |
| 6 | + |
| 7 | +/** The classes and predicates needed to generate a summary type tracker. */ |
| 8 | +signature module Input { |
| 9 | + // Dataflow nodes |
| 10 | + class Node; |
| 11 | + |
| 12 | + // Content |
| 13 | + class TypeTrackerContent; |
| 14 | + |
| 15 | + class TypeTrackerContentFilter; |
| 16 | + |
| 17 | + // Relating content and filters |
| 18 | + /** |
| 19 | + * Gets a content filter to use for a `WithoutContent[content]` step, or has no result if |
| 20 | + * the step should be treated as ordinary flow. |
| 21 | + * |
| 22 | + * `WithoutContent` is often used to perform strong updates on individual collection elements, but for |
| 23 | + * type-tracking this is rarely beneficial and quite expensive. However, `WithoutContent` can be quite useful |
| 24 | + * for restricting the type of an object, and in these cases we translate it to a filter. |
| 25 | + */ |
| 26 | + TypeTrackerContentFilter getFilterFromWithoutContentStep(TypeTrackerContent content); |
| 27 | + |
| 28 | + /** |
| 29 | + * Gets a content filter to use for a `WithContent[content]` step, or has no result if |
| 30 | + * the step cannot be handled by type-tracking. |
| 31 | + * |
| 32 | + * `WithContent` is often used to perform strong updates on individual collection elements (or rather |
| 33 | + * to preserve those that didn't get updated). But for type-tracking this is rarely beneficial and quite expensive. |
| 34 | + * However, `WithContent` can be quite useful for restricting the type of an object, and in these cases we translate it to a filter. |
| 35 | + */ |
| 36 | + TypeTrackerContentFilter getFilterFromWithContentStep(TypeTrackerContent content); |
| 37 | + |
| 38 | + // Summaries and their stacks |
| 39 | + class SummaryComponent; |
| 40 | + |
| 41 | + class SummaryComponentStack { |
| 42 | + SummaryComponent head(); |
| 43 | + } |
| 44 | + |
| 45 | + /** Gets a singleton stack containing `component`. */ |
| 46 | + SummaryComponentStack singleton(SummaryComponent component); |
| 47 | + |
| 48 | + /** |
| 49 | + * Gets the stack obtained by pushing `head` onto `tail`. |
| 50 | + */ |
| 51 | + SummaryComponentStack push(SummaryComponent component, SummaryComponentStack stack); |
| 52 | + |
| 53 | + /** Gets a singleton stack representing a return. */ |
| 54 | + SummaryComponent return(); |
| 55 | + |
| 56 | + // Relating content to summaries |
| 57 | + /** Gets a summary component for content `c`. */ |
| 58 | + SummaryComponent content(TypeTrackerContent contents); |
| 59 | + |
| 60 | + /** Gets a summary component where data is not allowed to be stored in `c`. */ |
| 61 | + SummaryComponent withoutContent(TypeTrackerContent contents); |
| 62 | + |
| 63 | + /** Gets a summary component where data must be stored in `c`. */ |
| 64 | + SummaryComponent withContent(TypeTrackerContent contents); |
| 65 | + |
| 66 | + // Callables |
| 67 | + class SummarizedCallable { |
| 68 | + predicate propagatesFlow( |
| 69 | + SummaryComponentStack input, SummaryComponentStack output, boolean preservesValue |
| 70 | + ); |
| 71 | + } |
| 72 | + |
| 73 | + // Relating nodes to summaries |
| 74 | + /** Gets a dataflow node respresenting the argument of `call` indicated by `arg`. */ |
| 75 | + Node argumentOf(Node call, SummaryComponent arg); |
| 76 | + |
| 77 | + /** Gets a dataflow node respresenting the parameter of `callable` indicated by `param`. */ |
| 78 | + Node parameterOf(Node callable, SummaryComponent param); |
| 79 | + |
| 80 | + /** Gets a dataflow node respresenting the return of `callable` indicated by `return`. */ |
| 81 | + Node returnOf(Node callable, SummaryComponent return); |
| 82 | + |
| 83 | + // Specific summary handling |
| 84 | + /** Holds if component should be treated as a level step by type tracking. */ |
| 85 | + predicate componentLevelStep(SummaryComponent component); |
| 86 | + |
| 87 | + /** Holds if the given component can't be evaluated by `evaluateSummaryComponentStackLocal`. */ |
| 88 | + predicate isNonLocal(SummaryComponent component); |
| 89 | + |
| 90 | + // Relating callables to nodes |
| 91 | + /** Gets a dataflow node respresenting a call to `callable`. */ |
| 92 | + Node callTo(SummarizedCallable callable); |
| 93 | +} |
| 94 | + |
| 95 | +/** |
| 96 | + * The predicates provided by a summary type tracker. |
| 97 | + * These are meant to be used in `TypeTrackerSpecific.qll` |
| 98 | + * inside the predicates of the same names. |
| 99 | + */ |
| 100 | +signature module Output<Input I> { |
| 101 | + /** |
| 102 | + * Holds if there is a level step from `nodeFrom` to `nodeTo`, which does not depend on the call graph. |
| 103 | + */ |
| 104 | + predicate levelStepNoCall(I::Node nodeFrom, I::Node nodeTo); |
| 105 | + |
| 106 | + /** |
| 107 | + * Holds if `nodeTo` is the result of accessing the `content` content of `nodeFrom`. |
| 108 | + */ |
| 109 | + predicate basicLoadStep(I::Node nodeFrom, I::Node nodeTo, I::TypeTrackerContent content); |
| 110 | + |
| 111 | + /** |
| 112 | + * Holds if `nodeFrom` is being written to the `content` content of the object in `nodeTo`. |
| 113 | + */ |
| 114 | + predicate basicStoreStep(I::Node nodeFrom, I::Node nodeTo, I::TypeTrackerContent content); |
| 115 | + |
| 116 | + /** |
| 117 | + * Holds if the `loadContent` of `nodeFrom` is stored in the `storeContent` of `nodeTo`. |
| 118 | + */ |
| 119 | + predicate basicLoadStoreStep( |
| 120 | + I::Node nodeFrom, I::Node nodeTo, I::TypeTrackerContent loadContent, |
| 121 | + I::TypeTrackerContent storeContent |
| 122 | + ); |
| 123 | + |
| 124 | + /** |
| 125 | + * Holds if type-tracking should step from `nodeFrom` to `nodeTo` but block flow of contents matched by `filter` through here. |
| 126 | + */ |
| 127 | + predicate basicWithoutContentStep( |
| 128 | + I::Node nodeFrom, I::Node nodeTo, I::TypeTrackerContentFilter filter |
| 129 | + ); |
| 130 | + |
| 131 | + /** |
| 132 | + * Holds if type-tracking should step from `nodeFrom` to `nodeTo` if inside a content matched by `filter`. |
| 133 | + */ |
| 134 | + predicate basicWithContentStep( |
| 135 | + I::Node nodeFrom, I::Node nodeTo, I::TypeTrackerContentFilter filter |
| 136 | + ); |
| 137 | +} |
| 138 | + |
| 139 | +/** |
| 140 | + * Implementation of the summary type tracker, that is type tracking through flow summaries. |
| 141 | + */ |
| 142 | +module SummaryFlow<Input I> implements Output<I> { |
| 143 | + pragma[nomagic] |
| 144 | + private predicate hasLoadSummary( |
| 145 | + I::SummarizedCallable callable, I::TypeTrackerContent contents, I::SummaryComponentStack input, |
| 146 | + I::SummaryComponentStack output |
| 147 | + ) { |
| 148 | + callable.propagatesFlow(I::push(I::content(contents), input), output, true) and |
| 149 | + not I::isNonLocal(input.head()) and |
| 150 | + not I::isNonLocal(output.head()) |
| 151 | + } |
| 152 | + |
| 153 | + pragma[nomagic] |
| 154 | + private predicate hasStoreSummary( |
| 155 | + I::SummarizedCallable callable, I::TypeTrackerContent contents, I::SummaryComponentStack input, |
| 156 | + I::SummaryComponentStack output |
| 157 | + ) { |
| 158 | + not I::isNonLocal(input.head()) and |
| 159 | + not I::isNonLocal(output.head()) and |
| 160 | + ( |
| 161 | + callable.propagatesFlow(input, I::push(I::content(contents), output), true) |
| 162 | + or |
| 163 | + // Allow the input to start with an arbitrary WithoutContent[X]. |
| 164 | + // Since type-tracking only tracks one content deep, and we're about to store into another content, |
| 165 | + // we're already preventing the input from being in a content. |
| 166 | + callable |
| 167 | + .propagatesFlow(I::push(I::withoutContent(_), input), |
| 168 | + I::push(I::content(contents), output), true) |
| 169 | + ) |
| 170 | + } |
| 171 | + |
| 172 | + pragma[nomagic] |
| 173 | + private predicate hasLoadStoreSummary( |
| 174 | + I::SummarizedCallable callable, I::TypeTrackerContent loadContents, |
| 175 | + I::TypeTrackerContent storeContents, I::SummaryComponentStack input, |
| 176 | + I::SummaryComponentStack output |
| 177 | + ) { |
| 178 | + callable |
| 179 | + .propagatesFlow(I::push(I::content(loadContents), input), |
| 180 | + I::push(I::content(storeContents), output), true) and |
| 181 | + not I::isNonLocal(input.head()) and |
| 182 | + not I::isNonLocal(output.head()) |
| 183 | + } |
| 184 | + |
| 185 | + pragma[nomagic] |
| 186 | + private predicate hasWithoutContentSummary( |
| 187 | + I::SummarizedCallable callable, I::TypeTrackerContentFilter filter, |
| 188 | + I::SummaryComponentStack input, I::SummaryComponentStack output |
| 189 | + ) { |
| 190 | + exists(I::TypeTrackerContent content | |
| 191 | + callable.propagatesFlow(I::push(I::withoutContent(content), input), output, true) and |
| 192 | + filter = I::getFilterFromWithoutContentStep(content) and |
| 193 | + not I::isNonLocal(input.head()) and |
| 194 | + not I::isNonLocal(output.head()) and |
| 195 | + input != output |
| 196 | + ) |
| 197 | + } |
| 198 | + |
| 199 | + pragma[nomagic] |
| 200 | + private predicate hasWithContentSummary( |
| 201 | + I::SummarizedCallable callable, I::TypeTrackerContentFilter filter, |
| 202 | + I::SummaryComponentStack input, I::SummaryComponentStack output |
| 203 | + ) { |
| 204 | + exists(I::TypeTrackerContent content | |
| 205 | + callable.propagatesFlow(I::push(I::withContent(content), input), output, true) and |
| 206 | + filter = I::getFilterFromWithContentStep(content) and |
| 207 | + not I::isNonLocal(input.head()) and |
| 208 | + not I::isNonLocal(output.head()) and |
| 209 | + input != output |
| 210 | + ) |
| 211 | + } |
| 212 | + |
| 213 | + /** |
| 214 | + * Gets a data flow I::Node corresponding an argument or return value of `call`, |
| 215 | + * as specified by `component`. |
| 216 | + */ |
| 217 | + bindingset[call, component] |
| 218 | + private I::Node evaluateSummaryComponentLocal(I::Node call, I::SummaryComponent component) { |
| 219 | + result = I::argumentOf(call, component) |
| 220 | + or |
| 221 | + component = I::return() and |
| 222 | + result = call |
| 223 | + } |
| 224 | + |
| 225 | + /** |
| 226 | + * Holds if `callable` is relevant for type-tracking and we therefore want `stack` to |
| 227 | + * be evaluated locally at its call sites. |
| 228 | + */ |
| 229 | + pragma[nomagic] |
| 230 | + private predicate dependsOnSummaryComponentStack( |
| 231 | + I::SummarizedCallable callable, I::SummaryComponentStack stack |
| 232 | + ) { |
| 233 | + exists(I::callTo(callable)) and |
| 234 | + ( |
| 235 | + callable.propagatesFlow(stack, _, true) |
| 236 | + or |
| 237 | + callable.propagatesFlow(_, stack, true) |
| 238 | + or |
| 239 | + // include store summaries as they may skip an initial step at the input |
| 240 | + hasStoreSummary(callable, _, stack, _) |
| 241 | + ) |
| 242 | + or |
| 243 | + dependsOnSummaryComponentStackCons(callable, _, stack) |
| 244 | + } |
| 245 | + |
| 246 | + pragma[nomagic] |
| 247 | + private predicate dependsOnSummaryComponentStackCons( |
| 248 | + I::SummarizedCallable callable, I::SummaryComponent head, I::SummaryComponentStack tail |
| 249 | + ) { |
| 250 | + dependsOnSummaryComponentStack(callable, I::push(head, tail)) |
| 251 | + } |
| 252 | + |
| 253 | + pragma[nomagic] |
| 254 | + private predicate dependsOnSummaryComponentStackConsLocal( |
| 255 | + I::SummarizedCallable callable, I::SummaryComponent head, I::SummaryComponentStack tail |
| 256 | + ) { |
| 257 | + dependsOnSummaryComponentStackCons(callable, head, tail) and |
| 258 | + not I::isNonLocal(head) |
| 259 | + } |
| 260 | + |
| 261 | + pragma[nomagic] |
| 262 | + private predicate dependsOnSummaryComponentStackLeaf( |
| 263 | + I::SummarizedCallable callable, I::SummaryComponent leaf |
| 264 | + ) { |
| 265 | + dependsOnSummaryComponentStack(callable, I::singleton(leaf)) |
| 266 | + } |
| 267 | + |
| 268 | + /** |
| 269 | + * Gets a data flow I::Node corresponding to the local input or output of `call` |
| 270 | + * identified by `stack`, if possible. |
| 271 | + */ |
| 272 | + pragma[nomagic] |
| 273 | + private I::Node evaluateSummaryComponentStackLocal( |
| 274 | + I::SummarizedCallable callable, I::Node call, I::SummaryComponentStack stack |
| 275 | + ) { |
| 276 | + exists(I::SummaryComponent component | |
| 277 | + dependsOnSummaryComponentStackLeaf(callable, component) and |
| 278 | + stack = I::singleton(component) and |
| 279 | + call = I::callTo(callable) and |
| 280 | + result = evaluateSummaryComponentLocal(call, component) |
| 281 | + ) |
| 282 | + or |
| 283 | + exists(I::Node prev, I::SummaryComponent head, I::SummaryComponentStack tail | |
| 284 | + prev = evaluateSummaryComponentStackLocal(callable, call, tail) and |
| 285 | + dependsOnSummaryComponentStackConsLocal(callable, pragma[only_bind_into](head), |
| 286 | + pragma[only_bind_out](tail)) and |
| 287 | + stack = I::push(pragma[only_bind_out](head), pragma[only_bind_out](tail)) |
| 288 | + | |
| 289 | + result = I::parameterOf(prev, head) |
| 290 | + or |
| 291 | + result = I::returnOf(prev, head) |
| 292 | + or |
| 293 | + I::componentLevelStep(head) and |
| 294 | + result = prev |
| 295 | + ) |
| 296 | + } |
| 297 | + |
| 298 | + // Implement Output |
| 299 | + predicate levelStepNoCall(I::Node nodeFrom, I::Node nodeTo) { |
| 300 | + exists( |
| 301 | + I::SummarizedCallable callable, I::Node call, I::SummaryComponentStack input, |
| 302 | + I::SummaryComponentStack output |
| 303 | + | |
| 304 | + callable.propagatesFlow(input, output, true) and |
| 305 | + call = I::callTo(callable) and |
| 306 | + nodeFrom = evaluateSummaryComponentStackLocal(callable, call, input) and |
| 307 | + nodeTo = evaluateSummaryComponentStackLocal(callable, call, output) |
| 308 | + ) |
| 309 | + } |
| 310 | + |
| 311 | + predicate basicLoadStep(I::Node nodeFrom, I::Node nodeTo, I::TypeTrackerContent content) { |
| 312 | + exists( |
| 313 | + I::SummarizedCallable callable, I::Node call, I::SummaryComponentStack input, |
| 314 | + I::SummaryComponentStack output |
| 315 | + | |
| 316 | + hasLoadSummary(callable, content, pragma[only_bind_into](input), |
| 317 | + pragma[only_bind_into](output)) and |
| 318 | + call = I::callTo(callable) and |
| 319 | + nodeFrom = evaluateSummaryComponentStackLocal(callable, call, input) and |
| 320 | + nodeTo = evaluateSummaryComponentStackLocal(callable, call, output) |
| 321 | + ) |
| 322 | + } |
| 323 | + |
| 324 | + predicate basicStoreStep(I::Node nodeFrom, I::Node nodeTo, I::TypeTrackerContent content) { |
| 325 | + exists( |
| 326 | + I::SummarizedCallable callable, I::Node call, I::SummaryComponentStack input, |
| 327 | + I::SummaryComponentStack output |
| 328 | + | |
| 329 | + hasStoreSummary(callable, content, pragma[only_bind_into](input), |
| 330 | + pragma[only_bind_into](output)) and |
| 331 | + call = I::callTo(callable) and |
| 332 | + nodeFrom = evaluateSummaryComponentStackLocal(callable, call, input) and |
| 333 | + nodeTo = evaluateSummaryComponentStackLocal(callable, call, output) |
| 334 | + ) |
| 335 | + } |
| 336 | + |
| 337 | + predicate basicLoadStoreStep( |
| 338 | + I::Node nodeFrom, I::Node nodeTo, I::TypeTrackerContent loadContent, |
| 339 | + I::TypeTrackerContent storeContent |
| 340 | + ) { |
| 341 | + exists( |
| 342 | + I::SummarizedCallable callable, I::Node call, I::SummaryComponentStack input, |
| 343 | + I::SummaryComponentStack output |
| 344 | + | |
| 345 | + hasLoadStoreSummary(callable, loadContent, storeContent, pragma[only_bind_into](input), |
| 346 | + pragma[only_bind_into](output)) and |
| 347 | + call = I::callTo(callable) and |
| 348 | + nodeFrom = evaluateSummaryComponentStackLocal(callable, call, input) and |
| 349 | + nodeTo = evaluateSummaryComponentStackLocal(callable, call, output) |
| 350 | + ) |
| 351 | + } |
| 352 | + |
| 353 | + predicate basicWithoutContentStep( |
| 354 | + I::Node nodeFrom, I::Node nodeTo, I::TypeTrackerContentFilter filter |
| 355 | + ) { |
| 356 | + exists( |
| 357 | + I::SummarizedCallable callable, I::Node call, I::SummaryComponentStack input, |
| 358 | + I::SummaryComponentStack output |
| 359 | + | |
| 360 | + hasWithoutContentSummary(callable, filter, pragma[only_bind_into](input), |
| 361 | + pragma[only_bind_into](output)) and |
| 362 | + call = I::callTo(callable) and |
| 363 | + nodeFrom = evaluateSummaryComponentStackLocal(callable, call, input) and |
| 364 | + nodeTo = evaluateSummaryComponentStackLocal(callable, call, output) |
| 365 | + ) |
| 366 | + } |
| 367 | + |
| 368 | + predicate basicWithContentStep( |
| 369 | + I::Node nodeFrom, I::Node nodeTo, I::TypeTrackerContentFilter filter |
| 370 | + ) { |
| 371 | + exists( |
| 372 | + I::SummarizedCallable callable, I::Node call, I::SummaryComponentStack input, |
| 373 | + I::SummaryComponentStack output |
| 374 | + | |
| 375 | + hasWithContentSummary(callable, filter, pragma[only_bind_into](input), |
| 376 | + pragma[only_bind_into](output)) and |
| 377 | + call = I::callTo(callable) and |
| 378 | + nodeFrom = evaluateSummaryComponentStackLocal(callable, call, input) and |
| 379 | + nodeTo = evaluateSummaryComponentStackLocal(callable, call, output) |
| 380 | + ) |
| 381 | + } |
| 382 | +} |
0 commit comments