Merge pull request #13760 from MathiasVP/split-invalid-ptr-deref-into-more-files

C++: Split `cpp/invalid-pointer-deref` into more files

cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/ProductFlow.qll

@@ -297,6 +297,22 @@ module ProductFlow {
       reachable(source1, source2, sink1, sink2)
     }
 
+    /** Holds if data can flow from `(source1, source2)` to `(sink1, sink2)`. */
+    predicate flow(
+      DataFlow::Node source1, DataFlow::Node source2, DataFlow::Node sink1, DataFlow::Node sink2
+    ) {
+      exists(
+        Flow1::PathNode pSource1, Flow2::PathNode pSource2, Flow1::PathNode pSink1,
+        Flow2::PathNode pSink2
+      |
+        pSource1.getNode() = source1 and
+        pSource2.getNode() = source2 and
+        pSink1.getNode() = sink1 and
+        pSink2.getNode() = sink2 and
+        flowPath(pSource1, pSource2, pSink1, pSink2)
+      )
+    }
+
     private module Config1 implements DataFlow::StateConfigSig {
       class FlowState = FlowState1;
 

cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/AllocationToInvalidPointer.qll

@@ -0,0 +1,256 @@
+/**
+ * This file provides the first phase of the `cpp/invalid-pointer-deref` query that identifies flow
+ * from an allocation to a pointer-arithmetic instruction that constructs a pointer that is out of bounds.
+ */
+
+private import cpp
+private import semmle.code.cpp.ir.dataflow.internal.ProductFlow
+private import semmle.code.cpp.ir.ValueNumbering
+private import semmle.code.cpp.controlflow.IRGuards
+private import codeql.util.Unit
+private import RangeAnalysisUtil
+
+private VariableAccess getAVariableAccess(Expr e) { e.getAChild*() = result }
+
+/**
+ * Holds if the `(n, state)` pair represents the source of flow for the size
+ * expression associated with `alloc`.
+ */
+predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
+  exists(VariableAccess va, Expr size, int delta |
+    size = alloc.getSizeExpr() and
+    // Get the unique variable in a size expression like `x` in `malloc(x + 1)`.
+    va = unique( | | getAVariableAccess(size)) and
+    // Compute `delta` as the constant difference between `x` and `x + 1`.
+    bounded1(any(Instruction instr | instr.getUnconvertedResultExpression() = size),
+      any(LoadInstruction load | load.getUnconvertedResultExpression() = va), delta) and
+    n.asConvertedExpr() = va.getFullyConverted() and
+    state = delta
+  )
+}
+
+/**
+ * A module that encapsulates a barrier guard to remove false positives from flow like:
+ * ```cpp
+ * char *p = new char[size];
+ * // ...
+ * unsigned n = size;
+ * // ...
+ * if(n < size) {
+ *   use(*p[n]);
+ * }
+ * ```
+ * In this case, the sink pair identified by the product flow library (without any additional barriers)
+ * would be `(p, n)` (where `n` is the `n` in `p[n]`), because there exists a pointer-arithmetic
+ * instruction `pai` such that:
+ * 1. The left-hand of `pai` flows from the allocation, and
+ * 2. The right-hand of `pai` is non-strictly upper bounded by `n` (where `n` is the `n` in `p[n]`)
+ * but because there's a strict comparison that compares `n` against the size of the allocation this
+ * snippet is fine.
+ */
+module Barrier2 {
+  private class FlowState2 = int;
+
+  private module BarrierConfig2 implements DataFlow::ConfigSig {
+    predicate isSource(DataFlow::Node source) {
+      // The sources is the same as in the sources for the second
+      // projection in the `AllocToInvalidPointerConfig` module.
+      hasSize(_, source, _)
+    }
+
+    additional predicate isSink(
+      DataFlow::Node left, DataFlow::Node right, IRGuardCondition g, FlowState2 state,
+      boolean testIsTrue
+    ) {
+      // The sink is any "large" side of a relational comparison.
+      g.comparesLt(left.asOperand(), right.asOperand(), state, true, testIsTrue)
+    }
+
+    predicate isSink(DataFlow::Node sink) { isSink(_, sink, _, _, _) }
+  }
+
+  private import DataFlow::Global<BarrierConfig2>
+
+  private FlowState2 getAFlowStateForNode(DataFlow::Node node) {
+    exists(DataFlow::Node source |
+      flow(source, node) and
+      hasSize(_, source, result)
+    )
+  }
+
+  private predicate operandGuardChecks(
+    IRGuardCondition g, Operand left, Operand right, FlowState2 state, boolean edge
+  ) {
+    exists(DataFlow::Node nLeft, DataFlow::Node nRight, FlowState2 state0 |
+      nRight.asOperand() = right and
+      nLeft.asOperand() = left and
+      BarrierConfig2::isSink(nLeft, nRight, g, state0, edge) and
+      state = getAFlowStateForNode(nRight) and
+      state0 <= state
+    )
+  }
+
+  /**
+   * Gets an instruction that is guarded by a guard condition which ensures that
+   * the value of the instruction is upper-bounded by size of some allocation.
+   */
+  Instruction getABarrierInstruction(FlowState2 state) {
+    exists(IRGuardCondition g, ValueNumber value, Operand use, boolean edge |
+      use = value.getAUse() and
+      operandGuardChecks(pragma[only_bind_into](g), pragma[only_bind_into](use), _,
+        pragma[only_bind_into](state), pragma[only_bind_into](edge)) and
+      result = value.getAnInstruction() and
+      g.controls(result.getBlock(), edge)
+    )
+  }
+
+  /**
+   * Gets a `DataFlow::Node` that is guarded by a guard condition which ensures that
+   * the value of the node is upper-bounded by size of some allocation.
+   */
+  DataFlow::Node getABarrierNode(FlowState2 state) {
+    result.asOperand() = getABarrierInstruction(state).getAUse()
+  }
+
+  /**
+   * Gets the block of a node that is guarded (see `getABarrierInstruction` or
+   * `getABarrierNode` for the definition of what it means to be guarded).
+   */
+  IRBlock getABarrierBlock(FlowState2 state) {
+    result.getAnInstruction() = getABarrierInstruction(state)
+  }
+}
+
+private module InterestingPointerAddInstruction {
+  private module PointerAddInstructionConfig implements DataFlow::ConfigSig {
+    predicate isSource(DataFlow::Node source) {
+      // The sources is the same as in the sources for the second
+      // projection in the `AllocToInvalidPointerConfig` module.
+      hasSize(source.asConvertedExpr(), _, _)
+    }
+
+    predicate isSink(DataFlow::Node sink) {
+      sink.asInstruction() = any(PointerAddInstruction pai).getLeft()
+    }
+  }
+
+  private import DataFlow::Global<PointerAddInstructionConfig>
+
+  /**
+   * Holds if `pai` is a pointer-arithmetic instruction such that the
+   * result of an allocation flows to the left-hand side of `pai`.
+   *
+   * This predicate is used to reduce the set of tuples in `isSinkPair`.
+   */
+  predicate isInteresting(PointerAddInstruction pai) {
+    exists(DataFlow::Node n |
+      n.asInstruction() = pai.getLeft() and
+      flowTo(n)
+    )
+  }
+}
+
+/**
+ * A product-flow configuration for flow from an (allocation, size) pair to a
+ * pointer-arithmetic operation that is non-strictly upper-bounded by `allocation + size`.
+ *
+ * The goal of this query is to find patterns such as:
+ * ```cpp
+ * 1. char* begin = (char*)malloc(size);
+ * 2. char* end = begin + size;
+ * 3. for(int *p = begin; p <= end; p++) {
+ * 4.   use(*p);
+ * 5. }
+ * ```
+ *
+ * We do this by splitting the task up into two configurations:
+ * 1. `AllocToInvalidPointerConfig` find flow from `malloc(size)` to `begin + size`, and
+ * 2. `InvalidPointerToDerefConfig` finds flow from `begin + size` to an `end` (on line 3).
+ *
+ * Finally, the range-analysis library will find a load from (or store to) an address that
+ * is non-strictly upper-bounded by `end` (which in this case is `*p`).
+ */
+private module Config implements ProductFlow::StateConfigSig {
+  class FlowState1 = Unit;
+
+  class FlowState2 = int;
+
+  predicate isSourcePair(
+    DataFlow::Node source1, FlowState1 state1, DataFlow::Node source2, FlowState2 state2
+  ) {
+    // In the case of an allocation like
+    // ```cpp
+    // malloc(size + 1);
+    // ```
+    // we use `state2` to remember that there was an offset (in this case an offset of `1`) added
+    // to the size of the allocation. This state is then checked in `isSinkPair`.
+    exists(state1) and
+    hasSize(source1.asConvertedExpr(), source2, state2)
+  }
+
+  predicate isSinkPair(
+    DataFlow::Node sink1, FlowState1 state1, DataFlow::Node sink2, FlowState2 state2
+  ) {
+    exists(state1) and
+    // We check that the delta computed by the range analysis matches the
+    // state value that we set in `isSourcePair`.
+    pointerAddInstructionHasBounds0(_, sink1, sink2, state2)
+  }
+
+  predicate isBarrier2(DataFlow::Node node, FlowState2 state) {
+    node = Barrier2::getABarrierNode(state)
+  }
+
+  predicate isBarrierIn1(DataFlow::Node node) { isSourcePair(node, _, _, _) }
+
+  predicate isBarrierOut2(DataFlow::Node node) {
+    node = any(DataFlow::SsaPhiNode phi).getAnInput(true)
+  }
+}
+
+private module AllocToInvalidPointerFlow = ProductFlow::GlobalWithState<Config>;
+
+/**
+ * Holds if `pai` is non-strictly upper bounded by `sink2 + delta` and `sink1` is the
+ * left operand of the pointer-arithmetic operation.
+ *
+ * For example in,
+ * ```cpp
+ * char* end = p + (size + 1);
+ * ```
+ * We will have:
+ * - `pai` is `p + (size + 1)`,
+ * - `sink1` is `p`
+ * - `sink2` is `size`
+ * - `delta` is `1`.
+ */
+pragma[nomagic]
+private predicate pointerAddInstructionHasBounds0(
+  PointerAddInstruction pai, DataFlow::Node sink1, DataFlow::Node sink2, int delta
+) {
+  InterestingPointerAddInstruction::isInteresting(pragma[only_bind_into](pai)) and
+  exists(Instruction right, Instruction instr2 |
+    pai.getRight() = right and
+    pai.getLeft() = sink1.asInstruction() and
+    instr2 = sink2.asInstruction() and
+    // pai.getRight() <= sink2 + delta
+    bounded1(right, instr2, delta) and
+    not right = Barrier2::getABarrierInstruction(delta) and
+    not instr2 = Barrier2::getABarrierInstruction(delta)
+  )
+}
+
+/**
+ * Holds if `allocation` flows to `sink1` and `sink1` represents the left-hand
+ * side of the pointer-arithmetic instruction `pai`, and the right-hand side of `pai`
+ * is non-strictly upper bounded by the size of `alllocation` + `delta`.
+ */
+pragma[nomagic]
+predicate pointerAddInstructionHasBounds(
+  DataFlow::Node allocation, PointerAddInstruction pai, DataFlow::Node sink1, int delta
+) {
+  exists(DataFlow::Node sink2 |
+    AllocToInvalidPointerFlow::flow(allocation, _, sink1, sink2) and
+    pointerAddInstructionHasBounds0(pai, sink1, sink2, delta)
+  )
+}

cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/InvalidPointerToDereference.qll

@@ -0,0 +1,196 @@
+/**
+ * This file provides the second phase of the `cpp/invalid-pointer-deref` query that identifies flow
+ * from the out-of-bounds pointer identified by the `AllocationToInvalidPointer.qll` library to
+ * a dereference of the out-of-bounds pointer.
+ */
+
+private import cpp
+private import semmle.code.cpp.dataflow.new.DataFlow
+private import semmle.code.cpp.ir.ValueNumbering
+private import semmle.code.cpp.controlflow.IRGuards
+private import AllocationToInvalidPointer as AllocToInvalidPointer
+private import RangeAnalysisUtil
+
+private module InvalidPointerToDerefBarrier {
+  private module BarrierConfig implements DataFlow::ConfigSig {
+    predicate isSource(DataFlow::Node source) {
+      // The sources is the same as in the sources for `InvalidPointerToDerefConfig`.
+      invalidPointerToDerefSource(_, _, source, _)
+    }
+
+    additional predicate isSink(
+      DataFlow::Node left, DataFlow::Node right, IRGuardCondition g, int state, boolean testIsTrue
+    ) {
+      // The sink is any "large" side of a relational comparison.
+      g.comparesLt(left.asOperand(), right.asOperand(), state, true, testIsTrue)
+    }
+
+    predicate isSink(DataFlow::Node sink) { isSink(_, sink, _, _, _) }
+  }
+
+  private module BarrierFlow = DataFlow::Global<BarrierConfig>;
+
+  private int getInvalidPointerToDerefSourceDelta(DataFlow::Node node) {
+    exists(DataFlow::Node source |
+      BarrierFlow::flow(source, node) and
+      invalidPointerToDerefSource(_, _, source, result)
+    )
+  }
+
+  private predicate operandGuardChecks(
+    IRGuardCondition g, Operand left, Operand right, int state, boolean edge
+  ) {
+    exists(DataFlow::Node nLeft, DataFlow::Node nRight, int state0 |
+      nRight.asOperand() = right and
+      nLeft.asOperand() = left and
+      BarrierConfig::isSink(nLeft, nRight, g, state0, edge) and
+      state = getInvalidPointerToDerefSourceDelta(nRight) and
+      state0 <= state
+    )
+  }
+
+  Instruction getABarrierInstruction(int state) {
+    exists(IRGuardCondition g, ValueNumber value, Operand use, boolean edge |
+      use = value.getAUse() and
+      operandGuardChecks(pragma[only_bind_into](g), pragma[only_bind_into](use), _, state,
+        pragma[only_bind_into](edge)) and
+      result = value.getAnInstruction() and
+      g.controls(result.getBlock(), edge)
+    )
+  }
+
+  DataFlow::Node getABarrierNode() { result.asOperand() = getABarrierInstruction(_).getAUse() }
+
+  pragma[nomagic]
+  IRBlock getABarrierBlock(int state) { result.getAnInstruction() = getABarrierInstruction(state) }
+}
+
+/**
+ * A configuration to track flow from a pointer-arithmetic operation found
+ * by `AllocToInvalidPointerConfig` to a dereference of the pointer.
+ */
+private module InvalidPointerToDerefConfig implements DataFlow::ConfigSig {
+  predicate isSource(DataFlow::Node source) { invalidPointerToDerefSource(_, _, source, _) }
+
+  pragma[inline]
+  predicate isSink(DataFlow::Node sink) { isInvalidPointerDerefSink(sink, _, _, _) }
+
+  predicate isBarrier(DataFlow::Node node) {
+    node = any(DataFlow::SsaPhiNode phi | not phi.isPhiRead()).getAnInput(true)
+    or
+    node = InvalidPointerToDerefBarrier::getABarrierNode()
+  }
+}
+
+private import DataFlow::Global<InvalidPointerToDerefConfig>
+
+/**
+ * Holds if `source1` is dataflow node that represents an allocation that flows to the
+ * left-hand side of the pointer-arithmetic `pai`, and `derefSource` is a dataflow node with
+ * a pointer-value that is non-strictly upper bounded by `pai + delta`.
+ *
+ * For example, if `pai` is a pointer-arithmetic operation `p + size` in an expression such
+ * as `(p + size) + 1` and `derefSource` is the node representing `(p + size) + 1`. In this
+ * case `delta` is 1.
+ */
+private predicate invalidPointerToDerefSource(
+  DataFlow::Node source1, PointerArithmeticInstruction pai, DataFlow::Node derefSource, int delta
+) {
+  exists(int delta0 |
+    // Note that `delta` is not necessarily equal to `delta0`:
+    // `delta0` is the constant offset added to the size of the allocation, and
+    // delta is the constant difference between the pointer-arithmetic instruction
+    // and the instruction computing the address for which we will search for a dereference.
+    AllocToInvalidPointer::pointerAddInstructionHasBounds(source1, pai, _, delta0) and
+    bounded2(derefSource.asInstruction(), pai, delta) and
+    delta >= 0 and
+    // TODO: This condition will go away once #13725 is merged, and then we can make `Barrier2`
+    // private to `AllocationToInvalidPointer.qll`.
+    not derefSource.getBasicBlock() = AllocToInvalidPointer::Barrier2::getABarrierBlock(delta0)
+  )
+}
+
+/**
+ * Holds if `sink` is a sink for `InvalidPointerToDerefConfig` and `i` is a `StoreInstruction` that
+ * writes to an address that non-strictly upper-bounds `sink`, or `i` is a `LoadInstruction` that
+ * reads from an address that non-strictly upper-bounds `sink`.
+ */
+pragma[inline]
+private predicate isInvalidPointerDerefSink(
+  DataFlow::Node sink, Instruction i, string operation, int delta
+) {
+  exists(AddressOperand addr, Instruction s, IRBlock b |
+    s = sink.asInstruction() and
+    bounded(addr.getDef(), s, delta) and
+    delta >= 0 and
+    i.getAnOperand() = addr and
+    b = i.getBlock() and
+    not b = InvalidPointerToDerefBarrier::getABarrierBlock(delta)
+  |
+    i instanceof StoreInstruction and
+    operation = "write"
+    or
+    i instanceof LoadInstruction and
+    operation = "read"
+  )
+}
+
+/**
+ * Yields any instruction that is control-flow reachable from `instr`.
+ */
+bindingset[instr, result]
+pragma[inline_late]
+private Instruction getASuccessor(Instruction instr) {
+  exists(IRBlock b, int instrIndex, int resultIndex |
+    b.getInstruction(instrIndex) = instr and
+    b.getInstruction(resultIndex) = result
+  |
+    resultIndex >= instrIndex
+  )
+  or
+  instr.getBlock().getASuccessor+() = result.getBlock()
+}
+
+private predicate paiForDereferenceSink(PointerArithmeticInstruction pai, DataFlow::Node derefSink) {
+  exists(DataFlow::Node derefSource |
+    invalidPointerToDerefSource(_, pai, derefSource, _) and
+    flow(derefSource, derefSink)
+  )
+}
+
+/**
+ * Holds if `derefSink` is a dataflow node that represents an out-of-bounds address that is about to
+ * be dereferenced by `operation` (which is either a `StoreInstruction` or `LoadInstruction`), and
+ * `pai` is the pointer-arithmetic operation that caused the `derefSink` to be out-of-bounds.
+ */
+private predicate derefSinkToOperation(
+  DataFlow::Node derefSink, PointerArithmeticInstruction pai, DataFlow::Node operation,
+  string description, int delta
+) {
+  exists(Instruction i |
+    paiForDereferenceSink(pai, pragma[only_bind_into](derefSink)) and
+    isInvalidPointerDerefSink(derefSink, i, description, delta) and
+    i = getASuccessor(derefSink.asInstruction()) and
+    operation.asInstruction() = i
+  )
+}
+
+/**
+ * Holds if `allocation` is the result of an allocation that flows to the left-hand side of `pai`, and where
+ * the right-hand side of `pai` is an offset such that the result of `pai` points to an out-of-bounds pointer.
+ *
+ * Furthermore, `derefSource` is at least as large as `pai` and flows to `derefSink` before being dereferenced
+ * by `operation` (which is either a `StoreInstruction` or `LoadInstruction`). The result is that `operation`
+ * dereferences a pointer that's "off by `delta`" number of elements.
+ */
+predicate operationIsOffBy(
+  DataFlow::Node allocation, PointerArithmeticInstruction pai, DataFlow::Node derefSource,
+  DataFlow::Node derefSink, string description, DataFlow::Node operation, int delta
+) {
+  exists(int deltaDerefSourceAndPai, int deltaDerefSinkAndDerefAddress |
+    invalidPointerToDerefSource(allocation, pai, derefSource, deltaDerefSourceAndPai) and
+    flow(derefSource, derefSink) and
+    derefSinkToOperation(derefSink, pai, operation, description, deltaDerefSinkAndDerefAddress) and
+    delta = deltaDerefSourceAndPai + deltaDerefSinkAndDerefAddress
+  )
+}

cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/RangeAnalysisUtil.qll

@@ -0,0 +1,48 @@
+/**
+ * This file contains the range-analysis specific parts of the `cpp/invalid-pointer-deref` query
+ * that is used by both `AllocationToInvalidPointer.qll` and `InvalidPointerToDereference.qll`.
+ */
+
+private import cpp
+private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysis
+private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
+private import semmle.code.cpp.ir.IR
+
+pragma[nomagic]
+private Instruction getABoundIn(SemBound b, IRFunction func) {
+  getSemanticExpr(result) = b.getExpr(0) and
+  result.getEnclosingIRFunction() = func
+}
+
+/**
+ * Holds if `i <= b + delta`.
+ */
+pragma[inline]
+private predicate boundedImpl(Instruction i, Instruction b, int delta) {
+  exists(SemBound bound, IRFunction func |
+    semBounded(getSemanticExpr(i), bound, delta, true, _) and
+    b = getABoundIn(bound, func) and
+    i.getEnclosingIRFunction() = func
+  )
+}
+
+/**
+ * Holds if `i <= b + delta`.
+ *
+ * This predicate enforces a join-order that ensures that `i` has already been bound.
+ */
+bindingset[i]
+pragma[inline_late]
+predicate bounded1(Instruction i, Instruction b, int delta) { boundedImpl(i, b, delta) }
+
+/**
+ * Holds if `i <= b + delta`.
+ *
+ * This predicate enforces a join-order that ensures that `b` has already been bound.
+ */
+bindingset[b]
+pragma[inline_late]
+predicate bounded2(Instruction i, Instruction b, int delta) { boundedImpl(i, b, delta) }
+
+/** Holds if `i <= b + delta`. */
+predicate bounded = boundedImpl/3;

cpp/ql/src/experimental/Security/CWE/CWE-193/InvalidPointerDeref.ql

@@ -16,428 +16,11 @@
  */
 
 import cpp
-import semmle.code.cpp.ir.dataflow.internal.ProductFlow
-import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysis
-import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
-import semmle.code.cpp.ir.ValueNumbering
-import semmle.code.cpp.controlflow.IRGuards
+import semmle.code.cpp.dataflow.new.DataFlow
 import semmle.code.cpp.ir.IR
-import codeql.util.Unit
 import FinalFlow::PathGraph
