Merge branch 'main' of github.com:github/codeql into RasmusWL-python-port-reflected-xss

2025-12-17 01:03:14 +01:00 · 2020-10-30 17:56:36 +01:00
parent ef9999a4a1 146787bb55
commit 80360450de
65 changed files with 14172 additions and 5507 deletions
--- a/change-notes/1.26/analysis-csharp.md
+++ b/change-notes/1.26/analysis-csharp.md
@@ -1,35 +0,0 @@
-# Improvements to C# analysis
-
-The following changes in version 1.26 affect C# analysis in all applications.
-
-## New queries
-
-| **Query**                   | **Tags**  | **Purpose**                                                        |
-|-----------------------------|-----------|--------------------------------------------------------------------|
-
-
-## Changes to existing queries
-
-| **Query**                    | **Expected impact**    | **Change**                        |
-|------------------------------|------------------------|-----------------------------------|
-| Weak encryption: Insufficient key size (`cs/insufficient-key-size`) | More results | The required key size has been increased from 1024 to 2048. |
-
-## Removal of old queries
-
-## Changes to code extraction
-
-* Partial method bodies are extracted. Previously, partial method bodies were skipped completely.
-* Inferring the lengths of implicitely sized arrays is fixed. Previously, multidimensional arrays were always extracted with the same length for
-each dimension. With the fix, the array sizes `2` and `1` are extracted for `new int[,]{{1},{2}}`. Previously `2` and `2` were extracted.
-* The extractor is now assembly-insensitive by default. This means that two entities with the same
-  fully-qualified name are now mapped to the same entity in the resulting database, regardless of
-  whether they belong to different assemblies. Assembly sensitivity can be reenabled by passing
-  `--assemblysensitivetrap` to the extractor.
-
-## Changes to libraries
-
-## Changes to autobuilder
-
-## Changes to tooling support
-
-* The Abstract Syntax Tree of C# files can be printed in Visual Studio Code.
--- a/config/identical-files.json
+++ b/config/identical-files.json
@@ -20,7 +20,9 @@
    "csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImpl4.qll",
    "csharp/ql/src/semmle/code/csharp/dataflow/internal/DataFlowImpl5.qll",
    "python/ql/src/experimental/dataflow/internal/DataFlowImpl.qll",
-    "python/ql/src/experimental/dataflow/internal/DataFlowImpl2.qll"
+    "python/ql/src/experimental/dataflow/internal/DataFlowImpl2.qll",
+    "python/ql/src/experimental/dataflow/internal/DataFlowImpl3.qll",
+    "python/ql/src/experimental/dataflow/internal/DataFlowImpl4.qll"
  ],
  "DataFlow Java/C++/C#/Python Common": [
    "java/ql/src/semmle/code/java/dataflow/internal/DataFlowImplCommon.qll",
@@ -41,7 +43,10 @@
    "csharp/ql/src/semmle/code/csharp/dataflow/internal/tainttracking5/TaintTrackingImpl.qll",
    "java/ql/src/semmle/code/java/dataflow/internal/tainttracking1/TaintTrackingImpl.qll",
    "java/ql/src/semmle/code/java/dataflow/internal/tainttracking2/TaintTrackingImpl.qll",
-    "python/ql/src/experimental/dataflow/internal/tainttracking1/TaintTrackingImpl.qll"
+    "python/ql/src/experimental/dataflow/internal/tainttracking1/TaintTrackingImpl.qll",
+    "python/ql/src/experimental/dataflow/internal/tainttracking2/TaintTrackingImpl.qll",
+    "python/ql/src/experimental/dataflow/internal/tainttracking3/TaintTrackingImpl.qll",
+    "python/ql/src/experimental/dataflow/internal/tainttracking4/TaintTrackingImpl.qll"
  ],
  "DataFlow Java/C++/C#/Python Consistency checks": [
    "java/ql/src/semmle/code/java/dataflow/internal/DataFlowImplConsistency.qll",
@@ -405,4 +410,4 @@
    "javascript/ql/src/Comments/CommentedOutCodeReferences.qhelp",
    "python/ql/src/Lexical/CommentedOutCodeReferences.qhelp"
  ]
