diff --git a/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/AllocationToInvalidPointer.qll b/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/AllocationToInvalidPointer.qll index 05cc53eb27e..0228f0c74ff 100644 --- a/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/AllocationToInvalidPointer.qll +++ b/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/AllocationToInvalidPointer.qll @@ -42,9 +42,9 @@ predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) { * ``` * 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]`) + * instruction `pai = a + b` such that: + * 1. the allocation flows to `a`, and + * 2. `b <= 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. */ @@ -147,8 +147,8 @@ private module InterestingPointerAddInstruction { } /** - * 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`. + * A product-flow configuration for flow from an `(allocation, size)` pair to a + * pointer-arithmetic operation `pai` such that `pai <= allocation + size`. * * The goal of this query is to find patterns such as: * ```cpp @@ -207,7 +207,7 @@ private module Config implements ProductFlow::StateConfigSig { private module AllocToInvalidPointerFlow = ProductFlow::GlobalWithState; /** - * Holds if `pai` is non-strictly upper bounded by `sink2 + delta` and `sink1` is the + * Holds if `pai` is non-strictly upper bounded by `sizeSink + delta` and `allocSink` is the * left operand of the pointer-arithmetic operation. * * For example in, @@ -216,8 +216,8 @@ private module AllocToInvalidPointerFlow = ProductFlow::GlobalWithState; * ``` * We will have: * - `pai` is `p + (size + 1)`, - * - `sink1` is `p` - * - `sink2` is `size` + * - `allocSink` is `p` + * - `sizeSink` is `size` * - `delta` is `1`. */ pragma[nomagic] @@ -237,9 +237,9 @@ private predicate pointerAddInstructionHasBounds0( } /** - * 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`. + * Holds if `allocation` flows to `allocSink` and `allocSink` represents the left operand + * of the pointer-arithmetic instruction `pai = a + b` (i.e., `allocSink = a`), and + * `b <= allocation + delta`. */ pragma[nomagic] predicate pointerAddInstructionHasBounds( diff --git a/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/InvalidPointerToDereference.qll b/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/InvalidPointerToDereference.qll index 28a127d8d20..5945e533153 100644 --- a/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/InvalidPointerToDereference.qll +++ b/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/InvalidPointerToDereference.qll @@ -85,9 +85,8 @@ private module InvalidPointerToDerefConfig implements DataFlow::ConfigSig { private import DataFlow::Global /** - * 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`. + * Holds if `allocSource` is dataflow node that represents an allocation that flows to the + * left-hand side of the pointer-arithmetic `pai`, and `derefSource <= pai + derefSourcePaiDelta`. * * 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 @@ -114,8 +113,8 @@ private predicate invalidPointerToDerefSource( /** * 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`. + * writes to an address `addr` such that `addr <= sink`, or `i` is a `LoadInstruction` that + * reads from an address `addr` such that `addr <= sink`. */ pragma[inline] private predicate isInvalidPointerDerefSink(