@@ -645,13 +645,7 @@ Memory Instructions
645
645
646
646
11. Pop the value :math: `\I32 .\CONST ~i` from the stack.
647
647
648
- 12. If :math: `n` is :math: `0 `, then:
649
-
650
- a. If :math: `i` is larger than the length of :math: `\X {mem}.\MIDATA `, then:
651
-
652
- i. Trap.
653
-
654
- 13. Else:
648
+ 12. Else:
655
649
656
650
a. Push the value :math: `\I32 .\CONST ~i` to the stack.
657
651
@@ -678,14 +672,7 @@ Memory Instructions
678
672
\end {array} \\
679
673
\begin {array}{lcl@{\qquad }l}
680
674
S; F; (\I32 .\CONST ~i)~\val ~(\I32 .\CONST ~0 )~(\MEMORYFILL ) &\stepto & S; F; \epsilon
681
- \end {array}
682
- \\ \qquad
683
- (\iff i \leq |\SMEMS [F.\AMODULE .\MIMEMS [0 ]]|) \\
684
- \begin {array}{lcl@{\qquad }l}
685
- S; F; (\I32 .\CONST ~i)~\val ~(\I32 .\CONST ~0 )~(\MEMORYFILL ) &\stepto & S; F; \TRAP
686
- \end {array}
687
- \\ \qquad
688
- (\otherwise ) \\
675
+ \end {array} \\
689
676
\end {array}
690
677
691
678
@@ -728,17 +715,7 @@ Memory Instructions
728
715
729
716
16. Pop the value :math: `\I32 .\CONST ~d` from the stack.
730
717
731
- 17. If :math: `n` is :math: `0 `, then:
732
-
733
- a. If :math: `d` is larger than the length of :math: `\X {mem}.\MIDATA `, then:
734
-
735
- i. Trap.
736
-
737
- b. If :math: `s` is larger than the length of :math: `\X {data}.\DIINIT `, then:
738
-
739
- i. Trap.
740
-
741
- 18. Else:
718
+ 17. Else:
742
719
743
720
a. Push the value :math: `\I32 .\CONST ~d` to the stack.
744
721
@@ -760,6 +737,10 @@ Memory Instructions
760
737
~\\[-1 ex]
761
738
\begin {array}{l}
762
739
\begin {array}{lcl@{\qquad }l}
740
+ S; F; (\I32 .\CONST ~d)~(\I32 .\CONST ~s)~(\I32 .\CONST ~0 )~(\MEMORYINIT ~x) &\stepto & S; F; \epsilon
741
+ \end {array}
742
+ \\[ 1 ex]
743
+ \begin {array}{lcl@{\qquad }l}
763
744
S; F; (\I32 .\CONST ~d)~(\I32 .\CONST ~s)~(\I32 .\CONST ~(n+1 ))~(\MEMORYINIT ~x) &\stepto & S; F;
764
745
\begin {array}[t]{@{}l@{}}
765
746
(\I32 .\CONST ~d)~(\I32 .\CONST ~b)~(\I32 \K {.}\STORE\K {8 }~\{ \OFFSET ~0 , \ALIGN ~0 \}) \\
@@ -773,15 +754,6 @@ Memory Instructions
773
754
\end {array}
774
755
\\[ 1 ex]
775
756
\begin {array}{lcl@{\qquad }l}
776
- S; F; (\I32 .\CONST ~d)~(\I32 .\CONST ~(s)~(\I32 .\CONST ~0 )~(\MEMORYINIT ~x) &\stepto & S; F; \epsilon
777
- \end {array}
778
- \\ \qquad
779
- \begin {array}[t]{@{}r@{~}l@{}}
780
- (\iff & d \leq |S.\SMEMS [F.\AMODULE .\MIMEMS [0 ]].\MIDATA | \\
781
- \wedge & s \leq |S.\SDATA [F.\AMODULE .\MIDATAS [x]].\DIINIT |) \\
782
- \end {array}
783
- \\[ 1 ex]
784
- \begin {array}{lcl@{\qquad }l}
785
757
S; F; (\I32 .\CONST ~d)~(\I32 .\CONST ~s)~(\I32 .\CONST ~n)~(\MEMORYINIT ~x) &\stepto & S; F; \TRAP
786
758
\end {array}
787
759
\\ \qquad
@@ -877,17 +849,7 @@ Table Instructions
877
849
878
850
16. Pop the value :math: `\I32 .\CONST ~d` from the stack.
879
851
880
- 17. If :math: `n` is :math: `0 `, then:
881
-
882
- a. If :math: `d` is larger than the length of :math: `\X {table}.\TIELEM `, then:
883
-
884
- i. Trap.
885
-
886
- b. If :math: `s` is larger than the length of :math: `\X {elem}.\EIINIT `, then:
887
-
888
- i. Trap.
889
-
890
- 18. Else:
852
+ 17. Else:
891
853
892
854
a. Push the value :math: `\I32 .\CONST ~d` to the stack.
893
855
@@ -907,6 +869,10 @@ Table Instructions
907
869
~\\[-1 ex]
908
870
\begin {array}{l}
909
871
\begin {array}{lcl@{\qquad }l}
872
+ S; F; (\I32 .\CONST ~d)~(\I32 .\CONST ~(s)~(\I32 .\CONST ~0 )~(\TABLEINIT ~x) &\stepto & S; F; \epsilon
873
+ \end {array}
874
+ \\[ 1 ex]
875
+ \begin {array}{lcl@{\qquad }l}
910
876
S; F; (\I32 .\CONST ~d)~(\I32 .\CONST ~s)~(\I32 .\CONST ~(n+1 ))~(\TABLEINIT ~x) &\stepto & S; F;
911
877
\begin {array}[t]{@{}l@{}}
912
878
(\I32 .\CONST ~d)~\funcelem ~\TABLESET \\
@@ -920,15 +886,6 @@ Table Instructions
920
886
\end {array}
921
887
\\[ 1 ex]
922
888
\begin {array}{lcl@{\qquad }l}
923
- S; F; (\I32 .\CONST ~d)~(\I32 .\CONST ~(s)~(\I32 .\CONST ~0 )~(\TABLEINIT ~x) &\stepto & S; F; \epsilon
924
- \end {array}
925
- \\ \qquad
926
- \begin {array}[t]{@{}r@{~}l@{}}
927
- (\iff & d \leq |S.\STABLES [F.\AMODULE .\MITABLES [0 ]].\TIELEM | \\
928
- \wedge & s \leq |S.\SELEM [F.\AMODULE .\MIELEMS [x]].\EIINIT |) \\
929
- \end {array}
930
- \\[ 1 ex]
931
- \begin {array}{lcl@{\qquad }l}
932
889
S; F; (\I32 .\CONST ~d)~(\I32 .\CONST ~s)~(\I32 .\CONST ~n)~(\TABLEINIT ~x) &\stepto & S; F; \TRAP
933
890
\end {array}
934
891
\\ \qquad
0 commit comments