From 0f285ccce002b43dfd3b0998f800f63caf86f670 Mon Sep 17 00:00:00 2001 From: Mathias Vorreiter Pedersen Date: Sat, 5 Aug 2023 21:54:08 +0200 Subject: [PATCH] C++: Fix QLDoc. --- .../InvalidPointerToDereference.qll | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) 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 1aa7d173a27..5b2eadacd11 100644 --- a/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/InvalidPointerToDereference.qll +++ b/cpp/ql/lib/semmle/code/cpp/security/InvalidPointerDereference/InvalidPointerToDereference.qll @@ -66,11 +66,14 @@ * module. Since the node we are tracking is not necessarily _equal_ to the pointer-arithmetic instruction, but rather satisfies * `node.asInstruction() <= pai + deltaDerefSourceAndPai`, we need to account for the delta when checking if a guard is sufficiently * strong to infer that a future dereference is safe. To do this, we check that the guard guarantees that a node `n` satisfies - * `n < node + k` where `node` is a node we know is equal to the value of the dereference source (i.e., it satisfies - * `node.asInstruction() <= pai + deltaDerefSourceAndPai`) and `k <= deltaDerefSourceAndPai`. Combining this we have - * `n < node + k <= node + deltaDerefSourceAndPai <= pai + 2*deltaDerefSourceAndPai` (TODO: Oops. This math doesn't quite work out. - * I think this is because we need to redefine the `BarrierConfig` to start flow at the pointer-arithmetic instruction instead of - * at the dereference source. When combined with TODO above it's easy to show that this guard ensures that the dereference is safe). + * `n < node + k` where `node` is a node such that `node <= pai`. Thus, we know that any node `n'` such that `n' <= n + delta` where + * `delta + k <= 0` will be safe because: + * ``` + * n' <= n + delta + * < node + k + delta + * <= pai + k + delta + * <= pai + * ``` */ private import cpp