From 776e35279ddde989b12f118f4a1ab441f52fd49a Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Fri, 27 Oct 2023 10:43:54 +0200
Subject: [PATCH] Dataflow: Improve qldoc on the type system.

---
 shared/dataflow/codeql/dataflow/DataFlow.qll | 29 ++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/shared/dataflow/codeql/dataflow/DataFlow.qll b/shared/dataflow/codeql/dataflow/DataFlow.qll
index f7a2429ee8a..57694df0948 100644
--- a/shared/dataflow/codeql/dataflow/DataFlow.qll
+++ b/shared/dataflow/codeql/dataflow/DataFlow.qll
@@ -91,6 +91,13 @@ signature module InputSig {
    */
   OutNode getAnOutNode(DataFlowCall call, ReturnKind kind);
 
+  /**
+   * A type for a data flow node.
+   *
+   * This may or may not coincide with any type system existing for the source
+   * language, but should minimally include unique types for individual closure
+   * expressions (typically lambdas).
+   */
   class DataFlowType {
     /** Gets a textual representation of this element. */
     string toString();
@@ -98,9 +105,25 @@ signature module InputSig {
 
   string ppReprType(DataFlowType t);
 
+  /**
+   * Holds if `t1` and `t2` are compatible types.
+   *
+   * This predicate must be symmetric and reflexive.
+   *
+   * This predicate is used in the following way: If the data flow library
+   * tracks an object from node `n1` to `n2` using solely value-preserving
+   * steps, then it will check that the types of `n1` and `n2` are compatible.
+   * If they are not, then flow will be blocked.
+   */
   bindingset[t1, t2]
   predicate compatibleTypes(DataFlowType t1, DataFlowType t2);
 
+  /**
+   * Holds if `t1` is strictly stronger than `t2`. That is, `t1` is a strict
+   * subtype of `t2`.
+   *
+   * This predicate must be transitive and imply `compatibleTypes(t1, t2)`.
+   */
   predicate typeStrongerThan(DataFlowType t1, DataFlowType t2);
 
   class Content {
@@ -199,6 +222,12 @@ signature module InputSig {
 
   /**
    * Holds if the value of `node2` is given by `node1`.
+   *
+   * This predicate is combined with type information in the following way: If
+   * the data flow library is able to compute an improved type for `node1` then
+   * it will also conclude that this type applies to `node2`. Vice versa, if
+   * `node2` must be visited along a flow path, then any type known for `node2`
+   * must also apply to `node1`.
    */
   predicate localMustFlowStep(Node node1, Node node2);