Reduce false positives compared to SDV for driver tests

src/drivers/general/queries/InvalidFunctionClassTypedef/InvalidFunctionClassTypedef.ql

@@ -16,7 +16,7 @@
  * @tags correctness
  *       ca_ported
  * @scope domainspecific
- * @query-version v1
+ * @query-version v2
  */
 
 import cpp
@@ -73,6 +73,11 @@ where
   not (
     funcClass.matches("EVT_WDF_DEVICE_%ARM_WAKE_FROM_S%") and
     declTypedef.matches("EVT_WDF_DEVICE_%ARM_WAKE_FROM_S%")
+  ) and
+  not (
+    declTypedef = funcClass + "_PAGED"
+    or
+    funcClass = declTypedef + "_PAGED"
   )
 select af, "The function class " + funcClass + " on the function does not match the function class " +
     declTypedef + " on the typedef used here"

src/drivers/general/queries/IrqlAnnotationIssue/IrqlAnnotationIssue.ql

@@ -18,12 +18,14 @@
  * @tags correctness
  *       ca_ported
  * @scope domainspecific
- * @query-version v1
+ * @query-version v2
  */
 
 import cpp
 import drivers.libraries.Irql
 
 from IrqlFunctionAnnotation ifa
-where not ifa.getIrqlLevel() instanceof IrqlValue
+where
+  not ifa.getIrqlLevel() instanceof IrqlValue and
+  ifa.getIrqlLevel() != -1
 select ifa, "Invalid IRQL annotation: " + ifa.getIrqlLevel()

src/drivers/general/queries/IrqlTooHigh/IrqlTooHigh.ql

@@ -18,23 +18,24 @@
  *       ca_ported
  *       wddst
  * @scope domainspecific
- * @query-version v2
+ * @query-version v3
  */
 
 import cpp
 import drivers.libraries.Irql
 
-from FunctionCall call, IrqlRestrictsFunction irqlFunc, ControlFlowNode prior, int irqlRequirement
+from
+  FunctionCall call, IrqlRestrictsFunction irqlFunc, ControlFlowNode prior, int irqlRequirement,
+  IrqlFunctionAnnotation ifa
 where
   call.getTarget() = irqlFunc and
   prior = call.getAPredecessor() and
-  (
-    irqlFunc.(IrqlMaxAnnotatedFunction).getIrqlLevel() = irqlRequirement
-    or
-    irqlFunc.(IrqlRequiresAnnotatedFunction).getIrqlLevel() = irqlRequirement
-  ) and
+  ifa = irqlFunc.getFuncIrqlAnnotation() and
+  (ifa instanceof IrqlMaxAnnotation or ifa instanceof IrqlRequiresAnnotation) and
+  irqlRequirement = ifa.getIrqlLevel() and
   irqlRequirement != -1 and
-  irqlRequirement < min(getPotentialExitIrqlAtCfn(prior))
+  irqlRequirement < min(getPotentialExitIrqlAtCfn(prior)) and
+  not ifa.whenConditionIsFalseAtCallSite(call)
 select call,
   "$@: IRQL potentially too high at call to $@.  Maximum IRQL for this call: " + irqlRequirement +
     ", IRQL at preceding node: " + min(getPotentialExitIrqlAtCfn(prior)),

src/drivers/general/queries/IrqlTooLow/IrqlTooLow.ql

@@ -18,23 +18,24 @@
  *       ca_ported
  *       wddst
  * @scope domainspecific
- * @query-version v3
+ * @query-version v4
  */
 
 import cpp
 import drivers.libraries.Irql
 
-from FunctionCall call, IrqlRestrictsFunction irqlFunc, ControlFlowNode prior, int irqlRequirement
+from
+  FunctionCall call, IrqlRestrictsFunction irqlFunc, ControlFlowNode prior, int irqlRequirement,
+  IrqlFunctionAnnotation ifa
 where
   call.getTarget() = irqlFunc and
   prior = call.getAPredecessor() and
