Restrict offsets to index type's range in validation (#79)

document/core/syntax/instructions.rst

@@ -683,7 +683,7 @@ Instructions in this group are concerned with linear :ref:`memory <syntax-mem>`.
  \DATADROP~\dataidx \\
  \end{array}
 
-Memory is accessed with |LOAD| and |STORE| instructions for the different :ref:`number types <syntax-numtype>` and `vector types <syntax-vectype>`.
+Memory is accessed with |LOAD| and |STORE| instructions for the different :ref:`number types <syntax-numtype>` and :ref:`vector types <syntax-vectype>`.
 They all take a :ref:`memory index <syntax-memidx>` and a *memory immediate* |memarg| that contains an address *offset* and the expected *alignment* (expressed as the exponent of a power of 2).
 
 Integer loads and stores can optionally specify a *storage size* that is smaller than the :ref:`bit width <syntax-numtype>` of the respective value type.
@@ -692,7 +692,7 @@ In the case of loads, a sign extension mode |sx| is then required to select appr
 Vector loads can specify a shape that is half the :ref:`bit width <syntax-valtype>` of |V128|. Each lane is half its usual size, and the sign extension mode |sx| then specifies how the smaller lane is extended to the larger lane.
 Alternatively, vector loads can perform a *splat*, such that only a single lane of the specified storage size is loaded, and the result is duplicated to all lanes.
 
-The static address offset is added to the dynamic address operand, yielding a 33 bit *effective address* that is the zero-based index at which the memory is accessed.
+The static address offset is added to the dynamic address operand, yielding a 33-bit or 65-bit *effective address* that is the zero-based index at which the memory is accessed.
 All values are read and written in |LittleEndian|_ byte order.
 A :ref:`trap <trap>` results if any of the accessed memory bytes lies outside the address range implied by the memory's current size.
 

document/core/valid/instructions.rst

@@ -1509,6 +1509,8 @@ Memory Instructions
 
 * Let :math:`\X{it}~\limits` be the :ref:`memory type <syntax-memtype>` :math:`C.\CMEMS[x]`.
 
+* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{it}|}`.
+
 * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width <syntax-numtype>` of :math:`t` divided by :math:`8`.
 
 * Then the instruction is valid with type :math:`[\X{it}] \to [t]`.
@@ -1517,6 +1519,8 @@ Memory Instructions
  \frac{
  C.\CMEMS[x] = \X{it}~\limits
  \qquad
+ \memarg.\OFFSET < 2^{|\X{it}|}
+ \qquad
  2^{\memarg.\ALIGN} \leq |t|/8
  }{
  C \vdashinstr t\K{.load}~x~\memarg : [\X{it}] \to [t]
@@ -1532,6 +1536,8 @@ Memory Instructions
 
 * Let :math:`\X{it}~\limits` be the :ref:`memory type <syntax-memtype>` :math:`C.\CMEMS[x]`.
 
+* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{it}|}`.
+
 * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8`.
 
 * Then the instruction is valid with type :math:`[\X{it}] \to [t]`.
@@ -1540,6 +1546,8 @@ Memory Instructions
  \frac{
  C.\CMEMS[x] = \X{it}~\limits
  \qquad
+ \memarg.\OFFSET < 2^{|\X{it}|}
+ \qquad
  2^{\memarg.\ALIGN} \leq N/8
  }{
  C \vdashinstr t\K{.load}N\K{\_}\sx~x~\memarg : [\X{it}] \to [t]
@@ -1553,6 +1561,8 @@ Memory Instructions
 
 * Let :math:`\X{it}~\limits` be the :ref:`memory type <syntax-memtype>` :math:`C.\CMEMS[x]`.
 
+* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{it}|}`.
+
 * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width <syntax-numtype>` of :math:`t` divided by :math:`8`.
 
 * Then the instruction is valid with type :math:`[\X{it}~t] \to []`.
@@ -1561,6 +1571,8 @@ Memory Instructions
  \frac{
  C.\CMEMS[x] = \X{it}~\limits
  \qquad
+ \memarg.\OFFSET < 2^{|\X{it}|}
+ \qquad
  2^{\memarg.\ALIGN} \leq |t|/8
  }{
  C \vdashinstr t\K{.store}~x~\memarg : [\X{it}~t] \to []
@@ -1574,6 +1586,10 @@ Memory Instructions
 
 * The memory :math:`C.\CMEMS[x]` must be defined in the context.
 
+* Let :math:`\X{it}~\limits` be the :ref:`memory type <syntax-memtype>` :math:`C.\CMEMS[x]`.
+
+* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{it}|}`.
+
 * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8`.
 
 * Then the instruction is valid with type :math:`[\X{it}~t] \to []`.
