wip

Author: hvitved

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

@@ -1068,6 +1068,17 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
       }
     }
 
+    private newtype TNodeAndBoolean = MkNodeAndBoolean(NodeEx n, Boolean b) { Stage1::revFlow(n) }
+
+    /** A `NodeEx` tagged with a `Boolean`. */
+    private class NodeAndBoolean extends TNodeAndBoolean {
+      NodeEx getNodeEx() { this = MkNodeAndBoolean(result, _) }
+
+      boolean getBoolean() { this = MkNodeAndBoolean(_, result) }
+
+      string toString() { result = this.getNodeEx().toString() + " " + this.getBoolean() }
+    }
+
     private predicate sinkNode = Stage1::sinkNode/2;
 
     private predicate sourceModel(NodeEx node, string model) {
@@ -2551,16 +2562,23 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
           /** Input from previous iteration. */
           private signature predicate storeReachesReadSig(NodeEx node1, NodeEx node2);
 
-          private module StoreReachesRead<storeReachesReadSig/2 storeReachesReadIn> {
+          private module StoreReachesRead<
+            storeReachesReadSig/2 storeReachesReadPrevDelta,
+            storeReachesReadSig/2 storeReachesReadPrevPrev>
+          {
             pragma[nomagic]
-            private predicate step(NodeEx node1, NodeEx node2) {
-              valueStep(node1, node2)
+            private predicate step(NodeEx node1, NodeEx node2, boolean usesPrevDelta) {
+              valueStep(node1, node2) and
+              usesPrevDelta = false
               or
               exists(FlowState state, Ap ap |
                 revFlow(node1, pragma[only_bind_into](state), _, _, pragma[only_bind_into](ap)) and
                 revFlow(node2, pragma[only_bind_into](state), _, _, pragma[only_bind_into](ap)) and
-                not ap instanceof ApNil and
-                storeReachesReadIn(node1, node2)
+                not ap instanceof ApNil
+              |
+                storeReachesReadPrevDelta(node1, node2) and usesPrevDelta = true
+                or
+                storeReachesReadPrevPrev(node1, node2) and usesPrevDelta = false
               )
             }
 
@@ -2573,7 +2591,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
             }
 
             private predicate stepNodeOrContent(ContentOrNodeContent n1, ContentOrNodeContent n2) {
-              step(n1.asNodeEx(), n2.asNodeEx())
+              step(n1.asNodeEx(), n2.asNodeEx(), _)
               or
               storeStepCand0(_, _, n1.asContent(), n2.asNodeEx(), _, _)
               or
@@ -2599,68 +2617,117 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
               )
             }
 
-            private predicate isStoreTarget(NodeEx node) {
+            private predicate isStoreTarget(NodeAndBoolean node) {
               exists(Content c |
                 contentIsReadAndStored(c) and
-                storeStepCand0(_, _, c, node, _, _)
+                storeStepCand0(_, _, c, node.getNodeEx(), _, _) and
+                node.getBoolean() = false
               )
             }
 
-            private predicate isReadSource(NodeEx node) {
+            private predicate isReadSource(NodeAndBoolean node) {
               exists(Content c |
                 contentIsReadAndStored(c) and
-                readStepCand0(node, c, _)
+                readStepCand0(node.getNodeEx(), c, _) and
+                node.getBoolean() = true
               )
             }
 
-            private predicate storeReachesReadTc(NodeEx node1, NodeEx node2) =
-              doublyBoundedFastTC(step/2, isStoreTarget/1, isReadSource/1)(node1, node2)
+            pragma[nomagic]
+            private predicate step0(NodeAndBoolean node1, NodeAndBoolean node2) {
+              exists(boolean usesPrevDelta |
+                step(node1.getNodeEx(), node2.getNodeEx(), usesPrevDelta)
+              |
+                node2.getBoolean() = node1.getBoolean().booleanOr(usesPrevDelta)
+              )
+            }
+
+            private predicate storeReachesReadTc(NodeAndBoolean node1, NodeAndBoolean node2) =
+              doublyBoundedFastTC(step0/2, isStoreTarget/1, isReadSource/1)(node1, node2)
 
             pragma[nomagic]
-            private predicate storeStepCandIsReadAndStored(NodeEx node1, Content c, NodeEx node2) {
+            private predicate storeStepCandIsReadAndStored(
+              NodeEx node1, Content c, NodeAndBoolean node2
+            ) {
               contentIsReadAndStored(c) and
-              storeStepCand0(node1, _, c, node2, _, _)
+              storeStepCand0(node1, _, c, node2.getNodeEx(), _, _) and
+              node2.getBoolean() = false
             }
 
             pragma[nomagic]
-            private predicate readStepCandIsReadAndStored(NodeEx node1, Content c, NodeEx node2) {
+            private predicate readStepCandIsReadAndStored(
+              NodeAndBoolean node1, Content c, NodeEx node2
+            ) {
               contentIsReadAndStored(c) and
-              readStepCand0(node1, c, node2)
+              readStepCand0(node1.getNodeEx(), c, node2) and
+              node1.getBoolean() = true
             }
 
             pragma[nomagic]
-            predicate storeReachesReadOut(NodeEx storeSource, NodeEx readTarget) {
-              exists(Content c, NodeEx storeTarget, NodeEx readSource |
+            predicate storeReachesReadPrev(NodeEx storeSource, NodeEx readTarget) {
+              storeReachesReadPrevDelta(storeSource, readTarget)
+              or
+              storeReachesReadPrevPrev(storeSource, readTarget)
+            }
+
+            pragma[nomagic]
+            predicate storeReachesReadDelta(NodeEx storeSource, NodeEx readTarget) {
+              exists(Content c, NodeAndBoolean storeTarget, NodeAndBoolean readSource |
                 storeReachesReadTc(storeTarget, readSource) and
                 storeStepCandIsReadAndStored(storeSource, c, storeTarget) and
                 readStepCandIsReadAndStored(readSource, c, readTarget)
               )
-              or
-              exists(Content c, NodeEx storeTargetReadSource |
-                storeStepCandIsReadAndStored(storeSource, c, storeTargetReadSource) and
-                readStepCandIsReadAndStored(storeTargetReadSource, c, readTarget)
-              )
             }
           }
 
-          private predicate storeReachesRead0(NodeEx node1, NodeEx node2) { none() }
+          private predicate storeReachesReadPrevDelta0(NodeEx node1, NodeEx node2) { node1 = node2 }
+
+          private predicate storeReachesReadPrevPrev0(NodeEx node1, NodeEx node2) { none() }
+
+          private module StoreReachesRead1 =
+            StoreReachesRead<storeReachesReadPrevDelta0/2, storeReachesReadPrevPrev0/2>;
+
+          private predicate storeReachesReadPrevDelta1(NodeEx storeSource, NodeEx readTarget) {
+            StoreReachesRead1::storeReachesReadDelta(storeSource, readTarget)
+            or
+            exists(Content c, NodeEx storeTargetReadSource |
+              StoreReachesRead1::contentIsReadAndStored(c) and
+              storeStepCand0(storeSource, _, c, storeTargetReadSource, _, _) and
+              readStepCand0(storeTargetReadSource, c, readTarget)
+            )
+          }
 
-          private predicate storeReachesRead1 =
-            StoreReachesRead<storeReachesRead0/2>::storeReachesReadOut/2;
+          private predicate storeReachesReadPrevPrev1(NodeEx storeSource, NodeEx readTarget) {
+            none()
+          }
 
-          private predicate storeReachesRead2 =
-            StoreReachesRead<storeReachesRead1/2>::storeReachesReadOut/2;
+          private module StoreReachesRead2 =
+            StoreReachesRead<storeReachesReadPrevDelta1/2, storeReachesReadPrevPrev1/2>;
 
-          private predicate storeReachesRead3 =
-            StoreReachesRead<storeReachesRead2/2>::storeReachesReadOut/2;
+          private predicate storeReachesReadPrevDelta2 = StoreReachesRead2::storeReachesReadDelta/2;
 
-          private predicate storeReachesRead4 =
-            StoreReachesRead<storeReachesRead3/2>::storeReachesReadOut/2;
+          private predicate storeReachesReadPrevPrev2 = StoreReachesRead2::storeReachesReadPrev/2;
+
+          private module StoreReachesRead3 =
+            StoreReachesRead<storeReachesReadPrevDelta2/2, storeReachesReadPrevPrev2/2>;
+
+          private predicate storeReachesReadPrevDelta3 = StoreReachesRead3::storeReachesReadDelta/2;
+
+          private predicate storeReachesReadPrevPrev3 = StoreReachesRead3::storeReachesReadPrev/2;
+
+          private module StoreReachesRead4 =
+            StoreReachesRead<storeReachesReadPrevDelta3/2, storeReachesReadPrevPrev3/2>;
+
+          predicate storeReachesRead(NodeEx storeSource, NodeEx readTarget) {
+            StoreReachesRead4::storeReachesReadDelta(storeSource, readTarget)
+            or
+            StoreReachesRead4::storeReachesReadPrev(storeSource, readTarget)
+          }
 
-          import StoreReachesRead<storeReachesRead4/2>
+          predicate contentIsReadAndStored = StoreReachesRead4::contentIsReadAndStored/1;
         }
 
-        predicate storeReachesRead = StoreReadReachability::storeReachesReadOut/2;
+        predicate storeReachesRead = StoreReadReachability::storeReachesRead/2;
 
         pragma[nomagic]
         predicate storeStepCand(