Data flow: Experiment

Author: hvitved

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

@@ -1019,6 +1019,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
         callEdgeReturn(call, c, _, _, _, _, _)
       }
 
+      bindingset[node1, node2]
+      predicate storeReachesRead(NodeEx node1, NodeEx node2) {
+        exists(node1) and
+        exists(node2)
+      }
+
       additional predicate stats(
         boolean fwd, int nodes, int fields, int conscand, int states, int tuples, int calledges
       ) {
@@ -1314,6 +1320,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
       predicate relevantCallEdgeIn(DataFlowCall call, DataFlowCallable c);
 
       predicate relevantCallEdgeOut(DataFlowCall call, DataFlowCallable c);
+
+      bindingset[node1, node2]
+      predicate storeReachesRead(NodeEx node1, NodeEx node2);
     }
 
     private module MkStage<StageSig PrevStage> {
@@ -1512,9 +1521,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
           )
           or
           // read
-          exists(Typ t0, Ap ap0, Content c |
+          exists(Typ t0, Ap ap0, Content c, NodeEx storeSource |
             fwdFlowRead(t0, ap0, c, _, node, state, cc, summaryCtx, argT, argAp) and
-            fwdFlowConsCand(t0, ap0, c, t, ap) and
+            fwdFlowConsCand(storeSource, t0, ap0, c, t, ap) and
+            PrevStage::storeReachesRead(storeSource, node) and
             apa = getApprox(ap)
           )
           or
@@ -1583,16 +1593,18 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
         /**
          * Holds if forward flow with access path `tail` and type `t1` reaches a
          * store of `c` on a container of type `t2` resulting in access path
-         * `cons`.
+         * `cons`. `storeSource` is a node that may be stored into `c`.
          */
         pragma[nomagic]
-        private predicate fwdFlowConsCand(Typ t2, Ap cons, Content c, Typ t1, Ap tail) {
-          fwdFlowStore(_, t1, tail, c, t2, _, _, _, _, _, _) and
+        private predicate fwdFlowConsCand(
+          NodeEx storeSource, Typ t2, Ap cons, Content c, Typ t1, Ap tail
+        ) {
+          fwdFlowStore(storeSource, t1, tail, c, t2, _, _, _, _, _, _) and
           cons = apCons(c, t1, tail)
           or
           exists(Typ t0 |
             typeStrengthen(t0, cons, t2) and
-            fwdFlowConsCand(t0, cons, c, t1, tail)
+            fwdFlowConsCand(storeSource, t0, cons, c, t1, tail)
           )
         }
 
@@ -2041,9 +2053,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
 
         pragma[nomagic]
         private predicate readStepFwd(NodeEx n1, Ap ap1, Content c, NodeEx n2, Ap ap2) {
-          exists(Typ t1 |
+          exists(Typ t1, NodeEx storeSource |
             fwdFlowRead(t1, ap1, c, n1, n2, _, _, _, _, _) and
-            fwdFlowConsCand(t1, ap1, c, _, ap2)
+            fwdFlowConsCand(storeSource, t1, ap1, c, _, ap2) and
+            PrevStage::storeReachesRead(storeSource, n2)
           )
         }
 
@@ -2157,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
@@ -2225,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)
           )
         }
 
@@ -2357,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)
           )
         }
 
@@ -2384,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)
           )
         }
 
@@ -2487,6 +2501,75 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
           callEdgeReturn(call, c, _, _, _, _, _)
         }
 
+        private signature predicate storeReachesReadSig(NodeEx node1, NodeEx node2);
+
+        private module StoreReachesRead<storeReachesReadSig/2 storeReachesReadIn> {
+          pragma[nomagic]
+          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, state, node2, state, true, _, _) and
+              returnAp1 = returnAp2
+              or
+              jumpStepEx(node1, node2)
+              or
+              callEdgeArgParam(_, _, node1, node2, _, _)
+              or
+              callEdgeReturn(_, _, node1, _, node2, _, _)
+              or
+              storeReachesReadIn(node1, node2)
+            )
+          }
+
+          private predicate isStoreTarget(NodeEx node) { storeStepCand(_, _, _, node, _, _) }
+
+          private predicate isReadSource(NodeEx node) { readStepCand(node, _, _) }
+
+          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(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)
+            )
+          }
+        }
+
+        private predicate storeReachesRead0(NodeEx node1, NodeEx node2) { none() }
+
+        private predicate storeReachesRead1 =
+          StoreReachesRead<storeReachesRead0/2>::storeReachesReadOut/2;
+
+        private predicate storeReachesRead2 =
+          StoreReachesRead<storeReachesRead1/2>::storeReachesReadOut/2;
+
+        private predicate storeReachesRead3 =
+          StoreReachesRead<storeReachesRead2/2>::storeReachesReadOut/2;
+
+        private predicate storeReachesRead4 =
+          StoreReachesRead<storeReachesRead3/2>::storeReachesReadOut/2;
+
+        private predicate storeReachesRead5 =
+          StoreReachesRead<storeReachesRead4/2>::storeReachesReadOut/2;
+
+        predicate storeReachesRead = storeReachesRead5/2;
+
         additional predicate stats(
           boolean fwd, int nodes, int fields, int conscand, int states, int tuples, int calledges,
           int tfnodes, int tftuples