RULE-8-7-1: PointerArithmeticFormsAnInvalidPointer does not terminate when pointer arithmetic forms a data-flow cycle #1217

Describe the bug

The query cpp/misra/pointer-arithmetic-forms-an-invalid-pointer does not terminate on code where the result of a constant-offset pointer addition flows back into its own base, as p = p + 1 does in a loop.

The recursive case of srcSinkLengthMap computes currentOffset = previousOffset + sinkOffset without a bound:

/* Recursive case: A fat pointer is derived from a fat pointer. */
exists(int previousOffset |
  srcSinkLengthMap(_, start, _, srcOffset, previousOffset, length) and
  currentOffset = previousOffset + sinkOffset
)

On a data-flow cycle with a nonzero offset, each iteration derives a new, larger currentOffset. The predicate has no fixpoint, so evaluation runs until it is killed.

To Reproduce

1. Save this file as repro.cpp:

   int main() {
     char buf[4] = {};
     const char* p = buf;
     while (*p != 0) {
       p = p + 1;
     }
     return 0;
   }

2. Create a database:

   codeql database create db --language=cpp --command="g++ -c repro.cpp -o repro.o"

3. Run the query from the released misra-cpp-coding-standards pack:

   codeql query run --database=db --additional-packs=<packs> \
       <packs>/misra-cpp/rules/RULE-8-7-1/PointerArithmeticFormsAnInvalidPointer.ql

4. Evaluation starts and does not finish.

Expected behavior

The query terminates. Extending a chain only while its offset is valid bounds the recursion. The select clause still reports the first invalid offset of each chain, and it no longer reports pointers derived from an already invalid pointer:

       /* Recursive case: A fat pointer is derived from a fat pointer. */
       exists(int previousOffset |
         srcSinkLengthMap(_, start, _, srcOffset, previousOffset, length) and
+        previousOffset >= 0 and
+        previousOffset <= length and
         currentOffset = previousOffset + sinkOffset
       )

With this change, the query finishes on repro.cpp and reports p + 1 at index 5 for an object of length 4. That result follows from the query's path insensitivity, which is a separate matter.