From 573763a4b339c9b7c5c6558f7375fac8dfb40efa Mon Sep 17 00:00:00 2001
From: Geoffrey White <40627776+geoffw0@users.noreply.github.com>
Date: Thu, 22 Feb 2024 18:44:17 +0000
Subject: [PATCH] Shared: More revisions, manual and aided by further
 discussion with Copilot.

---
 shared/dataflow/codeql/dataflow/DataFlow.qll  | 17 ++++++---
 .../codeql/rangeanalysis/RangeAnalysis.qll    | 35 +++++++++++++++----
 2 files changed, 40 insertions(+), 12 deletions(-)

diff --git a/shared/dataflow/codeql/dataflow/DataFlow.qll b/shared/dataflow/codeql/dataflow/DataFlow.qll
index fb3535416d3..ea44ec5d0ce 100644
--- a/shared/dataflow/codeql/dataflow/DataFlow.qll
+++ b/shared/dataflow/codeql/dataflow/DataFlow.qll
@@ -7,7 +7,7 @@
 /** Provides language-specific data flow parameters. */
 signature module InputSig {
   /**
-   * Represents a node in the data flow graph.
+   * A node in the data flow graph.
    */
   class Node {
     /** Gets a textual representation of this element. */
@@ -34,16 +34,23 @@ signature module InputSig {
   }
 
   /**
-   * Represents a node in the data flow graph that represents an output.
+   * A node in the data flow graph that represents an output.
    */
   class OutNode extends Node;
 
   /**
-   * Represents a node in the data flow graph that corresponds to a post-update operation.
+   * A node in the data flow graph representing the value of an argument after
+   * a function call returns. For example, consider the following C++ code:
+   * ```
+   * int a = 1;
+   * increment(&a);
+   * ```
+   * The post-update node for `&a` represents the value of `&a` after
+   * modification by the call to `increment`.
    */
   class PostUpdateNode extends Node {
     /**
-     * Gets the node that represents the pre-update operation.
+     * Gets the node that represents the same value prior to the operation.
      *
      * @return The pre-update node.
      */
@@ -170,7 +177,7 @@ signature module InputSig {
   }
 
   /**
-   * Represents a content approximation.
+   * A content approximation.
    */
   class ContentApprox {
     /** Gets a textual representation of this element. */
diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
index e57c6889799..28329e844da 100644
--- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
+++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
@@ -161,7 +161,7 @@ signature module Semantic {
   default string getBlockId2(BasicBlock bb) { result = "" }
 
   /**
-   * Represents a guard in the range analysis.
+   * A guard in the range analysis.
    */
   class Guard {
     /**
@@ -180,7 +180,15 @@ signature module Semantic {
     Expr asExpr();
 
     /**
-     * Holds if the guard directly controls a given basic block.
+     * Holds if the guard directly controls a given basic block. For example in
+     * the following code, the guard `(x > y)` directly controls the block
+     * beneath it:
+     * ```
+     * if (x > y)
+     * {
+     *   Console.WriteLine("x is greater than y");
+     * }
+     * ```
      *
      * @param controlled The basic block to check.
      */
@@ -194,7 +202,17 @@ signature module Semantic {
     predicate isEquality(Expr e1, Expr e2, boolean polarity);
 
     /**
-     * Holds if there is a branch edge between two basic blocks.
+     * Holds if there is a branch edge between two basic blocks. For example
+     * in the following C code, there are two branch edges from the basic block
+     * containing the condition `(x > y)` to the beginnings of the true and
+     * false blocks that follow:
+     * ```
+     * if (x > y) {
+     *   printf("x is greater than y\n");
+     * } else {
+     *   printf("x is not greater than y\n");
+     * }
+     * ```
      *
      * @param bb1 The first basic block.
      */
@@ -222,7 +240,7 @@ signature module Semantic {
   Type getExprType(Expr e);
 
   /**
-   * Represents a single static single assignment (SSA) variable.
+   * A single static single assignment (SSA) variable.
    */
   class SsaVariable {
     /**
@@ -237,7 +255,9 @@ signature module Semantic {
   }
 
   /**
-   * Represents a phi node in the SSA form.
+   * A phi node in the SSA form. A phi node is a kind of node in the SSA form
+   * that represents a merge point where multiple control flow paths converge
+   * and the value of a variable needs to be selected.
    */
   class SsaPhiNode extends SsaVariable {
     /** Holds if `inp` is an input to the phi node along the edge originating in `bb`. */
@@ -245,7 +265,7 @@ signature module Semantic {
   }
 
   /**
-   * Represents a single update to a variable in the SSA form.
+   * A single update to a variable in the SSA form.
    */
   class SsaExplicitUpdate extends SsaVariable {
     /**
@@ -344,7 +364,8 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
 
 signature module BoundSig<LocationSig Location, Semantic Sem, DeltaSig D> {
   /**
-   * Represents a semantic bound.
+   * A semantic bound, which defines a constraint on the possible values of an
+   * expression.
    */
   class SemBound {
     /**