From 927d3e24e466e56bef1078efb4e8c90a0c5c5b0b Mon Sep 17 00:00:00 2001 From: Tom Hvitved Date: Fri, 14 Jun 2024 09:07:03 +0200 Subject: [PATCH] wip2 --- shared/dataflow/codeql/dataflow/DataFlow.qll | 5 +- .../codeql/dataflow/internal/DataFlowImpl.qll | 62 +++++++++++++++---- 2 files changed, 52 insertions(+), 15 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/DataFlow.qll b/shared/dataflow/codeql/dataflow/DataFlow.qll index e2b6be22536f0..e2f7ae4484214 100644 --- a/shared/dataflow/codeql/dataflow/DataFlow.qll +++ b/shared/dataflow/codeql/dataflow/DataFlow.qll @@ -276,6 +276,7 @@ signature module InputSig { */ predicate isUnreachableInCall(NodeRegion nr, DataFlowCall call); + /** Gets the access path limit. A maximum limit of 5 is allowed. */ default int accessPathLimit() { result = 5 } /** @@ -412,7 +413,7 @@ module Configs Lang> { */ default int fieldFlowBranchLimit() { result = 2 } - /** Gets the access path limit. */ + /** Gets the access path limit. A maximum limit of 5 is allowed. */ default int accessPathLimit() { result = Lang::accessPathLimit() } /** @@ -534,7 +535,7 @@ module Configs Lang> { */ default int fieldFlowBranchLimit() { result = 2 } - /** Gets the access path limit. */ + /** Gets the access path limit. A maximum limit of 5 is allowed. */ default int accessPathLimit() { result = Lang::accessPathLimit() } /** diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index ef70d8449738b..cb6f5c82def56 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -94,7 +94,7 @@ module MakeImpl Lang> { */ int fieldFlowBranchLimit(); - /** Gets the access path limit. */ + /** Gets the access path limit. A maximum limit of 5 is allowed. */ int accessPathLimit(); /** @@ -2562,10 +2562,15 @@ module MakeImpl Lang> { /** Input from previous iteration. */ private signature predicate storeReachesReadSig(NodeEx node1, NodeEx node2); + private signature int iterationSig(); + private module StoreReachesRead< storeReachesReadSig/2 storeReachesReadPrevDelta, - storeReachesReadSig/2 storeReachesReadPrevPrev> + storeReachesReadSig/2 storeReachesReadPrevPrev, iterationSig/0 iteration> { + private predicate enabled() { Config::accessPathLimit() > iteration() } + + // private predicate enabled() { any() } pragma[nomagic] private predicate step(NodeEx node1, NodeEx node2, boolean usesPrevDelta) { valueStep(node1, node2) and @@ -2591,7 +2596,9 @@ module MakeImpl Lang> { } private predicate stepNodeOrContent(ContentOrNodeContent n1, ContentOrNodeContent n2) { - step(n1.asNodeEx(), n2.asNodeEx(), _) + exists(boolean usesPrevDelta | step(n1.asNodeEx(), n2.asNodeEx(), usesPrevDelta) | + usesPrevDelta = false or enabled() + ) or storeStepCand0(_, _, n1.asContent(), n2.asNodeEx(), _, _) or @@ -2618,6 +2625,7 @@ module MakeImpl Lang> { } private predicate isStoreTarget(NodeAndBoolean node) { + enabled() and exists(Content c | contentIsReadAndStored(c) and storeStepCand0(_, _, c, node.getNodeEx(), _, _) and @@ -2625,16 +2633,25 @@ module MakeImpl Lang> { ) } + private boolean mustUsePrevDelta() { + exists(int iteration | + iteration = iteration() and + if iteration > 0 then result = true else result = false + ) + } + private predicate isReadSource(NodeAndBoolean node) { + enabled() and exists(Content c | contentIsReadAndStored(c) and readStepCand0(node.getNodeEx(), c, _) and - node.getBoolean() = true + node.getBoolean() = mustUsePrevDelta() ) } pragma[nomagic] private predicate step0(NodeAndBoolean node1, NodeAndBoolean node2) { + enabled() and exists(boolean usesPrevDelta | step(node1.getNodeEx(), node2.getNodeEx(), usesPrevDelta) | @@ -2649,6 +2666,7 @@ module MakeImpl Lang> { private predicate storeStepCandIsReadAndStored( NodeEx node1, Content c, NodeAndBoolean node2 ) { + enabled() and contentIsReadAndStored(c) and storeStepCand0(node1, _, c, node2.getNodeEx(), _, _) and node2.getBoolean() = false @@ -2658,9 +2676,10 @@ module MakeImpl Lang> { private predicate readStepCandIsReadAndStored( NodeAndBoolean node1, Content c, NodeEx node2 ) { + enabled() and contentIsReadAndStored(c) and readStepCand0(node1.getNodeEx(), c, node2) and - node1.getBoolean() = true + node1.getBoolean() = mustUsePrevDelta() } pragma[nomagic] @@ -2680,12 +2699,14 @@ module MakeImpl Lang> { } } - private predicate storeReachesReadPrevDelta0(NodeEx node1, NodeEx node2) { node1 = node2 } + private predicate storeReachesReadPrevDelta0(NodeEx node1, NodeEx node2) { none() } private predicate storeReachesReadPrevPrev0(NodeEx node1, NodeEx node2) { none() } + private int iteration0() { result = 0 } + private module StoreReachesRead1 = - StoreReachesRead; + StoreReachesRead; private predicate storeReachesReadPrevDelta1(NodeEx storeSource, NodeEx readTarget) { StoreReachesRead1::storeReachesReadDelta(storeSource, readTarget) @@ -2701,30 +2722,45 @@ module MakeImpl Lang> { none() } + private int iteration1() { result = 1 } + private module StoreReachesRead2 = - StoreReachesRead; + StoreReachesRead; private predicate storeReachesReadPrevDelta2 = StoreReachesRead2::storeReachesReadDelta/2; private predicate storeReachesReadPrevPrev2 = StoreReachesRead2::storeReachesReadPrev/2; + private int iteration2() { result = 2 } + private module StoreReachesRead3 = - StoreReachesRead; + StoreReachesRead; private predicate storeReachesReadPrevDelta3 = StoreReachesRead3::storeReachesReadDelta/2; private predicate storeReachesReadPrevPrev3 = StoreReachesRead3::storeReachesReadPrev/2; + private int iteration3() { result = 3 } + private module StoreReachesRead4 = - StoreReachesRead; + StoreReachesRead; + + private predicate storeReachesReadPrevDelta4 = StoreReachesRead4::storeReachesReadDelta/2; + + private predicate storeReachesReadPrevPrev4 = StoreReachesRead4::storeReachesReadPrev/2; + + private int iteration4() { result = 4 } + + private module StoreReachesRead5 = + StoreReachesRead; predicate storeReachesRead(NodeEx storeSource, NodeEx readTarget) { - StoreReachesRead4::storeReachesReadDelta(storeSource, readTarget) + StoreReachesRead5::storeReachesReadDelta(storeSource, readTarget) or - StoreReachesRead4::storeReachesReadPrev(storeSource, readTarget) + StoreReachesRead5::storeReachesReadPrev(storeSource, readTarget) } - predicate contentIsReadAndStored = StoreReachesRead4::contentIsReadAndStored/1; + predicate contentIsReadAndStored = StoreReachesRead5::contentIsReadAndStored/1; } predicate storeReachesRead = StoreReadReachability::storeReachesRead/2;