-  (
-    irqlFunc.(IrqlMinAnnotatedFunction).getIrqlLevel() = irqlRequirement
-    or
-    irqlFunc.(IrqlRequiresAnnotatedFunction).getIrqlLevel() = irqlRequirement
-  ) and
+  ifa = irqlFunc.getFuncIrqlAnnotation() and
+  (ifa instanceof IrqlMinAnnotation or ifa instanceof IrqlRequiresAnnotation) and
+  irqlRequirement = ifa.getIrqlLevel() and
   irqlRequirement != -1 and
-  irqlRequirement > max(getPotentialExitIrqlAtCfn(prior))
+  irqlRequirement > max(getPotentialExitIrqlAtCfn(prior)) and
+  not ifa.whenConditionIsFalseAtCallSite(call)
 select call,
   "$@: IRQL potentially too low at call to $@.  Minimum IRQL for this call: " + irqlRequirement +
     ", IRQL at preceding node: " + max(getPotentialExitIrqlAtCfn(prior)), call.getControlFlowScope(),

src/drivers/libraries/Irql.qll

@@ -208,6 +208,36 @@
          then result = this.getIrqlLevelString().toInt()
          else result = -1
    }
+
+   /**
+    * Holds if this is a `_When_` annotation whose condition is demonstrably
+    * false at call site `call`.
+    *
+    * Callers should only pass the annotation that supplied the IRQL
+    * requirement being checked -- otherwise an unrelated `_When_` clause on
+    * the same function (e.g. the `Wait==1` clause when we are evaluating the
+    * `Wait==0` clause on `KeSetEvent`) would suppress legitimate findings.
+    */
+   predicate whenConditionIsFalseAtCallSite(FunctionCall call) {
+     this.getMacroName() = "_When_" and
+     exists(string cond, string paramName, int paramIdx |
+       cond = this.getUnexpandedArgument(0) and
+       call.getTarget().getParameter(paramIdx).getName() = paramName and
+       (
+         // "Param != 0" is false when arg is 0
+         paramName = cond.regexpCapture("(\\w+)\\s*!=\\s*0", 1) and
+         call.getArgument(paramIdx).getValue() = "0"
+         or
+         // "Param == N" (N>0) is false when arg is 0
+         paramName = cond.regexpCapture("(\\w+)\\s*==\\s*([1-9]\\d*)", 1) and
+         call.getArgument(paramIdx).getValue() = "0"
+         or
+         // "Param == 0" is false when arg is nonzero
+         paramName = cond.regexpCapture("(\\w+)\\s*==\\s*0", 1) and
+         call.getArgument(paramIdx).getValue() != "0"
+       )
+     )
+   }
  }
 
  /** Represents an "\_IRQL\_requires\_same\_" annotation. */

src/drivers/wdm/queries/IllegalFieldAccess2/IllegalFieldAccess2.ql

@@ -18,7 +18,7 @@
  *       ca_ported
  *       wddst
  * @scope domainspecific
- * @query-version v1
+ * @query-version v2
  */
 
 import cpp
@@ -87,6 +87,19 @@ class IllegalDeviceObjectFieldAccess extends FieldAccess, PotentiallyIllegalFiel
   }
 }
 
+/**
+ * Holds if `f` is `DriverEntry` itself or is transitively called from
+ * `DriverEntry`.
+ */
+predicate calledFromDriverEntry(Function f) {
+  f instanceof WdmDriverEntry
+  or
+  exists(Function caller |
+    calledFromDriverEntry(caller) and
+    f.getACallToThisFunction().getEnclosingFunction() = caller
+  )
+}
+
 /**
  * A potentially illegal access to a DriverObject field, namely:
  * - Accesses to a DriverObject's DriverStartIo, DriverUnload, MajorFunction, and DriverExtension fields outside DriverEntry
@@ -119,15 +132,14 @@ class IllegalDriverObjectFieldAccess extends FieldAccess, PotentiallyIllegalFiel
 
   override predicate isIllegalAccess() {
     /*
-     * Below fields are illegal iff we're not in a DriverEntry function.
-     * Possible future improvement: do flow analysis to figure out if we're in
-     * a call from a DriverEntry routine.
+     * Below fields are illegal iff we're not in a DriverEntry function or a
+     * function transitively called from DriverEntry.
      */
 
     this.getTarget()
         .getName()
         .matches(["DriverStartIo", "DriverUnload", "MajorFunction", "DriverExtension"]) and
