From 652b74db451f7a4411915d93f4b075feb0af9634 Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Tue, 1 Oct 2024 15:12:49 -0400
Subject: [PATCH 01/22] Altering TExceptionEdge to include SEH and regular C++
 exceptions, and updating uses of TExceptionEdge

---
 .../semmle/code/cpp/ir/implementation/EdgeKind.qll | 14 +++++++++++---
 .../implementation/raw/internal/TranslatedCall.qll |  5 ++++-
 .../implementation/raw/internal/TranslatedExpr.qll |  2 ++
 .../implementation/raw/internal/TranslatedStmt.qll |  2 +-
 4 files changed, 18 insertions(+), 5 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll
index 81db183fa63e..f1cb765e11b1 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll
@@ -8,7 +8,7 @@ private newtype TEdgeKind =
   TGotoEdge() or // Single successor (including fall-through)
   TTrueEdge() or // 'true' edge of conditional branch
   TFalseEdge() or // 'false' edge of conditional branch
-  TExceptionEdge() or // Thrown exception
+  TExceptionEdge(boolean isSEH){isSEH in [true, false]} or // Thrown exception, true for SEH exceptions, false otherwise
   TDefaultEdge() or // 'default' label of switch
   TCaseEdge(string minValue, string maxValue) {
     // Case label of switch
@@ -54,7 +54,15 @@ class FalseEdge extends EdgeKind, TFalseEdge {
  * instruction's evaluation throws an exception.
  */
 class ExceptionEdge extends EdgeKind, TExceptionEdge {
-  final override string toString() { result = "Exception" }
+  boolean isSEH; //true for Structured Exception Handling, false for C++ exceptions
+
+  ExceptionEdge() { this = TExceptionEdge(isSEH) }
+
+  final predicate isSEH() { isSEH = true }
+
+  final override string toString() { 
+    result = "Exception"
+   }
 }
 
 /**
@@ -123,7 +131,7 @@ module EdgeKind {
   /**
    * Gets the single instance of the `ExceptionEdge` class.
    */
-  ExceptionEdge exceptionEdge() { result = TExceptionEdge() }
+  ExceptionEdge exceptionEdge() { result = TExceptionEdge(_) }
 
   /**
    * Gets the single instance of the `DefaultEdge` class.
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
index daa6bdaafcf6..12830bcd9705 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
@@ -88,9 +88,12 @@ abstract class TranslatedCall extends TranslatedExpr {
       result = this.getParent().getChildSuccessor(this, kind)
       or
       this.mayThrowException() and
-      kind instanceof ExceptionEdge and
+      kind instanceof ExceptionEdge and not kind.(ExceptionEdge).isSEH() and
       result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
     )
+    or
+    kind instanceof ExceptionEdge and kind.(ExceptionEdge).isSEH() and
+    result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
   }
 
   override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
index e7ccac24eb92..08cf8d51fde4 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
@@ -3040,6 +3040,7 @@ class TranslatedDestructorsAfterThrow extends TranslatedElement, TTranslatedDest
       // And otherwise, exit this element with an exceptional edge
       not exists(this.getChild(id + 1)) and
       kind instanceof ExceptionEdge and
+      not kind.(ExceptionEdge).isSEH() and
       result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
     )
   }
@@ -3079,6 +3080,7 @@ abstract class TranslatedThrowExpr extends TranslatedNonConstantExpr {
       or
       not exists(this.getDestructors()) and
       kind instanceof ExceptionEdge and
+      not kind.(ExceptionEdge).isSEH() and
       result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
     )
   }
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
index e37df72abbd0..6da8d42b8c7b 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
@@ -932,7 +932,7 @@ class TranslatedCatchByTypeHandler extends TranslatedHandler {
       kind instanceof GotoEdge and
       result = this.getParameter().getFirstInstruction(kind)
       or
-      kind instanceof ExceptionEdge and
+      kind instanceof ExceptionEdge and not kind.(ExceptionEdge).isSEH() and
       if exists(this.getDestructors())
       then result = this.getDestructors().getFirstInstruction(any(GotoEdge edge))
       else result = this.getParent().(TranslatedTryStmt).getNextHandler(this, any(GotoEdge edge))

From 82cdd02e3f217af60ad58312ba8a47f54d906d78 Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Wed, 2 Oct 2024 16:59:09 -0400
Subject: [PATCH 02/22] Overhaul of IR exception handling to account for SEH
 and C++ exceptions.

---
 .../raw/internal/TranslatedCall.qll           | 139 ++++++++++++++----
 .../internal/TranslatedDeclarationEntry.qll   |  16 +-
 .../raw/internal/TranslatedExpr.qll           | 115 ++++++++++++---
 .../raw/internal/TranslatedFunction.qll       |  11 +-
 .../raw/internal/TranslatedInitialization.qll |  30 +++-
 .../StructuredExceptionHandling.qll           |  26 +++-
 .../code/cpp/models/interfaces/Throwing.qll   |  38 ++++-
 7 files changed, 307 insertions(+), 68 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
index 12830bcd9705..4a0b23ba4720 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
@@ -83,17 +83,36 @@ abstract class TranslatedCall extends TranslatedExpr {
         any(UnreachedInstruction instr |
           this.getEnclosingFunction().getFunction() = instr.getEnclosingFunction()
         )
-    else (
-      not this.mustThrowException() and
-      result = this.getParent().getChildSuccessor(this, kind)
-      or
-      this.mayThrowException() and
-      kind instanceof ExceptionEdge and not kind.(ExceptionEdge).isSEH() and
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
-    )
-    or
-    kind instanceof ExceptionEdge and kind.(ExceptionEdge).isSEH() and
-    result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
+    else
+      exists(boolean isSEH |
+        isSEH = true and kind.(ExceptionEdge).isSEH()
+        or
+        isSEH = false and not kind.(ExceptionEdge).isSEH()
+      |
+        // Call throw behavior is resolved from most restricted to least restricted in order
+        // if there are conflicting throwing specificaitons for a function.
+        (
+          // Highest Restriction: If the call is known to never throw, regardless of other defined throwing behavior,
+          // do not generate any exception edges, only an ordinary successor
+          if this.(TranslatedCallExpr).neverRaiseException(isSEH)
+          then result = this.getParent().getChildSuccessor(this, kind)
+          else
+            // Medium Restriction: If the call is known to always throw, regardless of other defined throwing behavior,
+            // only generate an exception edge.
+            if this.(TranslatedCallExpr).alwaysRaiseException(isSEH)
+            then result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
+            else (
+              // Lowest Restruction: if the call is known to conditionally throw, generate both an exception edge and an
+              // ordinary successor
+              this.(TranslatedCallExpr).mayRaiseException(isSEH) and
+              (
+                result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
+                or
+                result = this.getParent().getChildSuccessor(this, kind)
+              )
+            )
+        )
+      )
   }
 
   override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
@@ -120,14 +139,28 @@ abstract class TranslatedCall extends TranslatedExpr {
   final override Instruction getResult() { result = this.getInstruction(CallTag()) }
 
   /**
-   * Holds if the evaluation of this call may throw an exception.
+   * The call target is known to always raise an exception.
+   * Note that `alwaysRaiseException`, `mayRaiseException`,
+   * and `neverRaiseException` may conflict (e.g., all hold for a given target).
+   * Conflicting results are resolved during IR generation.
+   */
+  abstract predicate alwaysRaiseException(boolean isSEH);
+
+  /**
+   * The call target is known to conditionally raise an exception.
+   * Note that `alwaysRaiseException`, `mayRaiseException`,
+   * and `neverRaiseException` may conflict (e.g., all hold for a given target).
+   * Conflicting results are resolved during IR generation.
    */
-  abstract predicate mayThrowException();
+  abstract predicate mayRaiseException(boolean isSEH);
 
   /**
-   * Holds if the evaluation of this call always throws an exception.
+   * The call target is known to never raise an exception.
+   * Note that `alwaysRaiseException`, `mayRaiseException`,
+   * and `neverRaiseException` may conflict (e.g., all hold for a given target).
+   * Conflicting results are resolved during IR generation.
    */
-  abstract predicate mustThrowException();
+  abstract predicate neverRaiseException(boolean isSEH);
 
   /**
    * Gets the result type of the call.
@@ -323,6 +356,34 @@ abstract class TranslatedCallExpr extends TranslatedNonConstantExpr, TranslatedC
   final override int getNumberOfArguments() { result = expr.getNumberOfArguments() }
 
   final override predicate isNoReturn() { any(Options opt).exits(expr.getTarget()) }
+
+  override Function getInstructionFunction(InstructionTag tag) {
+    tag = CallTargetTag() and result = expr.getTarget()
+  }
+
+  override predicate alwaysRaiseException(boolean isSEH) {
+    exists(ExceptionAnnotation f | f = expr.getTarget() |
+      f.alwaysRaisesException() and f.isSEH() and isSEH = true
+      or
+      f.alwaysRaisesException() and f.isCxx() and isSEH = false
+    )
+  }
+
+  override predicate mayRaiseException(boolean isSEH) {
+    exists(ExceptionAnnotation f | f = expr.getTarget() |
+      f.mayRaiseException() and f.isSEH() and isSEH = true
+      or
+      f.mayRaiseException() and f.isCxx() and isSEH = false
+    )
+  }
+
+  override predicate neverRaiseException(boolean isSEH) {
+    exists(ExceptionAnnotation f | f = expr.getTarget() |
+      f.neverRaisesException() and f.isSEH() and isSEH = true
+      or
+      f.neverRaisesException() and f.isCxx() and isSEH = false
+    )
+  }
 }
 
 /**
@@ -335,14 +396,42 @@ class TranslatedExprCall extends TranslatedCallExpr {
     result = getTranslatedExpr(expr.getExpr().getFullyConverted())
   }
 
-  final override predicate mayThrowException() {
-    // We assume that a call to a function pointer will not throw an exception.
+  override predicate alwaysRaiseException(boolean isSEH) {
+    // We assume that a call to a function pointer will not throw a CXX exception.
     // This is not sound in general, but this will greatly reduce the number of
     // exceptional edges.
-    none()
+    // For SEH exceptions, use the defined ThrowingFunction behavior and
+    // if no throwing function is found, assume a conditional SEH exception
+    // see `mayRaiseException`
+    exists(ExceptionAnnotation f | f = expr.getTarget() |
+      f.alwaysRaisesException() and f.isSEH() and isSEH = true
+    )
+  }
+
+  override predicate mayRaiseException(boolean isSEH) {
+    // We assume that a call to a function pointer will not throw a CXX exception.
+    // This is not sound in general, but this will greatly reduce the number of
+    // exceptional edges.
+    // For SEH exceptions, use the defined ThrowingFunction behavior and
+    // if no throwing function is found, assume a conditional SEH exception.
+    exists(ExceptionAnnotation f | f = expr.getTarget() |
+      f.mayRaiseException() and f.isSEH() and isSEH = true
+    )
+    or
+    not exists(ExceptionAnnotation f | f = expr.getTarget() and f.isSEH()) and isSEH = true
   }
 
-  final override predicate mustThrowException() { none() }
+  override predicate neverRaiseException(boolean isSEH) {
+    // We assume that a call to a function pointer will not throw a CXX exception.
+    // This is not sound in general, but this will greatly reduce the number of
+    // exceptional edges.
+    // For SEH exceptions, use the defined ThrowingFunction behavior and
+    // if no throwing function is found, assume a conditional SEH exception
+    // see `mayRaiseException`
+    exists(ExceptionAnnotation f | f = expr.getTarget() |
+      f.neverRaisesException() and f.isSEH() and isSEH = true
+    )
+  }
 }
 
 /**
@@ -351,10 +440,6 @@ class TranslatedExprCall extends TranslatedCallExpr {
 class TranslatedFunctionCall extends TranslatedCallExpr, TranslatedDirectCall {
   override FunctionCall expr;
 
-  override Function getInstructionFunction(InstructionTag tag) {
-    tag = CallTargetTag() and result = expr.getTarget()
-  }
-
   override Instruction getQualifierResult() {
     this.hasQualifier() and
     result = this.getQualifier().getResult()
@@ -364,14 +449,6 @@ class TranslatedFunctionCall extends TranslatedCallExpr, TranslatedDirectCall {
     exists(this.getQualifier()) and
     not exists(MemberFunction func | expr.getTarget() = func and func.isStatic())
   }
-
-  final override predicate mayThrowException() {
-    expr.getTarget().(ThrowingFunction).mayThrowException(_)
-  }
-
-  final override predicate mustThrowException() {
-    expr.getTarget().(ThrowingFunction).mayThrowException(true)
-  }
 }
 
 /**
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll
index c0fe9cd2207d..a4ed98290450 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll
@@ -165,8 +165,13 @@ class TranslatedStaticLocalVariableDeclarationEntry extends TranslatedDeclaratio
     result = this.getInstruction(DynamicInitializationFlagLoadTag())
     or
     tag = DynamicInitializationFlagLoadTag() and
-    kind instanceof GotoEdge and
-    result = this.getInstruction(DynamicInitializationConditionalBranchTag())
+    (
+      kind instanceof GotoEdge and
+      result = this.getInstruction(DynamicInitializationConditionalBranchTag())
+      or
+      kind.(ExceptionEdge).isSEH() and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e))
+    )
     or
     tag = DynamicInitializationConditionalBranchTag() and
     (
@@ -182,7 +187,12 @@ class TranslatedStaticLocalVariableDeclarationEntry extends TranslatedDeclaratio
     result = this.getInstruction(DynamicInitializationFlagStoreTag())
     or
     tag = DynamicInitializationFlagStoreTag() and
-    result = this.getParent().getChildSuccessor(this, kind)
+    (
+      result = this.getParent().getChildSuccessor(this, kind)
+      or
+      // All store instructions may throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and kind.(ExceptionEdge).isSEH()
+    )
   }
 
   final override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
index 08cf8d51fde4..4ad0551381f4 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
@@ -280,7 +280,13 @@ class TranslatedConditionValue extends TranslatedCoreExpr, ConditionContext,
     )
     or
     tag = ConditionValueResultLoadTag() and
-    result = this.getParent().getChildSuccessor(this, kind)
+    (
+      result = this.getParent().getChildSuccessor(this, kind)
+      or
+      // All load instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      kind.(ExceptionEdge).isSEH()
+    )
   }
 
   override Instruction getInstructionRegisterOperand(InstructionTag tag, OperandTag operandTag) {
@@ -391,7 +397,13 @@ class TranslatedLoad extends TranslatedValueCategoryAdjustment, TTranslatedLoad
 
   override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = LoadTag() and
-    result = this.getParent().getChildSuccessor(this, kind)
+    (
+      result = this.getParent().getChildSuccessor(this, kind)
+      or
+      // All load instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      kind.(ExceptionEdge).isSEH()
+    )
   }
 
   override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
@@ -931,7 +943,13 @@ class TranslatedThisExpr extends TranslatedNonConstantExpr {
     result = this.getInstruction(ThisLoadTag())
     or
     tag = ThisLoadTag() and
-    result = this.getParent().getChildSuccessor(this, kind)
+    (
+      result = this.getParent().getChildSuccessor(this, kind)
+      or
+      // All load instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      kind.(ExceptionEdge).isSEH()
+    )
   }
 
   final override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
@@ -1083,7 +1101,13 @@ class TranslatedStructuredBindingVariableAccess extends TranslatedNonConstantExp
     result = this.getInstruction(LoadTag())
     or
     tag = LoadTag() and
-    result = this.getParent().getChildSuccessor(this, kind)
+    (
+      result = this.getParent().getChildSuccessor(this, kind)
+      or
+      // All load instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      kind.(ExceptionEdge).isSEH()
+    )
   }
 
   override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) { none() }
@@ -1898,8 +1922,13 @@ class TranslatedBlockAssignExpr extends TranslatedNonConstantExpr {
 
   override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = LoadTag() and
-    result = this.getInstruction(AssignmentStoreTag()) and
-    kind instanceof GotoEdge
+    (
+      result = this.getInstruction(AssignmentStoreTag()) and kind instanceof GotoEdge
+      or
+      // All load instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      kind.(ExceptionEdge).isSEH()
+    )
     or
     tag = AssignmentStoreTag() and
     result = this.getParent().getChildSuccessor(this, kind)
@@ -2375,14 +2404,16 @@ class TranslatedAllocatorCall extends TTranslatedAllocatorCall, TranslatedDirect
         result = getTranslatedExpr(expr.getAllocatorCall().getArgument(index).getFullyConverted())
   }
 
-  final override predicate mayThrowException() {
+  final override predicate mayRaiseException(boolean isSEH) {
     // We assume that a call to `new` or `new[]` will never throw. This is not
     // sound in general, but this will greatly reduce the number of exceptional
     // edges.
     none()
   }
 
-  final override predicate mustThrowException() { none() }
+  final override predicate alwaysRaiseException(boolean isSEH) { none() }
+
+  final override predicate neverRaiseException(boolean isSEH) { none() }
 }
 
 TranslatedAllocatorCall getTranslatedAllocatorCall(NewOrNewArrayExpr newExpr) {
@@ -2448,14 +2479,16 @@ class TranslatedDeleteOrDeleteArrayExpr extends TranslatedNonConstantExpr, Trans
     result = getTranslatedExpr(expr.getExprWithReuse().getFullyConverted())
   }
 
-  final override predicate mayThrowException() {
+  final override predicate mayRaiseException(boolean isSEH) {
     // We assume that a call to `delete` or `delete[]` will never throw. This is not
     // sound in general, but this will greatly reduce the number of exceptional
     // edges.
     none()
   }
 
-  final override predicate mustThrowException() { none() }
+  final override predicate alwaysRaiseException(boolean isSEH) { none() }
+
+  final override predicate neverRaiseException(boolean isSEH) { none() }
 }
 
 TranslatedDeleteOrDeleteArrayExpr getTranslatedDeleteOrDeleteArray(DeleteOrDeleteArrayExpr newExpr) {
@@ -2648,6 +2681,11 @@ abstract class TranslatedConditionalExpr extends TranslatedNonConstantExpr {
         result = this.getInstruction(ConditionValueResultTempAddressTag())
       )
       or
+      // All load instructions could throw an SEH exception
+      (tag = ConditionValueTrueStoreTag() or tag = ConditionValueFalseStoreTag()) and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      kind.(ExceptionEdge).isSEH()
+      or
       not this.elseIsVoid() and
       kind instanceof GotoEdge and
       (
@@ -2674,7 +2712,13 @@ abstract class TranslatedConditionalExpr extends TranslatedNonConstantExpr {
       or
       (not expr.hasLValueToRValueConversion() or not isExtractorFrontendVersion65OrHigher()) and
       tag = ConditionValueResultLoadTag() and
-      result = this.getParent().getChildSuccessor(this, kind)
+      (
+        result = this.getParent().getChildSuccessor(this, kind)
+        or
+        // All load instructions could throw an SEH exception
+        result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+        kind.(ExceptionEdge).isSEH()
+      )
     )
   }
 
@@ -3369,7 +3413,13 @@ class TranslatedVarArgsStart extends TranslatedNonConstantExpr {
     result = this.getVAList().getFirstInstruction(kind)
     or
     tag = VarArgsVAListStoreTag() and
-    result = this.getParent().getChildSuccessor(this, kind)
+    (
+      result = this.getParent().getChildSuccessor(this, kind)
+      or
+      // All store instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      kind.(ExceptionEdge).isSEH()
+    )
   }
 
   final override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
@@ -3439,8 +3489,13 @@ class TranslatedVarArg extends TranslatedNonConstantExpr {
 
   final override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = VarArgsVAListLoadTag() and
-    kind instanceof GotoEdge and
-    result = this.getInstruction(VarArgsArgAddressTag())
+    (
+      kind instanceof GotoEdge and result = this.getInstruction(VarArgsArgAddressTag())
+      or
+      // All load instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      kind.(ExceptionEdge).isSEH()
+    )
     or
     tag = VarArgsArgAddressTag() and
     kind instanceof GotoEdge and
@@ -3451,7 +3506,13 @@ class TranslatedVarArg extends TranslatedNonConstantExpr {
     result = this.getInstruction(VarArgsVAListStoreTag())
     or
     tag = VarArgsVAListStoreTag() and
-    result = this.getParent().getChildSuccessor(this, kind)
+    (
+      result = this.getParent().getChildSuccessor(this, kind)
+      or
+      // All store instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      kind.(ExceptionEdge).isSEH()
+    )
   }
 
   final override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
@@ -3573,10 +3634,22 @@ class TranslatedVarArgCopy extends TranslatedNonConstantExpr {
 
   final override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = VarArgsVAListLoadTag() and
-    result = this.getDestinationVAList().getFirstInstruction(kind)
+    (
+      result = this.getDestinationVAList().getFirstInstruction(kind)
+      or
+      // All load instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      kind.(ExceptionEdge).isSEH()
+    )
     or
     tag = VarArgsVAListStoreTag() and
-    result = this.getParent().getChildSuccessor(this, kind)
+    (
+      result = this.getParent().getChildSuccessor(this, kind)
+      or
+      // All store instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      kind.(ExceptionEdge).isSEH()
+    )
   }
 
   final override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
@@ -3780,7 +3853,13 @@ class TranslatedLambdaExpr extends TranslatedNonConstantExpr, InitializationCont
     )
     or
     tag = LoadTag() and
-    result = this.getParent().getChildSuccessor(this, kind)
+    (
+      result = this.getParent().getChildSuccessor(this, kind)
+      or
+      // All load instruction could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      kind.(ExceptionEdge).isSEH()
+    )
   }
 
   override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll
index 57f718bcb6ab..f2b808d92170 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll
@@ -214,7 +214,7 @@ class TranslatedFunction extends TranslatedRootElement, TTranslatedFunction {
         exists(ThrowExpr throw | throw.getEnclosingFunction() = func)
         or
         exists(FunctionCall call | call.getEnclosingFunction() = func |
-          getTranslatedExpr(call).(TranslatedCallExpr).mayThrowException()
+          getTranslatedExpr(call).(TranslatedCallExpr).mayRaiseException(_)
         )
       )
       or
@@ -401,9 +401,14 @@ abstract class TranslatedParameter extends TranslatedElement {
     then kind instanceof GotoEdge and result = this.getInstruction(InitializerIndirectAddressTag())
     else result = this.getParent().getChildSuccessor(this, kind)
     or
-    kind instanceof GotoEdge and
     tag = InitializerIndirectAddressTag() and
-    result = this.getInstruction(InitializerIndirectStoreTag())
+    (
+      result = this.getInstruction(InitializerIndirectStoreTag()) and kind instanceof GotoEdge
+      or
+      // All load instructions can throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      kind.(ExceptionEdge).isSEH()
+    )
     or
     tag = InitializerIndirectStoreTag() and
     result = this.getParent().getChildSuccessor(this, kind)
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll
index 06ce91932051..902e94d8a89a 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll
@@ -281,7 +281,12 @@ class TranslatedSimpleDirectInitialization extends TranslatedDirectInitializatio
 
   override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = InitializerStoreTag() and
-    result = this.getParent().getChildSuccessor(this, kind)
+    (
+      result = this.getParent().getChildSuccessor(this, kind)
+      or
+      // All store instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and kind.(ExceptionEdge).isSEH()
+    )
   }
 
   override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
@@ -357,9 +362,14 @@ class TranslatedStringLiteralInitialization extends TranslatedDirectInitializati
   }
 
   override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
-    kind instanceof GotoEdge and
+   
     tag = InitializerLoadStringTag() and
-    result = this.getInstruction(InitializerStoreTag())
+    (
+      result = this.getInstruction(InitializerStoreTag())  and kind instanceof GotoEdge
+      or
+      // All store instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and kind.(ExceptionEdge).isSEH()
+    )
     or
     if this.zeroInitRange(_, _)
     then (
@@ -650,7 +660,12 @@ class TranslatedFieldValueInitialization extends TranslatedFieldInitialization,
     )
     or
     tag = this.getFieldDefaultValueStoreTag() and
-    result = this.getParent().getChildSuccessor(this, kind)
+    (
+      result = this.getParent().getChildSuccessor(this, kind)
+      or
+      // All store instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and kind.(ExceptionEdge).isSEH()
+    )
   }
 
   override string getInstructionConstantValue(InstructionTag tag) {
@@ -850,7 +865,12 @@ class TranslatedElementValueInitialization extends TranslatedElementInitializati
     )
     or
     tag = this.getElementDefaultValueStoreTag() and
-    result = this.getParent().getChildSuccessor(this, kind)
+    (
+      result = this.getParent().getChildSuccessor(this, kind)
+      or
+      // All store instructions could throw an SEH exception
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and kind.(ExceptionEdge).isSEH()
+    )
   }
 
   override string getInstructionConstantValue(InstructionTag tag) {
diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll
index af8f3088f255..c729c9ac2df8 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll
@@ -1,9 +1,29 @@
 import semmle.code.cpp.models.interfaces.Throwing
 
-class WindowsDriverFunction extends ThrowingFunction {
-  WindowsDriverFunction() {
+/**
+ * The default behavior for SEH is any function may (conditionally) raise an exception.
+ * NOTE: this can be overriden by for any specific function to make in
+ * unconditional or non-throwing. IR generation will enforce
+ * the most strict interpretation.
+ */
+class DefaultSEHExceptionBehavior extends ExceptionAnnotation {
+  DefaultSEHExceptionBehavior() { this = any(Function f) }
+
+  override predicate raisesException(boolean unconditional) { 
+    unconditional = false
+  }
+
+  override TSEHException getExceptionType() { any() }
+}
+
+class WindowsDriverExceptionAnnotation extends ExceptionAnnotation {
+  WindowsDriverExceptionAnnotation() {
     this.hasGlobalName(["RaiseException", "ExRaiseAccessViolation", "ExRaiseDatatypeMisalignment"])
   }
 
-  final override predicate mayThrowException(boolean unconditional) { unconditional = true }
+  override predicate raisesException(boolean unconditional) { 
+    unconditional = true
+  }
+
+  override TSEHException getExceptionType() { any() }
 }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
index 79b7523f1d9f..64d2766489e6 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
@@ -10,13 +10,41 @@ import semmle.code.cpp.Function
 import semmle.code.cpp.models.Models
 import semmle.code.cpp.models.interfaces.FunctionInputsAndOutputs
 
-/**
+newtype TException =
+  TSEHException() or
+  TCxxException()
+
+ /**
  * A class that models the exceptional behavior of a function.
+ * This class models both Structed Exeception Handling (SEH) and C++ exceptions.
+ * This class also models if a function is definitively known to never throw an exception
+ * by concretizing the `raisesException` predicate to `none()`.
+ * This class is designed to explicitly model exception behavior when known.
+ * 
+ * If throwing details conflict for the same function, IR is assumed
+ * to use the most restricted interpretation, meaning taking options
+ * that stipulate no exception is raised, before the exception is always raised,
+ * before conditional exceptions.
  */
-abstract class ThrowingFunction extends Function {
+abstract class ExceptionAnnotation extends Function {
+  // TException exceptionType;
   /**
-   * Holds if this function may throw an exception during evaluation.
-   * If `unconditional` is `true` the function always throws an exception.
+   * Holds if this function may raise an exception during evaluation.
+   * If `conditional` is `false` the function may raise, and if `true` the function
+   * will always raise an exception.
+   * To specify the function never raises an exception, concretize as `none()`.
    */
-  abstract predicate mayThrowException(boolean unconditional);
+  abstract predicate raisesException(boolean unconditional);
+
+  abstract TException getExceptionType();
+
+  final predicate isSEH() { this.getExceptionType() = TSEHException() }
+
+  final predicate isCxx() { this.getExceptionType() = TCxxException() }
+
+  final predicate neverRaisesException() { not this.raisesException(_)}
+
+  final predicate alwaysRaisesException() { this.raisesException(true) }
+
+  final predicate mayRaiseException() { this.raisesException(false) }
 }

From a81834623bee391063a440a5139f19637983f1b9 Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Thu, 3 Oct 2024 11:29:31 -0400
Subject: [PATCH 03/22] Fixing bug in translated call edge generation.

---
 .../raw/internal/TranslatedCall.qll           | 23 +++++++++++--------
 1 file changed, 13 insertions(+), 10 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
index 4a0b23ba4720..5c9dd24521a4 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
@@ -91,26 +91,28 @@ abstract class TranslatedCall extends TranslatedExpr {
       |
         // Call throw behavior is resolved from most restricted to least restricted in order
         // if there are conflicting throwing specificaitons for a function.
+        // Enumerating all scenarios to be explicit.
         (
-          // Highest Restriction: If the call is known to never throw, regardless of other defined throwing behavior,
+          // If the call is known to never throw, regardless of other defined throwing behavior,
           // do not generate any exception edges, only an ordinary successor
           if this.(TranslatedCallExpr).neverRaiseException(isSEH)
           then result = this.getParent().getChildSuccessor(this, kind)
           else
-            // Medium Restriction: If the call is known to always throw, regardless of other defined throwing behavior,
+            // If the call is known to always throw, regardless of other defined throwing behavior,
             // only generate an exception edge.
             if this.(TranslatedCallExpr).alwaysRaiseException(isSEH)
             then result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
-            else (
-              // Lowest Restruction: if the call is known to conditionally throw, generate both an exception edge and an
-              // ordinary successor
-              this.(TranslatedCallExpr).mayRaiseException(isSEH) and
-              (
+            else
+              if this.(TranslatedCallExpr).mayRaiseException(isSEH)
+              then (
+                // if the call is known to conditionally throw, generate both an exception edge and an
+                // ordinary successor
                 result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
                 or
                 result = this.getParent().getChildSuccessor(this, kind)
-              )
-            )
+              ) else
+                // fallthrough case, no exceptions, just get the ordinary successor
+                result = this.getParent().getChildSuccessor(this, kind)
         )
       )
   }
@@ -418,7 +420,8 @@ class TranslatedExprCall extends TranslatedCallExpr {
       f.mayRaiseException() and f.isSEH() and isSEH = true
     )
     or
-    not exists(ExceptionAnnotation f | f = expr.getTarget() and f.isSEH()) and isSEH = true
+    not exists(ExceptionAnnotation f | f = expr.getTarget() and f.isSEH()) and
+    isSEH = true
   }
 
   override predicate neverRaiseException(boolean isSEH) {

From a2ede08e6004e7242a6ab7023ba281e9ee1f332e Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Mon, 7 Oct 2024 11:51:42 -0400
Subject: [PATCH 04/22] Finalizing a model for throwing and non-throwing
 functions.

---
 .../raw/internal/TranslatedCall.qll           | 25 +++++------
 .../cpp/models/implementations/Memcpy.qll     |  4 +-
 .../cpp/models/implementations/Memset.qll     |  4 +-
 .../implementations/NoexceptFunction.qll      |  4 +-
 .../cpp/models/implementations/Printf.qll     | 12 +++++-
 .../cpp/models/implementations/Strcat.qll     |  4 +-
 .../cpp/models/implementations/Strcpy.qll     |  6 ++-
 .../StructuredExceptionHandling.qll           |  4 +-
 .../cpp/models/interfaces/NonThrowing.qll     | 11 -----
 .../code/cpp/models/interfaces/Throwing.qll   | 42 +++++++++++--------
 10 files changed, 66 insertions(+), 50 deletions(-)
 delete mode 100644 cpp/ql/lib/semmle/code/cpp/models/interfaces/NonThrowing.qll

diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
index 5c9dd24521a4..8aa20286b653 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
@@ -364,7 +364,7 @@ abstract class TranslatedCallExpr extends TranslatedNonConstantExpr, TranslatedC
   }
 
   override predicate alwaysRaiseException(boolean isSEH) {
-    exists(ExceptionAnnotation f | f = expr.getTarget() |
+    exists(ThrowingFunction f | f = expr.getTarget() |
       f.alwaysRaisesException() and f.isSEH() and isSEH = true
       or
       f.alwaysRaisesException() and f.isCxx() and isSEH = false
@@ -372,7 +372,7 @@ abstract class TranslatedCallExpr extends TranslatedNonConstantExpr, TranslatedC
   }
 
   override predicate mayRaiseException(boolean isSEH) {
-    exists(ExceptionAnnotation f | f = expr.getTarget() |
+    exists(ThrowingFunction f | f = expr.getTarget() |
       f.mayRaiseException() and f.isSEH() and isSEH = true
       or
       f.mayRaiseException() and f.isCxx() and isSEH = false
@@ -380,10 +380,10 @@ abstract class TranslatedCallExpr extends TranslatedNonConstantExpr, TranslatedC
   }
 
   override predicate neverRaiseException(boolean isSEH) {
-    exists(ExceptionAnnotation f | f = expr.getTarget() |
-      f.neverRaisesException() and f.isSEH() and isSEH = true
+    exists(NonThrowingFunction f | f = expr.getTarget() |
+      f.isSEH() and isSEH = true
       or
-      f.neverRaisesException() and f.isCxx() and isSEH = false
+      f.isCxx() and isSEH = false
     )
   }
 }
@@ -405,7 +405,7 @@ class TranslatedExprCall extends TranslatedCallExpr {
     // For SEH exceptions, use the defined ThrowingFunction behavior and
     // if no throwing function is found, assume a conditional SEH exception
     // see `mayRaiseException`
-    exists(ExceptionAnnotation f | f = expr.getTarget() |
+    exists(ThrowingFunction f | f = expr.getTarget() |
       f.alwaysRaisesException() and f.isSEH() and isSEH = true
     )
   }
@@ -414,13 +414,14 @@ class TranslatedExprCall extends TranslatedCallExpr {
     // We assume that a call to a function pointer will not throw a CXX exception.
     // This is not sound in general, but this will greatly reduce the number of
     // exceptional edges.
-    // For SEH exceptions, use the defined ThrowingFunction behavior and
-    // if no throwing function is found, assume a conditional SEH exception.
-    exists(ExceptionAnnotation f | f = expr.getTarget() |
+    // For SEH exceptions, use the defined ThrowingFunction behavior.
+    // ASSUMPTION: if no ThrowingFunction is found for the given call, assume a conditional SEH exception
+    // on the call.
+    exists(ThrowingFunction f | f = expr.getTarget() |
       f.mayRaiseException() and f.isSEH() and isSEH = true
     )
     or
-    not exists(ExceptionAnnotation f | f = expr.getTarget() and f.isSEH()) and
+    not exists(ThrowingFunction f | f = expr.getTarget() and f.isSEH()) and
     isSEH = true
   }
 
@@ -431,8 +432,8 @@ class TranslatedExprCall extends TranslatedCallExpr {
     // For SEH exceptions, use the defined ThrowingFunction behavior and
     // if no throwing function is found, assume a conditional SEH exception
     // see `mayRaiseException`
-    exists(ExceptionAnnotation f | f = expr.getTarget() |
-      f.neverRaisesException() and f.isSEH() and isSEH = true
+    exists(NonThrowingFunction f | f = expr.getTarget() |
+      f.isSEH() and isSEH = true
     )
   }
 }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/Memcpy.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/Memcpy.qll
index 0bf2dd31fe40..8c3ae368da9d 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/Memcpy.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/Memcpy.qll
@@ -9,7 +9,7 @@ import semmle.code.cpp.models.interfaces.DataFlow
 import semmle.code.cpp.models.interfaces.Alias
 import semmle.code.cpp.models.interfaces.SideEffect
 import semmle.code.cpp.models.interfaces.Taint
-import semmle.code.cpp.models.interfaces.NonThrowing
+import semmle.code.cpp.models.interfaces.Throwing
 
 /**
  * The standard functions `memcpy`, `memmove` and `bcopy`; and the gcc variant
@@ -106,6 +106,8 @@ private class MemcpyFunction extends ArrayFunction, DataFlowFunction, SideEffect
     not this.hasGlobalName(["bcopy", mempcpy(), "memccpy"]) and
     index = this.getParamDest()
   }
+
+  override TCxxException getExceptionType() { any() }
 }
 
 private string mempcpy() { result = ["mempcpy", "wmempcpy"] }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/Memset.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/Memset.qll
index ab2e0af99f38..6a4ab8a133f2 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/Memset.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/Memset.qll
@@ -8,7 +8,7 @@ import semmle.code.cpp.models.interfaces.ArrayFunction
 import semmle.code.cpp.models.interfaces.DataFlow
 import semmle.code.cpp.models.interfaces.Alias
 import semmle.code.cpp.models.interfaces.SideEffect
-import semmle.code.cpp.models.interfaces.NonThrowing
+import semmle.code.cpp.models.interfaces.Throwing
 
 private class MemsetFunctionModel extends ArrayFunction, DataFlowFunction, AliasFunction,
   SideEffectFunction, NonThrowingFunction
@@ -74,6 +74,8 @@ private class MemsetFunctionModel extends ArrayFunction, DataFlowFunction, Alias
     i = 0 and
     if this.hasGlobalName(bzero()) then result = 1 else result = 2
   }
+
+  override TCxxException getExceptionType() { any() }
 }
 
 private string bzero() { result = ["bzero", "explicit_bzero"] }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/NoexceptFunction.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/NoexceptFunction.qll
index b0f76ee6538a..ee05b2a68a0b 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/NoexceptFunction.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/NoexceptFunction.qll
@@ -1,4 +1,4 @@
-import semmle.code.cpp.models.interfaces.NonThrowing
+import semmle.code.cpp.models.interfaces.Throwing
 
 /**
  * A function that is annotated with a `noexcept` specifier (or the equivalent
@@ -8,4 +8,6 @@ import semmle.code.cpp.models.interfaces.NonThrowing
  */
 class NoexceptFunction extends NonThrowingFunction {
   NoexceptFunction() { this.isNoExcept() or this.isNoThrow() }
+
+  override TCxxException getExceptionType() { any() }
 }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/Printf.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/Printf.qll
index 7286552e3ee0..8e94dba0ddbb 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/Printf.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/Printf.qll
@@ -8,7 +8,7 @@
 import semmle.code.cpp.models.interfaces.FormattingFunction
 import semmle.code.cpp.models.interfaces.Alias
 import semmle.code.cpp.models.interfaces.SideEffect
-import semmle.code.cpp.models.interfaces.NonThrowing
+import semmle.code.cpp.models.interfaces.Throwing
 
 /**
  * The standard functions `printf`, `wprintf` and their glib variants.
@@ -32,6 +32,8 @@ private class Printf extends FormattingFunction, AliasFunction, NonThrowingFunct
   override predicate parameterEscapesOnlyViaReturn(int n) { none() }
 
   override predicate parameterIsAlwaysReturned(int n) { none() }
+
+  override TCxxException getExceptionType() { any() }
 }
 
 /**
@@ -50,6 +52,8 @@ private class Fprintf extends FormattingFunction, NonThrowingFunction {
   override int getFormatParameterIndex() { result = 1 }
 
   override int getOutputParameterIndex(boolean isStream) { result = 0 and isStream = true }
+
+  override TCxxException getExceptionType() { any() }
 }
 
 /**
@@ -93,6 +97,8 @@ private class Sprintf extends FormattingFunction, NonThrowingFunction {
     then result = 4
     else result = this.getNumberOfParameters()
   }
+
+  override TCxxException getExceptionType() { any() }
 }
 
 /**
@@ -165,6 +171,8 @@ private class SnprintfImpl extends Snprintf, AliasFunction, SideEffectFunction,
     // We don't know how many parameters are passed to the function since it's varargs, but they also have read side effects.
     i = this.getFormatParameterIndex() and buffer = true
   }
+
+  override TCxxException getExceptionType() { any() }
 }
 
 /**
@@ -215,4 +223,6 @@ private class Syslog extends FormattingFunction, NonThrowingFunction {
   override int getFormatParameterIndex() { result = 1 }
 
   override predicate isOutputGlobal() { any() }
+
+  override TCxxException getExceptionType() { any() }
 }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcat.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcat.qll
index 9b11ed0af153..df85c56148a8 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcat.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcat.qll
@@ -7,7 +7,7 @@ import semmle.code.cpp.models.interfaces.ArrayFunction
 import semmle.code.cpp.models.interfaces.DataFlow
 import semmle.code.cpp.models.interfaces.Taint
 import semmle.code.cpp.models.interfaces.SideEffect
-import semmle.code.cpp.models.interfaces.NonThrowing
+import semmle.code.cpp.models.interfaces.Throwing
 
 /**
  * The standard function `strcat` and its wide, sized, and Microsoft variants.
@@ -94,6 +94,8 @@ class StrcatFunction extends TaintFunction, DataFlowFunction, ArrayFunction, Sid
     (i = 0 or i = 1) and
     buffer = true
   }
+
+  override TCxxException getExceptionType() { any() }
 }
 
 /**
diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcpy.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcpy.qll
index b7f06f0cebf4..f548ff648fd0 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcpy.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcpy.qll
@@ -7,13 +7,13 @@ import semmle.code.cpp.models.interfaces.ArrayFunction
 import semmle.code.cpp.models.interfaces.DataFlow
 import semmle.code.cpp.models.interfaces.Taint
 import semmle.code.cpp.models.interfaces.SideEffect
-import semmle.code.cpp.models.interfaces.NonThrowing
+import semmle.code.cpp.models.interfaces.Throwing
 
 /**
  * The standard function `strcpy` and its wide, sized, and Microsoft variants.
  */
 class StrcpyFunction extends ArrayFunction, DataFlowFunction, TaintFunction, SideEffectFunction,
-  NonThrowingFunction
+NonThrowingFunction
 {
   StrcpyFunction() {
     this.hasGlobalOrStdOrBslName([
@@ -145,4 +145,6 @@ class StrcpyFunction extends ArrayFunction, DataFlowFunction, TaintFunction, Sid
     i = this.getParamDest() and
     result = this.getParamSize()
   }
+
+  override TCxxException getExceptionType() { any() }
 }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll
index c729c9ac2df8..d4524adeb113 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll
@@ -6,7 +6,7 @@ import semmle.code.cpp.models.interfaces.Throwing
  * unconditional or non-throwing. IR generation will enforce
  * the most strict interpretation.
  */
-class DefaultSEHExceptionBehavior extends ExceptionAnnotation {
+class DefaultSEHExceptionBehavior extends ThrowingFunction {
   DefaultSEHExceptionBehavior() { this = any(Function f) }
 
   override predicate raisesException(boolean unconditional) { 
@@ -16,7 +16,7 @@ class DefaultSEHExceptionBehavior extends ExceptionAnnotation {
   override TSEHException getExceptionType() { any() }
 }
 
-class WindowsDriverExceptionAnnotation extends ExceptionAnnotation {
+class WindowsDriverExceptionAnnotation extends ThrowingFunction {
   WindowsDriverExceptionAnnotation() {
     this.hasGlobalName(["RaiseException", "ExRaiseAccessViolation", "ExRaiseDatatypeMisalignment"])
   }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/interfaces/NonThrowing.qll b/cpp/ql/lib/semmle/code/cpp/models/interfaces/NonThrowing.qll
deleted file mode 100644
index 64901d39ad30..000000000000
--- a/cpp/ql/lib/semmle/code/cpp/models/interfaces/NonThrowing.qll
+++ /dev/null
@@ -1,11 +0,0 @@
-/**
- * Provides an abstract class for modeling functions that never throw.
- */
-
-import semmle.code.cpp.Function
-import semmle.code.cpp.models.Models
-
-/**
- * A function that is guaranteed to never throw.
- */
-abstract class NonThrowingFunction extends Function { }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
index 64d2766489e6..cab7e18a2599 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
@@ -14,35 +14,41 @@ newtype TException =
   TSEHException() or
   TCxxException()
 
- /**
- * A class that models the exceptional behavior of a function.
- * This class models both Structed Exeception Handling (SEH) and C++ exceptions.
- * This class also models if a function is definitively known to never throw an exception
- * by concretizing the `raisesException` predicate to `none()`.
- * This class is designed to explicitly model exception behavior when known.
- * 
+/**
+ * Functions with information about how an exception is throwwn or if one is thrown at all.
  * If throwing details conflict for the same function, IR is assumed
  * to use the most restricted interpretation, meaning taking options
  * that stipulate no exception is raised, before the exception is always raised,
  * before conditional exceptions.
+ * 
+ * Annotations must specify if the exception is from SEH (structured exception handling)
+ * or ordinary c++ exceptions.
  */
-abstract class ExceptionAnnotation extends Function {
-  // TException exceptionType;
-  /**
-   * Holds if this function may raise an exception during evaluation.
-   * If `conditional` is `false` the function may raise, and if `true` the function
-   * will always raise an exception.
-   * To specify the function never raises an exception, concretize as `none()`.
-   */
-  abstract predicate raisesException(boolean unconditional);
-
+private abstract class ExceptionAnnotation extends Function {
   abstract TException getExceptionType();
 
   final predicate isSEH() { this.getExceptionType() = TSEHException() }
 
   final predicate isCxx() { this.getExceptionType() = TCxxException() }
+}
 
-  final predicate neverRaisesException() { not this.raisesException(_)}
+/**
+ * Functions that are known to not throw an exception.
+ */
+abstract class NonThrowingFunction extends ExceptionAnnotation { }
+
+/**
+ * Functions that are known to raise an exception.
+ */
+abstract class ThrowingFunction extends ExceptionAnnotation {
+  /**
+   * Holds if this function may raise an exception during evaluation.
+   * If `conditional` is `false` the function may raise, and if `true` the function
+   * will always raise an exception.
+   * Do not specify `none()` if no exception is raised, instead use the
+   * `NonThrowingFunction` class instead.
+   */
+  abstract predicate raisesException(boolean unconditional);
 
   final predicate alwaysRaisesException() { this.raisesException(true) }
 

From 0ed72d130eda91ae88e10eb71ebe7184cd8fb590 Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Mon, 7 Oct 2024 13:00:15 -0400
Subject: [PATCH 05/22] Propagating the exception kind into
 getExceptionSuccessorInstruction

---
 .../code/cpp/ir/implementation/EdgeKind.qll   |  3 ++
 .../raw/internal/TranslatedCall.qll           |  4 +-
 .../internal/TranslatedDeclarationEntry.qll   |  5 +-
 .../raw/internal/TranslatedElement.qll        |  8 +++-
 .../raw/internal/TranslatedExpr.qll           | 30 ++++++------
 .../raw/internal/TranslatedFunction.qll       |  7 ++-
 .../raw/internal/TranslatedInitialization.qll |  8 ++--
 .../raw/internal/TranslatedStmt.qll           | 47 +++++++++++++------
 8 files changed, 70 insertions(+), 42 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll
index f1cb765e11b1..c2b262f9c266 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll
@@ -58,6 +58,9 @@ class ExceptionEdge extends EdgeKind, TExceptionEdge {
 
   ExceptionEdge() { this = TExceptionEdge(isSEH) }
 
+  /**
+   * Holds if the exception is a Structured Exception Handling (SEH) exception.
+   */
   final predicate isSEH() { isSEH = true }
 
   final override string toString() { 
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
index 8aa20286b653..870c81bcfa3e 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
@@ -101,13 +101,13 @@ abstract class TranslatedCall extends TranslatedExpr {
             // If the call is known to always throw, regardless of other defined throwing behavior,
             // only generate an exception edge.
             if this.(TranslatedCallExpr).alwaysRaiseException(isSEH)
-            then result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
+            then result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), isSEH)
             else
               if this.(TranslatedCallExpr).mayRaiseException(isSEH)
               then (
                 // if the call is known to conditionally throw, generate both an exception edge and an
                 // ordinary successor
-                result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
+                result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), isSEH)
                 or
                 result = this.getParent().getChildSuccessor(this, kind)
               ) else
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll
index a4ed98290450..e10de508e874 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll
@@ -169,8 +169,9 @@ class TranslatedStaticLocalVariableDeclarationEntry extends TranslatedDeclaratio
       kind instanceof GotoEdge and
       result = this.getInstruction(DynamicInitializationConditionalBranchTag())
       or
+      // All load instructions may throw an SEH exception
       kind.(ExceptionEdge).isSEH() and
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e))
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true)
     )
     or
     tag = DynamicInitializationConditionalBranchTag() and
@@ -191,7 +192,7 @@ class TranslatedStaticLocalVariableDeclarationEntry extends TranslatedDeclaratio
       result = this.getParent().getChildSuccessor(this, kind)
       or
       // All store instructions may throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and kind.(ExceptionEdge).isSEH()
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and kind.(ExceptionEdge).isSEH()
     )
   }
 
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedElement.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedElement.qll
index 0f9bc370f7a5..4774a1eb2409 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedElement.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedElement.qll
@@ -1104,9 +1104,13 @@ abstract class TranslatedElement extends TTranslatedElement {
    * within this element. This will generally return first `catch` block of the
    * nearest enclosing `try`, or the `Unwind` instruction for the function if
    * there is no enclosing `try`. The successor edge kind is specified by `kind`.
+   * 
+   * `isSEH` is true if the exception is a structured exception, false if otherwise.
+   * The boolean value can be extracted from `ExceptionEdge` from the exception 
+   * edge triggering the call to this function.
    */
-  Instruction getExceptionSuccessorInstruction(EdgeKind kind) {
-    result = this.getParent().getExceptionSuccessorInstruction(kind)
+  Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSEH) {
+    result = this.getParent().getExceptionSuccessorInstruction(kind, isSEH)
   }
 
   /**
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
index 4ad0551381f4..9bb62b400e5e 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
@@ -284,7 +284,7 @@ class TranslatedConditionValue extends TranslatedCoreExpr, ConditionContext,
       result = this.getParent().getChildSuccessor(this, kind)
       or
       // All load instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
       kind.(ExceptionEdge).isSEH()
     )
   }
@@ -401,7 +401,7 @@ class TranslatedLoad extends TranslatedValueCategoryAdjustment, TTranslatedLoad
       result = this.getParent().getChildSuccessor(this, kind)
       or
       // All load instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
       kind.(ExceptionEdge).isSEH()
     )
   }
@@ -947,7 +947,7 @@ class TranslatedThisExpr extends TranslatedNonConstantExpr {
       result = this.getParent().getChildSuccessor(this, kind)
       or
       // All load instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
       kind.(ExceptionEdge).isSEH()
     )
   }
@@ -1105,7 +1105,7 @@ class TranslatedStructuredBindingVariableAccess extends TranslatedNonConstantExp
       result = this.getParent().getChildSuccessor(this, kind)
       or
       // All load instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
       kind.(ExceptionEdge).isSEH()
     )
   }
@@ -1926,7 +1926,7 @@ class TranslatedBlockAssignExpr extends TranslatedNonConstantExpr {
       result = this.getInstruction(AssignmentStoreTag()) and kind instanceof GotoEdge
       or
       // All load instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
       kind.(ExceptionEdge).isSEH()
     )
     or
@@ -2683,7 +2683,7 @@ abstract class TranslatedConditionalExpr extends TranslatedNonConstantExpr {
       or
       // All load instructions could throw an SEH exception
       (tag = ConditionValueTrueStoreTag() or tag = ConditionValueFalseStoreTag()) and
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
       kind.(ExceptionEdge).isSEH()
       or
       not this.elseIsVoid() and
@@ -2716,7 +2716,7 @@ abstract class TranslatedConditionalExpr extends TranslatedNonConstantExpr {
         result = this.getParent().getChildSuccessor(this, kind)
         or
         // All load instructions could throw an SEH exception
-        result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+        result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
         kind.(ExceptionEdge).isSEH()
       )
     )
@@ -3085,7 +3085,7 @@ class TranslatedDestructorsAfterThrow extends TranslatedElement, TTranslatedDest
       not exists(this.getChild(id + 1)) and
       kind instanceof ExceptionEdge and
       not kind.(ExceptionEdge).isSEH() and
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), true)
     )
   }
 
@@ -3125,7 +3125,7 @@ abstract class TranslatedThrowExpr extends TranslatedNonConstantExpr {
       not exists(this.getDestructors()) and
       kind instanceof ExceptionEdge and
       not kind.(ExceptionEdge).isSEH() and
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge))
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), true)
     )
   }
 
@@ -3417,7 +3417,7 @@ class TranslatedVarArgsStart extends TranslatedNonConstantExpr {
       result = this.getParent().getChildSuccessor(this, kind)
       or
       // All store instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
       kind.(ExceptionEdge).isSEH()
     )
   }
@@ -3493,7 +3493,7 @@ class TranslatedVarArg extends TranslatedNonConstantExpr {
       kind instanceof GotoEdge and result = this.getInstruction(VarArgsArgAddressTag())
       or
       // All load instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
       kind.(ExceptionEdge).isSEH()
     )
     or
@@ -3510,7 +3510,7 @@ class TranslatedVarArg extends TranslatedNonConstantExpr {
       result = this.getParent().getChildSuccessor(this, kind)
       or
       // All store instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
       kind.(ExceptionEdge).isSEH()
     )
   }
@@ -3638,7 +3638,7 @@ class TranslatedVarArgCopy extends TranslatedNonConstantExpr {
       result = this.getDestinationVAList().getFirstInstruction(kind)
       or
       // All load instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
       kind.(ExceptionEdge).isSEH()
     )
     or
@@ -3647,7 +3647,7 @@ class TranslatedVarArgCopy extends TranslatedNonConstantExpr {
       result = this.getParent().getChildSuccessor(this, kind)
       or
       // All store instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
       kind.(ExceptionEdge).isSEH()
     )
   }
@@ -3857,7 +3857,7 @@ class TranslatedLambdaExpr extends TranslatedNonConstantExpr, InitializationCont
       result = this.getParent().getChildSuccessor(this, kind)
       or
       // All load instruction could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
       kind.(ExceptionEdge).isSEH()
     )
   }
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll
index f2b808d92170..d41a18c25b11 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll
@@ -228,7 +228,10 @@ class TranslatedFunction extends TranslatedRootElement, TTranslatedFunction {
     )
   }
 
-  final override Instruction getExceptionSuccessorInstruction(EdgeKind kind) {
+  final override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSEH) {
+    // only unwind for C++ exceptions since SEH exceptions are too verbose
+    // and would generate unwind for all functions. 
+    isSEH = false and 
     result = this.getInstruction(UnwindTag()) and
     kind instanceof GotoEdge
   }
@@ -406,7 +409,7 @@ abstract class TranslatedParameter extends TranslatedElement {
       result = this.getInstruction(InitializerIndirectStoreTag()) and kind instanceof GotoEdge
       or
       // All load instructions can throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
       kind.(ExceptionEdge).isSEH()
     )
     or
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll
index 902e94d8a89a..3748b33e2abf 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll
@@ -285,7 +285,7 @@ class TranslatedSimpleDirectInitialization extends TranslatedDirectInitializatio
       result = this.getParent().getChildSuccessor(this, kind)
       or
       // All store instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and kind.(ExceptionEdge).isSEH()
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and kind.(ExceptionEdge).isSEH()
     )
   }
 
@@ -368,7 +368,7 @@ class TranslatedStringLiteralInitialization extends TranslatedDirectInitializati
       result = this.getInstruction(InitializerStoreTag())  and kind instanceof GotoEdge
       or
       // All store instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and kind.(ExceptionEdge).isSEH()
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and kind.(ExceptionEdge).isSEH()
     )
     or
     if this.zeroInitRange(_, _)
@@ -664,7 +664,7 @@ class TranslatedFieldValueInitialization extends TranslatedFieldInitialization,
       result = this.getParent().getChildSuccessor(this, kind)
       or
       // All store instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and kind.(ExceptionEdge).isSEH()
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and kind.(ExceptionEdge).isSEH()
     )
   }
 
@@ -869,7 +869,7 @@ class TranslatedElementValueInitialization extends TranslatedElementInitializati
       result = this.getParent().getChildSuccessor(this, kind)
       or
       // All store instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e)) and kind.(ExceptionEdge).isSEH()
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and kind.(ExceptionEdge).isSEH()
     )
   }
 
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
index 6da8d42b8c7b..18109f70decb 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
@@ -151,7 +151,7 @@ class TranslatedMicrosoftTryExceptHandler extends TranslatedElement,
       // TODO: This is not really correct. The semantics of `EXCEPTION_CONTINUE_EXECUTION` is that
       // we should continue execution at the point where the exception occurred. But we don't have
       // any instruction to model this behavior.
-      result = this.getExceptionSuccessorInstruction(any(GotoEdge edge))
+      result = this.getExceptionSuccessorInstruction(any(GotoEdge edge), true)
       or
       kind instanceof FalseEdge and
       result = this.getInstruction(TryExceptGenerateZero())
@@ -171,7 +171,7 @@ class TranslatedMicrosoftTryExceptHandler extends TranslatedElement,
     tag = TryExceptCompareZeroBranch() and
     (
       kind instanceof TrueEdge and
-      result = this.getExceptionSuccessorInstruction(any(GotoEdge edge))
+      result = this.getExceptionSuccessorInstruction(any(GotoEdge edge), true)
       or
       kind instanceof FalseEdge and
       result = this.getInstruction(TryExceptGenerateOne())
@@ -226,10 +226,11 @@ class TranslatedMicrosoftTryExceptHandler extends TranslatedElement,
 
   final override Function getFunction() { result = tryExcept.getEnclosingFunction() }
 
-  override Instruction getExceptionSuccessorInstruction(EdgeKind kind) {
+  override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSEH) {
     // A throw from within a `__except` block flows to the handler for the parent of
     // the `__try`.
-    result = this.getParent().getParent().getExceptionSuccessorInstruction(kind)
+    isSEH = true and
+    result = this.getParent().getParent().getExceptionSuccessorInstruction(kind, isSEH)
   }
 }
 
@@ -282,10 +283,11 @@ class TranslatedMicrosoftTryFinallyHandler extends TranslatedElement,
     result = getTranslatedStmt(tryFinally.getFinally())
   }
 
-  override Instruction getExceptionSuccessorInstruction(EdgeKind kind) {
+  override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSEH) {
     // A throw from within a `__finally` block flows to the handler for the parent of
     // the `__try`.
-    result = this.getParent().getParent().getExceptionSuccessorInstruction(kind)
+    isSEH = true and
+    result = this.getParent().getParent().getExceptionSuccessorInstruction(kind, isSEH)
   }
 }
 
@@ -734,14 +736,27 @@ class TranslatedTryStmt extends TranslatedStmt {
     // of the `try`, because the exception successor of the `try` itself is
     // the first catch clause.
     handler = this.getHandler(stmt.getNumberOfCatchClauses() - 1) and
-    result = this.getParent().getExceptionSuccessorInstruction(kind)
+    // TODO: uncertain of the SEH behavior here, not sure where a boolean would come from if I needed it
+    result = this.getParent().getExceptionSuccessorInstruction(kind, false)
   }
 
-  final override Instruction getExceptionSuccessorInstruction(EdgeKind kind) {
-    result = this.getHandler(0).getFirstInstruction(kind)
-    or
-    not exists(this.getHandler(_)) and
-    result = this.getFinally().getFirstInstruction(kind)
+  final override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSEH) {
+    // SEH exceptions are only handled for SEH try statements and
+    // C++ exceptions for C++ try statements.
+    // I.e., we are assuming there isn't a mix and match between SEH and C++ exceptions.
+    // They are either all SEH or all C++ within a single try block depending on the
+    // try type (TryStmt vs MicrosoftTryStmt).
+    (
+      stmt.getStmt() instanceof TryStmt and isSEH = false
+      or
+      stmt.getStmt() instanceof MicrosoftTryStmt and isSEH = true
+    ) and
+    (
+      result = this.getHandler(0).getFirstInstruction(kind)
+      or
+      not exists(this.getHandler(_)) and
+      result = this.getFinally().getFirstInstruction(kind)
+    )
   }
 
   private TranslatedElement getHandler(int index) { result = stmt.getTranslatedHandler(index) }
@@ -821,10 +836,11 @@ abstract class TranslatedHandler extends TranslatedStmt {
     child = this.getBlock() and result = this.getParent().getChildSuccessor(this, kind)
   }
 
-  override Instruction getExceptionSuccessorInstruction(EdgeKind kind) {
+  override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSEH) {
     // A throw from within a `catch` block flows to the handler for the parent of
     // the `try`.
-    result = this.getParent().getParent().getExceptionSuccessorInstruction(kind)
+    isSEH = false and
+    result = this.getParent().getParent().getExceptionSuccessorInstruction(kind, isSEH)
   }
 
   TranslatedStmt getBlock() { result = getTranslatedStmt(stmt.getBlock()) }
@@ -932,7 +948,8 @@ class TranslatedCatchByTypeHandler extends TranslatedHandler {
       kind instanceof GotoEdge and
       result = this.getParameter().getFirstInstruction(kind)
       or
-      kind instanceof ExceptionEdge and not kind.(ExceptionEdge).isSEH() and
+      kind instanceof ExceptionEdge and
+      not kind.(ExceptionEdge).isSEH() and
       if exists(this.getDestructors())
       then result = this.getDestructors().getFirstInstruction(any(GotoEdge edge))
       else result = this.getParent().(TranslatedTryStmt).getNextHandler(this, any(GotoEdge edge))

From e3d0015af38ab210f9de7511cfe81ff67f9d0be3 Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Mon, 7 Oct 2024 13:08:59 -0400
Subject: [PATCH 06/22] updating getNextHandler logic.

---
 .../implementation/raw/internal/TranslatedStmt.qll  | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
index 18109f70decb..f2f087ba39c2 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
@@ -736,8 +736,13 @@ class TranslatedTryStmt extends TranslatedStmt {
     // of the `try`, because the exception successor of the `try` itself is
     // the first catch clause.
     handler = this.getHandler(stmt.getNumberOfCatchClauses() - 1) and
-    // TODO: uncertain of the SEH behavior here, not sure where a boolean would come from if I needed it
-    result = this.getParent().getExceptionSuccessorInstruction(kind, false)
+    exists(boolean isSEH |
+      stmt instanceof MicrosoftTryStmt and isSEH = true
+      or
+      stmt instanceof TryStmt and isSEH = false
+    |
+      result = this.getParent().getExceptionSuccessorInstruction(kind, isSEH)
+    )
   }
 
   final override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSEH) {
@@ -747,9 +752,9 @@ class TranslatedTryStmt extends TranslatedStmt {
     // They are either all SEH or all C++ within a single try block depending on the
     // try type (TryStmt vs MicrosoftTryStmt).
     (
-      stmt.getStmt() instanceof TryStmt and isSEH = false
+      stmt instanceof TryStmt and isSEH = false
       or
-      stmt.getStmt() instanceof MicrosoftTryStmt and isSEH = true
+      stmt instanceof MicrosoftTryStmt and isSEH = true
     ) and
     (
       result = this.getHandler(0).getFirstInstruction(kind)

From 7a3ab8c7e04e3ebf5dfa86b38a4be1489150e697 Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Thu, 10 Oct 2024 11:51:34 -0400
Subject: [PATCH 07/22] Review updates to EdgeKind.qll

---
 .../semmle/code/cpp/ir/implementation/EdgeKind.qll | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll
index c2b262f9c266..51d95604d0a7 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll
@@ -3,12 +3,13 @@
  */
 
 private import internal.EdgeKindInternal
+private import codeql.util.Boolean
 
 private newtype TEdgeKind =
   TGotoEdge() or // Single successor (including fall-through)
   TTrueEdge() or // 'true' edge of conditional branch
   TFalseEdge() or // 'false' edge of conditional branch
-  TExceptionEdge(boolean isSEH){isSEH in [true, false]} or // Thrown exception, true for SEH exceptions, false otherwise
+  TExceptionEdge(Boolean isSEH) or // Thrown exception, true for SEH exceptions, false otherwise
   TDefaultEdge() or // 'default' label of switch
   TCaseEdge(string minValue, string maxValue) {
     // Case label of switch
@@ -63,9 +64,9 @@ class ExceptionEdge extends EdgeKind, TExceptionEdge {
    */
   final predicate isSEH() { isSEH = true }
 
-  final override string toString() { 
-    result = "Exception"
-   }
+  final override string toString() {
+    if isSEH = true then result = "SEH Exception" else result = "C++ Exception"
+  }
 }
 
 /**
@@ -132,9 +133,10 @@ module EdgeKind {
   FalseEdge falseEdge() { result = TFalseEdge() }
 
   /**
-   * Gets the single instance of the `ExceptionEdge` class.
+   * Gets the instance of the `ExceptionEdge` class.
+   * `isSEH` is true if the exception is an SEH exception, and false for a C++ edge.
    */
-  ExceptionEdge exceptionEdge() { result = TExceptionEdge(_) }
+  ExceptionEdge exceptionEdge(boolean isSEH) { result = TExceptionEdge(isSEH) }
 
   /**
    * Gets the single instance of the `DefaultEdge` class.

From d0a54a30f58ca9837208429a0a6427b8e8b738d7 Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Thu, 10 Oct 2024 14:36:43 -0400
Subject: [PATCH 08/22] Review updates.

---
 .../raw/internal/TranslatedCall.qll           | 19 +++----
 .../internal/TranslatedDeclarationEntry.qll   | 11 +---
 .../raw/internal/TranslatedExpr.qll           | 54 ++++---------------
 .../raw/internal/TranslatedFunction.qll       |  4 +-
 4 files changed, 21 insertions(+), 67 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
index 870c81bcfa3e..28c57b345af8 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
@@ -10,6 +10,7 @@ private import TranslatedElement
 private import TranslatedExpr
 private import TranslatedFunction
 private import DefaultOptions as DefaultOptions
+private import EdgeKind
 
 /**
  * Gets the `CallInstruction` from the `TranslatedCallExpr` for the specified expression.
@@ -84,11 +85,7 @@ abstract class TranslatedCall extends TranslatedExpr {
           this.getEnclosingFunction().getFunction() = instr.getEnclosingFunction()
         )
     else
-      exists(boolean isSEH |
-        isSEH = true and kind.(ExceptionEdge).isSEH()
-        or
-        isSEH = false and not kind.(ExceptionEdge).isSEH()
-      |
+      exists(boolean isSEH | kind = exceptionEdge(isSEH) |
         // Call throw behavior is resolved from most restricted to least restricted in order
         // if there are conflicting throwing specificaitons for a function.
         // Enumerating all scenarios to be explicit.
@@ -96,18 +93,20 @@ abstract class TranslatedCall extends TranslatedExpr {
           // If the call is known to never throw, regardless of other defined throwing behavior,
           // do not generate any exception edges, only an ordinary successor
           if this.(TranslatedCallExpr).neverRaiseException(isSEH)
-          then result = this.getParent().getChildSuccessor(this, kind)
+          then result = this.getParent().getChildSuccessor(this, any(GotoEdge edge))
           else
             // If the call is known to always throw, regardless of other defined throwing behavior,
             // only generate an exception edge.
             if this.(TranslatedCallExpr).alwaysRaiseException(isSEH)
-            then result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), isSEH)
+            then
+              result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), isSEH)
             else
               if this.(TranslatedCallExpr).mayRaiseException(isSEH)
               then (
                 // if the call is known to conditionally throw, generate both an exception edge and an
                 // ordinary successor
-                result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), isSEH)
+                result =
+                  this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), isSEH)
                 or
                 result = this.getParent().getChildSuccessor(this, kind)
               ) else
@@ -432,9 +431,7 @@ class TranslatedExprCall extends TranslatedCallExpr {
     // For SEH exceptions, use the defined ThrowingFunction behavior and
     // if no throwing function is found, assume a conditional SEH exception
     // see `mayRaiseException`
-    exists(NonThrowingFunction f | f = expr.getTarget() |
-      f.isSEH() and isSEH = true
-    )
+    exists(NonThrowingFunction f | f = expr.getTarget() | f.isSEH() and isSEH = true)
   }
 }
 
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll
index e10de508e874..1dc1eed9f6a3 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll
@@ -168,10 +168,6 @@ class TranslatedStaticLocalVariableDeclarationEntry extends TranslatedDeclaratio
     (
       kind instanceof GotoEdge and
       result = this.getInstruction(DynamicInitializationConditionalBranchTag())
-      or
-      // All load instructions may throw an SEH exception
-      kind.(ExceptionEdge).isSEH() and
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true)
     )
     or
     tag = DynamicInitializationConditionalBranchTag() and
@@ -188,12 +184,7 @@ class TranslatedStaticLocalVariableDeclarationEntry extends TranslatedDeclaratio
     result = this.getInstruction(DynamicInitializationFlagStoreTag())
     or
     tag = DynamicInitializationFlagStoreTag() and
-    (
-      result = this.getParent().getChildSuccessor(this, kind)
-      or
-      // All store instructions may throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and kind.(ExceptionEdge).isSEH()
-    )
+    result = this.getParent().getChildSuccessor(this, kind)
   }
 
   final override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
index 9bb62b400e5e..68f341950372 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
@@ -15,6 +15,7 @@ private import TranslatedInitialization
 private import TranslatedStmt
 private import TranslatedGlobalVar
 private import IRConstruction
+private import EdgeKind
 import TranslatedCall
 
 /**
@@ -280,13 +281,7 @@ class TranslatedConditionValue extends TranslatedCoreExpr, ConditionContext,
     )
     or
     tag = ConditionValueResultLoadTag() and
-    (
-      result = this.getParent().getChildSuccessor(this, kind)
-      or
-      // All load instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
-      kind.(ExceptionEdge).isSEH()
-    )
+    result = this.getParent().getChildSuccessor(this, kind)
   }
 
   override Instruction getInstructionRegisterOperand(InstructionTag tag, OperandTag operandTag) {
@@ -943,13 +938,7 @@ class TranslatedThisExpr extends TranslatedNonConstantExpr {
     result = this.getInstruction(ThisLoadTag())
     or
     tag = ThisLoadTag() and
-    (
-      result = this.getParent().getChildSuccessor(this, kind)
-      or
-      // All load instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
-      kind.(ExceptionEdge).isSEH()
-    )
+    result = this.getParent().getChildSuccessor(this, kind)
   }
 
   final override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
@@ -2681,11 +2670,6 @@ abstract class TranslatedConditionalExpr extends TranslatedNonConstantExpr {
         result = this.getInstruction(ConditionValueResultTempAddressTag())
       )
       or
-      // All load instructions could throw an SEH exception
-      (tag = ConditionValueTrueStoreTag() or tag = ConditionValueFalseStoreTag()) and
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
-      kind.(ExceptionEdge).isSEH()
-      or
       not this.elseIsVoid() and
       kind instanceof GotoEdge and
       (
@@ -2712,13 +2696,7 @@ abstract class TranslatedConditionalExpr extends TranslatedNonConstantExpr {
       or
       (not expr.hasLValueToRValueConversion() or not isExtractorFrontendVersion65OrHigher()) and
       tag = ConditionValueResultLoadTag() and
-      (
-        result = this.getParent().getChildSuccessor(this, kind)
-        or
-        // All load instructions could throw an SEH exception
-        result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
-        kind.(ExceptionEdge).isSEH()
-      )
+      result = this.getParent().getChildSuccessor(this, kind)
     )
   }
 
@@ -3084,8 +3062,8 @@ class TranslatedDestructorsAfterThrow extends TranslatedElement, TTranslatedDest
       // And otherwise, exit this element with an exceptional edge
       not exists(this.getChild(id + 1)) and
       kind instanceof ExceptionEdge and
-      not kind.(ExceptionEdge).isSEH() and
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), true)
+      kind = exceptionEdge(false) and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), false)
     )
   }
 
@@ -3124,8 +3102,8 @@ abstract class TranslatedThrowExpr extends TranslatedNonConstantExpr {
       or
       not exists(this.getDestructors()) and
       kind instanceof ExceptionEdge and
-      not kind.(ExceptionEdge).isSEH() and
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), true)
+      kind = exceptionEdge(false) and
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), false)
     )
   }
 
@@ -3413,13 +3391,7 @@ class TranslatedVarArgsStart extends TranslatedNonConstantExpr {
     result = this.getVAList().getFirstInstruction(kind)
     or
     tag = VarArgsVAListStoreTag() and
-    (
-      result = this.getParent().getChildSuccessor(this, kind)
-      or
-      // All store instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
-      kind.(ExceptionEdge).isSEH()
-    )
+    result = this.getParent().getChildSuccessor(this, kind)
   }
 
   final override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
@@ -3489,13 +3461,7 @@ class TranslatedVarArg extends TranslatedNonConstantExpr {
 
   final override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = VarArgsVAListLoadTag() and
-    (
-      kind instanceof GotoEdge and result = this.getInstruction(VarArgsArgAddressTag())
-      or
-      // All load instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
-      kind.(ExceptionEdge).isSEH()
-    )
+    (kind instanceof GotoEdge and result = this.getInstruction(VarArgsArgAddressTag()))
     or
     tag = VarArgsArgAddressTag() and
     kind instanceof GotoEdge and
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll
index d41a18c25b11..b647bbab2122 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll
@@ -230,8 +230,8 @@ class TranslatedFunction extends TranslatedRootElement, TTranslatedFunction {
 
   final override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSEH) {
     // only unwind for C++ exceptions since SEH exceptions are too verbose
-    // and would generate unwind for all functions. 
-    isSEH = false and 
+    // and would generate unwind for all functions.
+    isSEH = false and
     result = this.getInstruction(UnwindTag()) and
     kind instanceof GotoEdge
   }

From fcff6071330dfea70fac1f42d238b04b8cf414a9 Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Tue, 15 Oct 2024 12:43:28 -0400
Subject: [PATCH 09/22] PR review corrections.

---
 .../raw/internal/TranslatedDeclarationEntry.qll      |  6 ++----
 .../implementation/raw/internal/TranslatedExpr.qll   |  1 -
 .../raw/internal/TranslatedFunction.qll              | 12 ++++--------
 .../implementation/raw/internal/TranslatedStmt.qll   |  4 ----
 4 files changed, 6 insertions(+), 17 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll
index 1dc1eed9f6a3..c0fe9cd2207d 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedDeclarationEntry.qll
@@ -165,10 +165,8 @@ class TranslatedStaticLocalVariableDeclarationEntry extends TranslatedDeclaratio
     result = this.getInstruction(DynamicInitializationFlagLoadTag())
     or
     tag = DynamicInitializationFlagLoadTag() and
-    (
-      kind instanceof GotoEdge and
-      result = this.getInstruction(DynamicInitializationConditionalBranchTag())
-    )
+    kind instanceof GotoEdge and
+    result = this.getInstruction(DynamicInitializationConditionalBranchTag())
     or
     tag = DynamicInitializationConditionalBranchTag() and
     (
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
index 68f341950372..e6e0c861c962 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
@@ -3061,7 +3061,6 @@ class TranslatedDestructorsAfterThrow extends TranslatedElement, TTranslatedDest
       or
       // And otherwise, exit this element with an exceptional edge
       not exists(this.getChild(id + 1)) and
-      kind instanceof ExceptionEdge and
       kind = exceptionEdge(false) and
       result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), false)
     )
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll
index b647bbab2122..d53bd9328449 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll
@@ -214,7 +214,8 @@ class TranslatedFunction extends TranslatedRootElement, TTranslatedFunction {
         exists(ThrowExpr throw | throw.getEnclosingFunction() = func)
         or
         exists(FunctionCall call | call.getEnclosingFunction() = func |
-          getTranslatedExpr(call).(TranslatedCallExpr).mayRaiseException(_)
+          getTranslatedExpr(call).(TranslatedCallExpr).mayRaiseException(_) or
+          getTranslatedExpr(call).(TranslatedCallExpr).alwaysRaiseException(_)
         )
       )
       or
@@ -405,13 +406,8 @@ abstract class TranslatedParameter extends TranslatedElement {
     else result = this.getParent().getChildSuccessor(this, kind)
     or
     tag = InitializerIndirectAddressTag() and
-    (
-      result = this.getInstruction(InitializerIndirectStoreTag()) and kind instanceof GotoEdge
-      or
-      // All load instructions can throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
-      kind.(ExceptionEdge).isSEH()
-    )
+    result = this.getInstruction(InitializerIndirectStoreTag()) and
+    kind instanceof GotoEdge
     or
     tag = InitializerIndirectStoreTag() and
     result = this.getParent().getChildSuccessor(this, kind)
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
index f2f087ba39c2..cc12900c10cd 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
@@ -229,7 +229,6 @@ class TranslatedMicrosoftTryExceptHandler extends TranslatedElement,
   override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSEH) {
     // A throw from within a `__except` block flows to the handler for the parent of
     // the `__try`.
-    isSEH = true and
     result = this.getParent().getParent().getExceptionSuccessorInstruction(kind, isSEH)
   }
 }
@@ -286,7 +285,6 @@ class TranslatedMicrosoftTryFinallyHandler extends TranslatedElement,
   override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSEH) {
     // A throw from within a `__finally` block flows to the handler for the parent of
     // the `__try`.
-    isSEH = true and
     result = this.getParent().getParent().getExceptionSuccessorInstruction(kind, isSEH)
   }
 }
@@ -844,7 +842,6 @@ abstract class TranslatedHandler extends TranslatedStmt {
   override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSEH) {
     // A throw from within a `catch` block flows to the handler for the parent of
     // the `try`.
-    isSEH = false and
     result = this.getParent().getParent().getExceptionSuccessorInstruction(kind, isSEH)
   }
 
@@ -954,7 +951,6 @@ class TranslatedCatchByTypeHandler extends TranslatedHandler {
       result = this.getParameter().getFirstInstruction(kind)
       or
       kind instanceof ExceptionEdge and
-      not kind.(ExceptionEdge).isSEH() and
       if exists(this.getDestructors())
       then result = this.getDestructors().getFirstInstruction(any(GotoEdge edge))
       else result = this.getParent().(TranslatedTryStmt).getNextHandler(this, any(GotoEdge edge))

From fdf5ac6ec3b5727399252d00a6fb96abf7ab6158 Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Wed, 23 Oct 2024 13:56:19 -0400
Subject: [PATCH 10/22] Formatting.

---
 .../code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
index e6e0c861c962..bcdc4843acf7 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
@@ -3460,7 +3460,8 @@ class TranslatedVarArg extends TranslatedNonConstantExpr {
 
   final override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = VarArgsVAListLoadTag() and
-    (kind instanceof GotoEdge and result = this.getInstruction(VarArgsArgAddressTag()))
+    kind instanceof GotoEdge and
+    result = this.getInstruction(VarArgsArgAddressTag())
     or
     tag = VarArgsArgAddressTag() and
     kind instanceof GotoEdge and

From a0535195ea7089705bbdecdb71dc2b830a612478 Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Wed, 23 Oct 2024 14:00:26 -0400
Subject: [PATCH 11/22] Removing SEH load exceptions for var args and lambda
 translations

---
 .../raw/internal/TranslatedExpr.qll           | 32 +++----------------
 1 file changed, 4 insertions(+), 28 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
index bcdc4843acf7..632b211e97c4 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
@@ -3472,13 +3472,7 @@ class TranslatedVarArg extends TranslatedNonConstantExpr {
     result = this.getInstruction(VarArgsVAListStoreTag())
     or
     tag = VarArgsVAListStoreTag() and
-    (
-      result = this.getParent().getChildSuccessor(this, kind)
-      or
-      // All store instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
-      kind.(ExceptionEdge).isSEH()
-    )
+    result = this.getParent().getChildSuccessor(this, kind)
   }
 
   final override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
@@ -3600,22 +3594,10 @@ class TranslatedVarArgCopy extends TranslatedNonConstantExpr {
 
   final override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
     tag = VarArgsVAListLoadTag() and
-    (
-      result = this.getDestinationVAList().getFirstInstruction(kind)
-      or
-      // All load instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
-      kind.(ExceptionEdge).isSEH()
-    )
+    result = this.getDestinationVAList().getFirstInstruction(kind)
     or
     tag = VarArgsVAListStoreTag() and
-    (
-      result = this.getParent().getChildSuccessor(this, kind)
-      or
-      // All store instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
-      kind.(ExceptionEdge).isSEH()
-    )
+    result = this.getParent().getChildSuccessor(this, kind)
   }
 
   final override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {
@@ -3819,13 +3801,7 @@ class TranslatedLambdaExpr extends TranslatedNonConstantExpr, InitializationCont
     )
     or
     tag = LoadTag() and
-    (
-      result = this.getParent().getChildSuccessor(this, kind)
-      or
-      // All load instruction could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
-      kind.(ExceptionEdge).isSEH()
-    )
+    result = this.getParent().getChildSuccessor(this, kind)
   }
 
   override Instruction getChildSuccessorInternal(TranslatedElement child, EdgeKind kind) {

From e86c7644d8a39f95f97d24f93c6db403191a9b99 Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Wed, 23 Oct 2024 14:02:49 -0400
Subject: [PATCH 12/22] Updated comments and formatting.

---
 .../implementations/StructuredExceptionHandling.qll   | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll
index d4524adeb113..eac70ddd602a 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll
@@ -1,7 +1,8 @@
 import semmle.code.cpp.models.interfaces.Throwing
 
 /**
- * The default behavior for SEH is any function may (conditionally) raise an exception.
+ * The default behavior for Structured Exception Handling (SEH) is 
+ * any function may (conditionally) raise an exception.
  * NOTE: this can be overriden by for any specific function to make in
  * unconditional or non-throwing. IR generation will enforce
  * the most strict interpretation.
@@ -9,9 +10,7 @@ import semmle.code.cpp.models.interfaces.Throwing
 class DefaultSEHExceptionBehavior extends ThrowingFunction {
   DefaultSEHExceptionBehavior() { this = any(Function f) }
 
-  override predicate raisesException(boolean unconditional) { 
-    unconditional = false
-  }
+  override predicate raisesException(boolean unconditional) { unconditional = false }
 
   override TSEHException getExceptionType() { any() }
 }
@@ -21,9 +20,7 @@ class WindowsDriverExceptionAnnotation extends ThrowingFunction {
     this.hasGlobalName(["RaiseException", "ExRaiseAccessViolation", "ExRaiseDatatypeMisalignment"])
   }
 
-  override predicate raisesException(boolean unconditional) { 
-    unconditional = true
-  }
+  override predicate raisesException(boolean unconditional) { unconditional = true }
 
   override TSEHException getExceptionType() { any() }
 }

From a40343e92e9c98cf73e6970cd6d103d02f47abd2 Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Wed, 23 Oct 2024 14:12:32 -0400
Subject: [PATCH 13/22] Updating comments.

---
 .../code/cpp/models/interfaces/Throwing.qll       | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
index cab7e18a2599..7a37f1e0ab6d 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
@@ -20,11 +20,15 @@ newtype TException =
  * to use the most restricted interpretation, meaning taking options
  * that stipulate no exception is raised, before the exception is always raised,
  * before conditional exceptions.
- * 
+ *
  * Annotations must specify if the exception is from SEH (structured exception handling)
  * or ordinary c++ exceptions.
  */
-private abstract class ExceptionAnnotation extends Function {
+abstract private class ExceptionAnnotation extends Function {
+  /**
+   * Returns the type of exception this annotation is for,
+   * either a CPP exception or a STructured Exception Handling (SEH) exception.
+   */
   abstract TException getExceptionType();
 
   final predicate isSEH() { this.getExceptionType() = TSEHException() }
@@ -50,7 +54,14 @@ abstract class ThrowingFunction extends ExceptionAnnotation {
    */
   abstract predicate raisesException(boolean unconditional);
 
+  /**
+   * Holds if this function will always raise an exception if called
+   */
   final predicate alwaysRaisesException() { this.raisesException(true) }
 
+  /**
+   * Holds if this function may raise an exception if called but
+   * it is not guaranteed to do so. I.e., the function does not always raise an exception.
+   */
   final predicate mayRaiseException() { this.raisesException(false) }
 }

From cc4b280ad0d9e5ffb7d7ed0752d32029aa997b67 Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Wed, 23 Oct 2024 15:26:09 -0400
Subject: [PATCH 14/22] Comments and changed char pred (moved up to abstract
 class)

---
 .../implementations/StructuredExceptionHandling.qll  |  4 ++--
 .../semmle/code/cpp/models/interfaces/Throwing.qll   | 12 ++++++++++++
 2 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll
index eac70ddd602a..f455dd660852 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll
@@ -1,14 +1,14 @@
 import semmle.code.cpp.models.interfaces.Throwing
 
 /**
- * The default behavior for Structured Exception Handling (SEH) is 
+ * The default behavior for Structured Exception Handling (SEH) is
  * any function may (conditionally) raise an exception.
  * NOTE: this can be overriden by for any specific function to make in
  * unconditional or non-throwing. IR generation will enforce
  * the most strict interpretation.
  */
 class DefaultSEHExceptionBehavior extends ThrowingFunction {
-  DefaultSEHExceptionBehavior() { this = any(Function f) }
+  DefaultSEHExceptionBehavior() { any() }
 
   override predicate raisesException(boolean unconditional) { unconditional = false }
 
diff --git a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
index 7a37f1e0ab6d..83316a42b5b6 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
@@ -10,6 +10,10 @@ import semmle.code.cpp.Function
 import semmle.code.cpp.models.Models
 import semmle.code.cpp.models.interfaces.FunctionInputsAndOutputs
 
+/**
+ * Represents a type of exception,
+ * either Structure Exception Handling (SEH) or C++ exceptions.
+ */
 newtype TException =
   TSEHException() or
   TCxxException()
@@ -31,8 +35,14 @@ abstract private class ExceptionAnnotation extends Function {
    */
   abstract TException getExceptionType();
 
+  /**
+   * Holds if the exception type of this annotation is for a Structure Exception Handling (SEH) exception.
+   */
   final predicate isSEH() { this.getExceptionType() = TSEHException() }
 
+  /**
+   * Holds if the exception type of this annotation is for a CPP exception.
+   */
   final predicate isCxx() { this.getExceptionType() = TCxxException() }
 }
 
@@ -45,6 +55,8 @@ abstract class NonThrowingFunction extends ExceptionAnnotation { }
  * Functions that are known to raise an exception.
  */
 abstract class ThrowingFunction extends ExceptionAnnotation {
+  ThrowingFunction() { this instanceof Function }
+
   /**
    * Holds if this function may raise an exception during evaluation.
    * If `conditional` is `false` the function may raise, and if `true` the function

From fb16db29d768c68c98e82d3513f52b01624bebdf Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Wed, 23 Oct 2024 15:27:58 -0400
Subject: [PATCH 15/22] Formatting.

---
 .../raw/internal/TranslatedElement.qll            |  4 ++--
 .../raw/internal/TranslatedInitialization.qll     | 15 +++++++++------
 .../code/cpp/models/implementations/Strcpy.qll    |  2 +-
 3 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedElement.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedElement.qll
index 4774a1eb2409..3c3f211001f7 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedElement.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedElement.qll
@@ -1104,9 +1104,9 @@ abstract class TranslatedElement extends TTranslatedElement {
    * within this element. This will generally return first `catch` block of the
    * nearest enclosing `try`, or the `Unwind` instruction for the function if
    * there is no enclosing `try`. The successor edge kind is specified by `kind`.
-   * 
+   *
    * `isSEH` is true if the exception is a structured exception, false if otherwise.
-   * The boolean value can be extracted from `ExceptionEdge` from the exception 
+   * The boolean value can be extracted from `ExceptionEdge` from the exception
    * edge triggering the call to this function.
    */
   Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSEH) {
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll
index 3748b33e2abf..663d0ef87655 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll
@@ -285,7 +285,8 @@ class TranslatedSimpleDirectInitialization extends TranslatedDirectInitializatio
       result = this.getParent().getChildSuccessor(this, kind)
       or
       // All store instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and kind.(ExceptionEdge).isSEH()
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
+      kind.(ExceptionEdge).isSEH()
     )
   }
 
@@ -362,13 +363,13 @@ class TranslatedStringLiteralInitialization extends TranslatedDirectInitializati
   }
 
   override Instruction getInstructionSuccessorInternal(InstructionTag tag, EdgeKind kind) {
-   
     tag = InitializerLoadStringTag() and
     (
-      result = this.getInstruction(InitializerStoreTag())  and kind instanceof GotoEdge
+      result = this.getInstruction(InitializerStoreTag()) and kind instanceof GotoEdge
       or
       // All store instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and kind.(ExceptionEdge).isSEH()
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
+      kind.(ExceptionEdge).isSEH()
     )
     or
     if this.zeroInitRange(_, _)
@@ -664,7 +665,8 @@ class TranslatedFieldValueInitialization extends TranslatedFieldInitialization,
       result = this.getParent().getChildSuccessor(this, kind)
       or
       // All store instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and kind.(ExceptionEdge).isSEH()
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
+      kind.(ExceptionEdge).isSEH()
     )
   }
 
@@ -869,7 +871,8 @@ class TranslatedElementValueInitialization extends TranslatedElementInitializati
       result = this.getParent().getChildSuccessor(this, kind)
       or
       // All store instructions could throw an SEH exception
-      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and kind.(ExceptionEdge).isSEH()
+      result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
+      kind.(ExceptionEdge).isSEH()
     )
   }
 
diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcpy.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcpy.qll
index f548ff648fd0..b09cbeb8dc60 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcpy.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/Strcpy.qll
@@ -13,7 +13,7 @@ import semmle.code.cpp.models.interfaces.Throwing
  * The standard function `strcpy` and its wide, sized, and Microsoft variants.
  */
 class StrcpyFunction extends ArrayFunction, DataFlowFunction, TaintFunction, SideEffectFunction,
-NonThrowingFunction
+  NonThrowingFunction
 {
   StrcpyFunction() {
     this.hasGlobalOrStdOrBslName([

From 781a9b73fe463f0786f680a1aaaf2d3646458a2d Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Wed, 23 Oct 2024 15:29:22 -0400
Subject: [PATCH 16/22] Typo

---
 cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
index 83316a42b5b6..738b4165342f 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
@@ -19,7 +19,7 @@ newtype TException =
   TCxxException()
 
 /**
- * Functions with information about how an exception is throwwn or if one is thrown at all.
+ * Functions with information about how an exception is thrown or if one is thrown at all.
  * If throwing details conflict for the same function, IR is assumed
  * to use the most restricted interpretation, meaning taking options
  * that stipulate no exception is raised, before the exception is always raised,

From a498c87cf48d91b799be69fce3ca1d9cb95b4689 Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Thu, 24 Oct 2024 09:41:20 -0400
Subject: [PATCH 17/22] adding change log

---
 .../2024-10-24-ir-seh-exception-handling-updates.md           | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 cpp/ql/lib/change-notes/2024-10-24-ir-seh-exception-handling-updates.md

diff --git a/cpp/ql/lib/change-notes/2024-10-24-ir-seh-exception-handling-updates.md b/cpp/ql/lib/change-notes/2024-10-24-ir-seh-exception-handling-updates.md
new file mode 100644
index 000000000000..c68fdb91c717
--- /dev/null
+++ b/cpp/ql/lib/change-notes/2024-10-24-ir-seh-exception-handling-updates.md
@@ -0,0 +1,4 @@
+---
+category: minorAnalysis
+---
+* Added support for structured exception handling (SEH). As a result, dataflow queries may have more results in code bases that use SEH.
\ No newline at end of file

From 61b1fef7f0bc0cd635805a61d75bfd0d139560f6 Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Thu, 24 Oct 2024 09:50:10 -0400
Subject: [PATCH 18/22] Comments

---
 cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
index 738b4165342f..06e8adbfa313 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
@@ -15,7 +15,9 @@ import semmle.code.cpp.models.interfaces.FunctionInputsAndOutputs
  * either Structure Exception Handling (SEH) or C++ exceptions.
  */
 newtype TException =
+  // Structure Exception Handling (SEH) exception
   TSEHException() or
+  // C++ exception
   TCxxException()
 
 /**

From f85ba7a16a507c323ff9dd25b9c19e2d53b7259c Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Thu, 24 Oct 2024 10:14:44 -0400
Subject: [PATCH 19/22] Updating docs

---
 cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
index 06e8adbfa313..2d18cfa74e0e 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
@@ -15,9 +15,9 @@ import semmle.code.cpp.models.interfaces.FunctionInputsAndOutputs
  * either Structure Exception Handling (SEH) or C++ exceptions.
  */
 newtype TException =
-  // Structure Exception Handling (SEH) exception
+  /** Structure Exception Handling (SEH) exception */
   TSEHException() or
-  // C++ exception
+  /** C++ exception */
   TCxxException()
 
 /**

From 9dc776ede950c2b9cc18b8ad5453c552865d0444 Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Thu, 24 Oct 2024 10:40:40 -0400
Subject: [PATCH 20/22] Type in comments.

---
 cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
index 2d18cfa74e0e..cb995f743bff 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
@@ -12,10 +12,10 @@ import semmle.code.cpp.models.interfaces.FunctionInputsAndOutputs
 
 /**
  * Represents a type of exception,
- * either Structure Exception Handling (SEH) or C++ exceptions.
+ * either Structured Exception Handling (SEH) or C++ exceptions.
  */
 newtype TException =
-  /** Structure Exception Handling (SEH) exception */
+  /** Structured Exception Handling (SEH) exception */
   TSEHException() or
   /** C++ exception */
   TCxxException()
@@ -38,7 +38,7 @@ abstract private class ExceptionAnnotation extends Function {
   abstract TException getExceptionType();
 
   /**
-   * Holds if the exception type of this annotation is for a Structure Exception Handling (SEH) exception.
+   * Holds if the exception type of this annotation is for a Structured Exception Handling (SEH) exception.
    */
   final predicate isSEH() { this.getExceptionType() = TSEHException() }
 

From 3f01e4d65732a27e33aefca683b00af5c35a1165 Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Thu, 24 Oct 2024 13:24:15 -0400
Subject: [PATCH 21/22] changing isSEH to isSeh to match conventions.

---
 .../code/cpp/ir/implementation/EdgeKind.qll   | 14 ++---
 .../raw/internal/TranslatedCall.qll           | 52 +++++++++----------
 .../raw/internal/TranslatedElement.qll        |  6 +--
 .../raw/internal/TranslatedExpr.qll           | 18 +++----
 .../raw/internal/TranslatedFunction.qll       |  4 +-
 .../raw/internal/TranslatedInitialization.qll |  8 +--
 .../raw/internal/TranslatedStmt.qll           | 26 +++++-----
 .../code/cpp/models/interfaces/Throwing.qll   |  2 +-
 8 files changed, 65 insertions(+), 65 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll
index 51d95604d0a7..0dd16c6dd6b9 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/EdgeKind.qll
@@ -9,7 +9,7 @@ private newtype TEdgeKind =
   TGotoEdge() or // Single successor (including fall-through)
   TTrueEdge() or // 'true' edge of conditional branch
   TFalseEdge() or // 'false' edge of conditional branch
-  TExceptionEdge(Boolean isSEH) or // Thrown exception, true for SEH exceptions, false otherwise
+  TExceptionEdge(Boolean isSeh) or // Thrown exception, true for SEH exceptions, false otherwise
   TDefaultEdge() or // 'default' label of switch
   TCaseEdge(string minValue, string maxValue) {
     // Case label of switch
@@ -55,17 +55,17 @@ class FalseEdge extends EdgeKind, TFalseEdge {
  * instruction's evaluation throws an exception.
  */
 class ExceptionEdge extends EdgeKind, TExceptionEdge {
-  boolean isSEH; //true for Structured Exception Handling, false for C++ exceptions
+  boolean isSeh; //true for Structured Exception Handling, false for C++ exceptions
 
-  ExceptionEdge() { this = TExceptionEdge(isSEH) }
+  ExceptionEdge() { this = TExceptionEdge(isSeh) }
 
   /**
    * Holds if the exception is a Structured Exception Handling (SEH) exception.
    */
-  final predicate isSEH() { isSEH = true }
+  final predicate isSeh() { isSeh = true }
 
   final override string toString() {
-    if isSEH = true then result = "SEH Exception" else result = "C++ Exception"
+    if isSeh = true then result = "SEH Exception" else result = "C++ Exception"
   }
 }
 
@@ -134,9 +134,9 @@ module EdgeKind {
 
   /**
    * Gets the instance of the `ExceptionEdge` class.
-   * `isSEH` is true if the exception is an SEH exception, and false for a C++ edge.
+   * `isSeh` is true if the exception is an SEH exception, and false for a C++ edge.
    */
-  ExceptionEdge exceptionEdge(boolean isSEH) { result = TExceptionEdge(isSEH) }
+  ExceptionEdge exceptionEdge(boolean isSeh) { result = TExceptionEdge(isSeh) }
 
   /**
    * Gets the single instance of the `DefaultEdge` class.
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
index 28c57b345af8..d03b753d8c43 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
@@ -85,28 +85,28 @@ abstract class TranslatedCall extends TranslatedExpr {
           this.getEnclosingFunction().getFunction() = instr.getEnclosingFunction()
         )
     else
-      exists(boolean isSEH | kind = exceptionEdge(isSEH) |
+      exists(boolean isSeh | kind = exceptionEdge(isSeh) |
         // Call throw behavior is resolved from most restricted to least restricted in order
         // if there are conflicting throwing specificaitons for a function.
         // Enumerating all scenarios to be explicit.
         (
           // If the call is known to never throw, regardless of other defined throwing behavior,
           // do not generate any exception edges, only an ordinary successor
-          if this.(TranslatedCallExpr).neverRaiseException(isSEH)
+          if this.(TranslatedCallExpr).neverRaiseException(isSeh)
           then result = this.getParent().getChildSuccessor(this, any(GotoEdge edge))
           else
             // If the call is known to always throw, regardless of other defined throwing behavior,
             // only generate an exception edge.
-            if this.(TranslatedCallExpr).alwaysRaiseException(isSEH)
+            if this.(TranslatedCallExpr).alwaysRaiseException(isSeh)
             then
-              result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), isSEH)
+              result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), isSeh)
             else
-              if this.(TranslatedCallExpr).mayRaiseException(isSEH)
+              if this.(TranslatedCallExpr).mayRaiseException(isSeh)
               then (
                 // if the call is known to conditionally throw, generate both an exception edge and an
                 // ordinary successor
                 result =
-                  this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), isSEH)
+                  this.getParent().getExceptionSuccessorInstruction(any(GotoEdge edge), isSeh)
                 or
                 result = this.getParent().getChildSuccessor(this, kind)
               ) else
@@ -145,7 +145,7 @@ abstract class TranslatedCall extends TranslatedExpr {
    * and `neverRaiseException` may conflict (e.g., all hold for a given target).
    * Conflicting results are resolved during IR generation.
    */
-  abstract predicate alwaysRaiseException(boolean isSEH);
+  abstract predicate alwaysRaiseException(boolean isSeh);
 
   /**
    * The call target is known to conditionally raise an exception.
@@ -153,7 +153,7 @@ abstract class TranslatedCall extends TranslatedExpr {
    * and `neverRaiseException` may conflict (e.g., all hold for a given target).
    * Conflicting results are resolved during IR generation.
    */
-  abstract predicate mayRaiseException(boolean isSEH);
+  abstract predicate mayRaiseException(boolean isSeh);
 
   /**
    * The call target is known to never raise an exception.
@@ -161,7 +161,7 @@ abstract class TranslatedCall extends TranslatedExpr {
    * and `neverRaiseException` may conflict (e.g., all hold for a given target).
    * Conflicting results are resolved during IR generation.
    */
-  abstract predicate neverRaiseException(boolean isSEH);
+  abstract predicate neverRaiseException(boolean isSeh);
 
   /**
    * Gets the result type of the call.
@@ -362,27 +362,27 @@ abstract class TranslatedCallExpr extends TranslatedNonConstantExpr, TranslatedC
     tag = CallTargetTag() and result = expr.getTarget()
   }
 
-  override predicate alwaysRaiseException(boolean isSEH) {
+  override predicate alwaysRaiseException(boolean isSeh) {
     exists(ThrowingFunction f | f = expr.getTarget() |
-      f.alwaysRaisesException() and f.isSEH() and isSEH = true
+      f.alwaysRaisesException() and f.isSeh() and isSeh = true
       or
-      f.alwaysRaisesException() and f.isCxx() and isSEH = false
+      f.alwaysRaisesException() and f.isCxx() and isSeh = false
     )
   }
 
-  override predicate mayRaiseException(boolean isSEH) {
+  override predicate mayRaiseException(boolean isSeh) {
     exists(ThrowingFunction f | f = expr.getTarget() |
-      f.mayRaiseException() and f.isSEH() and isSEH = true
+      f.mayRaiseException() and f.isSeh() and isSeh = true
       or
-      f.mayRaiseException() and f.isCxx() and isSEH = false
+      f.mayRaiseException() and f.isCxx() and isSeh = false
     )
   }
 
-  override predicate neverRaiseException(boolean isSEH) {
+  override predicate neverRaiseException(boolean isSeh) {
     exists(NonThrowingFunction f | f = expr.getTarget() |
-      f.isSEH() and isSEH = true
+      f.isSeh() and isSeh = true
       or
-      f.isCxx() and isSEH = false
+      f.isCxx() and isSeh = false
     )
   }
 }
@@ -397,7 +397,7 @@ class TranslatedExprCall extends TranslatedCallExpr {
     result = getTranslatedExpr(expr.getExpr().getFullyConverted())
   }
 
-  override predicate alwaysRaiseException(boolean isSEH) {
+  override predicate alwaysRaiseException(boolean isSeh) {
     // We assume that a call to a function pointer will not throw a CXX exception.
     // This is not sound in general, but this will greatly reduce the number of
     // exceptional edges.
@@ -405,11 +405,11 @@ class TranslatedExprCall extends TranslatedCallExpr {
     // if no throwing function is found, assume a conditional SEH exception
     // see `mayRaiseException`
     exists(ThrowingFunction f | f = expr.getTarget() |
-      f.alwaysRaisesException() and f.isSEH() and isSEH = true
+      f.alwaysRaisesException() and f.isSeh() and isSeh = true
     )
   }
 
-  override predicate mayRaiseException(boolean isSEH) {
+  override predicate mayRaiseException(boolean isSeh) {
     // We assume that a call to a function pointer will not throw a CXX exception.
     // This is not sound in general, but this will greatly reduce the number of
     // exceptional edges.
@@ -417,21 +417,21 @@ class TranslatedExprCall extends TranslatedCallExpr {
     // ASSUMPTION: if no ThrowingFunction is found for the given call, assume a conditional SEH exception
     // on the call.
     exists(ThrowingFunction f | f = expr.getTarget() |
-      f.mayRaiseException() and f.isSEH() and isSEH = true
+      f.mayRaiseException() and f.isSeh() and isSeh = true
     )
     or
-    not exists(ThrowingFunction f | f = expr.getTarget() and f.isSEH()) and
-    isSEH = true
+    not exists(ThrowingFunction f | f = expr.getTarget() and f.isSeh()) and
+    isSeh = true
   }
 
-  override predicate neverRaiseException(boolean isSEH) {
+  override predicate neverRaiseException(boolean isSeh) {
     // We assume that a call to a function pointer will not throw a CXX exception.
     // This is not sound in general, but this will greatly reduce the number of
     // exceptional edges.
     // For SEH exceptions, use the defined ThrowingFunction behavior and
     // if no throwing function is found, assume a conditional SEH exception
     // see `mayRaiseException`
-    exists(NonThrowingFunction f | f = expr.getTarget() | f.isSEH() and isSEH = true)
+    exists(NonThrowingFunction f | f = expr.getTarget() | f.isSeh() and isSeh = true)
   }
 }
 
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedElement.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedElement.qll
index 3c3f211001f7..0dd6ec99a192 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedElement.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedElement.qll
@@ -1105,12 +1105,12 @@ abstract class TranslatedElement extends TTranslatedElement {
    * nearest enclosing `try`, or the `Unwind` instruction for the function if
    * there is no enclosing `try`. The successor edge kind is specified by `kind`.
    *
-   * `isSEH` is true if the exception is a structured exception, false if otherwise.
+   * `isSeh` is true if the exception is a structured exception, false if otherwise.
    * The boolean value can be extracted from `ExceptionEdge` from the exception
    * edge triggering the call to this function.
    */
-  Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSEH) {
-    result = this.getParent().getExceptionSuccessorInstruction(kind, isSEH)
+  Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSeh) {
+    result = this.getParent().getExceptionSuccessorInstruction(kind, isSeh)
   }
 
   /**
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
index 632b211e97c4..d9c2dede732f 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedExpr.qll
@@ -397,7 +397,7 @@ class TranslatedLoad extends TranslatedValueCategoryAdjustment, TTranslatedLoad
       or
       // All load instructions could throw an SEH exception
       result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
-      kind.(ExceptionEdge).isSEH()
+      kind.(ExceptionEdge).isSeh()
     )
   }
 
@@ -1095,7 +1095,7 @@ class TranslatedStructuredBindingVariableAccess extends TranslatedNonConstantExp
       or
       // All load instructions could throw an SEH exception
       result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
-      kind.(ExceptionEdge).isSEH()
+      kind.(ExceptionEdge).isSeh()
     )
   }
 
@@ -1916,7 +1916,7 @@ class TranslatedBlockAssignExpr extends TranslatedNonConstantExpr {
       or
       // All load instructions could throw an SEH exception
       result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
-      kind.(ExceptionEdge).isSEH()
+      kind.(ExceptionEdge).isSeh()
     )
     or
     tag = AssignmentStoreTag() and
@@ -2393,16 +2393,16 @@ class TranslatedAllocatorCall extends TTranslatedAllocatorCall, TranslatedDirect
         result = getTranslatedExpr(expr.getAllocatorCall().getArgument(index).getFullyConverted())
   }
 
-  final override predicate mayRaiseException(boolean isSEH) {
+  final override predicate mayRaiseException(boolean isSeh) {
     // We assume that a call to `new` or `new[]` will never throw. This is not
     // sound in general, but this will greatly reduce the number of exceptional
     // edges.
     none()
   }
 
-  final override predicate alwaysRaiseException(boolean isSEH) { none() }
+  final override predicate alwaysRaiseException(boolean isSeh) { none() }
 
-  final override predicate neverRaiseException(boolean isSEH) { none() }
+  final override predicate neverRaiseException(boolean isSeh) { none() }
 }
 
 TranslatedAllocatorCall getTranslatedAllocatorCall(NewOrNewArrayExpr newExpr) {
@@ -2468,16 +2468,16 @@ class TranslatedDeleteOrDeleteArrayExpr extends TranslatedNonConstantExpr, Trans
     result = getTranslatedExpr(expr.getExprWithReuse().getFullyConverted())
   }
 
-  final override predicate mayRaiseException(boolean isSEH) {
+  final override predicate mayRaiseException(boolean isSeh) {
     // We assume that a call to `delete` or `delete[]` will never throw. This is not
     // sound in general, but this will greatly reduce the number of exceptional
     // edges.
     none()
   }
 
-  final override predicate alwaysRaiseException(boolean isSEH) { none() }
+  final override predicate alwaysRaiseException(boolean isSeh) { none() }
 
-  final override predicate neverRaiseException(boolean isSEH) { none() }
+  final override predicate neverRaiseException(boolean isSeh) { none() }
 }
 
 TranslatedDeleteOrDeleteArrayExpr getTranslatedDeleteOrDeleteArray(DeleteOrDeleteArrayExpr newExpr) {
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll
index d53bd9328449..beccc7f3a839 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedFunction.qll
@@ -229,10 +229,10 @@ class TranslatedFunction extends TranslatedRootElement, TTranslatedFunction {
     )
   }
 
-  final override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSEH) {
+  final override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSeh) {
     // only unwind for C++ exceptions since SEH exceptions are too verbose
     // and would generate unwind for all functions.
-    isSEH = false and
+    isSeh = false and
     result = this.getInstruction(UnwindTag()) and
     kind instanceof GotoEdge
   }
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll
index 663d0ef87655..46b43571e3c3 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedInitialization.qll
@@ -286,7 +286,7 @@ class TranslatedSimpleDirectInitialization extends TranslatedDirectInitializatio
       or
       // All store instructions could throw an SEH exception
       result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
-      kind.(ExceptionEdge).isSEH()
+      kind.(ExceptionEdge).isSeh()
     )
   }
 
@@ -369,7 +369,7 @@ class TranslatedStringLiteralInitialization extends TranslatedDirectInitializati
       or
       // All store instructions could throw an SEH exception
       result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
-      kind.(ExceptionEdge).isSEH()
+      kind.(ExceptionEdge).isSeh()
     )
     or
     if this.zeroInitRange(_, _)
@@ -666,7 +666,7 @@ class TranslatedFieldValueInitialization extends TranslatedFieldInitialization,
       or
       // All store instructions could throw an SEH exception
       result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
-      kind.(ExceptionEdge).isSEH()
+      kind.(ExceptionEdge).isSeh()
     )
   }
 
@@ -872,7 +872,7 @@ class TranslatedElementValueInitialization extends TranslatedElementInitializati
       or
       // All store instructions could throw an SEH exception
       result = this.getParent().getExceptionSuccessorInstruction(any(GotoEdge e), true) and
-      kind.(ExceptionEdge).isSEH()
+      kind.(ExceptionEdge).isSeh()
     )
   }
 
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
index cc12900c10cd..1603e9e8ca7b 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedStmt.qll
@@ -226,10 +226,10 @@ class TranslatedMicrosoftTryExceptHandler extends TranslatedElement,
 
   final override Function getFunction() { result = tryExcept.getEnclosingFunction() }
 
-  override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSEH) {
+  override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSeh) {
     // A throw from within a `__except` block flows to the handler for the parent of
     // the `__try`.
-    result = this.getParent().getParent().getExceptionSuccessorInstruction(kind, isSEH)
+    result = this.getParent().getParent().getExceptionSuccessorInstruction(kind, isSeh)
   }
 }
 
@@ -282,10 +282,10 @@ class TranslatedMicrosoftTryFinallyHandler extends TranslatedElement,
     result = getTranslatedStmt(tryFinally.getFinally())
   }
 
-  override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSEH) {
+  override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSeh) {
     // A throw from within a `__finally` block flows to the handler for the parent of
     // the `__try`.
-    result = this.getParent().getParent().getExceptionSuccessorInstruction(kind, isSEH)
+    result = this.getParent().getParent().getExceptionSuccessorInstruction(kind, isSeh)
   }
 }
 
@@ -734,25 +734,25 @@ class TranslatedTryStmt extends TranslatedStmt {
     // of the `try`, because the exception successor of the `try` itself is
     // the first catch clause.
     handler = this.getHandler(stmt.getNumberOfCatchClauses() - 1) and
-    exists(boolean isSEH |
-      stmt instanceof MicrosoftTryStmt and isSEH = true
+    exists(boolean isSeh |
+      stmt instanceof MicrosoftTryStmt and isSeh = true
       or
-      stmt instanceof TryStmt and isSEH = false
+      stmt instanceof TryStmt and isSeh = false
     |
-      result = this.getParent().getExceptionSuccessorInstruction(kind, isSEH)
+      result = this.getParent().getExceptionSuccessorInstruction(kind, isSeh)
     )
   }
 
-  final override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSEH) {
+  final override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSeh) {
     // SEH exceptions are only handled for SEH try statements and
     // C++ exceptions for C++ try statements.
     // I.e., we are assuming there isn't a mix and match between SEH and C++ exceptions.
     // They are either all SEH or all C++ within a single try block depending on the
     // try type (TryStmt vs MicrosoftTryStmt).
     (
-      stmt instanceof TryStmt and isSEH = false
+      stmt instanceof TryStmt and isSeh = false
       or
-      stmt instanceof MicrosoftTryStmt and isSEH = true
+      stmt instanceof MicrosoftTryStmt and isSeh = true
     ) and
     (
       result = this.getHandler(0).getFirstInstruction(kind)
@@ -839,10 +839,10 @@ abstract class TranslatedHandler extends TranslatedStmt {
     child = this.getBlock() and result = this.getParent().getChildSuccessor(this, kind)
   }
 
-  override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSEH) {
+  override Instruction getExceptionSuccessorInstruction(EdgeKind kind, boolean isSeh) {
     // A throw from within a `catch` block flows to the handler for the parent of
     // the `try`.
-    result = this.getParent().getParent().getExceptionSuccessorInstruction(kind, isSEH)
+    result = this.getParent().getParent().getExceptionSuccessorInstruction(kind, isSeh)
   }
 
   TranslatedStmt getBlock() { result = getTranslatedStmt(stmt.getBlock()) }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
index cb995f743bff..e62ebb89da15 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
@@ -40,7 +40,7 @@ abstract private class ExceptionAnnotation extends Function {
   /**
    * Holds if the exception type of this annotation is for a Structured Exception Handling (SEH) exception.
    */
-  final predicate isSEH() { this.getExceptionType() = TSEHException() }
+  final predicate isSeh() { this.getExceptionType() = TSEHException() }
 
   /**
    * Holds if the exception type of this annotation is for a CPP exception.

From 222c9f2db7aeb849297cfe57a3a76433e47ae905 Mon Sep 17 00:00:00 2001
From: "REDMOND\\brodes" <brodes@microsoft.com>
Date: Thu, 24 Oct 2024 14:35:39 -0400
Subject: [PATCH 22/22] Style changes.

---
 .../implementation/raw/internal/TranslatedCall.qll   |  4 ++--
 .../implementations/StructuredExceptionHandling.qll  | 10 +++++-----
 .../semmle/code/cpp/models/interfaces/Throwing.qll   | 12 ++++++------
 3 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
index d03b753d8c43..4aebcad423fc 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll
@@ -148,7 +148,7 @@ abstract class TranslatedCall extends TranslatedExpr {
   abstract predicate alwaysRaiseException(boolean isSeh);
 
   /**
-   * The call target is known to conditionally raise an exception.
+   * Holds when call target is known to conditionally raise an exception.
    * Note that `alwaysRaiseException`, `mayRaiseException`,
    * and `neverRaiseException` may conflict (e.g., all hold for a given target).
    * Conflicting results are resolved during IR generation.
@@ -156,7 +156,7 @@ abstract class TranslatedCall extends TranslatedExpr {
   abstract predicate mayRaiseException(boolean isSeh);
 
   /**
-   * The call target is known to never raise an exception.
+   * Holds when the call target is known to never raise an exception.
    * Note that `alwaysRaiseException`, `mayRaiseException`,
    * and `neverRaiseException` may conflict (e.g., all hold for a given target).
    * Conflicting results are resolved during IR generation.
diff --git a/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll b/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll
index f455dd660852..d5941488d0d7 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll
@@ -3,16 +3,16 @@ import semmle.code.cpp.models.interfaces.Throwing
 /**
  * The default behavior for Structured Exception Handling (SEH) is
  * any function may (conditionally) raise an exception.
- * NOTE: this can be overriden by for any specific function to make in
+ * NOTE: this can be overridden by for any specific function to make in
  * unconditional or non-throwing. IR generation will enforce
  * the most strict interpretation.
  */
-class DefaultSEHExceptionBehavior extends ThrowingFunction {
-  DefaultSEHExceptionBehavior() { any() }
+class DefaultSehExceptionBehavior extends ThrowingFunction {
+  DefaultSehExceptionBehavior() { any() }
 
   override predicate raisesException(boolean unconditional) { unconditional = false }
 
-  override TSEHException getExceptionType() { any() }
+  override TSehException getExceptionType() { any() }
 }
 
 class WindowsDriverExceptionAnnotation extends ThrowingFunction {
@@ -22,5 +22,5 @@ class WindowsDriverExceptionAnnotation extends ThrowingFunction {
 
   override predicate raisesException(boolean unconditional) { unconditional = true }
 
-  override TSEHException getExceptionType() { any() }
+  override TSehException getExceptionType() { any() }
 }
diff --git a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
index e62ebb89da15..72db8c9e96c7 100644
--- a/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
+++ b/cpp/ql/lib/semmle/code/cpp/models/interfaces/Throwing.qll
@@ -16,7 +16,7 @@ import semmle.code.cpp.models.interfaces.FunctionInputsAndOutputs
  */
 newtype TException =
   /** Structured Exception Handling (SEH) exception */
-  TSEHException() or
+  TSehException() or
   /** C++ exception */
   TCxxException()
 
@@ -40,7 +40,7 @@ abstract private class ExceptionAnnotation extends Function {
   /**
    * Holds if the exception type of this annotation is for a Structured Exception Handling (SEH) exception.
    */
-  final predicate isSeh() { this.getExceptionType() = TSEHException() }
+  final predicate isSeh() { this.getExceptionType() = TSehException() }
 
   /**
    * Holds if the exception type of this annotation is for a CPP exception.
@@ -49,19 +49,19 @@ abstract private class ExceptionAnnotation extends Function {
 }
 
 /**
- * Functions that are known to not throw an exception.
+ * A Function that is known to not throw an exception.
  */
 abstract class NonThrowingFunction extends ExceptionAnnotation { }
 
 /**
- * Functions that are known to raise an exception.
+ * A function this is known to raise an exception.
  */
 abstract class ThrowingFunction extends ExceptionAnnotation {
-  ThrowingFunction() { this instanceof Function }
+  ThrowingFunction() { any() }
 
   /**
    * Holds if this function may raise an exception during evaluation.
-   * If `conditional` is `false` the function may raise, and if `true` the function
+   * If `unconditional` is `false` the function may raise, and if `true` the function
    * will always raise an exception.
    * Do not specify `none()` if no exception is raised, instead use the
    * `NonThrowingFunction` class instead.