wip3

Author: hvitved

shared/dataflow/codeql/dataflow/internal/FlowSummaryImpl.qll

@@ -1295,7 +1295,7 @@ module Make<
     }
 
     pragma[nomagic]
-    private predicate sourceOutputStateComplete(
+    private predicate sourceOutputStateEntry(
       SourceElement source, SummaryComponentStack s, string kind, string model
     ) {
       exists(string outSpec |
@@ -1309,13 +1309,13 @@ module Make<
       SourceElement source, SummaryComponentStack s, string kind, string model
     ) {
       exists(SummaryComponentStack exit |
-        sourceOutputStateComplete(source, exit, kind, model) and
+        sourceOutputStateEntry(source, exit, kind, model) and
         s = exit.drop(_)
       )
     }
 
     pragma[nomagic]
-    private predicate sinkInputStateComplete(
+    private predicate sinkInputStateEntry(
       SinkElement sink, SummaryComponentStack s, string kind, string model
     ) {
       exists(string inSpec |
@@ -1329,7 +1329,7 @@ module Make<
       SinkElement sink, SummaryComponentStack s, string kind, string model
     ) {
       exists(SummaryComponentStack entry |
-        sinkInputStateComplete(sink, entry, kind, model) and
+        sinkInputStateEntry(sink, entry, kind, model) and
         s = entry.drop(_)
       )
     }
@@ -1507,7 +1507,7 @@ module Make<
       ) {
         exists(SummaryComponentStack complete, SummaryComponentStack stack |
           state.isSourceOutputState(source, stack, kind, model) and
-          sourceOutputStateComplete(source, complete, kind, model) and
+          sourceOutputStateEntry(source, complete, kind, model) and
           stack =
             min(SummaryComponentStack stack0, int i |
               stack0 = complete.drop(i) and
@@ -1555,15 +1555,6 @@ module Make<
         )
       }
 
-      private predicate sourceOutputNode(
-        SourceElement source, SummaryNodeState state, SourceSinkReportingElement e, string kind,
-        string model
-      ) {
-        sourceOutputStepNode(source, state, e, kind, model)
-        or
-        sourceOutputStoreNode(source, state, e, kind, model)
-      }
-
       /**
        * For a sink access path like
        *
@@ -1584,7 +1575,7 @@ module Make<
       ) {
         exists(SummaryComponentStack complete, SummaryComponentStack stack |
           state.isSinkInputState(sink, stack, kind, model) and
-          sinkInputStateComplete(sink, complete, kind, model) and
+          sinkInputStateEntry(sink, complete, kind, model) and
           stack =
             max(SummaryComponentStack stack0, int i |
               stack0 = complete.drop(i) and
@@ -1633,15 +1624,6 @@ module Make<
         )
       }
 
-      private predicate sinkInputNode(
-        SinkElement sink, SummaryNodeState state, SourceSinkReportingElement e, string kind,
-        string model
-      ) {
-        sinkInputStepNode(sink, state, e, kind, model)
-        or
-        sinkInputReadNode(sink, state, e, kind, model)
-      }
-
       private newtype TSummaryNode =
         TSummaryInternalNode(SummarizedCallable c, SummaryNodeState state) {
           summaryNodeRange(c, state)
@@ -1659,13 +1641,17 @@ module Make<
           SourceElement source, SummaryNodeState state, SourceSinkReportingElement e, string kind,
           string model
         ) {
-          sourceOutputNode(source, state, e, kind, model)
+          sourceOutputStepNode(source, state, e, kind, model)
+          or
+          sourceOutputStoreNode(source, state, e, kind, model)
         } or
         TSinkInputNode(
           SinkElement sink, SummaryNodeState state, SourceSinkReportingElement e, string kind,
           string model
         ) {
-          sinkInputNode(sink, state, e, kind, model)
+          sinkInputStepNode(sink, state, e, kind, model)
+          or
+          sinkInputReadNode(sink, state, e, kind, model)
         }
 
       abstract class SummaryNode extends TSummaryNode {
@@ -1774,42 +1760,33 @@ module Make<
         SourceOutputNode() { this = TSourceOutputNode(source_, state_, e_, kind_, model_) }
 
         /**
-         * Holds if this node is an entry node, i.e. before any stores have been performed.
+         * Holds if this node is an entry node, i.e. before any stores or steps have been
+         * performed.
          *
          * This node should be used as the actual source node in data flow configurations.
          */
         predicate isEntry(string kind, string model) {
           model = model_ and
-          exists(SummaryComponentStack out |
-            state_.isSourceOutputState(source_, out, kind, model_) and
-            sourceOutputStateComplete(source_, out, kind, model_)
+          exists(SummaryComponentStack stack |
+            state_.isSourceOutputState(source_, stack, kind, model_) and
+            sourceOutputStateEntry(source_, stack, kind, model_)
           )
         }
 
         /**
-         * Holds if this node is an exit node, i.e. after all stores have been performed.
+         * Holds if this node is an exit node, i.e. after all stores and steps have been
+         * performed.
          *
-         * A local flow step should be added from this node to a data flow node representing
-         * `s` inside `source`.
+         * A flow step is added from this node to a data flow node representing
+         * `s` inside `source`, using `getSourceExitNode`.
          */
         predicate isExit(
           SourceElement source, SummaryComponent sc, SourceSinkReportingElement e, string model
         ) {
-          exists(SummaryComponentStack stack |
-            source = source_ and
-            model = model_ and
-            state_.isSourceOutputState(source, stack, _, model) and
-            e = e_ and
-            stack = TSingletonSummaryComponentStack(sc)
-            // sourceOutputStateExit(source, stack, kind_, model) and
-            // sc =
-            //   min(SummaryComponent sc0, int i |
-            //     sc0 = stack.drop(i).head() and
-            //     not sc0 instanceof TContentSummaryComponent
-            //   |
-            //     sc0 order by i
-            //   )
-          )
+          source = source_ and
+          model = model_ and
+          state_.isSourceOutputState(source, TSingletonSummaryComponentStack(sc), _, model) and
+          e = e_
         }
 
         override predicate isHidden() {
@@ -1849,10 +1826,11 @@ module Make<
         SinkInputNode() { this = TSinkInputNode(sink_, state_, e_, kind_, model_) }
 
         /**
-         * Holds if this node is an entry node, i.e. before any reads have been performed.
+         * Holds if this node is an entry node, i.e. before any reads and steps have been
+         * performed.
          *
-         * A local flow step should be added to this node from a data flow node representing
-         * `sc` inside `sink`.
+         * A flow step is added to this node from a data flow node representing
+         * `sc` inside `sink`, using `getSinkEntryNode`.
          */
         predicate isEntry(
           SinkElement sink, SummaryComponent sc, SourceSinkReportingElement e, string model
@@ -1861,20 +1839,15 @@ module Make<
           model = model_ and
           e = e_ and
           exists(SummaryComponentStack stack |
-            sinkInputStateComplete(sink, stack, kind_, model) and
+            sinkInputStateEntry(sink, stack, kind_, model) and
             state_.isSinkInputState(sink, stack, _, model) and
             sc = stack.head()
-            // min(SummaryComponent sc0, int i |
-            //   sc0 = stack.drop(i).head() and
-            //   not sc0 instanceof TContentSummaryComponent
-            // |
-            //   sc0 order by i
-            // )
           )
         }
 
         /**
-         * Holds if this node is an exit node, i.e. after all reads have been performed.
+         * Holds if this node is an exit node, i.e. after all reads and steps have been
+         * performed.
          *
          * This node should be used as the actual sink node in data flow configurations.
          */
@@ -2306,15 +2279,9 @@ module Make<
           or
           exists(SummaryNode succSummary |
             succSummary = StepsInput::getSummaryNode(succ) and
+            sinkEntryStep(pred, succSummary, true) and
             preservesValue = true and
             model = ""
-          |
-            sinkEntryStep(pred, succSummary, true)
-            // or
-            // exists(SummaryComponent sc, SourceSinkReportingElement e |
-            //   pred = getSinkEntryNode(e, sc) and
-            //   succSummary.(SinkInputNode).isEntry(_, sc, e, _)
-            // )
           )
           or
           exists(FlowSummaryCallBase summaryCall, ReturnKind rk, SummarizedCallable sc |
@@ -2332,37 +2299,38 @@ module Make<
 
         /**
          * Holds if there is a read step of content `c` from `pred` to `succ`, which
-         * is synthesized from a flow summary.
+         * is synthesized from a flow summary or a sink specification.
          */
         predicate summaryReadStep(SummaryNode pred, ContentSet c, SummaryNode succ) {
-          exists(SummarizedCallable sc, SummaryComponentStack s |
-            pred = summaryNodeInputState(sc, s.tail()) and
-            succ = summaryNodeInputState(sc, s) and
-            SummaryComponent::content(c) = s.head()
-          )
-          or
-          exists(SinkElement sink, SourceSinkReportingElement e, SummaryComponentStack s |
-            pred = sinkElementInputState(sink, e, s) and
-            succ = sinkElementInputState(sink, e, s.tail()) and
-            SummaryComponent::content(c) = s.tail().head() // todo
+          exists(SummaryComponentStack stack | SummaryComponent::content(c) = stack.head() |
+            exists(SummarizedCallable sc |
+              pred = summaryNodeInputState(sc, stack.tail()) and
+              succ = summaryNodeInputState(sc, stack)
+            )
+            or
+            exists(SinkElement sink, SourceSinkReportingElement e, SummaryComponentStack stack0 |
+              pred = sinkElementInputState(sink, e, stack0) and
+              stack = stack0.tail() and
+              succ = sinkElementInputState(sink, e, stack)
+            )
           )
         }
 
         /**
          * Holds if there is a store step of content `c` from `pred` to `succ`, which
-         * is synthesized from a flow summary.
+         * is synthesized from a flow summary or a source specification.
          */
         predicate summaryStoreStep(SummaryNode pred, ContentSet c, SummaryNode succ) {
-          exists(SummarizedCallable sc, SummaryComponentStack s |
-            pred = summaryNodeOutputState(sc, s) and
-            succ = summaryNodeOutputState(sc, s.tail()) and
-            SummaryComponent::content(c) = s.head()
-          )
-          or
-          exists(SourceElement source, SourceSinkReportingElement e, SummaryComponentStack s |
-            pred = sourceElementOutputState(source, e, s) and
-            succ = sourceElementOutputState(source, e, s.tail()) and
-            SummaryComponent::content(c) = s.head()
+          exists(SummaryComponentStack stack | SummaryComponent::content(c) = stack.head() |
+            exists(SummarizedCallable sc |
+              pred = summaryNodeOutputState(sc, stack) and
+              succ = summaryNodeOutputState(sc, stack.tail())
+            )
+            or
+            exists(SourceElement source, SourceSinkReportingElement e |
+              pred = sourceElementOutputState(source, e, stack) and
+              succ = sourceElementOutputState(source, e, stack.tail())
+            )
           )
         }
 
@@ -2390,7 +2358,7 @@ module Make<
                 succSummary = TSourceOutputNode(source, state, e, kind, model)
               )
               or
-              // We model all non-store steps as jumps in order to ensure that they are not stepped
+              // We model all non-read steps as jumps in order to ensure that they are not stepped
               // over in the path graph.
               exists(
                 SinkElement sink, string kind, SummaryNodeState state, SummaryNodeState state0,