-    not this.getControlFlowScope() instanceof WdmDriverEntry
+    not calledFromDriverEntry(this.getControlFlowScope())
     or
     not this.getTarget()
         .getName()

src/drivers/wdm/queries/OpaqueMdlUse/OpaqueMdlUse.ql

@@ -17,7 +17,7 @@
  * @tags correctness
  *       wddst
  * @scope domainspecific
- * @query-version v1
+ * @query-version v2
  */
 
 import cpp
@@ -42,6 +42,10 @@ class IncorrectMdlFieldAccess extends FieldAccess {
       exists(SafeMdlAccessMacro safeMacro |
         safeMacro.getAnInvocation().getAnExpandedElement() = this
       )
+    ) and
+    not exists(LocalVariable lv |
+      lv.getType().getUnspecifiedType() instanceof Mdl and
+      this.getQualifier().(VariableAccess).getTarget() = lv
     )
   }
 

src/drivers/wdm/queries/OpaqueMdlWrite/OpaqueMdlWrite.ql

@@ -18,7 +18,7 @@
  *       ca_ported
  *       wddst
  * @scope domainspecific
- * @query-version v1
+ * @query-version v2
  */
 
 import cpp
@@ -43,6 +43,10 @@ class IncorrectMdlWrite extends Assignment {
       exists(SafeMdlWriteMacro safeWriteMacro |
         safeWriteMacro.getAnInvocation().getAnExpandedElement() = this
       )
+    ) and
+    not exists(LocalVariable lv |
+      lv.getType().getUnspecifiedType() instanceof Mdl and
+      access.getQualifier().(VariableAccess).getTarget() = lv
     )
   }
 

src/microsoft/Likely Bugs/UnguardedNullReturnDereference.ql

@@ -79,7 +79,14 @@ class UnguardedNullReturnDereferenceReachability extends StackVariableReachabili
         .getDereferencingOperation()
         .(FunctionCall)
         .getTarget()
-        .hasGlobalName("free")
+        .hasGlobalName("free") and
+    not exists(FunctionCall fc, int i |
+      fc = node.(Dereference).getDereferencingOperation() and
+      fc.getArgument(i) = v.getAnAccess() and
+      exists(SALMaybeNull sa |
+        sa.getDeclaration() = fc.getTarget().getParameter(i)
+      )
+    )
   }
 
   override predicate isBarrier(ControlFlowNode node, StackVariable v) {
@@ -132,6 +139,19 @@ class UnguardedNullReturnDereferenceReachability extends StackVariableReachabili
         "_checked_pointer_impl", "_fail_on_unexpected_null_pointer", "_fail_on_memory_op"]
       and c.getAnArgument().getAChild*() = v.getAnAccess()
       and c = node)
+    or
+    exists(AssumeExpr ae |
+      ae = node and
+      ae.getOperand().getAChild*() = v.getAnAccess()
+    )
+    or
+    exists(MacroInvocation mi |
+      mi.getMacroName() = "_Analysis_assume_" and
+      mi.getUnexpandedArgument(0) = v.getName() and
+      node.getLocation().getFile() = mi.getLocation().getFile() and
+      node.getLocation().getStartLine() = mi.getLocation().getStartLine() and
+      node instanceof EmptyStmt
+    )
   }
 }
 

src/microsoft/code/cpp/public/windows/kernel/MemoryOrigins.qll

@@ -177,8 +177,6 @@ class MdlOrigin extends DirectMemoryOrigin, FunctionCall {
   }
 
   override Expr getABufferSizeExpression() { none() }
-
-  override predicate originCanWrite() { any() }
 }
 
 /**