From d5ccb2e396a909913a8586c251954e0986d69f68 Mon Sep 17 00:00:00 2001
From: Mathias Vorreiter Pedersen <mathiasvp@github.com>
Date: Wed, 17 Jul 2024 14:39:02 +0100
Subject: [PATCH] C++: Add a large QLDoc with example to
 'getInstructionSuccessor'.

---
 .../aliased_ssa/internal/SSAConstruction.qll  | 74 ++++++++++++++++++-
 1 file changed, 73 insertions(+), 1 deletion(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/internal/SSAConstruction.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/internal/SSAConstruction.qll
index 6e16b9bcb35..819f3906b82 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/internal/SSAConstruction.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/internal/SSAConstruction.qll
@@ -511,7 +511,79 @@ private module Cached {
    * that node is its successor in the new successor relation, and the Chi node's successors are
    * the new instructions generated from the successors of the old instruction.
    *
-   * Furthermore, the entry block is augmented with `UninitializedGroup` instructions.
+   * Furthermore, the entry block is augmented with `UninitializedGroup` instructions and `Chi`
+   * instructions. For example, consider this example:
+   * ```cpp
+   * int x, y;
+   * int* p;
+   * if(b) {
+   *   p = &x;
+   *   escape(&x);
+   * } else {
+   *   p = &y;
+   * }
+   * *p = 42;
+   *
+   * int z, w;
+   * int* q;
+   * if(b) {
+   *   q = &z;
+   * } else {
+   *   q = &w;
+   * }
+   * *q = 43;
+   * ```
+   *
+   * the unaliased IR for the entry block of this snippet is:
+   * ```
+   * v1(void)         = EnterFunction          :
+   * m1(unknown)      = AliasedDefinition      :
+   * m2(unknown)      = InitializeNonLocal     :
+   * r1(glval<bool>)  = VariableAddress[b]     :
+   * m3(bool)         = InitializeParameter[b] : &:r1
+   * r2(glval<int>)   = VariableAddress[x]     :
+   * m4(int)          = Uninitialized[x]       : &:r2
+   * r3(glval<int>)   = VariableAddress[y]     :
+   * m5(int)          = Uninitialized[y]       : &:r3
+   * r4(glval<int *>) = VariableAddress[p]     :
+   * m6(int *)        = Uninitialized[p]       : &:r4
+   * r5(glval<bool>)  = VariableAddress[b]     :
+   * r6(bool)         = Load[b]                : &:r5, m3
+   * v2(void)         = ConditionalBranch      : r6
+   * ```
+   * and we need to transform this to aliased IR by inserting an `UninitializedGroup`
+   * instruction for every `VariableGroup` memory location in the function. Furthermore,
+   * if the `VariableGroup` memory location contains an allocation that escapes we need
+   * to insert a `Chi` that writes the memory produced by `UninitializedGroup` into
+   * `{AllAliasedMemory}`. For the above snippet we then end up with:
+   * ```
+   * v1(void)         = EnterFunction           :
+   * m2(unknown)      = AliasedDefinition       :
+   * m3(unknown)      = InitializeNonLocal      :
+   * m4(unknown)      = Chi                     : total:m2, partial:m3
+   * m5(int)          = UninitializedGroup[x,y] :
+   * m6(unknown)      = Chi                     : total:m4, partial:m5
+   * m7(int)          = UninitializedGroup[w,z] :
+   * r1(glval<bool>)  = VariableAddress[b]      :
+   * m8(bool)         = InitializeParameter[b]  : &:r1
+   * r2(glval<int>)   = VariableAddress[x]      :
+   * m10(int)         = Uninitialized[x]       : &:r2
+   * m11(unknown)     = Chi                    : total:m6, partial:m10
+   * r3(glval<int>)   = VariableAddress[y]      :
+   * m12(int)         = Uninitialized[y]       : &:r3
+   * m13(unknown)     = Chi                    : total:m11, partial:m12
+   * r4(glval<int *>) = VariableAddress[p]      :
+   * m14(int *)       = Uninitialized[p]       : &:r4
+   * r5(glval<bool>)  = VariableAddress[b]      :
+   * r6(bool)         = Load[b]                 : &:r5, m8
+   * v2(void)         = ConditionalBranch       : r6
+   * ```
+   *
+   * Here, the group `{x, y}` contains an allocation that escapes (`x`), so there
+   * is a `Chi` after the `UninitializedGroup` that initializes the memory for the
+   * `VariableGroup` containing `x`. None of the allocations in `{w, z}` escape so
+   * there is no `Chi` following that the `UninitializedGroup` that initializes the
+   * memory of `{w, z}`.
    */
   cached
   Instruction getInstructionSuccessor(Instruction instruction, EdgeKind kind) {