Skip to content

Commit

Permalink
temp
Browse files Browse the repository at this point in the history
  • Loading branch information
hvitved committed Jun 12, 2024
1 parent e02310c commit 8f901da
Showing 1 changed file with 31 additions and 32 deletions.
63 changes: 31 additions & 32 deletions shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll
Original file line number Diff line number Diff line change
Expand Up @@ -2170,9 +2170,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
returnAp = apNone()
or
// store
exists(Ap ap0, Content c |
exists(NodeEx readTarget, Ap ap0, Content c |
revFlowStore(ap0, c, ap, _, node, state, _, returnCtx, returnAp) and
revFlowConsCand(ap0, c, ap)
revFlowConsCand(readTarget, ap0, c, ap) and
PrevStage::storeReachesRead(node, readTarget)
)
or
// read
Expand Down Expand Up @@ -2238,11 +2239,11 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
* resulting in access path `cons`.
*/
pragma[nomagic]
private predicate revFlowConsCand(Ap cons, Content c, Ap tail) {
exists(NodeEx mid, Ap tail0 |
revFlow(mid, _, _, _, tail) and
private predicate revFlowConsCand(NodeEx readTarget, Ap cons, Content c, Ap tail) {
exists(Ap tail0 |
revFlow(readTarget, _, _, _, tail) and
tail = pragma[only_bind_into](tail0) and
readStepFwd(_, cons, c, mid, tail0)
readStepFwd(_, cons, c, readTarget, tail0)
)
}

Expand Down Expand Up @@ -2370,7 +2371,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
exists(Ap ap2 |
PrevStage::storeStepCand(node1, _, c, node2, contentType, containerType) and
revFlowStore(ap2, c, ap1, _, node1, _, node2, _, _) and
revFlowConsCand(ap2, c, ap1)
revFlowConsCand(_, ap2, c, ap1)
)
}

Expand All @@ -2397,7 +2398,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
private predicate revConsCand(Content c, Typ t, Ap ap) {
exists(Ap ap2 |
revFlowStore(ap2, c, ap, t, _, _, _, _, _) and
revFlowConsCand(ap2, c, ap)
revFlowConsCand(_, ap2, c, ap)
)
}

Expand Down Expand Up @@ -2502,18 +2503,15 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {

private signature predicate storeReachesReadSig(NodeEx node1, NodeEx node2);

private newtype TNodeAndAp = MkNodeAndAp(TNodeEx node, Ap ap) { revFlow(node, _, _, _, ap) }

private module StoreReachesRead<storeReachesReadSig/2 storeReachesReadIn> {
pragma[nomagic]
private predicate step(TNodeAndAp n1, TNodeAndAp n2) {
exists(NodeEx node1, NodeEx node2, Ap ap, FlowState state1, FlowState state2 |
revFlow(node1, state1) and
revFlow(node2, state2) and
n1 = MkNodeAndAp(node1, pragma[only_bind_into](ap)) and
n2 = MkNodeAndAp(node2, pragma[only_bind_into](ap))
private predicate step(NodeEx node1, NodeEx node2) {
exists(FlowState state, Ap ap, ApOption returnAp1, ApOption returnAp2 |
revFlow(node1, pragma[only_bind_into](state), _, returnAp1, pragma[only_bind_into](ap)) and
revFlow(node2, pragma[only_bind_into](state), _, returnAp2, pragma[only_bind_into](ap))
|
localStep(node1, state1, node2, state2, true, _, _)
localStep(node1, state, node2, state, true, _, _) and
returnAp1 = returnAp2
or
jumpStepEx(node1, node2)
or
Expand All @@ -2525,30 +2523,31 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
)
}

private predicate isStoreTarget(TNodeAndAp n) {
exists(NodeEx node, Ap ap |
n = MkNodeAndAp(node, ap) and
storeStepCand(_, _, _, node, _, _)
)
}
private predicate isStoreTarget(NodeEx node) { storeStepCand(_, _, _, node, _, _) }

private predicate isReadSource(TNodeAndAp n) {
exists(NodeEx node, Ap ap |
n = MkNodeAndAp(node, ap) and
readStepCand(node, _, _)
)
}
private predicate isReadSource(NodeEx node) { readStepCand(node, _, _) }

private predicate storeReachesReadTc(TNodeAndAp node1, TNodeAndAp node2) =
private predicate storeReachesReadTc(NodeEx node1, NodeEx node2) =
doublyBoundedFastTC(step/2, isStoreTarget/1, isReadSource/1)(node1, node2)

bindingset[node2, c]
pragma[inline_late]
private predicate storeStepCand(NodeEx node1, Content c, NodeEx node2) {
storeStepCand(node1, _, c, node2, _, _)
}

pragma[nomagic]
predicate storeReachesReadOut(NodeEx node1, NodeEx node2) {
exists(Content c, NodeEx storeTarget, NodeEx readSource |
storeReachesReadTc(MkNodeAndAp(storeTarget, _), MkNodeAndAp(readSource, _)) and
storeStepCand(node1, _, c, storeTarget, _, _) and
storeReachesReadTc(storeTarget, readSource) and
storeStepCand(node1, c, storeTarget) and
readStepCand(readSource, c, node2)
)
or
exists(Content c, NodeEx storeTargetReadSource |
storeStepCand(node1, c, storeTargetReadSource) and
readStepCand(storeTargetReadSource, c, node2)
)
}
}

Expand Down

0 comments on commit 8f901da

Please sign in to comment.