Skip to content

[catalogue] Fix AArch64 ifetch typing and VMSA fault-handler expectations #1762

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
relokin wants to merge 3 commits into
base: master
Choose a base branch
from
Open

[catalogue] Fix AArch64 ifetch typing and VMSA fault-handler expectations #1762

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
ffcd54a
[catalogue] Fix register size mismatch for aarch64-ifetch WRC tests
relokin Mar 25, 2026
b30ad8e
[catalogue] Add types for registers that hold labels for aarch64-ifet…
relokin Mar 25, 2026
b54d507
[catalogue] Don't check for faults when there is a fault handler for …
relokin Mar 25, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion catalogue/aarch64-VMSA/tests/CASAL+FAIL+FH.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,4 +16,4 @@ Variant=vmsa
| L1: | ;
| LDR W5,[X2] | ;

exists (fault(P1:L0,x) /\ 1:X5=0)
exists(1:X9=label:"P1:L1" /\ 1:X5=0)
2 changes: 1 addition & 1 deletion catalogue/aarch64-VMSA/tests/CASAL+FAIL2+FH.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,4 +20,4 @@ Variant=vmsa
MOV W5,#1 | L1: | ;
STR W5,[X6] | LDR W5,[X2] | ;

exists (fault(P1:L0,x) /\ 1:X5=0)
exists (1:X9=label:"P1:L1" /\ 1:X5=0)
2 changes: 1 addition & 1 deletion catalogue/aarch64-VMSA/tests/newlob/S+dsb.sy-tlbi-dsb.sy+ctrl.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,4 +15,4 @@ Variant=vmsa
MOV W2,#1 | L0: | ;
STR W2,[X3] | | ;

exists (1:X2=1 /\ not (fault(P1,x,MMU:Permission)))
exists (1:X2=1 /\ 1:X9=0)
4 changes: 2 additions & 2 deletions catalogue/aarch64-VMSA/tests/order-via-faults/MP-via_fault_STLR.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,10 +7,10 @@ Variant=vmsa
1:X3=y; 1:X1=x; 1:X8=z;
}
P0 | P1 | P1.F ;
MOV X7,#1 | LDR W2,[X3] | ADR X9,L0 ;
MOV W7,#1 | LDR W2,[X3] | ADR X9,L0 ;
STR W7,[X8] | MOV W0,#1 | MSR ELR_EL1,X9 ;
STLR W7,[X3] | STLR W0,[X1] | LDR W10,[X8] ;
| | ERET ;
| L0: | ;

exists (1:X2=1 /\ 1:X10=0 /\ fault(P1))
exists (1:X2=1 /\ 1:X10=0 /\ 1:X9=label:"P1:L0")
4 changes: 2 additions & 2 deletions catalogue/aarch64-VMSA/tests/order-via-faults/R-via_fault_STR.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,10 +7,10 @@ Variant=vmsa
1:X3=y; 1:X1=x; 1:X8=z;
}
P0 | P1 | P1.F ;
MOV X7,#1 | MOV W2,#2 | ADR X9,L0 ;
MOV W7,#1 | MOV W2,#2 | ADR X9,L0 ;
STR W7,[X8] | STR W2,[X3] | MSR ELR_EL1,X9 ;
STLR W7,[X3] | DMB ST | LDR W10,[X8] ;
| STR W0,[X1] | ERET ;
| L0: | ;

