Merge from master

2026-05-03 04:39:29 +02:00 · 2019-09-26 22:15:02 -07:00
parent c389432922 18b28b1b57
commit 9b8b364c8f
107 changed files with 8138 additions and 245 deletions
--- a/change-notes/1.23/analysis-javascript.md
+++ b/change-notes/1.23/analysis-javascript.md
@@ -22,14 +22,16 @@
 | **Query**                      | **Expected impact**          | **Change**                                                                |
 |--------------------------------|------------------------------|---------------------------------------------------------------------------|
 | Incomplete string escaping or encoding (`js/incomplete-sanitization`) | Fewer false-positive results | This rule now recognizes additional ways delimiters can be stripped away. |
-| Client-side cross-site scripting (`js/xss`) | More results | More potential vulnerabilities involving functions that manipulate DOM attributes are now recognized. |
+| Client-side cross-site scripting (`js/xss`) | More results, fewer false-positive results | More potential vulnerabilities involving functions that manipulate DOM attributes are now recognized, and more sanitizers are detected. |
 | Code injection (`js/code-injection`) | More results | More potential vulnerabilities involving functions that manipulate DOM event handler attributes are now recognized. |
 | Hard-coded credentials (`js/hardcoded-credentials`) | Fewer false-positive results | This rule now flags fewer password examples. |
 | Illegal invocation (`js/illegal-invocation`) | Fewer false-positive results | This rule now correctly handles methods named `call` and `apply`. |
-| Incorrect suffix check (`js/incorrect-suffix-check`) | Fewer false-positive results | The query recognizes valid checks in more cases. 
+| Incorrect suffix check (`js/incorrect-suffix-check`) | Fewer false-positive results | The query recognizes valid checks in more cases. |
 | Network data written to file (`js/http-to-file-access`) | Fewer false-positive results | This query has been renamed to better match its intended purpose, and now only considers network data untrusted. | 
 | Password in configuration file (`js/password-in-configuration-file`) | Fewer false-positive results | This rule now flags fewer password examples. |
 | Prototype pollution (`js/prototype-pollution`) | More results | The query now highlights vulnerable uses of jQuery and Angular, and the results are shown on LGTM by default. |
+| Reflected cross-site scripting (`js/reflected-xss`) | Fewer false-positive results | The query now recognizes more sanitizers. |
+| Stored cross-site scripting (`js/stored-xss`) | Fewer false-positive results | The query now recognizes more sanitizers. |
 | Uncontrolled command line (`js/command-line-injection`) | More results | This query now treats responses from servers as untrusted. |

 ## Changes to QL libraries
