Adding model transition to using Throwing.qll.

Author: bdrodes

cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/internal/TranslatedCall.qll

@@ -363,11 +363,11 @@ class TranslatedFunctionCall extends TranslatedCallExpr, TranslatedDirectCall {
   }
 
   final override predicate mayThrowException() {
-    expr.getTarget().(ThrowingFunction).mayThrowException(_)
+    expr.getTarget().(ThrowingFunction).mayRaiseException()
   }
 
   final override predicate mustThrowException() {
-    expr.getTarget().(ThrowingFunction).mayThrowException(true)
+    expr.getTarget().(ThrowingFunction).alwaysRaisesException()
   }
 }
 

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"] }

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"] }

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() }
 }

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 = super.getFirstFormatArgumentIndex()
   }
+
+  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() }
 }

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() }
 }
 
 /**

cpp/ql/lib/semmle/code/cpp/models/implementations/Strcpy.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 `strcpy` and its wide, sized, and Microsoft variants.
@@ -145,4 +145,6 @@ class StrcpyFunction extends ArrayFunction, DataFlowFunction, TaintFunction, Sid
     i = this.getParamDest() and
     result = this.getParamSize()
   }
+
+  override TCxxException getExceptionType() { any() }
 }

cpp/ql/lib/semmle/code/cpp/models/implementations/StructuredExceptionHandling.qll

@@ -1,9 +1,26 @@
 import semmle.code.cpp.models.interfaces.Throwing
 
-class WindowsDriverFunction extends ThrowingFunction {
-  WindowsDriverFunction() {
+/**
+ * The default behavior for Structured Exception Handling (SEH) is
+ * any function may (conditionally) raise an exception.
+ * 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() }
+
+  override predicate raisesException(boolean unconditional) { unconditional = false }
+
+  override TSehException getExceptionType() { any() }
+}
+
+class WindowsDriverExceptionAnnotation extends ThrowingFunction {
+  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() }
 }

cpp/ql/lib/semmle/code/cpp/models/interfaces/NonThrowing.qll

@@ -11,12 +11,71 @@ import semmle.code.cpp.models.Models
 import semmle.code.cpp.models.interfaces.FunctionInputsAndOutputs
 
 /**
- * A class that models the exceptional behavior of a function.
+ * Represents a type of exception,
+ * either Structured Exception Handling (SEH) or C++ exceptions.
  */
-abstract class ThrowingFunction extends Function {
+newtype TException =
+  /** Structured Exception Handling (SEH) exception */
+  TSehException() or
+  /** C++ exception */
+  TCxxException()
+
+/**
+ * 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,
+ * before conditional exceptions.
+ *
+ * Annotations must specify if the exception is from SEH (structured exception handling)
+ * or ordinary c++ exceptions.
+ */
+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();
+
+  /**
+   * Holds if the exception type of this annotation is for a Structured 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() }
+}
+
+/**
+ * A Function that is known to not throw an exception.
+ */
+abstract class NonThrowingFunction extends ExceptionAnnotation { }
+
+/**
+ * A function this is known to raise an exception.
+ */
+abstract class ThrowingFunction extends ExceptionAnnotation {
+  ThrowingFunction() { any() }
+
+  /**
+   * Holds if this function may raise an exception during evaluation.
+   * 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.
+   */
+  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 throw an exception during evaluation.
-   * If `unconditional` is `true` the function always throws an exception.
+   * 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.
    */
-  abstract predicate mayThrowException(boolean unconditional);
+  final predicate mayRaiseException() { this.raisesException(false) }
 }