asgerf · Oct 12, 2026 · Oct 12, 2026 · Oct 15, 2026 · Oct 12, 2026 · Oct 12, 2026
@@ -12,6 +12,11 @@ module ConsistencyInput implements InputSig<Location, DataFlowInput> {
     // have post-update nodes for reverse-reads.
     any(DataFlowPlugin p).step(n, any(Step s | s.read(_)), _)
   }
+
+  predicate postWithInFlowExclude(DataFlow::Node n) {
+    // In summaries, 'inout' parameters result in flow directly into the post-update node for an argument
+    n instanceof TSummaryNode
+  }
 }
 
 module ConsistencyOutput =

@@ -10,6 +10,7 @@ import DataFlowGraph
 import DataFlowInstantiation
 import DataFlowNode
 import DataFlowPlugin
+import FlowSummary
 import LocalSsa
 import ParameterPositions
 import Step

@@ -4,4 +4,6 @@ private import codeql.unified.internal.typeinference.TypeInference as T
 
 DataFlowCallable viableCallable(DataFlowCall c) {
   result.asSourceCallable() = T::resolveCallTarget(c.asExplicitCall())
+  or
+  result.asSummarizedCallable().matchesCall(c.asExplicitCall())
 }
@@ -1,6 +1,13 @@
 private import unified
 private import AllDataFlow
 
+/**
+ * Holds if a MaD access path token of form `name[arg]` exists.
+ */
+predicate isAccessPathTokenPresent(string name, string arg) {
+  arg = any(FlowSummaryOutput::Private::AccessPathToken tok).getAnArgument(name)
+}
+
 private newtype TContent =
   TArrayElement() or
   TNamedMember(string name) {
@@ -11,6 +18,8 @@ private newtype TContent =
     name = [0 .. 20].toString()
     or
     name = getEnumCaseParameterFieldFromArgument(_, _)
+    or
+    isAccessPathTokenPresent("Member", name)
   } or
   TCapturedVariable(CaptureSsaInput::CapturedVariable v)
 

@@ -5,6 +5,9 @@ private import codeql.unified.internal.ExprPositions
 private newtype TDataFlowCall =
   TExplicitCall(CallExpr call) {
     not isInBindingContext(call, _) // ignore constructor patterns
+  } or
+  TSummaryCall(SummarizedCallable callable, SummaryNode callee) {
+    FlowSummaryOutput::summaryCallbackRange(callable, callee)
   }
 
 /**
@@ -17,15 +20,33 @@ class DataFlowCall extends TDataFlowCall {
   /** Gets the `CallExpr` wrapped by this dataflow call, if any. */
   CallExpr asExplicitCall() { this = TExplicitCall(result) }
 
+  /** Holds if this is a synthesized call to `callee` in `callable`. */
+  predicate isSummaryCall(SummarizedCallable callable, SummaryNode callee) {
+    this = TSummaryCall(callable, callee)
+  }
+
   /** Gets a textual representation of this call. */
-  string toString() { result = this.asExplicitCall().toString() }
+  string toString() {
+    result = this.asExplicitCall().toString()
+    or
+    exists(SummarizedCallable callable, SummaryNode callee |
+      this.isSummaryCall(callable, callee) and
+      result = "[summary] call to " + callee.toString() + " in " + callable.toString()
+    )
+  }
 
   /** Gets the location of this call, if any. */
-  Location getLocation() { result = this.asExplicitCall().getLocation() }
+  Location getLocation() {
+    result = this.asExplicitCall().getLocation()
+    or
+    this.isSummaryCall(_, _) and result instanceof EmptyLocation
+  }
 
   /** Gets the callable containing this call. */
   DataFlowCallable getEnclosingCallable() {
     result.asSourceCallable() = this.asExplicitCall().getEnclosingCallable()
+    or
+    this.isSummaryCall(result.asSummarizedCallable(), _)
   }
 }
 

@@ -3,7 +3,8 @@ private import AllDataFlow
 private import codeql.unified.internal.ExprPositions
 
 private newtype TDataFlowCallable =
-  TSourceCallable(Callable callable) { not isInTypeContext(callable) }
+  TSourceCallable(Callable callable) { not isInTypeContext(callable) } or
+  TSummarizedCallable(SummarizedCallable callable)
 
 /**
  * A callable entity: either a function-like entity in source code or
@@ -15,11 +16,21 @@ class DataFlowCallable extends TDataFlowCallable {
   /** Gets the `Callable` wrapped by this dataflow callable, if any. */
   Callable asSourceCallable() { this = TSourceCallable(result) }
 
+  /** Gets the `SummarizedCallable` wrapped by this dataflow callable, if any. */
+  SummarizedCallable asSummarizedCallable() { this = TSummarizedCallable(result) }
+
   /** Gets a string representation of this call. */