--- a/cpp/ql/src/semmle/code/cpp/exprs/Expr.qll
+++ b/cpp/ql/src/semmle/code/cpp/exprs/Expr.qll
@@ -131,6 +131,8 @@ class Expr extends StmtParent, @expr {
    valuebind(_, underlyingElement(this))
    or
    addressConstantExpression(this)
+    or
+    constantTemplateLiteral(this)
  }

  /**
@@ -1119,3 +1121,17 @@ private predicate isStandardPlacementNewAllocator(Function operatorNew) {

 // Pulled out for performance. See QL-796.
 private predicate hasNoConversions(Expr e) { not e.hasConversion() }
+
+/**
+ * Holds if `e` is a literal of unknown value in a template, or a cast thereof.
+ * We assume that such literals are constant.
+ */
+private predicate constantTemplateLiteral(Expr e) {
+  // Unknown literals in uninstantiated templates could be enum constant
+  // accesses or pointer-to-member literals.
+  e instanceof Literal and
+  e.isFromUninstantiatedTemplate(_) and
+  not exists(e.getValue())
+  or
+  constantTemplateLiteral(e.(Cast).getExpr())
+}
--- a/cpp/ql/src/semmle/code/cpp/exprs/Literal.qll
+++ b/cpp/ql/src/semmle/code/cpp/exprs/Literal.qll
@@ -132,7 +132,6 @@ class HexLiteral extends Literal {
 * A C/C++ aggregate literal.
 */
 class AggregateLiteral extends Expr, @aggregateliteral {
-  // if this is turned into a Literal we need to change mayBeImpure
  override string getCanonicalQLClass() { result = "AggregateLiteral" }

  /**
@@ -145,6 +144,10 @@ class AggregateLiteral extends Expr, @aggregateliteral {
    result = this.(ClassAggregateLiteral).getFieldExpr(f)
  }

+  override predicate mayBeImpure() { this.getAChild().mayBeImpure() }
+
+  override predicate mayBeGloballyImpure() { this.getAChild().mayBeGloballyImpure() }
+
  /** Gets a textual representation of this aggregate literal. */
  override string toString() { result = "{...}" }
 }
--- a/cpp/ql/src/semmle/code/cpp/internal/AddressConstantExpression.qll
+++ b/cpp/ql/src/semmle/code/cpp/internal/AddressConstantExpression.qll
@@ -32,6 +32,11 @@ private predicate constantAddressLValue(Expr lvalue) {
  // tells us how it's going to be used.
  lvalue.(FunctionAccess).getType() instanceof RoutineType
  or
+  // Pointer-to-member literals in uninstantiated templates
+  lvalue instanceof Literal and
+  not exists(lvalue.getValue()) and
+  lvalue.isFromUninstantiatedTemplate(_)
+  or
  // String literals have array types and undergo array-to-pointer conversion.
  lvalue instanceof StringLiteral
  or
@@ -61,6 +66,10 @@ private predicate constantAddressPointer(Expr pointer) {
  // tells us how it's going to be used.
  pointer.(FunctionAccess).getType() instanceof FunctionPointerType
  or
+  // Pointer to member function. These accesses are always pointers even though
+  // their type is `RoutineType`.
+  pointer.(FunctionAccess).getTarget() instanceof MemberFunction
+  or
  addressConstantVariable(pointer.(VariableAccess).getTarget()) and
  pointer.getType().getUnderlyingType() instanceof PointerType
  or
--- a/cpp/ql/src/semmle/code/cpp/models/interfaces/ArrayFunction.qll
+++ b/cpp/ql/src/semmle/code/cpp/models/interfaces/ArrayFunction.qll
@@ -1,11 +1,11 @@
 /**
 * Provides an abstract class for accurate modeling of input and output buffers
 * in library functions when source code is not available.  To use this QL
- * library, create a QL class extending `BufferFunction` with a characteristic
+ * library, create a QL class extending `ArrayFunction` with a characteristic
 * predicate that selects the function or set of functions you are trying to
- * model. Within that class, override the predicates provided by `BufferFunction`
+ * model. Within that class, override the predicates provided by `ArrayFunction`
 * to match the flow within that function.  Finally, add a private import
- * statement to `CustomModels.qll`
+ * statement to `Models.qll`
 */

 import semmle.code.cpp.Function
--- a/cpp/ql/test/library-tests/namespaces/same_name/decls.expected
+++ b/cpp/ql/test/library-tests/namespaces/same_name/decls.expected
@@ -7,5 +7,6 @@
 | file://:0:0:0:0 | (global namespace) | file://:0:0:0:0 | p#0 |
 | file://:0:0:0:0 | (global namespace) | file://:0:0:0:0 | p#0 |
 | file://:0:0:0:0 | (global namespace) | file://:0:0:0:0 | reg_save_area |
-| same_name.cpp:4:11:4:21 | namespace_a | same_name.cpp:2:11:2:11 | c |
+| file://:0:0:0:0 | (global namespace) | same_name.cpp:2:11:2:11 | c |
 | same_name.cpp:4:11:4:21 | namespace_a | same_name.cpp:6:12:6:12 | c |
+| same_name.cpp:9:11:9:21 | namespace_b | same_name.cpp:11:12:11:12 | c |
--- a/cpp/ql/test/library-tests/namespaces/same_name/same_name.cpp
+++ b/cpp/ql/test/library-tests/namespaces/same_name/same_name.cpp
@@ -8,9 +8,5 @@ namespace namespace_a

 namespace namespace_b
 {
-	//const int c = 1;
-	//
-	// this example is causing a DBCheck failure along the lines of:
-	// 
-	// [INVALID_KEY] Relation namespacembrs((@namespace parentid, unique @namespacembr memberid)): Value 132 of key field memberid occurs in several tuples. Two such tuples are: (134,132) and (144,132)
+	const int c = 1;
 }
--- a/cpp/ql/test/library-tests/sideEffects/exprs/exprs.c
+++ b/cpp/ql/test/library-tests/sideEffects/exprs/exprs.c
@@ -1,5 +1,5 @@

-void f1(int p) {
+int f1(int p) {
    int i;

    for (
@@ -11,3 +11,20 @@ void f1(int p) {

    return p;
 }
+
+int global_int;
+
+int f2(void) {
+    global_int = 3;
+    return 1;
+}
+
+int f3(void) {
+    return 2;
+}
+
+void f4(void) {
+    int is0[3] = { 3, 4, 5 };
+    int is1[3] = { 3, f2(), 5 };
+    int is2[3] = { 3, f3(), 5 };
+}
--- a/cpp/ql/test/library-tests/sideEffects/exprs/exprs.expected
+++ b/cpp/ql/test/library-tests/sideEffects/exprs/exprs.expected
@@ -10,6 +10,26 @@
 | exprs.c:9:3:9:5 | ++ ... |  | mayBeImpure |  |
 | exprs.c:9:5:9:5 | p | isPure |  |  |
 | exprs.c:12:12:12:12 | p | isPure |  |  |
+| exprs.c:18:5:18:14 | global_int | isPure |  |  |
+| exprs.c:18:5:18:18 | ... = ... |  | mayBeImpure | mayBeGloballyImpure |
+| exprs.c:18:18:18:18 | 3 | isPure |  |  |
+| exprs.c:19:12:19:12 | 1 | isPure |  |  |
+| exprs.c:23:12:23:12 | 2 | isPure |  |  |
+| exprs.c:27:13:27:13 | 3 | isPure |  |  |
+| exprs.c:27:17:27:28 | {...} | isPure |  |  |
+| exprs.c:27:20:27:20 | 3 | isPure |  |  |
+| exprs.c:27:23:27:23 | 4 | isPure |  |  |
+| exprs.c:27:26:27:26 | 5 | isPure |  |  |
+| exprs.c:28:13:28:13 | 3 | isPure |  |  |
+| exprs.c:28:17:28:31 | {...} |  | mayBeImpure | mayBeGloballyImpure |
+| exprs.c:28:20:28:20 | 3 | isPure |  |  |
+| exprs.c:28:23:28:24 | call to f2 |  | mayBeImpure | mayBeGloballyImpure |
+| exprs.c:28:29:28:29 | 5 | isPure |  |  |
+| exprs.c:29:13:29:13 | 3 | isPure |  |  |
+| exprs.c:29:17:29:31 | {...} | isPure |  |  |
+| exprs.c:29:20:29:20 | 3 | isPure |  |  |
+| exprs.c:29:23:29:24 | call to f3 | isPure |  |  |
+| exprs.c:29:29:29:29 | 5 | isPure |  |  |
 | exprs.cpp:7:10:7:16 | (...) | isPure |  |  |
 | exprs.cpp:7:10:7:16 | (reference to) | isPure |  |  |
 | exprs.cpp:7:11:7:15 | * ... | isPure |  |  |
--- a/cpp/ql/test/library-tests/syntax-zoo/aliased_ssa_sanity.expected
+++ b/cpp/ql/test/library-tests/syntax-zoo/aliased_ssa_sanity.expected
@@ -20,7 +20,7 @@ instructionWithoutSuccessor
 | ms_try_mix.cpp:11:12:11:15 | Chi: call to C |
 | ms_try_mix.cpp:28:12:28:15 | Chi: call to C |
 | ms_try_mix.cpp:48:10:48:13 | Chi: call to C |
-| pointer_to_member.cpp:35:11:35:21 | FieldAddress: {...} |
+| pointer_to_member.cpp:36:11:36:30 | FieldAddress: {...} |
 | stmt_expr.cpp:27:5:27:15 | Store: ... = ... |
 | vla.c:5:9:5:14 | VariableAddress: definition of matrix |
 | vla.c:11:6:11:16 | UnmodeledDefinition: vla_typedef |
--- a/cpp/ql/test/library-tests/syntax-zoo/pointer_to_member.cpp
+++ b/cpp/ql/test/library-tests/syntax-zoo/pointer_to_member.cpp
@@ -32,5 +32,16 @@ int usePM(int PM::* pm) {
 void pmIsConst() {
  static const struct {
    int PM::* pm1;
-  } pms = { &PM::x1 };
+    void (PM::* pm2)();
+  } pms = { &PM::x1, &PM::f1 };
 }
+
+template<typename T>
+void pmIsConstT() {
+  static const struct {
+    int T::* pm1;
+    void (T::* pm2)();
+  } pms = { &T::x1, &T::f1 };
+}
+
+template void pmIsConstT<PM>();
--- a/cpp/ql/test/library-tests/syntax-zoo/raw_sanity.expected
+++ b/cpp/ql/test/library-tests/syntax-zoo/raw_sanity.expected
@@ -7,7 +7,7 @@ missingOperand
 | misc.c:220:3:223:3 | Store: ... = ... | Instruction 'Store' is missing an expected operand with tag 'StoreValue' in function '$@'. | misc.c:219:5:219:26 | IR: assign_designated_init | int assign_designated_init(someStruct*) |
 | misc.c:220:9:223:3 | FieldAddress: {...} | Instruction 'FieldAddress' is missing an expected operand with tag 'Unary' in function '$@'. | misc.c:219:5:219:26 | IR: assign_designated_init | int assign_designated_init(someStruct*) |
 | misc.c:220:9:223:3 | FieldAddress: {...} | Instruction 'FieldAddress' is missing an expected operand with tag 'Unary' in function '$@'. | misc.c:219:5:219:26 | IR: assign_designated_init | int assign_designated_init(someStruct*) |
-| pointer_to_member.cpp:35:13:35:19 | FieldAddress: x1 | Instruction 'FieldAddress' is missing an expected operand with tag 'Unary' in function '$@'. | pointer_to_member.cpp:32:6:32:14 | IR: pmIsConst | void pmIsConst() |
+| pointer_to_member.cpp:36:13:36:19 | FieldAddress: x1 | Instruction 'FieldAddress' is missing an expected operand with tag 'Unary' in function '$@'. | pointer_to_member.cpp:32:6:32:14 | IR: pmIsConst | void pmIsConst() |
 | range_analysis.c:368:10:368:21 | Store: ... ? ... : ... | Instruction 'Store' is missing an expected operand with tag 'StoreValue' in function '$@'. | range_analysis.c:355:14:355:27 | IR: test_ternary01 | unsigned int test_ternary01(unsigned int) |
 | range_analysis.c:369:10:369:36 | Store: ... ? ... : ... | Instruction 'Store' is missing an expected operand with tag 'StoreValue' in function '$@'. | range_analysis.c:355:14:355:27 | IR: test_ternary01 | unsigned int test_ternary01(unsigned int) |
 | range_analysis.c:370:10:370:38 | Store: ... ? ... : ... | Instruction 'Store' is missing an expected operand with tag 'StoreValue' in function '$@'. | range_analysis.c:355:14:355:27 | IR: test_ternary01 | unsigned int test_ternary01(unsigned int) |
@@ -68,7 +68,7 @@ instructionWithoutSuccessor
 | ms_try_mix.cpp:48:10:48:13 | CallSideEffect: call to C |
 | ms_try_mix.cpp:51:5:51:11 | ThrowValue: throw ... |
 | ms_try_mix.cpp:53:13:54:3 | NoOp: { ... } |
-| pointer_to_member.cpp:35:11:35:21 | FieldAddress: {...} |
+| pointer_to_member.cpp:36:11:36:30 | FieldAddress: {...} |
 | static_init_templates.cpp:80:27:80:36 | Convert: (void *)... |
 | static_init_templates.cpp:80:27:80:36 | Convert: (void *)... |
 | static_init_templates.cpp:89:27:89:36 | Convert: (void *)... |
@@ -676,7 +676,8 @@ useNotDominatedByDefinition
 | ms_try_mix.cpp:38:16:38:19 | Operand | Operand 'Operand' is not dominated by its definition in function '$@'. | ms_try_mix.cpp:27:6:27:19 | IR: ms_finally_mix | void ms_finally_mix(int) |
 | ms_try_mix.cpp:41:12:41:15 | Operand | Operand 'Operand' is not dominated by its definition in function '$@'. | ms_try_mix.cpp:27:6:27:19 | IR: ms_finally_mix | void ms_finally_mix(int) |
 | ms_try_mix.cpp:51:5:51:11 | Load | Operand 'Load' is not dominated by its definition in function '$@'. | ms_try_mix.cpp:47:6:47:28 | IR: ms_empty_finally_at_end | void ms_empty_finally_at_end() |
-| pointer_to_member.cpp:35:13:35:19 | Address | Operand 'Address' is not dominated by its definition in function '$@'. | pointer_to_member.cpp:32:6:32:14 | IR: pmIsConst | void pmIsConst() |
+| pointer_to_member.cpp:36:11:36:30 | Unary | Operand 'Unary' is not dominated by its definition in function '$@'. | pointer_to_member.cpp:32:6:32:14 | IR: pmIsConst | void pmIsConst() |
+| pointer_to_member.cpp:36:13:36:19 | Address | Operand 'Address' is not dominated by its definition in function '$@'. | pointer_to_member.cpp:32:6:32:14 | IR: pmIsConst | void pmIsConst() |
 | stmt_expr.cpp:30:20:30:21 | Operand | Operand 'Operand' is not dominated by its definition in function '$@'. | stmt_expr.cpp:21:6:21:6 | IR: g | void stmtexpr::g(int) |
 | stmt_expr.cpp:31:16:31:18 | Load | Operand 'Load' is not dominated by its definition in function '$@'. | stmt_expr.cpp:21:6:21:6 | IR: g | void stmtexpr::g(int) |
 | try_catch.cpp:21:13:21:24 | Address | Operand 'Address' is not dominated by its definition in function '$@'. | try_catch.cpp:19:6:19:23 | IR: throw_from_nonstmt | void throw_from_nonstmt(int) |
--- a/cpp/ql/test/library-tests/syntax-zoo/staticlocals.cpp
+++ b/cpp/ql/test/library-tests/syntax-zoo/staticlocals.cpp
@@ -29,4 +29,16 @@ void f2() {
    static C c{};
 }

+template<typename T>
+struct Sizeof {
+  enum sizeof_enum { value = sizeof(T) };
+};
+
+template<typename T>
+void f3() {
+  static int i = Sizeof<T>::value;
+}
+
+template void f3<int>();
+
 }
--- a/cpp/ql/test/library-tests/syntax-zoo/tellDifferent.expected
+++ b/cpp/ql/test/library-tests/syntax-zoo/tellDifferent.expected
@@ -1,3 +1,3 @@
-| staticlocals__staticlocals_f2 | file://:0:0:0:0 | call to C | staticlocals.cpp:30:1:30:1 | return ... | Standard edge, only from QL |
-| staticlocals__staticlocals_f2 | file://:0:0:0:0 | initializer for c | file://:0:0:0:0 | call to C | Standard edge, only from QL |
-| staticlocals__staticlocals_f2 | staticlocals.cpp:29:5:29:17 | declaration | file://:0:0:0:0 | initializer for c | Standard edge, only from QL |
+| staticlocals__staticlocals_f2 | file://:0:0:0:0 | call to C | staticlocals.cpp:30:1:30:1 | return ... | Standard edge, only from QL |  |
+| staticlocals__staticlocals_f2 | file://:0:0:0:0 | initializer for c | file://:0:0:0:0 | call to C | Standard edge, only from QL |  |
+| staticlocals__staticlocals_f2 | staticlocals.cpp:29:5:29:17 | declaration | file://:0:0:0:0 | initializer for c | Standard edge, only from QL |  |
--- a/cpp/ql/test/library-tests/syntax-zoo/tellDifferent.ql
+++ b/cpp/ql/test/library-tests/syntax-zoo/tellDifferent.ql
@@ -1,5 +1,13 @@
 import Compare

+string describeTemplate(ControlFlowNode node) {
+  node.isFromTemplateInstantiation(_) and
+  result = "instantiation"
+  or
+  node.isFromUninstantiatedTemplate(_) and
+  result = "uninstantiated"
+}
+
 from ControlFlowNode n1, ControlFlowNode n2, string msg
 where differentEdge(n1, n2, msg)
-select getScopeName(n1), n1, n2, msg
+select getScopeName(n1), n1, n2, msg, concat(describeTemplate(n1), ", ")
--- a/cpp/ql/test/library-tests/syntax-zoo/unaliased_ssa_sanity.expected
+++ b/cpp/ql/test/library-tests/syntax-zoo/unaliased_ssa_sanity.expected
@@ -29,7 +29,7 @@ instructionWithoutSuccessor
 | ms_try_mix.cpp:11:12:11:15 | CallSideEffect: call to C |
 | ms_try_mix.cpp:28:12:28:15 | CallSideEffect: call to C |
 | ms_try_mix.cpp:48:10:48:13 | CallSideEffect: call to C |
-| pointer_to_member.cpp:35:11:35:21 | FieldAddress: {...} |
+| pointer_to_member.cpp:36:11:36:30 | FieldAddress: {...} |
 | stmt_expr.cpp:27:5:27:15 | Store: ... = ... |
 | vla.c:5:9:5:14 | VariableAddress: definition of matrix |
 | vla.c:11:6:11:16 | UnmodeledDefinition: vla_typedef |
--- a/csharp/ql/src/semmle/code/csharp/ir/IR.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/IR.qll
@@ -3,4 +3,4 @@
 * publicly as the "IR".
 */

-import implementation.raw.IR
+import implementation.unaliased_ssa.IR
--- a/csharp/ql/src/semmle/code/csharp/ir/PrintIR.ql
+++ b/csharp/ql/src/semmle/code/csharp/ir/PrintIR.ql
@@ -5,4 +5,4 @@
 * @kind graph
 */

-import implementation.raw.PrintIR
+import implementation.unaliased_ssa.PrintIR
--- a/csharp/ql/src/semmle/code/csharp/ir/PrintIR.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/PrintIR.qll
@@ -1 +1 @@
-import implementation.raw.PrintIR
+import implementation.unaliased_ssa.PrintIR
--- a/csharp/ql/src/semmle/code/csharp/ir/ValueNumbering.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/ValueNumbering.qll
@@ -1 +1 @@
-import implementation.raw.gvn.ValueNumbering
+import implementation.unaliased_ssa.gvn.ValueNumbering
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/raw/internal/TranslatedDeclaration.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/raw/internal/TranslatedDeclaration.qll
@@ -72,6 +72,4 @@ class TranslatedLocalVariableDeclaration extends TranslatedLocalDeclaration,
        // then the simple variable initialization
        result = getTranslatedInitialization(var.getInitializer())
  }
-
-  override predicate isInitializedByElement() { expr.getParent() instanceof IsExpr }
 }
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/raw/internal/TranslatedElement.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/raw/internal/TranslatedElement.qll
@@ -95,6 +95,12 @@ private predicate ignoreExprOnly(Expr expr) {
  // Ignore the expression (that is not a declaration)
  // that appears in a using block
  expr.getParent().(UsingBlockStmt).getExpr() = expr
+  or
+  // Ignore the `ThisAccess` when it is used as the qualifier for
+  // a callable access (e.g. when a member callable is passed as a
+  // parameter for a delegate creation expression)
+  expr instanceof ThisAccess and
+  expr.getParent() instanceof CallableAccess
 }

 /**
@@ -195,6 +201,10 @@ private predicate ignoreLoad(Expr expr) {
  // to get the address of the first element in an array
  expr = any(ArrayAccess aa).getQualifier()
  or
+  // Indexer calls returns a reference or a value,
+  // no need to load it
+  expr instanceof IndexerCall
+  or
  // No load is needed for the lvalue in an assignment such as:
  // Eg. `Object obj = oldObj`;
  expr = any(Assignment a).getLValue() and
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/raw/internal/TranslatedExpr.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/raw/internal/TranslatedExpr.qll
@@ -1371,6 +1371,11 @@ class TranslatedAssignExpr extends TranslatedAssignment {
 class TranslatedAssignOperation extends TranslatedAssignment {
  override AssignOperation expr;

+  TranslatedAssignOperation() {
+    // Assignments to events is handled differently
+    not expr.getLValue() instanceof EventAccess
+  }
+
  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) {
    kind instanceof GotoEdge and
    (
@@ -1775,18 +1780,18 @@ class TranslatedIsExpr extends TranslatedNonConstantExpr {
    this.hasVar() and
    tag = GeneratedBranchTag() and
    (
-      tag = GeneratedBranchTag() and
      kind instanceof TrueEdge and
-      result = getPatternVarDecl().getFirstInstruction()
+      result = this.getInstruction(InitializerStoreTag())
      or
-      tag = GeneratedBranchTag() and
      kind instanceof FalseEdge and
      result = this.getParent().getChildSuccessor(this)
    )
    or
    tag = GeneratedConstantTag() and
    kind instanceof GotoEdge and
-    result = this.getInstruction(GeneratedNEQTag())
+    if this.hasVar()
+    then result = this.getPatternVarDecl().getFirstInstruction()
+    else result = this.getInstruction(GeneratedNEQTag())
  }

  override Instruction getChildSuccessor(TranslatedElement child) {
@@ -1794,8 +1799,8 @@ class TranslatedIsExpr extends TranslatedNonConstantExpr {
    result = this.getInstruction(ConvertTag())
    or
    this.hasVar() and
-    child = getPatternVarDecl() and
-    result = this.getInstruction(InitializerStoreTag())
+    child = this.getPatternVarDecl() and
+    result = this.getInstruction(GeneratedNEQTag())
  }

  override predicate hasInstruction(
@@ -1821,7 +1826,7 @@ class TranslatedIsExpr extends TranslatedNonConstantExpr {
    this.hasVar() and
    tag = GeneratedBranchTag() and
    opcode instanceof Opcode::ConditionalBranch and
-    resultType = getTypeForPRValue(expr.getType())
+    resultType = getVoidType()
  }

  override string getInstructionConstantValue(InstructionTag tag) {
@@ -2128,3 +2133,37 @@ class TranslatedDelegateCreation extends TranslatedCreation {

  override predicate needsLoad() { none() }
 }
+
+/**
+ * Represents the IR translation of an assign operation where the lhs is an event access.
+ */
+class TranslatedEventAccess extends TranslatedNonConstantExpr {
+  override AssignOperation expr;
+
+  TranslatedEventAccess() { expr.getLValue() instanceof EventAccess }
+
+  // We only translate the lhs, since the rhs is translated as part of the
+  // accessor call.
+  override TranslatedElement getChild(int id) { id = 0 and result = this.getLValue() }
+
+  override predicate hasInstruction(
+    Opcode opcode, InstructionTag tag, Type resultType, boolean isLValue
+  ) {
+    none()
+  }
+
+  final override Instruction getFirstInstruction() {
+    result = this.getLValue().getFirstInstruction()
+  }
+
+  override Instruction getResult() { none() }
+
+  override Instruction getInstructionSuccessor(InstructionTag tag, EdgeKind kind) { none() }
+
+  override Instruction getChildSuccessor(TranslatedElement child) {
+    child = this.getLValue() and
+    result = this.getParent().getChildSuccessor(this)
+  }
+
+  private TranslatedExpr getLValue() { result = getTranslatedExpr(expr.getLValue()) }
+}
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/raw/internal/common/TranslatedDeclarationBase.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/raw/internal/common/TranslatedDeclarationBase.qll
@@ -38,12 +38,7 @@ abstract class LocalVariableDeclarationBase extends TranslatedElement {
      kind instanceof GotoEdge and
      if hasUninitializedInstruction()
      then result = getInstruction(InitializerStoreTag())
-      else
-        if isInitializedByElement()
-        then
-          // initialization is done by an element
-          result = getParent().getChildSuccessor(this)
-        else result = getInitialization().getFirstInstruction()
+      else result = getInitialization().getFirstInstruction()
    )
    or
    hasUninitializedInstruction() and
@@ -74,11 +69,8 @@ abstract class LocalVariableDeclarationBase extends TranslatedElement {
   * desugaring process.
   */
  predicate hasUninitializedInstruction() {
-    (
-      not exists(getInitialization()) or
-      getInitialization() instanceof TranslatedListInitialization
-    ) and
-    not isInitializedByElement()
+    not exists(getInitialization()) or
+    getInitialization() instanceof TranslatedListInitialization
  }

  Instruction getVarAddress() { result = getInstruction(InitializerVariableAddressTag()) }
@@ -100,10 +92,4 @@ abstract class LocalVariableDeclarationBase extends TranslatedElement {
   * as a different step, but do it during the declaration.
   */
  abstract TranslatedElement getInitialization();
-
-  /**
-   * Holds if a declaration is not explicitly initialized,
-   * but will be implicitly initialized by an element.
-   */
-  abstract predicate isInitializedByElement();
 }
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/raw/internal/desugar/internal/TranslatedCompilerGeneratedDeclaration.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/raw/internal/desugar/internal/TranslatedCompilerGeneratedDeclaration.qll
@@ -72,10 +72,6 @@ abstract class TranslatedCompilerGeneratedDeclaration extends LocalVariableDecla
  // element
  override LocalVariable getDeclVar() { none() }

-  // A compiler generated element always has an explicit
-  // initialization
-  override predicate isInitializedByElement() { none() }
-
  override Type getVarType() { result = getIRVariable().getType() }

  /**
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/IR.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/IR.qll
@@ -0,0 +1,29 @@
+import IRFunction
+import Instruction
+import IRBlock
+import IRVariable
+import Operand
+private import internal.IRImports as Imports
+import Imports::EdgeKind
+import Imports::MemoryAccessKind
+
+private newtype TIRPropertyProvider = MkIRPropertyProvider()
+
+/**
+ * Class that provides additional properties to be dumped for IR instructions and blocks when using
+ * the PrintIR module. Libraries that compute additional facts about IR elements can extend the
+ * single instance of this class to specify the additional properties computed by the library.
+ */
+class IRPropertyProvider extends TIRPropertyProvider {
+  string toString() { result = "IRPropertyProvider" }
+
+  /**
+   * Gets the value of the property named `key` for the specified instruction.
+   */
+  string getInstructionProperty(Instruction instruction, string key) { none() }
+
+  /**
+   * Gets the value of the property named `key` for the specified block.
+   */
+  string getBlockProperty(IRBlock block, string key) { none() }
+}
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/IRBlock.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/IRBlock.qll
@@ -0,0 +1,210 @@
+private import internal.IRInternal
+import Instruction
+private import internal.IRBlockImports as Imports
+import Imports::EdgeKind
+private import Cached
+
+/**
+ * A basic block in the IR. A basic block consists of a sequence of `Instructions` with the only
+ * incoming edges at the beginning of the sequence and the only outgoing edges at the end of the
+ * sequence.
+ *
+ * This class does not contain any members that query the predecessor or successor edges of the
+ * block. This allows different classes that extend `IRBlockBase` to expose different subsets of
+ * edges (e.g. ignoring unreachable edges).
+ *
+ * Most consumers should use the class `IRBlock`.
+ */
+class IRBlockBase extends TIRBlock {
+  final string toString() { result = getFirstInstruction(this).toString() }
+
+  final Language::Location getLocation() { result = getFirstInstruction().getLocation() }
+
+  final string getUniqueId() { result = getFirstInstruction(this).getUniqueId() }
+
+  /**
+   * Gets the zero-based index of the block within its function. This is used
+   * by debugging and printing code only.
+   */
+  int getDisplayIndex() {
+    this = rank[result + 1](IRBlock funcBlock |
+        funcBlock.getEnclosingFunction() = getEnclosingFunction()
+      |
+        funcBlock order by funcBlock.getUniqueId()
+      )
+  }
+
+  final Instruction getInstruction(int index) { result = getInstruction(this, index) }
+
+  final PhiInstruction getAPhiInstruction() {
+    Construction::getPhiInstructionBlockStart(result) = getFirstInstruction()
+  }
+
+  final Instruction getAnInstruction() {
+    result = getInstruction(_) or
+    result = getAPhiInstruction()
+  }
+
+  final Instruction getFirstInstruction() { result = getFirstInstruction(this) }
+
+  final Instruction getLastInstruction() { result = getInstruction(getInstructionCount() - 1) }
+
+  final int getInstructionCount() { result = getInstructionCount(this) }
+
+  final IRFunction getEnclosingIRFunction() {
+    result = getFirstInstruction(this).getEnclosingIRFunction()
+  }
+
+  final Language::Function getEnclosingFunction() {
+    result = getFirstInstruction(this).getEnclosingFunction()
+  }
+}
+
+/**
+ * A basic block with additional information about its predecessor and successor edges. Each edge
+ * corresponds to the control flow between the last instruction of one block and the first
+ * instruction of another block.
+ */
+class IRBlock extends IRBlockBase {
+  final IRBlock getASuccessor() { blockSuccessor(this, result) }
+
+  final IRBlock getAPredecessor() { blockSuccessor(result, this) }
+
+  final IRBlock getSuccessor(EdgeKind kind) { blockSuccessor(this, result, kind) }
+
+  final IRBlock getBackEdgeSuccessor(EdgeKind kind) { backEdgeSuccessor(this, result, kind) }
+
+  final predicate immediatelyDominates(IRBlock block) { blockImmediatelyDominates(this, block) }
+
+  final predicate strictlyDominates(IRBlock block) { blockImmediatelyDominates+(this, block) }
+
+  final predicate dominates(IRBlock block) { strictlyDominates(block) or this = block }
+
+  pragma[noinline]
+  final IRBlock dominanceFrontier() {
+    dominates(result.getAPredecessor()) and
+    not strictlyDominates(result)
+  }
+
+  /**
+   * Holds if this block is reachable from the entry point of its function
+   */
+  final predicate isReachableFromFunctionEntry() {
+    this = getEnclosingIRFunction().getEntryBlock() or
+    getAPredecessor().isReachableFromFunctionEntry()
+  }
+}
+
+private predicate startsBasicBlock(Instruction instr) {
+  not instr instanceof PhiInstruction and
+  (
+    count(Instruction predecessor | instr = predecessor.getASuccessor()) != 1 // Multiple predecessors or no predecessor
+    or
+    exists(Instruction predecessor |
+      instr = predecessor.getASuccessor() and
+      strictcount(Instruction other | other = predecessor.getASuccessor()) > 1
+    ) // Predecessor has multiple successors
+    or
+    exists(Instruction predecessor, EdgeKind kind |
+      instr = predecessor.getSuccessor(kind) and
+      not kind instanceof GotoEdge
+    ) // Incoming edge is not a GotoEdge
+    or
+    exists(Instruction predecessor |
+      instr = Construction::getInstructionBackEdgeSuccessor(predecessor, _)
+    ) // A back edge enters this instruction
+  )
+}
+
+private predicate isEntryBlock(TIRBlock block) {
+  block = MkIRBlock(any(EnterFunctionInstruction enter))
+}
+
+cached
+private module Cached {
+  cached
+  newtype TIRBlock = MkIRBlock(Instruction firstInstr) { startsBasicBlock(firstInstr) }
+
+  /** Holds if `i2` follows `i1` in a `IRBlock`. */
+  private predicate adjacentInBlock(Instruction i1, Instruction i2) {
+    exists(GotoEdge edgeKind | i2 = i1.getSuccessor(edgeKind)) and
+    not startsBasicBlock(i2)
+  }
+
+  /** Holds if `i` is the `index`th instruction the block starting with `first`. */
+  private Instruction getInstructionFromFirst(Instruction first, int index) =
+    shortestDistances(startsBasicBlock/1, adjacentInBlock/2)(first, result, index)
+
+  /** Holds if `i` is the `index`th instruction in `block`. */
+  cached
+  Instruction getInstruction(TIRBlock block, int index) {
+    result = getInstructionFromFirst(getFirstInstruction(block), index)
+  }
+
+  cached
+  int getInstructionCount(TIRBlock block) { result = strictcount(getInstruction(block, _)) }
+
+  cached
+  predicate blockSuccessor(TIRBlock pred, TIRBlock succ, EdgeKind kind) {
+    exists(Instruction predLast, Instruction succFirst |
+      predLast = getInstruction(pred, getInstructionCount(pred) - 1) and
+      succFirst = predLast.getSuccessor(kind) and
+      succ = MkIRBlock(succFirst)
+    )
+  }
+
+  pragma[noinline]
+  private predicate blockIdentity(TIRBlock b1, TIRBlock b2) { b1 = b2 }
+
+  pragma[noopt]
+  cached
+  predicate backEdgeSuccessor(TIRBlock pred, TIRBlock succ, EdgeKind kind) {
+    backEdgeSuccessorRaw(pred, succ, kind)
+    or
+    // See the QLDoc on `backEdgeSuccessorRaw`.
+    exists(TIRBlock pred2 |
+      // Joining with `blockIdentity` is a performance trick to get
+      // `forwardEdgeRaw` on the RHS of a join, where it's fast.
+      blockIdentity(pred, pred2) and
+      forwardEdgeRaw+(pred, pred2)
+    ) and
+    blockSuccessor(pred, succ, kind)
+  }
+
+  /**
+   * Holds if there is an edge from `pred` to `succ` that is not a back edge.
+   */
+  private predicate forwardEdgeRaw(TIRBlock pred, TIRBlock succ) {
+    exists(EdgeKind kind |
+      blockSuccessor(pred, succ, kind) and
+      not backEdgeSuccessorRaw(pred, succ, kind)
+    )
+  }
+
+  /**
+   * Holds if the `kind`-edge from `pred` to `succ` is a back edge according to
+   * `Construction`.
+   *
+   * There could be loops of non-back-edges if there is a flaw in the IR
+   * construction or back-edge detection, and this could cause non-termination
+   * of subsequent analysis. To prevent that, a subsequent predicate further
+   * classifies all edges as back edges if they are involved in a loop of
+   * non-back-edges.
+   */
+  private predicate backEdgeSuccessorRaw(TIRBlock pred, TIRBlock succ, EdgeKind kind) {
+    exists(Instruction predLast, Instruction succFirst |
+      predLast = getInstruction(pred, getInstructionCount(pred) - 1) and
+      succFirst = Construction::getInstructionBackEdgeSuccessor(predLast, kind) and
+      succ = MkIRBlock(succFirst)
+    )
+  }
+
+  cached
+  predicate blockSuccessor(TIRBlock pred, TIRBlock succ) { blockSuccessor(pred, succ, _) }
+
+  cached
+  predicate blockImmediatelyDominates(TIRBlock dominator, TIRBlock block) =
+    idominance(isEntryBlock/1, blockSuccessor/2)(_, dominator, block)
+}
+
+Instruction getFirstInstruction(TIRBlock block) { block = MkIRBlock(result) }
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/IRFunction.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/IRFunction.qll
@@ -0,0 +1,81 @@
+private import internal.IRInternal
+import Instruction
+
+private newtype TIRFunction =
+  MkIRFunction(Language::Function func) { Construction::functionHasIR(func) }
+
+/**
+ * Represents the IR for a function.
+ */
+class IRFunction extends TIRFunction {
+  Language::Function func;
+
+  IRFunction() { this = MkIRFunction(func) }
+
+  final string toString() { result = "IR: " + func.toString() }
+
+  /**
+   * Gets the function whose IR is represented.
+   */
+  final Language::Function getFunction() { result = func }
+
+  /**
+   * Gets the location of the function.
+   */
+  final Language::Location getLocation() { result = func.getLocation() }
+
+  /**
+   * Gets the entry point for this function.
+   */
+  pragma[noinline]
+  final EnterFunctionInstruction getEnterFunctionInstruction() {
+    result.getEnclosingIRFunction() = this
+  }
+
+  /**
+   * Gets the exit point for this function.
+   */
+  pragma[noinline]
+  final ExitFunctionInstruction getExitFunctionInstruction() {
+    result.getEnclosingIRFunction() = this
+  }
+
+  pragma[noinline]
+  final UnmodeledDefinitionInstruction getUnmodeledDefinitionInstruction() {
+    result.getEnclosingIRFunction() = this
+  }
+
+  pragma[noinline]
+  final UnmodeledUseInstruction getUnmodeledUseInstruction() {
+    result.getEnclosingIRFunction() = this
+  }
+
+  /**
+   * Gets the single return instruction for this function.
+   */
+  pragma[noinline]
+  final ReturnInstruction getReturnInstruction() { result.getEnclosingIRFunction() = this }
+
+  /**
+   * Gets the variable used to hold the return value of this function. If this
+   * function does not return a value, this predicate does not hold.
+   */
+  pragma[noinline]
+  final IRReturnVariable getReturnVariable() { result.getEnclosingIRFunction() = this }
+
+  /**
+   * Gets the block containing the entry point of this function.
+   */
+  pragma[noinline]
+  final IRBlock getEntryBlock() { result.getFirstInstruction() = getEnterFunctionInstruction() }
+
+  /**
+   * Gets all instructions in this function.
+   */
+  final Instruction getAnInstruction() { result.getEnclosingIRFunction() = this }
+
+  /**
+   * Gets all blocks in this function.
+   */
+  final IRBlock getABlock() { result.getEnclosingIRFunction() = this }
+}
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/IRSanity.ql
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/IRSanity.ql
@@ -0,0 +1,8 @@
+/**
+ * @name SSA IR Sanity Check
+ * @description Performs sanity checks on the Intermediate Representation. This query should have no results.
+ * @kind table
+ * @id cpp/ssa-ir-sanity-check
+ */
+
+import IRSanity
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/IRSanity.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/IRSanity.qll
@@ -0,0 +1,2 @@
+private import IR
+import InstructionSanity
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/IRVariable.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/IRVariable.qll
@@ -0,0 +1,145 @@
+private import internal.IRInternal
+import IRFunction
+private import internal.IRVariableImports as Imports
+import Imports::TempVariableTag
+private import Imports::IRUtilities
+private import Imports::TTempVariableTag
+private import Imports::TIRVariable
+
+IRUserVariable getIRUserVariable(Language::Function func, Language::Variable var) {
+  result.getVariable() = var and
+  result.getEnclosingFunction() = func
+}
+
+/**
+ * Represents a variable referenced by the IR for a function. The variable may
+ * be a user-declared variable (`IRUserVariable`) or a temporary variable
+ * generated by the AST-to-IR translation (`IRTempVariable`).
+ */
+abstract class IRVariable extends TIRVariable {
+  Language::Function func;
+
+  abstract string toString();
+
+  /**
+   * Gets the type of the variable.
+   */
+  abstract Language::Type getType();
+
+  /**
+   * Gets the AST node that declared this variable, or that introduced this
+   * variable as part of the AST-to-IR translation.
+   */
+  abstract Language::AST getAST();
+
+  /**
+   * Gets an identifier string for the variable. This identifier is unique
+   * within the function.
+   */
+  abstract string getUniqueId();
+
+  /**
+   * Gets the source location of this variable.
+   */
+  final Language::Location getLocation() { result = getAST().getLocation() }
+
+  /**
+   * Gets the IR for the function that references this variable.
+   */
+  final IRFunction getEnclosingIRFunction() { result.getFunction() = func }
+
+  /**
+   * Gets the function that references this variable.
+   */
+  final Language::Function getEnclosingFunction() { result = func }
+}
+
+/**
+ * Represents a user-declared variable referenced by the IR for a function.
+ */
+class IRUserVariable extends IRVariable, TIRUserVariable {
+  Language::Variable var;
+  Language::Type type;
+
+  IRUserVariable() { this = TIRUserVariable(var, type, func) }
+
+  final override string toString() { result = getVariable().toString() }
+
+  final override Language::AST getAST() { result = var }
+
+  final override string getUniqueId() {
+    result = getVariable().toString() + " " + getVariable().getLocation().toString()
+  }
+
+  final override Language::Type getType() { result = type }
+
+  /**
+   * Gets the original user-declared variable.
+   */
+  Language::Variable getVariable() { result = var }
+}
+
+/**
+ * Represents a variable (user-declared or temporary) that is allocated on the
+ * stack. This includes all parameters, non-static local variables, and
+ * temporary variables.
+ */
+abstract class IRAutomaticVariable extends IRVariable { }
+
+class IRAutomaticUserVariable extends IRUserVariable, IRAutomaticVariable {
+  override Language::AutomaticVariable var;
+
+  IRAutomaticUserVariable() { Language::isVariableAutomatic(var) }
+
+  final override Language::AutomaticVariable getVariable() { result = var }
+}
+
+class IRStaticUserVariable extends IRUserVariable {
+  override Language::StaticVariable var;
+
+  IRStaticUserVariable() { not Language::isVariableAutomatic(var) }
+
+  final override Language::StaticVariable getVariable() { result = var }
+}
+
+IRTempVariable getIRTempVariable(Language::AST ast, TempVariableTag tag) {
+  result.getAST() = ast and
+  result.getTag() = tag
+}
+
+class IRTempVariable extends IRVariable, IRAutomaticVariable, TIRTempVariable {
+  Language::AST ast;
+  TempVariableTag tag;
+  Language::Type type;
+
+  IRTempVariable() { this = TIRTempVariable(func, ast, tag, type) }
+
+  final override Language::Type getType() { result = type }
+
+  final override Language::AST getAST() { result = ast }
+
+  final override string getUniqueId() {
+    result = "Temp: " + Construction::getTempVariableUniqueId(this)
+  }
+
+  final TempVariableTag getTag() { result = tag }
+
+  override string toString() {
+    result = getBaseString() + ast.getLocation().getStartLine().toString() + ":" +
+        ast.getLocation().getStartColumn().toString()
+  }
+
+  string getBaseString() { result = "#temp" }
+}
+
+class IRReturnVariable extends IRTempVariable {
+  IRReturnVariable() { tag = ReturnValueTempVar() }
+
+  final override string toString() { result = "#return" }
+}
+
+class IRThrowVariable extends IRTempVariable {
+  IRThrowVariable() { tag = ThrowTempVar() }
+
+  override string getBaseString() { result = "#throw" }
+}
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/Instruction.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/Instruction.qll
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/Operand.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/Operand.qll
@@ -0,0 +1,460 @@
+private import internal.IRInternal
+import Instruction
+import IRBlock
+private import internal.OperandImports as Imports
+import Imports::MemoryAccessKind
+import Imports::Overlap
+private import Imports::OperandTag
+
+cached
+private newtype TOperand =
+  TRegisterOperand(Instruction useInstr, RegisterOperandTag tag, Instruction defInstr) {
+    defInstr = Construction::getRegisterOperandDefinition(useInstr, tag) and
+    not isInCycle(useInstr)
+  } or
+  TNonPhiMemoryOperand(
+    Instruction useInstr, MemoryOperandTag tag, Instruction defInstr, Overlap overlap
+  ) {
+    defInstr = Construction::getMemoryOperandDefinition(useInstr, tag, overlap) and
+    not isInCycle(useInstr)
+  } or
+  TPhiOperand(
+    PhiInstruction useInstr, Instruction defInstr, IRBlock predecessorBlock, Overlap overlap
+  ) {
+    defInstr = Construction::getPhiOperandDefinition(useInstr, predecessorBlock, overlap)
+  }
+
+/** Gets a non-phi instruction that defines an operand of `instr`. */
+private Instruction getNonPhiOperandDef(Instruction instr) {
+  result = Construction::getRegisterOperandDefinition(instr, _)
+  or
+  result = Construction::getMemoryOperandDefinition(instr, _, _)
+}
+
+/**
+ * Holds if `instr` is part of a cycle in the operand graph that doesn't go
+ * through a phi instruction and therefore should be impossible.
+ *
+ * If such cycles are present, either due to a programming error in the IR
+ * generation or due to a malformed database, it can cause infinite loops in
+ * analyses that assume a cycle-free graph of non-phi operands. Therefore it's
+ * better to remove these operands than to leave cycles in the operand graph.
+ */
+pragma[noopt]
+private predicate isInCycle(Instruction instr) {
+  instr instanceof Instruction and
+  getNonPhiOperandDef+(instr) = instr
+}
+
+/**
+ * A source operand of an `Instruction`. The operand represents a value consumed by the instruction.
+ */
+class Operand extends TOperand {
+  string toString() { result = "Operand" }
+
+  final Language::Location getLocation() { result = getUse().getLocation() }
+
+  final IRFunction getEnclosingIRFunction() { result = getUse().getEnclosingIRFunction() }
+
+  /**
+   * Gets the `Instruction` that consumes this operand.
+   */
+  Instruction getUse() { none() }
+
+  /**
+   * Gets the `Instruction` whose result is the value of the operand. Unlike
+   * `getDef`, this also has a result when `isDefinitionInexact` holds, which
+   * means that the resulting instruction may only _partially_ or _potentially_
+   * be the value of this operand.
+   */
+  Instruction getAnyDef() { none() }
+
+  /**
+   * Gets the `Instruction` whose result is the value of the operand. Unlike
+   * `getAnyDef`, this also has no result when `isDefinitionInexact` holds,
+   * which means that the resulting instruction must always be exactly the be
+   * the value of this operand.
+   */
+  final Instruction getDef() {
+    result = this.getAnyDef() and
+    getDefinitionOverlap() instanceof MustExactlyOverlap
+  }
+
+  /**
+   * DEPRECATED: renamed to `getUse`.
+   *
+   * Gets the `Instruction` that consumes this operand.
+   */
+  deprecated final Instruction getUseInstruction() { result = getUse() }
+
+  /**
+   * DEPRECATED: use `getAnyDef` or `getDef`. The exact replacement for this
+   * predicate is `getAnyDef`, but most uses of this predicate should probably
+   * be replaced with `getDef`.
+   *
+   * Gets the `Instruction` whose result is the value of the operand.
+   */
+  deprecated final Instruction getDefinitionInstruction() { result = getAnyDef() }
+
+  /**
+   * Gets the overlap relationship between the operand's definition and its use.
+   */
+  Overlap getDefinitionOverlap() { none() }
+
+  /**
+   * Holds if the result of the definition instruction does not exactly overlap this use.
+   */
+  final predicate isDefinitionInexact() { not getDefinitionOverlap() instanceof MustExactlyOverlap }
+
+  /**
+   * Gets a prefix to use when dumping the operand in an operand list.
+   */
+  string getDumpLabel() { result = "" }
+
+  /**
+   * Gets a string describing this operand, suitable for display in IR dumps. This consists of the
+   * result ID of the instruction consumed by the operand, plus a label identifying the operand
+   * kind.
+   *
+   * For example: `this:r3_5`
+   */
+  final string getDumpString() {
+    result = getDumpLabel() + getInexactSpecifier() + getAnyDef().getResultId()
+  }
+
+  /**
+   * Gets a string prefix to prepend to the operand's definition ID in an IR dump, specifying whether the operand is
+   * an exact or inexact use of its definition. For an inexact use, the prefix is "~". For an exact use, the prefix is
+   * the empty string.
+   */
+  private string getInexactSpecifier() {
+    if isDefinitionInexact() then result = "~" else result = ""
+  }
+
+  /**
+   * Get the order in which the operand should be sorted in the operand list.
+   */
+  int getDumpSortOrder() { result = -1 }
+
+  /**
+   * Gets the type of the value consumed by this operand. This is usually the same as the
+   * result type of the definition instruction consumed by this operand. For register operands,
+   * this is always the case. For some memory operands, the operand type may be different from
+   * the definition type, such as in the case of a partial read or a read from a pointer that
+   * has been cast to a different type.
+   */
+  Language::Type getType() { result = getAnyDef().getResultType() }
+
+  /**
+   * Holds if the value consumed by this operand is a glvalue. If this
+   * holds, the value of the operand represents the address of a location,
+   * and the type of the location is given by `getType()`. If this does
+   * not hold, the value of the operand represents a value whose type is
+   * given by `getResultType()`.
+   */
+  predicate isGLValue() { getAnyDef().isGLValue() }
+
+  /**
+   * Gets the size of the value consumed by this operand, in bytes. If the operand does not have
+   * a known constant size, this predicate does not hold.
+   */
+  int getSize() { result = Language::getTypeSize(getType()) }
+}
+
+/**
+ * An operand that consumes a memory result (e.g. the `LoadOperand` on a `Load` instruction).
+ */
+class MemoryOperand extends Operand {
+  MemoryOperand() {
+    this = TNonPhiMemoryOperand(_, _, _, _) or
+    this = TPhiOperand(_, _, _, _)
+  }
+
+  override predicate isGLValue() {
+    // A `MemoryOperand` can never be a glvalue
+    none()
+  }
+
+  /**
+   * Gets the kind of memory access performed by the operand.
+   */
+  MemoryAccessKind getMemoryAccess() { none() }
+
+  /**
+   * Returns the operand that holds the memory address from which the current operand loads its
+   * value, if any. For example, in `r3 = Load r1, m2`, the result of `getAddressOperand()` for `m2`
+   * is `r1`.
+   */
+  final AddressOperand getAddressOperand() {
+    getMemoryAccess().usesAddressOperand() and
+    result.getUse() = getUse()
+  }
+}
+
+/**
+ * An operand that is not an operand of a `PhiInstruction`.
+ */
+class NonPhiOperand extends Operand {
+  Instruction useInstr;
+  Instruction defInstr;
+  OperandTag tag;
+
+  NonPhiOperand() {
+    this = TRegisterOperand(useInstr, tag, defInstr) or
+    this = TNonPhiMemoryOperand(useInstr, tag, defInstr, _)
+  }
+
+  final override Instruction getUse() { result = useInstr }
+
+  final override Instruction getAnyDef() { result = defInstr }
+
+  final override string getDumpLabel() { result = tag.getLabel() }
+
+  final override int getDumpSortOrder() { result = tag.getSortOrder() }
+
+  final OperandTag getOperandTag() { result = tag }
+}
+
+/**
+ * An operand that consumes a register (non-memory) result.
+ */
+class RegisterOperand extends NonPhiOperand, TRegisterOperand {
+  override RegisterOperandTag tag;
+
+  final override Overlap getDefinitionOverlap() {
+    // All register results overlap exactly with their uses.
+    result instanceof MustExactlyOverlap
+  }
+}
+
+class NonPhiMemoryOperand extends NonPhiOperand, MemoryOperand, TNonPhiMemoryOperand {
+  override MemoryOperandTag tag;
+  Overlap overlap;
+
+  NonPhiMemoryOperand() { this = TNonPhiMemoryOperand(useInstr, tag, defInstr, overlap) }
+
+  final override Overlap getDefinitionOverlap() { result = overlap }
+}
+
+class TypedOperand extends NonPhiMemoryOperand {
+  override TypedOperandTag tag;
+
+  final override Language::Type getType() {
+    result = Construction::getInstructionOperandType(useInstr, tag)
+  }
+}
+
+/**
+ * The address operand of an instruction that loads or stores a value from
+ * memory (e.g. `Load`, `Store`).
+ */
+class AddressOperand extends RegisterOperand {
+  override AddressOperandTag tag;
+
+  override string toString() { result = "Address" }
+}
+
+/**
+ * The source value operand of an instruction that loads a value from memory (e.g. `Load`,
+ * `ReturnValue`, `ThrowValue`).
+ */
+class LoadOperand extends TypedOperand {
+  override LoadOperandTag tag;
+
+  override string toString() { result = "Load" }
+
+  final override MemoryAccessKind getMemoryAccess() { result instanceof IndirectMemoryAccess }
+}
+
+/**
+ * The source value operand of a `Store` instruction.
+ */
+class StoreValueOperand extends RegisterOperand {
+  override StoreValueOperandTag tag;
+
+  override string toString() { result = "StoreValue" }
+}
+
+/**
+ * The sole operand of a unary instruction (e.g. `Convert`, `Negate`, `Copy`).
+ */
+class UnaryOperand extends RegisterOperand {
+  override UnaryOperandTag tag;
+
+  override string toString() { result = "Unary" }
+}
+
+/**
+ * The left operand of a binary instruction (e.g. `Add`, `CompareEQ`).
+ */
+class LeftOperand extends RegisterOperand {
+  override LeftOperandTag tag;
+
+  override string toString() { result = "Left" }
+}
+
+/**
+ * The right operand of a binary instruction (e.g. `Add`, `CompareEQ`).
+ */
+class RightOperand extends RegisterOperand {
+  override RightOperandTag tag;
+
+  override string toString() { result = "Right" }
+}
+
+/**
+ * The condition operand of a `ConditionalBranch` or `Switch` instruction.
+ */
+class ConditionOperand extends RegisterOperand {
+  override ConditionOperandTag tag;
+
+  override string toString() { result = "Condition" }
+}
+
+/**
+ * An operand of the special `UnmodeledUse` instruction, representing a value
+ * whose set of uses is unknown.
+ */
+class UnmodeledUseOperand extends NonPhiMemoryOperand {
+  override UnmodeledUseOperandTag tag;
+
+  override string toString() { result = "UnmodeledUse" }
+
+  final override MemoryAccessKind getMemoryAccess() { result instanceof UnmodeledMemoryAccess }
+}
+
+/**
+ * The operand representing the target function of an `Call` instruction.
+ */
+class CallTargetOperand extends RegisterOperand {
+  override CallTargetOperandTag tag;
+
+  override string toString() { result = "CallTarget" }
+}
+
+/**
+ * An operand representing an argument to a function call. This includes both
+ * positional arguments (represented by `PositionalArgumentOperand`) and the
+ * implicit `this` argument, if any (represented by `ThisArgumentOperand`).
+ */
+class ArgumentOperand extends RegisterOperand {
+  override ArgumentOperandTag tag;
+}
+
+/**
+ * An operand representing the implicit 'this' argument to a member function
+ * call.
+ */
+class ThisArgumentOperand extends ArgumentOperand {
+  override ThisArgumentOperandTag tag;
+
+  override string toString() { result = "ThisArgument" }
+}
+
+/**
+ * An operand representing an argument to a function call.
+ */
+class PositionalArgumentOperand extends ArgumentOperand {
+  override PositionalArgumentOperandTag tag;
+  int argIndex;
+
+  PositionalArgumentOperand() { argIndex = tag.getArgIndex() }
+
+  override string toString() { result = "Arg(" + argIndex + ")" }
+
+  /**
+   * Gets the zero-based index of the argument.
+   */
+  final int getIndex() { result = argIndex }
+}
+
+class SideEffectOperand extends TypedOperand {
+  override SideEffectOperandTag tag;
+
+  final override int getSize() {
+    if getType() instanceof Language::UnknownType
+    then result = Construction::getInstructionOperandSize(useInstr, tag)
+    else result = Language::getTypeSize(getType())
+  }
+
+  override MemoryAccessKind getMemoryAccess() {
+    useInstr instanceof CallSideEffectInstruction and
+    result instanceof EscapedMayMemoryAccess
+    or
+    useInstr instanceof CallReadSideEffectInstruction and
+    result instanceof EscapedMayMemoryAccess
+    or
+    useInstr instanceof IndirectReadSideEffectInstruction and
+    result instanceof IndirectMemoryAccess
+    or
+    useInstr instanceof BufferReadSideEffectInstruction and
+    result instanceof BufferMemoryAccess
+    or
+    useInstr instanceof IndirectWriteSideEffectInstruction and
+    result instanceof IndirectMemoryAccess
+    or
+    useInstr instanceof BufferWriteSideEffectInstruction and
+    result instanceof BufferMemoryAccess
+    or
+    useInstr instanceof IndirectMayWriteSideEffectInstruction and
+    result instanceof IndirectMayMemoryAccess
+    or
+    useInstr instanceof BufferMayWriteSideEffectInstruction and
+    result instanceof BufferMayMemoryAccess
+  }
+}
+
+/**
+ * An operand of a `PhiInstruction`.
+ */
+class PhiInputOperand extends MemoryOperand, TPhiOperand {
+  PhiInstruction useInstr;
+  Instruction defInstr;
+  IRBlock predecessorBlock;
+  Overlap overlap;
+
+  PhiInputOperand() { this = TPhiOperand(useInstr, defInstr, predecessorBlock, overlap) }
+
+  override string toString() { result = "Phi" }
+
+  final override PhiInstruction getUse() { result = useInstr }
+
+  final override Instruction getAnyDef() { result = defInstr }
+
+  final override Overlap getDefinitionOverlap() { result = overlap }
+
+  final override int getDumpSortOrder() { result = 11 + getPredecessorBlock().getDisplayIndex() }
+
+  final override string getDumpLabel() {
+    result = "from " + getPredecessorBlock().getDisplayIndex().toString() + ":"
+  }
+
+  /**
+   * Gets the predecessor block from which this value comes.
+   */
+  final IRBlock getPredecessorBlock() { result = predecessorBlock }
+
+  final override MemoryAccessKind getMemoryAccess() { result instanceof PhiMemoryAccess }
+}
+
+/**
+ * The total operand of a Chi node, representing the previous value of the memory.
+ */
+class ChiTotalOperand extends NonPhiMemoryOperand {
+  override ChiTotalOperandTag tag;
+
+  override string toString() { result = "ChiTotal" }
+
+  final override MemoryAccessKind getMemoryAccess() { result instanceof ChiTotalMemoryAccess }
+}
+
+/**
+ * The partial operand of a Chi node, representing the value being written to part of the memory.
+ */
+class ChiPartialOperand extends NonPhiMemoryOperand {
+  override ChiPartialOperandTag tag;
+
+  override string toString() { result = "ChiPartial" }
+
+  final override MemoryAccessKind getMemoryAccess() { result instanceof ChiPartialMemoryAccess }
+}
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/PrintIR.ql
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/PrintIR.ql
@@ -0,0 +1,8 @@
+/**
+ * @name Print SSA IR
+ * @description Outputs a representation of the SSA IR graph
+ * @id cpp/print-ssa-ir
+ * @kind graph
+ */
+
+import PrintIR
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/PrintIR.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/PrintIR.qll
@@ -0,0 +1,260 @@
+private import internal.IRInternal
+private import IR
+private import internal.PrintIRImports as Imports
+import Imports::IRConfiguration
+
+private newtype TPrintIRConfiguration = MkPrintIRConfiguration()
+
+/**
+ * The query can extend this class to control which functions are printed.
+ */
+class PrintIRConfiguration extends TPrintIRConfiguration {
+  string toString() { result = "PrintIRConfiguration" }
+
+  /**
+   * Holds if the IR for `func` should be printed. By default, holds for all
+   * functions.
+   */
+  predicate shouldPrintFunction(Language::Function func) { any() }
+}
+
+private predicate shouldPrintFunction(Language::Function func) {
+  exists(PrintIRConfiguration config | config.shouldPrintFunction(func))
+}
+
+/**
+ * Override of `IRConfiguration` to only create IR for the functions that are to be dumped.
+ */
+private class FilteredIRConfiguration extends IRConfiguration {
+  override predicate shouldCreateIRForFunction(Language::Function func) {
+    shouldPrintFunction(func)
+  }
+}
+
+private string getAdditionalInstructionProperty(Instruction instr, string key) {
+  exists(IRPropertyProvider provider | result = provider.getInstructionProperty(instr, key))
+}
+
+private string getAdditionalBlockProperty(IRBlock block, string key) {
+  exists(IRPropertyProvider provider | result = provider.getBlockProperty(block, key))
+}
+
+private newtype TPrintableIRNode =
+  TPrintableIRFunction(IRFunction irFunc) { shouldPrintFunction(irFunc.getFunction()) } or
+  TPrintableIRBlock(IRBlock block) { shouldPrintFunction(block.getEnclosingFunction()) } or
+  TPrintableInstruction(Instruction instr) { shouldPrintFunction(instr.getEnclosingFunction()) }
+
+/**
+ * A node to be emitted in the IR graph.
+ */
+abstract class PrintableIRNode extends TPrintableIRNode {
+  abstract string toString();
+
+  /**
+   * Gets the location to be emitted for the node.
+   */
+  abstract Language::Location getLocation();
+
+  /**
+   * Gets the label to be emitted for the node.
+   */
+  abstract string getLabel();
+
+  /**
+   * Gets the order in which the node appears in its parent node.
+   */
+  abstract int getOrder();
+
+  /**
+   * Gets the parent of this node.
+   */
+  abstract PrintableIRNode getParent();
+
+  /**
+   * Gets the kind of graph represented by this node ("graph" or "tree").
+   */
+  string getGraphKind() { none() }
+
+  /**
+   * Holds if this node should always be rendered as text, even in a graphical
+   * viewer.
+   */
+  predicate forceText() { none() }
+
+  /**
+   * Gets the value of the node property with the specified key.
+   */
+  string getProperty(string key) {
+    key = "semmle.label" and result = getLabel()
+    or
+    key = "semmle.order" and result = getOrder().toString()
+    or
+    key = "semmle.graphKind" and result = getGraphKind()
+    or
+    key = "semmle.forceText" and forceText() and result = "true"
+  }
+}
+
+/**
+ * An IR graph node representing a `IRFunction` object.
+ */
+class PrintableIRFunction extends PrintableIRNode, TPrintableIRFunction {
+  IRFunction irFunc;
+
+  PrintableIRFunction() { this = TPrintableIRFunction(irFunc) }
+
+  override string toString() { result = irFunc.toString() }
+
+  override Language::Location getLocation() { result = irFunc.getLocation() }
+
+  override string getLabel() { result = Language::getIdentityString(irFunc.getFunction()) }
+
+  override int getOrder() {
+    this = rank[result + 1](PrintableIRFunction orderedFunc, Language::Location location |
+        location = orderedFunc.getIRFunction().getLocation()
+      |
+        orderedFunc
+        order by
+          location.getFile().getAbsolutePath(), location.getStartLine(), location.getStartColumn(),
+          orderedFunc.getLabel()
+      )
+  }
+
+  final override PrintableIRNode getParent() { none() }
+
+  final IRFunction getIRFunction() { result = irFunc }
+}
+
+/**
+ * An IR graph node representing an `IRBlock` object.
+ */
+class PrintableIRBlock extends PrintableIRNode, TPrintableIRBlock {
+  IRBlock block;
+
+  PrintableIRBlock() { this = TPrintableIRBlock(block) }
+
+  override string toString() { result = getLabel() }
+
+  override Language::Location getLocation() { result = block.getLocation() }
+
+  override string getLabel() { result = "Block " + block.getDisplayIndex().toString() }
+
+  override int getOrder() { result = block.getDisplayIndex() }
+
+  final override string getGraphKind() { result = "tree" }
+
+  final override predicate forceText() { any() }
+
+  final override PrintableIRFunction getParent() {
+    result.getIRFunction() = block.getEnclosingIRFunction()
+  }
+
+  override string getProperty(string key) {
+    result = PrintableIRNode.super.getProperty(key) or
+    result = getAdditionalBlockProperty(block, key)
+  }
+
+  final IRBlock getBlock() { result = block }
+}
+
+/**
+ * An IR graph node representing an `Instruction`.
+ */
+class PrintableInstruction extends PrintableIRNode, TPrintableInstruction {
+  Instruction instr;
+
+  PrintableInstruction() { this = TPrintableInstruction(instr) }
+
+  override string toString() { result = instr.toString() }
+
+  override Language::Location getLocation() { result = instr.getLocation() }
+
+  override string getLabel() {
+    exists(IRBlock block |
+      instr = block.getAnInstruction() and
+      exists(
+        string resultString, string operationString, string operandsString, int resultWidth,
+        int operationWidth
+      |
+        resultString = instr.getResultString() and
+        operationString = instr.getOperationString() and
+        operandsString = instr.getOperandsString() and
+        columnWidths(block, resultWidth, operationWidth) and
+        result = resultString + getPaddingString(resultWidth - resultString.length()) + " = " +
+            operationString + getPaddingString(operationWidth - operationString.length()) + " : " +
+            operandsString
+      )
+    )
+  }
+
+  override int getOrder() { result = instr.getDisplayIndexInBlock() }
+
+  final override PrintableIRBlock getParent() { result.getBlock() = instr.getBlock() }
+
+  final Instruction getInstruction() { result = instr }
+
+  override string getProperty(string key) {
+    result = PrintableIRNode.super.getProperty(key) or
+    result = getAdditionalInstructionProperty(instr, key)
+  }
+}
+
+private predicate columnWidths(IRBlock block, int resultWidth, int operationWidth) {
+  resultWidth = max(Instruction instr | instr.getBlock() = block | instr.getResultString().length()) and
+  operationWidth = max(Instruction instr |
+      instr.getBlock() = block
+    |
+      instr.getOperationString().length()
+    )
+}
+
+private int maxColumnWidth() {
+  result = max(Instruction instr, int width |
+      width = instr.getResultString().length() or
+      width = instr.getOperationString().length() or
+      width = instr.getOperandsString().length()
+    |
+      width
+    )
+}
+
+private string getPaddingString(int n) {
+  n = 0 and result = ""
+  or
+  n > 0 and n <= maxColumnWidth() and result = getPaddingString(n - 1) + " "
+}
+
+query predicate nodes(PrintableIRNode node, string key, string value) {
+  value = node.getProperty(key)
+}
+
+private int getSuccessorIndex(IRBlock pred, IRBlock succ) {
+  succ = rank[result + 1](IRBlock aSucc, EdgeKind kind |
+      aSucc = pred.getSuccessor(kind)
+    |
+      aSucc order by kind.toString()
+    )
+}
+
+query predicate edges(PrintableIRBlock pred, PrintableIRBlock succ, string key, string value) {
+  exists(EdgeKind kind, IRBlock predBlock, IRBlock succBlock |
+    predBlock = pred.getBlock() and
+    succBlock = succ.getBlock() and
+    predBlock.getSuccessor(kind) = succBlock and
+    (
+      (
+        key = "semmle.label" and
+        if predBlock.getBackEdgeSuccessor(kind) = succBlock
+        then value = kind.toString() + " (back edge)"
+        else value = kind.toString()
+      )
+      or
+      key = "semmle.order" and
+      value = getSuccessorIndex(predBlock, succBlock).toString()
+    )
+  )
+}
+
+query predicate parents(PrintableIRNode child, PrintableIRNode parent) {
+  parent = child.getParent()
+}
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/constant/ConstantAnalysis.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/constant/ConstantAnalysis.qll
@@ -0,0 +1,54 @@
+private import internal.ConstantAnalysisInternal
+private import semmle.code.csharp.ir.internal.IntegerPartial
+private import IR
+
+language[monotonicAggregates]
+int getConstantValue(Instruction instr) {
+  result = instr.(IntegerConstantInstruction).getValue().toInt()
+  or
+  result = getBinaryInstructionValue(instr)
+  or
+  result = neg(getConstantValue(instr.(NegateInstruction).getUnary()))
+  or
+  result = getConstantValue(instr.(CopyInstruction).getSourceValue())
+  or
+  exists(PhiInstruction phi |
+    phi = instr and
+    result = max(Operand op | op = phi.getAnInputOperand() | getConstantValue(op.getDef())) and
+    result = min(Operand op | op = phi.getAnInputOperand() | getConstantValue(op.getDef()))
+  )
+}
+
+pragma[noinline]
+private predicate binaryInstructionOperands(BinaryInstruction instr, int left, int right) {
+  left = getConstantValue(instr.getLeft()) and
+  right = getConstantValue(instr.getRight())
+}
+
+pragma[noinline]
+private int getBinaryInstructionValue(BinaryInstruction instr) {
+  exists(int left, int right |
+    binaryInstructionOperands(instr, left, right) and
+    (
+      instr instanceof AddInstruction and result = add(left, right)
+      or
+      instr instanceof SubInstruction and result = sub(left, right)
+      or
+      instr instanceof MulInstruction and result = mul(left, right)
+      or
+      instr instanceof DivInstruction and result = div(left, right)
+      or
+      instr instanceof CompareEQInstruction and result = compareEQ(left, right)
+      or
+      instr instanceof CompareNEInstruction and result = compareNE(left, right)
+      or
+      instr instanceof CompareLTInstruction and result = compareLT(left, right)
+      or
+      instr instanceof CompareGTInstruction and result = compareGT(left, right)
+      or
+      instr instanceof CompareLEInstruction and result = compareLE(left, right)
+      or
+      instr instanceof CompareGEInstruction and result = compareGE(left, right)
+    )
+  )
+}
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/constant/PrintConstantAnalysis.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/constant/PrintConstantAnalysis.qll
@@ -0,0 +1,11 @@
+private import internal.ConstantAnalysisInternal
+private import semmle.code.csharp.ir.internal.IntegerConstant
+private import ConstantAnalysis
+import IR
+
+private class ConstantAnalysisPropertyProvider extends IRPropertyProvider {
+  override string getInstructionProperty(Instruction instr, string key) {
+    key = "ConstantValue" and
+    result = getValue(getConstantValue(instr)).toString()
+  }
+}
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/constant/internal/ConstantAnalysisInternal.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/constant/internal/ConstantAnalysisInternal.qll
@@ -0,0 +1 @@
+import semmle.code.csharp.ir.implementation.unaliased_ssa.IR as IR
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/gvn/ValueNumbering.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/gvn/ValueNumbering.qll
@@ -0,0 +1,315 @@
+private import internal.ValueNumberingInternal
+private import csharp
+private import IR
+
+/**
+ * Provides additional information about value numbering in IR dumps.
+ */
+class ValueNumberPropertyProvider extends IRPropertyProvider {
+  override string getInstructionProperty(Instruction instr, string key) {
+    exists(ValueNumber vn |
+      vn = valueNumber(instr) and
+      key = "valnum" and
+      if strictcount(vn.getAnInstruction()) > 1 then result = vn.toString() else result = "unique"
+    )
+  }
+}
+
+newtype TValueNumber =
+  TVariableAddressValueNumber(IRFunction irFunc, IRVariable var) {
+    variableAddressValueNumber(_, irFunc, var)
+  } or
+  TInitializeParameterValueNumber(IRFunction irFunc, IRVariable var) {
+    initializeParameterValueNumber(_, irFunc, var)
+  } or
+  TInitializeThisValueNumber(IRFunction irFunc) { initializeThisValueNumber(_, irFunc) } or
+  TConstantValueNumber(IRFunction irFunc, Type type, string value) {
+    constantValueNumber(_, irFunc, type, value)
+  } or
+  TStringConstantValueNumber(IRFunction irFunc, Type type, string value) {
+    stringConstantValueNumber(_, irFunc, type, value)
+  } or
+  TFieldAddressValueNumber(IRFunction irFunc, Field field, ValueNumber objectAddress) {
+    fieldAddressValueNumber(_, irFunc, field, objectAddress)
+  } or
+  TBinaryValueNumber(
+    IRFunction irFunc, Opcode opcode, Type type, ValueNumber leftOperand, ValueNumber rightOperand
+  ) {
+    binaryValueNumber(_, irFunc, opcode, type, leftOperand, rightOperand)
+  } or
+  TPointerArithmeticValueNumber(
+    IRFunction irFunc, Opcode opcode, Type type, int elementSize, ValueNumber leftOperand,
+    ValueNumber rightOperand
+  ) {
+    pointerArithmeticValueNumber(_, irFunc, opcode, type, elementSize, leftOperand, rightOperand)
+  } or
+  TUnaryValueNumber(IRFunction irFunc, Opcode opcode, Type type, ValueNumber operand) {
+    unaryValueNumber(_, irFunc, opcode, type, operand)
+  } or
+  TInheritanceConversionValueNumber(
+    IRFunction irFunc, Opcode opcode, Class baseClass, Class derivedClass, ValueNumber operand
+  ) {
+    inheritanceConversionValueNumber(_, irFunc, opcode, baseClass, derivedClass, operand)
+  } or
+  TUniqueValueNumber(IRFunction irFunc, Instruction instr) { uniqueValueNumber(instr, irFunc) }
+
+/**
+ * The value number assigned to a particular set of instructions that produce equivalent results.
+ */
+class ValueNumber extends TValueNumber {
+  final string toString() { result = getExampleInstruction().getResultId() }
+
+  final Location getLocation() { result = getExampleInstruction().getLocation() }
+
+  /**
+   * Gets the instructions that have been assigned this value number. This will always produce at
+   * least one result.
+   */
+  final Instruction getAnInstruction() { this = valueNumber(result) }
+
+  /**
+   * Gets one of the instructions that was assigned this value number. The chosen instuction is
+   * deterministic but arbitrary. Intended for use only in debugging.
+   */
+  final Instruction getExampleInstruction() {
+    result = min(Instruction instr |
+        instr = getAnInstruction()
+      |
+        instr order by instr.getBlock().getDisplayIndex(), instr.getDisplayIndexInBlock()
+      )
+  }
+
+  /**
+   * Gets an `Operand` whose definition is exact and has this value number.
+   */
+  final Operand getAUse() { this = valueNumber(result.getDef()) }
+}
+
+/**
+ * A `CopyInstruction` whose source operand's value is congruent to the definition of that source
+ * operand.
+ * For example:
+ * ```
+ * Point p = { 1, 2 };
+ * Point q = p;
+ * int a = p.x;
+ * ```
+ * The use of `p` on line 2 is linked to the definition of `p` on line 1, and is congruent to that
+ * definition because it accesses the exact same memory.
+ * The use of `p.x` on line 3 is linked to the definition of `p` on line 1 as well, but is not
+ * congruent to that definition because `p.x` accesses only a subset of the memory defined by `p`.
+ */
+private class CongruentCopyInstruction extends CopyInstruction {
+  CongruentCopyInstruction() {
+    this.getSourceValueOperand().getDefinitionOverlap() instanceof MustExactlyOverlap
+  }
+}
+
+/**
+ * Holds if this library knows how to assign a value number to the specified instruction, other than
+ * a `unique` value number that is never shared by multiple instructions.
+ */
+private predicate numberableInstruction(Instruction instr) {
+  instr instanceof VariableAddressInstruction
+  or
+  instr instanceof InitializeParameterInstruction
+  or
+  instr instanceof InitializeThisInstruction
+  or
+  instr instanceof ConstantInstruction
+  or
+  instr instanceof StringConstantInstruction
+  or
+  instr instanceof FieldAddressInstruction
+  or
+  instr instanceof BinaryInstruction
+  or
+  instr instanceof UnaryInstruction and not instr instanceof CopyInstruction
+  or
+  instr instanceof PointerArithmeticInstruction
+  or
+  instr instanceof CongruentCopyInstruction
+}
+
+private predicate variableAddressValueNumber(
+  VariableAddressInstruction instr, IRFunction irFunc, IRVariable var
+) {
+  instr.getEnclosingIRFunction() = irFunc and
+  instr.getVariable() = var
+}
+
+private predicate initializeParameterValueNumber(
+  InitializeParameterInstruction instr, IRFunction irFunc, IRVariable var
+) {
+  instr.getEnclosingIRFunction() = irFunc and
+  instr.getVariable() = var
+}
+
+private predicate initializeThisValueNumber(InitializeThisInstruction instr, IRFunction irFunc) {
+  instr.getEnclosingIRFunction() = irFunc
+}
+
+private predicate constantValueNumber(
+  ConstantInstruction instr, IRFunction irFunc, Type type, string value
+) {
+  instr.getEnclosingIRFunction() = irFunc and
+  instr.getResultType() = type and
+  instr.getValue() = value
+}
+
+private predicate stringConstantValueNumber(
+  StringConstantInstruction instr, IRFunction irFunc, Type type, string value
+) {
+  instr.getEnclosingIRFunction() = irFunc and
+  instr.getResultType() = type and
+  instr.getValue().getValue() = value
+}
+
+private predicate fieldAddressValueNumber(
+  FieldAddressInstruction instr, IRFunction irFunc, Field field, ValueNumber objectAddress
+) {
+  instr.getEnclosingIRFunction() = irFunc and
+  instr.getField() = field and
+  valueNumber(instr.getObjectAddress()) = objectAddress
+}
+
+private predicate binaryValueNumber(
+  BinaryInstruction instr, IRFunction irFunc, Opcode opcode, Type type, ValueNumber leftOperand,
+  ValueNumber rightOperand
+) {
+  instr.getEnclosingIRFunction() = irFunc and
+  not instr instanceof PointerArithmeticInstruction and
+  instr.getOpcode() = opcode and
+  instr.getResultType() = type and
+  valueNumber(instr.getLeft()) = leftOperand and
+  valueNumber(instr.getRight()) = rightOperand
+}
+
+private predicate pointerArithmeticValueNumber(
+  PointerArithmeticInstruction instr, IRFunction irFunc, Opcode opcode, Type type, int elementSize,
+  ValueNumber leftOperand, ValueNumber rightOperand
+) {
+  instr.getEnclosingIRFunction() = irFunc and
+  instr.getOpcode() = opcode and
+  instr.getResultType() = type and
+  instr.getElementSize() = elementSize and
+  valueNumber(instr.getLeft()) = leftOperand and
+  valueNumber(instr.getRight()) = rightOperand
+}
+
+private predicate unaryValueNumber(
+  UnaryInstruction instr, IRFunction irFunc, Opcode opcode, Type type, ValueNumber operand
+) {
+  instr.getEnclosingIRFunction() = irFunc and
+  not instr instanceof InheritanceConversionInstruction and
+  not instr instanceof CopyInstruction and
+  instr.getOpcode() = opcode and
+  instr.getResultType() = type and
+  valueNumber(instr.getUnary()) = operand
+}
+
+private predicate inheritanceConversionValueNumber(
+  InheritanceConversionInstruction instr, IRFunction irFunc, Opcode opcode, Class baseClass,
+  Class derivedClass, ValueNumber operand
+) {
+  instr.getEnclosingIRFunction() = irFunc and
+  instr.getOpcode() = opcode and
+  instr.getBaseClass() = baseClass and
+  instr.getDerivedClass() = derivedClass and
+  valueNumber(instr.getUnary()) = operand
+}
+
+/**
+ * Holds if `instr` should be assigned a unique value number because this library does not know how
+ * to determine if two instances of that instruction are equivalent.
+ */
+private predicate uniqueValueNumber(Instruction instr, IRFunction irFunc) {
+  instr.getEnclosingIRFunction() = irFunc and
+  not instr.getResultType() instanceof VoidType and
+  not numberableInstruction(instr)
+}
+
+/**
+ * Gets the value number assigned to `instr`, if any. Returns at most one result.
+ */
+cached
+ValueNumber valueNumber(Instruction instr) {
+  result = nonUniqueValueNumber(instr)
+  or
+  exists(IRFunction irFunc |
+    uniqueValueNumber(instr, irFunc) and
+    result = TUniqueValueNumber(irFunc, instr)
+  )
+}
+
+/**
+ * Gets the value number assigned to the exact definition of `op`, if any.
+ * Returns at most one result.
+ */
+ValueNumber valueNumberOfOperand(Operand op) { result = valueNumber(op.getDef()) }
+
+/**
+ * Gets the value number assigned to `instr`, if any, unless that instruction is assigned a unique
+ * value number.
+ */
+private ValueNumber nonUniqueValueNumber(Instruction instr) {
+  exists(IRFunction irFunc |
+    irFunc = instr.getEnclosingIRFunction() and
+    (
+      exists(IRVariable var |
+        variableAddressValueNumber(instr, irFunc, var) and
+        result = TVariableAddressValueNumber(irFunc, var)
+      )
+      or
+      exists(IRVariable var |
+        initializeParameterValueNumber(instr, irFunc, var) and
+        result = TInitializeParameterValueNumber(irFunc, var)
+      )
+      or
+      initializeThisValueNumber(instr, irFunc) and
+      result = TInitializeThisValueNumber(irFunc)
+      or
+      exists(Type type, string value |
+        constantValueNumber(instr, irFunc, type, value) and
+        result = TConstantValueNumber(irFunc, type, value)
+      )
+      or
+      exists(Type type, string value |
+        stringConstantValueNumber(instr, irFunc, type, value) and
+        result = TStringConstantValueNumber(irFunc, type, value)
+      )
+      or
+      exists(Field field, ValueNumber objectAddress |
+        fieldAddressValueNumber(instr, irFunc, field, objectAddress) and
+        result = TFieldAddressValueNumber(irFunc, field, objectAddress)
+      )
+      or
+      exists(Opcode opcode, Type type, ValueNumber leftOperand, ValueNumber rightOperand |
+        binaryValueNumber(instr, irFunc, opcode, type, leftOperand, rightOperand) and
+        result = TBinaryValueNumber(irFunc, opcode, type, leftOperand, rightOperand)
+      )
+      or
+      exists(Opcode opcode, Type type, ValueNumber operand |
+        unaryValueNumber(instr, irFunc, opcode, type, operand) and
+        result = TUnaryValueNumber(irFunc, opcode, type, operand)
+      )
+      or
+      exists(Opcode opcode, Class baseClass, Class derivedClass, ValueNumber operand |
+        inheritanceConversionValueNumber(instr, irFunc, opcode, baseClass, derivedClass, operand) and
+        result = TInheritanceConversionValueNumber(irFunc, opcode, baseClass, derivedClass, operand)
+      )
+      or
+      exists(
+        Opcode opcode, Type type, int elementSize, ValueNumber leftOperand, ValueNumber rightOperand
+      |
+        pointerArithmeticValueNumber(instr, irFunc, opcode, type, elementSize, leftOperand,
+          rightOperand) and
+        result = TPointerArithmeticValueNumber(irFunc, opcode, type, elementSize, leftOperand,
+            rightOperand)
+      )
+      or
+      // The value number of a copy is just the value number of its source value.
+      result = valueNumber(instr.(CongruentCopyInstruction).getSourceValue())
+    )
+  )
+}
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/gvn/internal/ValueNumberingInternal.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/gvn/internal/ValueNumberingInternal.qll
@@ -0,0 +1 @@
+import semmle.code.csharp.ir.implementation.unaliased_ssa.IR as IR
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/AliasAnalysis.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/AliasAnalysis.qll
@@ -0,0 +1,313 @@
+private import AliasAnalysisInternal
+private import csharp
+private import InputIR
+private import semmle.code.csharp.ir.internal.IntegerConstant as Ints
+
+private class IntValue = Ints::IntValue;
+
+/**
+ * Converts the bit count in `bits` to a byte count and a bit count in the form
+ * bytes:bits.
+ */
+bindingset[bits]
+string bitsToBytesAndBits(int bits) { result = (bits / 8).toString() + ":" + (bits % 8).toString() }
+
+/**
+ * Gets a printable string for a bit offset with possibly unknown value.
+ */
+bindingset[bitOffset]
+string getBitOffsetString(IntValue bitOffset) {
+  if Ints::hasValue(bitOffset)
+  then
+    if bitOffset >= 0
+    then result = "+" + bitsToBytesAndBits(bitOffset)
+    else result = "-" + bitsToBytesAndBits(Ints::neg(bitOffset))
+  else result = "+?"
+}
+
+///**
+// * Gets the offset of field `field` in bits.
+// */
+//private IntValue getFieldBitOffset(Field field) {
+//  if field instanceof BitField
+//  then result = Ints::add(Ints::mul(field.getByteOffset(), 8), field.(BitField).getBitOffset())
+//  else result = Ints::mul(field.getByteOffset(), 8)
+//}
+/**
+ * Holds if the operand `operand` of instruction `instr` is used in a way that does
+ * not result in any address held in that operand from escaping beyond the
+ * instruction.
+ */
+private predicate operandIsConsumedWithoutEscaping(Operand operand) {
+  // The source/destination address of a Load/Store does not escape (but the
+  // loaded/stored value could).
+  operand instanceof AddressOperand
+  or
+  exists(Instruction instr |
+    instr = operand.getUse() and
+    (
+      // Neither operand of a Compare escapes.
+      instr instanceof CompareInstruction
+      or
+      // Neither operand of a PointerDiff escapes.
+      instr instanceof PointerDiffInstruction
+    )
+  )
+  or
+  // Some standard function arguments never escape
+  isNeverEscapesArgument(operand)
+}
+
+private predicate operandEscapesDomain(Operand operand) {
+  not operandIsConsumedWithoutEscaping(operand) and
+  not operandIsPropagated(operand, _) and
+  not isArgumentForParameter(_, operand, _) and
+  not isOnlyEscapesViaReturnArgument(operand) and
+  not operand.getUse() instanceof ReturnValueInstruction and
+  not operand instanceof PhiInputOperand
+}
+
+/**
+ * If the result of instruction `instr` is an integer constant, returns the
+ * value of that constant. Otherwise, returns unknown.
+ */
+IntValue getConstantValue(Instruction instr) {
+  if instr instanceof IntegerConstantInstruction
+  then result = instr.(IntegerConstantInstruction).getValue().toInt()
+  else result = Ints::unknown()
+}
+
+/**
+ * Computes the offset, in bits, by which the result of `instr` differs from the
+ * pointer argument to `instr`, if that offset is a constant. Otherwise, returns
+ * unknown.
+ */
+IntValue getPointerBitOffset(PointerOffsetInstruction instr) {
+  exists(IntValue bitOffset |
+    bitOffset = Ints::mul(Ints::mul(getConstantValue(instr.getRight()), instr.getElementSize()), 8) and
+    (
+      instr instanceof PointerAddInstruction and result = bitOffset
+      or
+      instr instanceof PointerSubInstruction and result = Ints::neg(bitOffset)
+    )
+  )
+}
+
+/**
+ * Holds if any address held in operand `operand` of instruction `instr` is
+ * propagated to the result of `instr`, offset by the number of bits in
+ * `bitOffset`. If the address is propagated, but the offset is not known to be
+ * a constant, then `bitOffset` is unknown.
+ */
+private predicate operandIsPropagated(Operand operand, IntValue bitOffset) {
+  exists(Instruction instr |
+    instr = operand.getUse() and
+    (
+      // REVIEW: See the REVIEW comment bellow
+      //      // Converting to a non-virtual base class adds the offset of the base class.
+      //      exists(ConvertToBaseInstruction convert |
+      //        convert = instr and
+      //        bitOffset = Ints::mul(convert.getDerivation().getByteOffset(), 8)
+      //      )
+      //      or
+      //      // Converting to a derived class subtracts the offset of the base class.
+      //      exists(ConvertToDerivedInstruction convert |
+      //        convert = instr and
+      //        bitOffset = Ints::neg(Ints::mul(convert.getDerivation().getByteOffset(), 8))
+      //      )
+      //      or
+      //      // Converting to a virtual base class adds an unknown offset.
+      //      instr instanceof ConvertToVirtualBaseInstruction and
+      //      bitOffset = Ints::unknown()
+      //      or
+      // REVIEW: In the C# IR, we should ignore the above types of conversion all together,
+      //         since first of all they do not provide correct information (nothing is known
+      //         for sure about heap allocated objects) and second of all even if we create a
+      //         virtual memory model for the IR I don't think such conversions provide any meaningful
+      //         information;
+      // Conversion to another pointer type propagates the source address.
+      exists(ConvertInstruction convert, Type resultType |
+        convert = instr and
+        resultType = convert.getResultType() and
+        (
+          resultType instanceof PointerType or
+          resultType instanceof RefType
+        ) and
+        bitOffset = 0
+      )
+      or
+      // Adding an integer to or subtracting an integer from a pointer propagates
+      // the address with an offset.
+      bitOffset = getPointerBitOffset(instr.(PointerOffsetInstruction))
+      or
+      // Computing a field address from a pointer propagates the address plus the
+      // offset of the field.
+      // TODO: Fix once class layout is synthesized
+      // bitOffset = Ints::unknown()
+      //or
+      // A copy propagates the source value.
+      operand = instr.(CopyInstruction).getSourceValueOperand() and bitOffset = 0
+      or
+      // Some functions are known to propagate an argument
+      isAlwaysReturnedArgument(operand) and bitOffset = 0
+    )
+  )
+}
+
+private predicate operandEscapesNonReturn(Operand operand) {
+  // The address is propagated to the result of the instruction, and that result itself is returned
+  operandIsPropagated(operand, _) and resultEscapesNonReturn(operand.getUse())
+  or
+  // The operand is used in a function call which returns it, and the return value is then returned
+  exists(CallInstruction ci, Instruction init |
+    isArgumentForParameter(ci, operand, init) and
+    (
+      resultMayReachReturn(init) and
+      resultEscapesNonReturn(ci)
+      or
+      resultEscapesNonReturn(init)
+    )
+  )
+  or
+  isOnlyEscapesViaReturnArgument(operand) and resultEscapesNonReturn(operand.getUse())
+  or
+  operand instanceof PhiInputOperand and
+  resultEscapesNonReturn(operand.getUse())
+  or
+  operandEscapesDomain(operand)
+}
+
+private predicate operandMayReachReturn(Operand operand) {
+  // The address is propagated to the result of the instruction, and that result itself is returned
+  operandIsPropagated(operand, _) and
+  resultMayReachReturn(operand.getUse())
+  or
+  // The operand is used in a function call which returns it, and the return value is then returned
+  exists(CallInstruction ci, Instruction init |
+    isArgumentForParameter(ci, operand, init) and
+    resultMayReachReturn(init) and
+    resultMayReachReturn(ci)
+  )
+  or
+  // The address is returned
+  operand.getUse() instanceof ReturnValueInstruction
+  or
+  isOnlyEscapesViaReturnArgument(operand) and resultMayReachReturn(operand.getUse())
+  or
+  operand instanceof PhiInputOperand and
+  resultMayReachReturn(operand.getUse())
+}
+
+private predicate operandReturned(Operand operand, IntValue bitOffset) {
+  // The address is propagated to the result of the instruction, and that result itself is returned
+  exists(IntValue bitOffset1, IntValue bitOffset2 |
+    operandIsPropagated(operand, bitOffset1) and
+    resultReturned(operand.getUse(), bitOffset2) and
+    bitOffset = Ints::add(bitOffset1, bitOffset2)
+  )
+  or
+  // The operand is used in a function call which returns it, and the return value is then returned
+  exists(CallInstruction ci, Instruction init, IntValue bitOffset1, IntValue bitOffset2 |
+    isArgumentForParameter(ci, operand, init) and
+    resultReturned(init, bitOffset1) and
+    resultReturned(ci, bitOffset2) and
+    bitOffset = Ints::add(bitOffset1, bitOffset2)
+  )
+  or
+  // The address is returned
+  operand.getUse() instanceof ReturnValueInstruction and
+  bitOffset = 0
+  or
+  isOnlyEscapesViaReturnArgument(operand) and
+  resultReturned(operand.getUse(), _) and
+  bitOffset = Ints::unknown()
+}
+
+private predicate isArgumentForParameter(CallInstruction ci, Operand operand, Instruction init) {
+  exists(Callable c |
+    ci = operand.getUse() and
+    c = ci.getStaticCallTarget() and
+    (
+      init.(InitializeParameterInstruction).getParameter() = c
+            .getParameter(operand.(PositionalArgumentOperand).getIndex())
+      or
+      init instanceof InitializeThisInstruction and
+      init.getEnclosingFunction() = c and
+      operand instanceof ThisArgumentOperand
+    ) // and
+    //    not f.isVirtual() and
+    //    not f instanceof AliasFunction
+  )
+}
+
+private predicate isAlwaysReturnedArgument(Operand operand) { none() }
+
+private predicate isOnlyEscapesViaReturnArgument(Operand operand) { none() }
+
+private predicate isNeverEscapesArgument(Operand operand) { none() }
+
+private predicate resultReturned(Instruction instr, IntValue bitOffset) {
+  operandReturned(instr.getAUse(), bitOffset)
+}
+
+private predicate resultMayReachReturn(Instruction instr) { operandMayReachReturn(instr.getAUse()) }
+
+/**
+ * Holds if any address held in the result of instruction `instr` escapes
+ * outside the domain of the analysis.
+ */
+private predicate resultEscapesNonReturn(Instruction instr) {
+  // The result escapes if it has at least one use that escapes.
+  operandEscapesNonReturn(instr.getAUse())
+}
+
+/**
+ * Holds if the address of the specified local variable or parameter escapes the
+ * domain of the analysis.
+ */
+private predicate automaticVariableAddressEscapes(IRAutomaticVariable var) {
+  // The variable's address escapes if the result of any
+  // VariableAddressInstruction that computes the variable's address escapes.
+  exists(VariableAddressInstruction instr |
+    instr.getVariable() = var and
+    resultEscapesNonReturn(instr)
+  )
+}
+
+/**
+ * Holds if the address of the specified variable escapes the domain of the
+ * analysis.
+ */
+predicate variableAddressEscapes(IRVariable var) {
+  automaticVariableAddressEscapes(var.(IRAutomaticVariable))
+  or
+  // All variables with static storage duration have their address escape.
+  not var instanceof IRAutomaticVariable
+}
+
+/**
+ * Holds if the result of instruction `instr` points within variable `var`, at
+ * bit offset `bitOffset` within the variable. If the result points within
+ * `var`, but at an unknown or non-constant offset, then `bitOffset` is unknown.
+ */
+predicate resultPointsTo(Instruction instr, IRVariable var, IntValue bitOffset) {
+  // The address of a variable points to that variable, at offset 0.
+  instr.(VariableAddressInstruction).getVariable() = var and
+  bitOffset = 0
+  or
+  exists(Operand operand, IntValue originalBitOffset, IntValue propagatedBitOffset |
+    operand = instr.getAnOperand() and
+    // If an operand is propagated, then the result points to the same variable,
+    // offset by the bit offset from the propagation.
+    resultPointsTo(operand.getAnyDef(), var, originalBitOffset) and
+    (
+      operandIsPropagated(operand, propagatedBitOffset)
+      or
+      exists(CallInstruction ci, Instruction init |
+        isArgumentForParameter(ci, operand, init) and
+        resultReturned(init, propagatedBitOffset)
+      )
+    ) and
+    bitOffset = Ints::add(originalBitOffset, propagatedBitOffset)
+  )
+}
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/AliasAnalysisInternal.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/AliasAnalysisInternal.qll
@@ -0,0 +1 @@
+import semmle.code.csharp.ir.implementation.raw.IR as InputIR
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/IRBlockImports.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/IRBlockImports.qll
@@ -0,0 +1 @@
+import semmle.code.csharp.ir.implementation.EdgeKind as EdgeKind
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/IRImports.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/IRImports.qll
@@ -0,0 +1,2 @@
+import semmle.code.csharp.ir.implementation.EdgeKind as EdgeKind
+import semmle.code.csharp.ir.implementation.MemoryAccessKind as MemoryAccessKind
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/IRInternal.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/IRInternal.qll
@@ -0,0 +1,2 @@
+import semmle.code.csharp.ir.internal.IRCSharpLanguage as Language
+import SSAConstruction as Construction
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/IRVariableImports.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/IRVariableImports.qll
@@ -0,0 +1,4 @@
+import semmle.code.csharp.ir.implementation.TempVariableTag as TempVariableTag
+import semmle.code.csharp.ir.internal.IRUtilities as IRUtilities
+import semmle.code.csharp.ir.internal.TempVariableTag as TTempVariableTag
+import semmle.code.csharp.ir.implementation.internal.TIRVariable as TIRVariable
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/InstructionImports.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/InstructionImports.qll
@@ -0,0 +1,4 @@
+import semmle.code.csharp.ir.implementation.EdgeKind as EdgeKind
+import semmle.code.csharp.ir.implementation.MemoryAccessKind as MemoryAccessKind
+import semmle.code.csharp.ir.implementation.Opcode as Opcode
+import semmle.code.csharp.ir.implementation.internal.OperandTag as OperandTag
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/OperandImports.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/OperandImports.qll
@@ -0,0 +1,3 @@
+import semmle.code.csharp.ir.implementation.MemoryAccessKind as MemoryAccessKind
+import semmle.code.csharp.ir.internal.Overlap as Overlap
+import semmle.code.csharp.ir.implementation.internal.OperandTag as OperandTag
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/PrintIRImports.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/PrintIRImports.qll
@@ -0,0 +1 @@
+import semmle.code.csharp.ir.IRConfiguration as IRConfiguration
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/PrintSSA.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/PrintSSA.qll
@@ -0,0 +1,126 @@
+private import SSAConstructionInternal
+private import OldIR
+private import Alias
+private import SSAConstruction
+private import DebugSSA
+
+/**
+ * Property provide that dumps the memory access of each result. Useful for debugging SSA
+ * construction.
+ */
+class PropertyProvider extends IRPropertyProvider {
+  override string getInstructionProperty(Instruction instruction, string key) {
+    exists(MemoryLocation location |
+      location = getResultMemoryLocation(instruction) and
+      (
+        key = "ResultMemoryLocation" and result = location.toString()
+        or
+        key = "ResultVirtualVariable" and result = location.getVirtualVariable().toString()
+      )
+    )
+    or
+    exists(MemoryLocation location |
+      location = getOperandMemoryLocation(instruction.getAnOperand()) and
+      (
+        key = "OperandMemoryAccess" and result = location.toString()
+        or
+        key = "OperandVirtualVariable" and result = location.getVirtualVariable().toString()
+      )
+    )
+    or
+    exists(MemoryLocation useLocation, IRBlock defBlock, int defRank, int defIndex |
+      hasDefinitionAtRank(useLocation, _, defBlock, defRank, defIndex) and
+      defBlock.getInstruction(defIndex) = instruction and
+      key = "DefinitionRank[" + useLocation.toString() + "]" and
+      result = defRank.toString()
+    )
+    or
+    exists(MemoryLocation useLocation, IRBlock useBlock, int useRank |
+      hasUseAtRank(useLocation, useBlock, useRank, instruction) and
+      key = "UseRank[" + useLocation.toString() + "]" and
+      result = useRank.toString()
+    )
+    or
+    exists(MemoryLocation useLocation, IRBlock defBlock, int defRank, int defIndex |
+      hasDefinitionAtRank(useLocation, _, defBlock, defRank, defIndex) and
+      defBlock.getInstruction(defIndex) = instruction and
+      key = "DefinitionReachesUse[" + useLocation.toString() + "]" and
+      result = strictconcat(IRBlock useBlock, int useRank, int useIndex |
+          exists(Instruction useInstruction |
+            hasUseAtRank(useLocation, useBlock, useRank, useInstruction) and
+            useBlock.getInstruction(useIndex) = useInstruction and
+            definitionReachesUse(useLocation, defBlock, defRank, useBlock, useRank)
+          )
+        |
+          useBlock.getDisplayIndex().toString() + "_" + useIndex, ", "
+          order by
+            useBlock.getDisplayIndex(), useIndex
+        )
+    )
+  }
+
+  override string getBlockProperty(IRBlock block, string key) {
+    exists(MemoryLocation useLocation, int defRank, int defIndex |
+      hasDefinitionAtRank(useLocation, _, block, defRank, defIndex) and
+      defIndex = -1 and
+      key = "DefinitionRank(Phi)[" + useLocation.toString() + "]" and
+      result = defRank.toString()
+    )
+    or
+    exists(MemoryLocation useLocation, MemoryLocation defLocation, int defRank, int defIndex |
+      hasDefinitionAtRank(useLocation, defLocation, block, defRank, defIndex) and
+      defIndex = -1 and
+      key = "DefinitionReachesUse(Phi)[" + useLocation.toString() + "]" and
+      result = strictconcat(IRBlock useBlock, int useRank, int useIndex |
+          exists(Instruction useInstruction |
+            hasUseAtRank(useLocation, useBlock, useRank, useInstruction) and
+            useBlock.getInstruction(useIndex) = useInstruction and
+            definitionReachesUse(useLocation, block, defRank, useBlock, useRank) and
+            exists(getOverlap(defLocation, useLocation))
+          )
+        |
+          useBlock.getDisplayIndex().toString() + "_" + useIndex, ", "
+          order by
+            useBlock.getDisplayIndex(), useIndex
+        )
+    )
+    or
+    exists(
+      MemoryLocation useLocation, IRBlock predBlock, IRBlock defBlock, int defIndex, Overlap overlap
+    |
+      hasPhiOperandDefinition(_, useLocation, block, predBlock, defBlock, defIndex, overlap) and
+      key = "PhiUse[" + useLocation.toString() + " from " + predBlock.getDisplayIndex().toString() +
+          "]" and
+      result = defBlock.getDisplayIndex().toString() + "_" + defIndex + " (" + overlap.toString() +
+          ")"
+    )
+    or
+    key = "LiveOnEntry" and
+    result = strictconcat(MemoryLocation useLocation |
+        locationLiveOnEntryToBlock(useLocation, block)
+      |
+        useLocation.toString(), ", " order by useLocation.toString()
+      )
+    or
+    key = "LiveOnExit" and
+    result = strictconcat(MemoryLocation useLocation |
+        locationLiveOnExitFromBlock(useLocation, block)
+      |
+        useLocation.toString(), ", " order by useLocation.toString()
+      )
+    or
+    key = "DefsLiveOnEntry" and
+    result = strictconcat(MemoryLocation defLocation |
+        definitionLiveOnEntryToBlock(defLocation, block)
+      |
+        defLocation.toString(), ", " order by defLocation.toString()
+      )
+    or
+    key = "DefsLiveOnExit" and
+    result = strictconcat(MemoryLocation defLocation |
+        definitionLiveOnExitFromBlock(defLocation, block)
+      |
+        defLocation.toString(), ", " order by defLocation.toString()
+      )
+  }
+}
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/SSAConstruction.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/SSAConstruction.qll
@@ -0,0 +1,886 @@
+import SSAConstructionInternal
+private import semmle.code.csharp.ir.implementation.Opcode
+private import semmle.code.csharp.ir.implementation.internal.OperandTag
+private import semmle.code.csharp.ir.internal.Overlap
+private import NewIR
+private import semmle.code.csharp.ir.internal.IRCSharpLanguage as Language
+
+private class OldBlock = Reachability::ReachableBlock;
+
+private class OldInstruction = Reachability::ReachableInstruction;
+
+import Cached
+
+cached
+private module Cached {
+  private IRBlock getNewBlock(OldBlock oldBlock) {
+    result.getFirstInstruction() = getNewInstruction(oldBlock.getFirstInstruction())
+  }
+
+  cached
+  predicate functionHasIR(Language::Function func) {
+    exists(OldIR::IRFunction irFunc | irFunc.getFunction() = func)
+  }
+
+  cached
+  OldInstruction getOldInstruction(Instruction instr) { instr = WrappedInstruction(result) }
+
+  private IRVariable getNewIRVariable(OldIR::IRVariable var) {
+    // This is just a type cast. Both classes derive from the same newtype.
+    result = var
+  }
+
+  cached
+  newtype TInstruction =
+    WrappedInstruction(OldInstruction oldInstruction) {
+      not oldInstruction instanceof OldIR::PhiInstruction
+    } or
+    Phi(OldBlock block, Alias::MemoryLocation defLocation) {
+      definitionHasPhiNode(defLocation, block)
+    } or
+    Chi(OldInstruction oldInstruction) {
+      not oldInstruction instanceof OldIR::PhiInstruction and
+      hasChiNode(_, oldInstruction)
+    } or
+    Unreached(Language::Function function) {
+      exists(OldInstruction oldInstruction |
+        function = oldInstruction.getEnclosingFunction() and
+        Reachability::isInfeasibleInstructionSuccessor(oldInstruction, _)
+      )
+    }
+
+  cached
+  predicate hasTempVariable(
+    Language::Function func, Language::AST ast, TempVariableTag tag, Language::Type type
+  ) {
+    exists(OldIR::IRTempVariable var |
+      var.getEnclosingFunction() = func and
+      var.getAST() = ast and
+      var.getTag() = tag and
+      var.getType() = type
+    )
+  }
+
+  cached
+  predicate hasModeledMemoryResult(Instruction instruction) {
+    exists(Alias::getResultMemoryLocation(getOldInstruction(instruction))) or
+    instruction instanceof PhiInstruction or // Phis always have modeled results
+    instruction instanceof ChiInstruction // Chis always have modeled results
+  }
+
+  cached
+  Instruction getRegisterOperandDefinition(Instruction instruction, RegisterOperandTag tag) {
+    exists(OldInstruction oldInstruction, OldIR::RegisterOperand oldOperand |
+      oldInstruction = getOldInstruction(instruction) and
+      oldOperand = oldInstruction.getAnOperand() and
+      tag = oldOperand.getOperandTag() and
+      result = getNewInstruction(oldOperand.getAnyDef())
+    )
+  }
+
+  cached
+  Instruction getMemoryOperandDefinition(
+    Instruction instruction, MemoryOperandTag tag, Overlap overlap
+  ) {
+    exists(OldInstruction oldInstruction, OldIR::NonPhiMemoryOperand oldOperand |
+      oldInstruction = getOldInstruction(instruction) and
+      oldOperand = oldInstruction.getAnOperand() and
+      tag = oldOperand.getOperandTag() and
+      (
+        (
+          if exists(Alias::getOperandMemoryLocation(oldOperand))
+          then
+            exists(
+              OldBlock useBlock, int useRank, Alias::MemoryLocation useLocation,
+              Alias::MemoryLocation defLocation, OldBlock defBlock, int defRank, int defOffset
+            |
+              useLocation = Alias::getOperandMemoryLocation(oldOperand) and
+              hasDefinitionAtRank(useLocation, defLocation, defBlock, defRank, defOffset) and
+              hasUseAtRank(useLocation, useBlock, useRank, oldInstruction) and
+              definitionReachesUse(useLocation, defBlock, defRank, useBlock, useRank) and
+              overlap = Alias::getOverlap(defLocation, useLocation) and
+              result = getDefinitionOrChiInstruction(defBlock, defOffset, defLocation)
+            )
+          else (
+            result = instruction.getEnclosingIRFunction().getUnmodeledDefinitionInstruction() and
+            overlap instanceof MustTotallyOverlap
+          )
+        )
+        or
+        // Connect any definitions that are not being modeled in SSA to the
+        // `UnmodeledUse` instruction.
+        exists(OldInstruction oldDefinition |
+          instruction instanceof UnmodeledUseInstruction and
+          tag instanceof UnmodeledUseOperandTag and
+          oldDefinition = oldOperand.getAnyDef() and
+          not exists(Alias::getResultMemoryLocation(oldDefinition)) and
+          result = getNewInstruction(oldDefinition) and
+          overlap instanceof MustTotallyOverlap
+        )
+      )
+    )
+    or
+    instruction = Chi(getOldInstruction(result)) and
+    tag instanceof ChiPartialOperandTag and
+    overlap instanceof MustExactlyOverlap
+    or
+    exists(IRFunction f |
+      tag instanceof UnmodeledUseOperandTag and
+      result = f.getUnmodeledDefinitionInstruction() and
+      instruction = f.getUnmodeledUseInstruction() and
+      overlap instanceof MustTotallyOverlap
+    )
+    or
+    tag instanceof ChiTotalOperandTag and
+    result = getChiInstructionTotalOperand(instruction) and
+    overlap instanceof MustExactlyOverlap
+  }
+
+  cached
+  Language::Type getInstructionOperandType(Instruction instr, TypedOperandTag tag) {
+    exists(OldInstruction oldInstruction, OldIR::TypedOperand oldOperand |
+      oldInstruction = getOldInstruction(instr) and
+      oldOperand = oldInstruction.getAnOperand() and
+      tag = oldOperand.getOperandTag() and
+      result = oldOperand.getType()
+    )
+  }
+
+  cached
+  int getInstructionOperandSize(Instruction instr, SideEffectOperandTag tag) {
+    exists(OldInstruction oldInstruction, OldIR::SideEffectOperand oldOperand |
+      oldInstruction = getOldInstruction(instr) and
+      oldOperand = oldInstruction.getAnOperand() and
+      tag = oldOperand.getOperandTag() and
+      // Only return a result for operands that need an explicit result size.
+      oldOperand.getType() instanceof Language::UnknownType and
+      result = oldOperand.getSize()
+    )
+  }
+
+  cached
+  Instruction getPhiOperandDefinition(
+    PhiInstruction instr, IRBlock newPredecessorBlock, Overlap overlap
+  ) {
+    exists(
+      Alias::MemoryLocation defLocation, Alias::MemoryLocation useLocation, OldBlock phiBlock,
+      OldBlock predBlock, OldBlock defBlock, int defOffset
+    |
+      hasPhiOperandDefinition(defLocation, useLocation, phiBlock, predBlock, defBlock, defOffset,
+        overlap) and
+      instr = Phi(phiBlock, useLocation) and
+      newPredecessorBlock = getNewBlock(predBlock) and
+      result = getDefinitionOrChiInstruction(defBlock, defOffset, defLocation)
+    )
+  }
+
+  cached
+  Instruction getChiInstructionTotalOperand(ChiInstruction chiInstr) {
+    exists(
+      Alias::VirtualVariable vvar, OldInstruction oldInstr, Alias::MemoryLocation defLocation,
+      OldBlock defBlock, int defRank, int defOffset, OldBlock useBlock, int useRank
+    |
+      chiInstr = Chi(oldInstr) and
+      vvar = Alias::getResultMemoryLocation(oldInstr).getVirtualVariable() and
+      hasDefinitionAtRank(vvar, defLocation, defBlock, defRank, defOffset) and
+      hasUseAtRank(vvar, useBlock, useRank, oldInstr) and
+      definitionReachesUse(vvar, defBlock, defRank, useBlock, useRank) and
+      result = getDefinitionOrChiInstruction(defBlock, defOffset, vvar)
+    )
+  }
+
+  cached
+  Instruction getPhiInstructionBlockStart(PhiInstruction instr) {
+    exists(OldBlock oldBlock |
+      instr = Phi(oldBlock, _) and
+      result = getNewInstruction(oldBlock.getFirstInstruction())
+    )
+  }
+
+  cached
+  Language::Expr getInstructionConvertedResultExpression(Instruction instruction) {
+    result = getOldInstruction(instruction).getConvertedResultExpression()
+  }
+
+  cached
+  Language::Expr getInstructionUnconvertedResultExpression(Instruction instruction) {
+    result = getOldInstruction(instruction).getUnconvertedResultExpression()
+  }
+
+  /*
+   * This adds Chi nodes to the instruction successor relation; if an instruction has a Chi node,
+   * that node is its successor in the new successor relation, and the Chi node's successors are
+   * the new instructions generated from the successors of the old instruction
+   */
+
+  cached
+  Instruction getInstructionSuccessor(Instruction instruction, EdgeKind kind) {
+    if hasChiNode(_, getOldInstruction(instruction))
+    then
+      result = Chi(getOldInstruction(instruction)) and
+      kind instanceof GotoEdge
+    else (
+      exists(OldInstruction oldInstruction |
+        oldInstruction = getOldInstruction(instruction) and
+        (
+          if Reachability::isInfeasibleInstructionSuccessor(oldInstruction, kind)
+          then result = Unreached(instruction.getEnclosingFunction())
+          else result = getNewInstruction(oldInstruction.getSuccessor(kind))
+        )
+      )
+      or
+      exists(OldInstruction oldInstruction |
+        instruction = Chi(oldInstruction) and
+        result = getNewInstruction(oldInstruction.getSuccessor(kind))
+      )
+    )
+  }
+
+  cached
+  Instruction getInstructionBackEdgeSuccessor(Instruction instruction, EdgeKind kind) {
+    exists(OldInstruction oldInstruction |
+      not Reachability::isInfeasibleInstructionSuccessor(oldInstruction, kind) and
+      // There is only one case for the translation into `result` because the
+      // SSA construction never inserts extra instructions _before_ an existing
+      // instruction.
+      getOldInstruction(result) = oldInstruction.getBackEdgeSuccessor(kind) and
+      // There are two cases for the translation into `instruction` because the
+      // SSA construction might have inserted a chi node _after_
+      // `oldInstruction`, in which case the back edge should come out of the
+      // chi node instead.
+      if hasChiNode(_, oldInstruction)
+      then instruction = Chi(oldInstruction)
+      else instruction = getNewInstruction(oldInstruction)
+    )
+  }
+
+  cached
+  Language::AST getInstructionAST(Instruction instruction) {
+    exists(OldInstruction oldInstruction |
+      instruction = WrappedInstruction(oldInstruction)
+      or
+      instruction = Chi(oldInstruction)
+    |
+      result = oldInstruction.getAST()
+    )
+    or
+    exists(OldBlock block |
+      instruction = Phi(block, _) and
+      result = block.getFirstInstruction().getAST()
+    )
+    or
+    instruction = Unreached(result)
+  }
+
+  cached
+  predicate instructionHasType(Instruction instruction, Language::Type type, boolean isGLValue) {
+    exists(OldInstruction oldInstruction |
+      instruction = WrappedInstruction(oldInstruction) and
+      type = oldInstruction.getResultType() and
+      if oldInstruction.isGLValue() then isGLValue = true else isGLValue = false
+    )
+    or
+    exists(OldInstruction oldInstruction, Alias::VirtualVariable vvar |
+      instruction = Chi(oldInstruction) and
+      hasChiNode(vvar, oldInstruction) and
+      type = vvar.getType() and
+      isGLValue = false
+    )
+    or
+    exists(Alias::MemoryLocation location |
+      instruction = Phi(_, location) and
+      type = location.getType() and
+      isGLValue = false
+    )
+    or
+    instruction = Unreached(_) and
+    type instanceof Language::VoidType and
+    isGLValue = false
+  }
+
+  cached
+  Opcode getInstructionOpcode(Instruction instruction) {
+    exists(OldInstruction oldInstruction |
+      instruction = WrappedInstruction(oldInstruction) and
+      result = oldInstruction.getOpcode()
+    )
+    or
+    instruction instanceof Chi and
+    result instanceof Opcode::Chi
+    or
+    instruction instanceof Phi and
+    result instanceof Opcode::Phi
+    or
+    instruction instanceof Unreached and
+    result instanceof Opcode::Unreached
+  }
+
+  cached
+  IRFunction getInstructionEnclosingIRFunction(Instruction instruction) {
+    exists(OldInstruction oldInstruction |
+      instruction = WrappedInstruction(oldInstruction)
+      or
+      instruction = Chi(oldInstruction)
+    |
+      result.getFunction() = oldInstruction.getEnclosingFunction()
+    )
+    or
+    exists(OldBlock block |
+      instruction = Phi(block, _) and
+      result.getFunction() = block.getEnclosingFunction()
+    )
+    or
+    instruction = Unreached(result.getFunction())
+  }
+
+  cached
+  IRVariable getInstructionVariable(Instruction instruction) {
+    result = getNewIRVariable(getOldInstruction(instruction)
+            .(OldIR::VariableInstruction)
+            .getVariable())
+  }
+
+  cached
+  Language::Field getInstructionField(Instruction instruction) {
+    result = getOldInstruction(instruction).(OldIR::FieldInstruction).getField()
+  }
+
+  cached
+  Language::Function getInstructionFunction(Instruction instruction) {
+    result = getOldInstruction(instruction).(OldIR::FunctionInstruction).getFunctionSymbol()
+  }
+
+  cached
+  string getInstructionConstantValue(Instruction instruction) {
+    result = getOldInstruction(instruction).(OldIR::ConstantValueInstruction).getValue()
+  }
+
+  cached
+  Language::StringLiteral getInstructionStringLiteral(Instruction instruction) {
+    result = getOldInstruction(instruction).(OldIR::StringConstantInstruction).getValue()
+  }
+
+  cached
+  Language::BuiltInOperation getInstructionBuiltInOperation(Instruction instruction) {
+    result = getOldInstruction(instruction)
+          .(OldIR::BuiltInOperationInstruction)
+          .getBuiltInOperation()
+  }
+
+  cached
+  Language::Type getInstructionExceptionType(Instruction instruction) {
+    result = getOldInstruction(instruction).(OldIR::CatchByTypeInstruction).getExceptionType()
+  }
+
+  cached
+  int getInstructionElementSize(Instruction instruction) {
+    result = getOldInstruction(instruction).(OldIR::PointerArithmeticInstruction).getElementSize()
+  }
+
+  cached
+  int getInstructionResultSize(Instruction instruction) {
+    // Only return a result for instructions that needed an explicit result size.
+    instruction.getResultType() instanceof Language::UnknownType and
+    result = getOldInstruction(instruction).getResultSize()
+  }
+
+  cached
+  predicate getInstructionInheritance(
+    Instruction instruction, Language::Class baseClass, Language::Class derivedClass
+  ) {
+    exists(OldIR::InheritanceConversionInstruction oldInstr |
+      oldInstr = getOldInstruction(instruction) and
+      baseClass = oldInstr.getBaseClass() and
+      derivedClass = oldInstr.getDerivedClass()
+    )
+  }
+
+  cached
+  Instruction getPrimaryInstructionForSideEffect(Instruction instruction) {
+    exists(OldIR::SideEffectInstruction oldInstruction |
+      oldInstruction = getOldInstruction(instruction) and
+      result = getNewInstruction(oldInstruction.getPrimaryInstruction())
+    )
+    or
+    exists(OldIR::Instruction oldInstruction |
+      instruction = Chi(oldInstruction) and
+      result = getNewInstruction(oldInstruction)
+    )
+  }
+}
+
+private Instruction getNewInstruction(OldInstruction instr) { getOldInstruction(result) = instr }
+
+/**
+ * Holds if instruction `def` needs to have a `Chi` instruction inserted after it, to account for a partial definition
+ * of a virtual variable. The `Chi` instruction provides a definition of the entire virtual variable of which the
+ * original definition location is a member.
+ */
+private predicate hasChiNode(Alias::VirtualVariable vvar, OldInstruction def) {
+  exists(Alias::MemoryLocation defLocation |
+    defLocation = Alias::getResultMemoryLocation(def) and
+    defLocation.getVirtualVariable() = vvar and
+    // If the definition totally (or exactly) overlaps the virtual variable, then there's no need for a `Chi`
+    // instruction.
+    Alias::getOverlap(defLocation, vvar) instanceof MayPartiallyOverlap
+  )
+}
+
+private import PhiInsertion
+
+/**
+ * Module to handle insertion of `Phi` instructions at the correct blocks. We insert a `Phi` instruction at the
+ * beginning of a block for a given location when that block is on the dominance frontier of a definition of the
+ * location and there is a use of that location reachable from that block without an intervening definition of the
+ * location.
+ * Within the approach outlined above, we treat a location slightly differently depending on whether or not it is a
+ * virtual variable. For a virtual variable, we will insert a `Phi` instruction on the dominance frontier if there is
+ * a use of any member location of that virtual variable that is reachable from the `Phi` instruction. For a location
+ * that is not a virtual variable, we insert a `Phi` instruction only if there is an exactly-overlapping use of the
+ * location reachable from the `Phi` instruction. This ensures that we insert a `Phi` instruction for a non-virtual
+ * variable only if doing so would allow dataflow analysis to get a more precise result than if we just used a `Phi`
+ * instruction for the virtual variable as a whole.
+ */
+private module PhiInsertion {
+  /**
+   * Holds if a `Phi` instruction needs to be inserted for location `defLocation` at the beginning of block `phiBlock`.
+   */
+  predicate definitionHasPhiNode(Alias::MemoryLocation defLocation, OldBlock phiBlock) {
+    exists(OldBlock defBlock |
+      phiBlock = Dominance::getDominanceFrontier(defBlock) and
+      definitionHasDefinitionInBlock(defLocation, defBlock) and
+      /* We can also eliminate those nodes where the definition is not live on any incoming edge */
+      definitionLiveOnEntryToBlock(defLocation, phiBlock)
+    )
+  }
+
+  /**
+   * Holds if the memory location `defLocation` has a definition in block `block`, either because of an existing
+   * instruction, a `Phi` node, or a `Chi` node.
+   */
+  private predicate definitionHasDefinitionInBlock(Alias::MemoryLocation defLocation, OldBlock block) {
+    definitionHasPhiNode(defLocation, block)
+    or
+    exists(OldInstruction def, Alias::MemoryLocation resultLocation |
+      def.getBlock() = block and
+      resultLocation = Alias::getResultMemoryLocation(def) and
+      (
+        defLocation = resultLocation
+        or
+        // For a virtual variable, any definition of a member location will either generate a `Chi` node that defines
+        // the virtual variable, or will totally overlap the virtual variable. Either way, treat this as a definition of
+        // the virtual variable.
+        defLocation = resultLocation.getVirtualVariable()
+      )
+    )
+  }
+
+  /**
+   * Holds if there is a use at (`block`, `index`) that could consume the result of a `Phi` instruction for
+   * `defLocation`.
+   */
+  private predicate definitionHasUse(Alias::MemoryLocation defLocation, OldBlock block, int index) {
+    exists(OldInstruction use |
+      block.getInstruction(index) = use and
+      if defLocation instanceof Alias::VirtualVariable
+      then (
+        exists(Alias::MemoryLocation useLocation |
+          // For a virtual variable, any use of a location that is a member of the virtual variable counts as a use.
+          useLocation = Alias::getOperandMemoryLocation(use.getAnOperand()) and
+          defLocation = useLocation.getVirtualVariable()
+        )
+        or
+        // A `Chi` instruction consumes the enclosing virtual variable of its use location.
+        hasChiNode(defLocation, use)
+      ) else (
+        // For other locations, only an exactly-overlapping use of the same location counts as a use.
+        defLocation = Alias::getOperandMemoryLocation(use.getAnOperand()) and
+        Alias::getOverlap(defLocation, defLocation) instanceof MustExactlyOverlap
+      )
+    )
+  }
+
+  /**
+   * Holds if the location `defLocation` is redefined at (`block`, `index`). A location is considered "redefined" if
+   * there is a definition that would prevent a previous definition of `defLocation` from being consumed as the operand
+   * of a `Phi` node that occurs after the redefinition.
+   */
+  private predicate definitionHasRedefinition(
+    Alias::MemoryLocation defLocation, OldBlock block, int index
+  ) {
+    exists(OldInstruction redef, Alias::MemoryLocation redefLocation |
+      block.getInstruction(index) = redef and
+      redefLocation = Alias::getResultMemoryLocation(redef) and
+      if defLocation instanceof Alias::VirtualVariable
+      then
+        // For a virtual variable, the definition may be consumed by any use of a location that is a member of the
+        // virtual variable. Thus, the definition is live until a subsequent redefinition of the entire virtual
+        // variable.
+        exists(Overlap overlap |
+          overlap = Alias::getOverlap(redefLocation, defLocation) and
+          not overlap instanceof MayPartiallyOverlap
+        )
+      else
+        // For other locations, the definition may only be consumed by an exactly-overlapping use of the same location.
+        // Thus, the definition is live until a subsequent definition of any location that may overlap the original
+        // definition location.
+        exists(Alias::getOverlap(redefLocation, defLocation))
+    )
+  }
+
+  /**
+   * Holds if the definition `defLocation` is live on entry to block `block`. The definition is live if there is at
+   * least one use of that definition before any intervening instruction that redefines the definition location.
+   */
+  predicate definitionLiveOnEntryToBlock(Alias::MemoryLocation defLocation, OldBlock block) {
+    exists(int firstAccess |
+      definitionHasUse(defLocation, block, firstAccess) and
+      firstAccess = min(int index |
+          definitionHasUse(defLocation, block, index)
+          or
+          definitionHasRedefinition(defLocation, block, index)
+        )
+    )
+    or
+    definitionLiveOnExitFromBlock(defLocation, block) and
+    not definitionHasRedefinition(defLocation, block, _)
+  }
+
+  /**
+   * Holds if the definition `defLocation` is live on exit from block `block`. The definition is live on exit if it is
+   * live on entry to any of the successors of `block`.
+   */
+  pragma[noinline]
+  predicate definitionLiveOnExitFromBlock(Alias::MemoryLocation defLocation, OldBlock block) {
+    definitionLiveOnEntryToBlock(defLocation, block.getAFeasibleSuccessor())
+  }
+}
+
+private import DefUse
+
+/**
+ * Module containing the predicates that connect uses to their reaching definition. The reaching definitions are
+ * computed separately for each unique use `MemoryLocation`. An instruction is treated as a definition of a use location
+ * if the defined location overlaps the use location in any way. Thus, a single instruction may serve as a definition
+ * for multiple use locations, since a single definition location may overlap many use locations.
+ *
+ * Definitions and uses are identified by a block and an integer "offset". An offset of -1 indicates the definition
+ * from a `Phi` instruction at the beginning of the block. An offset of 2*i indicates a definition or use on the
+ * instruction at index `i` in the block. An offset of 2*i+1 indicates a definition or use on the `Chi` instruction that
+ * will be inserted immediately after the instruction at index `i` in the block.
+ *
+ * For a given use location, each definition and use is also assigned a "rank" within its block. The rank is simply the
+ * one-based index of that definition or use within the list of definitions and uses of that location within the block,
+ * ordered by offset. The rank allows the various reachability predicates to be computed more efficiently than they
+ * would if based solely on offset, since the set of possible ranks is dense while the set of possible offsets is
+ * potentially very sparse.
+ */
+module DefUse {
+  /**
+   * Gets the `Instruction` for the definition at offset `defOffset` in block `defBlock`.
+   */
+  bindingset[defOffset, defLocation]
+  pragma[inline]
+  Instruction getDefinitionOrChiInstruction(
+    OldBlock defBlock, int defOffset, Alias::MemoryLocation defLocation
+  ) {
+    defOffset >= 0 and
+    exists(OldInstruction oldInstr |
+      oldInstr = defBlock.getInstruction(defOffset / 2) and
+      if (defOffset % 2) > 0
+      then
+        // An odd offset corresponds to the `Chi` instruction.
+        result = Chi(oldInstr)
+      else
+        // An even offset corresponds to the original instruction.
+        result = getNewInstruction(oldInstr)
+    )
+    or
+    defOffset < 0 and
+    result = Phi(defBlock, defLocation)
+  }
+
+  /**
+   * Gets the rank index of a hyphothetical use one instruction past the end of
+   * the block. This index can be used to determine if a definition reaches the
+   * end of the block, even if the definition is the last instruction in the
+   * block.
+   */
+  private int exitRank(Alias::MemoryLocation useLocation, OldBlock block) {
+    result = max(int rankIndex | defUseRank(useLocation, block, rankIndex, _)) + 1
+  }
+
+  /**
+   * Holds if a definition that overlaps `useLocation` at (`defBlock`, `defRank`) reaches the use of `useLocation` at
+   * (`useBlock`, `useRank`) without any intervening definitions that overlap `useLocation`, where `defBlock` and
+   * `useBlock` are the same block.
+   */
+  private predicate definitionReachesUseWithinBlock(
+    Alias::MemoryLocation useLocation, OldBlock defBlock, int defRank, OldBlock useBlock,
+    int useRank
+  ) {
+    defBlock = useBlock and
+    hasDefinitionAtRank(useLocation, _, defBlock, defRank, _) and
+    hasUseAtRank(useLocation, useBlock, useRank, _) and
+    definitionReachesRank(useLocation, defBlock, defRank, useRank)
+  }
+
+  /**
+   * Holds if a definition that overlaps `useLocation` at (`defBlock`, `defRank`) reaches the use of `useLocation` at
+   * (`useBlock`, `useRank`) without any intervening definitions that overlap `useLocation`.
+   */
+  predicate definitionReachesUse(
+    Alias::MemoryLocation useLocation, OldBlock defBlock, int defRank, OldBlock useBlock,
+    int useRank
+  ) {
+    hasUseAtRank(useLocation, useBlock, useRank, _) and
+    (
+      definitionReachesUseWithinBlock(useLocation, defBlock, defRank, useBlock, useRank)
+      or
+      definitionReachesEndOfBlock(useLocation, defBlock, defRank, useBlock.getAFeasiblePredecessor()) and
+      not definitionReachesUseWithinBlock(useLocation, useBlock, _, useBlock, useRank)
+    )
+  }
+
+  /**
+   * Holds if the definition that overlaps `useLocation` at `(block, defRank)` reaches the rank
+   * index `reachesRank` in block `block`.
+   */
+  private predicate definitionReachesRank(
+    Alias::MemoryLocation useLocation, OldBlock block, int defRank, int reachesRank
+  ) {
+    hasDefinitionAtRank(useLocation, _, block, defRank, _) and
+    reachesRank <= exitRank(useLocation, block) and // Without this, the predicate would be infinite.
+    (
+      // The def always reaches the next use, even if there is also a def on the
+      // use instruction.
+      reachesRank = defRank + 1
+      or
+      // If the def reached the previous rank, it also reaches the current rank,
+      // unless there was another def at the previous rank.
+      definitionReachesRank(useLocation, block, defRank, reachesRank - 1) and
+      not hasDefinitionAtRank(useLocation, _, block, reachesRank - 1, _)
+    )
+  }
+
+  /**
+   * Holds if the definition that overlaps `useLocation` at `(defBlock, defRank)` reaches the end of
+   * block `block` without any intervening definitions that overlap `useLocation`.
+   */
+  predicate definitionReachesEndOfBlock(
+    Alias::MemoryLocation useLocation, OldBlock defBlock, int defRank, OldBlock block
+  ) {
+    hasDefinitionAtRank(useLocation, _, defBlock, defRank, _) and
+    (
+      // If we're looking at the def's own block, just see if it reaches the exit
+      // rank of the block.
+      block = defBlock and
+      locationLiveOnExitFromBlock(useLocation, defBlock) and
+      definitionReachesRank(useLocation, defBlock, defRank, exitRank(useLocation, defBlock))
+      or
+      exists(OldBlock idom |
+        definitionReachesEndOfBlock(useLocation, defBlock, defRank, idom) and
+        noDefinitionsSinceIDominator(useLocation, idom, block)
+      )
+    )
+  }
+
+  pragma[noinline]
+  private predicate noDefinitionsSinceIDominator(
+    Alias::MemoryLocation useLocation, OldBlock idom, OldBlock block
+  ) {
+    Dominance::blockImmediatelyDominates(idom, block) and // It is sufficient to traverse the dominator graph, cf. discussion above.
+    locationLiveOnExitFromBlock(useLocation, block) and
+    not hasDefinition(useLocation, _, block, _)
+  }
+
+  /**
+   * Holds if the specified `useLocation` is live on entry to `block`. This holds if there is a use of `useLocation`
+   * that is reachable from the start of `block` without passing through a definition that overlaps `useLocation`.
+   * Note that even a partially-overlapping definition blocks liveness, because such a definition will insert a `Chi`
+   * instruction whose result totally overlaps the location.
+   */
+  predicate locationLiveOnEntryToBlock(Alias::MemoryLocation useLocation, OldBlock block) {
+    definitionHasPhiNode(useLocation, block)
+    or
+    exists(int firstAccess |
+      hasUse(useLocation, block, firstAccess, _) and
+      firstAccess = min(int offset |
+          hasUse(useLocation, block, offset, _)
+          or
+          hasNonPhiDefinition(useLocation, _, block, offset)
+        )
+    )
+    or
+    locationLiveOnExitFromBlock(useLocation, block) and
+    not hasNonPhiDefinition(useLocation, _, block, _)
+  }
+
+  /**
+   * Holds if the specified `useLocation` is live on exit from `block`.
+   */
+  pragma[noinline]
+  predicate locationLiveOnExitFromBlock(Alias::MemoryLocation useLocation, OldBlock block) {
+    locationLiveOnEntryToBlock(useLocation, block.getAFeasibleSuccessor())
+  }
+
+  /**
+   * Holds if there is a definition at offset `offset` in block `block` that overlaps memory location `useLocation`.
+   * This predicate does not include definitions for Phi nodes.
+   */
+  private predicate hasNonPhiDefinition(
+    Alias::MemoryLocation useLocation, Alias::MemoryLocation defLocation, OldBlock block, int offset
+  ) {
+    exists(OldInstruction def, Overlap overlap, int index |
+      defLocation = Alias::getResultMemoryLocation(def) and
+      block.getInstruction(index) = def and
+      overlap = Alias::getOverlap(defLocation, useLocation) and
+      if overlap instanceof MayPartiallyOverlap
+      then offset = (index * 2) + 1 // The use will be connected to the definition on the `Chi` instruction.
+      else offset = index * 2 // The use will be connected to the definition on the original instruction.
+    )
+  }
+
+  /**
+   * Holds if there is a definition at offset `offset` in block `block` that overlaps memory location `useLocation`.
+   * This predicate includes definitions for Phi nodes (at offset -1).
+   */
+  private predicate hasDefinition(
+    Alias::MemoryLocation useLocation, Alias::MemoryLocation defLocation, OldBlock block, int offset
+  ) {
+    (
+      // If there is a Phi node for the use location itself, treat that as a definition at offset -1.
+      offset = -1 and
+      if definitionHasPhiNode(useLocation, block)
+      then defLocation = useLocation
+      else (
+        definitionHasPhiNode(defLocation, block) and
+        defLocation = useLocation.getVirtualVariable()
+      )
+    )
+    or
+    hasNonPhiDefinition(useLocation, defLocation, block, offset)
+  }
+
+  /**
+   * Holds if there is a definition at offset `offset` in block `block` that overlaps memory location `useLocation`.
+   * `rankIndex` is the rank of the definition as computed by `defUseRank()`.
+   */
+  predicate hasDefinitionAtRank(
+    Alias::MemoryLocation useLocation, Alias::MemoryLocation defLocation, OldBlock block,
+    int rankIndex, int offset
+  ) {
+    hasDefinition(useLocation, defLocation, block, offset) and
+    defUseRank(useLocation, block, rankIndex, offset)
+  }
+
+  /**
+   * Holds if there is a use of `useLocation` on instruction `use` at offset `offset` in block `block`.
+   */
+  private predicate hasUse(
+    Alias::MemoryLocation useLocation, OldBlock block, int offset, OldInstruction use
+  ) {
+    exists(int index |
+      block.getInstruction(index) = use and
+      (
+        // A direct use of the location.
+        useLocation = Alias::getOperandMemoryLocation(use.getAnOperand()) and offset = index * 2
+        or
+        // A `Chi` instruction will include a use of the virtual variable.
+        hasChiNode(useLocation, use) and offset = (index * 2) + 1
+      )
+    )
+  }
+
+  /**
+   * Holds if there is a use of memory location `useLocation` on instruction `use` in block `block`. `rankIndex` is the
+   * rank of the use use as computed by `defUseRank`.
+   */
+  predicate hasUseAtRank(
+    Alias::MemoryLocation useLocation, OldBlock block, int rankIndex, OldInstruction use
+  ) {
+    exists(int offset |
+      hasUse(useLocation, block, offset, use) and
+      defUseRank(useLocation, block, rankIndex, offset)
+    )
+  }
+
+  /**
+   * Holds if there is a definition at offset `offset` in block `block` that overlaps memory location `useLocation`, or
+   * a use of `useLocation` at offset `offset` in block `block`. `rankIndex` is the sequence number of the definition
+   * or use within `block`, counting only uses of `useLocation` and definitions that overlap `useLocation`.
+   */
+  private predicate defUseRank(
+    Alias::MemoryLocation useLocation, OldBlock block, int rankIndex, int offset
+  ) {
+    offset = rank[rankIndex](int j |
+        hasDefinition(useLocation, _, block, j) or hasUse(useLocation, block, j, _)
+      )
+  }
+
+  /**
+   * Holds if the `Phi` instruction for location `useLocation` at the beginning of block `phiBlock` has an operand along
+   * the incoming edge from `predBlock`, where that operand's definition is at offset `defOffset` in block `defBlock`,
+   * and overlaps the use operand with overlap relationship `overlap`.
+   */
+  pragma[inline]
+  predicate hasPhiOperandDefinition(
+    Alias::MemoryLocation defLocation, Alias::MemoryLocation useLocation, OldBlock phiBlock,
+    OldBlock predBlock, OldBlock defBlock, int defOffset, Overlap overlap
+  ) {
+    exists(int defRank |
+      definitionHasPhiNode(useLocation, phiBlock) and
+      predBlock = phiBlock.getAFeasiblePredecessor() and
+      hasDefinitionAtRank(useLocation, defLocation, defBlock, defRank, defOffset) and
+      definitionReachesEndOfBlock(useLocation, defBlock, defRank, predBlock) and
+      overlap = Alias::getOverlap(defLocation, useLocation)
+    )
+  }
+}
+
+/**
+ * Expose some of the internal predicates to PrintSSA.qll. We do this by publicly importing those modules in the
+ * `DebugSSA` module, which is then imported by PrintSSA.
+ */
+module DebugSSA {
+  import PhiInsertion
+  import DefUse
+}
+
+import CachedForDebugging
+
+cached
+private module CachedForDebugging {
+  cached
+  string getTempVariableUniqueId(IRTempVariable var) {
+    result = getOldTempVariable(var).getUniqueId()
+  }
+
+  cached
+  string getInstructionUniqueId(Instruction instr) {
+    exists(OldInstruction oldInstr |
+      oldInstr = getOldInstruction(instr) and
+      result = "NonSSA: " + oldInstr.getUniqueId()
+    )
+    or
+    exists(Alias::MemoryLocation location, OldBlock phiBlock, string specificity |
+      instr = Phi(phiBlock, location) and
+      result = "Phi Block(" + phiBlock.getUniqueId() + ")[" + specificity + "]: " +
+          location.getUniqueId() and
+      if location instanceof Alias::VirtualVariable
+      then
+        // Sort Phi nodes for virtual variables before Phi nodes for member locations.
+        specificity = "g"
+      else specificity = "s"
+    )
+    or
+    instr = Unreached(_) and
+    result = "Unreached"
+  }
+
+  private OldIR::IRTempVariable getOldTempVariable(IRTempVariable var) {
+    result.getEnclosingFunction() = var.getEnclosingFunction() and
+    result.getAST() = var.getAST() and
+    result.getTag() = var.getTag()
+  }
+}
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/SSAConstructionInternal.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/SSAConstructionInternal.qll
@@ -0,0 +1,5 @@
+import semmle.code.csharp.ir.implementation.raw.IR as OldIR
+import semmle.code.csharp.ir.implementation.raw.internal.reachability.ReachableBlock as Reachability
+import semmle.code.csharp.ir.implementation.raw.internal.reachability.Dominance as Dominance
+import semmle.code.csharp.ir.implementation.unaliased_ssa.IR as NewIR
+import SimpleSSA as Alias
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/SimpleSSA.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/SimpleSSA.qll
@@ -0,0 +1,87 @@
+import AliasAnalysis
+private import csharp
+private import semmle.code.csharp.ir.implementation.raw.IR
+private import semmle.code.csharp.ir.internal.IntegerConstant as Ints
+private import semmle.code.csharp.ir.implementation.internal.OperandTag
+private import semmle.code.csharp.ir.internal.Overlap
+
+private class IntValue = Ints::IntValue;
+
+private predicate hasResultMemoryAccess(
+  Instruction instr, IRVariable var, Type type, IntValue bitOffset
+) {
+  resultPointsTo(instr.getResultAddressOperand().getAnyDef(), var, bitOffset) and
+  type = instr.getResultType()
+}
+
+private predicate hasOperandMemoryAccess(
+  MemoryOperand operand, IRVariable var, Type type, IntValue bitOffset
+) {
+  resultPointsTo(operand.getAddressOperand().getAnyDef(), var, bitOffset) and
+  type = operand.getType()
+}
+
+/**
+ * Holds if the specified variable should be modeled in SSA form. For unaliased SSA, we only model a variable if its
+ * address never escapes and all reads and writes of that variable access the entire variable using the original type
+ * of the variable.
+ */
+private predicate isVariableModeled(IRVariable var) {
+  not variableAddressEscapes(var) and
+  // There's no need to check for the right size. An `IRVariable` never has an `UnknownType`, so the test for
+  // `type = var.getType()` is sufficient.
+  forall(Instruction instr, Type type, IntValue bitOffset |
+    hasResultMemoryAccess(instr, var, type, bitOffset)
+  |
+    bitOffset = 0 and
+    type = var.getType()
+  ) and
+  forall(MemoryOperand operand, Type type, IntValue bitOffset |
+    hasOperandMemoryAccess(operand, var, type, bitOffset)
+  |
+    bitOffset = 0 and
+    type = var.getType()
+  )
+}
+
+private newtype TMemoryLocation = MkMemoryLocation(IRVariable var) { isVariableModeled(var) }
+
+private MemoryLocation getMemoryLocation(IRVariable var) { result.getIRVariable() = var }
+
+class MemoryLocation extends TMemoryLocation {
+  IRVariable var;
+
+  MemoryLocation() { this = MkMemoryLocation(var) }
+
+  final string toString() { result = var.toString() }
+
+  final IRVariable getIRVariable() { result = var }
+
+  final VirtualVariable getVirtualVariable() { result = this }
+
+  final Type getType() { result = var.getType() }
+
+  final string getUniqueId() { result = var.getUniqueId() }
+}
+
+class VirtualVariable extends MemoryLocation { }
+
+Overlap getOverlap(MemoryLocation def, MemoryLocation use) {
+  def = use and result instanceof MustExactlyOverlap
+  or
+  none() // Avoid compiler error in SSAConstruction
+}
+
+MemoryLocation getResultMemoryLocation(Instruction instr) {
+  exists(IRVariable var |
+    hasResultMemoryAccess(instr, var, _, _) and
+    result = getMemoryLocation(var)
+  )
+}
+
+MemoryLocation getOperandMemoryLocation(MemoryOperand operand) {
+  exists(IRVariable var |
+    hasOperandMemoryAccess(operand, var, _, _) and
+    result = getMemoryLocation(var)
+  )
+}
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/reachability/Dominance.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/reachability/Dominance.qll
@@ -0,0 +1,22 @@
+private import DominanceInternal
+
+predicate blockImmediatelyDominates(Graph::Block dominator, Graph::Block block) =
+  idominance(Graph::isEntryBlock/1, Graph::blockSuccessor/2)(_, dominator, block)
+
+predicate blockStrictlyDominates(Graph::Block dominator, Graph::Block block) {
+  blockImmediatelyDominates+(dominator, block)
+}
+
+predicate blockDominates(Graph::Block dominator, Graph::Block block) {
+  blockStrictlyDominates(dominator, block) or dominator = block
+}
+
+Graph::Block getDominanceFrontier(Graph::Block dominator) {
+  Graph::blockSuccessor(dominator, result) and
+  not blockImmediatelyDominates(dominator, result)
+  or
+  exists(Graph::Block prev | result = getDominanceFrontier(prev) |
+    blockImmediatelyDominates(dominator, prev) and
+    not blockImmediatelyDominates(dominator, result)
+  )
+}
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/reachability/DominanceInternal.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/reachability/DominanceInternal.qll
@@ -0,0 +1,9 @@
+private import ReachableBlock as Reachability
+
+private module ReachabilityGraph = Reachability::Graph;
+
+module Graph {
+  import Reachability::Graph
+
+  class Block = Reachability::ReachableBlock;
+}
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/reachability/PrintDominance.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/reachability/PrintDominance.qll
@@ -0,0 +1,21 @@
+private import DominanceInternal
+private import ReachableBlockInternal
+private import Dominance
+import IR
+
+private class DominancePropertyProvider extends IRPropertyProvider {
+  override string getBlockProperty(IRBlock block, string key) {
+    exists(IRBlock dominator |
+      blockImmediatelyDominates(dominator, block) and
+      key = "ImmediateDominator" and
+      result = "Block " + dominator.getDisplayIndex().toString()
+    )
+    or
+    key = "DominanceFrontier" and
+    result = strictconcat(IRBlock frontierBlock |
+        frontierBlock = getDominanceFrontier(block)
+      |
+        frontierBlock.getDisplayIndex().toString(), ", " order by frontierBlock.getDisplayIndex()
+      )
+  }
+}
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/reachability/PrintReachableBlock.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/reachability/PrintReachableBlock.qll
@@ -0,0 +1,17 @@
+private import ReachableBlockInternal
+private import ReachableBlock
+import IR
+
+private class ReachableBlockPropertyProvider extends IRPropertyProvider {
+  override string getBlockProperty(IRBlock block, string key) {
+    not block instanceof ReachableBlock and
+    key = "Unreachable" and
+    result = "true"
+    or
+    exists(EdgeKind kind |
+      isInfeasibleEdge(block, kind) and
+      key = "Infeasible(" + kind.toString() + ")" and
+      result = "true"
+    )
+  }
+}
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/reachability/ReachableBlock.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/reachability/ReachableBlock.qll
@@ -0,0 +1,53 @@
+private import ReachableBlockInternal
+private import IR
+private import ConstantAnalysis
+
+predicate isInfeasibleInstructionSuccessor(Instruction instr, EdgeKind kind) {
+  exists(int conditionValue |
+    conditionValue = getConstantValue(instr.(ConditionalBranchInstruction).getCondition()) and
+    if conditionValue = 0 then kind instanceof TrueEdge else kind instanceof FalseEdge
+  )
+}
+
+pragma[noinline]
+predicate isInfeasibleEdge(IRBlockBase block, EdgeKind kind) {
+  isInfeasibleInstructionSuccessor(block.getLastInstruction(), kind)
+}
+
+private IRBlock getAFeasiblePredecessorBlock(IRBlock successor) {
+  exists(EdgeKind kind |
+    result.getSuccessor(kind) = successor and
+    not isInfeasibleEdge(result, kind)
+  )
+}
+
+private predicate isBlockReachable(IRBlock block) {
+  exists(IRFunction f | getAFeasiblePredecessorBlock*(block) = f.getEntryBlock())
+}
+
+/**
+ * An IR block that is reachable from the entry block of the function, considering only feasible
+ * edges.
+ */
+class ReachableBlock extends IRBlockBase {
+  ReachableBlock() { isBlockReachable(this) }
+
+  final ReachableBlock getAFeasiblePredecessor() { result = getAFeasiblePredecessorBlock(this) }
+
+  final ReachableBlock getAFeasibleSuccessor() { this = getAFeasiblePredecessorBlock(result) }
+}
+
+/**
+ * An instruction that is contained in a reachable block.
+ */
+class ReachableInstruction extends Instruction {
+  ReachableInstruction() { this.getBlock() instanceof ReachableBlock }
+}
+
+module Graph {
+  predicate isEntryBlock(ReachableBlock block) { exists(IRFunction f | block = f.getEntryBlock()) }
+
+  predicate blockSuccessor(ReachableBlock pred, ReachableBlock succ) {
+    succ = pred.getAFeasibleSuccessor()
+  }
+}
--- a/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/reachability/ReachableBlockInternal.qll
+++ b/csharp/ql/src/semmle/code/csharp/ir/implementation/unaliased_ssa/internal/reachability/ReachableBlockInternal.qll
@@ -0,0 +1,2 @@
+import semmle.code.cpp.ir.implementation.unaliased_ssa.IR as IR
+import semmle.code.cpp.ir.implementation.unaliased_ssa.constant.ConstantAnalysis as ConstantAnalysis
--- a/csharp/ql/test/library-tests/ir/ir/events.cs
+++ b/csharp/ql/test/library-tests/ir/ir/events.cs
@@ -0,0 +1,35 @@
+class Events
+{
+    public delegate string MyDel(string str);
+    public MyDel Inst;
+
+    event MyDel MyEvent;
+
+    public Events()
+    {
+        this.Inst = new MyDel(this.Fun);
+    }
+
+    public void AddEvent() 
+    {
+        this.MyEvent += this.Inst;
+    }
+
+    public void RemoveEvent()
+    {
+        this.MyEvent -= this.Inst;
+    }
+
+    public string Fun(string str) 
+    {
+        return str;
+    }
+    
+    static void Main(string[] args) 
+    {
+        Events obj = new Events();
+        obj.AddEvent();
+        string result = obj.MyEvent("string");
+        obj.RemoveEvent();
+    }
+}
--- a/csharp/ql/test/library-tests/ir/ir/indexers.cs
+++ b/csharp/ql/test/library-tests/ir/ir/indexers.cs
@@ -0,0 +1,30 @@
+class Indexers
+{
+    public class MyClass
+    {
+        public MyClass()
+        {
+        }
+
+        private string[] address = new string[2];
+        public string this[int index]
+        {
+            get
+            {
+                return address[index];
+            }
+            set
+            {
+                address[index] = value;
+            }
+        }
+    }
+
+    public static void Main()
+    {
+        MyClass inst = new MyClass();
+        inst[0] = "str1";
+        inst[1] = "str1";
+        inst[1] = inst[0];
+    }
+}
--- a/csharp/ql/test/library-tests/ir/ir/raw_ir.expected
+++ b/csharp/ql/test/library-tests/ir/ir/raw_ir.expected
@@ -480,6 +480,111 @@ delegates.cs:
 #   11|     v0_17(Void)       = UnmodeledUse             : mu*
 #   11|     v0_18(Void)       = ExitFunction             : 

+events.cs:
+#    8| System.Void Events..ctor()
+#    8|   Block 0
+#    8|     v0_0(Void)          = EnterFunction          : 
+#    8|     mu0_1(null)         = AliasedDefinition      : 
+#    8|     mu0_2(null)         = UnmodeledDefinition    : 
+#    8|     r0_3(glval<Events>) = InitializeThis         : 
+#   10|     r0_4(MyDel)         = NewObj                 : 
+#   10|     r0_5(glval<null>)   = FunctionAddress[MyDel] : 
+#   10|     r0_6(glval<MyDel>)  = FunctionAddress[Fun]   : 
+#   10|     v0_7(Void)          = Call                   : func:r0_5, this:r0_4, 0:r0_6
+#   10|     mu0_8(null)         = ^CallSideEffect        : ~mu0_2
+#   10|     r0_9(Events)        = CopyValue              : r0_3
+#   10|     r0_10(glval<MyDel>) = FieldAddress[Inst]     : r0_9
+#   10|     mu0_11(MyDel)       = Store                  : &:r0_10, r0_4
+#    8|     v0_12(Void)         = ReturnVoid             : 
+#    8|     v0_13(Void)         = UnmodeledUse           : mu*
+#    8|     v0_14(Void)         = ExitFunction           : 
+
+#   13| System.Void Events.AddEvent()
+#   13|   Block 0
+#   13|     v0_0(Void)          = EnterFunction                : 
+#   13|     mu0_1(null)         = AliasedDefinition            : 
+#   13|     mu0_2(null)         = UnmodeledDefinition          : 
+#   13|     r0_3(glval<Events>) = InitializeThis               : 
+#   15|     r0_4(Events)        = CopyValue                    : r0_3
+#   15|     r0_5(glval<null>)   = FunctionAddress[add_MyEvent] : 
+#   15|     r0_6(Events)        = CopyValue                    : r0_3
+#   15|     r0_7(glval<MyDel>)  = FieldAddress[Inst]           : r0_6
+#   15|     r0_8(MyDel)         = Load                         : &:r0_7, ~mu0_2
+#   15|     v0_9(Void)          = Call                         : func:r0_5, this:r0_4, 0:r0_8
+#   15|     mu0_10(null)        = ^CallSideEffect              : ~mu0_2
+#   13|     v0_11(Void)         = ReturnVoid                   : 
+#   13|     v0_12(Void)         = UnmodeledUse                 : mu*
+#   13|     v0_13(Void)         = ExitFunction                 : 
+
+#   18| System.Void Events.RemoveEvent()
+#   18|   Block 0
+#   18|     v0_0(Void)          = EnterFunction                   : 
+#   18|     mu0_1(null)         = AliasedDefinition               : 
+#   18|     mu0_2(null)         = UnmodeledDefinition             : 
+#   18|     r0_3(glval<Events>) = InitializeThis                  : 
+#   20|     r0_4(Events)        = CopyValue                       : r0_3
+#   20|     r0_5(glval<null>)   = FunctionAddress[remove_MyEvent] : 
+#   20|     r0_6(Events)        = CopyValue                       : r0_3
+#   20|     r0_7(glval<MyDel>)  = FieldAddress[Inst]              : r0_6
+#   20|     r0_8(MyDel)         = Load                            : &:r0_7, ~mu0_2
+#   20|     v0_9(Void)          = Call                            : func:r0_5, this:r0_4, 0:r0_8
+#   20|     mu0_10(null)        = ^CallSideEffect                 : ~mu0_2
+#   18|     v0_11(Void)         = ReturnVoid                      : 
+#   18|     v0_12(Void)         = UnmodeledUse                    : mu*
+#   18|     v0_13(Void)         = ExitFunction                    : 
+
+#   23| System.String Events.Fun(System.String)
+#   23|   Block 0
+#   23|     v0_0(Void)           = EnterFunction            : 
+#   23|     mu0_1(null)          = AliasedDefinition        : 
+#   23|     mu0_2(null)          = UnmodeledDefinition      : 
+#   23|     r0_3(glval<Events>)  = InitializeThis           : 
+#   23|     r0_4(glval<String>)  = VariableAddress[str]     : 
+#   23|     mu0_5(String)        = InitializeParameter[str] : &:r0_4
+#   25|     r0_6(glval<String>)  = VariableAddress[#return] : 
+#   25|     r0_7(glval<String>)  = VariableAddress[str]     : 
+#   25|     r0_8(String)         = Load                     : &:r0_7, ~mu0_2
+#   25|     mu0_9(String)        = Store                    : &:r0_6, r0_8
+#   23|     r0_10(glval<String>) = VariableAddress[#return] : 
+#   23|     v0_11(Void)          = ReturnValue              : &:r0_10, ~mu0_2
+#   23|     v0_12(Void)          = UnmodeledUse             : mu*
+#   23|     v0_13(Void)          = ExitFunction             : 
+
+#   28| System.Void Events.Main(System.String[])
+#   28|   Block 0
+#   28|     v0_0(Void)            = EnterFunction                : 
+#   28|     mu0_1(null)           = AliasedDefinition            : 
+#   28|     mu0_2(null)           = UnmodeledDefinition          : 
+#   28|     r0_3(glval<String[]>) = VariableAddress[args]        : 
+#   28|     mu0_4(String[])       = InitializeParameter[args]    : &:r0_3
+#   30|     r0_5(glval<Events>)   = VariableAddress[obj]         : 
+#   30|     r0_6(Events)          = NewObj                       : 
+#   30|     r0_7(glval<null>)     = FunctionAddress[Events]      : 
+#   30|     v0_8(Void)            = Call                         : func:r0_7, this:r0_6
+#   30|     mu0_9(null)           = ^CallSideEffect              : ~mu0_2
+#   30|     mu0_10(Events)        = Store                        : &:r0_5, r0_6
+#   31|     r0_11(glval<Events>)  = VariableAddress[obj]         : 
+#   31|     r0_12(Events)         = Load                         : &:r0_11, ~mu0_2
+#   31|     r0_13(glval<null>)    = FunctionAddress[AddEvent]    : 
+#   31|     v0_14(Void)           = Call                         : func:r0_13, this:r0_12
+#   31|     mu0_15(null)          = ^CallSideEffect              : ~mu0_2
+#   32|     r0_16(glval<String>)  = VariableAddress[result]      : 
+#   32|     r0_17(glval<Events>)  = VariableAddress[obj]         : 
+#   32|     r0_18(Events)         = Load                         : &:r0_17, ~mu0_2
+#   32|     r0_19(glval<null>)    = FunctionAddress[Invoke]      : 
+#   32|     r0_20(String)         = StringConstant["string"]     : 
+#   32|     v0_21(Void)           = Call                         : func:r0_19, this:r0_18, 0:r0_20
+#   32|     mu0_22(null)          = ^CallSideEffect              : ~mu0_2
+#   32|     mu0_23(String)        = Store                        : &:r0_16, v0_21
+#   33|     r0_24(glval<Events>)  = VariableAddress[obj]         : 
+#   33|     r0_25(Events)         = Load                         : &:r0_24, ~mu0_2
+#   33|     r0_26(glval<null>)    = FunctionAddress[RemoveEvent] : 
+#   33|     v0_27(Void)           = Call                         : func:r0_26, this:r0_25
+#   33|     mu0_28(null)          = ^CallSideEffect              : ~mu0_2
+#   28|     v0_29(Void)           = ReturnVoid                   : 
+#   28|     v0_30(Void)           = UnmodeledUse                 : mu*
+#   28|     v0_31(Void)           = ExitFunction                 : 
+
 foreach.cs:
 #    4| System.Void ForEach.Main()
 #    4|   Block 0
@@ -598,6 +703,104 @@ func_with_param_call.cs:
 #   10|     v0_12(Void)         = UnmodeledUse             : mu*
 #   10|     v0_13(Void)         = ExitFunction             : 

+indexers.cs:
+#    5| System.Void Indexers.MyClass..ctor()
+#    5|   Block 0
+#    5|     v0_0(Void)           = EnterFunction       : 
+#    5|     mu0_1(null)          = AliasedDefinition   : 
+#    5|     mu0_2(null)          = UnmodeledDefinition : 
+#    5|     r0_3(glval<MyClass>) = InitializeThis      : 
+#    6|     v0_4(Void)           = NoOp                : 
+#    5|     v0_5(Void)           = ReturnVoid          : 
+#    5|     v0_6(Void)           = UnmodeledUse        : mu*
+#    5|     v0_7(Void)           = ExitFunction        : 
+
+#   12| System.String Indexers.MyClass.get_Item(System.Int32)
+#   12|   Block 0
+#   12|     v0_0(Void)            = EnterFunction              : 
+#   12|     mu0_1(null)           = AliasedDefinition          : 
+#   12|     mu0_2(null)           = UnmodeledDefinition        : 
+#   12|     r0_3(glval<MyClass>)  = InitializeThis             : 
+#   10|     r0_4(glval<Int32>)    = VariableAddress[index]     : 
+#   10|     mu0_5(Int32)          = InitializeParameter[index] : &:r0_4
+#   14|     r0_6(glval<String>)   = VariableAddress[#return]   : 
+#   14|     r0_7(MyClass)         = CopyValue                  : r0_3
+#   14|     r0_8(glval<String[]>) = FieldAddress[address]      : r0_7
+#   14|     r0_9(String[])        = ElementsAddress            : r0_8
+#   14|     r0_10(glval<Int32>)   = VariableAddress[index]     : 
+#   14|     r0_11(Int32)          = Load                       : &:r0_10, ~mu0_2
+#   14|     r0_12(String[])       = PointerAdd[8]              : r0_9, r0_11
+#   14|     r0_13(String)         = Load                       : &:r0_12, ~mu0_2
+#   14|     mu0_14(String)        = Store                      : &:r0_6, r0_13
+#   12|     r0_15(glval<String>)  = VariableAddress[#return]   : 
+#   12|     v0_16(Void)           = ReturnValue                : &:r0_15, ~mu0_2
+#   12|     v0_17(Void)           = UnmodeledUse               : mu*
+#   12|     v0_18(Void)           = ExitFunction               : 
+
+#   16| System.Void Indexers.MyClass.set_Item(System.Int32,System.String)
+#   16|   Block 0
+#   16|     v0_0(Void)             = EnterFunction              : 
+#   16|     mu0_1(null)            = AliasedDefinition          : 
+#   16|     mu0_2(null)            = UnmodeledDefinition        : 
+#   16|     r0_3(glval<MyClass>)   = InitializeThis             : 
+#   10|     r0_4(glval<Int32>)     = VariableAddress[index]     : 
+#   10|     mu0_5(Int32)           = InitializeParameter[index] : &:r0_4
+#   16|     r0_6(glval<String>)    = VariableAddress[value]     : 
+#   16|     mu0_7(String)          = InitializeParameter[value] : &:r0_6
+#   18|     r0_8(glval<String>)    = VariableAddress[value]     : 
+#   18|     r0_9(String)           = Load                       : &:r0_8, ~mu0_2
+#   18|     r0_10(MyClass)         = CopyValue                  : r0_3
+#   18|     r0_11(glval<String[]>) = FieldAddress[address]      : r0_10
+#   18|     r0_12(String[])        = ElementsAddress            : r0_11
+#   18|     r0_13(glval<Int32>)    = VariableAddress[index]     : 
+#   18|     r0_14(Int32)           = Load                       : &:r0_13, ~mu0_2
+#   18|     r0_15(String[])        = PointerAdd[8]              : r0_12, r0_14
+#   18|     mu0_16(String)         = Store                      : &:r0_15, r0_9
+#   16|     v0_17(Void)            = ReturnVoid                 : 
+#   16|     v0_18(Void)            = UnmodeledUse               : mu*
+#   16|     v0_19(Void)            = ExitFunction               : 
+
+#   23| System.Void Indexers.Main()
+#   23|   Block 0
+#   23|     v0_0(Void)            = EnterFunction             : 
+#   23|     mu0_1(null)           = AliasedDefinition         : 
+#   23|     mu0_2(null)           = UnmodeledDefinition       : 
+#   25|     r0_3(glval<MyClass>)  = VariableAddress[inst]     : 
+#   25|     r0_4(MyClass)         = NewObj                    : 
+#   25|     r0_5(glval<null>)     = FunctionAddress[MyClass]  : 
+#   25|     v0_6(Void)            = Call                      : func:r0_5, this:r0_4
+#   25|     mu0_7(null)           = ^CallSideEffect           : ~mu0_2
+#   25|     mu0_8(MyClass)        = Store                     : &:r0_3, r0_4
+#   26|     r0_9(glval<MyClass>)  = VariableAddress[inst]     : 
+#   26|     r0_10(MyClass)        = Load                      : &:r0_9, ~mu0_2
+#   26|     r0_11(glval<null>)    = FunctionAddress[set_Item] : 
+#   26|     r0_12(Int32)          = Constant[0]               : 
+#   26|     r0_13(String)         = StringConstant["str1"]    : 
+#   26|     v0_14(Void)           = Call                      : func:r0_11, this:r0_10, 0:r0_12, 1:r0_13
+#   26|     mu0_15(null)          = ^CallSideEffect           : ~mu0_2
+#   27|     r0_16(glval<MyClass>) = VariableAddress[inst]     : 
+#   27|     r0_17(MyClass)        = Load                      : &:r0_16, ~mu0_2
+#   27|     r0_18(glval<null>)    = FunctionAddress[set_Item] : 
+#   27|     r0_19(Int32)          = Constant[1]               : 
+#   27|     r0_20(String)         = StringConstant["str1"]    : 
+#   27|     v0_21(Void)           = Call                      : func:r0_18, this:r0_17, 0:r0_19, 1:r0_20
+#   27|     mu0_22(null)          = ^CallSideEffect           : ~mu0_2
+#   28|     r0_23(glval<MyClass>) = VariableAddress[inst]     : 
+#   28|     r0_24(MyClass)        = Load                      : &:r0_23, ~mu0_2
+#   28|     r0_25(glval<null>)    = FunctionAddress[set_Item] : 
+#   28|     r0_26(Int32)          = Constant[1]               : 
+#   28|     r0_27(glval<MyClass>) = VariableAddress[inst]     : 
+#   28|     r0_28(MyClass)        = Load                      : &:r0_27, ~mu0_2
+#   28|     r0_29(glval<null>)    = FunctionAddress[get_Item] : 
+#   28|     r0_30(Int32)          = Constant[0]               : 
+#   28|     r0_31(String)         = Call                      : func:r0_29, this:r0_28, 0:r0_30
+#   28|     mu0_32(null)          = ^CallSideEffect           : ~mu0_2
+#   28|     v0_33(Void)           = Call                      : func:r0_25, this:r0_24, 0:r0_26, 1:r0_31
+#   28|     mu0_34(null)          = ^CallSideEffect           : ~mu0_2
+#   23|     v0_35(Void)           = ReturnVoid                : 
+#   23|     v0_36(Void)           = UnmodeledUse              : mu*
+#   23|     v0_37(Void)           = ExitFunction              : 
+
 inheritance_polymorphism.cs:
 #    3| System.Int32 A.function()
 #    3|   Block 0
@@ -806,8 +1009,10 @@ isexpr.cs:
 #   13|     r0_13(Object)        = Load                 : &:r0_12, ~mu0_2
 #   13|     r0_14(Is_A)          = CheckedConvertOrNull : r0_13
 #   13|     r0_15(Is_A)          = Constant[0]          : 
-#   13|     r0_16(Boolean)       = CompareNE            : r0_14, r0_15
-#   13|     r0_17(Boolean)       = ConditionalBranch    : r0_16
+#   13|     r0_16(glval<Is_A>)   = VariableAddress[tmp] : 
+#   13|     mu0_17(Is_A)         = Uninitialized[tmp]   : &:r0_16
+#   13|     r0_18(Boolean)       = CompareNE            : r0_14, r0_15
+#   13|     v0_19(Void)          = ConditionalBranch    : r0_18
 #-----|   False -> Block 2
 #-----|   True -> Block 3

@@ -817,13 +1022,12 @@ isexpr.cs:
 #    8|     v1_2(Void) = ExitFunction : 

 #   13|   Block 2
-#   13|     v2_0(Void) = ConditionalBranch : r0_16
+#   13|     v2_0(Void) = ConditionalBranch : r0_18
 #-----|   False -> Block 5
 #-----|   True -> Block 4

 #   13|   Block 3
-#   13|     r3_0(glval<Is_A>) = VariableAddress[tmp] : 
-#   13|     mu3_1(Is_A)       = Store                : &:r3_0, r0_14
+#   13|     mu3_0(Is_A) = Store : &:r0_16, r0_14
 #-----|   Goto -> Block 2

 #   15|   Block 4
--- a/csharp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.expected
+++ b/csharp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.expected
@@ -0,0 +1,15 @@
+missingOperand
+unexpectedOperand
+duplicateOperand
+missingPhiOperand
+missingOperandType
+instructionWithoutSuccessor
+ambiguousSuccessors
+unexplainedLoop
+unnecessaryPhiInstruction
+operandAcrossFunctions
+instructionWithoutUniqueBlock
+containsLoopOfForwardEdges
+lostReachability
+backEdgeCountMismatch
+useNotDominatedByDefinition
--- a/csharp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.qlref
+++ b/csharp/ql/test/library-tests/ir/ir/unaliased_ssa_sanity.qlref
@@ -0,0 +1 @@
+semmle/code/csharp/ir/implementation/unaliased_ssa/IRSanity.ql
--- a/docs/language/learn-ql/python/pointsto-type-infer.rst
+++ b/docs/language/learn-ql/python/pointsto-type-infer.rst
@@ -173,7 +173,7 @@ Many of the results shown will have ``cls`` as ``NoneType``. It is more informat
     not cls.hasAttribute("__iter__")
   select loop, cls, origin

-➤ `See this in the query console <https://lgtm.com/query/6718356557331218618/>`__. This reports the same results, but with a third column showing the source of the ``None`` values.
+➤ `See this in the query console <https://lgtm.com/query/3795352249440053606/>`__. This reports the same results, but with a third column showing the source of the ``None`` values.

 Finding calls using call-graph analysis
 ----------------------------------------------------
--- a/docs/language/learn-ql/python/statements-expressions.rst
+++ b/docs/language/learn-ql/python/statements-expressions.rst
@@ -72,7 +72,7 @@ An ``if`` statement where one branch is composed of just ``pass`` statements cou

 To find statements like this we can run the following query:

-**Find ``if`` statements with empty branches**
+**Find 'if' statements with empty branches**

 .. code-block:: ql

--- a/javascript/extractor/lib/typescript/src/ast_extractor.ts
+++ b/javascript/extractor/lib/typescript/src/ast_extractor.ts
@@ -22,6 +22,7 @@ export interface AugmentedNode extends ts.Node {
    $symbol?: number;
    $resolvedSignature?: number;
    $overloadIndex?: number;
+    $declaredSignature?: number;
 }

 export type AugmentedPos = number;
@@ -263,6 +264,17 @@ export function augmentAst(ast: AugmentedSourceFile, code: string, project: Proj
                    namePart.$symbol = typeTable.getSymbolId(symbol);
                }
            }
+            if (ts.isFunctionLike(node)) {
+                let signature = typeChecker.getSignatureFromDeclaration(node);
+                if (signature != null) {
+                    let kind = ts.isConstructSignatureDeclaration(node) || ts.isConstructorDeclaration(node)
+                            ? ts.SignatureKind.Construct : ts.SignatureKind.Call;
+                    let id = typeTable.getSignatureId(kind, signature);
+                    if (id != null) {
+                        (node as AugmentedNode).$declaredSignature = id;
+                    }
+                }
+            }
        }
    }
 }
