Skip to content

Commit a001ca0

Browse files
hvitvedhvitved
committed
temp
1 parent 1d5cfac commit a001ca0

File tree

1 file changed

+157
-48
lines changed

1 file changed

+157
-48
lines changed

‎shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll

Lines changed: 157 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -1051,6 +1051,23 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
10511051
/* End: Stage 1 logic. */
10521052
}
10531053

1054+
private newtype TContentOrNode =
1055+
TContentOrNodeContent(Content c) { Stage1::revFlowIsReadAndStored(c) } or
1056+
TContentOrNodeNode(NodeEx n) { Stage1::revFlow(n) }
1057+
1058+
/** A `Content` or a `NodeEx`. */
1059+
private class ContentOrNodeContent extends TContentOrNode {
1060+
Content asContent() { this = TContentOrNodeContent(result) }
1061+
1062+
NodeEx asNodeEx() { this = TContentOrNodeNode(result) }
1063+
1064+
string toString() {
1065+
result = this.asContent().toString()
1066+
or
1067+
result = this.asNodeEx().toString()
1068+
}
1069+
}
1070+
10541071
private predicate sinkNode = Stage1::sinkNode/2;
10551072

10561073
private predicate sourceModel(NodeEx node, string model) {
@@ -2364,7 +2381,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
23642381
}
23652382

23662383
pragma[nomagic]
2367-
predicate storeStepCand(
2384+
private predicate storeStepCand0(
23682385
NodeEx node1, Ap ap1, Content c, NodeEx node2, DataFlowType contentType,
23692386
DataFlowType containerType
23702387
) {
@@ -2375,7 +2392,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
23752392
)
23762393
}
23772394

