[llvm] [LangRef] Update the semantic of `experimental.get.vector.length` (PR #104475)

[Min-Yih Hsu via llvm-commits]

https://github.com/mshockwave created https://github.com/llvm/llvm-project/pull/104475

The previous semantics of `llvm.experimental.get.vector.length` was too permissive such that it gave optimizers a hard time on anything related to the number of iterations of VP-vectorized loops.

This patch tries to address this by assigning it a set of stricter semantics similar to that of RVV's VSETVLI instructions, while being not too RISC-V specific and leaving room for other (future) targets.

>From 2cd78f259d74f287d1edeafb75a59e4fa3efbf60 Mon Sep 17 00:00:00 2001
From: Min Hsu <min.hsu at sifive.com>
Date: Mon, 15 Jul 2024 14:29:32 -0700
Subject: [PATCH] [doc] Update the semantic of `experimental.get.vector.length`
 in LangRef

The previous semantics of `llvm.experimental.get.vector.length` was too
permissive such that it gave optimizers a hard time on anything related
to the number of iterations of VP-vectorized loops.

This patch tries to address this by assigning it a set of stricter
semantics similar to that of RVV's VSETVLI instructions, while being not
too RISC-V specific and leaving room for other (future) targets.

Co-authored-by: Craig Topper <craig.topper at sifive.com>
---
 llvm/docs/LangRef.rst | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/llvm/docs/LangRef.rst b/llvm/docs/LangRef.rst
index 5e5e9b9e8a93b1..22fd805a4685b1 100644
--- a/llvm/docs/LangRef.rst
+++ b/llvm/docs/LangRef.rst
@@ -19644,13 +19644,19 @@ in order to get the number of elements to process on each loop iteration. The
 result should be used to decrease the count for the next iteration until the
 count reaches zero.
 
-If the count is larger than the number of lanes in the type described by the
-last 2 arguments, this intrinsic may return a value less than the number of
-lanes implied by the type. The result will be at least as large as the result
-will be on any later loop iteration.
-
-This intrinsic will only return 0 if the input count is also 0. A non-zero input
-count will produce a non-zero result.
+Let ``%max_lanes`` be the number of lanes in the type described by ``%vf`` and
+``%scalable``, here are the constraints on the returned value:
+- If ``%cnt`` equals to 0, returns 0.
+- The returned value is always less or equal to ``%max_lanes``.
+- The returned value is always larger or equal to
+  ``ceil(%cnt / ceil(%cnt / %max_lanes))``.
+  - This implies that if ``%cnt`` is non-zero, the result should be non-zero
+    as well.
+  - This also implies that if ``%cnt`` is less than ``%max_lanes``, it has to
+    return ``%cnt``.
+- The returned values decrease monotonically in each loop iteration. That is,
+  the returned value of a iteration is at least as large as that of any later
+  iterations.
 
 '``llvm.experimental.vector.partial.reduce.add.*``' Intrinsic
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^