@@ -1582,6 +1598,8 @@ Memory Instructions
  \frac{
  C.\CMEMS[x] = \X{it}~\limits
  \qquad
+ \memarg.\OFFSET < 2^{|\X{it}|}
+ \qquad
  2^{\memarg.\ALIGN} \leq N/8
  }{
  C \vdashinstr t\K{.store}N~x~\memarg : [\X{it}~t] \to []
@@ -1597,6 +1615,8 @@ Memory Instructions
 
 * Let :math:`\X{it}~\limits` be the :ref:`memory type <syntax-memtype>` :math:`C.\CMEMS[x]`.
 
+* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{it}|}`.
+
 * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8 \cdot M`.
 
 * Then the instruction is valid with type :math:`[\X{it}] \to [\V128]`.
@@ -1605,6 +1625,8 @@ Memory Instructions
  \frac{
  C.\CMEMS[x] = \X{it}~\limits
  \qquad
+ \memarg.\OFFSET < 2^{|\X{it}|}
+ \qquad
  2^{\memarg.\ALIGN} \leq N/8 \cdot M
  }{
  C \vdashinstr \K{v128.}\LOAD{N}\K{x}M\_\sx~x~\memarg : [\X{it}] \to [\V128]
@@ -1620,6 +1642,8 @@ Memory Instructions
 
 * Let :math:`\X{it}~\limits` be the :ref:`memory type <syntax-memtype>` :math:`C.\CMEMS[x]`.
 
+* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{it}|}`.
+
 * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8`.
 
 * Then the instruction is valid with type :math:`[\X{it}] \to [\V128]`.
@@ -1628,6 +1652,8 @@ Memory Instructions
  \frac{
  C.\CMEMS[x] = \X{it}~\limits
  \qquad
+ \memarg.\OFFSET < 2^{|\X{it}|}
+ \qquad
  2^{\memarg.\ALIGN} \leq N/8
  }{
  C \vdashinstr \K{v128.}\LOAD{N}\K{\_splat}~x~\memarg : [\X{it}] \to [\V128]
@@ -1643,6 +1669,8 @@ Memory Instructions
 
 * Let :math:`\X{it}~\limits` be the :ref:`memory type <syntax-memtype>` :math:`C.\CMEMS[x]`.
 
+* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{it}|}`.
+
 * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8`.
 
 * Then the instruction is valid with type :math:`[\X{it}] \to [\V128]`.
@@ -1651,6 +1679,8 @@ Memory Instructions
  \frac{
  C.\CMEMS[x] = \X{it}~\limits
  \qquad
+ \memarg.\OFFSET < 2^{|\X{it}|}
+ \qquad
  2^{\memarg.\ALIGN} \leq N/8
  }{
  C \vdashinstr \K{v128.}\LOAD{N}\K{\_zero}~x~\memarg : [\X{it}] \to [\V128]
@@ -1666,6 +1696,8 @@ Memory Instructions
 
 * Let :math:`\X{it}~\limits` be the :ref:`memory type <syntax-memtype>` :math:`C.\CMEMS[x]`.
 
+* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{it}|}`.
+
 * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8`.
 
 * The lane index :math:`\laneidx` must be smaller than :math:`128/N`.
@@ -1676,6 +1708,8 @@ Memory Instructions
  \frac{
  C.\CMEMS[x] = \X{it}~\limits
  \qquad
+ \memarg.\OFFSET < 2^{|\X{it}|}
+ \qquad
  2^{\memarg.\ALIGN} \leq N/8
  \qquad
  \laneidx < 128/N
@@ -1692,6 +1726,9 @@ Memory Instructions
 * The memory :math:`C.\CMEMS[x]` must be defined in the context.
 
 * Let :math:`\X{it}~\limits` be the :ref:`memory type <syntax-memtype>` :math:`C.\CMEMS[x]`.
+
+* The offset :math:`\memarg.\OFFSET` must be less than :math:`2^{|\X{it}|}`.
+
 * The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than :math:`N/8`.
 
 * The lane index :math:`\laneidx` must be smaller than :math:`128/N`.
@@ -1702,6 +1739,8 @@ Memory Instructions
  \frac{
  C.\CMEMS[x] = \X{it}~\limits
  \qquad
+ \memarg.\OFFSET < 2^{|\X{it}|}
+ \qquad
  2^{\memarg.\ALIGN} \leq N/8
  \qquad
  \laneidx < 128/N