|
4 | 4 | */ |
5 | 5 |
|
6 | 6 | private import DataFlowImplCommon |
7 | | -private import DataFlowPrivate as DataFlowPrivate |
8 | 7 |
|
9 | 8 | module ContentDataFlow { |
10 | 9 | private import DataFlowImplSpecific::Private |
| 10 | + private import DataFlowImplSpecific::Private as DataFlowPrivate |
11 | 11 | private import DataFlowImplForContentDataFlow as DF |
12 | 12 |
|
13 | 13 | class Node = DF::Node; |
@@ -253,6 +253,7 @@ module ContentDataFlow { |
253 | 253 |
|
254 | 254 | final override FlowFeature getAFeature() { result = c.getAFeature() } |
255 | 255 |
|
| 256 | + // needed to record reads/stores inside summarized callables |
256 | 257 | final override predicate includeHiddenNodes() { any() } |
257 | 258 | } |
258 | 259 |
|
@@ -289,143 +290,239 @@ module ContentDataFlow { |
289 | 290 | } |
290 | 291 | } |
291 | 292 |
|
292 | | - pragma[nomagic] |
293 | | - private predicate pathNodeSuccEntry(DF::PathNode node) { |
294 | | - node.getConfiguration() instanceof Configuration and |
295 | | - ( |
296 | | - any(ConfigurationAdapter config).isSource(node.getNode(), node.getState()) |
297 | | - or |
298 | | - DF::PathGraph::subpaths(_, _, _, node) |
299 | | - or |
300 | | - DF::PathGraph::subpaths(_, node, _, _) |
301 | | - or |
302 | | - storeStep(_, _, _, node.getNode(), node.getState(), node.getConfiguration()) |
303 | | - or |
304 | | - readStep(_, _, _, node.getNode(), node.getState(), node.getConfiguration()) |
305 | | - ) |
306 | | - } |
| 293 | + // important to use `edges` and not `PathNode::getASuccessor()`, as the latter |
| 294 | + // is not pruned for reachability |
| 295 | + private predicate pathSucc = DF::PathGraph::edges/2; |
307 | 296 |
|
308 | | - pragma[nomagic] |
309 | | - private predicate pathNodeSuccExit(DF::PathNode node) { |
310 | | - node.getConfiguration() instanceof Configuration and |
311 | | - ( |
| 297 | + /** |
| 298 | + * Provides a big-step flow relation, where flow stops at read/store steps that |
| 299 | + * must be recorded, and flow via `subpaths` such that reads/stores inside |
| 300 | + * summarized callables can be recorded as well. |
| 301 | + */ |
| 302 | + private module BigStepFlow { |
| 303 | + private predicate reachesSink(DF::PathNode node) { |
312 | 304 | any(ConfigurationAdapter config).isSink(node.getNode(), node.getState()) |
313 | 305 | or |
314 | | - DF::PathGraph::subpaths(node, _, _, _) |
315 | | - or |
316 | | - DF::PathGraph::subpaths(_, _, node, _) |
317 | | - or |
318 | | - storeStep(node.getNode(), node.getState(), _, _, _, node.getConfiguration()) |
319 | | - or |
320 | | - readStep(node.getNode(), node.getState(), _, _, _, node.getConfiguration()) |
321 | | - ) |
322 | | - } |
| 306 | + exists(DF::PathNode mid | |
| 307 | + pathSucc(node, mid) and |
| 308 | + reachesSink(mid) |
| 309 | + ) |
| 310 | + } |
323 | 311 |
|
324 | | - pragma[nomagic] |
325 | | - private predicate pathNodeSuccRec(DF::PathNode pred, DF::PathNode succ) { |
326 | | - pathNodeSuccEntry(pred) and |
327 | | - succ = pred |
328 | | - or |
329 | | - exists(DF::PathNode mid | |
330 | | - pathNodeSuccRec(pred, mid) and |
331 | | - succ = mid.getASuccessor() and |
332 | | - not DF::PathGraph::subpaths(mid, succ, _, _) and |
333 | | - not pathNodeSuccExit(mid) |
334 | | - ) |
335 | | - } |
| 312 | + /** |
| 313 | + * Holds if the flow step `pred -> succ` should not be allowed to be included |
| 314 | + * in the big-step relation. |
| 315 | + */ |
| 316 | + pragma[nomagic] |
| 317 | + private predicate excludeStep(DF::PathNode pred, DF::PathNode succ) { |
| 318 | + pathSucc(pred, succ) and |
| 319 | + ( |
| 320 | + // we need to record reads/stores inside summarized callables |
| 321 | + DF::PathGraph::subpaths(pred, _, _, succ) |
| 322 | + or |
| 323 | + // only allow flow into a summarized callable, as part of the big-step |
| 324 | + // relation, when flow can reach a sink without going back out |
| 325 | + DF::PathGraph::subpaths(pred, succ, _, _) and |
| 326 | + not reachesSink(succ) |
| 327 | + or |
| 328 | + // needed to record store steps |
| 329 | + storeStep(pred.getNode(), pred.getState(), _, succ.getNode(), succ.getState(), |
| 330 | + pred.getConfiguration()) |
| 331 | + or |
| 332 | + // needed to record read steps |
| 333 | + readStep(pred.getNode(), pred.getState(), _, succ.getNode(), succ.getState(), |
| 334 | + pred.getConfiguration()) |
| 335 | + ) |
| 336 | + } |
336 | 337 |
|
337 | | - pragma[nomagic] |
338 | | - private predicate pathNodeSuccBigStep(DF::PathNode pred, DF::PathNode succ) { |
339 | | - pathNodeSuccRec(pred, succ) and |
340 | | - pathNodeSuccExit(succ) |
| 338 | + pragma[nomagic] |
| 339 | + private DataFlowCallable getEnclosingCallableImpl(DF::PathNode node) { |
| 340 | + result = getNodeEnclosingCallable(node.getNode()) |
| 341 | + } |
| 342 | + |
| 343 | + pragma[inline] |
| 344 | + private DataFlowCallable getEnclosingCallable(DF::PathNode node) { |
| 345 | + pragma[only_bind_into](result) = getEnclosingCallableImpl(pragma[only_bind_out](node)) |
| 346 | + } |
| 347 | + |
| 348 | + pragma[nomagic] |
| 349 | + private predicate bigStepEntry(DF::PathNode node) { |
| 350 | + node.getConfiguration() instanceof Configuration and |
| 351 | + ( |
| 352 | + any(ConfigurationAdapter config).isSource(node.getNode(), node.getState()) |
| 353 | + or |
| 354 | + excludeStep(_, node) |
| 355 | + or |
| 356 | + DF::PathGraph::subpaths(_, node, _, _) |
| 357 | + ) |
| 358 | + } |
| 359 | + |
| 360 | + pragma[nomagic] |
| 361 | + private predicate bigStepExit(DF::PathNode node) { |
| 362 | + node.getConfiguration() instanceof Configuration and |
| 363 | + ( |
| 364 | + bigStepEntry(node) |
| 365 | + or |
| 366 | + any(ConfigurationAdapter config).isSink(node.getNode(), node.getState()) |
| 367 | + or |
| 368 | + excludeStep(node, _) |
| 369 | + or |
| 370 | + DF::PathGraph::subpaths(_, _, node, _) |
| 371 | + ) |
| 372 | + } |
| 373 | + |
| 374 | + pragma[nomagic] |
| 375 | + private predicate step(DF::PathNode pred, DF::PathNode succ) { |
| 376 | + pathSucc(pred, succ) and |
| 377 | + not excludeStep(pred, succ) |
| 378 | + } |
| 379 | + |
| 380 | + pragma[nomagic] |
| 381 | + private predicate stepRec(DF::PathNode pred, DF::PathNode succ) { |
| 382 | + step(pred, succ) and |
| 383 | + not bigStepEntry(pred) |
| 384 | + } |
| 385 | + |
| 386 | + private predicate stepRecPlus(DF::PathNode n1, DF::PathNode n2) = fastTC(stepRec/2)(n1, n2) |
| 387 | + |
| 388 | + /** |
| 389 | + * Holds if there is flow `pathSucc+(pred) = succ`, and such a flow path does |
| 390 | + * not go through any reads/stores that need to be recorded, or summarized |
| 391 | + * steps. |
| 392 | + */ |
| 393 | + pragma[nomagic] |
| 394 | + private predicate bigStep(DF::PathNode pred, DF::PathNode succ) { |
| 395 | + exists(DF::PathNode mid | |
| 396 | + bigStepEntry(pred) and |
| 397 | + step(pred, mid) |
| 398 | + | |
| 399 | + succ = mid |
| 400 | + or |
| 401 | + stepRecPlus(mid, succ) |
| 402 | + ) and |
| 403 | + bigStepExit(succ) |
| 404 | + } |
| 405 | + |
| 406 | + pragma[nomagic] |
| 407 | + predicate bigStepNotLocal(DF::PathNode pred, DF::PathNode succ) { |
| 408 | + bigStep(pred, succ) and |
| 409 | + not getEnclosingCallable(pred) = getEnclosingCallable(succ) |
| 410 | + } |
| 411 | + |
| 412 | + pragma[nomagic] |
| 413 | + predicate bigStepMaybeLocal(DF::PathNode pred, DF::PathNode succ) { |
| 414 | + bigStep(pred, succ) and |
| 415 | + getEnclosingCallable(pred) = getEnclosingCallable(succ) |
| 416 | + } |
341 | 417 | } |
342 | 418 |
|
| 419 | + /** |
| 420 | + * Holds if `source` can reach `node`, having read `reads` from the source and |
| 421 | + * written `stores` into `node`. |
| 422 | + * |
| 423 | + * `source` is either a source from a configuration, in which case `scReads` and |
| 424 | + * `scStores` are always empty, or it is the parameter of a summarized callable, |
| 425 | + * in which case `scReads` and `scStores` record the reads/stores for a summary |
| 426 | + * context, that is, the reads/stores for an argument that can reach the parameter. |
| 427 | + */ |
343 | 428 | pragma[nomagic] |
344 | 429 | private predicate nodeReaches( |
345 | | - DF::PathNode source, AccessPath readsIn, AccessPath storesIn, DF::PathNode node, |
346 | | - AccessPath readsOut, AccessPath storesOut |
| 430 | + DF::PathNode source, AccessPath scReads, AccessPath scStores, DF::PathNode node, |
| 431 | + AccessPath reads, AccessPath stores |
347 | 432 | ) { |
348 | 433 | exists(ConfigurationAdapter config | |
349 | 434 | node = source and |
350 | | - readsOut = readsIn and |
351 | | - storesOut = storesIn |
| 435 | + reads = scReads and |
| 436 | + stores = scStores |
352 | 437 | | |
353 | 438 | config.hasFlowPath(source, _) and |
354 | | - readsIn = TAccessPathNil() and |
355 | | - storesIn = TAccessPathNil() |
| 439 | + scReads = TAccessPathNil() and |
| 440 | + scStores = TAccessPathNil() |
356 | 441 | or |
| 442 | + // the argument in a sub path can be reached, so we start flow from the sub path |
| 443 | + // parameter, while recording the read/store summary context |
357 | 444 | exists(DF::PathNode arg | |
358 | | - nodeReachesSubpathArg(_, _, _, arg, readsIn, storesIn) and |
| 445 | + nodeReachesSubpathArg(_, _, _, arg, scReads, scStores) and |
359 | 446 | DF::PathGraph::subpaths(arg, source, _, _) |
360 | 447 | ) |
361 | 448 | ) |
362 | 449 | or |
363 | 450 | exists(DF::PathNode mid | |
364 | | - nodeReaches(source, readsIn, storesIn, mid, readsOut, storesOut) and |
365 | | - pathNodeSuccBigStep(mid, node) |
| 451 | + nodeReaches(source, scReads, scStores, mid, reads, stores) and |
| 452 | + BigStepFlow::bigStepMaybeLocal(mid, node) |
| 453 | + ) |
| 454 | + or |
| 455 | + exists(DF::PathNode mid | |
| 456 | + nodeReaches(source, scReads, scStores, mid, reads, stores) and |
| 457 | + BigStepFlow::bigStepNotLocal(mid, node) and |
| 458 | + // when flow is not local, we cannot flow back out, so we may stop |
| 459 | + // flow early when computing summary flow |
| 460 | + any(ConfigurationAdapter config).hasFlowPath(source, _) and |
| 461 | + scReads = TAccessPathNil() and |
| 462 | + scStores = TAccessPathNil() |
366 | 463 | ) |
367 | 464 | or |
368 | 465 | // store step |
369 | | - exists(AccessPath storesOutMid, ContentSet c | |
370 | | - nodeReachesStore(source, readsIn, storesIn, node, c, readsOut, storesOutMid) and |
371 | | - storesOut = TAccessPathCons(c, storesOutMid) |
| 466 | + exists(AccessPath storesMid, ContentSet c | |
| 467 | + nodeReachesStore(source, scReads, scStores, node, c, reads, storesMid) and |
| 468 | + stores = TAccessPathCons(c, storesMid) |
372 | 469 | ) |
373 | 470 | or |
374 | 471 | // read step |
375 | | - exists(AccessPath readsOutMid, ContentSet c | |
376 | | - nodeReachesRead(source, readsIn, storesIn, node, c, readsOutMid, storesOut) and |
377 | | - readsOut = TAccessPathCons(c, readsOutMid) |
| 472 | + exists(AccessPath readsMid, ContentSet c | |
| 473 | + nodeReachesRead(source, scReads, scStores, node, c, readsMid, stores) and |
| 474 | + reads = TAccessPathCons(c, readsMid) |
378 | 475 | ) |
379 | 476 | or |
380 | | - // flow-through step |
381 | | - exists(DF::PathNode mid, AccessPath readsMid, AccessPath storesMid | |
382 | | - nodeReachesSubpathArg(source, readsIn, storesIn, mid, readsMid, storesMid) and |
383 | | - subpathArgReachesOut(mid, readsMid, storesMid, node, readsOut, storesOut) |
| 477 | + // flow-through step; match outer stores/reads with inner store/read summary contexts |
| 478 | + exists(DF::PathNode mid, AccessPath innerScReads, AccessPath innerScStores | |
| 479 | + nodeReachesSubpathArg(source, scReads, scStores, mid, innerScReads, innerScStores) and |
| 480 | + subpathArgReachesOut(mid, innerScReads, innerScStores, node, reads, stores) |
384 | 481 | ) |
385 | 482 | } |
386 | 483 |
|
387 | 484 | pragma[nomagic] |
388 | 485 | private predicate nodeReachesStore( |
389 | | - DF::PathNode source, AccessPath readsIn, AccessPath storesIn, DF::PathNode node, ContentSet c, |
390 | | - AccessPath readsOut, AccessPath storesOut |
| 486 | + DF::PathNode source, AccessPath scReads, AccessPath scStores, DF::PathNode node, ContentSet c, |
| 487 | + AccessPath reads, AccessPath stores |
391 | 488 | ) { |
392 | 489 | exists(DF::PathNode mid | |
393 | | - nodeReaches(source, readsIn, storesIn, mid, readsOut, storesOut) and |
| 490 | + nodeReaches(source, scReads, scStores, mid, reads, stores) and |
394 | 491 | storeStep(mid.getNode(), mid.getState(), c, node.getNode(), node.getState(), |
395 | 492 | node.getConfiguration()) and |
396 | | - node = mid.getASuccessor() |
| 493 | + pathSucc(mid, node) |
397 | 494 | ) |
398 | 495 | } |
399 | 496 |
|
400 | 497 | pragma[nomagic] |
401 | 498 | private predicate nodeReachesRead( |
402 | | - DF::PathNode source, AccessPath readsIn, AccessPath storesIn, DF::PathNode node, ContentSet c, |
403 | | - AccessPath readsOut, AccessPath storesOut |
| 499 | + DF::PathNode source, AccessPath scReads, AccessPath scStores, DF::PathNode node, ContentSet c, |
| 500 | + AccessPath reads, AccessPath stores |
404 | 501 | ) { |
405 | 502 | exists(DF::PathNode mid | |
406 | | - nodeReaches(source, readsIn, storesIn, mid, readsOut, storesOut) and |
| 503 | + nodeReaches(source, scReads, scStores, mid, reads, stores) and |
407 | 504 | readStep(mid.getNode(), mid.getState(), c, node.getNode(), node.getState(), |
408 | 505 | node.getConfiguration()) and |
409 | | - node = mid.getASuccessor() |
| 506 | + pathSucc(mid, node) |
410 | 507 | ) |
411 | 508 | } |
412 | 509 |
|
413 | 510 | pragma[nomagic] |
414 | 511 | private predicate nodeReachesSubpathArg( |
415 | | - DF::PathNode source, AccessPath readsIn, AccessPath storesIn, DF::PathNode arg, |
416 | | - AccessPath readsOut, AccessPath storesOut |
| 512 | + DF::PathNode source, AccessPath scReads, AccessPath scStores, DF::PathNode arg, |
| 513 | + AccessPath reads, AccessPath stores |
417 | 514 | ) { |
418 | | - nodeReaches(source, readsIn, storesIn, arg, readsOut, storesOut) and |
| 515 | + nodeReaches(source, scReads, scStores, arg, reads, stores) and |
419 | 516 | DF::PathGraph::subpaths(arg, _, _, _) |
420 | 517 | } |
421 | 518 |
|
422 | 519 | pragma[nomagic] |
423 | 520 | private predicate subpathArgReachesOut( |
424 | | - DF::PathNode arg, AccessPath readsIn, AccessPath storesIn, DF::PathNode out, |
425 | | - AccessPath readsOut, AccessPath storesOut |
| 521 | + DF::PathNode arg, AccessPath scReads, AccessPath scStores, DF::PathNode out, AccessPath reads, |
| 522 | + AccessPath stores |
426 | 523 | ) { |
427 | 524 | exists(DF::PathNode source, DF::PathNode ret | |
428 | | - nodeReaches(source, readsIn, storesIn, ret, readsOut, storesOut) and |
| 525 | + nodeReaches(source, scReads, scStores, ret, reads, stores) and |
429 | 526 | DF::PathGraph::subpaths(arg, source, ret, out) |
430 | 527 | ) |
431 | 528 | } |
|
0 commit comments