-}
+}
--- a/cpp/ql/src/semmle/code/cpp/PrintAST.qll
+++ b/cpp/ql/src/semmle/code/cpp/PrintAST.qll
@@ -124,23 +124,38 @@ class PrintASTNode extends TPrintASTNode {
   * regular parent/child relation traversal.
   */
  final PrintASTNode getChild(int childIndex) {
-    result = getChildInternal(childIndex)
-    or
-    // We first compute the first available child index that is not used by
-    // `getChildInternal`, then we synthesize the child for fully converted
-    // expressions at `nextAvailableIndex` plus the childIndex of the non-converted
-    // expression. This ensures that both disjuncts are disjoint.
-    exists(int nonConvertedIndex, int nextAvailableIndex, Expr expr |
-      nextAvailableIndex = max(int idx | exists(this.getChildInternal(idx))) + 1 and
-      childIndex - nextAvailableIndex = nonConvertedIndex and
-      expr = getChildInternal(nonConvertedIndex).(ASTNode).getAST()
-    |
+    // The exact value of `childIndex` doesn't matter, as long as we preserve the correct order.
+    result =
+      rank[childIndex](PrintASTNode child, int nonConvertedIndex, boolean isConverted |
+        childAndAccessorPredicate(child, _, nonConvertedIndex, isConverted)
+      |
+        // Unconverted children come first, then sort by original child index within each group.
+        child order by isConverted, nonConvertedIndex
+      )
+  }
+
+  /**
+   * Gets the node for the `.getFullyConverted()` version of the child originally at index
+   * `childIndex`, if that node has any conversions.
+   */
+  private PrintASTNode getConvertedChild(int childIndex) {
+    exists(Expr expr |
+      expr = getChildInternal(childIndex).(ASTNode).getAST() and
      expr.getFullyConverted() instanceof Conversion and
      result.(ASTNode).getAST() = expr.getFullyConverted() and
      not expr instanceof Conversion
    )
  }

+  /**
+   * Gets the child access predicate for the `.getFullyConverted()` version of the child originally
+   * at index `childIndex`, if that node has any conversions.
+   */
+  private string getConvertedChildAccessorPredicate(int childIndex) {
+    exists(getConvertedChild(childIndex)) and
+    result = getChildAccessorPredicateInternal(childIndex) + ".getFullyConverted()"
+  }
+
  /**
   * Holds if this node should be printed in the output. By default, all nodes
   * within a function are printed, but the query can override
@@ -173,33 +188,46 @@ class PrintASTNode extends TPrintASTNode {
  }

  /**
-   * Gets the label for the edge from this node to the specified child. By
-   * default, this is just the index of the child, but subclasses can override
-   * this.
+   * Holds if there is a child node `child` for original child index `nonConvertedIndex` with
+   * predicate name `childPredicate`. If the original child at that index has any conversions, there
+   * will be two result tuples for this predicate: one with the original child and predicate, with
+   * `isConverted = false`, and the other with the `.getFullyConverted()` version of the child and
+   * predicate, with `isConverted = true`. For a child without any conversions, there will be only
+   * one result tuple, with `isConverted = false`.
   */
-  string getChildEdgeLabelInternal(int childIndex) {
-    exists(getChild(childIndex)) and
-    result = childIndex.toString()
+  private predicate childAndAccessorPredicate(
+    PrintASTNode child, string childPredicate, int nonConvertedIndex, boolean isConverted
+  ) {
+    child = getChildInternal(nonConvertedIndex) and
+    childPredicate = getChildAccessorPredicateInternal(nonConvertedIndex) and
+    isConverted = false
+    or
+    child = getConvertedChild(nonConvertedIndex) and
+    childPredicate = getConvertedChildAccessorPredicate(nonConvertedIndex) and
+    isConverted = true
  }

  /**
-   * Gets the label for the edge from this node to the specified child,
-   * including labels for edges to nodes that represent conversions.
+   * Gets the QL predicate that can be used to access the child at `childIndex`.
+   * May not always return a QL predicate, see for example `FunctionNode`.
   */
-  final string getChildEdgeLabel(int childIndex) {
-    exists(getChildInternal(childIndex)) and
-    result = getChildEdgeLabelInternal(childIndex)
-    or
-    not exists(getChildInternal(childIndex)) and
-    exists(getChild(childIndex)) and
-    exists(int nonConvertedIndex, int nextAvailableIndex |
-      nextAvailableIndex = max(int idx | exists(this.getChildInternal(idx))) + 1 and
-      childIndex - nextAvailableIndex = nonConvertedIndex
-    |
-      result = getChildEdgeLabelInternal(nonConvertedIndex) + " converted"
-    )
+  final string getChildAccessorPredicate(int childIndex) {
+    // The exact value of `childIndex` doesn't matter, as long as we preserve the correct order.
+    result =
+      rank[childIndex](string childPredicate, int nonConvertedIndex, boolean isConverted |
+        childAndAccessorPredicate(_, childPredicate, nonConvertedIndex, isConverted)
+      |
+        // Unconverted children come first, then sort by original child index within each group.
+        childPredicate order by isConverted, nonConvertedIndex
+      )
  }

+  /**
+   * Gets the QL predicate that can be used to access the child at `childIndex`.
+   * INTERNAL DO NOT USE: Does not contain accessors for the synthesized nodes for conversions.
+   */
+  abstract string getChildAccessorPredicateInternal(int childIndex);
+
  /**
   * Gets the `Function` that contains this node.
   */
@@ -261,6 +289,10 @@ class ExprNode extends ASTNode {
    result = expr.getValueCategoryString()
  }

+  override string getChildAccessorPredicateInternal(int childIndex) {
+    result = getChildAccessorWithoutConversions(ast, getChildInternal(childIndex).getAST())
+  }
+
  /**
   * Gets the value of this expression, if it is a constant.
   */
@@ -291,8 +323,6 @@ class ConversionNode extends ExprNode {
    result.getAST() = conv.getExpr() and
    conv.getExpr() instanceof Conversion
  }
-
-  override string getChildEdgeLabelInternal(int childIndex) { childIndex = 0 and result = "expr" }
 }

 /**
@@ -311,6 +341,18 @@ class CastNode extends ConversionNode {
  }
 }

+/**
+ * A node representing a `StmtExpr`.
+ */
+class StmtExprNode extends ExprNode {
+  override StmtExpr expr;
+
+  override ASTNode getChildInternal(int childIndex) {
+    childIndex = 0 and
+    result.getAST() = expr.getStmt()
+  }
+}
+
 /**
 * A node representing a `DeclarationEntry`.
 */
@@ -322,6 +364,8 @@ class DeclarationEntryNode extends BaseASTNode, TDeclarationEntryNode {

  override PrintASTNode getChildInternal(int childIndex) { none() }

+  override string getChildAccessorPredicateInternal(int childIndex) { none() }
+
  override string getProperty(string key) {
    result = BaseASTNode.super.getProperty(key)
    or
@@ -341,7 +385,10 @@ class VariableDeclarationEntryNode extends DeclarationEntryNode {
    result.getAST() = ast.getVariable().getInitializer()
  }

-  override string getChildEdgeLabelInternal(int childIndex) { childIndex = 0 and result = "init" }
+  override string getChildAccessorPredicateInternal(int childIndex) {
+    childIndex = 0 and
+    result = "getVariable().getInitializer()"
+  }
 }

 /**
@@ -361,6 +408,10 @@ class StmtNode extends ASTNode {
      )
    )
  }
+
+  override string getChildAccessorPredicateInternal(int childIndex) {
+    result = getChildAccessorWithoutConversions(ast, getChildInternal(childIndex).getAST())
+  }
 }

 /**
@@ -389,6 +440,8 @@ class ParameterNode extends ASTNode {

  final override PrintASTNode getChildInternal(int childIndex) { none() }

+  final override string getChildAccessorPredicateInternal(int childIndex) { none() }
+
  final override string getProperty(string key) {
    result = super.getProperty(key)
    or
@@ -410,9 +463,9 @@ class InitializerNode extends ASTNode {
    result.getAST() = init.getExpr()
  }

-  override string getChildEdgeLabelInternal(int childIndex) {
+  override string getChildAccessorPredicateInternal(int childIndex) {
    childIndex = 0 and
-    result = "expr"
+    result = "getExpr()"
  }
 }

@@ -432,6 +485,11 @@ class ParametersNode extends PrintASTNode, TParametersNode {
    result.getAST() = func.getParameter(childIndex)
  }

+  override string getChildAccessorPredicateInternal(int childIndex) {
+    exists(getChildInternal(childIndex)) and
+    result = "getParameter(" + childIndex.toString() + ")"
+  }
+
  /**
   * Gets the `Function` for which this node represents the parameters.
   */
@@ -454,6 +512,11 @@ class ConstructorInitializersNode extends PrintASTNode, TConstructorInitializers
    result.getAST() = ctor.getInitializer(childIndex)
  }

+  final override string getChildAccessorPredicateInternal(int childIndex) {
+    exists(getChildInternal(childIndex)) and
+    result = "getInitializer(" + childIndex.toString() + ")"
+  }
+
  /**
   * Gets the `Constructor` for which this node represents the initializer list.
   */
@@ -476,6 +539,11 @@ class DestructorDestructionsNode extends PrintASTNode, TDestructorDestructionsNo
    result.getAST() = dtor.getDestruction(childIndex)
  }

+  final override string getChildAccessorPredicateInternal(int childIndex) {
+    exists(getChildInternal(childIndex)) and
+    result = "getDestruction(" + childIndex.toString() + ")"
+  }
+
  /**
   * Gets the `Destructor` for which this node represents the destruction list.
   */
@@ -506,14 +574,14 @@ class FunctionNode extends ASTNode {
    result.(DestructorDestructionsNode).getDestructor() = func
  }

-  override string getChildEdgeLabelInternal(int childIndex) {
-    childIndex = 0 and result = "params"
+  override string getChildAccessorPredicateInternal(int childIndex) {
+    childIndex = 0 and result = "<params>"
    or
-    childIndex = 1 and result = "initializations"
+    childIndex = 1 and result = "<initializations>"
    or
-    childIndex = 2 and result = "body"
+    childIndex = 2 and result = "getEntryPoint()"
    or
-    childIndex = 3 and result = "destructions"
+    childIndex = 3 and result = "<destructions>"
  }

  private int getOrder() {
@@ -538,36 +606,237 @@ class FunctionNode extends ASTNode {
  final Function getFunction() { result = func }
 }

-/**
- * A node representing an `ClassAggregateLiteral`.
- */
-class ClassAggregateLiteralNode extends ExprNode {
-  ClassAggregateLiteral list;
-
-  ClassAggregateLiteralNode() { list = ast }
-
-  override string getChildEdgeLabelInternal(int childIndex) {
-    exists(Field field |
-      list.getFieldExpr(field) = list.getChild(childIndex) and
-      result = "." + field.getName()
+private string getChildAccessorWithoutConversions(Locatable parent, Element child) {
+  shouldPrintFunction(getEnclosingFunction(parent)) and
+  (
+    exists(Stmt s | s = parent |
+      namedStmtChildPredicates(s, child, result)
+      or
+      not namedStmtChildPredicates(s, child, _) and
+      exists(int n | s.getChild(n) = child and result = "getChild(" + n + ")")
    )
-  }
+    or
+    exists(Expr expr | expr = parent |
+      namedExprChildPredicates(expr, child, result)
+      or
+      not namedExprChildPredicates(expr, child, _) and
+      exists(int n | expr.getChild(n) = child and result = "getChild(" + n + ")")
+    )
+  )
 }

-/**
- * A node representing an `ArrayAggregateLiteral`.
- */
-class ArrayAggregateLiteralNode extends ExprNode {
-  ArrayAggregateLiteral list;
-
-  ArrayAggregateLiteralNode() { list = ast }
-
-  override string getChildEdgeLabelInternal(int childIndex) {
-    exists(int elementIndex |
-      list.getElementExpr(elementIndex) = list.getChild(childIndex) and
-      result = "[" + elementIndex.toString() + "]"
+private predicate namedStmtChildPredicates(Locatable s, Element e, string pred) {
+  shouldPrintFunction(getEnclosingFunction(s)) and
+  (
+    exists(int n | s.(BlockStmt).getStmt(n) = e and pred = "getStmt(" + n + ")")
+    or
+    s.(ComputedGotoStmt).getExpr() = e and pred = "getExpr()"
+    or
+    s.(ConstexprIfStmt).getCondition() = e and pred = "getCondition()"
+    or
+    s.(ConstexprIfStmt).getThen() = e and pred = "getThen()"
+    or
+    s.(ConstexprIfStmt).getElse() = e and pred = "getElse()"
+    or
+    s.(IfStmt).getCondition() = e and pred = "getCondition()"
+    or
+    s.(IfStmt).getThen() = e and pred = "getThen()"
+    or
+    s.(IfStmt).getElse() = e and pred = "getElse()"
+    or
+    s.(SwitchStmt).getExpr() = e and pred = "getExpr()"
+    or
+    s.(SwitchStmt).getStmt() = e and pred = "getStmt()"
+    or
+    s.(DoStmt).getCondition() = e and pred = "getCondition()"
+    or
+    s.(DoStmt).getStmt() = e and pred = "getStmt()"
+    or
+    s.(ForStmt).getInitialization() = e and pred = "getInitialization()"
+    or
+    s.(ForStmt).getCondition() = e and pred = "getCondition()"
+    or
+    s.(ForStmt).getUpdate() = e and pred = "getUpdate()"
+    or
+    s.(ForStmt).getStmt() = e and pred = "getStmt()"
+    or
+    s.(RangeBasedForStmt).getChild(0) = e and pred = "getChild(0)"
+    or
+    s.(RangeBasedForStmt).getBeginEndDeclaration() = e and pred = "getBeginEndDeclaration()"
+    or
+    s.(RangeBasedForStmt).getCondition() = e and pred = "getCondition()"
+    or
+    s.(RangeBasedForStmt).getUpdate() = e and pred = "getUpdate()"
+    or
+    s.(RangeBasedForStmt).getChild(4) = e and pred = "getChild(4)"
+    or
+    s.(RangeBasedForStmt).getStmt() = e and pred = "getStmt()"
+    or
+    s.(WhileStmt).getCondition() = e and pred = "getCondition()"
+    or
+    s.(WhileStmt).getStmt() = e and pred = "getStmt()"
+    or
+    exists(int n |
+      s.(DeclStmt).getDeclarationEntry(n) = e and pred = "getDeclarationEntry(" + n.toString() + ")"
    )
-  }
+    or
+    // EmptyStmt does not have children
+    s.(ExprStmt).getExpr() = e and pred = "getExpr()"
+    or
+    s.(Handler).getBlock() = e and pred = "getBlock()"
+    or
+    s.(JumpStmt).getTarget() = e and pred = "getTarget()"
+    or
+    s.(MicrosoftTryStmt).getStmt() = e and pred = "getStmt()"
+    or
+    s.(MicrosoftTryExceptStmt).getCondition() = e and pred = "getCondition()"
+    or
+    s.(MicrosoftTryExceptStmt).getExcept() = e and pred = "getExcept()"
+    or
+    s.(MicrosoftTryFinallyStmt).getFinally() = e and pred = "getFinally()"
+    or
+    s.(ReturnStmt).getExpr() = e and pred = "getExpr()"
+    or
+    s.(SwitchCase).getExpr() = e and pred = "getExpr()"
+    or
+    s.(SwitchCase).getEndExpr() = e and pred = "getEndExpr()"
+    or
+    s.(TryStmt).getStmt() = e and pred = "getStmt()"
+    or
+    s.(VlaDimensionStmt).getDimensionExpr() = e and pred = "getDimensionExpr()"
+  )
+}
+
+private predicate namedExprChildPredicates(Expr expr, Element ele, string pred) {
+  shouldPrintFunction(expr.getEnclosingFunction()) and
+  (
+    expr.(Access).getTarget() = ele and pred = "getTarget()"
+    or
+    expr.(VariableAccess).getQualifier() = ele and pred = "getQualifier()"
+    or
+    exists(Field f |
+      expr.(ClassAggregateLiteral).getFieldExpr(f) = ele and
+      pred = "getFieldExpr(" + f.toString() + ")"
+    )
+    or
+    exists(int n |
+      expr.(ArrayOrVectorAggregateLiteral).getElementExpr(n) = ele and
+      pred = "getElementExpr(" + n.toString() + ")"
+    )
+    or
+    expr.(AlignofExprOperator).getExprOperand() = ele and pred = "getExprOperand()"
+    or
+    expr.(ArrayExpr).getArrayBase() = ele and pred = "getArrayBase()"
+    or
+    expr.(ArrayExpr).getArrayOffset() = ele and pred = "getArrayOffset()"
+    or
+    expr.(AssumeExpr).getOperand() = ele and pred = "getOperand()"
+    or
+    expr.(BuiltInComplexOperation).getRealOperand() = ele and pred = "getRealOperand()"
+    or
+    expr.(BuiltInComplexOperation).getImaginaryOperand() = ele and pred = "getImaginaryOperand()"
+    or
+    expr.(BuiltInVarArg).getVAList() = ele and pred = "getVAList()"
+    or
+    expr.(BuiltInVarArgCopy).getDestinationVAList() = ele and pred = "getDestinationVAList()"
+    or
+    expr.(BuiltInVarArgCopy).getSourceVAList() = ele and pred = "getSourceVAList()"
+    or
+    expr.(BuiltInVarArgsEnd).getVAList() = ele and pred = "getVAList()"
+    or
+    expr.(BuiltInVarArgsStart).getVAList() = ele and pred = "getVAList()"
+    or
+    expr.(BuiltInVarArgsStart).getLastNamedParameter() = ele and pred = "getLastNamedParameter()"
+    or
+    expr.(Call).getQualifier() = ele and pred = "getQualifier()"
+    or
+    exists(int n | expr.(Call).getArgument(n) = ele and pred = "getArgument(" + n.toString() + ")")
+    or
+    expr.(ExprCall).getExpr() = ele and pred = "getExpr()"
+    or
+    expr.(OverloadedArrayExpr).getArrayBase() = ele and pred = "getArrayBase()"
+    or
+    expr.(OverloadedArrayExpr).getArrayOffset() = ele and pred = "getArrayOffset()"
+    or
+    expr.(OverloadedPointerDereferenceExpr).getExpr() = ele and pred = "getExpr()"
+    or
+    expr.(CommaExpr).getLeftOperand() = ele and pred = "getLeftOperand()"
+    or
+    expr.(CommaExpr).getRightOperand() = ele and pred = "getRightOperand()"
+    or
+    expr.(ConditionDeclExpr).getVariableAccess() = ele and pred = "getVariableAccess()"
+    or
+    expr.(ConstructorFieldInit).getExpr() = ele and pred = "getExpr()"
+    or
+    expr.(Conversion).getExpr() = ele and pred = "getExpr()"
+    or
+    expr.(DeleteArrayExpr).getAllocatorCall() = ele and pred = "getAllocatorCall()"
+    or
+    expr.(DeleteArrayExpr).getDestructorCall() = ele and pred = "getDestructorCall()"
+    or
+    expr.(DeleteArrayExpr).getExpr() = ele and pred = "getExpr()"
+    or
+    expr.(DeleteExpr).getAllocatorCall() = ele and pred = "getAllocatorCall()"
+    or
+    expr.(DeleteExpr).getDestructorCall() = ele and pred = "getDestructorCall()"
+    or
+    expr.(DeleteExpr).getExpr() = ele and pred = "getExpr()"
+    or
+    expr.(DestructorFieldDestruction).getExpr() = ele and pred = "getExpr()"
+    or
+    expr.(FoldExpr).getInitExpr() = ele and pred = "getInitExpr()"
+    or
+    expr.(FoldExpr).getPackExpr() = ele and pred = "getPackExpr()"
+    or
+    expr.(LambdaExpression).getInitializer() = ele and pred = "getInitializer()"
+    or
+    expr.(NewOrNewArrayExpr).getAllocatorCall() = ele and pred = "getAllocatorCall()"
+    or
+    expr.(NewOrNewArrayExpr).getAlignmentArgument() = ele and pred = "getAlignmentArgument()"
+    or
+    expr.(NewArrayExpr).getInitializer() = ele and pred = "getInitializer()"
+    or
+    expr.(NewArrayExpr).getExtent() = ele and pred = "getExtent()"
+    or
+    expr.(NewExpr).getInitializer() = ele and pred = "getInitializer()"
+    or
+    expr.(NoExceptExpr).getExpr() = ele and pred = "getExpr()"
+    or
+    expr.(Assignment).getLValue() = ele and pred = "getLValue()"
+    or
+    expr.(Assignment).getRValue() = ele and pred = "getRValue()"
+    or
+    not expr instanceof RelationalOperation and
+    expr.(BinaryOperation).getLeftOperand() = ele and
+    pred = "getLeftOperand()"
+    or
+    not expr instanceof RelationalOperation and
+    expr.(BinaryOperation).getRightOperand() = ele and
+    pred = "getRightOperand()"
+    or
+    expr.(RelationalOperation).getGreaterOperand() = ele and pred = "getGreaterOperand()"
+    or
+    expr.(RelationalOperation).getLesserOperand() = ele and pred = "getLesserOperand()"
+    or
+    expr.(ConditionalExpr).getCondition() = ele and pred = "getCondition()"
+    or
+    // If ConditionalExpr is in two-operand form, getThen() = getCondition() holds
+    not expr.(ConditionalExpr).isTwoOperand() and
+    expr.(ConditionalExpr).getThen() = ele and
+    pred = "getThen()"
+    or
+    expr.(ConditionalExpr).getElse() = ele and pred = "getElse()"
+    or
+    expr.(UnaryOperation).getOperand() = ele and pred = "getOperand()"
+    or
+    expr.(SizeofExprOperator).getExprOperand() = ele and pred = "getExprOperand()"
+    or
+    expr.(StmtExpr).getStmt() = ele and pred = "getStmt()"
+    or
+    expr.(ThrowExpr).getExpr() = ele and pred = "getExpr()"
+    or
+    expr.(TypeidOperator).getExpr() = ele and pred = "getExpr()"
+  )
 }

 /** Holds if `node` belongs to the output tree, and its property `key` has the given `value`. */
@@ -586,7 +855,7 @@ query predicate edges(PrintASTNode source, PrintASTNode target, string key, stri
    target.shouldPrint() and
    target = source.getChild(childIndex) and
    (
-      key = "semmle.label" and value = source.getChildEdgeLabel(childIndex)
+      key = "semmle.label" and value = source.getChildAccessorPredicate(childIndex)
      or
      key = "semmle.order" and value = childIndex.toString()
    )
--- a/cpp/ql/src/semmle/code/cpp/ir/dataflow/DefaultTaintTracking.qll
+++ b/cpp/ql/src/semmle/code/cpp/ir/dataflow/DefaultTaintTracking.qll
@@ -303,8 +303,6 @@ private predicate instructionTaintStep(Instruction i1, Instruction i2) {
    )
  or
  // Flow from input argument to output argument
-  // TODO: This won't work in practice as long as all aliased memory is tracked
-  // together in a single virtual variable.
  // TODO: Will this work on the test for `TaintedPath.ql`, where the output arg
  // is a pointer addition expression?
  i2 =
--- a/cpp/ql/test/examples/expressions/PrintAST.expected
+++ b/cpp/ql/test/examples/expressions/PrintAST.expected
--- a/cpp/ql/test/library-tests/dataflow/DefaultTaintTracking/defaulttainttracking.cpp
+++ b/cpp/ql/test/library-tests/dataflow/DefaultTaintTracking/defaulttainttracking.cpp
@@ -208,4 +208,50 @@ void test_field_to_obj_test_pointer_arith(Point* pp) {
  (pp + sizeof(*pp))->x = getenv("VAR")[0];
  sink(pp); // tainted [field -> object]
  sink(pp + sizeof(*pp)); // tainted [field -> object]
-}
+}
+
+void sink(char **);
+
+void test_pointers1()
+{
+	char buffer[1024];
+	char *s = getenv("VAR");
+	char *ptr1, **ptr2;
+	char *ptr3, **ptr4;
+
+	ptr1 = buffer;
+	ptr2 = &ptr1;
+	memcpy(buffer, s, 1024);
+	ptr3 = buffer;
+	ptr4 = &ptr3;
+
+	sink(buffer); // tainted
+	sink(ptr1); // tainted
+	sink(ptr2);
+	sink(*ptr2); // tainted [NOT DETECTED]
+	sink(ptr3); // tainted
+	sink(ptr4);
+	sink(*ptr4); // tainted [NOT DETECTED]
+}
+
+void test_pointers2()
+{
+	char buffer[1024];
+	char *s = getenv("VAR");
+	char *ptr1, **ptr2;
+	char *ptr3, **ptr4;
+
+	ptr1 = buffer;
+	ptr2 = &ptr1;
+	memcpy(*ptr2, s, 1024);
+	ptr3 = buffer;
+	ptr4 = &ptr3;
+
+	sink(buffer); // tainted [NOT DETECTED]
+	sink(ptr1); // tainted [NOT DETECTED]
+	sink(ptr2);
+	sink(*ptr2); // tainted [NOT DETECTED]
+	sink(ptr3); // tainted [NOT DETECTED]
+	sink(ptr4);
+	sink(*ptr4); // tainted [NOT DETECTED]
+}
--- a/cpp/ql/test/library-tests/dataflow/DefaultTaintTracking/shared.h
+++ b/cpp/ql/test/library-tests/dataflow/DefaultTaintTracking/shared.h
@@ -12,3 +12,6 @@ char *strcat(char * s1, const char * s2);
 char *strdup(const char *string);
 char *_strdup(const char *string);
 char *unmodeled_function(const char *const_string);
+
+typedef unsigned long size_t;
+void *memcpy(void *s1, const void *s2, size_t n);
--- a/cpp/ql/test/library-tests/dataflow/DefaultTaintTracking/tainted.expected
+++ b/cpp/ql/test/library-tests/dataflow/DefaultTaintTracking/tainted.expected
@@ -134,6 +134,26 @@
 | defaulttainttracking.cpp:208:27:208:32 | call to getenv | defaulttainttracking.cpp:208:27:208:32 | call to getenv |
 | defaulttainttracking.cpp:208:27:208:32 | call to getenv | defaulttainttracking.cpp:208:27:208:42 | (int)... |
 | defaulttainttracking.cpp:208:27:208:32 | call to getenv | defaulttainttracking.cpp:208:27:208:42 | access to array |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:218:8:218:8 | s |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:218:12:218:17 | call to getenv |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:224:2:224:7 | call to memcpy |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:224:17:224:17 | (const void *)... |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:224:17:224:17 | s |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:228:7:228:12 | (const char *)... |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:228:7:228:12 | array to pointer conversion |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:228:7:228:12 | buffer |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:229:7:229:10 | (const char *)... |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:229:7:229:10 | ptr1 |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:232:7:232:10 | (const char *)... |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:232:7:232:10 | ptr3 |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | shared.h:5:23:5:31 | sinkparam |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | shared.h:17:36:17:37 | s2 |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:240:8:240:8 | s |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:240:12:240:17 | call to getenv |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:246:2:246:7 | call to memcpy |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:246:16:246:16 | (const void *)... |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:246:16:246:16 | s |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | shared.h:17:36:17:37 | s2 |
 | dispatch.cpp:28:29:28:34 | call to getenv | dispatch.cpp:28:24:28:27 | call to atoi |
 | dispatch.cpp:28:29:28:34 | call to getenv | dispatch.cpp:28:29:28:34 | call to getenv |
 | dispatch.cpp:28:29:28:34 | call to getenv | dispatch.cpp:28:29:28:45 | (const char *)... |
--- a/cpp/ql/test/library-tests/dataflow/DefaultTaintTracking/test_diff.expected
+++ b/cpp/ql/test/library-tests/dataflow/DefaultTaintTracking/test_diff.expected
@@ -36,6 +36,50 @@
 | defaulttainttracking.cpp:195:11:195:16 | call to getenv | defaulttainttracking.cpp:195:7:195:7 | x | AST only |
 | defaulttainttracking.cpp:201:13:201:18 | call to getenv | defaulttainttracking.cpp:201:9:201:9 | x | AST only |
 | defaulttainttracking.cpp:208:27:208:32 | call to getenv | defaulttainttracking.cpp:208:23:208:23 | x | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:213:11:213:14 | (unnamed parameter 0) | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:217:7:217:12 | buffer | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:219:8:219:11 | ptr1 | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:219:16:219:19 | ptr2 | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:220:8:220:11 | ptr3 | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:220:16:220:19 | ptr4 | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:222:2:222:5 | ptr1 | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:222:9:222:14 | buffer | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:223:2:223:5 | ptr2 | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:223:9:223:13 | & ... | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:223:10:223:13 | ptr1 | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:224:9:224:14 | buffer | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:225:2:225:5 | ptr3 | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:225:9:225:14 | buffer | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:226:2:226:5 | ptr4 | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:226:9:226:13 | & ... | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:226:10:226:13 | ptr3 | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:228:7:228:12 | (const char *)... | IR only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:228:7:228:12 | array to pointer conversion | IR only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:230:7:230:10 | ptr2 | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:231:7:231:11 | (const char *)... | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:231:7:231:11 | * ... | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:231:8:231:11 | ptr2 | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:233:7:233:10 | ptr4 | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:234:7:234:11 | (const char *)... | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:234:7:234:11 | * ... | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | defaulttainttracking.cpp:234:8:234:11 | ptr4 | AST only |
+| defaulttainttracking.cpp:218:12:218:17 | call to getenv | shared.h:17:20:17:21 | s1 | AST only |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:213:11:213:14 | (unnamed parameter 0) | AST only |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:241:8:241:11 | ptr1 | AST only |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:241:16:241:19 | ptr2 | AST only |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:245:2:245:5 | ptr2 | AST only |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:245:9:245:13 | & ... | AST only |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:245:10:245:13 | ptr1 | AST only |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:246:9:246:13 | * ... | AST only |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:246:10:246:13 | ptr2 | AST only |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:251:7:251:10 | (const char *)... | AST only |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:251:7:251:10 | ptr1 | AST only |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:252:7:252:10 | ptr2 | AST only |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:253:7:253:11 | (const char *)... | AST only |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:253:7:253:11 | * ... | AST only |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | defaulttainttracking.cpp:253:8:253:11 | ptr2 | AST only |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | shared.h:5:23:5:31 | sinkparam | AST only |
+| defaulttainttracking.cpp:240:12:240:17 | call to getenv | shared.h:17:20:17:21 | s1 | AST only |
 | globals.cpp:13:15:13:20 | call to getenv | globals.cpp:13:5:13:11 | global1 | AST only |
 | globals.cpp:23:15:23:20 | call to getenv | globals.cpp:23:5:23:11 | global2 | AST only |
 | stl.cpp:62:25:62:30 | call to getenv | stl.cpp:43:78:43:104 | (unnamed parameter 0) | IR only |
--- a/cpp/ql/test/library-tests/ir/ir/PrintAST.expected
+++ b/cpp/ql/test/library-tests/ir/ir/PrintAST.expected
--- a/cpp/ql/test/library-tests/ir/ir/ir.cpp
+++ b/cpp/ql/test/library-tests/ir/ir/ir.cpp
@@ -997,7 +997,7 @@ int PointerDecay(int a[], int fn(float)) {
  return a[0] + fn(1.0);
 }

-int ExprStmt(int b, int y, int z) {
+int StmtExpr(int b, int y, int z) {
  int x = ({
    int w;
    if (b) {
--- a/cpp/ql/test/library-tests/ir/ir/raw_ir.expected
+++ b/cpp/ql/test/library-tests/ir/ir/raw_ir.expected
@@ -5532,7 +5532,7 @@ ir.cpp:
 #  996|     v996_13(void)            = AliasedUse               : ~m?
 #  996|     v996_14(void)            = ExitFunction             : 

-# 1000| int ExprStmt(int, int, int)
+# 1000| int StmtExpr(int, int, int)
 # 1000|   Block 0
 # 1000|     v1000_1(void)       = EnterFunction          : 
 # 1000|     mu1000_2(unknown)   = AliasedDefinition      : 
--- a/csharp/change-notes/2020-08-18-ast-viewer.md
+++ b/csharp/change-notes/2020-08-18-ast-viewer.md
@@ -0,0 +1,2 @@
+tooling
+* The Abstract Syntax Tree of C# files can be viewed in Visual Studio Code.
--- a/csharp/change-notes/2020-08-18-partial-method-bodies.md
+++ b/csharp/change-notes/2020-08-18-partial-method-bodies.md
@@ -0,0 +1,2 @@
+lgtm,codescanning
+* Partial method bodies are extracted. Previously, partial method bodies were skipped.
--- a/csharp/change-notes/2020-08-26-implicit-array-lengths.md
+++ b/csharp/change-notes/2020-08-26-implicit-array-lengths.md
@@ -0,0 +1,5 @@
+lgtm,codescanning
+* Inferring the lengths of implicitely sized arrays is fixed. Previously, multi
+  dimensional arrays were always extracted with the same length for each dimension.
+  With the fix, the array sizes `2` and `1` are extracted for `new int[,]{{1},{2}}`.
+  Previously `2` and `2` were extracted.
--- a/csharp/change-notes/2020-09-02-assembly-insensitive-trap.md
+++ b/csharp/change-notes/2020-09-02-assembly-insensitive-trap.md
@@ -0,0 +1,5 @@
+lgtm,codescanning
+* The extractor is now assembly-insensitive by default. This means that two entities
+  with the same fully-qualified name are now mapped to the same entity in the resulting
+  database, regardless of whether they belong to different assemblies. Assembly
+  sensitivity can be reenabled by passing `--assemblysensitivetrap` to the extractor.
--- a/csharp/change-notes/2020-09-22-weak-encryption.md
+++ b/csharp/change-notes/2020-09-22-weak-encryption.md
@@ -0,0 +1,2 @@
+lgtm,codescanning
+* The required key size for the query "Weak encryption: Insufficient key size" has been increased from 1024 to 2048.
--- a/csharp/ql/src/semmle/code/csharp/commons/Assertions.qll
+++ b/csharp/ql/src/semmle/code/csharp/commons/Assertions.qll
@@ -9,43 +9,114 @@ private import ControlFlow::BasicBlocks

 /** An assertion method. */
 abstract class AssertMethod extends Method {
-  /**
-   * DEPRECATED: renamed to `getAnAssertionIndex`.
-   *
-   * Gets the index of a parameter being asserted.
-   */
-  deprecated int getAssertionIndex() { result = getAnAssertionIndex() }
-
  /** Gets the index of a parameter being asserted. */
  abstract int getAnAssertionIndex();

  /**
-   * DEPRECATED: renamed to `getAnAssertedParameter`.
+   * DEPRECATED: Use `getAnAssertionIndex()` instead.
+   *
+   * Gets the index of a parameter being asserted.
+   */
+  deprecated final int getAssertionIndex() { result = getAnAssertionIndex() }
+
+  /** Gets the parameter at position `i` being asserted. */
+  final Parameter getAssertedParameter(int i) {
+    result = this.getParameter(i) and
+    i = this.getAnAssertionIndex()
+  }
+
+  /**
+   * DEPRECATED: Use `getAssertedParameter(_)` instead.
   *
   * Gets a parameter being asserted.
   */
-  deprecated Parameter getAssertedParameter() { result = getAnAssertedParameter() }
+  deprecated final Parameter getAssertedParameter() { result = getAssertedParameter(_) }

-  /** Gets a parameter being asserted. */
-  final Parameter getAnAssertedParameter() {
-    result = this.getParameter(this.getAnAssertionIndex())
-  }
+  /** Gets the exception being thrown if the assertion fails for argument `i`, if any. */
+  abstract Class getExceptionClass(int i);

-  /** Gets the exception being thrown if the assertion fails, if any. */
-  abstract Class getExceptionClass();
+  /**
+   * DEPRECATED: Use `getExceptionClass(_)` instead.
+   *
+   * Gets the exception being thrown if the assertion fails, if any.
+   */
+  deprecated final Class getExceptionClass() { result = this.getExceptionClass(_) }
+}
+
+/** A Boolean assertion method. */
+abstract class BooleanAssertMethod extends AssertMethod {
+  /** Gets the index of a parameter asserted to have value `b`. */
+  abstract int getAnAssertionIndex(boolean b);
+
+  override int getAnAssertionIndex() { result = this.getAnAssertionIndex(_) }
 }

 /** A positive assertion method. */
-abstract class AssertTrueMethod extends AssertMethod { }
+deprecated class AssertTrueMethod extends AssertMethod {
+  private BooleanAssertMethod m;
+
+  AssertTrueMethod() {
+    this = m and
+    exists(m.getAnAssertionIndex(true))
+  }
+
+  final override int getAnAssertionIndex() { result = m.getAnAssertionIndex() }
+
+  final override Class getExceptionClass(int i) { result = m.getExceptionClass(i) }
+}

 /** A negated assertion method. */
-abstract class AssertFalseMethod extends AssertMethod { }
+deprecated class AssertFalseMethod extends AssertMethod {
+  private BooleanAssertMethod m;
+
+  AssertFalseMethod() {
+    this = m and
+    exists(m.getAnAssertionIndex(false))
+  }
+
+  final override int getAnAssertionIndex() { result = m.getAnAssertionIndex() }
+
+  final override Class getExceptionClass(int i) { result = m.getExceptionClass(i) }
+}
+
+/** A nullness assertion method. */
+abstract class NullnessAssertMethod extends AssertMethod {
+  /**
+   * Gets the index of a parameter asserted to be `null` (`b = true`)
+   * or non-`null` (`b = false`).
+   */
+  abstract int getAnAssertionIndex(boolean b);
+
+  override int getAnAssertionIndex() { result = this.getAnAssertionIndex(_) }
+}

 /** A `null` assertion method. */
-abstract class AssertNullMethod extends AssertMethod { }
+deprecated class AssertNullMethod extends AssertMethod {
+  private NullnessAssertMethod m;
+
+  AssertNullMethod() {
+    this = m and
+    exists(m.getAnAssertionIndex(true))
+  }
+
+  final override int getAnAssertionIndex() { result = m.getAnAssertionIndex() }
+
+  final override Class getExceptionClass(int i) { result = m.getExceptionClass(i) }
+}

 /** A non-`null` assertion method. */
-abstract class AssertNonNullMethod extends AssertMethod { }
+deprecated class AssertNonNullMethod extends AssertMethod {
+  private NullnessAssertMethod m;
+
+  AssertNonNullMethod() {
+    this = m and
+    exists(m.getAnAssertionIndex(false))
+  }
+
+  final override int getAnAssertionIndex() { result = m.getAnAssertionIndex() }
+
+  final override Class getExceptionClass(int i) { result = m.getExceptionClass(i) }
+}

 /** An assertion, that is, a call to an assertion method. */
 class Assertion extends MethodCall {
@@ -56,15 +127,21 @@ class Assertion extends MethodCall {
  /** Gets the assertion method targeted by this assertion. */
  AssertMethod getAssertMethod() { result = target }

+  /** Gets an expression at argument position `i` that this assertion pertains to. */
+  Expr getExpr(int i) {
+    i = target.getAnAssertionIndex() and
+    exists(Parameter p |
+      p = target.getParameter(i) and
+      result = this.getArgumentForParameter(p)
+    )
+  }
+
  /**
-   * DEPRECATED: renamed to `getAnExpr`.
+   * DEPRECATED: Use `getExpr(_)` instead.
   *
   * Gets an expression that this assertion pertains to.
   */
-  deprecated Expr getExpr() { result = this.getAnExpr() }
-
-  /** Gets an expression that this assertion pertains to. */
-  Expr getAnExpr() { result = this.getArgumentForParameter(target.getAnAssertedParameter()) }
+  deprecated Expr getExpr() { result = this.getExpr(_) }

  /**
   * Holds if basic block `succ` is immediately dominated by this assertion.
@@ -164,31 +241,37 @@ class Assertion extends MethodCall {

 /** A trivially failing assertion, for example `Debug.Assert(false)`. */
 class FailingAssertion extends Assertion {
+  private int i;
+
  FailingAssertion() {
-    exists(AssertMethod am, Expr e |
+    exists(BooleanAssertMethod am, Expr e, boolean b |
      am = this.getAssertMethod() and
-      e = this.getAnExpr()
+      e = this.getExpr(i) and
+      i = am.getAnAssertionIndex(b)
    |
-      am instanceof AssertTrueMethod and
+      b = true and
      e.getValue() = "false"
      or
-      am instanceof AssertFalseMethod and
+      b = false and
      e.getValue() = "true"
    )
  }
+
+  /** Gets the exception being thrown by this failing assertion, if any. */
+  Class getExceptionClass() { result = this.getAssertMethod().getExceptionClass(i) }
 }

 /**
 * A `System.Diagnostics.Debug` assertion method.
 */
-class SystemDiagnosticsDebugAssertTrueMethod extends AssertTrueMethod {
+class SystemDiagnosticsDebugAssertTrueMethod extends BooleanAssertMethod {
  SystemDiagnosticsDebugAssertTrueMethod() {
    this = any(SystemDiagnosticsDebugClass c).getAssertMethod()
  }

-  override int getAnAssertionIndex() { result = 0 }
+  override int getAnAssertionIndex(boolean b) { result = 0 and b = true }

-  override Class getExceptionClass() {
+  override Class getExceptionClass(int i) {
    // A failing assertion generates a message box, see
    // https://docs.microsoft.com/en-us/dotnet/api/system.diagnostics.debug.assert
    none()
@@ -198,7 +281,7 @@ class SystemDiagnosticsDebugAssertTrueMethod extends AssertTrueMethod {
 /**
 * A `System.Diagnostics.Contracts.Contract` assertion method.
 */
-class SystemDiagnosticsContractAssertTrueMethod extends AssertTrueMethod {
+class SystemDiagnosticsContractAssertTrueMethod extends BooleanAssertMethod {
  SystemDiagnosticsContractAssertTrueMethod() {
    exists(SystemDiagnosticsContractsContractClass c |
      this = c.getAnAssertMethod()
@@ -209,9 +292,9 @@ class SystemDiagnosticsContractAssertTrueMethod extends AssertTrueMethod {
    )
  }

-  override int getAnAssertionIndex() { result = 0 }
+  override int getAnAssertionIndex(boolean b) { result = 0 and b = true }

-  override Class getExceptionClass() {
+  override Class getExceptionClass(int i) {
    // A failing assertion generates a message box, see
    // https://docs.microsoft.com/en-us/dotnet/api/system.diagnostics.contracts.contract.assert
    none()
@@ -229,79 +312,82 @@ private predicate isDoesNotReturnIfAttributeParameter(Parameter p, boolean value
 * A method with a parameter that is annotated with
 * `System.Diagnostics.CodeAnalysis.DoesNotReturnIfAttribute(false)`.
 */
-class SystemDiagnosticsCodeAnalysisDoesNotReturnIfAnnotatedAssertTrueMethod extends AssertTrueMethod {
-  private int i;
+class SystemDiagnosticsCodeAnalysisDoesNotReturnIfAnnotatedAssertTrueMethod extends BooleanAssertMethod {
+  private int i_;

  SystemDiagnosticsCodeAnalysisDoesNotReturnIfAnnotatedAssertTrueMethod() {
-    isDoesNotReturnIfAttributeParameter(this.getParameter(i), false)
+    isDoesNotReturnIfAttributeParameter(this.getParameter(i_), false)
  }

-  override int getAnAssertionIndex() { result = i }
+  override int getAnAssertionIndex(boolean b) { result = i_ and b = true }

-  override SystemExceptionClass getExceptionClass() { any() }
+  override Class getExceptionClass(int i) { i = i_ and result instanceof SystemExceptionClass }
 }

 /**
 * A method with a parameter that is annotated with
 * `System.Diagnostics.CodeAnalysis.DoesNotReturnIfAttribute(true)`.
 */
-class SystemDiagnosticsCodeAnalysisDoesNotReturnIfAnnotatedAssertFalseMethod extends AssertFalseMethod {
-  private int i;
+class SystemDiagnosticsCodeAnalysisDoesNotReturnIfAnnotatedAssertFalseMethod extends BooleanAssertMethod {
+  private int i_;

  SystemDiagnosticsCodeAnalysisDoesNotReturnIfAnnotatedAssertFalseMethod() {
-    isDoesNotReturnIfAttributeParameter(this.getParameter(i), true)
+    isDoesNotReturnIfAttributeParameter(this.getParameter(i_), true)
  }

-  override int getAnAssertionIndex() { result = i }
+  override int getAnAssertionIndex(boolean b) {
+    result = i_ and
+    b = false
+  }

-  override SystemExceptionClass getExceptionClass() { any() }
+  override Class getExceptionClass(int i) { i = i_ and result instanceof SystemExceptionClass }
 }

 /** A Visual Studio assertion method. */
-class VSTestAssertTrueMethod extends AssertTrueMethod {
+class VSTestAssertTrueMethod extends BooleanAssertMethod {
  VSTestAssertTrueMethod() { this = any(VSTestAssertClass c).getIsTrueMethod() }

-  override int getAnAssertionIndex() { result = 0 }
+  override int getAnAssertionIndex(boolean b) { result = 0 and b = true }

-  override AssertFailedExceptionClass getExceptionClass() { any() }
+  override Class getExceptionClass(int i) { i = 0 and result instanceof AssertFailedExceptionClass }
 }

 /** A Visual Studio negated assertion method. */
-class VSTestAssertFalseMethod extends AssertFalseMethod {
+class VSTestAssertFalseMethod extends BooleanAssertMethod {
  VSTestAssertFalseMethod() { this = any(VSTestAssertClass c).getIsFalseMethod() }

-  override int getAnAssertionIndex() { result = 0 }
+  override int getAnAssertionIndex(boolean b) { result = 0 and b = false }

-  override AssertFailedExceptionClass getExceptionClass() { any() }
+  override Class getExceptionClass(int i) { i = 0 and result instanceof AssertFailedExceptionClass }
 }

 /** A Visual Studio `null` assertion method. */
-class VSTestAssertNullMethod extends AssertNullMethod {
+class VSTestAssertNullMethod extends NullnessAssertMethod {
  VSTestAssertNullMethod() { this = any(VSTestAssertClass c).getIsNullMethod() }

-  override int getAnAssertionIndex() { result = 0 }
+  override int getAnAssertionIndex(boolean b) { result = 0 and b = true }

-  override AssertFailedExceptionClass getExceptionClass() { any() }
+  override Class getExceptionClass(int i) { i = 0 and result instanceof AssertFailedExceptionClass }
 }

 /** A Visual Studio non-`null` assertion method. */
-class VSTestAssertNonNullMethod extends AssertNonNullMethod {
+class VSTestAssertNonNullMethod extends NullnessAssertMethod {
  VSTestAssertNonNullMethod() { this = any(VSTestAssertClass c).getIsNotNullMethod() }

-  override int getAnAssertionIndex() { result = 0 }
+  override int getAnAssertionIndex(boolean b) { result = 0 and b = false }

-  override AssertFailedExceptionClass getExceptionClass() { any() }
+  override Class getExceptionClass(int i) { i = 0 and result instanceof AssertFailedExceptionClass }
 }

 /** An NUnit assertion method. */
 abstract class NUnitAssertMethod extends AssertMethod {
  override int getAnAssertionIndex() { result = 0 }

-  override AssertionExceptionClass getExceptionClass() { any() }
+  override Class getExceptionClass(int i) { i = 0 and result instanceof AssertionExceptionClass }
 }

 /** An NUnit assertion method. */
-class NUnitAssertTrueMethod extends AssertTrueMethod, NUnitAssertMethod {
+class NUnitAssertTrueMethod extends BooleanAssertMethod, NUnitAssertMethod {
  NUnitAssertTrueMethod() {
    exists(NUnitAssertClass c |
      this = c.getATrueMethod()
@@ -312,56 +398,77 @@ class NUnitAssertTrueMethod extends AssertTrueMethod, NUnitAssertMethod {
      this.getParameter(0).getType() instanceof BoolType
    )
  }
+
+  override int getAnAssertionIndex() { result = NUnitAssertMethod.super.getAnAssertionIndex() }
+
+  override int getAnAssertionIndex(boolean b) { result = this.getAnAssertionIndex() and b = true }
 }

 /** An NUnit negated assertion method. */
-class NUnitAssertFalseMethod extends AssertFalseMethod, NUnitAssertMethod {
+class NUnitAssertFalseMethod extends BooleanAssertMethod, NUnitAssertMethod {
  NUnitAssertFalseMethod() {
    exists(NUnitAssertClass c |
      this = c.getAFalseMethod() or
      this = c.getAnIsFalseMethod()
    )
  }
+
+  override int getAnAssertionIndex() { result = NUnitAssertMethod.super.getAnAssertionIndex() }
+
+  override int getAnAssertionIndex(boolean b) { result = this.getAnAssertionIndex() and b = false }
 }

 /** An NUnit `null` assertion method. */
-class NUnitAssertNullMethod extends AssertNullMethod, NUnitAssertMethod {
+class NUnitAssertNullMethod extends NullnessAssertMethod, NUnitAssertMethod {
  NUnitAssertNullMethod() {
    exists(NUnitAssertClass c |
      this = c.getANullMethod() or
      this = c.getAnIsNullMethod()
    )
  }
+
+  override int getAnAssertionIndex() { result = NUnitAssertMethod.super.getAnAssertionIndex() }
+
+  override int getAnAssertionIndex(boolean b) { result = this.getAnAssertionIndex() and b = true }
 }

 /** An NUnit non-`null` assertion method. */
-class NUnitAssertNonNullMethod extends AssertNonNullMethod, NUnitAssertMethod {
+class NUnitAssertNonNullMethod extends NullnessAssertMethod, NUnitAssertMethod {
  NUnitAssertNonNullMethod() {
    exists(NUnitAssertClass c |
      this = c.getANotNullMethod() or
      this = c.getAnIsNotNullMethod()
    )
  }
+
+  override int getAnAssertionIndex() { result = NUnitAssertMethod.super.getAnAssertionIndex() }
+
+  override int getAnAssertionIndex(boolean b) { result = this.getAnAssertionIndex() and b = false }
 }

 /** A method that forwards to another assertion method. */
 class ForwarderAssertMethod extends AssertMethod {
-  Assertion a;
-  Parameter p;
+  private Assertion a;
+  private Parameter p;
+  private int forwarderIndex;

  ForwarderAssertMethod() {
    p = this.getAParameter() and
    strictcount(AssignableDefinition def | def.getTarget() = p) = 1 and
    forex(ControlFlowElement body | body = this.getBody() |
      bodyAsserts(this, body, a) and
-      a.getAnExpr() = p.getAnAccess()
+      a.getExpr(forwarderIndex) = p.getAnAccess()
    )
  }

  override int getAnAssertionIndex() { result = p.getPosition() }

-  override Class getExceptionClass() {
-    result = this.getUnderlyingAssertMethod().getExceptionClass()
+  /** Gets the assertion index of the forwarded assertion, for assertion index `i`. */
+  int getAForwarderAssertionIndex(int i) { i = p.getPosition() and result = forwarderIndex }
+
+  override Class getExceptionClass(int i) {
+    i = p.getPosition() and
+    result = this.getUnderlyingAssertMethod().getExceptionClass(forwarderIndex)
  }

  /** Gets the underlying assertion method that is being forwarded to. */
@@ -386,25 +493,63 @@ private Stmt getAnAssertingStmt(Assertion a) {
  result.(BlockStmt).getFirstStmt() = getAnAssertingElement(a)
 }

+/** A method that forwards to a Boolean assertion method. */
+class ForwarderBooleanAssertMethod extends BooleanAssertMethod {
+  private ForwarderAssertMethod forwarder;
+  private BooleanAssertMethod underlying;
+
+  ForwarderBooleanAssertMethod() {
+    forwarder = this and
+    underlying = forwarder.getUnderlyingAssertMethod()
+  }
+
+  override int getAnAssertionIndex(boolean b) {
+    forwarder.getAForwarderAssertionIndex(result) = underlying.getAnAssertionIndex(b)
+  }
+
+  override Class getExceptionClass(int i) {
+    result = underlying.getExceptionClass(forwarder.getAForwarderAssertionIndex(i))
+  }
+}
+
 /** A method that forwards to a positive assertion method. */
-class ForwarderAssertTrueMethod extends ForwarderAssertMethod, AssertTrueMethod {
-  ForwarderAssertTrueMethod() { this.getUnderlyingAssertMethod() instanceof AssertTrueMethod }
+deprecated class ForwarderAssertTrueMethod extends ForwarderBooleanAssertMethod {
+  ForwarderAssertTrueMethod() { exists(this.getAnAssertionIndex(true)) }
 }

 /** A method that forwards to a negated assertion method. */
-class ForwarderAssertFalseMethod extends ForwarderAssertMethod, AssertFalseMethod {
-  ForwarderAssertFalseMethod() { this.getUnderlyingAssertMethod() instanceof AssertFalseMethod }
+deprecated class ForwarderAssertFalseMethod extends ForwarderBooleanAssertMethod {
+  ForwarderAssertFalseMethod() { exists(this.getAnAssertionIndex(false)) }
+}
+
+/** A method that forwards to a nullness assertion method. */
+class ForwarderNullnessAssertMethod extends NullnessAssertMethod {
+  private ForwarderAssertMethod forwarder;
+  private NullnessAssertMethod underlying;
+
+  ForwarderNullnessAssertMethod() {
+    forwarder = this and
+    underlying = forwarder.getUnderlyingAssertMethod()
+  }
+
+  override int getAnAssertionIndex(boolean b) {
+    forwarder.getAForwarderAssertionIndex(result) = underlying.getAnAssertionIndex(b)
+  }
+
+  override Class getExceptionClass(int i) {
+    result = underlying.getExceptionClass(forwarder.getAForwarderAssertionIndex(i))
+  }
 }

 /** A method that forwards to a `null` assertion method. */
-class ForwarderAssertNullMethod extends ForwarderAssertMethod, AssertNullMethod {
-  ForwarderAssertNullMethod() { this.getUnderlyingAssertMethod() instanceof AssertNullMethod }
+deprecated class ForwarderAssertNullMethod extends ForwarderNullnessAssertMethod {
+  ForwarderAssertNullMethod() { exists(this.getAnAssertionIndex(true)) }
 }

 /** A method that forwards to a non-`null` assertion method. */
-class ForwarderAssertNonNullMethod extends ForwarderAssertMethod, AssertNonNullMethod {
-  ForwarderAssertNonNullMethod() { this.getUnderlyingAssertMethod() instanceof AssertNonNullMethod }
+deprecated class ForwarderAssertNonNullMethod extends ForwarderNullnessAssertMethod {
+  ForwarderAssertNonNullMethod() { exists(this.getAnAssertionIndex(false)) }
 }

 /** Holds if expression `e` appears in an assertion. */
-predicate isExprInAssertion(Expr e) { e = any(Assertion a).getAnExpr().getAChildExpr*() }
+predicate isExprInAssertion(Expr e) { e = any(Assertion a).getExpr(_).getAChildExpr*() }
--- a/csharp/ql/src/semmle/code/csharp/controlflow/internal/Completion.qll
+++ b/csharp/ql/src/semmle/code/csharp/controlflow/internal/Completion.qll
@@ -99,12 +99,7 @@ class Completion extends TCompletion {
    cfe instanceof ThrowElement and
    this = TThrowCompletion(cfe.(ThrowElement).getThrownExceptionType())
    or
-    exists(AssertMethod m | assertion(cfe, m, _) |
-      this = TThrowCompletion(m.getExceptionClass())
-      or
-      not exists(m.getExceptionClass()) and
-      this = TExitCompletion()
-    )
+    this = assertionCompletion(cfe, _)
    or
    completionIsValidForStmt(cfe, this)
    or
@@ -390,11 +385,22 @@ private predicate invalidCastCandidate(CastExpr ce) {
  ce.getType() = ce.getExpr().getType().(ValueOrRefType).getASubType+()
 }

-private predicate assertion(Assertion a, AssertMethod am, Expr e) {
-  e = a.getAnExpr() and
+private predicate assertion(Assertion a, int i, AssertMethod am, Expr e) {
+  e = a.getExpr(i) and
  am = a.getAssertMethod()
 }

+/** Gets a valid completion when argument `i` fails in assertion `a`. */
+Completion assertionCompletion(Assertion a, int i) {
+  exists(AssertMethod am | am = a.getAssertMethod() |
+    result = TThrowCompletion(am.getExceptionClass(i))
+    or
+    i = am.getAnAssertionIndex() and
+    not exists(am.getExceptionClass(i)) and
+    result = TExitCompletion()
+  )
+}
+
 /**
 * Holds if a normal completion of `e` must be a Boolean completion.
 */
@@ -422,8 +428,11 @@ private predicate inBooleanContext(Expr e, boolean isBooleanCompletionForParent)
  or
  exists(SpecificCatchClause scc | scc.getFilterClause() = e | isBooleanCompletionForParent = false)
  or
-  assertion(_, [any(AssertTrueMethod m).(AssertMethod), any(AssertFalseMethod m)], e) and
-  isBooleanCompletionForParent = false
+  exists(BooleanAssertMethod m, int i |
+    assertion(_, i, m, e) and
+    i = m.getAnAssertionIndex(_) and
+    isBooleanCompletionForParent = false
+  )
  or
  exists(LogicalNotExpr lne | lne.getAnOperand() = e |
    inBooleanContext(lne, _) and
@@ -495,8 +504,11 @@ private predicate inNullnessContext(Expr e, boolean isNullnessCompletionForParen
    isNullnessCompletionForParent = false
  )
  or
-  assertion(_, [any(AssertNullMethod m).(AssertMethod), any(AssertNonNullMethod m)], e) and
-  isNullnessCompletionForParent = false
+  exists(NullnessAssertMethod m, int i |
+    assertion(_, i, m, e) and
+    i = m.getAnAssertionIndex(_) and
+    isNullnessCompletionForParent = false
+  )
  or
  exists(ConditionalExpr ce | inNullnessContext(ce, _) |
    (e = ce.getThen() or e = ce.getElse()) and
--- a/csharp/ql/src/semmle/code/csharp/controlflow/internal/NonReturning.qll
+++ b/csharp/ql/src/semmle/code/csharp/controlflow/internal/NonReturning.qll
@@ -23,9 +23,7 @@ private class ExitingCall extends NonReturningCall {
  ExitingCall() {
    this.getTarget() instanceof ExitingCallable
    or
-    exists(AssertMethod m | m = this.(FailingAssertion).getAssertMethod() |
-      not exists(m.getExceptionClass())
-    )
+    this = any(FailingAssertion fa | not exists(fa.getExceptionClass()))
  }

  override ExitCompletion getACompletion() { not result instanceof NestedCompletion }
@@ -39,9 +37,7 @@ private class ThrowingCall extends NonReturningCall {
    (
      c = this.getTarget().(ThrowingCallable).getACallCompletion()
      or
-      exists(AssertMethod m | m = this.(FailingAssertion).getAssertMethod() |
-        c.getExceptionClass() = m.getExceptionClass()
-      )
+      c.getExceptionClass() = this.(FailingAssertion).getExceptionClass()
      or
      exists(CIL::Method m, CIL::Type ex |
        this.getTarget().matchesHandle(m) and
--- a/csharp/ql/src/semmle/code/csharp/controlflow/internal/Splitting.qll
+++ b/csharp/ql/src/semmle/code/csharp/controlflow/internal/Splitting.qll
@@ -36,14 +36,17 @@ private module Cached {
  cached
  newtype TSplit =
    TInitializerSplit(Constructor c) { InitializerSplitting::constructorInitializes(c, _) } or
-    TAssertionSplit(AssertionSplitting::Assertion a, boolean success) { success = [true, false] } or
+    TAssertionSplit(AssertionSplitting::Assertion a, int i, boolean success) {
+      exists(a.getExpr(i)) and
+      success in [false, true]
+    } or
    TFinallySplit(FinallySplitting::FinallySplitType type, int nestLevel) {
      nestLevel = FinallySplitting::nestLevel(_)
    } or
    TExceptionHandlerSplit(ExceptionClass ec) or
    TBooleanSplit(BooleanSplitting::BooleanSplitSubKind kind, boolean branch) {
      kind.startsSplit(_) and
-      (branch = true or branch = false)
+      branch in [false, true]
    } or
    TLoopSplit(LoopSplitting::AnalyzableLoopStmt loop)

@@ -414,8 +417,9 @@ module AssertionSplitting {
  class AssertionSplitImpl extends SplitImpl, TAssertionSplit {
    Assertion a;
    boolean success;
+    int i;

-    AssertionSplitImpl() { this = TAssertionSplit(a, success) }
+    AssertionSplitImpl() { this = TAssertionSplit(a, i, success) }

    /** Gets the assertion. */
    Assertion getAssertion() { result = a }
@@ -445,37 +449,29 @@ module AssertionSplitting {

    override predicate hasEntry(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
      exists(AssertMethod m |
-        pred = last(a.getAnExpr(), c) and
+        pred = last(a.getExpr(i), c) and
        succ = succ(pred, c) and
-        this.getAssertion() = a and
-        m = a.getAssertMethod()
+        m = a.getAssertMethod() and
+        // The assertion only succeeds when all asserted arguments succeeded, so
+        // we only enter a "success" state after the last argument has succeeded.
+        //
+        // The split is only entered if we are not already in a "failing" state
+        // for one of the previous arguments, which ensures that the "success"
+        // state is only entered when all arguments succeed. This also means
+        // that if multiple arguments fail, then the first failing argument
+        // will determine the exception being thrown by the assertion.
+        if success = true then i = max(int j | exists(a.getExpr(j))) else any()
      |
-        m instanceof AssertTrueMethod and
-        (
-          c instanceof TrueCompletion and success = true
+        exists(boolean b | i = m.(BooleanAssertMethod).getAnAssertionIndex(b) |
+          c instanceof TrueCompletion and success = b
          or
-          c instanceof FalseCompletion and success = false
+          c instanceof FalseCompletion and success = b.booleanNot()
        )
        or
-        m instanceof AssertFalseMethod and
-        (
-          c instanceof TrueCompletion and success = false
+        exists(boolean b | i = m.(NullnessAssertMethod).getAnAssertionIndex(b) |
+          c.(NullnessCompletion).isNull() and success = b
          or
-          c instanceof FalseCompletion and success = true
-        )
-        or
-        m instanceof AssertNullMethod and
-        (
-          c.(NullnessCompletion).isNull() and success = true
-          or
-          c.(NullnessCompletion).isNonNull() and success = false
-        )
-        or
-        m instanceof AssertNonNullMethod and
-        (
-          c.(NullnessCompletion).isNull() and success = false
-          or
-          c.(NullnessCompletion).isNonNull() and success = true
+          c.(NullnessCompletion).isNonNull() and success = b.booleanNot()
        )
      )
    }
@@ -491,7 +487,7 @@ module AssertionSplitting {
        c instanceof NormalCompletion
        or
        success = false and
-        not c instanceof NormalCompletion
+        c = assertionCompletion(a, i)
      )
    }

@@ -504,7 +500,7 @@ module AssertionSplitting {
        c instanceof NormalCompletion
        or
        success = false and
-        not c instanceof NormalCompletion
+        c = assertionCompletion(a, i)
      )
    }

@@ -1604,7 +1600,7 @@ private module SuccSplits {

  /**
   * Holds if `succSplits` should not inherit a split of kind `sk` from
-   * `predSplits, except possibly because of a split in `except`.
+   * `predSplits`, except possibly because of a split in `except`.
   *
   * The predicate is written using explicit recursion, as opposed to a `forall`,
   * to avoid negative recursion.
--- a/csharp/ql/test/library-tests/commons/Assertions/Assertions.ql
+++ b/csharp/ql/test/library-tests/commons/Assertions/Assertions.ql
@@ -2,21 +2,29 @@ import csharp
 import semmle.code.csharp.commons.Assertions

 query predicate assertTrue(Assertion a, Expr e) {
-  a.getAnExpr() = e and
-  a.getTarget() instanceof AssertTrueMethod
+  exists(int i |
+    a.getExpr(i) = e and
+    i = a.getTarget().(BooleanAssertMethod).getAnAssertionIndex(true)
+  )
 }

 query predicate assertFalse(Assertion a, Expr e) {
-  a.getAnExpr() = e and
-  a.getTarget() instanceof AssertFalseMethod
+  exists(int i |
+    a.getExpr(i) = e and
+    i = a.getTarget().(BooleanAssertMethod).getAnAssertionIndex(false)
+  )
 }

 query predicate assertNull(Assertion a, Expr e) {
-  a.getAnExpr() = e and
-  a.getTarget() instanceof AssertNullMethod
+  exists(int i |
+    a.getExpr(i) = e and
+    i = a.getTarget().(NullnessAssertMethod).getAnAssertionIndex(true)
+  )
 }

 query predicate assertNonNull(Assertion a, Expr e) {
-  a.getAnExpr() = e and
-  a.getTarget() instanceof AssertNonNullMethod
+  exists(int i |
+    a.getExpr(i) = e and
+    i = a.getTarget().(NullnessAssertMethod).getAnAssertionIndex(false)
+  )
 }
--- a/csharp/ql/test/library-tests/controlflow/graph/Assert.cs
+++ b/csharp/ql/test/library-tests/controlflow/graph/Assert.cs
@@ -127,4 +127,17 @@ class AssertTests
        Assert.IsFalse(s != null || !b);
        Console.WriteLine(s.Length);
    }
+
+    private void AssertTrueFalse(
+           [System.Diagnostics.CodeAnalysis.DoesNotReturnIf(false)] bool condition1,
+           [System.Diagnostics.CodeAnalysis.DoesNotReturnIf(true)] bool condition2,
+           bool nonCondition)
+    {
+    }
+
+    void M13(bool b1, bool b2, bool b3)
+    {
+        AssertTrueFalse(b1, b2, b3);
+        return;
+    }
 }
--- a/csharp/ql/test/library-tests/controlflow/graph/BasicBlock.expected
+++ b/csharp/ql/test/library-tests/controlflow/graph/BasicBlock.expected
@@ -134,6 +134,13 @@
 | Assert.cs:123:36:123:36 | [b (line 84): true] access to parameter b | Assert.cs:127:24:127:32 | [b (line 84): true] ... != ... | 16 |
 | Assert.cs:127:9:127:39 | [assertion failure] call to method IsFalse | Assert.cs:127:9:127:39 | [assertion failure] call to method IsFalse | 1 |
 | Assert.cs:127:37:127:38 | [b (line 84): true] !... | Assert.cs:128:9:128:35 | call to method WriteLine | 7 |
+| Assert.cs:131:18:131:32 | enter AssertTrueFalse | Assert.cs:131:18:131:32 | exit AssertTrueFalse | 3 |
+| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:25:140:26 | access to parameter b1 | 5 |
+| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:138:10:138:12 | exit M13 | 1 |
+| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | 3 |
+| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:29:140:30 | access to parameter b2 | 1 |
+| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | 2 |
+| Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | Assert.cs:141:9:141:15 | return ...; | 3 |
 | Assignments.cs:3:10:3:10 | enter M | Assignments.cs:3:10:3:10 | exit M | 33 |
 | Assignments.cs:14:18:14:35 | enter (...) => ... | Assignments.cs:14:18:14:35 | exit (...) => ... | 3 |
 | Assignments.cs:17:40:17:40 | enter + | Assignments.cs:17:40:17:40 | exit + | 5 |
--- a/csharp/ql/test/library-tests/controlflow/graph/Condition.expected
+++ b/csharp/ql/test/library-tests/controlflow/graph/Condition.expected
@@ -294,6 +294,12 @@ conditionBlock
 | Assert.cs:119:37:119:38 | [b (line 84): true] !... | Assert.cs:127:37:127:38 | [b (line 84): true] !... | true |
 | Assert.cs:123:36:123:36 | [b (line 84): true] access to parameter b | Assert.cs:127:9:127:39 | [assertion failure] call to method IsFalse | true |
 | Assert.cs:123:36:123:36 | [b (line 84): true] access to parameter b | Assert.cs:127:37:127:38 | [b (line 84): true] !... | false |
+| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | false |
+| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:29:140:30 | access to parameter b2 | true |
+| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | true |
+| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | true |
+| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | true |
+| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | false |
 | BreakInTry.cs:7:13:11:13 | foreach (... ... in ...) ... | BreakInTry.cs:7:26:7:28 | String arg | false |
 | BreakInTry.cs:7:13:11:13 | foreach (... ... in ...) ... | BreakInTry.cs:10:21:10:26 | break; | false |
 | BreakInTry.cs:7:26:7:28 | String arg | BreakInTry.cs:10:21:10:26 | break; | true |
@@ -1207,6 +1213,12 @@ conditionFlow
 | Assert.cs:127:24:127:32 | [b (line 84): true] ... != ... | Assert.cs:127:9:127:39 | [assertion failure] call to method IsFalse | true |
 | Assert.cs:127:24:127:32 | [b (line 84): true] ... != ... | Assert.cs:127:37:127:38 | [b (line 84): true] !... | false |
 | Assert.cs:127:38:127:38 | [b (line 84): true] access to parameter b | Assert.cs:127:9:127:39 | [assertion success] call to method IsFalse | true |
+| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | false |
+| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | access to parameter b2 | true |
+| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | false |
+| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | true |
+| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | true |
+| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | false |
 | BreakInTry.cs:9:21:9:31 | ... == ... | BreakInTry.cs:7:13:11:13 | foreach (... ... in ...) ... | false |
 | BreakInTry.cs:9:21:9:31 | ... == ... | BreakInTry.cs:10:21:10:26 | break; | true |
 | BreakInTry.cs:15:17:15:28 | ... == ... | BreakInTry.cs:3:10:3:11 | exit M1 | false |
--- a/csharp/ql/test/library-tests/controlflow/graph/Consistency.expected
+++ b/csharp/ql/test/library-tests/controlflow/graph/Consistency.expected
@@ -3,6 +3,8 @@ nonUniqueSetRepresentation
 breakInvariant2
 breakInvariant3
 breakInvariant4
+| Assert.cs:140:29:140:30 | access to parameter b2 | assertion failure | Assert.cs:140:33:140:34 | access to parameter b3 | assertion failure | assertion failure | true |
+| Assert.cs:140:29:140:30 | access to parameter b2 | assertion failure | Assert.cs:140:33:140:34 | access to parameter b3 | assertion failure | assertion success | false |
 breakInvariant5
 multipleSuccessors
 | ConditionalAccess.cs:30:28:30:32 | ... = ... | successor | ConditionalAccess.cs:1:7:1:23 | exit ConditionalAccess |
--- a/csharp/ql/test/library-tests/controlflow/graph/Dominance.expected
+++ b/csharp/ql/test/library-tests/controlflow/graph/Dominance.expected
@@ -801,6 +801,21 @@ dominance
 | Assert.cs:128:9:128:36 | ...; | Assert.cs:128:27:128:27 | access to local variable s |
 | Assert.cs:128:27:128:27 | access to local variable s | Assert.cs:128:27:128:34 | access to property Length |
 | Assert.cs:128:27:128:34 | access to property Length | Assert.cs:128:9:128:35 | call to method WriteLine |
+| Assert.cs:131:18:131:32 | enter AssertTrueFalse | Assert.cs:135:5:136:5 | {...} |
+| Assert.cs:135:5:136:5 | {...} | Assert.cs:131:18:131:32 | exit AssertTrueFalse |
+| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:139:5:142:5 | {...} |
+| Assert.cs:139:5:142:5 | {...} | Assert.cs:140:9:140:36 | ...; |
+| Assert.cs:140:9:140:35 | [assertion success] call to method AssertTrueFalse | Assert.cs:141:9:141:15 | return ...; |
+| Assert.cs:140:9:140:35 | this access | Assert.cs:140:25:140:26 | access to parameter b1 |
+| Assert.cs:140:9:140:36 | ...; | Assert.cs:140:9:140:35 | this access |
+| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 |
+| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | access to parameter b2 |
+| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 |
+| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 |
+| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 |
+| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse |
+| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse |
+| Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | Assert.cs:140:9:140:35 | [assertion success] call to method AssertTrueFalse |
 | Assignments.cs:3:10:3:10 | enter M | Assignments.cs:4:5:15:5 | {...} |
 | Assignments.cs:4:5:15:5 | {...} | Assignments.cs:5:9:5:18 | ... ...; |
 | Assignments.cs:5:9:5:18 | ... ...; | Assignments.cs:5:17:5:17 | 0 |
@@ -4534,6 +4549,20 @@ postDominance
 | Assert.cs:128:9:128:36 | ...; | Assert.cs:127:9:127:39 | [assertion success] call to method IsFalse |
 | Assert.cs:128:27:128:27 | access to local variable s | Assert.cs:128:9:128:36 | ...; |
 | Assert.cs:128:27:128:34 | access to property Length | Assert.cs:128:27:128:27 | access to local variable s |
+| Assert.cs:131:18:131:32 | exit AssertTrueFalse | Assert.cs:135:5:136:5 | {...} |
+| Assert.cs:135:5:136:5 | {...} | Assert.cs:131:18:131:32 | enter AssertTrueFalse |
+| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse |
+| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse |
+| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:141:9:141:15 | return ...; |
+| Assert.cs:139:5:142:5 | {...} | Assert.cs:138:10:138:12 | enter M13 |
+| Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 |
+| Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 |
+| Assert.cs:140:9:140:35 | [assertion success] call to method AssertTrueFalse | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 |
+| Assert.cs:140:9:140:35 | this access | Assert.cs:140:9:140:36 | ...; |
+| Assert.cs:140:9:140:36 | ...; | Assert.cs:139:5:142:5 | {...} |
+| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:9:140:35 | this access |
+| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 |
+| Assert.cs:141:9:141:15 | return ...; | Assert.cs:140:9:140:35 | [assertion success] call to method AssertTrueFalse |
 | Assignments.cs:3:10:3:10 | exit M | Assignments.cs:14:9:14:35 | ... += ... |
 | Assignments.cs:4:5:15:5 | {...} | Assignments.cs:3:10:3:10 | enter M |
 | Assignments.cs:5:9:5:18 | ... ...; | Assignments.cs:4:5:15:5 | {...} |
@@ -7880,6 +7909,20 @@ blockDominance
 | Assert.cs:123:36:123:36 | [b (line 84): true] access to parameter b | Assert.cs:127:37:127:38 | [b (line 84): true] !... |
 | Assert.cs:127:9:127:39 | [assertion failure] call to method IsFalse | Assert.cs:127:9:127:39 | [assertion failure] call to method IsFalse |
 | Assert.cs:127:37:127:38 | [b (line 84): true] !... | Assert.cs:127:37:127:38 | [b (line 84): true] !... |
+| Assert.cs:131:18:131:32 | enter AssertTrueFalse | Assert.cs:131:18:131:32 | enter AssertTrueFalse |
+| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:138:10:138:12 | enter M13 |
+| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:138:10:138:12 | exit M13 |
+| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 |
+| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:29:140:30 | access to parameter b2 |
+| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 |
+| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 |
+| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:138:10:138:12 | exit M13 |
+| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 |
+| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:29:140:30 | access to parameter b2 |
+| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 |
+| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 |
+| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 |
+| Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 |
 | Assignments.cs:3:10:3:10 | enter M | Assignments.cs:3:10:3:10 | enter M |
 | Assignments.cs:14:18:14:35 | enter (...) => ... | Assignments.cs:14:18:14:35 | enter (...) => ... |
 | Assignments.cs:17:40:17:40 | enter + | Assignments.cs:17:40:17:40 | enter + |
@@ -10628,6 +10671,18 @@ postBlockDominance
 | Assert.cs:123:36:123:36 | [b (line 84): true] access to parameter b | Assert.cs:123:36:123:36 | [b (line 84): true] access to parameter b |
 | Assert.cs:127:9:127:39 | [assertion failure] call to method IsFalse | Assert.cs:127:9:127:39 | [assertion failure] call to method IsFalse |
 | Assert.cs:127:37:127:38 | [b (line 84): true] !... | Assert.cs:127:37:127:38 | [b (line 84): true] !... |
+| Assert.cs:131:18:131:32 | enter AssertTrueFalse | Assert.cs:131:18:131:32 | enter AssertTrueFalse |
+| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:138:10:138:12 | enter M13 |
+| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:138:10:138:12 | enter M13 |
+| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:138:10:138:12 | exit M13 |
+| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 |
+| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:140:29:140:30 | access to parameter b2 |
+| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 |
+| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 |
+| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 |
+| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:29:140:30 | access to parameter b2 |
+| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 |
+| Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 |
 | Assignments.cs:3:10:3:10 | enter M | Assignments.cs:3:10:3:10 | enter M |
 | Assignments.cs:14:18:14:35 | enter (...) => ... | Assignments.cs:14:18:14:35 | enter (...) => ... |
 | Assignments.cs:17:40:17:40 | enter + | Assignments.cs:17:40:17:40 | enter + |
--- a/csharp/ql/test/library-tests/controlflow/graph/EnclosingCallable.expected
+++ b/csharp/ql/test/library-tests/controlflow/graph/EnclosingCallable.expected
@@ -853,6 +853,24 @@ nodeEnclosing
 | Assert.cs:128:9:128:36 | ...; | Assert.cs:84:10:84:12 | M12 |
 | Assert.cs:128:27:128:27 | access to local variable s | Assert.cs:84:10:84:12 | M12 |
 | Assert.cs:128:27:128:34 | access to property Length | Assert.cs:84:10:84:12 | M12 |
+| Assert.cs:131:18:131:32 | enter AssertTrueFalse | Assert.cs:131:18:131:32 | AssertTrueFalse |
+| Assert.cs:131:18:131:32 | exit AssertTrueFalse | Assert.cs:131:18:131:32 | AssertTrueFalse |
+| Assert.cs:135:5:136:5 | {...} | Assert.cs:131:18:131:32 | AssertTrueFalse |
+| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:139:5:142:5 | {...} | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:140:9:140:35 | [assertion success] call to method AssertTrueFalse | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:140:9:140:35 | this access | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:140:9:140:36 | ...; | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:141:9:141:15 | return ...; | Assert.cs:138:10:138:12 | M13 |
 | Assignments.cs:3:10:3:10 | enter M | Assignments.cs:3:10:3:10 | M |
 | Assignments.cs:3:10:3:10 | exit M | Assignments.cs:3:10:3:10 | M |
 | Assignments.cs:4:5:15:5 | {...} | Assignments.cs:3:10:3:10 | M |
@@ -4338,6 +4356,13 @@ blockEnclosing
 | Assert.cs:123:36:123:36 | [b (line 84): true] access to parameter b | Assert.cs:84:10:84:12 | M12 |
 | Assert.cs:127:9:127:39 | [assertion failure] call to method IsFalse | Assert.cs:84:10:84:12 | M12 |
 | Assert.cs:127:37:127:38 | [b (line 84): true] !... | Assert.cs:84:10:84:12 | M12 |
+| Assert.cs:131:18:131:32 | enter AssertTrueFalse | Assert.cs:131:18:131:32 | AssertTrueFalse |
+| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:138:10:138:12 | exit M13 | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:138:10:138:12 | M13 |
+| Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | Assert.cs:138:10:138:12 | M13 |
 | Assignments.cs:3:10:3:10 | enter M | Assignments.cs:3:10:3:10 | M |
 | Assignments.cs:14:18:14:35 | enter (...) => ... | Assignments.cs:14:18:14:35 | (...) => ... |
 | Assignments.cs:17:40:17:40 | enter + | Assignments.cs:17:40:17:40 | + |
--- a/csharp/ql/test/library-tests/controlflow/graph/EntryElement.expected
+++ b/csharp/ql/test/library-tests/controlflow/graph/EntryElement.expected
@@ -659,6 +659,17 @@
 | Assert.cs:128:9:128:36 | ...; | Assert.cs:128:9:128:36 | ...; |
 | Assert.cs:128:27:128:27 | access to local variable s | Assert.cs:128:27:128:27 | access to local variable s |
 | Assert.cs:128:27:128:34 | access to property Length | Assert.cs:128:27:128:27 | access to local variable s |
+| Assert.cs:132:61:132:65 | false | Assert.cs:132:61:132:65 | false |
+| Assert.cs:133:61:133:64 | true | Assert.cs:133:61:133:64 | true |
+| Assert.cs:135:5:136:5 | {...} | Assert.cs:135:5:136:5 | {...} |
+| Assert.cs:139:5:142:5 | {...} | Assert.cs:139:5:142:5 | {...} |
+| Assert.cs:140:9:140:35 | call to method AssertTrueFalse | Assert.cs:140:9:140:35 | this access |
+| Assert.cs:140:9:140:35 | this access | Assert.cs:140:9:140:35 | this access |
+| Assert.cs:140:9:140:36 | ...; | Assert.cs:140:9:140:36 | ...; |
+| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:25:140:26 | access to parameter b1 |
+| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:29:140:30 | access to parameter b2 |
+| Assert.cs:140:33:140:34 | access to parameter b3 | Assert.cs:140:33:140:34 | access to parameter b3 |
+| Assert.cs:141:9:141:15 | return ...; | Assert.cs:141:9:141:15 | return ...; |
 | Assignments.cs:4:5:15:5 | {...} | Assignments.cs:4:5:15:5 | {...} |
 | Assignments.cs:5:9:5:18 | ... ...; | Assignments.cs:5:9:5:18 | ... ...; |
 | Assignments.cs:5:13:5:17 | Int32 x = ... | Assignments.cs:5:17:5:17 | 0 |
--- a/csharp/ql/test/library-tests/controlflow/graph/ExitElement.expected
+++ b/csharp/ql/test/library-tests/controlflow/graph/ExitElement.expected
@@ -817,6 +817,22 @@
 | Assert.cs:128:9:128:36 | ...; | Assert.cs:128:9:128:35 | call to method WriteLine | normal |
 | Assert.cs:128:27:128:27 | access to local variable s | Assert.cs:128:27:128:27 | access to local variable s | normal |
 | Assert.cs:128:27:128:34 | access to property Length | Assert.cs:128:27:128:34 | access to property Length | normal |
+| Assert.cs:132:61:132:65 | false | Assert.cs:132:61:132:65 | false | normal |
+| Assert.cs:133:61:133:64 | true | Assert.cs:133:61:133:64 | true | normal |
+| Assert.cs:135:5:136:5 | {...} | Assert.cs:135:5:136:5 | {...} | normal |
+| Assert.cs:139:5:142:5 | {...} | Assert.cs:140:9:140:35 | call to method AssertTrueFalse | throw(Exception) |
+| Assert.cs:139:5:142:5 | {...} | Assert.cs:141:9:141:15 | return ...; | return |
+| Assert.cs:140:9:140:35 | call to method AssertTrueFalse | Assert.cs:140:9:140:35 | call to method AssertTrueFalse | normal |
+| Assert.cs:140:9:140:35 | call to method AssertTrueFalse | Assert.cs:140:9:140:35 | call to method AssertTrueFalse | throw(Exception) |
+| Assert.cs:140:9:140:35 | this access | Assert.cs:140:9:140:35 | this access | normal |
+| Assert.cs:140:9:140:36 | ...; | Assert.cs:140:9:140:35 | call to method AssertTrueFalse | normal |
+| Assert.cs:140:9:140:36 | ...; | Assert.cs:140:9:140:35 | call to method AssertTrueFalse | throw(Exception) |
+| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:25:140:26 | access to parameter b1 | false |
+| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:25:140:26 | access to parameter b1 | true |
+| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:29:140:30 | access to parameter b2 | false |
+| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:29:140:30 | access to parameter b2 | true |
+| Assert.cs:140:33:140:34 | access to parameter b3 | Assert.cs:140:33:140:34 | access to parameter b3 | normal |
+| Assert.cs:141:9:141:15 | return ...; | Assert.cs:141:9:141:15 | return ...; | return |
 | Assignments.cs:4:5:15:5 | {...} | Assignments.cs:14:9:14:35 | ... += ... | normal |
 | Assignments.cs:5:9:5:18 | ... ...; | Assignments.cs:5:13:5:17 | Int32 x = ... | normal |
 | Assignments.cs:5:13:5:17 | Int32 x = ... | Assignments.cs:5:13:5:17 | Int32 x = ... | normal |
--- a/csharp/ql/test/library-tests/controlflow/graph/NodeGraph.expected
+++ b/csharp/ql/test/library-tests/controlflow/graph/NodeGraph.expected
@@ -869,6 +869,25 @@
 | Assert.cs:128:9:128:36 | ...; | Assert.cs:128:27:128:27 | access to local variable s | semmle.label | successor |
 | Assert.cs:128:27:128:27 | access to local variable s | Assert.cs:128:27:128:34 | access to property Length | semmle.label | successor |
 | Assert.cs:128:27:128:34 | access to property Length | Assert.cs:128:9:128:35 | call to method WriteLine | semmle.label | successor |
+| Assert.cs:131:18:131:32 | enter AssertTrueFalse | Assert.cs:135:5:136:5 | {...} | semmle.label | successor |
+| Assert.cs:135:5:136:5 | {...} | Assert.cs:131:18:131:32 | exit AssertTrueFalse | semmle.label | successor |
+| Assert.cs:138:10:138:12 | enter M13 | Assert.cs:139:5:142:5 | {...} | semmle.label | successor |
+| Assert.cs:139:5:142:5 | {...} | Assert.cs:140:9:140:36 | ...; | semmle.label | successor |
+| Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | Assert.cs:138:10:138:12 | exit M13 | semmle.label | exception(Exception) |
+| Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | Assert.cs:138:10:138:12 | exit M13 | semmle.label | exception(Exception) |
+| Assert.cs:140:9:140:35 | [assertion success] call to method AssertTrueFalse | Assert.cs:141:9:141:15 | return ...; | semmle.label | successor |
+| Assert.cs:140:9:140:35 | this access | Assert.cs:140:25:140:26 | access to parameter b1 | semmle.label | successor |
+| Assert.cs:140:9:140:36 | ...; | Assert.cs:140:9:140:35 | this access | semmle.label | successor |
+| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | semmle.label | false |
+| Assert.cs:140:25:140:26 | access to parameter b1 | Assert.cs:140:29:140:30 | access to parameter b2 | semmle.label | true |
+| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | semmle.label | false |
+| Assert.cs:140:29:140:30 | [assertion failure] access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | semmle.label | true |
+| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | semmle.label | true |
+| Assert.cs:140:29:140:30 | access to parameter b2 | Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | semmle.label | false |
+| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | semmle.label | successor |
+| Assert.cs:140:33:140:34 | [assertion failure] access to parameter b3 | Assert.cs:140:9:140:35 | [assertion failure] call to method AssertTrueFalse | semmle.label | successor |
+| Assert.cs:140:33:140:34 | [assertion success] access to parameter b3 | Assert.cs:140:9:140:35 | [assertion success] call to method AssertTrueFalse | semmle.label | successor |
+| Assert.cs:141:9:141:15 | return ...; | Assert.cs:138:10:138:12 | exit M13 | semmle.label | return |
 | Assignments.cs:3:10:3:10 | enter M | Assignments.cs:4:5:15:5 | {...} | semmle.label | successor |
 | Assignments.cs:4:5:15:5 | {...} | Assignments.cs:5:9:5:18 | ... ...; | semmle.label | successor |
 | Assignments.cs:5:9:5:18 | ... ...; | Assignments.cs:5:17:5:17 | 0 | semmle.label | successor |
--- a/csharp/ql/test/library-tests/controlflow/graph/Nodes.expected
+++ b/csharp/ql/test/library-tests/controlflow/graph/Nodes.expected
@@ -1000,6 +1000,8 @@ entryPoint
 | Assert.cs:70:10:70:12 | M10 | Assert.cs:71:5:75:5 | {...} |
 | Assert.cs:77:10:77:12 | M11 | Assert.cs:78:5:82:5 | {...} |
 | Assert.cs:84:10:84:12 | M12 | Assert.cs:85:5:129:5 | {...} |
+| Assert.cs:131:18:131:32 | AssertTrueFalse | Assert.cs:135:5:136:5 | {...} |
+| Assert.cs:138:10:138:12 | M13 | Assert.cs:139:5:142:5 | {...} |
 | Assignments.cs:3:10:3:10 | M | Assignments.cs:4:5:15:5 | {...} |
 | Assignments.cs:14:18:14:35 | (...) => ... | Assignments.cs:14:33:14:35 | {...} |
 | Assignments.cs:17:40:17:40 | + | Assignments.cs:18:5:20:5 | {...} |
--- a/csharp/ql/test/library-tests/controlflow/guards/AbstractValue.expected
+++ b/csharp/ql/test/library-tests/controlflow/guards/AbstractValue.expected
@@ -72,6 +72,7 @@ abstractValue
 | empty | Collections.cs:87:17:87:32 | array creation of type String[] |
 | empty | Collections.cs:87:30:87:32 | { ..., ... } |
 | empty | Collections.cs:88:22:88:24 | { ..., ... } |
+| false | Assert.cs:85:61:85:65 | false |
 | false | Guards.cs:178:16:178:20 | false |
 | false | Guards.cs:181:53:181:57 | false |
 | false | Guards.cs:217:18:217:22 | false |
@@ -124,6 +125,7 @@ abstractValue
 | non-null | Assert.cs:79:31:79:32 | "" |
 | non-null | Assert.cs:80:9:80:14 | access to type Assert |
 | non-null | Assert.cs:81:9:81:15 | access to type Console |
+| non-null | Assert.cs:93:9:93:35 | this access |
 | non-null | Collections.cs:12:17:12:20 | access to parameter args |
 | non-null | Collections.cs:13:13:13:16 | access to parameter args |
 | non-null | Collections.cs:14:13:14:16 | access to parameter args |
@@ -457,6 +459,7 @@ abstractValue
 | null | Splitting.cs:116:27:116:30 | null |
 | null | Splitting.cs:125:21:125:24 | null |
 | null | Splitting.cs:129:22:129:25 | null |
+| true | Assert.cs:86:61:86:64 | true |
 | true | Guards.cs:177:20:177:23 | true |
 | true | Guards.cs:181:46:181:49 | true |
 | true | Guards.cs:185:50:185:53 | true |
--- a/csharp/ql/test/library-tests/controlflow/guards/Assert.cs
+++ b/csharp/ql/test/library-tests/controlflow/guards/Assert.cs
@@ -80,6 +80,19 @@ class AssertTests
        Assert.IsFalse(s != null || b);
        Console.WriteLine(s.Length);
    }
+
+    private void AssertTrueFalse(
+           [System.Diagnostics.CodeAnalysis.DoesNotReturnIf(false)] bool condition1,
+           [System.Diagnostics.CodeAnalysis.DoesNotReturnIf(true)] bool condition2,
+           bool nonCondition)
+    {
+    }
+
+    bool M12(bool b1, bool b2)
+    {
+        AssertTrueFalse(b1, b2, b2);
+        return b1 && !b2;
+    }
 }

 // semmle-extractor-options: ${testdir}/../../../resources/stubs/Microsoft.VisualStudio.TestTools.UnitTesting.cs
--- a/csharp/ql/test/library-tests/controlflow/guards/BooleanGuardedExpr.expected
+++ b/csharp/ql/test/library-tests/controlflow/guards/BooleanGuardedExpr.expected
@@ -11,6 +11,8 @@
 | Assert.cs:74:27:74:27 | access to local variable s | Assert.cs:73:23:73:31 | ... == ... | Assert.cs:73:23:73:23 | access to local variable s | true |
 | Assert.cs:80:37:80:37 | access to parameter b | Assert.cs:79:20:79:20 | access to parameter b | Assert.cs:79:20:79:20 | access to parameter b | true |
 | Assert.cs:81:27:81:27 | access to local variable s | Assert.cs:80:24:80:32 | ... != ... | Assert.cs:80:24:80:24 | access to local variable s | false |
+| Assert.cs:94:16:94:17 | access to parameter b1 | Assert.cs:93:25:93:26 | access to parameter b1 | Assert.cs:93:25:93:26 | access to parameter b1 | true |
+| Assert.cs:94:23:94:24 | access to parameter b2 | Assert.cs:93:29:93:30 | access to parameter b2 | Assert.cs:93:29:93:30 | access to parameter b2 | false |
 | Collections.cs:52:17:52:20 | access to parameter args | Collections.cs:50:13:50:27 | ... == ... | Collections.cs:50:13:50:16 | access to parameter args | false |
 | Collections.cs:53:9:53:12 | access to parameter args | Collections.cs:50:13:50:27 | ... == ... | Collections.cs:50:13:50:16 | access to parameter args | false |
 | Collections.cs:54:13:54:16 | access to parameter args | Collections.cs:50:13:50:27 | ... == ... | Collections.cs:50:13:50:16 | access to parameter args | false |
--- a/csharp/ql/test/library-tests/controlflow/guards/GuardedControlFlowNode.expected
+++ b/csharp/ql/test/library-tests/controlflow/guards/GuardedControlFlowNode.expected
@@ -38,6 +38,10 @@
 | Assert.cs:80:37:80:37 | [b (line 77): true] access to parameter b | Assert.cs:79:20:79:32 | ... ? ... : ... | Assert.cs:79:20:79:20 | access to parameter b | null |
 | Assert.cs:81:27:81:27 | access to local variable s | Assert.cs:80:24:80:24 | access to local variable s | Assert.cs:80:24:80:24 | access to local variable s | null |
 | Assert.cs:81:27:81:27 | access to local variable s | Assert.cs:80:24:80:32 | ... != ... | Assert.cs:80:24:80:24 | access to local variable s | false |
+| Assert.cs:93:33:93:34 | [assertion failure, b1 (line 91): true] access to parameter b2 | Assert.cs:93:29:93:30 | access to parameter b2 | Assert.cs:93:29:93:30 | access to parameter b2 | true |
+| Assert.cs:93:33:93:34 | [assertion success, b1 (line 91): true] access to parameter b2 | Assert.cs:93:29:93:30 | access to parameter b2 | Assert.cs:93:29:93:30 | access to parameter b2 | false |
+| Assert.cs:94:16:94:17 | [b1 (line 91): true] access to parameter b1 | Assert.cs:93:25:93:26 | access to parameter b1 | Assert.cs:93:25:93:26 | access to parameter b1 | true |
+| Assert.cs:94:23:94:24 | access to parameter b2 | Assert.cs:93:29:93:30 | access to parameter b2 | Assert.cs:93:29:93:30 | access to parameter b2 | false |
 | Collections.cs:52:17:52:20 | access to parameter args | Collections.cs:50:13:50:16 | access to parameter args | Collections.cs:50:13:50:16 | access to parameter args | non-empty |
 | Collections.cs:52:17:52:20 | access to parameter args | Collections.cs:50:13:50:27 | ... == ... | Collections.cs:50:13:50:16 | access to parameter args | false |
 | Collections.cs:53:9:53:12 | access to parameter args | Collections.cs:50:13:50:27 | ... == ... | Collections.cs:50:13:50:16 | access to parameter args | false |
--- a/csharp/ql/test/library-tests/controlflow/guards/GuardedExpr.expected
+++ b/csharp/ql/test/library-tests/controlflow/guards/GuardedExpr.expected
@@ -26,6 +26,8 @@
 | Assert.cs:80:37:80:37 | access to parameter b | Assert.cs:79:20:79:32 | ... ? ... : ... | Assert.cs:79:20:79:20 | access to parameter b | null |
 | Assert.cs:81:27:81:27 | access to local variable s | Assert.cs:80:24:80:24 | access to local variable s | Assert.cs:80:24:80:24 | access to local variable s | null |
 | Assert.cs:81:27:81:27 | access to local variable s | Assert.cs:80:24:80:32 | ... != ... | Assert.cs:80:24:80:24 | access to local variable s | false |
+| Assert.cs:94:16:94:17 | access to parameter b1 | Assert.cs:93:25:93:26 | access to parameter b1 | Assert.cs:93:25:93:26 | access to parameter b1 | true |
+| Assert.cs:94:23:94:24 | access to parameter b2 | Assert.cs:93:29:93:30 | access to parameter b2 | Assert.cs:93:29:93:30 | access to parameter b2 | false |
 | Collections.cs:52:17:52:20 | access to parameter args | Collections.cs:50:13:50:16 | access to parameter args | Collections.cs:50:13:50:16 | access to parameter args | non-empty |
 | Collections.cs:52:17:52:20 | access to parameter args | Collections.cs:50:13:50:27 | ... == ... | Collections.cs:50:13:50:16 | access to parameter args | false |
 | Collections.cs:53:9:53:12 | access to parameter args | Collections.cs:50:13:50:27 | ... == ... | Collections.cs:50:13:50:16 | access to parameter args | false |
--- a/csharp/ql/test/library-tests/controlflow/guards/Implications.expected
+++ b/csharp/ql/test/library-tests/controlflow/guards/Implications.expected
@@ -156,6 +156,10 @@
 | Assert.cs:80:24:80:37 | ... \|\| ... | false | Assert.cs:80:37:80:37 | access to parameter b | false |
 | Assert.cs:81:27:81:27 | access to local variable s | non-null | Assert.cs:79:20:79:32 | ... ? ... : ... | non-null |
 | Assert.cs:81:27:81:27 | access to local variable s | null | Assert.cs:79:20:79:32 | ... ? ... : ... | null |
+| Assert.cs:94:16:94:24 | ... && ... | true | Assert.cs:94:16:94:17 | access to parameter b1 | true |
+| Assert.cs:94:16:94:24 | ... && ... | true | Assert.cs:94:22:94:24 | !... | true |
+| Assert.cs:94:22:94:24 | !... | false | Assert.cs:94:23:94:24 | access to parameter b2 | true |
+| Assert.cs:94:22:94:24 | !... | true | Assert.cs:94:23:94:24 | access to parameter b2 | false |
 | Collections.cs:12:17:12:32 | ... == ... | false | Collections.cs:12:17:12:20 | access to parameter args | non-empty |
 | Collections.cs:12:17:12:32 | ... == ... | true | Collections.cs:12:17:12:20 | access to parameter args | empty |
 | Collections.cs:13:13:13:28 | ... == ... | true | Collections.cs:13:13:13:16 | access to parameter args | non-empty |
--- a/csharp/ql/test/library-tests/frameworks/test/Assertions.ql
+++ b/csharp/ql/test/library-tests/frameworks/test/Assertions.ql
@@ -1,18 +1,18 @@
 import csharp
 import semmle.code.csharp.commons.Assertions

-query predicate assertTrue(AssertTrueMethod m, Parameter p) {
-  m.fromSource() and m.fromSource() and p = m.getAnAssertedParameter()
+query predicate assertTrue(BooleanAssertMethod m, Parameter p) {
+  m.fromSource() and m.fromSource() and p = m.getParameter(m.getAnAssertionIndex(true))
 }

-query predicate assertFalse(AssertFalseMethod m, Parameter p) {
-  m.fromSource() and m.fromSource() and p = m.getAnAssertedParameter()
+query predicate assertFalse(BooleanAssertMethod m, Parameter p) {
+  m.fromSource() and m.fromSource() and p = m.getParameter(m.getAnAssertionIndex(false))
 }

-query predicate assertNull(AssertNullMethod m, Parameter p) {
-  m.fromSource() and m.fromSource() and p = m.getAnAssertedParameter()
+query predicate assertNull(NullnessAssertMethod m, Parameter p) {
+  m.fromSource() and m.fromSource() and p = m.getParameter(m.getAnAssertionIndex(true))
 }

-query predicate assertNonNull(AssertNonNullMethod m, Parameter p) {
-  m.fromSource() and m.fromSource() and p = m.getAnAssertedParameter()
+query predicate assertNonNull(NullnessAssertMethod m, Parameter p) {
+  m.fromSource() and m.fromSource() and p = m.getParameter(m.getAnAssertionIndex(false))
 }
--- a/python/ql/src/experimental/Security-new-dataflow/CWE-022/ChainedConfigs12.qll
+++ b/python/ql/src/experimental/Security-new-dataflow/CWE-022/ChainedConfigs12.qll
@@ -0,0 +1,75 @@
+/**
+ * This defines a `PathGraph` where sinks from `TaintTracking::Configuration`s are identified with
+ * sources from `TaintTracking2::Configuration`s if they represent the same `ControlFlowNode`.
+ *
+ * Paths are then connected appropriately.
+ */
+
+import python
+import experimental.dataflow.DataFlow
+import experimental.dataflow.DataFlow2
+import experimental.dataflow.TaintTracking
+import experimental.dataflow.TaintTracking2
+
+/**
+ * A `DataFlow::Node` that appears as a sink in Config1 and a source in Config2.
+ */
+private predicate crossoverNode(DataFlow::Node n) {
+  any(TaintTracking::Configuration t1).isSink(n) and
+  any(TaintTracking2::Configuration t2).isSource(n)
+}
+
+/**
+ * A new type which represents the union of the two sets of nodes.
+ */
+private newtype TCustomPathNode =
+  Config1Node(DataFlow::PathNode node1) { not crossoverNode(node1.getNode()) } or
+  Config2Node(DataFlow2::PathNode node2) { not crossoverNode(node2.getNode()) } or
+  CrossoverNode(DataFlow::Node node) { crossoverNode(node) }
+
+/**
+ * A class representing the set of all the path nodes in either config.
+ */
+class CustomPathNode extends TCustomPathNode {
+  /** Gets the PathNode if it is in Config1. */
+  DataFlow::PathNode asNode1() {
+    this = Config1Node(result) or this = CrossoverNode(result.getNode())
+  }
+
+  /** Gets the PathNode if it is in Config2. */
+  DataFlow2::PathNode asNode2() {
+    this = Config2Node(result) or this = CrossoverNode(result.getNode())
+  }
+
+  predicate hasLocationInfo(
+    string filepath, int startline, int startcolumn, int endline, int endcolumn
+  ) {
+    asNode1().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
+    or
+    asNode2().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
+  }
+
+  string toString() {
+    result = asNode1().toString()
+    or
+    result = asNode2().toString()
+  }
+}
+
+/** Holds if `(a,b)` is an edge in the graph of data flow path explanations. */
+query predicate edges(CustomPathNode a, CustomPathNode b) {
+  // Edge is in Config1 graph
+  DataFlow::PathGraph::edges(a.asNode1(), b.asNode1())
+  or
+  // Edge is in Config2 graph
+  DataFlow2::PathGraph::edges(a.asNode2(), b.asNode2())
+}
+
+/** Holds if `n` is a node in the graph of data flow path explanations. */
+query predicate nodes(CustomPathNode n, string key, string val) {
+  // Node is in Config1 graph
+  DataFlow::PathGraph::nodes(n.asNode1(), key, val)
+  or
+  // Node is in Config2 graph
+  DataFlow2::PathGraph::nodes(n.asNode2(), key, val)
+}
--- a/python/ql/src/experimental/Security-new-dataflow/CWE-022/PathInjection.ql
+++ b/python/ql/src/experimental/Security-new-dataflow/CWE-022/PathInjection.ql
@@ -0,0 +1,116 @@
+/**
+ * @name Uncontrolled data used in path expression
+ * @description Accessing paths influenced by users can allow an attacker to access unexpected resources.
+ * @kind path-problem
+ * @problem.severity error
+ * @sub-severity high
+ * @precision high
+ * @id py/path-injection
+ * @tags correctness
+ *       security
+ *       external/owasp/owasp-a1
+ *       external/cwe/cwe-022
+ *       external/cwe/cwe-023
+ *       external/cwe/cwe-036
+ *       external/cwe/cwe-073
+ *       external/cwe/cwe-099
+ *
+ * The query detects cases where a user-controlled path is used in an unsafe manner,
+ * meaning it is not both normalized and _afterwards_ checked.
+ *
+ * It does so by dividing the problematic situation into two cases:
+ *  1. The file path is never normalized.
+ *     This is easily detected by using normalization as a sanitizer.
+ *
+ *  2. The file path is normalized at least once, but never checked afterwards.
+ *     This is detected by finding the earliest normalization and then ensuring that
+ *     no checks happen later. Since we start from the earliest normalization,
+ *     we know that the absence of checks means that no normalization has a
+ *     check after it. (No checks after a second normalization would be ok if
+ *     there was a check between the first and the second.)
+ *
+ * Note that one could make the dual split on whether the file path is ever checked. This does
+ * not work as nicely, however, since checking is modelled as a `BarrierGuard` rather than
+ * as a `Sanitizer`. That means that only some dataflow paths out of a check will be removed,
+ * and so identifying the last check is not possible simply by finding a dataflow path from it
+ * to a sink.
+ */
+
+import python
+import experimental.dataflow.DataFlow
+import experimental.dataflow.DataFlow2
+import experimental.dataflow.TaintTracking
+import experimental.dataflow.TaintTracking2
+import experimental.semmle.python.Concepts
+import experimental.dataflow.RemoteFlowSources
+import ChainedConfigs12
+
+// ---------------------------------------------------------------------------
+// Case 1. The path is never normalized.
+// ---------------------------------------------------------------------------
+/** Configuration to find paths from sources to sinks that contain no normalization. */
+class PathNotNormalizedConfiguration extends TaintTracking::Configuration {
+  PathNotNormalizedConfiguration() { this = "PathNotNormalizedConfiguration" }
+
+  override predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
+
+  override predicate isSink(DataFlow::Node sink) {
+    sink = any(FileSystemAccess e).getAPathArgument()
+  }
+
+  override predicate isSanitizer(DataFlow::Node node) { node instanceof Path::PathNormalization }
+}
+
+predicate pathNotNormalized(CustomPathNode source, CustomPathNode sink) {
+  any(PathNotNormalizedConfiguration config).hasFlowPath(source.asNode1(), sink.asNode1())
+}
+
+// ---------------------------------------------------------------------------
+// Case 2. The path is normalized at least once, but never checked afterwards.
+// ---------------------------------------------------------------------------
+/** Configuration to find paths from sources to normalizations that contain no prior normalizations. */
+class FirstNormalizationConfiguration extends TaintTracking::Configuration {
+  FirstNormalizationConfiguration() { this = "FirstNormalizationConfiguration" }
+
+  override predicate isSource(DataFlow::Node source) { source instanceof RemoteFlowSource }
+
+  override predicate isSink(DataFlow::Node sink) { sink instanceof Path::PathNormalization }
+
+  override predicate isSanitizerOut(DataFlow::Node node) { node instanceof Path::PathNormalization }
+}
+
+/** Configuration to find paths from normalizations to sinks that do not go through a check. */
+class NormalizedPathNotCheckedConfiguration extends TaintTracking2::Configuration {
+  NormalizedPathNotCheckedConfiguration() { this = "NormalizedPathNotCheckedConfiguration" }
+
+  override predicate isSource(DataFlow::Node source) { source instanceof Path::PathNormalization }
+
+  override predicate isSink(DataFlow::Node sink) {
+    sink = any(FileSystemAccess e).getAPathArgument()
+  }
+
+  override predicate isSanitizerGuard(DataFlow::BarrierGuard guard) {
+    guard instanceof Path::SafeAccessCheck
+  }
+}
+
+predicate pathNotCheckedAfterNormalization(CustomPathNode source, CustomPathNode sink) {
+  exists(
+    FirstNormalizationConfiguration config, DataFlow::PathNode mid1, DataFlow2::PathNode mid2,
+    NormalizedPathNotCheckedConfiguration config2
+  |
+    config.hasFlowPath(source.asNode1(), mid1) and
+    config2.hasFlowPath(mid2, sink.asNode2()) and
+    mid1.getNode().asCfgNode() = mid2.getNode().asCfgNode()
+  )
+}
+
+// ---------------------------------------------------------------------------
+// Query: Either case 1 or case 2.
+// ---------------------------------------------------------------------------
+from CustomPathNode source, CustomPathNode sink
+where
+  pathNotNormalized(source, sink)
+  or
+  pathNotCheckedAfterNormalization(source, sink)
+select sink, source, sink, "This path depends on $@.", source, "a user-provided value"
--- a/python/ql/src/experimental/dataflow/DataFlow3.qll
+++ b/python/ql/src/experimental/dataflow/DataFlow3.qll
@@ -0,0 +1,26 @@
+/**
+ * Provides a library for local (intra-procedural) and global (inter-procedural)
+ * data flow analysis: deciding whether data can flow from a _source_ to a
+ * _sink_.
+ *
+ * Unless configured otherwise, _flow_ means that the exact value of
+ * the source may reach the sink. We do not track flow across pointer
+ * dereferences or array indexing. To track these types of flow, where the
+ * exact value may not be preserved, import
+ * `experimental.dataflow.TaintTracking`.
+ *
+ * To use global (interprocedural) data flow, extend the class
+ * `DataFlow::Configuration` as documented on that class. To use local
+ * (intraprocedural) data flow, call `DataFlow::localFlow` or
+ * `DataFlow::localFlowStep` with arguments of type `DataFlow::Node`.
+ */
+
+private import python
+
+/**
+ * Provides classes for performing local (intra-procedural) and
+ * global (inter-procedural) data flow analyses.
+ */
+module DataFlow3 {
+  import experimental.dataflow.internal.DataFlowImpl3
+}
--- a/python/ql/src/experimental/dataflow/DataFlow4.qll
+++ b/python/ql/src/experimental/dataflow/DataFlow4.qll
@@ -0,0 +1,26 @@
+/**
+ * Provides a library for local (intra-procedural) and global (inter-procedural)
+ * data flow analysis: deciding whether data can flow from a _source_ to a
+ * _sink_.
+ *
+ * Unless configured otherwise, _flow_ means that the exact value of
+ * the source may reach the sink. We do not track flow across pointer
+ * dereferences or array indexing. To track these types of flow, where the
+ * exact value may not be preserved, import
+ * `experimental.dataflow.TaintTracking`.
+ *
+ * To use global (interprocedural) data flow, extend the class
+ * `DataFlow::Configuration` as documented on that class. To use local
+ * (intraprocedural) data flow, call `DataFlow::localFlow` or
+ * `DataFlow::localFlowStep` with arguments of type `DataFlow::Node`.
+ */
+
+private import python
+
+/**
+ * Provides classes for performing local (intra-procedural) and
+ * global (inter-procedural) data flow analyses.
+ */
+module DataFlow4 {
+  import experimental.dataflow.internal.DataFlowImpl4
+}
--- a/python/ql/src/experimental/dataflow/TaintTracking2.qll
+++ b/python/ql/src/experimental/dataflow/TaintTracking2.qll
@@ -0,0 +1,19 @@
+/**
+ * Provides classes for performing local (intra-procedural) and
+ * global (inter-procedural) taint-tracking analyses.
+ *
+ * To use global (interprocedural) taint tracking, extend the class
+ * `TaintTracking::Configuration` as documented on that class. To use local
+ * (intraprocedural) taint tracking, call `TaintTracking::localTaint` or
+ * `TaintTracking::localTaintStep` with arguments of type `DataFlow::Node`.
+ */
+
+private import python
+
+/**
+ * Provides classes for performing local (intra-procedural) and
+ * global (inter-procedural) taint-tracking analyses.
+ */
+module TaintTracking2 {
+  import experimental.dataflow.internal.tainttracking2.TaintTrackingImpl
+}
--- a/python/ql/src/experimental/dataflow/TaintTracking3.qll
+++ b/python/ql/src/experimental/dataflow/TaintTracking3.qll
@@ -0,0 +1,19 @@
+/**
+ * Provides classes for performing local (intra-procedural) and
+ * global (inter-procedural) taint-tracking analyses.
+ *
+ * To use global (interprocedural) taint tracking, extend the class
+ * `TaintTracking::Configuration` as documented on that class. To use local
+ * (intraprocedural) taint tracking, call `TaintTracking::localTaint` or
+ * `TaintTracking::localTaintStep` with arguments of type `DataFlow::Node`.
+ */
+
+private import python
+
+/**
+ * Provides classes for performing local (intra-procedural) and
+ * global (inter-procedural) taint-tracking analyses.
+ */
+module TaintTracking3 {
+  import experimental.dataflow.internal.tainttracking3.TaintTrackingImpl
+}
--- a/python/ql/src/experimental/dataflow/TaintTracking4.qll
+++ b/python/ql/src/experimental/dataflow/TaintTracking4.qll
@@ -0,0 +1,19 @@
+/**
+ * Provides classes for performing local (intra-procedural) and
+ * global (inter-procedural) taint-tracking analyses.
+ *
+ * To use global (interprocedural) taint tracking, extend the class
+ * `TaintTracking::Configuration` as documented on that class. To use local
+ * (intraprocedural) taint tracking, call `TaintTracking::localTaint` or
+ * `TaintTracking::localTaintStep` with arguments of type `DataFlow::Node`.
+ */
+
+private import python
+
+/**
+ * Provides classes for performing local (intra-procedural) and
+ * global (inter-procedural) taint-tracking analyses.
+ */
+module TaintTracking4 {
+  import experimental.dataflow.internal.tainttracking4.TaintTrackingImpl
+}
--- a/python/ql/src/experimental/dataflow/internal/DataFlowImpl3.qll
+++ b/python/ql/src/experimental/dataflow/internal/DataFlowImpl3.qll
--- a/python/ql/src/experimental/dataflow/internal/DataFlowImpl4.qll
+++ b/python/ql/src/experimental/dataflow/internal/DataFlowImpl4.qll
--- a/python/ql/src/experimental/dataflow/internal/tainttracking2/TaintTrackingImpl.qll
+++ b/python/ql/src/experimental/dataflow/internal/tainttracking2/TaintTrackingImpl.qll
@@ -0,0 +1,115 @@
+/**
+ * Provides an implementation of global (interprocedural) taint tracking.
+ * This file re-exports the local (intraprocedural) taint-tracking analysis
+ * from `TaintTrackingParameter::Public` and adds a global analysis, mainly
+ * exposed through the `Configuration` class. For some languages, this file
+ * exists in several identical copies, allowing queries to use multiple
+ * `Configuration` classes that depend on each other without introducing
+ * mutual recursion among those configurations.
+ */
+
+import TaintTrackingParameter::Public
+private import TaintTrackingParameter::Private
+
+/**
+ * A configuration of interprocedural taint tracking analysis. This defines
+ * sources, sinks, and any other configurable aspect of the analysis. Each
+ * use of the taint tracking library must define its own unique extension of
+ * this abstract class.
+ *
+ * A taint-tracking configuration is a special data flow configuration
+ * (`DataFlow::Configuration`) that allows for flow through nodes that do not
+ * necessarily preserve values but are still relevant from a taint tracking
+ * perspective. (For example, string concatenation, where one of the operands
+ * is tainted.)
+ *
+ * To create a configuration, extend this class with a subclass whose
+ * characteristic predicate is a unique singleton string. For example, write
+ *
+ * ```ql
+ * class MyAnalysisConfiguration extends TaintTracking::Configuration {
+ *   MyAnalysisConfiguration() { this = "MyAnalysisConfiguration" }
+ *   // Override `isSource` and `isSink`.
+ *   // Optionally override `isSanitizer`.
+ *   // Optionally override `isSanitizerIn`.
+ *   // Optionally override `isSanitizerOut`.
+ *   // Optionally override `isSanitizerGuard`.
+ *   // Optionally override `isAdditionalTaintStep`.
+ * }
+ * ```
+ *
+ * Then, to query whether there is flow between some `source` and `sink`,
+ * write
+ *
+ * ```ql
+ * exists(MyAnalysisConfiguration cfg | cfg.hasFlow(source, sink))
+ * ```
+ *
+ * Multiple configurations can coexist, but it is unsupported to depend on
+ * another `TaintTracking::Configuration` or a `DataFlow::Configuration` in the
+ * overridden predicates that define sources, sinks, or additional steps.
+ * Instead, the dependency should go to a `TaintTracking2::Configuration` or a
+ * `DataFlow2::Configuration`, `DataFlow3::Configuration`, etc.
+ */
+abstract class Configuration extends DataFlow::Configuration {
+  bindingset[this]
+  Configuration() { any() }
+
+  /**
+   * Holds if `source` is a relevant taint source.
+   *
+   * The smaller this predicate is, the faster `hasFlow()` will converge.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  abstract override predicate isSource(DataFlow::Node source);
+
+  /**
+   * Holds if `sink` is a relevant taint sink.
+   *
+   * The smaller this predicate is, the faster `hasFlow()` will converge.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  abstract override predicate isSink(DataFlow::Node sink);
+
+  /** Holds if the node `node` is a taint sanitizer. */
+  predicate isSanitizer(DataFlow::Node node) { none() }
+
+  final override predicate isBarrier(DataFlow::Node node) {
+    isSanitizer(node) or
+    defaultTaintSanitizer(node)
+  }
+
+  /** Holds if taint propagation into `node` is prohibited. */
+  predicate isSanitizerIn(DataFlow::Node node) { none() }
+
+  final override predicate isBarrierIn(DataFlow::Node node) { isSanitizerIn(node) }
+
+  /** Holds if taint propagation out of `node` is prohibited. */
+  predicate isSanitizerOut(DataFlow::Node node) { none() }
+
+  final override predicate isBarrierOut(DataFlow::Node node) { isSanitizerOut(node) }
+
+  /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
+  predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
+
+  final override predicate isBarrierGuard(DataFlow::BarrierGuard guard) { isSanitizerGuard(guard) }
+
+  /**
+   * Holds if the additional taint propagation step from `node1` to `node2`
+   * must be taken into account in the analysis.
+   */
+  predicate isAdditionalTaintStep(DataFlow::Node node1, DataFlow::Node node2) { none() }
+
+  final override predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
+    isAdditionalTaintStep(node1, node2) or
+    defaultAdditionalTaintStep(node1, node2)
+  }
+
+  /**
+   * Holds if taint may flow from `source` to `sink` for this configuration.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  override predicate hasFlow(DataFlow::Node source, DataFlow::Node sink) {
+    super.hasFlow(source, sink)
+  }
+}
--- a/python/ql/src/experimental/dataflow/internal/tainttracking2/TaintTrackingParameter.qll
+++ b/python/ql/src/experimental/dataflow/internal/tainttracking2/TaintTrackingParameter.qll
@@ -0,0 +1,6 @@
+import experimental.dataflow.internal.TaintTrackingPublic as Public
+
+module Private {
+  import experimental.dataflow.DataFlow2::DataFlow2 as DataFlow
+  import experimental.dataflow.internal.TaintTrackingPrivate
+}
--- a/python/ql/src/experimental/dataflow/internal/tainttracking3/TaintTrackingImpl.qll
+++ b/python/ql/src/experimental/dataflow/internal/tainttracking3/TaintTrackingImpl.qll
@@ -0,0 +1,115 @@
+/**
+ * Provides an implementation of global (interprocedural) taint tracking.
+ * This file re-exports the local (intraprocedural) taint-tracking analysis
+ * from `TaintTrackingParameter::Public` and adds a global analysis, mainly
+ * exposed through the `Configuration` class. For some languages, this file
+ * exists in several identical copies, allowing queries to use multiple
+ * `Configuration` classes that depend on each other without introducing
+ * mutual recursion among those configurations.
+ */
+
+import TaintTrackingParameter::Public
+private import TaintTrackingParameter::Private
+
+/**
+ * A configuration of interprocedural taint tracking analysis. This defines
+ * sources, sinks, and any other configurable aspect of the analysis. Each
+ * use of the taint tracking library must define its own unique extension of
+ * this abstract class.
+ *
+ * A taint-tracking configuration is a special data flow configuration
+ * (`DataFlow::Configuration`) that allows for flow through nodes that do not
+ * necessarily preserve values but are still relevant from a taint tracking
+ * perspective. (For example, string concatenation, where one of the operands
+ * is tainted.)
+ *
+ * To create a configuration, extend this class with a subclass whose
+ * characteristic predicate is a unique singleton string. For example, write
+ *
+ * ```ql
+ * class MyAnalysisConfiguration extends TaintTracking::Configuration {
+ *   MyAnalysisConfiguration() { this = "MyAnalysisConfiguration" }
+ *   // Override `isSource` and `isSink`.
+ *   // Optionally override `isSanitizer`.
+ *   // Optionally override `isSanitizerIn`.
+ *   // Optionally override `isSanitizerOut`.
+ *   // Optionally override `isSanitizerGuard`.
+ *   // Optionally override `isAdditionalTaintStep`.
+ * }
+ * ```
+ *
+ * Then, to query whether there is flow between some `source` and `sink`,
+ * write
+ *
+ * ```ql
+ * exists(MyAnalysisConfiguration cfg | cfg.hasFlow(source, sink))
+ * ```
+ *
+ * Multiple configurations can coexist, but it is unsupported to depend on
+ * another `TaintTracking::Configuration` or a `DataFlow::Configuration` in the
+ * overridden predicates that define sources, sinks, or additional steps.
+ * Instead, the dependency should go to a `TaintTracking2::Configuration` or a
+ * `DataFlow2::Configuration`, `DataFlow3::Configuration`, etc.
+ */
+abstract class Configuration extends DataFlow::Configuration {
+  bindingset[this]
+  Configuration() { any() }
+
+  /**
+   * Holds if `source` is a relevant taint source.
+   *
+   * The smaller this predicate is, the faster `hasFlow()` will converge.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  abstract override predicate isSource(DataFlow::Node source);
+
+  /**
+   * Holds if `sink` is a relevant taint sink.
+   *
+   * The smaller this predicate is, the faster `hasFlow()` will converge.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  abstract override predicate isSink(DataFlow::Node sink);
+
+  /** Holds if the node `node` is a taint sanitizer. */
+  predicate isSanitizer(DataFlow::Node node) { none() }
+
+  final override predicate isBarrier(DataFlow::Node node) {
+    isSanitizer(node) or
+    defaultTaintSanitizer(node)
+  }
+
+  /** Holds if taint propagation into `node` is prohibited. */
+  predicate isSanitizerIn(DataFlow::Node node) { none() }
+
+  final override predicate isBarrierIn(DataFlow::Node node) { isSanitizerIn(node) }
+
+  /** Holds if taint propagation out of `node` is prohibited. */
+  predicate isSanitizerOut(DataFlow::Node node) { none() }
+
+  final override predicate isBarrierOut(DataFlow::Node node) { isSanitizerOut(node) }
+
+  /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
+  predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
+
+  final override predicate isBarrierGuard(DataFlow::BarrierGuard guard) { isSanitizerGuard(guard) }
+
+  /**
+   * Holds if the additional taint propagation step from `node1` to `node2`
+   * must be taken into account in the analysis.
+   */
+  predicate isAdditionalTaintStep(DataFlow::Node node1, DataFlow::Node node2) { none() }
+
+  final override predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
+    isAdditionalTaintStep(node1, node2) or
+    defaultAdditionalTaintStep(node1, node2)
+  }
+
+  /**
+   * Holds if taint may flow from `source` to `sink` for this configuration.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  override predicate hasFlow(DataFlow::Node source, DataFlow::Node sink) {
+    super.hasFlow(source, sink)
+  }
+}
--- a/python/ql/src/experimental/dataflow/internal/tainttracking3/TaintTrackingParameter.qll
+++ b/python/ql/src/experimental/dataflow/internal/tainttracking3/TaintTrackingParameter.qll
@@ -0,0 +1,6 @@
+import experimental.dataflow.internal.TaintTrackingPublic as Public
+
+module Private {
+  import experimental.dataflow.DataFlow3::DataFlow3 as DataFlow
+  import experimental.dataflow.internal.TaintTrackingPrivate
+}
--- a/python/ql/src/experimental/dataflow/internal/tainttracking4/TaintTrackingImpl.qll
+++ b/python/ql/src/experimental/dataflow/internal/tainttracking4/TaintTrackingImpl.qll
@@ -0,0 +1,115 @@
+/**
+ * Provides an implementation of global (interprocedural) taint tracking.
+ * This file re-exports the local (intraprocedural) taint-tracking analysis
+ * from `TaintTrackingParameter::Public` and adds a global analysis, mainly
+ * exposed through the `Configuration` class. For some languages, this file
+ * exists in several identical copies, allowing queries to use multiple
+ * `Configuration` classes that depend on each other without introducing
+ * mutual recursion among those configurations.
+ */
+
+import TaintTrackingParameter::Public
+private import TaintTrackingParameter::Private
+
+/**
+ * A configuration of interprocedural taint tracking analysis. This defines
+ * sources, sinks, and any other configurable aspect of the analysis. Each
+ * use of the taint tracking library must define its own unique extension of
+ * this abstract class.
+ *
+ * A taint-tracking configuration is a special data flow configuration
+ * (`DataFlow::Configuration`) that allows for flow through nodes that do not
+ * necessarily preserve values but are still relevant from a taint tracking
+ * perspective. (For example, string concatenation, where one of the operands
+ * is tainted.)
+ *
+ * To create a configuration, extend this class with a subclass whose
+ * characteristic predicate is a unique singleton string. For example, write
+ *
+ * ```ql
+ * class MyAnalysisConfiguration extends TaintTracking::Configuration {
+ *   MyAnalysisConfiguration() { this = "MyAnalysisConfiguration" }
+ *   // Override `isSource` and `isSink`.
+ *   // Optionally override `isSanitizer`.
+ *   // Optionally override `isSanitizerIn`.
+ *   // Optionally override `isSanitizerOut`.
+ *   // Optionally override `isSanitizerGuard`.
+ *   // Optionally override `isAdditionalTaintStep`.
+ * }
+ * ```
+ *
+ * Then, to query whether there is flow between some `source` and `sink`,
+ * write
+ *
+ * ```ql
+ * exists(MyAnalysisConfiguration cfg | cfg.hasFlow(source, sink))
+ * ```
+ *
+ * Multiple configurations can coexist, but it is unsupported to depend on
+ * another `TaintTracking::Configuration` or a `DataFlow::Configuration` in the
+ * overridden predicates that define sources, sinks, or additional steps.
+ * Instead, the dependency should go to a `TaintTracking2::Configuration` or a
+ * `DataFlow2::Configuration`, `DataFlow3::Configuration`, etc.
+ */
+abstract class Configuration extends DataFlow::Configuration {
+  bindingset[this]
+  Configuration() { any() }
+
+  /**
+   * Holds if `source` is a relevant taint source.
+   *
+   * The smaller this predicate is, the faster `hasFlow()` will converge.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  abstract override predicate isSource(DataFlow::Node source);
+
+  /**
+   * Holds if `sink` is a relevant taint sink.
+   *
+   * The smaller this predicate is, the faster `hasFlow()` will converge.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  abstract override predicate isSink(DataFlow::Node sink);
+
+  /** Holds if the node `node` is a taint sanitizer. */
+  predicate isSanitizer(DataFlow::Node node) { none() }
+
+  final override predicate isBarrier(DataFlow::Node node) {
+    isSanitizer(node) or
+    defaultTaintSanitizer(node)
+  }
+
+  /** Holds if taint propagation into `node` is prohibited. */
+  predicate isSanitizerIn(DataFlow::Node node) { none() }
+
+  final override predicate isBarrierIn(DataFlow::Node node) { isSanitizerIn(node) }
+
+  /** Holds if taint propagation out of `node` is prohibited. */
+  predicate isSanitizerOut(DataFlow::Node node) { none() }
+
+  final override predicate isBarrierOut(DataFlow::Node node) { isSanitizerOut(node) }
+
+  /** Holds if taint propagation through nodes guarded by `guard` is prohibited. */
+  predicate isSanitizerGuard(DataFlow::BarrierGuard guard) { none() }
+
+  final override predicate isBarrierGuard(DataFlow::BarrierGuard guard) { isSanitizerGuard(guard) }
+
+  /**
+   * Holds if the additional taint propagation step from `node1` to `node2`
+   * must be taken into account in the analysis.
+   */
+  predicate isAdditionalTaintStep(DataFlow::Node node1, DataFlow::Node node2) { none() }
+
+  final override predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
+    isAdditionalTaintStep(node1, node2) or
+    defaultAdditionalTaintStep(node1, node2)
+  }
+
+  /**
+   * Holds if taint may flow from `source` to `sink` for this configuration.
+   */
+  // overridden to provide taint-tracking specific qldoc
+  override predicate hasFlow(DataFlow::Node source, DataFlow::Node sink) {
+    super.hasFlow(source, sink)
+  }
+}
--- a/python/ql/src/experimental/dataflow/internal/tainttracking4/TaintTrackingParameter.qll
+++ b/python/ql/src/experimental/dataflow/internal/tainttracking4/TaintTrackingParameter.qll
@@ -0,0 +1,6 @@
+import experimental.dataflow.internal.TaintTrackingPublic as Public
+
+module Private {
+  import experimental.dataflow.DataFlow4::DataFlow4 as DataFlow
+  import experimental.dataflow.internal.TaintTrackingPrivate
+}
--- a/python/ql/src/experimental/semmle/python/Concepts.qll
+++ b/python/ql/src/experimental/semmle/python/Concepts.qll
@@ -40,6 +40,74 @@ module SystemCommandExecution {
  }
 }

+/**
+ * A data flow node that performs a file system access, including reading and writing data,
+ * creating and deleting files and folders, checking and updating permissions, and so on.
+ *
+ * Extend this class to refine existing API models. If you want to model new APIs,
+ * extend `FileSystemAccess::Range` instead.
+ */
+class FileSystemAccess extends DataFlow::Node {
+  FileSystemAccess::Range range;
+
+  FileSystemAccess() { this = range }
+
+  /** Gets an argument to this file system access that is interpreted as a path. */
+  DataFlow::Node getAPathArgument() { result = range.getAPathArgument() }
+}
+
+/** Provides a class for modeling new file system access APIs. */
+module FileSystemAccess {
+  /**
+   * A data-flow node that performs a file system access, including reading and writing data,
+   * creating and deleting files and folders, checking and updating permissions, and so on.
+   *
+   * Extend this class to model new APIs. If you want to refine existing API models,
+   * extend `FileSystemAccess` instead.
+   */
+  abstract class Range extends DataFlow::Node {
+    /** Gets an argument to this file system access that is interpreted as a path. */
+    abstract DataFlow::Node getAPathArgument();
+  }
+}
+
+/** Provides classes for modeling path-related APIs. */
+module Path {
+  /**
+   * A data-flow node that performs path normalization. This is often needed in order
+   * to safely access paths.
+   */
+  class PathNormalization extends DataFlow::Node {
+    PathNormalization::Range range;
+
+    PathNormalization() { this = range }
+  }
+
+  /** Provides a class for modeling new path normalization APIs. */
+  module PathNormalization {
+    /**
+     * A data-flow node that performs path normalization. This is often needed in order
+     * to safely access paths.
+     */
+    abstract class Range extends DataFlow::Node { }
+  }
+
+  /** A data-flow node that checks that a path is safe to access. */
+  class SafeAccessCheck extends DataFlow::BarrierGuard {
+    SafeAccessCheck::Range range;
+
+    SafeAccessCheck() { this = range }
+
+    override predicate checks(ControlFlowNode node, boolean branch) { range.checks(node, branch) }
+  }
+
+  /** Provides a class for modeling new path safety checks. */
+  module SafeAccessCheck {
+    /** A data-flow node that checks that a path is safe to access. */
+    abstract class Range extends DataFlow::BarrierGuard { }
+  }
+}
+
 /**
 * A data-flow node that decodes data from a binary or textual format. This
 * is intended to include deserialization, unmarshalling, decoding, unpickling,
--- a/python/ql/src/experimental/semmle/python/frameworks/Stdlib.qll
+++ b/python/ql/src/experimental/semmle/python/frameworks/Stdlib.qll
@@ -82,19 +82,76 @@ private module Stdlib {

    /** Provides models for the `os.path` module */
    module path {
-      /** Gets a reference to the `os.path.join` function. */
-      private DataFlow::Node join(DataFlow::TypeTracker t) {
-        t.start() and
-        result = DataFlow::importNode("os.path.join")
+      /**
+       * Gets a reference to the attribute `attr_name` of the `os.path` module.
+       * WARNING: Only holds for a few predefined attributes.
+       *
+       * For example, using `attr_name = "join"` will get all uses of `os.path.join`.
+       */
+      private DataFlow::Node path_attr(DataFlow::TypeTracker t, string attr_name) {
+        attr_name in ["join", "normpath"] and
+        (
+          t.start() and
+          result = DataFlow::importNode("os.path." + attr_name)
+          or
+          t.startInAttr(attr_name) and
+          result = os::path()
+        )
        or
-        t.startInAttr("join") and
-        result = os::path()
-        or
-        exists(DataFlow::TypeTracker t2 | result = join(t2).track(t2, t))
+        // Due to bad performance when using normal setup with `path_attr(t2, attr_name).track(t2, t)`
+        // we have inlined that code and forced a join
+        exists(DataFlow::TypeTracker t2 |
+          exists(DataFlow::StepSummary summary |
+            path_attr_first_join(t2, attr_name, result, summary) and
+            t = t2.append(summary)
+          )
+        )
+      }
+
+      pragma[nomagic]
+      private predicate path_attr_first_join(
+        DataFlow::TypeTracker t2, string attr_name, DataFlow::Node res,
+        DataFlow::StepSummary summary
+      ) {
+        DataFlow::StepSummary::step(path_attr(t2, attr_name), res, summary)
+      }
+
+      /**
+       * Gets a reference to the attribute `attr_name` of the `os.path` module.
+       * WARNING: Only holds for a few predefined attributes.
+       *
+       * For example, using `attr_name = "join"` will get all uses of `os.path.join`.
+       */
+      DataFlow::Node path_attr(string attr_name) {
+        result = path_attr(DataFlow::TypeTracker::end(), attr_name)
      }

      /** Gets a reference to the `os.path.join` function. */
-      DataFlow::Node join() { result = join(DataFlow::TypeTracker::end()) }
+      DataFlow::Node join() { result = path_attr("join") }
+    }
+  }
+
+  /**
+   * A call to `os.path.normpath`.
+   * See https://docs.python.org/3/library/os.path.html#os.path.normpath
+   */
+  private class OsPathNormpathCall extends Path::PathNormalization::Range, DataFlow::CfgNode {
+    override CallNode node;
+
+    OsPathNormpathCall() { node.getFunction() = os::path::path_attr("normpath").asCfgNode() }
+
+    DataFlow::Node getPathArg() {
+      result.asCfgNode() in [node.getArg(0), node.getArgByName("path")]
+    }
+  }
+
+  /** An additional taint step for calls to `os.path.normpath` */
+  private class OsPathNormpathCallAdditionalTaintStep extends TaintTracking::AdditionalTaintStep {
+    override predicate step(DataFlow::Node nodeFrom, DataFlow::Node nodeTo) {
+      exists(OsPathNormpathCall call |
+        nodeTo = call and
+        nodeFrom = call.getPathArg()
+      )
    }
  }

@@ -681,3 +738,30 @@ private class ExecStatement extends CodeExecution::Range {

  override DataFlow::Node getCode() { result = this }
 }
+
+/**
+ * A call to the builtin `open` function.
+ * See https://docs.python.org/3/library/functions.html#open
+ */
+private class OpenCall extends FileSystemAccess::Range, DataFlow::CfgNode {
+  override CallNode node;
+
+  OpenCall() { node.getFunction().(NameNode).getId() = "open" }
+
+  override DataFlow::Node getAPathArgument() {
+    result.asCfgNode() in [node.getArg(0), node.getArgByName("file")]
+  }
+}
+
+/**
+ * A call to the `startswith` method on a string.
+ * See https://docs.python.org/3.9/library/stdtypes.html#str.startswith
+ */
+private class StartswithCall extends Path::SafeAccessCheck::Range {
+  StartswithCall() { this.(CallNode).getFunction().(AttrNode).getName() = "startswith" }
+
+  override predicate checks(ControlFlowNode node, boolean branch) {
+    node = this.(CallNode).getFunction().(AttrNode).getObject() and
+    branch = true
+  }
+}
--- a/python/ql/test/experimental/library-tests/frameworks/stdlib/FileSystemAccess.py
+++ b/python/ql/test/experimental/library-tests/frameworks/stdlib/FileSystemAccess.py
@@ -0,0 +1,7 @@
+open("filepath")  # $getAPathArgument="filepath"
+open(file="filepath")  # $getAPathArgument="filepath"
+
+o = open
+
+o("filepath")  # f-:$getAPathArgument="filepath"
+o(file="filepath")  # f-:$getAPathArgument="filepath"
--- a/python/ql/test/experimental/library-tests/frameworks/stdlib/PathNormalization.py
+++ b/python/ql/test/experimental/library-tests/frameworks/stdlib/PathNormalization.py
@@ -0,0 +1,19 @@
+import os.path
+
+path = "un\\normalized/path"
+
+p1 = os.path.normpath(path)  # $pathNormalization
+p2 = os.path.normpath(path=path)  # $pathNormalization
+
+np = os.path.normpath
+
+p3 = np(path)  # $pathNormalization
+p4 = np(path=path)  # $pathNormalization
+
+
+def normalize(path):
+    return os.path.normpath(path)  # $pathNormalization
+
+
+p5 = normalize(path)
+p6 = normalize(path=path)
--- a/python/ql/test/experimental/library-tests/frameworks/stdlib/SafeAccessCheck.py
+++ b/python/ql/test/experimental/library-tests/frameworks/stdlib/SafeAccessCheck.py
@@ -0,0 +1,8 @@
+s = "taintedString"
+
+if s.startswith("tainted"):  # $checks=s $branch=true
+    pass
+
+sw = s.startswith  # $f-:checks=s $f-:branch=true
+if sw("safe"):
+    pass
--- a/python/ql/test/experimental/meta/ConceptsTest.qll
+++ b/python/ql/test/experimental/meta/ConceptsTest.qll
@@ -184,3 +184,59 @@ class HttpServerHttpResponseTest extends InlineExpectationsTest {
    )
  }
 }
+
+class FileSystemAccessTest extends InlineExpectationsTest {
+  FileSystemAccessTest() { this = "FileSystemAccessTest" }
+
+  override string getARelevantTag() { result = "getAPathArgument" }
+
+  override predicate hasActualResult(Location location, string element, string tag, string value) {
+    exists(FileSystemAccess a, DataFlow::Node path |
+      exists(location.getFile().getRelativePath()) and
+      path = a.getAPathArgument() and
+      location = a.getLocation() and
+      element = path.toString() and
+      value = value_from_expr(path.asExpr()) and
+      tag = "getAPathArgument"
+    )
+  }
+}
+
+class PathNormalizationTest extends InlineExpectationsTest {
+  PathNormalizationTest() { this = "PathNormalizationTest" }
+
+  override string getARelevantTag() { result = "pathNormalization" }
+
+  override predicate hasActualResult(Location location, string element, string tag, string value) {
+    exists(Path::PathNormalization n |
+      exists(location.getFile().getRelativePath()) and
+      location = n.getLocation() and
+      element = n.toString() and
+      value = "" and
+      tag = "pathNormalization"
+    )
+  }
+}
+
+class SafeAccessCheckTest extends InlineExpectationsTest {
+  SafeAccessCheckTest() { this = "SafeAccessCheckTest" }
+
+  override string getARelevantTag() { result in ["checks", "branch"] }
+
+  override predicate hasActualResult(Location location, string element, string tag, string value) {
+    exists(Path::SafeAccessCheck c, DataFlow::Node checks, boolean branch |
+      exists(location.getFile().getRelativePath()) and
+      c.checks(checks.asCfgNode(), branch) and
+      location = c.getLocation() and
+      (
+        element = checks.toString() and
+        value = value_from_expr(checks.asExpr()) and
+        tag = "checks"
+        or
+        element = branch.toString() and
+        value = branch.toString() and
+        tag = "branch"
+      )
+    )
+  }
+}
--- a/python/ql/test/experimental/query-tests/Security-new-dataflow/CWE-022/PathInjection.expected
+++ b/python/ql/test/experimental/query-tests/Security-new-dataflow/CWE-022/PathInjection.expected
@@ -0,0 +1,94 @@
+edges
+| path_injection.py:9:12:9:23 | ControlFlowNode for Attribute | path_injection.py:10:14:10:44 | ControlFlowNode for Attribute() |
+| path_injection.py:15:12:15:23 | ControlFlowNode for Attribute | path_injection.py:16:13:16:61 | ControlFlowNode for Attribute() |
+| path_injection.py:16:13:16:61 | ControlFlowNode for Attribute() | path_injection.py:17:14:17:18 | ControlFlowNode for npath |
+| path_injection.py:24:12:24:23 | ControlFlowNode for Attribute | path_injection.py:25:13:25:61 | ControlFlowNode for Attribute() |
+| path_injection.py:25:13:25:61 | ControlFlowNode for Attribute() | path_injection.py:28:14:28:18 | ControlFlowNode for npath |
+| path_injection.py:33:12:33:23 | ControlFlowNode for Attribute | path_injection.py:34:13:34:61 | ControlFlowNode for Attribute() |
+| test.py:9:12:9:23 | ControlFlowNode for Attribute | test.py:9:12:9:39 | ControlFlowNode for Attribute() |
+| test.py:9:12:9:23 | ControlFlowNode for Attribute | test.py:9:12:9:39 | ControlFlowNode for Attribute() |
+| test.py:9:12:9:39 | ControlFlowNode for Attribute() | test.py:18:9:18:16 | ControlFlowNode for source() |
+| test.py:9:12:9:39 | ControlFlowNode for Attribute() | test.py:24:9:24:16 | ControlFlowNode for source() |
+| test.py:9:12:9:39 | ControlFlowNode for Attribute() | test.py:31:9:31:16 | ControlFlowNode for source() |
+| test.py:9:12:9:39 | ControlFlowNode for Attribute() | test.py:38:9:38:16 | ControlFlowNode for source() |
+| test.py:9:12:9:39 | ControlFlowNode for Attribute() | test.py:46:9:46:16 | ControlFlowNode for source() |
+| test.py:12:15:12:15 | SSA variable x | test.py:13:12:13:30 | ControlFlowNode for Attribute() |
+| test.py:13:12:13:30 | ControlFlowNode for Attribute() | test.py:25:9:25:20 | ControlFlowNode for normalize() |
+| test.py:13:12:13:30 | ControlFlowNode for Attribute() | test.py:48:13:48:24 | ControlFlowNode for normalize() |
+| test.py:18:9:18:16 | ControlFlowNode for source() | test.py:19:10:19:10 | ControlFlowNode for x |
+| test.py:24:9:24:16 | ControlFlowNode for source() | test.py:25:19:25:19 | ControlFlowNode for x |
+| test.py:25:9:25:20 | ControlFlowNode for normalize() | test.py:26:10:26:10 | ControlFlowNode for y |
+| test.py:25:19:25:19 | ControlFlowNode for x | test.py:12:15:12:15 | SSA variable x |
+| test.py:31:9:31:16 | ControlFlowNode for source() | test.py:33:14:33:14 | ControlFlowNode for x |
+| test.py:38:9:38:16 | ControlFlowNode for source() | test.py:39:19:39:19 | ControlFlowNode for x |
+| test.py:39:19:39:19 | ControlFlowNode for x | test.py:12:15:12:15 | SSA variable x |
+| test.py:46:9:46:16 | ControlFlowNode for source() | test.py:48:23:48:23 | ControlFlowNode for x |
+| test.py:48:13:48:24 | ControlFlowNode for normalize() | test.py:49:14:49:14 | ControlFlowNode for y |
+| test.py:48:23:48:23 | ControlFlowNode for x | test.py:12:15:12:15 | SSA variable x |
+| test_chaining.py:9:12:9:23 | ControlFlowNode for Attribute | test_chaining.py:9:12:9:39 | ControlFlowNode for Attribute() |
+| test_chaining.py:9:12:9:39 | ControlFlowNode for Attribute() | test_chaining.py:20:9:20:16 | ControlFlowNode for source() |
+| test_chaining.py:9:12:9:39 | ControlFlowNode for Attribute() | test_chaining.py:28:9:28:16 | ControlFlowNode for source() |
+| test_chaining.py:9:12:9:39 | ControlFlowNode for Attribute() | test_chaining.py:41:9:41:16 | ControlFlowNode for source() |
+| test_chaining.py:14:15:14:15 | SSA variable x | test_chaining.py:15:12:15:30 | ControlFlowNode for Attribute() |
+| test_chaining.py:15:12:15:30 | ControlFlowNode for Attribute() | test_chaining.py:31:13:31:24 | ControlFlowNode for normalize() |
+| test_chaining.py:20:9:20:16 | ControlFlowNode for source() | test_chaining.py:21:19:21:19 | ControlFlowNode for x |
+| test_chaining.py:21:19:21:19 | ControlFlowNode for x | test_chaining.py:14:15:14:15 | SSA variable x |
+| test_chaining.py:28:9:28:16 | ControlFlowNode for source() | test_chaining.py:29:19:29:19 | ControlFlowNode for x |
+| test_chaining.py:29:19:29:19 | ControlFlowNode for x | test_chaining.py:14:15:14:15 | SSA variable x |
+| test_chaining.py:31:13:31:24 | ControlFlowNode for normalize() | test_chaining.py:32:14:32:14 | ControlFlowNode for z |
+| test_chaining.py:41:9:41:16 | ControlFlowNode for source() | test_chaining.py:42:9:42:19 | ControlFlowNode for normpath() |
+| test_chaining.py:44:13:44:23 | ControlFlowNode for normpath() | test_chaining.py:45:14:45:14 | ControlFlowNode for z |
+nodes
+| path_injection.py:9:12:9:23 | ControlFlowNode for Attribute | semmle.label | ControlFlowNode for Attribute |
+| path_injection.py:10:14:10:44 | ControlFlowNode for Attribute() | semmle.label | ControlFlowNode for Attribute() |
+| path_injection.py:15:12:15:23 | ControlFlowNode for Attribute | semmle.label | ControlFlowNode for Attribute |
+| path_injection.py:16:13:16:61 | ControlFlowNode for Attribute() | semmle.label | ControlFlowNode for Attribute() |
+| path_injection.py:17:14:17:18 | ControlFlowNode for npath | semmle.label | ControlFlowNode for npath |
+| path_injection.py:24:12:24:23 | ControlFlowNode for Attribute | semmle.label | ControlFlowNode for Attribute |
+| path_injection.py:25:13:25:61 | ControlFlowNode for Attribute() | semmle.label | ControlFlowNode for Attribute() |
+| path_injection.py:28:14:28:18 | ControlFlowNode for npath | semmle.label | ControlFlowNode for npath |
+| path_injection.py:33:12:33:23 | ControlFlowNode for Attribute | semmle.label | ControlFlowNode for Attribute |
+| path_injection.py:34:13:34:61 | ControlFlowNode for Attribute() | semmle.label | ControlFlowNode for Attribute() |
+| test.py:9:12:9:23 | ControlFlowNode for Attribute | semmle.label | ControlFlowNode for Attribute |
+| test.py:9:12:9:23 | ControlFlowNode for Attribute | semmle.label | ControlFlowNode for Attribute |
+| test.py:9:12:9:39 | ControlFlowNode for Attribute() | semmle.label | ControlFlowNode for Attribute() |
+| test.py:9:12:9:39 | ControlFlowNode for Attribute() | semmle.label | ControlFlowNode for Attribute() |
+| test.py:12:15:12:15 | SSA variable x | semmle.label | SSA variable x |
+| test.py:13:12:13:30 | ControlFlowNode for Attribute() | semmle.label | ControlFlowNode for Attribute() |
+| test.py:18:9:18:16 | ControlFlowNode for source() | semmle.label | ControlFlowNode for source() |
+| test.py:19:10:19:10 | ControlFlowNode for x | semmle.label | ControlFlowNode for x |
+| test.py:24:9:24:16 | ControlFlowNode for source() | semmle.label | ControlFlowNode for source() |
+| test.py:25:9:25:20 | ControlFlowNode for normalize() | semmle.label | ControlFlowNode for normalize() |
+| test.py:25:19:25:19 | ControlFlowNode for x | semmle.label | ControlFlowNode for x |
+| test.py:26:10:26:10 | ControlFlowNode for y | semmle.label | ControlFlowNode for y |
+| test.py:31:9:31:16 | ControlFlowNode for source() | semmle.label | ControlFlowNode for source() |
+| test.py:33:14:33:14 | ControlFlowNode for x | semmle.label | ControlFlowNode for x |
+| test.py:38:9:38:16 | ControlFlowNode for source() | semmle.label | ControlFlowNode for source() |
+| test.py:39:19:39:19 | ControlFlowNode for x | semmle.label | ControlFlowNode for x |
+| test.py:46:9:46:16 | ControlFlowNode for source() | semmle.label | ControlFlowNode for source() |
+| test.py:48:13:48:24 | ControlFlowNode for normalize() | semmle.label | ControlFlowNode for normalize() |
+| test.py:48:23:48:23 | ControlFlowNode for x | semmle.label | ControlFlowNode for x |
+| test.py:49:14:49:14 | ControlFlowNode for y | semmle.label | ControlFlowNode for y |
+| test_chaining.py:9:12:9:23 | ControlFlowNode for Attribute | semmle.label | ControlFlowNode for Attribute |
+| test_chaining.py:9:12:9:39 | ControlFlowNode for Attribute() | semmle.label | ControlFlowNode for Attribute() |
+| test_chaining.py:14:15:14:15 | SSA variable x | semmle.label | SSA variable x |
+| test_chaining.py:15:12:15:30 | ControlFlowNode for Attribute() | semmle.label | ControlFlowNode for Attribute() |
+| test_chaining.py:20:9:20:16 | ControlFlowNode for source() | semmle.label | ControlFlowNode for source() |
+| test_chaining.py:21:19:21:19 | ControlFlowNode for x | semmle.label | ControlFlowNode for x |
+| test_chaining.py:28:9:28:16 | ControlFlowNode for source() | semmle.label | ControlFlowNode for source() |
+| test_chaining.py:29:19:29:19 | ControlFlowNode for x | semmle.label | ControlFlowNode for x |
+| test_chaining.py:31:13:31:24 | ControlFlowNode for normalize() | semmle.label | ControlFlowNode for normalize() |
+| test_chaining.py:32:14:32:14 | ControlFlowNode for z | semmle.label | ControlFlowNode for z |
+| test_chaining.py:41:9:41:16 | ControlFlowNode for source() | semmle.label | ControlFlowNode for source() |
+| test_chaining.py:42:9:42:19 | ControlFlowNode for normpath() | semmle.label | ControlFlowNode for normpath() |
+| test_chaining.py:44:13:44:23 | ControlFlowNode for normpath() | semmle.label | ControlFlowNode for normpath() |
+| test_chaining.py:45:14:45:14 | ControlFlowNode for z | semmle.label | ControlFlowNode for z |
+#select
+| path_injection.py:10:14:10:44 | ControlFlowNode for Attribute() | path_injection.py:9:12:9:23 | ControlFlowNode for Attribute | path_injection.py:10:14:10:44 | ControlFlowNode for Attribute() | This path depends on $@. | path_injection.py:9:12:9:23 | ControlFlowNode for Attribute | a user-provided value |
+| path_injection.py:17:14:17:18 | ControlFlowNode for npath | path_injection.py:15:12:15:23 | ControlFlowNode for Attribute | path_injection.py:17:14:17:18 | ControlFlowNode for npath | This path depends on $@. | path_injection.py:15:12:15:23 | ControlFlowNode for Attribute | a user-provided value |
+| path_injection.py:28:14:28:18 | ControlFlowNode for npath | path_injection.py:24:12:24:23 | ControlFlowNode for Attribute | path_injection.py:28:14:28:18 | ControlFlowNode for npath | This path depends on $@. | path_injection.py:24:12:24:23 | ControlFlowNode for Attribute | a user-provided value |
+| test.py:19:10:19:10 | ControlFlowNode for x | test.py:9:12:9:23 | ControlFlowNode for Attribute | test.py:19:10:19:10 | ControlFlowNode for x | This path depends on $@. | test.py:9:12:9:23 | ControlFlowNode for Attribute | a user-provided value |
+| test.py:26:10:26:10 | ControlFlowNode for y | test.py:9:12:9:23 | ControlFlowNode for Attribute | test.py:26:10:26:10 | ControlFlowNode for y | This path depends on $@. | test.py:9:12:9:23 | ControlFlowNode for Attribute | a user-provided value |
+| test.py:33:14:33:14 | ControlFlowNode for x | test.py:9:12:9:23 | ControlFlowNode for Attribute | test.py:33:14:33:14 | ControlFlowNode for x | This path depends on $@. | test.py:9:12:9:23 | ControlFlowNode for Attribute | a user-provided value |
+| test.py:49:14:49:14 | ControlFlowNode for y | test.py:9:12:9:23 | ControlFlowNode for Attribute | test.py:49:14:49:14 | ControlFlowNode for y | This path depends on $@. | test.py:9:12:9:23 | ControlFlowNode for Attribute | a user-provided value |
+| test_chaining.py:32:14:32:14 | ControlFlowNode for z | test_chaining.py:9:12:9:23 | ControlFlowNode for Attribute | test_chaining.py:32:14:32:14 | ControlFlowNode for z | This path depends on $@. | test_chaining.py:9:12:9:23 | ControlFlowNode for Attribute | a user-provided value |
--- a/python/ql/test/experimental/query-tests/Security-new-dataflow/CWE-022/PathInjection.qlref
+++ b/python/ql/test/experimental/query-tests/Security-new-dataflow/CWE-022/PathInjection.qlref
@@ -0,0 +1 @@
+experimental/Security-new-dataflow/CWE-022/PathInjection.ql
--- a/python/ql/test/experimental/query-tests/Security-new-dataflow/CWE-022/path_injection.py
+++ b/python/ql/test/experimental/query-tests/Security-new-dataflow/CWE-022/path_injection.py
@@ -0,0 +1,36 @@
+
+import os.path
+
+from flask import Flask, request
+app = Flask(__name__)
+
+@app.route("/path1")
+def path_injection():
+    path = request.args.get('path', '')
+    f = open(os.path.join(os.getcwd(), path))
+
+@app.route("/path2")
+def path_injection():
+    # Normalized, but not checked
+    path = request.args.get('path', '')
+    npath = os.path.normpath(os.path.join(os.getcwd(), path))
+    f = open(npath)  # Path not found
+
+SAFE = "/tmp/scratch_area/"
+
+@app.route("/path3")
+def safe_path():
+    # Normalized, but check doesn't reach open().
+    path = request.args.get('path', '')
+    npath = os.path.normpath(os.path.join(os.getcwd(), path))
+    if npath.startswith(SAFE):
+        pass
+    f = open(npath)  # Path not found
+
+@app.route("/path4")
+def safe_path():
+    # Normalized, and checked properly
+    path = request.args.get('path', '')
+    npath = os.path.normpath(os.path.join(os.getcwd(), path))
+    if npath.startswith(SAFE):
+        f = open(npath)
--- a/python/ql/test/experimental/query-tests/Security-new-dataflow/CWE-022/test.py
+++ b/python/ql/test/experimental/query-tests/Security-new-dataflow/CWE-022/test.py
@@ -0,0 +1,49 @@
+import os.path
+
+from flask import Flask, request
+
+app = Flask(__name__)
+
+
+def source():
+    return request.args.get("path", "")
+
+
+def normalize(x):
+    return os.path.normpath(x)
+
+
+@app.route("/path")
+def simple():
+    x = source()
+    open(x)  # NOT OK
+
+
+@app.route("/path")
+def normalization():
+    x = source()
+    y = normalize(x)
+    open(y)  # NOT OK
+
+
+@app.route("/path")
+def check():
+    x = source()
+    if x.startswith("subfolder/"):
+        open(x)  # NOT OK
+
+
+@app.route("/path")
+def normalize_then_check():
+    x = source()
+    y = normalize(x)
+    if y.startswith("subfolder/"):
+        open(y)  # OK
+
+
+@app.route("/path")
+def check_then_normalize():
+    x = source()
+    if x.startswith("subfolder/"):
+        y = normalize(x)
+        open(y)  # NOT OK
--- a/python/ql/test/experimental/query-tests/Security-new-dataflow/CWE-022/test_chaining.py
+++ b/python/ql/test/experimental/query-tests/Security-new-dataflow/CWE-022/test_chaining.py
@@ -0,0 +1,45 @@
+import os.path
+
+from flask import Flask, request
+
+app = Flask(__name__)
+
+
+def source():
+    return request.args.get("path", "")
+
+
+# Wrap normalization, so we can fool the chained configurations.
+# (Call context is lost at cross-over nodes.)
+def normalize(x):
+    return os.path.normpath(x)
+
+
+@app.route("/path")
+def normalize_then_check():
+    x = source()
+    y = normalize(x)  # <--- this call...
+    if y.startswith("subfolder/"):
+        open(y)  # OK
+
+
+@app.route("/path")
+def normalize_check_normalize():
+    x = source()
+    y = normalize(x)  # (...or this call...)
+    if y.startswith("subfolder/"):
+        z = normalize(y)  # <--- ...can jump to here, resulting in FP
+        open(z)  # OK
+
+
+# The problem does not manifest if we simply define an alias
+normpath = os.path.normpath
+
+
+@app.route("/path")
+def normalize_check_normalize_alias():
+    x = source()
+    y = normpath(x)
+    if y.startswith("subfolder/"):
+        z = normpath(y)
+        open(z)  # OK
				`@@ -0,0 +1 @@`
				`experimental/Security-new-dataflow/CWE-022/PathInjection.ql`