2378-
predicate readStepCand(NodeEx node1, Content c, NodeEx node2) {
2395+
private predicate readStepCand0(NodeEx node1, Content c, NodeEx node2) {
23792396
exists(Ap ap1, Ap ap2 |
23802397
revFlow(node2, _, _, _, pragma[only_bind_into](ap2)) and
23812398
readStepFwd(node1, ap1, c, node2, ap2) and
@@ -2395,10 +2412,11 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
23952412

23962413
private predicate fwdConsCand(Content c, Typ t, Ap ap) { storeStepFwd(_, t, ap, c, _, _) }
23972414

2398-
private predicate revConsCand(Content c, Typ t, Ap ap) {
2399-
exists(Ap ap2 |
2400-
revFlowStore(ap2, c, ap, t, _, _, _, _, _) and
2401-
revFlowConsCand(_, ap2, c, ap)
2415+
private predicate revConsCand(NodeEx readTarget, Content c, Typ t, Ap ap) {
2416+
exists(NodeEx storeSource, Ap ap2 |
2417+
revFlowStore(ap2, c, ap, t, storeSource, _, _, _, _) and
2418+
revFlowConsCand(readTarget, ap2, c, ap) and
2419+
storeReachesRead(storeSource, readTarget)
24022420
)
24032421
}
24042422

@@ -2412,7 +2430,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
24122430
}
24132431

24142432
additional predicate consCand(Content c, Typ t, Ap ap) {
2415-
revConsCand(c, t, ap) and
2433+
revConsCand(_, c, t, ap) and
24162434
validAp(ap)
24172435
}
24182436

@@ -2501,14 +2519,23 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
25012519
callEdgeReturn(call, c, _, _, _, _, _)
25022520
}
25032521

2504-
private signature predicate storeReachesReadSig(NodeEx node1, NodeEx node2);
2505-
2506-
private module StoreReachesRead<storeReachesReadSig/2 storeReachesReadIn> {
2522+
/**
2523+
* Provides logic for computing compatible and (likely) reachable store-read pairs.
2524+
*
2525+
* In order to determine whether a store can reach a compatible read, we first compute
2526+
* the set of contents that may be both stored and read.
2527+
*
2528+
* The implementation is based on `doublyBoundedFastTC`, and in order to avoid poor
2529+
* performance through recursion, we unroll the recursion manually 4 times, in order to
2530+
* be able to handle access paths of maximum length 5.
2531+
*/
2532+
private module StoreReadReachability {
25072533
pragma[nomagic]
2508-
private predicate step(NodeEx node1, NodeEx node2) {
2534+
private predicate valueStep(NodeEx node1, NodeEx node2) {
25092535
exists(FlowState state, Ap ap, ApOption returnAp1, ApOption returnAp2 |
25102536
revFlow(node1, pragma[only_bind_into](state), _, returnAp1, pragma[only_bind_into](ap)) and
2511-
revFlow(node2, pragma[only_bind_into](state), _, returnAp2, pragma[only_bind_into](ap))
2537+
revFlow(node2, pragma[only_bind_into](state), _, returnAp2, pragma[only_bind_into](ap)) and
2538+
not ap instanceof ApNil
25122539
|
25132540
localStep(node1, state, node2, state, true, _, _) and
25142541
returnAp1 = returnAp2
@@ -2518,57 +2545,139 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
25182545
callEdgeArgParam(_, _, node1, node2, _, _)
25192546
or
25202547
callEdgeReturn(_, _, node1, _, node2, _, _)
2521-
or
2522-
storeReachesReadIn(node1, node2)
25232548
)
25242549
}
25252550

2526-
private predicate isStoreTarget(NodeEx node) { storeStepCand(_, _, _, node, _, _) }
2551+
/** Input from previous iteration. */
2552+
private signature predicate storeReachesReadSig(NodeEx node1, NodeEx node2);
25272553

2528-
private predicate isReadSource(NodeEx node) { readStepCand(node, _, _) }
2554+
private module StoreReachesRead<storeReachesReadSig/2 storeReachesReadIn> {
2555+
pragma[nomagic]
2556+
private predicate step(NodeEx node1, NodeEx node2) {
2557+
valueStep(node1, node2)
2558+
or
2559+
exists(FlowState state, Ap ap |
2560+
revFlow(node1, pragma[only_bind_into](state), _, _, pragma[only_bind_into](ap)) and
2561+
revFlow(node2, pragma[only_bind_into](state), _, _, pragma[only_bind_into](ap)) and
2562+
not ap instanceof ApNil and
2563+
storeReachesReadIn(node1, node2)
2564+
)
2565+
}
25292566

2530-
private predicate storeReachesReadTc(NodeEx node1, NodeEx node2) =
2531-
doublyBoundedFastTC(step/2, isStoreTarget/1, isReadSource/1)(node1, node2)
2567+
private predicate contentIsStored(ContentOrNodeContent c) {
2568+
storeStepCand0(_, _, c.asContent(), _, _, _)
2569+
}
25322570

2533-
bindingset[node2, c]
2534-
pragma[inline_late]
2535-
private predicate storeStepCand(NodeEx node1, Content c, NodeEx node2) {
2536-
storeStepCand(node1, _, c, node2, _, _)
2537-
}
2571+
private predicate contentIsRead(ContentOrNodeContent c) {
2572+
readStepCand0(_, c.asContent(), _)
2573+
}
25382574

2539-
pragma[nomagic]
2540-
predicate storeReachesReadOut(NodeEx node1, NodeEx node2) {
2541-
exists(Content c, NodeEx storeTarget, NodeEx readSource |
2542-
storeReachesReadTc(storeTarget, readSource) and
2543-
storeStepCand(node1, c, storeTarget) and
2544-
readStepCand(readSource, c, node2)
2545-
)
2546-
or
2547-
exists(Content c, NodeEx storeTargetReadSource |
2548-
storeStepCand(node1, c, storeTargetReadSource) and
2549-
readStepCand(storeTargetReadSource, c, node2)
2550-
)
2575+
private predicate stepNodeOrContent(ContentOrNodeContent n1, ContentOrNodeContent n2) {
2576+
step(n1.asNodeEx(), n2.asNodeEx())
2577+
or
2578+
storeStepCand0(_, _, n1.asContent(), n2.asNodeEx(), _, _)
2579+
or
2580+
readStepCand0(n1.asNodeEx(), n2.asContent(), _)
2581+
}
2582+
2583+
private predicate contentReachesReadTc(
2584+
ContentOrNodeContent node1, ContentOrNodeContent node2
2585+
) =
2586+
doublyBoundedFastTC(stepNodeOrContent/2, contentIsStored/1, contentIsRead/1)(node1,
2587+
node2)
2588+
2589+
pragma[nomagic]
2590+
private predicate contentId(ContentOrNodeContent c1, ContentOrNodeContent c2, Content c) {
2591+
c1.asContent() = c and
2592+
c2.asContent() = c
2593+
}
2594+
2595+
predicate contentIsReadAndStored(Content c) {
2596+
exists(ContentOrNodeContent n1, ContentOrNodeContent n2 |
2597+
contentReachesReadTc(n1, n2) and
2598+
contentId(n1, n2, c)
2599+
)
2600+
}
2601+
2602+
private predicate isStoreTarget(NodeEx node) {
2603+
exists(Content c |
2604+
contentIsReadAndStored(c) and
2605+
storeStepCand0(_, _, c, node, _, _)
2606+
)
2607+
}
2608+
2609+
private predicate isReadSource(NodeEx node) {
2610+
exists(Content c |
2611+
contentIsReadAndStored(c) and
2612+
readStepCand0(node, c, _)
2613+
)
2614+
}
2615+
2616+
private predicate storeReachesReadTc(NodeEx node1, NodeEx node2) =
2617+
doublyBoundedFastTC(step/2, isStoreTarget/1, isReadSource/1)(node1, node2)
2618+
2619+
pragma[nomagic]
2620+
private predicate storeStepCandIsReadAndStored(NodeEx node1, Content c, NodeEx node2) {
2621+
contentIsReadAndStored(c) and
2622+
storeStepCand0(node1, _, c, node2, _, _)
2623+
}
2624+
2625+
pragma[nomagic]
2626+
private predicate readStepCandIsReadAndStored(NodeEx node1, Content c, NodeEx node2) {
2627+
contentIsReadAndStored(c) and
2628+
readStepCand0(node1, c, node2)
2629+
}
2630+
2631+
pragma[nomagic]
2632+
predicate storeReachesReadOut(NodeEx storeSource, NodeEx readTarget) {
2633+
exists(Content c, NodeEx storeTarget, NodeEx readSource |
2634+
storeReachesReadTc(storeTarget, readSource) and
2635+
storeStepCandIsReadAndStored(storeSource, c, storeTarget) and
2636+
readStepCandIsReadAndStored(readSource, c, readTarget)
2637+
)
2638+
or
2639+
exists(Content c, NodeEx storeTargetReadSource |
2640+
storeStepCandIsReadAndStored(storeSource, c, storeTargetReadSource) and
2641+
readStepCandIsReadAndStored(storeTargetReadSource, c, readTarget)
2642+
)
2643+
}
25512644
}
2552-
}
25532645

2554-
private predicate storeReachesRead0(NodeEx node1, NodeEx node2) { none() }
2646+
private predicate storeReachesRead0(NodeEx node1, NodeEx node2) { none() }
25552647

2556-
private predicate storeReachesRead1 =
2557-
StoreReachesRead<storeReachesRead0/2>::storeReachesReadOut/2;
2648+
private predicate storeReachesRead1 =
2649+
StoreReachesRead<storeReachesRead0/2>::storeReachesReadOut/2;
25582650

2559-
private predicate storeReachesRead2 =
2560-
StoreReachesRead<storeReachesRead1/2>::storeReachesReadOut/2;
2651+
private predicate storeReachesRead2 =
2652+
StoreReachesRead<storeReachesRead1/2>::storeReachesReadOut/2;
25612653

2562-
private predicate storeReachesRead3 =
2563-
StoreReachesRead<storeReachesRead2/2>::storeReachesReadOut/2;
2654+
private predicate storeReachesRead3 =
2655+
StoreReachesRead<storeReachesRead2/2>::storeReachesReadOut/2;
25642656

2565-
private predicate storeReachesRead4 =
2566-
StoreReachesRead<storeReachesRead3/2>::storeReachesReadOut/2;
2657+
private predicate storeReachesRead4 =
2658+
StoreReachesRead<storeReachesRead3/2>::storeReachesReadOut/2;
25672659

2568-
private predicate storeReachesRead5 =
2569-
StoreReachesRead<storeReachesRead4/2>::storeReachesReadOut/2;
2660+
import StoreReachesRead<storeReachesRead4/2>
2661+
}
2662+
2663+
predicate storeReachesRead = StoreReadReachability::storeReachesReadOut/2;
2664+
2665+
pragma[nomagic]
2666+
predicate storeStepCand(
2667+
NodeEx node1, Ap ap1, Content c, NodeEx node2, DataFlowType contentType,
2668+
DataFlowType containerType
2669+
) {
2670+
storeStepCand0(node1, ap1, c, node2, contentType, containerType) and
2671+
StoreReadReachability::contentIsReadAndStored(c) and
2672+
storeReachesRead(node1, _)
2673+
}
25702674

2571-
predicate storeReachesRead = storeReachesRead5/2;
2675+
pragma[nomagic]
2676+
predicate readStepCand(NodeEx node1, Content c, NodeEx node2) {
2677+
readStepCand0(node1, c, node2) and
2678+
StoreReadReachability::contentIsReadAndStored(c) and
2679+
storeReachesRead(_, node2)
2680+
}
25722681

25732682
additional predicate stats(
25742683
boolean fwd, int nodes, int fields, int conscand, int states, int tuples, int calledges,

0 commit comments

Comments
 (0)