-
-pragma[nomagic]
-Instruction getABoundIn(SemBound b, IRFunction func) {
-  getSemanticExpr(result) = b.getExpr(0) and
-  result.getEnclosingIRFunction() = func
-}
-
-/**
- * Holds if `i <= b + delta`.
- */
-pragma[inline]
-predicate boundedImpl(Instruction i, Instruction b, int delta) {
-  exists(SemBound bound, IRFunction func |
-    semBounded(getSemanticExpr(i), bound, delta, true, _) and
-    b = getABoundIn(bound, func) and
-    i.getEnclosingIRFunction() = func
-  )
-}
-
-bindingset[i]
-pragma[inline_late]
-predicate bounded1(Instruction i, Instruction b, int delta) { boundedImpl(i, b, delta) }
-
-bindingset[b]
-pragma[inline_late]
-predicate bounded2(Instruction i, Instruction b, int delta) { boundedImpl(i, b, delta) }
-
-VariableAccess getAVariableAccess(Expr e) { e.getAChild*() = result }
-
-/**
- * Holds if `(n, state)` pair represents the source of flow for the size
- * expression associated with `alloc`.
- */
-predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
-  exists(VariableAccess va, Expr size, int delta |
-    size = alloc.getSizeExpr() and
-    // Get the unique variable in a size expression like `x` in `malloc(x + 1)`.
-    va = unique( | | getAVariableAccess(size)) and
-    // Compute `delta` as the constant difference between `x` and `x + 1`.
-    bounded1(any(Instruction instr | instr.getUnconvertedResultExpression() = size),
-      any(LoadInstruction load | load.getUnconvertedResultExpression() = va), delta) and
-    n.asConvertedExpr() = va.getFullyConverted() and
-    state = delta
-  )
-}
-
-/**
- * A module that encapsulates a barrier guard to remove false positives from flow like:
- * ```cpp
- * char *p = new char[size];
- * // ...
- * unsigned n = size;
- * // ...
- * if(n < size) {
- *   use(*p[n]);
- * }
- * ```
- * In this case, the sink pair identified by the product flow library (without any additional barriers)
- * would be `(p, n)` (where `n` is the `n` in `p[n]`), because there exists a pointer-arithmetic
- * instruction `pai` such that:
- * 1. The left-hand of `pai` flows from the allocation, and
- * 2. The right-hand of `pai` is non-strictly upper bounded by `n` (where `n` is the `n` in `p[n]`)
- * but because there's a strict comparison that compares `n` against the size of the allocation this
- * snippet is fine.
- */
-module Barrier2 {
-  private class FlowState2 = AllocToInvalidPointerConfig::FlowState2;
-
-  private module BarrierConfig2 implements DataFlow::ConfigSig {
-    predicate isSource(DataFlow::Node source) {
-      // The sources is the same as in the sources for the second
-      // projection in the `AllocToInvalidPointerConfig` module.
-      hasSize(_, source, _)
-    }
-
-    additional predicate isSink(
-      DataFlow::Node left, DataFlow::Node right, IRGuardCondition g, FlowState2 state,
-      boolean testIsTrue
-    ) {
-      // The sink is any "large" side of a relational comparison.
-      g.comparesLt(left.asOperand(), right.asOperand(), state, true, testIsTrue)
-    }
-
-    predicate isSink(DataFlow::Node sink) { isSink(_, sink, _, _, _) }
-  }
-
-  private import DataFlow::Global<BarrierConfig2>
-
-  private FlowState2 getAFlowStateForNode(DataFlow::Node node) {
-    exists(DataFlow::Node source |
-      flow(source, node) and
-      hasSize(_, source, result)
-    )
-  }
-
-  private predicate operandGuardChecks(
-    IRGuardCondition g, Operand left, Operand right, FlowState2 state, boolean edge
-  ) {
-    exists(DataFlow::Node nLeft, DataFlow::Node nRight, FlowState2 state0 |
-      nRight.asOperand() = right and
-      nLeft.asOperand() = left and
-      BarrierConfig2::isSink(nLeft, nRight, g, state0, edge) and
-      state = getAFlowStateForNode(nRight) and
-      state0 <= state
-    )
-  }
-
-  Instruction getABarrierInstruction(FlowState2 state) {
-    exists(IRGuardCondition g, ValueNumber value, Operand use, boolean edge |
-      use = value.getAUse() and
-      operandGuardChecks(pragma[only_bind_into](g), pragma[only_bind_into](use), _,
-        pragma[only_bind_into](state), pragma[only_bind_into](edge)) and
-      result = value.getAnInstruction() and
-      g.controls(result.getBlock(), edge)
-    )
-  }
-
-  DataFlow::Node getABarrierNode(FlowState2 state) {
-    result.asOperand() = getABarrierInstruction(state).getAUse()
-  }
-
-  IRBlock getABarrierBlock(FlowState2 state) {
-    result.getAnInstruction() = getABarrierInstruction(state)
-  }
-}
-
-/**
- * A product-flow configuration for flow from an (allocation, size) pair to a
- * pointer-arithmetic operation that is non-strictly upper-bounded by `allocation + size`.
- *
- * The goal of this query is to find patterns such as:
- * ```cpp
- * 1. char* begin = (char*)malloc(size);
- * 2. char* end = begin + size;
- * 3. for(int *p = begin; p <= end; p++) {
- * 4.   use(*p);
- * 5. }
- * ```
- *
- * We do this by splitting the task up into two configurations:
- * 1. `AllocToInvalidPointerConfig` find flow from `malloc(size)` to `begin + size`, and
- * 2. `InvalidPointerToDerefConfig` finds flow from `begin + size` to an `end` (on line 3).
- *
- * Finally, the range-analysis library will find a load from (or store to) an address that
- * is non-strictly upper-bounded by `end` (which in this case is `*p`).
- */
-module AllocToInvalidPointerConfig implements ProductFlow::StateConfigSig {
-  class FlowState1 = Unit;
-
-  class FlowState2 = int;
-
-  predicate isSourcePair(
-    DataFlow::Node source1, FlowState1 state1, DataFlow::Node source2, FlowState2 state2
-  ) {
-    // In the case of an allocation like
-    // ```cpp
-    // malloc(size + 1);
-    // ```
-    // we use `state2` to remember that there was an offset (in this case an offset of `1`) added
-    // to the size of the allocation. This state is then checked in `isSinkPair`.
-    exists(state1) and
-    hasSize(source1.asConvertedExpr(), source2, state2)
-  }
-
-  predicate isSinkPair(
-    DataFlow::Node sink1, FlowState1 state1, DataFlow::Node sink2, FlowState2 state2
-  ) {
-    exists(state1) and
-    // We check that the delta computed by the range analysis matches the
-    // state value that we set in `isSourcePair`.
-    isSinkImpl(_, sink1, sink2, state2)
-  }
-
-  predicate isBarrier2(DataFlow::Node node, FlowState2 state) {
-    node = Barrier2::getABarrierNode(state)
-  }
-
-  predicate isBarrierIn1(DataFlow::Node node) { isSourcePair(node, _, _, _) }
-
-  predicate isBarrierOut2(DataFlow::Node node) {
-    node = any(DataFlow::SsaPhiNode phi).getAnInput(true)
-  }
-}
-
-module AllocToInvalidPointerFlow = ProductFlow::GlobalWithState<AllocToInvalidPointerConfig>;
-
-/**
- * Holds if `pai` is non-strictly upper bounded by `sink2 + delta` and `sink1` is the
- * left operand of the pointer-arithmetic operation.
- *
- * For example in,
- * ```cpp
- * char* end = p + (size + 1);
- * ```
- * We will have:
- * - `pai` is `p + (size + 1)`,
- * - `sink1` is `p`
- * - `sink2` is `size`
- * - `delta` is `1`.
- */
-pragma[nomagic]
-predicate pointerAddInstructionHasBounds(
-  PointerAddInstruction pai, DataFlow::Node sink1, DataFlow::Node sink2, int delta
-) {
-  InterestingPointerAddInstruction::isInteresting(pragma[only_bind_into](pai)) and
-  exists(Instruction right, Instruction instr2 |
-    pai.getRight() = right and
-    pai.getLeft() = sink1.asInstruction() and
-    instr2 = sink2.asInstruction() and
-    bounded1(right, instr2, delta) and
-    not right = Barrier2::getABarrierInstruction(delta) and
-    not instr2 = Barrier2::getABarrierInstruction(delta)
-  )
-}
-
-module InterestingPointerAddInstruction {
-  private module PointerAddInstructionConfig implements DataFlow::ConfigSig {
-    predicate isSource(DataFlow::Node source) {
-      // The sources is the same as in the sources for the second
-      // projection in the `AllocToInvalidPointerConfig` module.
-      hasSize(source.asConvertedExpr(), _, _)
-    }
-
-    predicate isSink(DataFlow::Node sink) {
-      sink.asInstruction() = any(PointerAddInstruction pai).getLeft()
-    }
-  }
-
-  private import DataFlow::Global<PointerAddInstructionConfig>
-
-  predicate isInteresting(PointerAddInstruction pai) {
-    exists(DataFlow::Node n |
-      n.asInstruction() = pai.getLeft() and
-      flowTo(n)
-    )
-  }
-}
-
-/**
- * Holds if `pai` is non-strictly upper bounded by `sink2 + delta` and `sink1` is the
- * left operand of the pointer-arithmetic operation.
- *
- * See `pointerAddInstructionHasBounds` for an example.
- */
-predicate isSinkImpl(
-  PointerAddInstruction pai, DataFlow::Node sink1, DataFlow::Node sink2, int delta
-) {
-  pointerAddInstructionHasBounds(pai, sink1, sink2, delta)
-}
-
-/**
- * Yields any instruction that is control-flow reachable from `instr`.
- */
-bindingset[instr, result]
-pragma[inline_late]
-Instruction getASuccessor(Instruction instr) {
-  exists(IRBlock b, int instrIndex, int resultIndex |
-    result.getBlock() = b and
-    instr.getBlock() = b and
-    b.getInstruction(instrIndex) = instr and
-    b.getInstruction(resultIndex) = result
-  |
-    resultIndex >= instrIndex
-  )
-  or
-  instr.getBlock().getASuccessor+() = result.getBlock()
-}
-
-/**
- * Holds if `sink` is a sink for `InvalidPointerToDerefConfig` and `i` is a `StoreInstruction` that
- * writes to an address that non-strictly upper-bounds `sink`, or `i` is a `LoadInstruction` that
- * reads from an address that non-strictly upper-bounds `sink`.
- */
-pragma[inline]
-predicate isInvalidPointerDerefSink(DataFlow::Node sink, Instruction i, string operation, int delta) {
-  exists(AddressOperand addr, Instruction s, IRBlock b |
-    s = sink.asInstruction() and
-    boundedImpl(addr.getDef(), s, delta) and
-    delta >= 0 and
-    i.getAnOperand() = addr and
-    b = i.getBlock() and
-    not b = InvalidPointerToDerefBarrier::getABarrierBlock(delta)
-  |
-    i instanceof StoreInstruction and
-    operation = "write"
-    or
-    i instanceof LoadInstruction and
-    operation = "read"
-  )
-}
-
-module InvalidPointerToDerefBarrier {
-  private module BarrierConfig implements DataFlow::ConfigSig {
-    predicate isSource(DataFlow::Node source) {
-      // The sources is the same as in the sources for `InvalidPointerToDerefConfig`.
-      invalidPointerToDerefSource(_, _, source, _)
-    }
-
-    additional predicate isSink(
-      DataFlow::Node left, DataFlow::Node right, IRGuardCondition g, int state, boolean testIsTrue
-    ) {
-      // The sink is any "large" side of a relational comparison.
-      g.comparesLt(left.asOperand(), right.asOperand(), state, true, testIsTrue)
-    }
-
-    predicate isSink(DataFlow::Node sink) { isSink(_, sink, _, _, _) }
-  }
-
-  private import DataFlow::Global<BarrierConfig>
-
-  private int getInvalidPointerToDerefSourceDelta(DataFlow::Node node) {
-    exists(DataFlow::Node source |
-      flow(source, node) and
-      invalidPointerToDerefSource(_, _, source, result)
-    )
-  }
-
-  private predicate operandGuardChecks(
-    IRGuardCondition g, Operand left, Operand right, int state, boolean edge
-  ) {
-    exists(DataFlow::Node nLeft, DataFlow::Node nRight, int state0 |
-      nRight.asOperand() = right and
-      nLeft.asOperand() = left and
-      BarrierConfig::isSink(nLeft, nRight, g, state0, edge) and
-      state = getInvalidPointerToDerefSourceDelta(nRight) and
-      state0 <= state
-    )
-  }
-
-  Instruction getABarrierInstruction(int state) {
-    exists(IRGuardCondition g, ValueNumber value, Operand use, boolean edge |
-      use = value.getAUse() and
-      operandGuardChecks(pragma[only_bind_into](g), pragma[only_bind_into](use), _, state,
-        pragma[only_bind_into](edge)) and
-      result = value.getAnInstruction() and
-      g.controls(result.getBlock(), edge)
-    )
-  }
-
-  DataFlow::Node getABarrierNode() { result.asOperand() = getABarrierInstruction(_).getAUse() }
-
-  pragma[nomagic]
-  IRBlock getABarrierBlock(int state) { result.getAnInstruction() = getABarrierInstruction(state) }
-}
-
-/**
- * A configuration to track flow from a pointer-arithmetic operation found
- * by `AllocToInvalidPointerConfig` to a dereference of the pointer.
- */
-module InvalidPointerToDerefConfig implements DataFlow::ConfigSig {
-  predicate isSource(DataFlow::Node source) { invalidPointerToDerefSource(_, _, source, _) }
-
-  pragma[inline]
-  predicate isSink(DataFlow::Node sink) { isInvalidPointerDerefSink(sink, _, _, _) }
-
-  predicate isBarrier(DataFlow::Node node) {
-    node = any(DataFlow::SsaPhiNode phi | not phi.isPhiRead()).getAnInput(true)
-    or
-    node = InvalidPointerToDerefBarrier::getABarrierNode()
-  }
-}
-
-module InvalidPointerToDerefFlow = DataFlow::Global<InvalidPointerToDerefConfig>;
-
-/**
- * Holds if `source1` is dataflow node that represents an allocation that flows to the
- * left-hand side of the pointer-arithmetic `pai`, and `derefSource` is a dataflow node with
- * a pointer-value that is non-strictly upper bounded by `pai + delta`.
- *
- * For example, if `pai` is a pointer-arithmetic operation `p + size` in an expression such
- * as `(p + size) + 1` and `derefSource` is the node representing `(p + size) + 1`. In this
- * case `delta` is 1.
- */
-predicate invalidPointerToDerefSource(
-  DataFlow::Node source1, PointerArithmeticInstruction pai, DataFlow::Node derefSource, int delta
-) {
-  exists(
-    AllocToInvalidPointerFlow::PathNode1 pSource1, AllocToInvalidPointerFlow::PathNode1 pSink1,
-    AllocToInvalidPointerFlow::PathNode2 pSink2, DataFlow::Node sink1, DataFlow::Node sink2,
-    int delta0
-  |
-    pragma[only_bind_out](pSource1.getNode()) = source1 and
-    pragma[only_bind_out](pSink1.getNode()) = sink1 and
-    pragma[only_bind_out](pSink2.getNode()) = sink2 and
-    AllocToInvalidPointerFlow::flowPath(pSource1, _, pragma[only_bind_into](pSink1),
-      pragma[only_bind_into](pSink2)) and
-    // Note that `delta` is not necessarily equal to `delta0`:
-    // `delta0` is the constant offset added to the size of the allocation, and
-    // delta is the constant difference between the pointer-arithmetic instruction
-    // and the instruction computing the address for which we will search for a dereference.
-    isSinkImpl(pai, sink1, sink2, delta0) and
-    bounded2(derefSource.asInstruction(), pai, delta) and
-    delta >= 0 and
-    not derefSource.getBasicBlock() = Barrier2::getABarrierBlock(delta0)
-  )
-}
-
-/**
- * Holds if `derefSink` is a dataflow node that represents an out-of-bounds address that is about to
- * be dereferenced by `operation` (which is either a `StoreInstruction` or `LoadInstruction`), and
- * `pai` is the pointer-arithmetic operation that caused the `derefSink` to be out-of-bounds.
- */
-predicate derefSinkToOperation(
-  DataFlow::Node derefSink, PointerArithmeticInstruction pai, DataFlow::Node operation
-) {
-  exists(DataFlow::Node source, Instruction i |
-    InvalidPointerToDerefFlow::flow(pragma[only_bind_into](source),
-      pragma[only_bind_into](derefSink)) and
-    invalidPointerToDerefSource(_, pai, source, _) and
-    isInvalidPointerDerefSink(derefSink, i, _, _) and
-    i = getASuccessor(derefSink.asInstruction()) and
-    operation.asInstruction() = i
-  )
-}
+import semmle.code.cpp.security.InvalidPointerDereference.AllocationToInvalidPointer
+import semmle.code.cpp.security.InvalidPointerDereference.InvalidPointerToDereference
 
 /**
  * A configuration that represents the full dataflow path all the way from
@@ -451,20 +34,18 @@ module FinalConfig implements DataFlow::StateConfigSig {
   newtype FlowState =
     additional TInitial() or
     additional TPointerArith(PointerArithmeticInstruction pai) {
-      invalidPointerToDerefSource(_, pai, _, _)
+      operationIsOffBy(_, pai, _, _, _, _, _)
     }
 
   predicate isSource(DataFlow::Node source, FlowState state) {
     state = TInitial() and
-    exists(DataFlow::Node derefSource |
-      invalidPointerToDerefSource(source, _, derefSource, _) and
-      InvalidPointerToDerefFlow::flow(derefSource, _)
-    )
+    operationIsOffBy(source, _, _, _, _, _, _)
   }
 
   predicate isSink(DataFlow::Node sink, FlowState state) {
     exists(PointerArithmeticInstruction pai |
-      derefSinkToOperation(_, pai, sink) and state = TPointerArith(pai)
+      operationIsOffBy(_, pai, _, _, _, sink, _) and
+      state = TPointerArith(pai)
     )
   }
 
@@ -474,14 +55,9 @@ module FinalConfig implements DataFlow::StateConfigSig {
     // A step from the left-hand side of a pointer-arithmetic operation that has been
     // identified as creating an out-of-bounds pointer to the result of the pointer-arithmetic
     // operation.
-    exists(
-      PointerArithmeticInstruction pai, AllocToInvalidPointerFlow::PathNode1 p1,
-      InvalidPointerToDerefFlow::PathNode p2
-    |
-      isSinkImpl(pai, node1, _, _) and
-      invalidPointerToDerefSource(_, pai, node2, _) and
-      node1 = p1.getNode() and
-      node2 = p2.getNode() and
+    exists(PointerArithmeticInstruction pai |
+      pointerAddInstructionHasBounds(_, pai, node1, _) and
+      operationIsOffBy(_, pai, node2, _, _, _, _) and
       state1 = TInitial() and
       state2 = TPointerArith(pai)
     )
@@ -491,11 +67,9 @@ module FinalConfig implements DataFlow::StateConfigSig {
     // This step exists purely for aesthetic reasons: we want the alert to be placed at the operation
     // that causes the dereference, and not at the address that flows into the operation.
     state1 = state2 and
-    exists(DataFlow::Node derefSource, PointerArithmeticInstruction pai |
-      InvalidPointerToDerefFlow::flow(derefSource, node1) and
-      invalidPointerToDerefSource(_, pai, derefSource, _) and
+    exists(PointerArithmeticInstruction pai |
       state1 = TPointerArith(pai) and
-      derefSinkToOperation(node1, pai, node2)
+      operationIsOffBy(_, pai, _, node1, _, node2, _)
     )
   }
 }
@@ -515,19 +89,9 @@ predicate hasFlowPath(
   FinalFlow::PathNode source, FinalFlow::PathNode sink, PointerArithmeticInstruction pai,
   string operation, int delta
 ) {
-  exists(
-    DataFlow::Node derefSink, DataFlow::Node derefSource, int deltaDerefSourceAndPai,
-    int deltaDerefSinkAndDerefAddress
-  |
-    FinalFlow::flowPath(source, sink) and
-    sink.getState() = FinalConfig::TPointerArith(pai) and
-    invalidPointerToDerefSource(source.getNode(), pai, derefSource, deltaDerefSourceAndPai) and
-    InvalidPointerToDerefFlow::flow(derefSource, derefSink) and
-    derefSinkToOperation(derefSink, pai, sink.getNode()) and
-    isInvalidPointerDerefSink(derefSink, sink.getNode().asInstruction(), operation,
-      deltaDerefSinkAndDerefAddress) and
-    delta = deltaDerefSourceAndPai + deltaDerefSinkAndDerefAddress
-  )
+  FinalFlow::flowPath(source, sink) and
+  operationIsOffBy(source.getNode(), pai, _, _, operation, sink.getNode(), delta) and
+  sink.getState() = FinalConfig::TPointerArith(pai)
 }
 
 from

cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/AllocationToInvalidPointer.expected

@@ -0,0 +1,2 @@
+failures
+testFailures

cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/AllocationToInvalidPointer.ql

@@ -0,0 +1,29 @@
+import cpp
+import semmle.code.cpp.security.InvalidPointerDereference.AllocationToInvalidPointer
+import TestUtilities.InlineExpectationsTest
+import semmle.code.cpp.ir.IR
+import semmle.code.cpp.dataflow.new.DataFlow
+
+module AllocationToInvalidPointerTest implements TestSig {
+  string getARelevantTag() { result = "alloc" }
+
+  predicate hasActualResult(Location location, string element, string tag, string value) {
+    exists(DataFlow::Node allocation, PointerAddInstruction pai, int delta |
+      pointerAddInstructionHasBounds(allocation, pai, _, delta) and
+      location = pai.getLocation() and
+      element = pai.toString() and
+      tag = "alloc"
+    |
+      delta > 0 and
+      value = "L" + allocation.getLocation().getStartLine().toString() + "+" + delta.toString()
+      or
+      delta = 0 and
+      value = "L" + allocation.getLocation().getStartLine().toString()
+      or
+      delta < 0 and
+      value = "L" + allocation.getLocation().getStartLine().toString() + "-" + (-delta).toString()
+    )
+  }
+}
+
+import MakeTest<AllocationToInvalidPointerTest>

cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/InvalidPointerToDereference.expected

@@ -0,0 +1,2 @@
+failures
+testFailures

cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/InvalidPointerToDereference.ql

@@ -0,0 +1,81 @@
+import cpp
+import semmle.code.cpp.security.InvalidPointerDereference.InvalidPointerToDereference
+import TestUtilities.InlineExpectationsTest
+import semmle.code.cpp.ir.IR
+import semmle.code.cpp.dataflow.new.DataFlow
+
+string case3(DataFlow::Node derefSource, DataFlow::Node derefSink, DataFlow::Node operation) {
+  operationIsOffBy(_, _, derefSource, derefSink, _, operation, _) and
+  not exists(case2(_, _, operation)) and
+  not exists(case1(_, _, operation)) and
+  exists(int derefSourceLine, int derefSinkLine, int operationLine |
+    derefSourceLine = derefSource.getLocation().getStartLine() and
+    derefSinkLine = derefSink.getLocation().getStartLine() and
+    operationLine = operation.getLocation().getStartLine() and
+    derefSourceLine != derefSinkLine and
+    derefSinkLine != operationLine and
+    result = "L" + derefSourceLine + "->L" + derefSinkLine + "->L" + operationLine
+  )
+}
+
+string case2(DataFlow::Node derefSource, DataFlow::Node derefSink, DataFlow::Node operation) {
+  operationIsOffBy(_, _, derefSource, derefSink, _, operation, _) and
+  not exists(case1(_, _, operation)) and
+  exists(int derefSourceLine, int derefSinkLine, int operationLine |
+    derefSourceLine = derefSource.getLocation().getStartLine() and
+    derefSinkLine = derefSink.getLocation().getStartLine() and
+    operationLine = operation.getLocation().getStartLine() and
+    derefSourceLine = derefSinkLine and
+    derefSinkLine != operationLine and
+    result = "L" + derefSourceLine + "->L" + operationLine
+  )
+}
+
+string case1(DataFlow::Node derefSource, DataFlow::Node derefSink, DataFlow::Node operation) {
+  operationIsOffBy(_, _, derefSource, derefSink, _, operation, _) and
+  exists(int derefSourceLine, int derefSinkLine, int operationLine |
+    derefSourceLine = derefSource.getLocation().getStartLine() and
+    derefSinkLine = derefSink.getLocation().getStartLine() and
+    operationLine = operation.getLocation().getStartLine() and
+    derefSourceLine = derefSinkLine and
+    derefSinkLine = operationLine and
+    result = "L" + derefSourceLine
+  )
+}
+
+module InvalidPointerToDereferenceTest implements TestSig {
+  string getARelevantTag() { result = "deref" }
+
+  predicate hasActualResult(Location location, string element, string tag, string value) {
+    exists(
+      DataFlow::Node derefSource, DataFlow::Node derefSink, DataFlow::Node operation, int delta,
+      string value1, string value2
+    |
+      operationIsOffBy(_, _, derefSource, derefSink, _, operation, delta) and
+      location = operation.getLocation() and
+      element = operation.toString() and
+      tag = "deref" and
+      value = value1 + value2
+    |
+      (
+        value1 = case3(derefSource, derefSink, operation)
+        or
+        value1 = case2(derefSource, derefSink, operation)
+        or
+        value1 = case1(derefSource, derefSink, operation)
+      ) and
+      (
+        delta > 0 and
+        value2 = "+" + delta
+        or
+        delta = 0 and
+        value2 = ""
+        or
+        delta < 0 and
+        value2 = "-" + (-delta)
+      )
+    )
+  }
+}
+
+import MakeTest<InvalidPointerToDereferenceTest>

cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/test.cpp

@@ -2,10 +2,10 @@ char *malloc(int size);
 
 void test1(int size) {
     char* p = malloc(size);
-    char* q = p + size;
-    char a = *q; // BAD
+    char* q = p + size; // $ alloc=L4
+    char a = *q; // $ deref=L6 // BAD
     char b = *(q - 1); // GOOD
-    char c = *(q + 1); // BAD
+    char c = *(q + 1); // $ deref=L8+1 // BAD
     char d = *(q + size); // BAD [NOT DETECTED]
     char e = *(q - size); // GOOD
     char f = *(q + size + 1); // BAD [NOT DETECTED]
@@ -14,10 +14,10 @@ void test1(int size) {
 
 void test2(int size) {
     char* p = malloc(size);
-    char* q = p + size - 1;
+    char* q = p + size - 1; // $ alloc=L16
     char a = *q; // GOOD
     char b = *(q - 1); // GOOD
-    char c = *(q + 1); // BAD
+    char c = *(q + 1); // $ deref=L20 // BAD
     char d = *(q + size); // BAD [NOT DETECTED]
     char e = *(q - size); // GOOD
     char f = *(q + size + 1); // BAD [NOT DETECTED]
@@ -26,10 +26,10 @@ void test2(int size) {
 
 void test3(int size) {
     char* p = malloc(size + 1);
-    char* q = p + (size + 1);
-    char a = *q; // BAD
+    char* q = p + (size + 1); // $ alloc=L28+1
+    char a = *q; // $ deref=L30 // BAD
     char b = *(q - 1); // GOOD
-    char c = *(q + 1); // BAD
+    char c = *(q + 1); // $ deref=L32+1 // BAD
     char d = *(q + size); // BAD [NOT DETECTED]
     char e = *(q - size); // GOOD
     char f = *(q + size + 1); // BAD [NOT DETECTED]
@@ -38,10 +38,10 @@ void test3(int size) {
 
 void test4(int size) {
     char* p = malloc(size - 1);
-    char* q = p + (size - 1);
-    char a = *q; // BAD
+    char* q = p + (size - 1); // $ alloc=L40-1
+    char a = *q; // $ deref=L42 // BAD
     char b = *(q - 1); // GOOD
-    char c = *(q + 1); // BAD
+    char c = *(q + 1); // $ deref=L44+1 // BAD
     char d = *(q + size); // BAD [NOT DETECTED]
     char e = *(q - size); // GOOD
     char f = *(q + size + 1); // BAD [NOT DETECTED]
@@ -50,7 +50,7 @@ void test4(int size) {
 
 char* mk_array(int size, char** end) {
     char* begin = malloc(size);
-    *end = begin + size;
+    *end = begin + size; // $ alloc=L52
 
     return begin;
 }
@@ -64,7 +64,7 @@ void test5(int size) {
     }
 
     for (char* p = begin; p <= end; ++p) {
-        *p = 0; // BAD
+        *p = 0; // $ deref=L53->L62->L67 deref=L53->L66->L67 // BAD
     }
 
     for (char* p = begin; p < end; ++p) {
@@ -80,7 +80,7 @@ struct array_t {
 array_t mk_array(int size) {
     array_t arr;
     arr.begin = malloc(size);
-    arr.end = arr.begin + size;
+    arr.end = arr.begin + size; // $ alloc=L82
 
     return arr;
 }
@@ -93,7 +93,7 @@ void test6(int size) {
     }
 
     for (char* p = arr.begin; p <= arr.end; ++p) {
-        *p = 0; // BAD
+        *p = 0; // $ deref=L83->L91->L96 deref=L83->L95->L96 // BAD
     }
 
     for (char* p = arr.begin; p < arr.end; ++p) {
@@ -107,7 +107,7 @@ void test7_callee(array_t arr) {
     }
 
     for (char* p = arr.begin; p <= arr.end; ++p) {
-        *p = 0; // BAD
+        *p = 0; // $ deref=L83->L105->L110 deref=L83->L109->L110 // BAD
     }
 
     for (char* p = arr.begin; p < arr.end; ++p) {
@@ -123,7 +123,7 @@ void test8(int size) {
     array_t arr;
     char* p = malloc(size);
     arr.begin = p;
-    arr.end = p + size;
+    arr.end = p + size; // $ alloc=L124
 
     for (int i = 0; i < arr.end - arr.begin; i++) {
         *(arr.begin + i) = 0; // GOOD
@@ -141,7 +141,7 @@ void test8(int size) {
 array_t *mk_array_p(int size) {
     array_t *arr = (array_t*) malloc(sizeof(array_t));
     arr->begin = malloc(size);
-    arr->end = arr->begin + size;
+    arr->end = arr->begin + size; // $ alloc=L143
 
     return arr;
 }
@@ -154,7 +154,7 @@ void test9(int size) {
     }
 
     for (char* p = arr->begin; p <= arr->end; ++p) {
-        *p = 0; // BAD
+        *p = 0; // $ deref=L144->L156->L157 // BAD
     }
 
     for (char* p = arr->begin; p < arr->end; ++p) {
@@ -168,7 +168,7 @@ void test10_callee(array_t *arr) {
     }
 
     for (char* p = arr->begin; p <= arr->end; ++p) {
-        *p = 0; // BAD
+        *p = 0; // $ deref=L144->L166->L171 deref=L144->L170->L171 // BAD
     }
 
     for (char* p = arr->begin; p < arr->end; ++p) {
@@ -186,31 +186,31 @@ void deref_plus_one(char* q) {
 
 void test11(unsigned size) {
     char *p = malloc(size);
-    char *q = p + size - 1;
+    char *q = p + size - 1; // $ alloc=L188
     deref_plus_one(q);
 }
 
 void test12(unsigned len, unsigned index) {
     char* p = (char *)malloc(len);
-    char* end = p + len;
+    char* end = p + len; // $ alloc=L194
     
     if(p + index > end) {
         return;
     }
     
-    p[index] = '\0'; // BAD
+    p[index] = '\0'; // $ deref=L201 // BAD
 }
 
 void test13(unsigned len, unsigned index) {
     char* p = (char *)malloc(len);
-    char* end = p + len;
+    char* end = p + len; // $ alloc=L205
     
     char* q = p + index;
     if(q > end) {
         return;
     }
     
-    *q = '\0'; // BAD
+    *q = '\0'; // $ deref=L213 // BAD
 }
 
 bool unknown();
@@ -229,14 +229,14 @@ void test15(unsigned index) {
     return;
   }
   int* newname = new int[size];
-  newname[index] = 0; // GOOD [FALSE POSITIVE]
+  newname[index] = 0; // $ alloc=L231 deref=L232 // GOOD [FALSE POSITIVE]
 }
 
 void test16(unsigned index) {
   unsigned size = index + 13;
   if(size >= index) {
     int* newname = new int[size];
-    newname[index] = 0; // GOOD [FALSE POSITIVE]
+    newname[index] = 0; // $ alloc=L238 deref=L239 // GOOD [FALSE POSITIVE]
   }
 }
 
@@ -251,34 +251,34 @@ void test17(unsigned *p, unsigned x, unsigned k) {
         // The following access is okay because:
         // n = 3*p[0] + k >= p[0] + k >= p[1] + k > p[1] = i
         // (where p[0] denotes the original value for p[0])
-        p[i] = x; // GOOD [FALSE POSITIVE]
+        p[i] = x; // $ alloc=L248 deref=L254 // GOOD [FALSE POSITIVE]
     }
 }
 
 void test17(unsigned len)
 {
   int *xs = new int[len];
-  int *end = xs + len;
+  int *end = xs + len; // $ alloc=L260
   for (int *x = xs; x <= end; x++)
   {
-    int i = *x; // BAD
+    int i = *x; // $ deref=L264 // BAD
   }
 }
 
 void test18(unsigned len)
 {
   int *xs = new int[len];
-  int *end = xs + len;
+  int *end = xs + len; // $ alloc=L270
   for (int *x = xs; x <= end; x++)
   {
-    *x = 0; // BAD
+    *x = 0; // $ deref=L274 // BAD
   }
 }
 
 void test19(unsigned len)
 {
   int *xs = new int[len];
-  int *end = xs + len;
+  int *end = xs + len; // $ alloc=L280
   for (int *x = xs; x < end; x++)
   {
     int i = *x; // GOOD
@@ -288,7 +288,7 @@ void test19(unsigned len)
 void test20(unsigned len)
 {
   int *xs = new int[len];
-  int *end = xs + len;
+  int *end = xs + len; // $ alloc=L290
   for (int *x = xs; x < end; x++)
   {
     *x = 0; // GOOD
@@ -305,13 +305,13 @@ void test21() {
 
   for (int i = 0; i < n; i += 2) {
     xs[i] = test21_get(i); // GOOD
-    xs[i+1] = test21_get(i+1); // GOOD [FALSE POSITIVE]
+    xs[i+1] = test21_get(i+1); // $ alloc=L304 alloc=L304-1 deref=L308 // GOOD [FALSE POSITIVE]
   }
 }
 
 void test22(unsigned size, int val) {
   char *xs = new char[size];
-  char *end = xs + size; // GOOD
+  char *end = xs + size; // $ alloc=L313 // GOOD
   char **current = &end;
   do {
     if (*current - xs < 1) // GOOD
@@ -323,7 +323,7 @@ void test22(unsigned size, int val) {
 
 void test23(unsigned size, int val) {
   char *xs = new char[size];
-  char *end = xs + size;
+  char *end = xs + size; // $ alloc=L325
   char **current = &end;
 
   if (val < 1) {
@@ -345,7 +345,7 @@ void test23(unsigned size, int val) {
 
 void test24(unsigned size) {
   char *xs = new char[size];
-  char *end = xs + size;
+  char *end = xs + size; // $ alloc=L347
   if (xs < end) {
     int val = *xs++; // GOOD
   }
@@ -353,16 +353,16 @@ void test24(unsigned size) {
 
 void test25(unsigned size) {
   char *xs = new char[size];
-  char *end = xs + size;
+  char *end = xs + size; // $ alloc=L355
   char *end_plus_one = end + 1;
-  int val1 = *end_plus_one; // BAD
-  int val2 = *(end_plus_one + 1); // BAD
+  int val1 = *end_plus_one; // $ deref=L358+1 // BAD
+  int val2 = *(end_plus_one + 1); // $ deref=L359+2 // BAD
 }
 
 void test26(unsigned size) {
   char *xs = new char[size];
   char *p = xs;
-  char *end = p + size;
+  char *end = p + size; // $ alloc=L363
 
   if (p + 4 <= end) {
     p += 4;
@@ -375,18 +375,18 @@ void test26(unsigned size) {
 
 void test27(unsigned size, bool b) {
   char *xs = new char[size];
-  char *end = xs + size;
+  char *end = xs + size; // $ alloc=L377
 
   if (b) {
     end++;
   }
 
-  int val = *end; // BAD
+  int val = *end; // $ deref=L384+1 // BAD
 }
 
 void test28(unsigned size) {
   char *xs = new char[size];
-  char *end = &xs[size];
+  char *end = &xs[size]; // $ alloc=L388
   if (xs >= end)
     return;
   xs++;
@@ -397,7 +397,7 @@ void test28(unsigned size) {
 
 void test28_simple(unsigned size) {
   char *xs = new char[size];
-  char *end = &xs[size];
+  char *end = &xs[size]; // $ alloc=L399
   if (xs < end) {
     xs++;
     if (xs < end) {
@@ -408,46 +408,46 @@ void test28_simple(unsigned size) {
 
 void test28_simple2(unsigned size) {
   char *xs = new char[size];
-  char *end = &xs[size];
+  char *end = &xs[size]; // $ alloc=L410
   if (xs < end) {
     xs++;
     if (xs < end + 1) {
-      xs[0] = 0;  // BAD
+      xs[0] = 0; // $ deref=L415 // BAD
     }
   }
 }
 
 void test28_simple3(unsigned size) {
   char *xs = new char[size];
-  char *end = &xs[size];
+  char *end = &xs[size]; // $ alloc=L421
   if (xs < end) {
     xs++;
     if (xs - 1 < end) {
-      xs[0] = 0;  // BAD
+      xs[0] = 0; // $ deref=L426 // BAD
     }
   }
 }
 
 void test28_simple4(unsigned size) {
   char *xs = new char[size];
-  char *end = &xs[size];
+  char *end = &xs[size]; // $ alloc=L432
   if (xs < end) {
     end++;
     xs++;
     if (xs < end) {
-      xs[0] = 0;  // BAD
+      xs[0] = 0; // $ deref=L438 // BAD
     }
   }
 }
 
 void test28_simple5(unsigned size) {
   char *xs = new char[size];
-  char *end = &xs[size];
+  char *end = &xs[size]; // $ alloc=L444
   end++;
   if (xs < end) {
     xs++;
     if (xs < end) {
-      xs[0] = 0;  // BAD
+      xs[0] = 0; // $ deref=L450 // BAD
     }
   }
 }
@@ -466,7 +466,7 @@ void test28_simple6(unsigned size) {
 
 void test28_simple7(unsigned size) {
   char *xs = new char[size];
-  char *end = &xs[size];
+  char *end = &xs[size]; // $ alloc=L468
   end++;
   if (xs < end) {
     xs++;
@@ -478,12 +478,12 @@ void test28_simple7(unsigned size) {
 
 void test28_simple8(unsigned size) {
   char *xs = new char[size];
-  char *end = &xs[size];
+  char *end = &xs[size]; // $ alloc=L480
   end += 500;
   if (xs < end) {
     xs++;
     if (xs < end - 1) {
-      xs[0] = 0;  // BAD
+      xs[0] = 0; // $ deref=L486+498 // BAD
     }
   }
 }
@@ -545,7 +545,7 @@ void test31_simple2(unsigned size, unsigned src_pos)
     src_pos = size;
   }
   if (src_pos < size + 1) {
-    xs[src_pos] = 0; // BAD
+    xs[src_pos] = 0; // $ alloc=L543 deref=L548 // BAD
   }
 }
 
@@ -556,7 +556,7 @@ void test31_simple3(unsigned size, unsigned src_pos)
     src_pos = size;
   }
   if (src_pos - 1 < size) {
-    xs[src_pos] = 0; // BAD
+    xs[src_pos] = 0; // $ alloc=L554 deref=L559 // BAD
   }
 }
 
@@ -644,13 +644,13 @@ void test31_simple1_sub1(unsigned size, unsigned src_pos)
     src_pos = size;
   }
   if (src_pos < size) {
-    xs[src_pos] = 0; // BAD
+    xs[src_pos] = 0; // $ alloc=L642-1 deref=L647 // BAD
   }
 }
 
 void test32(unsigned size) {
   char *xs = new char[size];
-  char *end = &xs[size];
+  char *end = &xs[size]; // $ alloc=L652
   if (xs >= end)
     return;
   xs++;
@@ -659,7 +659,7 @@ void test32(unsigned size) {
   xs++;
   if (xs >= end)
     return;
-  xs[0] = 0; // GOOD [FALSE POSITIVE]
+  xs[0] = 0; // $ deref=L656->L662+1 deref=L657->L662+1 GOOD [FALSE POSITIVE]
 }
 
 void test33(unsigned size, unsigned src_pos)
@@ -672,12 +672,12 @@ void test33(unsigned size, unsigned src_pos)
   while (dst_pos < size - 1) {
     dst_pos++;
     if (true)
-      xs[dst_pos++] = 0; // GOOD [FALSE POSITIVE]
+      xs[dst_pos++] = 0; // $ alloc=L667+1 deref=L675 // GOOD [FALSE POSITIVE]
   }
 }
 
 int* pointer_arithmetic(int *p, int offset) {
-  return p + offset;
+  return p + offset; // $ alloc=L684
 }
 
 void test_missing_call_context_1(unsigned size) {
@@ -688,5 +688,5 @@ void test_missing_call_context_1(unsigned size) {
 void test_missing_call_context_2(unsigned size) {
   int* p = new int[size];
   int* end_minus_one = pointer_arithmetic(p, size - 1);
-  *end_minus_one = '0'; // GOOD
+  *end_minus_one = '0'; // $ deref=L680->L690->L691 // GOOD
 }