-  string toString() { result = this.asSourceCallable().toString() }
+  string toString() {
+    result = this.asSourceCallable().toString() or
+    result = this.asSummarizedCallable().toString()
+  }
 
   /** Gets the location of this call, if any. */
-  Location getLocation() { result = this.asSourceCallable().getLocation() }
+  Location getLocation() {
+    result = this.asSourceCallable().getLocation()
+    or
+    this instanceof TSummarizedCallable and result instanceof EmptyLocation
+  }
 }
 
 DataFlowCallable toDataFlowCallable(Callable callable) { result.asSourceCallable() = callable }
@@ -5,6 +5,18 @@ private import codeql.unified.internal.LocalNameBinding
 predicate step(BuilderNode node1, Step step, BuilderNode node2) {
   any(DataFlowPlugin p).step(node1, step, node2)
   or
+  exists(Expr expr1, Expr expr2, boolean mustFlow |
+    any(DataFlowPlugin p).exprStep(expr1, expr2, mustFlow)
+  |
+    node1.isResultValue(expr1) and
+    (if mustFlow = true then step.valueMustFlow() else step.value()) and
+    node2.isResultValue(expr2)
+    or
+    node1.isPostUpdate(expr2) and
+    step.value() and
+    node2.isPostUpdate(expr1)
+  )
+  or
   exists(Callable callable |
     node1.isReceiverParameter(callable) and
     step.value() and

@@ -22,20 +22,38 @@ module DataFlowInput implements InputSig<Location> {
   //
   // Parameter, argument, return, and out nodes and their positions/kinds
   //
+  private predicate isReturnNode(Node n, ReturnKind kind) {
+    // TODO: Handle short-hand returns such as `func foo() -> Int { 5 }`
+    n.asExpr() = any(ReturnExpr r).getValue() and kind.isStandardReturnValue()
+    or
+    FlowSummaryOutput::summaryReturnNode(getSummaryNode(n), kind)
+  }
+
   class ReturnNode extends Node {
-    ReturnNode() {
-      // TODO: Handle short-hand returns such as `func foo() -> Int { 5 }`
-      this.asExpr() = any(ReturnExpr r).getValue()
-    }
+    ReturnNode() { isReturnNode(this, _) }
 
-    ReturnKind getKind() { exists(result) }
+    ReturnKind getKind() { isReturnNode(this, result) }
+  }
+
+  private predicate isOutNode(Node n, DataFlowCall call, ReturnKind kind) {
+    n.asExpr() = call.asExplicitCall() and kind.isStandardReturnValue()
+    or
+    exists(FlowSummaryOutput::SummaryNode callee |
+      FlowSummaryOutput::summaryOutNode(callee, getSummaryNode(n), kind) and
+      call.isSummaryCall(_, callee)
+    )
   }
 
   class OutNode extends Node {
-    OutNode() { this.asExpr() instanceof CallExpr }
+    OutNode() { isOutNode(this, _, _) }
   }
 
-  class ReturnKind = Unit;
+  OutNode getAnOutNode(DataFlowCall call, ReturnKind kind) { isOutNode(result, call, kind) }
+
+  class ReturnKind extends Unit {
+    /** Holds if this is the standard return value */
+    predicate isStandardReturnValue() { any() }
+  }
 
   import ParameterPositions
   //
@@ -58,6 +76,9 @@ module DataFlowInput implements InputSig<Location> {
     )
     or
     p.(BuilderNode).isImplicitParameter(c, pos)
+    or
+    FlowSummaryOutput::summaryParameterNode(getSummaryNode(p), pos) and
+    c = p.getEnclosingCallableEx()
   }
 
   class ParameterNode extends Node {
@@ -80,6 +101,11 @@ module DataFlowInput implements InputSig<Location> {
     )
     or
     n.(BuilderNode).isImplicitArgument(call, pos, false)
+    or
+    exists(FlowSummaryOutput::SummaryNode callee |
+      FlowSummaryOutput::summaryArgumentNode(callee, getSummaryNode(n), pos) and
+      call.isSummaryCall(_, callee)
+    )
   }
 
   class ArgumentNode extends Node {
@@ -91,10 +117,6 @@ module DataFlowInput implements InputSig<Location> {
     isArgumentNodeImpl(n, call, pos)
   }
 
-  OutNode getAnOutNode(DataFlowCall call, ReturnKind kind) {
-    result.asExpr() = call.asExplicitCall() and exists(kind)
-  }
-
   //
   // Post-update nodes
   //
@@ -129,6 +151,8 @@ module DataFlowInput implements InputSig<Location> {
   private Step valueStepEx() {
     result.value()
     or
+    result.valueMustFlow()
+    or
     exists(ContentSet contents | bypassContentSet(contents) |
       result.read(contents)
       or
@@ -142,15 +166,29 @@ module DataFlowInput implements InputSig<Location> {
     localSsaStep(node1, node2, _) and model = ""
     or
     captureSsaLocalFlowStep(node1, node2) and model = ""
+    or
+    FlowSummaryOutput::summaryLocalStep(node1, node2, true, model)
+    or
+    model = "" and
+    exists(ContentSet contents | bypassContentSet(contents) |
+      FlowSummaryOutput::summaryReadStep(getSummaryNode(node1), contents, getSummaryNode(node2))
+      or
+      FlowSummaryOutput::summaryStoreStep(getSummaryNode(node1), contents, getSummaryNode(node2))
+    )
   }
 
-  predicate jumpStep(Node node1, Node node2) { step(node1, any(Step s | s.jump()), node2) }
+  predicate jumpStep(Node node1, Node node2) {
+    step(node1, any(Step s | s.jump()), node2) or
+    FlowSummaryOutput::summaryJumpStep(node1, node2)
+  }
 
   predicate readStep(Node node1, ContentSet c, Node node2) {
     (
       step(node1, any(Step s | s.read(c)), node2)
       or
       captureSsaReadStep(node1, c, node2)
+      or
+      FlowSummaryOutput::summaryReadStep(getSummaryNode(node1), c, getSummaryNode(node2))
     ) and
     not bypassContentSet(c)
   }
@@ -160,15 +198,29 @@ module DataFlowInput implements InputSig<Location> {
       step(node1, any(Step s | s.store(c)), node2)
       or
       captureSsaStoreStep(node1, c, node2)
+      or
+      FlowSummaryOutput::summaryStoreStep(getSummaryNode(node1), c, getSummaryNode(node2))
     ) and
     not bypassContentSet(c)
   }
 
-  predicate clearsContent(Node n, ContentSet c) { captureSsaClearsContent(n, c) } // TODO
+  predicate clearsContent(Node n, ContentSet c) {
+    captureSsaClearsContent(n, c)
+    or
+    FlowSummaryOutput::summaryClearsContent(getSummaryNode(n), c) and
+    not bypassContentSet(c)
+  }
 
-  predicate expectsContent(Node n, ContentSet c) { none() } // TODO
+  predicate expectsContent(Node n, ContentSet c) {
+    FlowSummaryOutput::summaryExpectsContent(getSummaryNode(n), c) and
+    not bypassContentSet(c)
+  }
 
-  predicate localMustFlowStep(Node node1, Node node2) { localSsaMustFlowStep(node1, node2) } // TODO
+  predicate localMustFlowStep(Node node1, Node node2) {
+    step(node1, any(Step s | s.valueMustFlow()), node2) or
+    localSsaMustFlowStep(node1, node2) or
+    FlowSummaryOutput::summaryLocalMustFlowStep(getSummaryNode(node1), getSummaryNode(node2))
+  }
 
   //
   // Misc
@@ -207,7 +259,14 @@ module DataFlowInput implements InputSig<Location> {
 
   predicate isUnreachableInCall(NodeRegion nr, DataFlowCall call) { none() } // TODO
 
-  predicate allowParameterReturnInSelf(ParameterNode p) { captureSsaAllowParameterReturnInSelf(p) }
+  predicate allowParameterReturnInSelf(ParameterNode p) {
+    captureSsaAllowParameterReturnInSelf(p)
+    or
+    exists(DataFlowCallable c, ParameterPosition pos |
+      FlowSummaryOutput::summaryAllowParameterReturnInSelf(c.asSummarizedCallable(), pos) and
+      isParameterNodeImpl(p, c, pos)
+    )
+  }
 
   class LambdaCallKind extends Unit { }
 
@@ -216,9 +275,11 @@ module DataFlowInput implements InputSig<Location> {
     exists(kind)
   }
 
-  predicate lambdaCall(DataFlowCall call, LambdaCallKind kind, Node receiver) {
-    receiver.(BuilderNode).isImplicitArgument(call, any(ArgumentPosition p | p.isCallee()), false) and
+  predicate lambdaCall(DataFlowCall call, LambdaCallKind kind, Node callee) {
+    callee.(BuilderNode).isImplicitArgument(call, any(ArgumentPosition p | p.isCallee()), false) and
     exists(kind)
+    or
+    call.isSummaryCall(_, getSummaryNode(callee)) and exists(kind)
   }
 
   predicate additionalLambdaFlowStep(Node nodeFrom, Node nodeTo, boolean preservesValue) {