@@ -295,54 +307,61 @@ function isNamedNodeWithSymbol(node: ts.Node): node is NamedNodeWithSymbol {
 */
 function isTypedNode(node: ts.Node): boolean {
    switch (node.kind) {
-      case ts.SyntaxKind.ArrayLiteralExpression:
-      case ts.SyntaxKind.ArrowFunction:
-      case ts.SyntaxKind.AsExpression:
-      case ts.SyntaxKind.AwaitExpression:
-      case ts.SyntaxKind.BinaryExpression:
-      case ts.SyntaxKind.CallExpression:
-      case ts.SyntaxKind.ClassExpression:
-      case ts.SyntaxKind.CommaListExpression:
-      case ts.SyntaxKind.ConditionalExpression:
-      case ts.SyntaxKind.DeleteExpression:
-      case ts.SyntaxKind.ElementAccessExpression:
-      case ts.SyntaxKind.ExpressionStatement:
-      case ts.SyntaxKind.ExpressionWithTypeArguments:
-      case ts.SyntaxKind.FalseKeyword:
-      case ts.SyntaxKind.FunctionDeclaration:
-      case ts.SyntaxKind.FunctionExpression:
-      case ts.SyntaxKind.Identifier:
-      case ts.SyntaxKind.JsxExpression:
-      case ts.SyntaxKind.LiteralType:
-      case ts.SyntaxKind.NewExpression:
-      case ts.SyntaxKind.NonNullExpression:
-      case ts.SyntaxKind.NoSubstitutionTemplateLiteral:
-      case ts.SyntaxKind.NumericLiteral:
-      case ts.SyntaxKind.ObjectKeyword:
-      case ts.SyntaxKind.ObjectLiteralExpression:
-      case ts.SyntaxKind.OmittedExpression:
-      case ts.SyntaxKind.ParenthesizedExpression:
-      case ts.SyntaxKind.PartiallyEmittedExpression:
-      case ts.SyntaxKind.PostfixUnaryExpression:
-      case ts.SyntaxKind.PrefixUnaryExpression:
-      case ts.SyntaxKind.PropertyAccessExpression:
-      case ts.SyntaxKind.RegularExpressionLiteral:
-      case ts.SyntaxKind.StringLiteral:
-      case ts.SyntaxKind.TaggedTemplateExpression:
-      case ts.SyntaxKind.TemplateExpression:
-      case ts.SyntaxKind.TemplateHead:
-      case ts.SyntaxKind.TemplateMiddle:
-      case ts.SyntaxKind.TemplateSpan:
-      case ts.SyntaxKind.TemplateTail:
-      case ts.SyntaxKind.TrueKeyword:
-      case ts.SyntaxKind.TypeAssertionExpression:
-      case ts.SyntaxKind.TypeLiteral:
-      case ts.SyntaxKind.TypeOfExpression:
-      case ts.SyntaxKind.VoidExpression:
-      case ts.SyntaxKind.YieldExpression:
-        return true;
-      default:
-        return ts.isTypeNode(node);
+        case ts.SyntaxKind.ArrayLiteralExpression:
+        case ts.SyntaxKind.ArrowFunction:
+        case ts.SyntaxKind.AsExpression:
+        case ts.SyntaxKind.AwaitExpression:
+        case ts.SyntaxKind.BinaryExpression:
+        case ts.SyntaxKind.CallExpression:
+        case ts.SyntaxKind.ClassExpression:
+        case ts.SyntaxKind.ClassDeclaration:
+        case ts.SyntaxKind.CommaListExpression:
+        case ts.SyntaxKind.ConditionalExpression:
+        case ts.SyntaxKind.Constructor:
+        case ts.SyntaxKind.DeleteExpression:
+        case ts.SyntaxKind.ElementAccessExpression:
+        case ts.SyntaxKind.ExpressionStatement:
+        case ts.SyntaxKind.ExpressionWithTypeArguments:
+        case ts.SyntaxKind.FalseKeyword:
+        case ts.SyntaxKind.FunctionDeclaration:
+        case ts.SyntaxKind.FunctionExpression:
+        case ts.SyntaxKind.GetAccessor:
+        case ts.SyntaxKind.Identifier:
+        case ts.SyntaxKind.IndexSignature:
+        case ts.SyntaxKind.JsxExpression:
+        case ts.SyntaxKind.LiteralType:
+        case ts.SyntaxKind.MethodDeclaration:
+        case ts.SyntaxKind.MethodSignature:
+        case ts.SyntaxKind.NewExpression:
+        case ts.SyntaxKind.NonNullExpression:
+        case ts.SyntaxKind.NoSubstitutionTemplateLiteral:
+        case ts.SyntaxKind.NumericLiteral:
+        case ts.SyntaxKind.ObjectKeyword:
+        case ts.SyntaxKind.ObjectLiteralExpression:
+        case ts.SyntaxKind.OmittedExpression:
+        case ts.SyntaxKind.ParenthesizedExpression:
+        case ts.SyntaxKind.PartiallyEmittedExpression:
+        case ts.SyntaxKind.PostfixUnaryExpression:
+        case ts.SyntaxKind.PrefixUnaryExpression:
+        case ts.SyntaxKind.PropertyAccessExpression:
+        case ts.SyntaxKind.RegularExpressionLiteral:
+        case ts.SyntaxKind.SetAccessor:
+        case ts.SyntaxKind.StringLiteral:
+        case ts.SyntaxKind.TaggedTemplateExpression:
+        case ts.SyntaxKind.TemplateExpression:
+        case ts.SyntaxKind.TemplateHead:
+        case ts.SyntaxKind.TemplateMiddle:
+        case ts.SyntaxKind.TemplateSpan:
+        case ts.SyntaxKind.TemplateTail:
+        case ts.SyntaxKind.TrueKeyword:
+        case ts.SyntaxKind.TypeAssertionExpression:
+        case ts.SyntaxKind.TypeLiteral:
+        case ts.SyntaxKind.TypeOfExpression:
+        case ts.SyntaxKind.VoidExpression:
+        case ts.SyntaxKind.YieldExpression:
+            return true;
+        default:
+            return ts.isTypeNode(node);
    }
 }

--- a/javascript/extractor/src/com/semmle/js/ast/AFunctionExpression.java
+++ b/javascript/extractor/src/com/semmle/js/ast/AFunctionExpression.java
@@ -12,6 +12,7 @@ import java.util.List;
 public abstract class AFunctionExpression extends Expression implements IFunction {
  private final AFunction<? extends Node> fn;
  private int symbol = -1;
+  private int declaredSignature = -1;

  public AFunctionExpression(
      String type,
@@ -144,4 +145,14 @@ public abstract class AFunctionExpression extends Expression implements IFunctio
  public void setSymbol(int symbol) {
    this.symbol = symbol;
  }
+
+  @Override
+  public int getDeclaredSignatureId() {
+    return declaredSignature;
+  }
+
+  @Override
+  public void setDeclaredSignatureId(int id) {
+    declaredSignature = id;
+  }
 }
--- a/javascript/extractor/src/com/semmle/js/ast/FunctionDeclaration.java
+++ b/javascript/extractor/src/com/semmle/js/ast/FunctionDeclaration.java
@@ -19,6 +19,8 @@ public class FunctionDeclaration extends Statement implements IFunction {
  private final AFunction<? extends Node> fn;
  private final boolean hasDeclareKeyword;
  private int symbol = -1;
+  private int staticType = -1;
+  private int declaredSignature = -1;

  public FunctionDeclaration(
      SourceLocation loc,
@@ -185,4 +187,24 @@ public class FunctionDeclaration extends Statement implements IFunction {
  public void setSymbol(int symbol) {
    this.symbol = symbol;
  }
+
+  @Override
+  public int getStaticTypeId() {
+    return staticType;
+  }
+
+  @Override
+  public void setStaticTypeId(int id) {
+    staticType = id;
+  }
+
+  @Override
+  public int getDeclaredSignatureId() {
+    return declaredSignature;
+  }
+
+  @Override
+  public void setDeclaredSignatureId(int id) {
+    declaredSignature = id;
+  }
 }
--- a/javascript/extractor/src/com/semmle/js/ast/IFunction.java
+++ b/javascript/extractor/src/com/semmle/js/ast/IFunction.java
@@ -3,11 +3,12 @@ package com.semmle.js.ast;
 import com.semmle.ts.ast.DecoratorList;
 import com.semmle.ts.ast.INodeWithSymbol;
 import com.semmle.ts.ast.ITypeExpression;
+import com.semmle.ts.ast.ITypedAstNode;
 import com.semmle.ts.ast.TypeParameter;
 import java.util.List;

 /** A function declaration or expression. */
-public interface IFunction extends IStatementContainer, INodeWithSymbol {
+public interface IFunction extends IStatementContainer, INodeWithSymbol, ITypedAstNode {
  /** The function name; may be null for function expressions. */
  public Identifier getId();

@@ -63,4 +64,15 @@ public interface IFunction extends IStatementContainer, INodeWithSymbol {
  public List<DecoratorList> getParameterDecorators();

  public boolean hasDeclareKeyword();
+
+  /**
+   * Gets the type signature of this function as determined by the TypeScript compiler, or -1 if no
+   * call signature was extracted.
+   *
+   * <p>The ID refers to a signature in a table that is extracted on a per-project basis, and the
+   * meaning of this type ID is not available at the AST level.
+   */
+  public int getDeclaredSignatureId();
+
+  public void setDeclaredSignatureId(int id);
 }
--- a/javascript/extractor/src/com/semmle/js/extractor/ASTExtractor.java
+++ b/javascript/extractor/src/com/semmle/js/extractor/ASTExtractor.java
@@ -762,6 +762,7 @@ public class ASTExtractor {
        trapwriter.addTuple("hasDeclareKeyword", key);
      }
      extractFunction(nd, key);
+      emitStaticType(nd, key);
      return key;
    }

@@ -833,7 +834,13 @@ public class ASTExtractor {
      extractParameterDefaultsAndTypes(nd, key, i);

      extractFunctionAttributes(nd, key);
+
+      // Extract associated symbol and signature
      emitNodeSymbol(nd, key);
+      if (nd.getDeclaredSignatureId() != -1) {
+        Label signatureKey = trapwriter.globalID("signature;" + nd.getDeclaredSignatureId());
+        trapwriter.addTuple("declared_function_signature", key, signatureKey);
+      }

      boolean oldIsStrict = isStrict;
      isStrict = bodyIsStrict;
--- a/javascript/extractor/src/com/semmle/js/extractor/Main.java
+++ b/javascript/extractor/src/com/semmle/js/extractor/Main.java
@@ -1,5 +1,13 @@
 package com.semmle.js.extractor;

+import java.io.File;
+import java.io.IOException;
+import java.util.ArrayList;
+import java.util.LinkedHashSet;
+import java.util.List;
+import java.util.Set;
+import java.util.regex.Pattern;
+
 import com.semmle.js.extractor.ExtractorConfig.HTMLHandling;
 import com.semmle.js.extractor.ExtractorConfig.Platform;
 import com.semmle.js.extractor.ExtractorConfig.SourceType;
@@ -23,13 +31,6 @@ import com.semmle.util.language.LegacyLanguage;
 import com.semmle.util.process.ArgsParser;
 import com.semmle.util.process.ArgsParser.FileMode;
 import com.semmle.util.trap.TrapWriter;
-import java.io.File;
-import java.io.IOException;
-import java.util.ArrayList;
-import java.util.LinkedHashSet;
-import java.util.List;
-import java.util.Set;
-import java.util.regex.Pattern;

 /** The main entry point of the JavaScript extractor. */
 public class Main {
@@ -37,7 +38,7 @@ public class Main {
   * A version identifier that should be updated every time the extractor changes in such a way that
   * it may produce different tuples for the same file under the same {@link ExtractorConfig}.
   */
-  public static final String EXTRACTOR_VERSION = "2019-09-13";
+  public static final String EXTRACTOR_VERSION = "2019-09-18";

  public static final Pattern NEWLINE = Pattern.compile("\n");

--- a/javascript/extractor/src/com/semmle/js/parser/TypeScriptASTConverter.java
+++ b/javascript/extractor/src/com/semmle/js/parser/TypeScriptASTConverter.java
@@ -42,6 +42,7 @@ import com.semmle.js.ast.ForOfStatement;
 import com.semmle.js.ast.ForStatement;
 import com.semmle.js.ast.FunctionDeclaration;
 import com.semmle.js.ast.FunctionExpression;
+import com.semmle.js.ast.IFunction;
 import com.semmle.js.ast.INode;
 import com.semmle.js.ast.IPattern;
 import com.semmle.js.ast.Identifier;
@@ -670,6 +671,13 @@ public class TypeScriptASTConverter {
    attachSymbolInformation(node, json);
  }

+  /** Attached the declared call signature to a function. */
+  private void attachDeclaredSignature(IFunction node, JsonObject json) {
+    if (json.has("$declaredSignature")) {
+      node.setDeclaredSignatureId(json.get("$declaredSignature").getAsInt());
+    }
+  }
+
  /**
   * Convert the given array of TypeScript AST nodes into a list of JavaScript AST nodes, skipping
   * any {@code null} elements.
@@ -786,15 +794,18 @@ public class TypeScriptASTConverter {
  }

  private Node convertArrowFunction(JsonObject node, SourceLocation loc) throws ParseError {
-    return new ArrowFunctionExpression(
-        loc,
-        convertParameters(node),
-        convertChild(node, "body"),
-        false,
-        hasModifier(node, "AsyncKeyword"),
-        convertChildrenNotNull(node, "typeParameters"),
-        convertParameterTypes(node),
-        convertChildAsType(node, "type"));
+    ArrowFunctionExpression function =
+        new ArrowFunctionExpression(
+            loc,
+            convertParameters(node),
+            convertChild(node, "body"),
+            false,
+            hasModifier(node, "AsyncKeyword"),
+            convertChildrenNotNull(node, "typeParameters"),
+            convertParameterTypes(node),
+            convertChildAsType(node, "type"));
+    attachDeclaredSignature(function, node);
+    return function;
  }

  private Node convertAwaitExpression(JsonObject node, SourceLocation loc) throws ParseError {
@@ -1044,6 +1055,8 @@ public class TypeScriptASTConverter {
            null,
            null);
    attachSymbolInformation(value, node);
+    attachStaticType(value, node);
+    attachDeclaredSignature(value, node);
    List<FieldDefinition> parameterFields = convertParameterFields(node);
    return new MethodDefinition(loc, flags, methodKind, key, value, parameterFields);
  }
@@ -1234,6 +1247,8 @@ public class TypeScriptASTConverter {
            returnType,
            thisParam);
    attachSymbolInformation(function, node);
+    attachStaticType(function, node);
+    attachDeclaredSignature(function, node);
    return fixExports(loc, function);
  }

@@ -1247,18 +1262,22 @@ public class TypeScriptASTConverter {
    List<DecoratorList> paramDecorators = convertParameterDecorators(node);
    ITypeExpression returnType = convertChildAsType(node, "type");
    ITypeExpression thisParam = convertThisParameterType(node);
-    return new FunctionExpression(
-        loc,
-        fnId,
-        params,
-        fnbody,
-        generator,
-        async,
-        convertChildrenNotNull(node, "typeParameters"),
-        paramTypes,
-        paramDecorators,
-        returnType,
-        thisParam);
+    FunctionExpression function =
+        new FunctionExpression(
+            loc,
+            fnId,
+            params,
+            fnbody,
+            generator,
+            async,
+            convertChildrenNotNull(node, "typeParameters"),
+            paramTypes,
+            paramDecorators,
+            returnType,
+            thisParam);
+    attachStaticType(function, node);
+    attachDeclaredSignature(function, node);
+    return function;
  }

  private Node convertFunctionType(JsonObject node, SourceLocation loc) throws ParseError {
@@ -1591,7 +1610,7 @@ public class TypeScriptASTConverter {
    List<DecoratorList> paramDecorators = convertParameterDecorators(node);
    List<TypeParameter> typeParameters = convertChildrenNotNull(node, "typeParameters");
    ITypeExpression thisType = convertThisParameterType(node);
-    FunctionExpression method =
+    FunctionExpression function =
        new FunctionExpression(
            loc,
            null,
@@ -1604,8 +1623,10 @@ public class TypeScriptASTConverter {
            paramDecorators,
            returnType,
            thisType);
-    attachSymbolInformation(method, node);
-    return method;
+    attachSymbolInformation(function, node);
+    attachStaticType(function, node);
+    attachDeclaredSignature(function, node);
+    return function;
  }

  private Node convertNamespaceDeclaration(JsonObject node, SourceLocation loc) throws ParseError {
--- a/javascript/ql/src/semmle/javascript/Classes.qll
+++ b/javascript/ql/src/semmle/javascript/Classes.qll
@@ -48,6 +48,9 @@ class ClassOrInterface extends @classorinterface, TypeParameterized {
  /** Gets a member declared in this class or interface. */
  MemberDeclaration getAMember() { result.getDeclaringType() = this }

+  /** Gets the `i`th member declared in this class or interface. */
+  MemberDeclaration getMemberByIndex(int i) { properties(result, this, i, _, _) }
+
  /** Gets the member with the given name declared in this class or interface. */
  MemberDeclaration getMember(string name) {
    result = getAMember() and
@@ -57,9 +60,19 @@ class ClassOrInterface extends @classorinterface, TypeParameterized {
  /** Gets a method declared in this class or interface. */
  MethodDeclaration getAMethod() { result = getAMember() }

-  /** Gets the method with the given name declared in this class or interface. */
+  /**
+   * Gets the method with the given name declared in this class or interface.
+   *
+   * Note that for overloaded method signatures in TypeScript files, this returns every overload.
+   */
  MethodDeclaration getMethod(string name) { result = getMember(name) }

+  /** Gets an overloaded version of the method with the given name declared in this class or interface. */
+  MethodDeclaration getMethodOverload(string name, int overloadIndex) {
+    result = getMethod(name) and
+    overloadIndex = result.getOverloadIndex()
+  }
+
  /** Gets a field declared in this class or interface. */
  FieldDeclaration getAField() { result = getAMember() }

@@ -523,6 +536,9 @@ class MemberDeclaration extends @property, Documentable {
  /** Gets the class this member belongs to, if any. */
  ClassDefinition getDeclaringClass() { properties(this, result, _, _, _) }

+  /** Gets the index of this member within its enclosing type. */
+  int getMemberIndex() { properties(this, _, result, _, _) }
+
  /** Gets the nearest enclosing function or toplevel in which this member occurs. */
  StmtContainer getContainer() { result = getDeclaringType().getContainer() }

@@ -642,6 +658,80 @@ class MethodDeclaration extends MemberDeclaration {
   * Gets the body of this method.
   */
  FunctionExpr getBody() { result = getChildExpr(1) }
+
+  /**
+   * Holds if this method is overloaded, that is, there are multiple method
+   * signatures with its name declared in the enclosing type.
+   */
+  predicate isOverloaded() {
+    not this instanceof ConstructorDeclaration and
+    hasOverloadedMethod(getDeclaringType(), getName())
+    or
+    this instanceof ConstructorDeclaration and
+    hasOverloadedConstructor(getDeclaringClass())
+  }
+
+  /**
+   * Gets the index of this method declaration among all the method declarations
+   * with this name.
+   *
+   * In the rare case of a class containing multiple concrete methods with the same name,
+   * the overload index is defined as if only one of them was concrete.
+   */
+  int getOverloadIndex() {
+    exists(ClassOrInterface type, string name |
+      this = rank[result + 1](MethodDeclaration method, int i |
+          methodDeclaredInType(type, name, i, method)
+        |
+          method order by i
+        )
+    )
+    or
+    exists(ClassDefinition type |
+      this = rank[result + 1](ConstructorDeclaration ctor, int i |
+          ctor = type.getMemberByIndex(i)
+        |
+          ctor order by i
+        )
+    )
+  }
+}
+
+/**
+ * Holds if the `index`th member of `type` is `method`, which has the given `name`.
+ */
+private predicate methodDeclaredInType(
+  ClassOrInterface type, string name, int index, MethodDeclaration method
+) {
+  not method instanceof ConstructorDeclaration and // distinguish methods named "constructor" from the constructor
+  type.getMemberByIndex(index) = method and
+  method.getName() = name
+}
+
+/**
+ * Holds if `type` has an overloaded method named `name`.
+ */
+private predicate hasOverloadedMethod(ClassOrInterface type, string name) {
+  exists(MethodDeclaration method |
+    method = type.getMethod(name) and
+    not method instanceof ConstructorDeclaration and
+    method.getOverloadIndex() > 0
+  )
+}
+
+/** Holds if `type` has an overloaded constructor declaration. */
+private predicate hasOverloadedConstructor(ClassDefinition type) {
+  type.getConstructor().getOverloadIndex() > 0
+}
+
+/** Holds if `type` has an overloaded function call signature. */
+private predicate hasOverloadedFunctionCallSignature(ClassOrInterface type) {
+  type.getACallSignature().(FunctionCallSignature).getOverloadIndex() > 0
+}
+
+/** Holds if `type` has an overloaded constructor call signature. */
+private predicate hasOverloadedConstructorCallSignature(ClassOrInterface type) {
+  type.getACallSignature().(ConstructorCallSignature).getOverloadIndex() > 0
 }

 /**
@@ -1048,7 +1138,24 @@ class CallSignature extends @call_signature, MemberSignature {
 * }
 * ```
 */
-class FunctionCallSignature extends @function_call_signature, CallSignature { }
+class FunctionCallSignature extends @function_call_signature, CallSignature {
+  /** Gets the index of this function call signature among the function call signatures in the enclosing type. */
+  int getOverloadIndex() {
+    exists(ClassOrInterface type | type = getDeclaringType() |
+      this = rank[result + 1](FunctionCallSignature sig, int i |
+          sig = type.getMemberByIndex(i)
+        |
+          sig order by i
+        )
+    )
+  }
+
+  /**
+   * Holds if this function call signature is overloaded, that is, there are multiple function call
+   * signatures declared in the enclosing type.
+   */
+  predicate isOverloaded() { hasOverloadedFunctionCallSignature(getDeclaringType()) }
+}

 /**
 * A constructor call signature declared in an interface.
@@ -1061,7 +1168,24 @@ class FunctionCallSignature extends @function_call_signature, CallSignature { }
 * }
 * ```
 */
-class ConstructorCallSignature extends @constructor_call_signature, CallSignature { }
+class ConstructorCallSignature extends @constructor_call_signature, CallSignature {
+  /** Gets the index of this constructor call signature among the constructor call signatures in the enclosing type. */
+  int getOverloadIndex() {
+    exists(ClassOrInterface type | type = getDeclaringType() |
+      this = rank[result + 1](ConstructorCallSignature sig, int i |
+          sig = type.getMemberByIndex(i)
+        |
+          sig order by i
+        )
+    )
+  }
+
+  /**
+   * Holds if this constructor call signature is overloaded, that is, there are multiple constructor call
+   * signatures declared in the enclosing type.
+   */
+  predicate isOverloaded() { hasOverloadedConstructorCallSignature(getDeclaringType()) }
+}

 /**
 * An index signature declared in an interface.
--- a/javascript/ql/src/semmle/javascript/Functions.qll
+++ b/javascript/ql/src/semmle/javascript/Functions.qll
@@ -416,6 +416,13 @@ class Function extends @function, Parameterized, TypeParameterized, StmtContaine
   * This predicate is only populated for files extracted with full TypeScript extraction.
   */
  CanonicalFunctionName getCanonicalName() { ast_node_symbol(this, result) }
+
+  /**
+   * Gets the call signature of this function, as determined by the TypeScript compiler, if any.
+   */
+  CallSignatureType getCallSignature() {
+    declared_function_signature(this, result)
+  }
 }

 /**
--- a/javascript/ql/src/semmle/javascript/security/dataflow/Xss.qll
+++ b/javascript/ql/src/semmle/javascript/security/dataflow/Xss.qll
@@ -34,7 +34,7 @@ module Shared {
    MetacharEscapeSanitizer() {
      getMethodName() = "replace" and
      exists(RegExpConstant c |
-        c.getLiteral() = getArgument(0).asExpr() and
+        c.getLiteral() = getArgument(0).getALocalSource().asExpr() and
        c.getValue().regexpMatch("['\"&<>]")
      )
    }
--- a/javascript/ql/src/semmlecode.javascript.dbscheme
+++ b/javascript/ql/src/semmlecode.javascript.dbscheme
@@ -641,6 +641,11 @@ ast_node_type(
  unique int node: @typed_ast_node ref, 
  int typ: @type ref);

+declared_function_signature(
+  unique int node: @function ref,
+  int sig: @signature_type ref
+);
+
 invoke_expr_signature(
  unique int node: @invokeexpr ref,
  int sig: @signature_type ref
--- a/javascript/ql/src/semmlecode.javascript.dbscheme.stats
+++ b/javascript/ql/src/semmlecode.javascript.dbscheme.stats
@@ -16715,6 +16715,69 @@
 </dependencies>
 </relation>
 <relation>
+<name>declared_function_signature</name>
+<cardinality>62664</cardinality>
+<columnsizes>
+<e>
+<k>node</k>
+<v>62664</v>
+</e>
+<e>
+<k>sig</k>
+<v>21731</v>
+</e>
+</columnsizes>
+<dependencies>
+<dep>
+<src>node</src>
+<trg>sig</trg>
+<val>
+<hist>
+<budget>12</budget>
+<bs>
+<b>
+<a>1</a>
+<b>2</b>
+<v>62664</v>
+</b>
+</bs>
+</hist>
+</val>
+</dep>
+<dep>
+<src>sig</src>
+<trg>node</trg>
+<val>
+<hist>
+<budget>12</budget>
+<bs>
+<b>
+<a>1</a>
+<b>2</b>
+<v>16826</v>
+</b>
+<b>
+<a>2</a>
+<b>3</b>
+<v>2358</v>
+</b>
+<b>
+<a>3</a>
+<b>6</b>
+<v>1683</v>
+</b>
+<b>
+<a>6</a>
+<b>10251</b>
+<v>864</v>
+</b>
+</bs>
+</hist>
+</val>
+</dep>
+</dependencies>
+</relation>
+<relation>
 <name>invoke_expr_signature</name>
 <cardinality>140668</cardinality>
 <columnsizes>
--- a/javascript/ql/test/library-tests/TypeScript/CallSignatureTypes/ExprSignatures.expected
+++ b/javascript/ql/test/library-tests/TypeScript/CallSignatureTypes/ExprSignatures.expected
@@ -1,31 +0,0 @@
-| tst.ts:2:4:2:4 | x | number |
-| tst.ts:6:4:6:4 | x | number |
-| tst.ts:7:4:7:4 | x | string |
-| tst.ts:8:4:8:4 | x | any |
-| tst.ts:12:8:12:8 | x | number |
-| tst.ts:16:8:16:8 | x | number |
-| tst.ts:17:8:17:8 | x | any |
-| tst.ts:21:10:21:10 | x | number |
-| tst.ts:23:20:23:20 | x | number |
-| tst.ts:24:20:24:20 | x | string |
-| tst.ts:25:20:25:20 | x | any |
-| tst.ts:28:5:28:5 | m | Method |
-| tst.ts:29:1:29:1 | m | Method |
-| tst.ts:29:1:29:8 | m.method | (x: number): string |
-| tst.ts:29:1:29:12 | m.method(42) | string |
-| tst.ts:29:10:29:11 | 42 | 42 |
-| tst.ts:30:1:30:1 | m | Method |
-| tst.ts:30:1:30:18 | m.overloadedMethod | (x: any): any |
-| tst.ts:30:1:30:18 | m.overloadedMethod | (x: number): number |
-| tst.ts:30:1:30:18 | m.overloadedMethod | (x: string): string |
-| tst.ts:30:1:30:25 | m.overl ... ("foo") | string |
-| tst.ts:30:20:30:24 | "foo" | "foo" |
-| tst.ts:33:3:33:10 | callback | (x: number): string |
-| tst.ts:33:14:33:14 | x | number |
-| tst.ts:37:10:37:10 | x | T |
-| tst.ts:40:10:40:12 | foo | (g: Generic<string>): string |
-| tst.ts:40:14:40:14 | g | Generic<string> |
-| tst.ts:41:10:41:10 | g | Generic<string> |
-| tst.ts:41:10:41:17 | g.method | (x: string): string |
-| tst.ts:41:10:41:24 | g.method("foo") | string |
-| tst.ts:41:19:41:23 | "foo" | "foo" |
--- a/javascript/ql/test/library-tests/TypeScript/CallSignatureTypes/ExprSignatures.ql
+++ b/javascript/ql/test/library-tests/TypeScript/CallSignatureTypes/ExprSignatures.ql
@@ -1,14 +0,0 @@
-import javascript
-
-string getASignatureOrElseType(Type t) {
-  result = t.getASignature(_).toString()
-  or
-  not exists(t.getASignature(_)) and
-  result = t.toString()
-}
-
-from Expr expr
-where
-  not exists(MethodDeclaration decl | decl.getNameExpr() = expr) and
-  not exists(DotExpr dot | expr = dot.getPropertyNameExpr())
-select expr, getASignatureOrElseType(expr.getType())
--- a/javascript/ql/test/library-tests/TypeScript/CallSignatureTypes/Signatures.expected
+++ b/javascript/ql/test/library-tests/TypeScript/CallSignatureTypes/Signatures.expected
@@ -1,7 +0,0 @@
-| Callable | function | 0 | (x: number): string |
-| Newable | constructor | 0 | new (x: number): any |
-| OverloadedCallable | function | 0 | (x: number): number |
-| OverloadedCallable | function | 1 | (x: string): string |
-| OverloadedCallable | function | 2 | (x: any): any |
-| OverloadedNewable | constructor | 0 | new (x: number): OverloadedNewable |
-| OverloadedNewable | constructor | 1 | new (x: any): any |
--- a/javascript/ql/test/library-tests/TypeScript/CallSignatureTypes/Signatures.ql
+++ b/javascript/ql/test/library-tests/TypeScript/CallSignatureTypes/Signatures.ql
@@ -1,4 +0,0 @@
-import javascript
-
-from TypeReference type, SignatureKind kind, int n
-select type, kind, n, type.getSignature(kind, n)
--- a/javascript/ql/test/library-tests/TypeScript/CallSignatureTypes/test.expected
+++ b/javascript/ql/test/library-tests/TypeScript/CallSignatureTypes/test.expected
@@ -0,0 +1,74 @@
+test_ExprSignature
+| tst.ts:2:4:2:4 | x | number |
+| tst.ts:6:4:6:4 | x | number |
+| tst.ts:7:4:7:4 | x | string |
+| tst.ts:8:4:8:4 | x | any |
+| tst.ts:12:8:12:8 | x | number |
+| tst.ts:16:8:16:8 | x | number |
+| tst.ts:17:8:17:8 | x | any |
+| tst.ts:21:3:21:28 | method( ... string; | (x: number): string |
+| tst.ts:21:10:21:10 | x | number |
+| tst.ts:23:3:23:38 | overloa ... number; | (x: any): any |
+| tst.ts:23:3:23:38 | overloa ... number; | (x: number): number |
+| tst.ts:23:3:23:38 | overloa ... number; | (x: string): string |
+| tst.ts:23:20:23:20 | x | number |
+| tst.ts:24:3:24:38 | overloa ... string; | (x: any): any |
+| tst.ts:24:3:24:38 | overloa ... string; | (x: number): number |
+| tst.ts:24:3:24:38 | overloa ... string; | (x: string): string |
+| tst.ts:24:20:24:20 | x | string |
+| tst.ts:25:3:25:32 | overloa ... ): any; | (x: any): any |
+| tst.ts:25:3:25:32 | overloa ... ): any; | (x: number): number |
+| tst.ts:25:3:25:32 | overloa ... ): any; | (x: string): string |
+| tst.ts:25:20:25:20 | x | any |
+| tst.ts:28:5:28:5 | m | Method |
+| tst.ts:29:1:29:1 | m | Method |
+| tst.ts:29:1:29:8 | m.method | (x: number): string |
+| tst.ts:29:1:29:12 | m.method(42) | string |
+| tst.ts:29:10:29:11 | 42 | 42 |
+| tst.ts:30:1:30:1 | m | Method |
+| tst.ts:30:1:30:18 | m.overloadedMethod | (x: any): any |
+| tst.ts:30:1:30:18 | m.overloadedMethod | (x: number): number |
+| tst.ts:30:1:30:18 | m.overloadedMethod | (x: string): string |
+| tst.ts:30:1:30:25 | m.overl ... ("foo") | string |
+| tst.ts:30:20:30:24 | "foo" | "foo" |
+| tst.ts:33:3:33:10 | callback | (x: number): string |
+| tst.ts:33:13:33:33 | (x: num ...  string | (x: number): string |
+| tst.ts:33:14:33:14 | x | number |
+| tst.ts:37:3:37:18 | method(x: T): T; | (x: T): T |
+| tst.ts:37:10:37:10 | x | T |
+| tst.ts:40:10:40:12 | foo | (g: Generic<string>): string |
+| tst.ts:40:14:40:14 | g | Generic<string> |
+| tst.ts:41:10:41:10 | g | Generic<string> |
+| tst.ts:41:10:41:17 | g.method | (x: string): string |
+| tst.ts:41:10:41:24 | g.method("foo") | string |
+| tst.ts:41:19:41:23 | "foo" | "foo" |
+| tst.ts:44:15:44:15 | C | C |
+| tst.ts:45:3:45:25 | constru ... tring); | any |
+| tst.ts:45:15:45:15 | x | string |
+| tst.ts:46:3:46:25 | constru ... umber); | any |
+| tst.ts:46:15:46:15 | x | number |
+test_TypeReferenceSig
+| Callable | function | 0 | (x: number): string |
+| Newable | constructor | 0 | new (x: number): any |
+| OverloadedCallable | function | 0 | (x: number): number |
+| OverloadedCallable | function | 1 | (x: string): string |
+| OverloadedCallable | function | 2 | (x: any): any |
+| OverloadedNewable | constructor | 0 | new (x: number): OverloadedNewable |
+| OverloadedNewable | constructor | 1 | new (x: any): any |
+test_FunctionCallSig
+| tst.ts:2:3:2:22 | (x: number): string; | (x: number): string |
+| tst.ts:6:3:6:22 | (x: number): number; | (x: number): number |
+| tst.ts:7:3:7:22 | (x: string): string; | (x: string): string |
+| tst.ts:8:3:8:16 | (x: any): any; | (x: any): any |
+| tst.ts:12:3:12:23 | new (x: ... ): any; | new (x: number): any |
+| tst.ts:16:3:16:37 | new (x: ... ewable; | new (x: number): OverloadedNewable |
+| tst.ts:17:3:17:20 | new (x: any): any; | new (x: any): any |
+| tst.ts:21:3:21:28 | method( ... string; | (x: number): string |
+| tst.ts:23:3:23:38 | overloa ... number; | (x: number): number |
+| tst.ts:24:3:24:38 | overloa ... string; | (x: string): string |
+| tst.ts:25:3:25:32 | overloa ... ): any; | (x: any): any |
+| tst.ts:33:13:33:33 | (x: num ...  string | (x: number): string |
+| tst.ts:37:3:37:18 | method(x: T): T; | (x: T): T |
+| tst.ts:40:1:42:1 | functio ... oo");\\n} | (g: Generic<string>): string |
+| tst.ts:45:3:45:25 | constru ... tring); | new (x: string): C |
+| tst.ts:46:3:46:25 | constru ... umber); | new (x: number): C |
--- a/javascript/ql/test/library-tests/TypeScript/CallSignatureTypes/test.ql
+++ b/javascript/ql/test/library-tests/TypeScript/CallSignatureTypes/test.ql
@@ -0,0 +1,22 @@
+import javascript
+
+string getASignatureOrElseType(Type t) {
+  result = t.getASignature(_).toString()
+  or
+  not exists(t.getASignature(_)) and
+  result = t.toString()
+}
+
+query predicate test_ExprSignature(Expr expr, string type) {
+  not exists(MethodDeclaration decl | decl.getNameExpr() = expr) and
+  not exists(DotExpr dot | expr = dot.getPropertyNameExpr()) and
+  type = getASignatureOrElseType(expr.getType())
+}
+
+query predicate test_TypeReferenceSig(TypeReference type, SignatureKind kind, int n, CallSignatureType sig) {
+  sig = type.getSignature(kind, n)
+}
+
+query predicate test_FunctionCallSig(Function f, CallSignatureType sig) {
+  sig = f.getCallSignature()
+}
--- a/javascript/ql/test/library-tests/TypeScript/CallSignatureTypes/tst.ts
+++ b/javascript/ql/test/library-tests/TypeScript/CallSignatureTypes/tst.ts
@@ -40,3 +40,8 @@ interface Generic<T> {
 function foo(g: Generic<string>) {
  return g.method("foo");
 }
+
+declare class C {
+  constructor(x: string);
+  constructor(x: number);
+}
--- a/javascript/ql/test/library-tests/TypeScript/CallSignatures/CallSignatures.expected
+++ b/javascript/ql/test/library-tests/TypeScript/CallSignatures/CallSignatures.expected
@@ -1,4 +0,0 @@
-| tst.ts:7:3:7:22 | (x: number): number; | interface I | tst.ts:7:3:7:22 | (x: number): number; | abstract |
-| tst.ts:8:3:8:21 | new (x: number): C; | interface I | tst.ts:8:3:8:21 | new (x: number): C; | abstract |
-| tst.ts:13:3:13:22 | (x: number): number; | anonymous interface | tst.ts:13:3:13:22 | (x: number): number; | abstract |
-| tst.ts:14:3:14:21 | new (x: number): C; | anonymous interface | tst.ts:14:3:14:21 | new (x: number): C; | abstract |
--- a/javascript/ql/test/library-tests/TypeScript/CallSignatures/CallSignatures.ql
+++ b/javascript/ql/test/library-tests/TypeScript/CallSignatures/CallSignatures.ql
@@ -1,5 +0,0 @@
-import javascript
-
-from CallSignature call, string abstractness
-where if call.isAbstract() then abstractness = "abstract" else abstractness = "not abstract"
-select call, call.getDeclaringType().describe(), call.getBody(), abstractness
--- a/javascript/ql/test/library-tests/TypeScript/CallSignatures/IndexSignatures.expected
+++ b/javascript/ql/test/library-tests/TypeScript/CallSignatures/IndexSignatures.expected
@@ -1,2 +0,0 @@
-| tst.ts:9:3:9:22 | [x: number]: string; | interface I | tst.ts:9:3:9:22 | [x: number]: string; | abstract |
-| tst.ts:15:3:15:22 | [x: number]: string; | anonymous interface | tst.ts:15:3:15:22 | [x: number]: string; | abstract |
--- a/javascript/ql/test/library-tests/TypeScript/CallSignatures/IndexSignatures.ql
+++ b/javascript/ql/test/library-tests/TypeScript/CallSignatures/IndexSignatures.ql
@@ -1,5 +0,0 @@
-import javascript
-
-from IndexSignature sig, string abstractness
-where if sig.isAbstract() then abstractness = "abstract" else abstractness = "not abstract"
-select sig, sig.getDeclaringType().describe(), sig.getBody(), abstractness
--- a/javascript/ql/test/library-tests/TypeScript/CallSignatures/MethodDeclarations.expected
+++ b/javascript/ql/test/library-tests/TypeScript/CallSignatures/MethodDeclarations.expected
@@ -1,3 +0,0 @@
-| tst.ts:1:18:1:17 | constructor() {} | Method constructor in class C |
-| tst.ts:2:3:2:31 | abstrac ... number; | Method abstract in class C |
-| tst.ts:3:3:3:30 | abstrac ... er): C; | Method new in class C |
--- a/javascript/ql/test/library-tests/TypeScript/CallSignatures/MethodDeclarations.ql
+++ b/javascript/ql/test/library-tests/TypeScript/CallSignatures/MethodDeclarations.ql
@@ -1,4 +0,0 @@
-import javascript
-
-from MethodDeclaration method
-select method, "Method " + method.getName() + " in " + method.getDeclaringType().describe()
--- a/javascript/ql/test/library-tests/TypeScript/CallSignatures/test.expected
+++ b/javascript/ql/test/library-tests/TypeScript/CallSignatures/test.expected
@@ -0,0 +1,66 @@
+test_CallSignature
+| tst.ts:7:3:7:22 | (x: number): number; | interface I | tst.ts:7:3:7:22 | (x: number): number; | abstract |
+| tst.ts:8:3:8:21 | new (x: number): C; | interface I | tst.ts:8:3:8:21 | new (x: number): C; | abstract |
+| tst.ts:13:3:13:22 | (x: number): number; | anonymous interface | tst.ts:13:3:13:22 | (x: number): number; | abstract |
+| tst.ts:14:3:14:21 | new (x: number): C; | anonymous interface | tst.ts:14:3:14:21 | new (x: number): C; | abstract |
+| tst.ts:47:3:47:14 | (x: number); | interface ICallSigOverloads | tst.ts:47:3:47:14 | (x: number); | abstract |
+| tst.ts:48:3:48:17 | new(x: number); | interface ICallSigOverloads | tst.ts:48:3:48:17 | new(x: number); | abstract |
+| tst.ts:49:3:49:14 | (x: string); | interface ICallSigOverloads | tst.ts:49:3:49:14 | (x: string); | abstract |
+| tst.ts:50:3:50:17 | new(x: string); | interface ICallSigOverloads | tst.ts:50:3:50:17 | new(x: string); | abstract |
+| tst.ts:52:3:52:17 | new(x: number); | interface ICallSigOverloads | tst.ts:52:3:52:17 | new(x: number); | abstract |
+| tst.ts:53:3:53:14 | (x: number); | interface ICallSigOverloads | tst.ts:53:3:53:14 | (x: number); | abstract |
+test_IndexSignature
+| tst.ts:9:3:9:22 | [x: number]: string; | interface I | tst.ts:9:3:9:22 | [x: number]: string; | abstract |
+| tst.ts:15:3:15:22 | [x: number]: string; | anonymous interface | tst.ts:15:3:15:22 | [x: number]: string; | abstract |
+test_MethodDeclarations
+| tst.ts:1:18:1:17 | constructor() {} | Method constructor in class C |
+| tst.ts:2:3:2:31 | abstrac ... number; | Method abstract in class C |
+| tst.ts:3:3:3:30 | abstrac ... er): C; | Method new in class C |
+| tst.ts:19:3:19:17 | foo(x: number); | Method foo in interface IOverloads |
+| tst.ts:20:3:20:17 | foo(x: string); | Method foo in interface IOverloads |
+| tst.ts:21:3:21:8 | bar(); | Method bar in interface IOverloads |
+| tst.ts:22:3:22:17 | foo(x: number); | Method foo in interface IOverloads |
+| tst.ts:25:27:25:26 | constructor() {} | Method constructor in class COverloads |
+| tst.ts:26:3:26:26 | abstrac ... umber); | Method foo in class COverloads |
+| tst.ts:27:3:27:26 | abstrac ... tring); | Method foo in class COverloads |
+| tst.ts:28:3:28:26 | abstrac ... umber); | Method foo in class COverloads |
+| tst.ts:30:3:30:17 | bar(x: number); | Method bar in class COverloads |
+| tst.ts:31:3:31:17 | bar(x: string); | Method bar in class COverloads |
+| tst.ts:33:3:33:11 | bar(x) {} | Method bar in class COverloads |
+| tst.ts:37:3:37:25 | constru ... umber); | Method constructor in class ConstructorOverloads |
+| tst.ts:38:3:38:25 | constru ... tring); | Method constructor in class ConstructorOverloads |
+| tst.ts:40:3:40:25 | constru ... umber); | Method constructor in class ConstructorOverloads |
+| tst.ts:42:3:42:29 | ["const ... tring); | Method constructor in class ConstructorOverloads |
+| tst.ts:43:3:43:29 | ["const ... umber); | Method constructor in class ConstructorOverloads |
+test_MethodOverload
+| tst.ts:1:18:1:17 | constructor() {} | 0 | false |
+| tst.ts:2:3:2:31 | abstrac ... number; | 0 | false |
+| tst.ts:3:3:3:30 | abstrac ... er): C; | 0 | false |
+| tst.ts:19:3:19:17 | foo(x: number); | 0 | true |
+| tst.ts:20:3:20:17 | foo(x: string); | 1 | true |
+| tst.ts:21:3:21:8 | bar(); | 0 | false |
+| tst.ts:22:3:22:17 | foo(x: number); | 2 | true |
+| tst.ts:25:27:25:26 | constructor() {} | 0 | false |
+| tst.ts:26:3:26:26 | abstrac ... umber); | 0 | true |
+| tst.ts:27:3:27:26 | abstrac ... tring); | 1 | true |
+| tst.ts:28:3:28:26 | abstrac ... umber); | 2 | true |
+| tst.ts:30:3:30:17 | bar(x: number); | 0 | true |
+| tst.ts:31:3:31:17 | bar(x: string); | 1 | true |
+| tst.ts:33:3:33:11 | bar(x) {} | 2 | true |
+| tst.ts:37:3:37:25 | constru ... umber); | 0 | true |
+| tst.ts:38:3:38:25 | constru ... tring); | 1 | true |
+| tst.ts:40:3:40:25 | constru ... umber); | 2 | true |
+| tst.ts:42:3:42:29 | ["const ... tring); | 0 | true |
+| tst.ts:43:3:43:29 | ["const ... umber); | 1 | true |
+test_FunctionCallSigOverload
+| tst.ts:7:3:7:22 | (x: number): number; | 0 | false |
+| tst.ts:13:3:13:22 | (x: number): number; | 0 | false |
+| tst.ts:47:3:47:14 | (x: number); | 0 | true |
+| tst.ts:49:3:49:14 | (x: string); | 1 | true |
+| tst.ts:53:3:53:14 | (x: number); | 2 | true |
+test_ConstructorCallSigOverload
+| tst.ts:8:3:8:21 | new (x: number): C; | 0 | false |
+| tst.ts:14:3:14:21 | new (x: number): C; | 0 | false |
+| tst.ts:48:3:48:17 | new(x: number); | 0 | true |
+| tst.ts:50:3:50:17 | new(x: string); | 1 | true |
+| tst.ts:52:3:52:17 | new(x: number); | 2 | true |
--- a/javascript/ql/test/library-tests/TypeScript/CallSignatures/test.ql
+++ b/javascript/ql/test/library-tests/TypeScript/CallSignatures/test.ql
@@ -0,0 +1,32 @@
+import javascript
+
+query predicate test_CallSignature(CallSignature call, string declType, ASTNode body, string abstractness) {
+  (if call.isAbstract() then abstractness = "abstract" else abstractness = "not abstract") and
+  declType = call.getDeclaringType().describe() and
+  body = call.getBody()
+}
+
+query predicate test_IndexSignature(IndexSignature sig, string declType, ASTNode body, string abstractness) {
+  (if sig.isAbstract() then abstractness = "abstract" else abstractness = "not abstract") and
+  declType = sig.getDeclaringType().describe() and
+  body = sig.getBody()
+}
+
+query predicate test_MethodDeclarations(MethodDeclaration method, string descr) {
+  descr = "Method " + method.getName() + " in " + method.getDeclaringType().describe()
+}
+
+query predicate test_MethodOverload(MethodDeclaration method, int index, boolean overloaded) {
+  index = method.getOverloadIndex() and
+  if method.isOverloaded() then overloaded = true else overloaded = false
+}
+
+query predicate test_FunctionCallSigOverload(FunctionCallSignature sig, int index, boolean overloaded) {
+  index = sig.getOverloadIndex() and
+  if sig.isOverloaded() then overloaded = true else overloaded = false
+}
+
+query predicate test_ConstructorCallSigOverload(ConstructorCallSignature sig, int index, boolean overloaded) {
+  index = sig.getOverloadIndex() and
+  if sig.isOverloaded() then overloaded = true else overloaded = false
+}
--- a/javascript/ql/test/library-tests/TypeScript/CallSignatures/tst.ts
+++ b/javascript/ql/test/library-tests/TypeScript/CallSignatures/tst.ts
@@ -14,3 +14,41 @@ var x : {
  new (x: number): C;
  [x: number]: string;
 }
+
+interface IOverloads {
+  foo(x: number);
+  foo(x: string);
+  bar();
+  foo(x: number);
+}
+
+abstract class COverloads {
+  abstract foo(x: number);
+  abstract foo(x: string);
+  abstract foo(x: number);
+
+  bar(x: number);
+  bar(x: string);
+  x = 45;
+  bar(x) {};
+}
+
+declare class ConstructorOverloads {
+  constructor(x: number);
+  constructor(x: string);
+  x: number;
+  constructor(x: number);
+
+  ["constructor"](x: string);
+  ["constructor"](x: number);
+}
+
+interface ICallSigOverloads {
+  (x: number);
+  new(x: number);
+  (x: string);
+  new(x: string);
+  field: number;
+  new(x: number);
+  (x: number);
+}
--- a/javascript/ql/test/library-tests/TypeScript/TypeVariableTypes/SignatureTypeParameters.expected
+++ b/javascript/ql/test/library-tests/TypeScript/TypeVariableTypes/SignatureTypeParameters.expected
@@ -1,5 +1,6 @@
 | <D>(x: D): D | 1 | 0 | D | no bound |
 | <E>(x: () => E): E | 1 | 0 | E | no bound |
+| <E>(x: E[] \| (() => E)): E | 1 | 0 | E | no bound |
 | <E>(x: E[]): E | 1 | 0 | E | no bound |
 | <S extends E>(callbackfn: (value: E, index: number, array: E[]) => va... | 1 | 0 | S | no bound |
 | <S extends T \| S>(callbackfn: (value: T \| S, index: number, array: (T... | 1 | 0 | S | no bound |
--- a/javascript/ql/test/library-tests/TypeScript/Types/GetExprType.expected
+++ b/javascript/ql/test/library-tests/TypeScript/Types/GetExprType.expected
@@ -64,10 +64,12 @@
 | tst.ts:22:29:22:29 | 2 | 2 |
 | tst.ts:24:5:24:9 | array | number[] |
 | tst.ts:26:5:26:12 | voidType | () => void |
+| tst.ts:26:15:26:24 | () => void | () => void |
 | tst.ts:27:5:27:17 | undefinedType | undefined |
 | tst.ts:28:5:28:12 | nullType | null |
 | tst.ts:28:22:28:25 | null | null |
 | tst.ts:29:5:29:13 | neverType | () => never |
+| tst.ts:29:16:29:26 | () => never | () => never |
 | tst.ts:30:5:30:14 | symbolType | symbol |
 | tst.ts:31:7:31:22 | uniqueSymbolType | typeof uniqueSymbolType |
 | tst.ts:31:41:31:44 | null | null |
--- a/javascript/ql/test/query-tests/Security/CWE-079/sanitiser.js
+++ b/javascript/ql/test/query-tests/Security/CWE-079/sanitiser.js
@@ -1,8 +1,9 @@
 function escapeHtml(s) {
+    var amp = /&/g, lt = /</g, gt = />/g;
    return s.toString()
-        .replace(/&/g, '&amp;')
-        .replace(/</g, '&lt;')
-        .replace(/>/g, '&gt;');
+        .replace(amp, '&amp;')
+        .replace(lt, '&lt;')
+        .replace(gt, '&gt;');
 }

 function escapeAttr(s) {
--- a/javascript/upgrades/56b74a6808d3fe01835d454c25ea8dc3da1a8fdf/old.dbscheme
+++ b/javascript/upgrades/56b74a6808d3fe01835d454c25ea8dc3da1a8fdf/old.dbscheme
--- a/javascript/upgrades/56b74a6808d3fe01835d454c25ea8dc3da1a8fdf/semmlecode.javascript.dbscheme
+++ b/javascript/upgrades/56b74a6808d3fe01835d454c25ea8dc3da1a8fdf/semmlecode.javascript.dbscheme
--- a/javascript/upgrades/56b74a6808d3fe01835d454c25ea8dc3da1a8fdf/upgrade.properties
+++ b/javascript/upgrades/56b74a6808d3fe01835d454c25ea8dc3da1a8fdf/upgrade.properties
@@ -0,0 +1,2 @@
+description: add declared function signatures to database
+compatibility: backwards
--- a/Show More
+++ b/Show More
				`@@ -0,0 +1 @@`
				`import semmle.code.csharp.ir.implementation.unaliased_ssa.IR as IR`
				`@@ -0,0 +1 @@`
				`import semmle.code.csharp.ir.IRConfiguration as IRConfiguration`
				`@@ -0,0 +1 @@`
				`semmle/code/csharp/ir/implementation/unaliased_ssa/IRSanity.ql`