|
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