From 8f901daea68cf6d2376ef8f92f45a9afaebb014e Mon Sep 17 00:00:00 2001 From: Tom Hvitved Date: Wed, 12 Jun 2024 16:53:07 +0200 Subject: [PATCH] temp --- .../codeql/dataflow/internal/DataFlowImpl.qll | 63 +++++++++---------- 1 file changed, 31 insertions(+), 32 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index 4b1a2e23a1898..8aaef06aa399f 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -2170,9 +2170,10 @@ module MakeImpl 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 @@ -2238,11 +2239,11 @@ module MakeImpl 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) ) } @@ -2370,7 +2371,7 @@ module MakeImpl 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) ) } @@ -2397,7 +2398,7 @@ module MakeImpl 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) ) } @@ -2502,18 +2503,15 @@ module MakeImpl Lang> { private signature predicate storeReachesReadSig(NodeEx node1, NodeEx node2); - private newtype TNodeAndAp = MkNodeAndAp(TNodeEx node, Ap ap) { revFlow(node, _, _, _, ap) } - private module StoreReachesRead { 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 @@ -2525,30 +2523,31 @@ module MakeImpl 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) + ) } }