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)
           )
         }
 
@@ -2487,6 +2500,77 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
           callEdgeReturn(call, c, _, _, _, _, _)
         }
 
+        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))
+            |
+              localStep(node1, state1, node2, state2, true, _, _)
+              or
+              jumpStepEx(node1, node2)
+              or
+              callEdgeArgParam(_, _, node1, node2, _, _)
+              or
+              callEdgeReturn(_, _, node1, _, node2, _, _)
+              or
+              storeReachesReadIn(node1, node2)
+            )
+          }
+
+          private predicate isStoreTarget(TNodeAndAp n) {
+            exists(NodeEx node, Ap ap |
+              n = MkNodeAndAp(node, ap) and
+              storeStepCand(_, _, _, node, _, _)
+            )
+          }
+
+          private predicate isReadSource(TNodeAndAp n) {
+            exists(NodeEx node, Ap ap |
+              n = MkNodeAndAp(node, ap) and
+              readStepCand(node, _, _)
+            )
+          }
+
+          private predicate storeReachesReadTc(TNodeAndAp node1, TNodeAndAp node2) =
+            doublyBoundedFastTC(step/2, isStoreTarget/1, isReadSource/1)(node1, 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
+              readStepCand(readSource, 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