Revert "Merge pull request #18057 from jketema/codeql-cli-2.19.4"

This reverts commit ed922f6519, reversing changes made to aa4cc72f30.
2026-04-28 02:05:14 +02:00 · 2024-12-04 14:32:18 +00:00
parent 32bfbb832b
commit 20dfbdc5cc
9 changed files with 755 additions and 125 deletions
--- a/cpp/ql/lib/change-notes/released/2.1.1.md
+++ b/cpp/ql/lib/change-notes/released/2.1.1.md
@@ -1,3 +1,5 @@
 ## 2.1.1

-No user-facing changes.
+### Minor Analysis Improvements
+
+* The `Guards` library (`semmle.code.cpp.controlflow.Guards`) has been improved to recognize more guard conditions. Additionally, the guards library no longer considers guards in static local initializers or global initializers as `GuardCondition`s.
--- a/cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll
+++ b/cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll
@@ -5,6 +5,7 @@

 import cpp
 import semmle.code.cpp.ir.IR
+private import semmle.code.cpp.ir.ValueNumbering
 private import semmle.code.cpp.ir.implementation.raw.internal.TranslatedExpr
 private import semmle.code.cpp.ir.implementation.raw.internal.InstructionTag

@@ -59,7 +60,91 @@ class MatchValue extends AbstractValue, TMatchValue {
 }

 /**
- * A Boolean condition in the AST that guards one or more basic blocks.
+ * A value number such that at least one of the instructions is
+ * a `CompareInstruction`.
+ */
+private class CompareValueNumber extends ValueNumber {
+  CompareInstruction cmp;
+
+  CompareValueNumber() { cmp = this.getAnInstruction() }
+
+  /** Gets a `CompareInstruction` belonging to this value number. */
+  CompareInstruction getCompareInstruction() { result = cmp }
+
+  /**
+   * Gets the left and right operands of a `CompareInstruction` that
+   * belong to this value number.
+   */
+  predicate hasOperands(Operand left, Operand right) {
+    left = cmp.getLeftOperand() and
+    right = cmp.getRightOperand()
+  }
+}
+
+private class CompareEQValueNumber extends CompareValueNumber {
+  override CompareEQInstruction cmp;
+}
+
+private class CompareNEValueNumber extends CompareValueNumber {
+  override CompareNEInstruction cmp;
+}
+
+private class CompareLTValueNumber extends CompareValueNumber {
+  override CompareLTInstruction cmp;
+}
+
+private class CompareGTValueNumber extends CompareValueNumber {
+  override CompareGTInstruction cmp;
+}
+
+private class CompareLEValueNumber extends CompareValueNumber {
+  override CompareLEInstruction cmp;
+}
+
+private class CompareGEValueNumber extends CompareValueNumber {
+  override CompareGEInstruction cmp;
+}
+
+/**
+ * A value number such that at least one of the instructions provides
+ * the integer value controlling a  `SwitchInstruction`.
+ */
+private class SwitchConditionValueNumber extends ValueNumber {
+  SwitchInstruction switch;
+
+  pragma[nomagic]
+  SwitchConditionValueNumber() { this.getAnInstruction() = switch.getExpression() }
+
+  /** Gets an expression that belongs to this value number. */
+  Operand getExpressionOperand() { result = switch.getExpressionOperand() }
+
+  Instruction getSuccessor(CaseEdge kind) { result = switch.getSuccessor(kind) }
+}
+
+private class BuiltinExpectCallValueNumber extends ValueNumber {
+  BuiltinExpectCallInstruction instr;
+
+  BuiltinExpectCallValueNumber() { this.getAnInstruction() = instr }
+
+  ValueNumber getCondition() { result.getAnInstruction() = instr.getCondition() }
+
+  Operand getAUse() { result = instr.getAUse() }
+}
+
+private class LogicalNotValueNumber extends ValueNumber {
+  LogicalNotInstruction instr;
+
+  LogicalNotValueNumber() { this.getAnInstruction() = instr }
+
+  ValueNumber getUnary() { result.getAnInstruction() = instr.getUnary() }
+}
+
+/**
+ * A Boolean condition in the AST that guards one or more basic blocks. This includes
+ * operands of logical operators but not switch statements.
+ *
+ * For performance reasons conditions inside static local initializers or
+ * global initializers are not considered `GuardCondition`s.
 */
 cached
 class GuardCondition extends Expr {
@@ -369,6 +454,9 @@ private predicate nonExcludedIRAndBasicBlock(IRBlock irb, BasicBlock controlled)
 *
 * Note that `&&` and `||` don't have an explicit representation in the IR,
 * and therefore will not appear as IRGuardConditions.
+ *
+ * For performance reasons conditions inside static local initializers or
+ * global initializers are not considered `IRGuardCondition`s.
 */
 cached
 class IRGuardCondition extends Instruction {
@@ -517,7 +605,7 @@ class IRGuardCondition extends Instruction {
  cached
  predicate comparesLt(Operand left, Operand right, int k, boolean isLessThan, boolean testIsTrue) {
    exists(BooleanValue value |
-      compares_lt(this, left, right, k, isLessThan, value) and
+      compares_lt(valueNumber(this), left, right, k, isLessThan, value) and
      value.getValue() = testIsTrue
    )
  }
@@ -528,7 +616,7 @@ class IRGuardCondition extends Instruction {
   */
  cached
  predicate comparesLt(Operand op, int k, boolean isLessThan, AbstractValue value) {
-    compares_lt(this, op, k, isLessThan, value)
+    compares_lt(valueNumber(this), op, k, isLessThan, value)
  }

  /**
@@ -538,7 +626,8 @@ class IRGuardCondition extends Instruction {
  cached
  predicate ensuresLt(Operand left, Operand right, int k, IRBlock block, boolean isLessThan) {
    exists(AbstractValue value |
-      compares_lt(this, left, right, k, isLessThan, value) and this.valueControls(block, value)
+      compares_lt(valueNumber(this), left, right, k, isLessThan, value) and
+      this.valueControls(block, value)
    )
  }

@@ -549,7 +638,8 @@ class IRGuardCondition extends Instruction {
  cached
  predicate ensuresLt(Operand op, int k, IRBlock block, boolean isLessThan) {
    exists(AbstractValue value |
-      compares_lt(this, op, k, isLessThan, value) and this.valueControls(block, value)
+      compares_lt(valueNumber(this), op, k, isLessThan, value) and
+      this.valueControls(block, value)
    )
  }

@@ -562,7 +652,7 @@ class IRGuardCondition extends Instruction {
    Operand left, Operand right, int k, IRBlock pred, IRBlock succ, boolean isLessThan
  ) {
    exists(AbstractValue value |
-      compares_lt(this, left, right, k, isLessThan, value) and
+      compares_lt(valueNumber(this), left, right, k, isLessThan, value) and
      this.valueControlsEdge(pred, succ, value)
    )
  }
@@ -574,7 +664,7 @@ class IRGuardCondition extends Instruction {
  cached
  predicate ensuresLtEdge(Operand left, int k, IRBlock pred, IRBlock succ, boolean isLessThan) {
    exists(AbstractValue value |
-      compares_lt(this, left, k, isLessThan, value) and
+      compares_lt(valueNumber(this), left, k, isLessThan, value) and
      this.valueControlsEdge(pred, succ, value)
    )
  }
@@ -583,7 +673,7 @@ class IRGuardCondition extends Instruction {
  cached
  predicate comparesEq(Operand left, Operand right, int k, boolean areEqual, boolean testIsTrue) {
    exists(BooleanValue value |
-      compares_eq(this, left, right, k, areEqual, value) and
+      compares_eq(valueNumber(this), left, right, k, areEqual, value) and
      value.getValue() = testIsTrue
    )
  }
@@ -591,7 +681,7 @@ class IRGuardCondition extends Instruction {
  /** Holds if (determined by this guard) `op == k` evaluates to `areEqual` if this expression evaluates to `value`. */
  cached
  predicate comparesEq(Operand op, int k, boolean areEqual, AbstractValue value) {
-    unary_compares_eq(this, op, k, areEqual, false, value)
+    unary_compares_eq(valueNumber(this), op, k, areEqual, false, value)
  }

  /**
@@ -601,7 +691,8 @@ class IRGuardCondition extends Instruction {
  cached
  predicate ensuresEq(Operand left, Operand right, int k, IRBlock block, boolean areEqual) {
    exists(AbstractValue value |
-      compares_eq(this, left, right, k, areEqual, value) and this.valueControls(block, value)
+      compares_eq(valueNumber(this), left, right, k, areEqual, value) and
+      this.valueControls(block, value)
    )
  }

@@ -612,7 +703,8 @@ class IRGuardCondition extends Instruction {
  cached
  predicate ensuresEq(Operand op, int k, IRBlock block, boolean areEqual) {
    exists(AbstractValue value |
-      unary_compares_eq(this, op, k, areEqual, false, value) and this.valueControls(block, value)
+      unary_compares_eq(valueNumber(this), op, k, areEqual, false, value) and
+      this.valueControls(block, value)
    )
  }

@@ -625,7 +717,7 @@ class IRGuardCondition extends Instruction {
    Operand left, Operand right, int k, IRBlock pred, IRBlock succ, boolean areEqual
  ) {
    exists(AbstractValue value |
-      compares_eq(this, left, right, k, areEqual, value) and
+      compares_eq(valueNumber(this), left, right, k, areEqual, value) and
      this.valueControlsEdge(pred, succ, value)
    )
  }
@@ -637,7 +729,7 @@ class IRGuardCondition extends Instruction {
  cached
  predicate ensuresEqEdge(Operand op, int k, IRBlock pred, IRBlock succ, boolean areEqual) {
    exists(AbstractValue value |
-      unary_compares_eq(this, op, k, areEqual, false, value) and
+      unary_compares_eq(valueNumber(this), op, k, areEqual, false, value) and
      this.valueControlsEdge(pred, succ, value)
    )
  }
@@ -725,13 +817,20 @@ class IRGuardCondition extends Instruction {
 }

 private Instruction getBranchForCondition(Instruction guard) {
-  result.(ConditionalBranchInstruction).getCondition() = guard
+  // There are a lot of guards inside global or static local initializers,
+  // and on certain databases this can make the `ensures*` predicates
+  // blow up.
+  // These guards are likely not super important anyway.
+  guard.getEnclosingFunction() instanceof Function and
+  (
+    result.(ConditionalBranchInstruction).getCondition() = guard
+    or
+    result.(SwitchInstruction).getExpression() = guard
+  )
  or
  exists(LogicalNotInstruction cond |
    result = getBranchForCondition(cond) and cond.getUnary() = guard
  )
-  or
-  result.(SwitchInstruction).getExpression() = guard
 }

 /**
@@ -740,7 +839,7 @@ private Instruction getBranchForCondition(Instruction guard) {
 * Beware making mistaken logical implications here relating `areEqual` and `testIsTrue`.
 */
 private predicate compares_eq(
-  Instruction test, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
+  ValueNumber test, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
 ) {
  /* The simple case where the test *is* the comparison so areEqual = testIsTrue xor eq. */
  exists(AbstractValue v | simple_comparison_eq(test, left, right, k, v) |
@@ -759,10 +858,10 @@ private predicate compares_eq(
  or
  /* (x is true => (left == right + k)) => (!x is false => (left == right + k)) */
  exists(AbstractValue dual | value = dual.getDualValue() |
-    compares_eq(test.(LogicalNotInstruction).getUnary(), left, right, k, areEqual, dual)
+    compares_eq(test.(LogicalNotValueNumber).getUnary(), left, right, k, areEqual, dual)
  )
  or
-  compares_eq(test.(BuiltinExpectCallInstruction).getCondition(), left, right, k, areEqual, value)
+  compares_eq(test.(BuiltinExpectCallValueNumber).getCondition(), left, right, k, areEqual, value)
 }

 /**
@@ -801,12 +900,10 @@ private predicate compares_eq(
 * latter.
 */
 private predicate unary_compares_eq(
-  Instruction test, Operand op, int k, boolean areEqual, boolean inNonZeroCase, AbstractValue value
+  ValueNumber test, Operand op, int k, boolean areEqual, boolean inNonZeroCase, AbstractValue value
 ) {
  /* The simple case where the test *is* the comparison so areEqual = testIsTrue xor eq. */
-  exists(AbstractValue v |
-    unary_simple_comparison_eq(test, k, inNonZeroCase, v) and op.getDef() = test
-  |
+  exists(AbstractValue v | unary_simple_comparison_eq(test, op, k, inNonZeroCase, v) |
    areEqual = true and value = v
    or
    areEqual = false and value = v.getDualValue()
@@ -817,7 +914,7 @@ private predicate unary_compares_eq(
  /* (x is true => (op == k)) => (!x is false => (op == k)) */
  exists(AbstractValue dual, boolean inNonZeroCase0 |
    value = dual.getDualValue() and
-    unary_compares_eq(test.(LogicalNotInstruction).getUnary(), op, k, inNonZeroCase0, areEqual, dual)
+    unary_compares_eq(test.(LogicalNotValueNumber).getUnary(), op, k, inNonZeroCase0, areEqual, dual)
  |
    k = 0 and inNonZeroCase = inNonZeroCase0
    or
@@ -827,82 +924,95 @@ private predicate unary_compares_eq(
  // ((test is `areEqual` => op == const + k2) and const == `k1`) =>
  // test is `areEqual` => op == k1 + k2
  inNonZeroCase = false and
-  exists(int k1, int k2, ConstantInstruction const |
+  exists(int k1, int k2, Instruction const |
    compares_eq(test, op, const.getAUse(), k2, areEqual, value) and
    int_value(const) = k1 and
    k = k1 + k2
  )
  or
-  unary_compares_eq(test.(BuiltinExpectCallInstruction).getCondition(), op, k, areEqual,
+  unary_compares_eq(test.(BuiltinExpectCallValueNumber).getCondition(), op, k, areEqual,
    inNonZeroCase, value)
 }

 /** Rearrange various simple comparisons into `left == right + k` form. */
 private predicate simple_comparison_eq(
-  CompareInstruction cmp, Operand left, Operand right, int k, AbstractValue value
+  CompareValueNumber cmp, Operand left, Operand right, int k, AbstractValue value
 ) {
-  left = cmp.getLeftOperand() and
-  cmp instanceof CompareEQInstruction and
-  right = cmp.getRightOperand() and
+  cmp instanceof CompareEQValueNumber and
+  cmp.hasOperands(left, right) and
  k = 0 and
  value.(BooleanValue).getValue() = true
  or
-  left = cmp.getLeftOperand() and
-  cmp instanceof CompareNEInstruction and
-  right = cmp.getRightOperand() and
+  cmp instanceof CompareNEValueNumber and
+  cmp.hasOperands(left, right) and
  k = 0 and
  value.(BooleanValue).getValue() = false
 }

 /**
- * Rearrange various simple comparisons into `op == k` form.
+ * Holds if `op` is an operand that is eventually used in a unary comparison
+ * with a constant.
 */
+private predicate isRelevantUnaryComparisonOperand(Operand op) {
+  // Base case: `op` is an operand of a `CompareEQInstruction` or `CompareNEInstruction`,
+  // and the other operand is a constant.
+  exists(CompareInstruction eq, Instruction instr |
+    eq.hasOperands(op, instr.getAUse()) and
+    exists(int_value(instr))
+  |
+    eq instanceof CompareEQInstruction
+    or
+    eq instanceof CompareNEInstruction
+  )
+  or
+  // C doesn't have int-to-bool conversions, so `if(x)` will just generate:
+  // r2_1(glval<int>) = VariableAddress[x]
+  // r2_2(int)        = Load[x]                : &:r2_1, m1_6
+  // v2_3(void)       = ConditionalBranch      : r2_2
+  exists(ConditionalBranchInstruction branch | branch.getConditionOperand() = op)
+  or
+  // If `!x` is a relevant unary comparison then so is `x`.
+  exists(LogicalNotInstruction logicalNot |
+    isRelevantUnaryComparisonOperand(unique( | | logicalNot.getAUse())) and
+    logicalNot.getUnaryOperand() = op
+  )
+  or
+  // If `y` is a relevant unary comparison and `y = x` then so is `x`.
+  not op.isDefinitionInexact() and
+  exists(CopyInstruction copy |
+    isRelevantUnaryComparisonOperand(unique( | | copy.getAUse())) and
+    op = copy.getSourceValueOperand()
+  )
+  or
+  // If phi(x1, x2) is a relevant unary comparison then so are `x1` and `x2`.
+  not op.isDefinitionInexact() and
+  exists(PhiInstruction phi |
+    isRelevantUnaryComparisonOperand(unique( | | phi.getAUse())) and
+    op = phi.getAnInputOperand()
+  )
+  or
+  // If `__builtin_expect(x)` is a relevant unary comparison then so is `x`.
+  exists(BuiltinExpectCallInstruction call |
+    isRelevantUnaryComparisonOperand(unique( | | call.getAUse())) and
+    op = call.getConditionOperand()
+  )
+}
+
+/** Rearrange various simple comparisons into `op == k` form. */
 private predicate unary_simple_comparison_eq(
-  Instruction test, int k, boolean inNonZeroCase, AbstractValue value
+  ValueNumber test, Operand op, int k, boolean inNonZeroCase, AbstractValue value
 ) {
-  exists(SwitchInstruction switch, CaseEdge case |
-    test = switch.getExpression() and
+  exists(CaseEdge case, SwitchConditionValueNumber condition |
+    condition = test and
+    op = condition.getExpressionOperand() and
    case = value.(MatchValue).getCase() and
-    exists(switch.getSuccessor(case)) and
+    exists(condition.getSuccessor(case)) and
    case.getValue().toInt() = k and
    inNonZeroCase = false
  )
  or
-  // Any instruction with an integral type could potentially be part of a
-  // check for nullness when used in a guard. So we include all integral
-  // typed instructions here. However, since some of these instructions are
-  // already included as guards in other cases, we exclude those here.
-  // These are instructions that compute a binary equality or inequality
-  // relation. For example, the following:
-  // ```cpp
-  // if(a == b + 42) { ... }
-  // ```
-  // generates the following IR:
-  // ```
-  // r1(glval<int>) = VariableAddress[a]     :
-  // r2(int)        = Load[a]                : &:r1, m1
-  // r3(glval<int>) = VariableAddress[b]     :
-  // r4(int)        = Load[b]                : &:r3, m2
-  // r5(int)        = Constant[42]           :
-  // r6(int)        = Add                    : r4, r5
-  // r7(bool)       = CompareEQ              : r2, r6
-  // v1(void)       = ConditionalBranch      : r7
-  // ```
-  // and since `r7` is an integral typed instruction this predicate could
-  // include a case for when `r7` evaluates to true (in which case we would
-  // infer that `r6` was non-zero, and a case for when `r7` evaluates to false
-  // (in which case we would infer that `r6` was zero).
-  // However, since `a == b + 42` is already supported when reasoning about
-  // binary equalities we exclude those cases here.
-  not test.isGLValue() and
-  not simple_comparison_eq(test, _, _, _, _) and
-  not simple_comparison_lt(test, _, _, _) and
-  not test = any(SwitchInstruction switch).getExpression() and
-  (
-    test.getResultIRType() instanceof IRAddressType or
-    test.getResultIRType() instanceof IRIntegerType or
-    test.getResultIRType() instanceof IRBooleanType
-  ) and
+  isRelevantUnaryComparisonOperand(op) and
+  op.getDef() = test.getAnInstruction() and
  (
    k = 1 and
    value.(BooleanValue).getValue() = true and
@@ -919,10 +1029,12 @@ private class BuiltinExpectCallInstruction extends CallInstruction {
  BuiltinExpectCallInstruction() { this.getStaticCallTarget().hasName("__builtin_expect") }

  /** Gets the condition of this call. */
-  Instruction getCondition() {
+  Instruction getCondition() { result = this.getConditionOperand().getDef() }
+
+  Operand getConditionOperand() {
    // The first parameter of `__builtin_expect` has type `long`. So we skip
    // the conversion when inferring guards.
-    result = this.getArgument(0).(ConvertInstruction).getUnary()
+    result = this.getArgument(0).(ConvertInstruction).getUnaryOperand()
  }
 }

@@ -932,23 +1044,23 @@ private class BuiltinExpectCallInstruction extends CallInstruction {
 * `__builtin_expect(left == right + k, _)` to `0`.
 */
 private predicate builtin_expect_eq(
-  CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
+  CompareValueNumber cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
 ) {
-  exists(BuiltinExpectCallInstruction call, Instruction const, AbstractValue innerValue |
+  exists(BuiltinExpectCallValueNumber call, Instruction const, AbstractValue innerValue |
    int_value(const) = 0 and
    cmp.hasOperands(call.getAUse(), const.getAUse()) and
    compares_eq(call.getCondition(), left, right, k, areEqual, innerValue)
  |
-    cmp instanceof CompareNEInstruction and
+    cmp instanceof CompareNEValueNumber and
    value = innerValue
    or
-    cmp instanceof CompareEQInstruction and
+    cmp instanceof CompareEQValueNumber and
    value.getDualValue() = innerValue
  )
 }

 private predicate complex_eq(
-  CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
+  ValueNumber cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
 ) {
  sub_eq(cmp, left, right, k, areEqual, value)
  or
@@ -962,24 +1074,24 @@ private predicate complex_eq(
 * an instruction that compares the value of `__builtin_expect(op == k, _)` to `0`.
 */
 private predicate unary_builtin_expect_eq(
-  CompareInstruction cmp, Operand op, int k, boolean areEqual, boolean inNonZeroCase,
+  CompareValueNumber cmp, Operand op, int k, boolean areEqual, boolean inNonZeroCase,
  AbstractValue value
 ) {
-  exists(BuiltinExpectCallInstruction call, Instruction const, AbstractValue innerValue |
+  exists(BuiltinExpectCallValueNumber call, Instruction const, AbstractValue innerValue |
    int_value(const) = 0 and
    cmp.hasOperands(call.getAUse(), const.getAUse()) and
    unary_compares_eq(call.getCondition(), op, k, areEqual, inNonZeroCase, innerValue)
  |
-    cmp instanceof CompareNEInstruction and
+    cmp instanceof CompareNEValueNumber and
    value = innerValue
    or
-    cmp instanceof CompareEQInstruction and
+    cmp instanceof CompareEQValueNumber and
    value.getDualValue() = innerValue
  )
 }

 private predicate unary_complex_eq(
-  Instruction test, Operand op, int k, boolean areEqual, boolean inNonZeroCase, AbstractValue value
+  ValueNumber test, Operand op, int k, boolean areEqual, boolean inNonZeroCase, AbstractValue value
 ) {
  unary_sub_eq(test, op, k, areEqual, inNonZeroCase, value)
  or
@@ -995,7 +1107,7 @@ private predicate unary_complex_eq(

 /** Holds if `left < right + k` evaluates to `isLt` given that test is `testIsTrue`. */
 private predicate compares_lt(
-  Instruction test, Operand left, Operand right, int k, boolean isLt, AbstractValue value
+  ValueNumber test, Operand left, Operand right, int k, boolean isLt, AbstractValue value
 ) {
  /* In the simple case, the test is the comparison, so isLt = testIsTrue */
  simple_comparison_lt(test, left, right, k) and
@@ -1008,23 +1120,22 @@ private predicate compares_lt(
  or
  /* (x is true => (left < right + k)) => (!x is false => (left < right + k)) */
  exists(AbstractValue dual | value = dual.getDualValue() |
-    compares_lt(test.(LogicalNotInstruction).getUnary(), left, right, k, isLt, dual)
+    compares_lt(test.(LogicalNotValueNumber).getUnary(), left, right, k, isLt, dual)
  )
 }

 /** Holds if `op < k` evaluates to `isLt` given that `test` evaluates to `value`. */
-private predicate compares_lt(Instruction test, Operand op, int k, boolean isLt, AbstractValue value) {
-  unary_simple_comparison_lt(test, k, isLt, value) and
-  op.getDef() = test
+private predicate compares_lt(ValueNumber test, Operand op, int k, boolean isLt, AbstractValue value) {
+  unary_simple_comparison_lt(test, op, k, isLt, value)
  or
  complex_lt(test, op, k, isLt, value)
  or
  /* (x is true => (op < k)) => (!x is false => (op < k)) */
  exists(AbstractValue dual | value = dual.getDualValue() |
-    compares_lt(test.(LogicalNotInstruction).getUnary(), op, k, isLt, dual)
+    compares_lt(test.(LogicalNotValueNumber).getUnary(), op, k, isLt, dual)
  )
  or
-  exists(int k1, int k2, ConstantInstruction const |
+  exists(int k1, int k2, Instruction const |
    compares_lt(test, op, const.getAUse(), k2, isLt, value) and
    int_value(const) = k1 and
    k = k1 + k2
@@ -1033,42 +1144,38 @@ private predicate compares_lt(Instruction test, Operand op, int k, boolean isLt,

 /** `(a < b + k) => (b > a - k) => (b >= a + (1-k))` */
 private predicate compares_ge(
-  Instruction test, Operand left, Operand right, int k, boolean isGe, AbstractValue value
+  ValueNumber test, Operand left, Operand right, int k, boolean isGe, AbstractValue value
 ) {
  exists(int onemk | k = 1 - onemk | compares_lt(test, right, left, onemk, isGe, value))
 }

 /** Rearrange various simple comparisons into `left < right + k` form. */
-private predicate simple_comparison_lt(CompareInstruction cmp, Operand left, Operand right, int k) {
-  left = cmp.getLeftOperand() and
-  cmp instanceof CompareLTInstruction and
-  right = cmp.getRightOperand() and
+private predicate simple_comparison_lt(CompareValueNumber cmp, Operand left, Operand right, int k) {
+  cmp.hasOperands(left, right) and
+  cmp instanceof CompareLTValueNumber and
  k = 0
  or
-  left = cmp.getLeftOperand() and
-  cmp instanceof CompareLEInstruction and
-  right = cmp.getRightOperand() and
+  cmp.hasOperands(left, right) and
+  cmp instanceof CompareLEValueNumber and
  k = 1
  or
-  right = cmp.getLeftOperand() and
-  cmp instanceof CompareGTInstruction and
-  left = cmp.getRightOperand() and
+  cmp.hasOperands(right, left) and
+  cmp instanceof CompareGTValueNumber and
  k = 0
  or
-  right = cmp.getLeftOperand() and
-  cmp instanceof CompareGEInstruction and
-  left = cmp.getRightOperand() and
+  cmp.hasOperands(right, left) and
+  cmp instanceof CompareGEValueNumber and
  k = 1
 }

 /** Rearrange various simple comparisons into `op < k` form. */
 private predicate unary_simple_comparison_lt(
-  Instruction test, int k, boolean isLt, AbstractValue value
+  SwitchConditionValueNumber test, Operand op, int k, boolean isLt, AbstractValue value
 ) {
-  exists(SwitchInstruction switch, CaseEdge case |
-    test = switch.getExpression() and
+  exists(CaseEdge case |
+    test.getExpressionOperand() = op and
    case = value.(MatchValue).getCase() and
-    exists(switch.getSuccessor(case)) and
+    exists(test.getSuccessor(case)) and
    case.getMaxValue() > case.getMinValue()
  |
    // op <= k => op < k - 1
@@ -1081,7 +1188,7 @@ private predicate unary_simple_comparison_lt(
 }

 private predicate complex_lt(
-  CompareInstruction cmp, Operand left, Operand right, int k, boolean isLt, AbstractValue value
+  ValueNumber cmp, Operand left, Operand right, int k, boolean isLt, AbstractValue value
 ) {
  sub_lt(cmp, left, right, k, isLt, value)
  or
@@ -1089,7 +1196,7 @@ private predicate complex_lt(
 }

 private predicate complex_lt(
-  Instruction test, Operand left, int k, boolean isLt, AbstractValue value
+  ValueNumber test, Operand left, int k, boolean isLt, AbstractValue value
 ) {
  sub_lt(test, left, k, isLt, value)
  or
@@ -1099,7 +1206,7 @@ private predicate complex_lt(
 // left - x < right + c => left < right + (c+x)
 // left < (right - x) + c => left < right + (c-x)
 private predicate sub_lt(
-  CompareInstruction cmp, Operand left, Operand right, int k, boolean isLt, AbstractValue value
+  ValueNumber cmp, Operand left, Operand right, int k, boolean isLt, AbstractValue value
 ) {
  exists(SubInstruction lhs, int c, int x |
    compares_lt(cmp, lhs.getAUse(), right, c, isLt, value) and
@@ -1130,7 +1237,7 @@ private predicate sub_lt(
  )
 }

-private predicate sub_lt(Instruction test, Operand left, int k, boolean isLt, AbstractValue value) {
+private predicate sub_lt(ValueNumber test, Operand left, int k, boolean isLt, AbstractValue value) {
  exists(SubInstruction lhs, int c, int x |
    compares_lt(test, lhs.getAUse(), c, isLt, value) and
    left = lhs.getLeftOperand() and
@@ -1149,7 +1256,7 @@ private predicate sub_lt(Instruction test, Operand left, int k, boolean isLt, Ab
 // left + x < right + c => left < right + (c-x)
 // left < (right + x) + c => left < right + (c+x)
 private predicate add_lt(
-  CompareInstruction cmp, Operand left, Operand right, int k, boolean isLt, AbstractValue value
+  ValueNumber cmp, Operand left, Operand right, int k, boolean isLt, AbstractValue value
 ) {
  exists(AddInstruction lhs, int c, int x |
    compares_lt(cmp, lhs.getAUse(), right, c, isLt, value) and
@@ -1192,7 +1299,7 @@ private predicate add_lt(
  )
 }

-private predicate add_lt(Instruction test, Operand left, int k, boolean isLt, AbstractValue value) {
+private predicate add_lt(ValueNumber test, Operand left, int k, boolean isLt, AbstractValue value) {
  exists(AddInstruction lhs, int c, int x |
    compares_lt(test, lhs.getAUse(), c, isLt, value) and
    (
@@ -1217,7 +1324,7 @@ private predicate add_lt(Instruction test, Operand left, int k, boolean isLt, Ab
 // left - x == right + c => left == right + (c+x)
 // left == (right - x) + c => left == right + (c-x)
 private predicate sub_eq(
-  CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
+  ValueNumber cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
 ) {
  exists(SubInstruction lhs, int c, int x |
    compares_eq(cmp, lhs.getAUse(), right, c, areEqual, value) and
@@ -1250,7 +1357,7 @@ private predicate sub_eq(

 // op - x == c => op == (c+x)
 private predicate unary_sub_eq(
-  Instruction test, Operand op, int k, boolean areEqual, boolean inNonZeroCase, AbstractValue value
+  ValueNumber test, Operand op, int k, boolean areEqual, boolean inNonZeroCase, AbstractValue value
 ) {
  inNonZeroCase = false and
  exists(SubInstruction sub, int c, int x |
@@ -1272,7 +1379,7 @@ private predicate unary_sub_eq(
 // left + x == right + c => left == right + (c-x)
 // left == (right + x) + c => left == right + (c+x)
 private predicate add_eq(
-  CompareInstruction cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
+  ValueNumber cmp, Operand left, Operand right, int k, boolean areEqual, AbstractValue value
 ) {
  exists(AddInstruction lhs, int c, int x |
    compares_eq(cmp, lhs.getAUse(), right, c, areEqual, value) and
@@ -1317,7 +1424,7 @@ private predicate add_eq(

 // left + x == right + c => left == right + (c-x)
 private predicate unary_add_eq(
-  Instruction test, Operand left, int k, boolean areEqual, boolean inNonZeroCase,
+  ValueNumber test, Operand left, int k, boolean areEqual, boolean inNonZeroCase,
  AbstractValue value
 ) {
  inNonZeroCase = false and
@@ -1351,6 +1458,4 @@ private class IntegerOrPointerConstantInstruction extends ConstantInstruction {
 }

 /** The int value of integer constant expression. */
-private int int_value(Instruction i) {
-  result = i.(IntegerOrPointerConstantInstruction).getValue().toInt()
-}
+private int int_value(IntegerOrPointerConstantInstruction i) { result = i.getValue().toInt() }