exists ([y]=2 /\ 1:X10=0 /\ fault(P1))
exists ([y]=2 /\ 1:X10=0 /\ 1:X9=label:"P1:L0")
4 changes: 3 additions & 1 deletion catalogue/aarch64-ifetch/tests/DIC0-IDC0/MP.RF+cachesync+switch-ctrl.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,13 @@
AArch64 MP.RF+cachesync+switch-ctrl
Hash=6319cdacf8d9276fce801d15c883acd7
(* switch table -- this one is allowed *)
(* Will suggests that compilers require that this test be allowed iff the miniJit01 is allowed *)
{
[x]=P1:Lend;
0:X0=NOP; 0:X1=P1:Lself; 0:X3=x;
1:X3=x;
1:X11=P1:Lself;
ins_t *1:X1;
}
P0 | P1 ;
STR W0,[X1] | LDR X1,[X3] ;
Expand All @@ -18,4 +20,4 @@ AArch64 MP.RF+cachesync+switch-ctrl
| Lold: ;
| MOV W9,#1 ;
| Lend: ;
exists (1:X9=1)
exists (1:X9=1)
4 changes: 3 additions & 1 deletion catalogue/aarch64-ifetch/tests/DIC0-IDC0/MP.RF+cachesync+switch-ctrlisb.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,13 @@
AArch64 MP.RF+cachesync+switch-ctrlisb
Hash=453c2373bfaf0de1acbab7308a8e830f
(* switch table -- this one is forbidden *)
(* Will suggests that compilers require that this test be forbidden iff the miniJit02 is forbidden *)
{
[x]=P1:Lend;
0:X0=NOP; 0:X1=P1:Lself; 0:X3=x;
1:X3=x;
1:X11=P1:Lself;
ins_t *1:X1;
}
P0 | P1 ;
STR W0,[X1] | LDR X1,[X3] ;
Expand All @@ -19,4 +21,4 @@ AArch64 MP.RF+cachesync+switch-ctrlisb
| Lold: ;
| MOV W9,#1 ;
| Lend: ;
exists (1:X9=1)
exists (1:X9=1)
4 changes: 3 additions & 1 deletion catalogue/aarch64-ifetch/tests/DIC0-IDC0/MP.RF+dc-dsb-ic-dsb+addr.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,10 @@
AArch64 MP.RF+dc-dsb-ic-dsb+addr
Hash=59f012b3284ceff1fb7a9c250ee29698
{
[z]=P1:Lend;
0:X0=NOP; 0:X1=P1:Lself; 0:X3=z;
1:X2=P1:Lself; 1:X3=z; 1:X9=0;
ins_t *1:X1;
}
P0 | P1 ;
STR W0,[X1] | LDR X1,[X3] ;
Expand All @@ -13,4 +15,4 @@ DSB ISH | MOV W9,#1 ;
STR X1,[X3] | Lend: ;
| CMP X1,X2 ;
| CSET W8,EQ ;
exists 1:X8=1 /\ 1:X9=0
exists 1:X8=1 /\ 1:X9=0
4 changes: 3 additions & 1 deletion catalogue/aarch64-ifetch/tests/DIC0-IDC0/MP.RF+dc-dsb-ic-dsb+ctrlisb.br.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,10 @@
AArch64 MP.RF+dc-dsb-ic-dsb+ctrlisb.br
Hash=efe5f360d48e0779ea53d214421998c4
{
[z]=P1:Lend;
0:X0=NOP; 0:X1=P1:Lself; 0:X3=z;
1:X2=P1:Lself; 1:X3=z; 1:X9=0;
ins_t *1:X1;
}
P0 | P1 ;
STR W0,[X1] | LDR X1,[X3] ;
Expand All @@ -16,4 +18,4 @@ STR X1,[X3] | Lself: ;
| Lend: ;
| CMP X1,X2 ;
| CSET W8,EQ ;
exists 1:X8=1 /\ 1:X9=0
exists 1:X8=1 /\ 1:X9=0
4 changes: 3 additions & 1 deletion catalogue/aarch64-ifetch/tests/DIC0-IDC0/S-self+dmb.st+fault.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,14 +1,16 @@
AArch64 S-self+dmb.st+fault
Hash=20c53bed0175ae545392c7631a4ad471
{
0:X1=x;
0:X2=0; (*any invalid instruction value*)
0:X3=P1:m0;
1:X3=x;
ins_t *1:X9;
}
P0 | P1 | P1.F ;
MOV W0,#1 |m0: | MOV W2,#2 ;
STR W0,[X1] | B l1 | STR W2,[X3] ;
DMB ST |l1: | ADR X9,l1 ;
STR W2,[X3] | | MSR ELR_EL1,X9 ;
| | ERET ;
exists(1:X2=2 /\ x=1)
exists(1:X2=2 /\ x=1)
5 changes: 3 additions & 2 deletions catalogue/aarch64-ifetch/tests/DIC0-IDC0/S.RF-dsb-iccvau-dsb-isb.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
AArch64 S.RF-dsb-iccvau-dsb-isb
Hash=5f922605f239a09dc8ea6dafc54fbd2f
Stable=X9
{
0:X0=NOP; 0:X1=P0:mod;
Expand All @@ -9,8 +10,8 @@ Stable=X9
B end | DSB SY ;
mod: | IC IVAU,X1 ;
B l0 | DSB SY ;
MOV X9,#1 | ISB ;
MOV W9,#1 | ISB ;
l0: | BLR X1 ;
RET | CMP W0,W2 ;
end: | CSET W8,EQ ;
exists(1:X8=1 /\ 1:X9=0) (* 1:X8=1 <=> 1:W2=NOP *)
exists(1:X8=1 /\ 1:X9=0) (* 1:X8=1 <=> 1:W2=NOP *)
3 changes: 2 additions & 1 deletion catalogue/aarch64-ifetch/tests/DIC0-IDC0/WRC-inst+cachesync+ctrlisb.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
AArch64 WRC-inst+cachesync+ctrlisb
Hash=3971a43cb5b943ea359fd32a35904073
Stable=X9
{ 0:X0=NOP;
0:X1=P0:mod; 1:X1=P0:mod; 2:X1=P0:mod;
Expand All @@ -13,7 +14,7 @@ Stable=X9
B end | | ;
mod: | | ;
B l0 | | ;
MOV X9,#1 | | ;
MOV W9,#1 | | ;
l0: | | ;
RET | | ;
end: | | ;
Expand Down
3 changes: 2 additions & 1 deletion catalogue/aarch64-ifetch/tests/DIC0-IDC0/WRC-inst+cachesync+dsb.ish-isb.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
AArch64 WRC-inst+cachesync+dsb.ish-isb
Hash=ce504185ca2f882ca77a75f36af5f10b
Stable=X9
{ 0:X0=NOP;
0:X1=P0:mod; 1:X1=P0:mod; 2:X1=P0:mod;
Expand All @@ -13,7 +14,7 @@ Stable=X9
B end | | ;
mod: | | ;
B l0 | | ;
MOV X9,#1 | | ;
MOV W9,#1 | | ;
l0: | | ;
RET | | ;
end: | | ;
Expand Down
3 changes: 2 additions & 1 deletion catalogue/aarch64-ifetch/tests/DIC0-IDC0/WRC-inst+cachesync+dsb.ish.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
AArch64 WRC-inst+cachesync+dsb.ish
Hash=783aa7fb941d9d368764b5847a21fcb3
Stable=X9
{ 0:X0=NOP;
0:X1=P0:mod; 1:X1=P0:mod; 2:X1=P0:mod;
Expand All @@ -13,7 +14,7 @@ Stable=X9
B end | | ;
mod: | | ;
B l0 | | ;
MOV X9,#1 | | ;
MOV W9,#1 | | ;
l0: | | ;
RET | | ;
end: | | ;
Expand Down
3 changes: 2 additions & 1 deletion catalogue/aarch64-ifetch/tests/DIC0-IDC0/WRC-inst+ctrlisb.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
AArch64 WRC-inst+ctrlisb
Hash=330105fb19f2df2836e1db4d9e2c3a66
Stable=X9
{ 0:X0=NOP;
0:X1=P0:mod; 1:X1=P0:mod; 2:X1=P0:mod;
Expand All @@ -8,7 +9,7 @@ Stable=X9
B end | MOV W2,#1 | CBNZ W2,l2 ;
mod: | STR W2,[X3] | l2: ;
B l0 | | ISB ;
MOV X9,#1 | | BLR X1 ;
MOV W9,#1 | | BLR X1 ;
l0: | | ;
RET | | ;
end: | | ;
Expand Down
3 changes: 2 additions & 1 deletion catalogue/aarch64-ifetch/tests/DIC0-IDC0/WRC-inst+dsb.ish-isb.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
AArch64 WRC-inst+dsb.ish-isb
Hash=465a8c9ba4e094202d0039bc70dcac97
Stable=X9
{ 0:X0=NOP;
0:X1=P0:mod; 1:X1=P0:mod; 2:X1=P0:mod;
Expand All @@ -8,7 +9,7 @@ Stable=X9
B end | MOV W2,#1 | DSB ISH ;
mod: | STR W2,[X3] | ISB ;
B l0 | | BLR X1 ;
MOV X9,#1 | | ;
MOV W9,#1 | | ;
l0: | | ;
RET | | ;
end: | | ;
Expand Down
3 changes: 2 additions & 1 deletion catalogue/aarch64-ifetch/tests/DIC0-IDC0/WRC-inst+dsb.ish.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
AArch64 WRC-inst+dsb.ish
Hash=cc06ac744a4fc992a36b3fa52594a251
Stable=X9
{ 0:X0=NOP;
0:X1=P0:mod; 1:X1=P0:mod; 2:X1=P0:mod;
Expand All @@ -8,7 +9,7 @@ Stable=X9
B end | MOV W2,#1 | DSB ISH ;
mod: | STR W2,[X3] | BLR X1 ;
B l0 | | ;
MOV X9,#1 | | ;
MOV W9,#1 | | ;
l0: | | ;
RET | | ;
end: | | ;
Expand Down
5 changes: 3 additions & 2 deletions catalogue/aarch64-ifetch/tests/DIC0-IDC0/WRC-inst+po+dsb-cachesyncisb.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
AArch64 WRC-inst+po+dsb-cachesyncisb
Hash=664513c2143575b760ae6106be4eb67d
Stable=X9
{ 0:X0=NOP;
0:X1=P0:mod; 1:X1=P0:mod; 2:X1=P0:mod;
Expand All @@ -8,8 +9,8 @@ Stable=X9
B end | MOV W2,#1 | DSB SY ;
mod: | STR W2,[X3] | DC CVAU,X1 ;
B l0 | | DSB SY ;
MOV X9,#1 | | IC IVAU,X1 ;
MOV W9,#1 | | IC IVAU,X1 ;
l0: | | DSB SY ;
RET | | ISB ;
end: | | BLR X1 ;
exists(1:X9=1 /\ 2:X2=1 /\ 2:X9=0)
exists(1:X9=1 /\ 2:X2=1 /\ 2:X9=0)
5 changes: 3 additions & 2 deletions catalogue/aarch64-ifetch/tests/DIC0-IDC0/WRC-inst+po+dsb-iccvau-dsb-isb.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
AArch64 WRC-inst+po+dsb-iccvau-dsb-isb
Hash=35c754818f99337b5095a3c3b7c10cdd
Stable=X9
{ 0:X0=NOP;
0:X1=P0:mod; 1:X1=P0:mod; 2:X1=P0:mod;
Expand All @@ -8,8 +9,8 @@ Stable=X9
B end | MOV W2,#1 | DSB SY ;
mod: | STR W2,[X3] | IC IVAU,X1 ;
B l0 | | DSB SY ;
MOV X9,#1 | | ISB ;
MOV W9,#1 | | ISB ;
l0: | | BLR X1 ;
RET | | ;
end: | | ;
exists(1:X9=1 /\ 2:X2=1 /\ 2:X9=0)
exists(1:X9=1 /\ 2:X2=1 /\ 2:X9=0)
3 changes: 2 additions & 1 deletion catalogue/aarch64-ifetch/tests/DIC0-IDC0/WRC-inst-mod+cachesync+po+ctrlisb.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
AArch64 WRC-inst-mod+cachesync+po+ctrlisb
Hash=f468825999709c59a024ec54a4d5eb2d
Stable=X9
{ 0:X0=NOP;
0:X1=P0:mod; 1:X1=P0:mod; 2:X1=P0:mod;
Expand All @@ -14,7 +15,7 @@ Stable=X9
B end | | ;
mod: | | ;
B l0 | | ;
MOV X9,#1 | | ;
MOV W9,#1 | | ;
l0: | | ;
RET | | ;
end: | | ;
Expand Down
3 changes: 2 additions & 1 deletion catalogue/aarch64-ifetch/tests/DIC0-IDC0/WRC-mmrb-1-nodc.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
AArch64 WRC-mmrb-1-nodc
Hash=70f9ebf2c4ca287cd3213a2018643c2e
Stable=X9
{ 1:X0=NOP;
0:X1=P0:mod; 1:X1=P0:mod; 2:X1=P0:mod;
Expand All @@ -9,7 +10,7 @@ Stable=X9
B end | MOV W2,#1 | DSB SY ;
mod: | STR W2,[X3] | ;
B l0 | | ;
MOV X9,#1 | | IC IVAU,X1 ;
MOV W9,#1 | | IC IVAU,X1 ;
l0: | | DSB SY ;
RET | | ISB ;
end: | | BLR X1 ;
Expand Down
3 changes: 2 additions & 1 deletion catalogue/aarch64-ifetch/tests/DIC0-IDC0/WRC-mmrb-1-noic.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
AArch64 WRC-mmrb-1-noic
Hash=42f81303790ffef846a25ec30ff6f968
Stable=X9
{ 1:X0=NOP;
0:X1=P0:mod; 1:X1=P0:mod; 2:X1=P0:mod;
Expand All @@ -9,7 +10,7 @@ Stable=X9
B end | MOV W2,#1 | DSB SY ;
mod: | STR W2,[X3] | DC CVAU,X1 ;
B l0 | | ;
MOV X9,#1 | | ;
MOV W9,#1 | | ;
l0: | | DSB SY ;
RET | | ISB ;
end: | | BLR X1 ;
Expand Down
3 changes: 2 additions & 1 deletion catalogue/aarch64-ifetch/tests/DIC0-IDC0/WRC-mmrb-1.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
AArch64 WRC-mmrb-1
Hash=62178e8dc65798e2b5433ec7e9bb47a8
Stable=X9
{ 1:X0=NOP;
0:X1=P0:mod; 1:X1=P0:mod; 2:X1=P0:mod;
Expand All @@ -9,7 +10,7 @@ Stable=X9
B end | MOV W2,#1 | DSB SY ;
mod: | STR W2,[X3] | DC CVAU,X1 ;
B l0 | | DSB SY ;
MOV X9,#1 | | IC IVAU,X1 ;
MOV W9,#1 | | IC IVAU,X1 ;
l0: | | DSB SY ;
RET | | ISB ;
end: | | BLR X1 ;
Expand Down
2 changes: 2 additions & 0 deletions catalogue/aarch64-ifetch/tests/DIC0-IDC0/miniJit01.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,11 @@
AArch64 miniJit01
Hash=d3d1710fc058878e5818dc35f79560cf
Variant=self
{
[x] = P1:L0 ;
0:X1=P1:L1; 0:X3=x; 0:X0=NOP;
1:X3=x; 1:X9=0;
void *1:X1;
}
P0 | P1 ;
STR W0,[X1] | LDR X1,[X3] ;
Expand Down
2 changes: 2 additions & 0 deletions catalogue/aarch64-ifetch/tests/DIC0-IDC0/miniJit02.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,11 @@
AArch64 miniJit02
Hash=230ee4762fb46026f3cda51b3d6f97fc
Variant=self
{
[x] = P1:L0 ;
0:X1=P1:L1; 0:X3=x; 0:X0=NOP;
1:X3=x; 1:X9=0; 1:X2=P1:L3;
void *1:X1;
}
P0 | P1 ;
STR W0,[X1] | LDR X1,[X3] ;
Expand Down
4 changes: 3 additions & 1 deletion catalogue/aarch64-ifetch/tests/DIC0-IDC1/IDC1.MP.RF+cachesync+switch-ctrl.litmus
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
AArch64 IDC1.MP.RF+cachesync+switch-ctrl
Hash=cbfa044af26ce69568f1bf4263e0daf6
(* switch table -- this one is allowed *)
(* Will suggests that compilers require that this test be allowed iff the miniJit01 is allowed *)
CacheType=IDC
Expand All @@ -7,6 +8,7 @@ CacheType=IDC
0:X0=NOP; 0:X1=P1:Lself; 0:X3=x;
1:X3=x;
1:X11=P1:Lself;
ins_t *1:X1;
}
P0 | P1 ;
STR W0,[X1] | LDR X1,[X3] ;
Expand All @@ -19,4 +21,4 @@ CacheType=IDC
| Lold: ;
| MOV W9,#1 ;
| Lend: ;
exists (1:X9=1)
exists (1:X9=1)
Loading
Loading