Merge pull request #1762 from relokin/catalogue-fixes2

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

This PR fixes a set of issues in the AArch64 catalogue tests:

- fix register size mismatches in aarch64-ifetch WRC tests
- add explicit types for registers that hold labels in aarch64-ifetch tests
- stop checking for faults in aarch64-VMSA tests when a fault handler is present

The changes are limited to catalogue litmus tests:
- catalogue/aarch64-ifetch/tests/...
- catalogue/aarch64-VMSA/tests/...

Author: relokin

catalogue/aarch64-VMSA/shelf.py

@@ -112,7 +112,6 @@
     "tests/F2.mod.litmus",
     "tests/F2S+DSB-ETS.litmus",
     "tests/F2S.litmus",
-    "tests/F2Sdb+DSB-ETS.litmus",
     "tests/F2V.litmus",
     "tests/F3.litmus",
     "tests/F4.litmus",
@@ -802,7 +801,6 @@
     "tests/needTLBI2.litmus",
     "tests/permchange-M-shoot+DMB.ISH.litmus",
     "tests/newlob/LB+dmb.sy+acq-HU.litmus",
-    "tests/newlob/LB+dmb.sy+dmb.sy-HU.litmus",
     "tests/newlob/LB+dmb.sy+dsb.sy-HU.litmus",
     "tests/newlob/LB+dmb.sy+dsb.sy-isb-HU.litmus",
     "tests/newlob/LB+dmb.sy+pickaddr-po-HUdb.litmus",

catalogue/aarch64-VMSA/tests/@armv8-a

@@ -92,7 +92,6 @@ F2.mod-with-type+BBM2.litmus
 F2.mod.litmus
 F2S+DSB-ETS.litmus
 F2S.litmus
-F2Sdb+DSB-ETS.litmus
 F2V.litmus
 F3.litmus
 F4.litmus

catalogue/aarch64-VMSA/tests/CASAL+FAIL+FH.litmus

@@ -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)

catalogue/aarch64-VMSA/tests/CASAL+FAIL2+FH.litmus

@@ -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)

catalogue/aarch64-VMSA/tests/F2Sdb+DSB-ETS.litmus

@@ -1,5 +1,4 @@
 LB+dmb.sy+acq-HU.litmus
-LB+dmb.sy+dmb.sy-HU.litmus
 LB+dmb.sy+dsb.sy-HU.litmus
 LB+dmb.sy+dsb.sy-isb-HU.litmus
 LB+dmb.sy+pickaddr-po-HUdb.litmus

catalogue/aarch64-VMSA/tests/newlob/@all

@@ -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)

catalogue/aarch64-VMSA/tests/newlob/LB+dmb.sy+dmb.sy-HU.litmus

@@ -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")

catalogue/aarch64-VMSA/tests/newlob/S+dsb.sy-tlbi-dsb.sy+ctrl.litmus

@@ -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")