[herd] Modify tests to match new fault syntax

diaolo01 · artkhyzha · commit 78f3a1c4cfcf · 2026-02-09T18:24:49.000Z
diff --git a/herd/tests/instructions/AArch64.PAC/A13.litmus.expected b/herd/tests/instructions/AArch64.PAC/A13.litmus.expected
@@ -1,6 +1,6 @@
 Test A13 Required
 States 1
- Fault(P0,x,MMU:Translation);
+ Fault(P0,x,D-MMU:Translation);
 Ok
 Witnesses
 Positive: 1 Negative: 0
diff --git a/herd/tests/instructions/AArch64.PAC/A14.litmus.expected b/herd/tests/instructions/AArch64.PAC/A14.litmus.expected
@@ -1,6 +1,6 @@
 Test A14 Required
 States 1
- Fault(P0,x,MMU:Translation);
+ Fault(P0,x,D-MMU:Translation);
 Ok
 Witnesses
 Positive: 1 Negative: 0
diff --git a/herd/tests/instructions/AArch64.kvm/A004.litmus.expected b/herd/tests/instructions/AArch64.kvm/A004.litmus.expected
@@ -1,6 +1,6 @@
 Test A004 Required
 States 1
- Fault(P0:L0,x,MMU:Translation);
+ Fault(P0:L0,x,D-MMU:Translation);
 Ok
 Witnesses
 Positive: 1 Negative: 0
diff --git a/herd/tests/instructions/AArch64.kvm/A013.litmus.expected b/herd/tests/instructions/AArch64.kvm/A013.litmus.expected
@@ -1,6 +1,6 @@
 Test A013 Required
 States 1
- Fault(P0:L0,UndefinedInstruction); Fault(P0:L1,x,MMU:Translation); Fault(P0:L2,y,MMU:AccessFlag);
+ Fault(P0:L0,UndefinedInstruction); Fault(P0:L1,x,D-MMU:Translation); Fault(P0:L2,y,D-MMU:AccessFlag);
 Ok
 Witnesses
 Positive: 1 Negative: 0
diff --git a/herd/tests/instructions/AArch64.kvm/F000.litmus.expected b/herd/tests/instructions/AArch64.kvm/F000.litmus.expected
@@ -1,6 +1,6 @@
 Test F000 Required
 States 1
- Fault(P0:L0,x,MMU:Translation);
+ Fault(P0:L0,x,D-MMU:Translation);
 Ok
 Witnesses
 Positive: 1 Negative: 0
diff --git a/herd/tests/instructions/AArch64.kvm/F002.litmus.expected b/herd/tests/instructions/AArch64.kvm/F002.litmus.expected
@@ -1,6 +1,6 @@
 Test F002 Required
 States 1
- Fault(P0:L0,x,MMU:Permission);
+ Fault(P0:L0,x,D-MMU:Permission);
 Ok
 Witnesses
 Positive: 1 Negative: 0
diff --git a/herd/tests/instructions/AArch64.kvm/MP-I2V+rel+dmb.ld.litmus.expected b/herd/tests/instructions/AArch64.kvm/MP-I2V+rel+dmb.ld.litmus.expected
@@ -1,6 +1,6 @@
 Test MP-I2V+rel+dmb.ld Allowed
 States 2
-1:X0=0; Fault(P1:L0,y,MMU:Translation);
+1:X0=0; Fault(P1:L0,y,D-MMU:Translation);
 1:X0=1;  ~Fault(P1:L0,y);
 No
 Witnesses
diff --git a/herd/tests/instructions/AArch64.kvm/MP-I2V+rel+noret-dmb.ld.litmus.expected b/herd/tests/instructions/AArch64.kvm/MP-I2V+rel+noret-dmb.ld.litmus.expected
@@ -1,6 +1,6 @@
 Test MP-I2V+rel+noret-dmb.ld Allowed
 States 2
-1:X0=0; Fault(P1:L0,y,MMU:Translation);
+1:X0=0; Fault(P1:L0,y,D-MMU:Translation);
 1:X0=1;  ~Fault(P1:L0,y);
 No
 Witnesses
diff --git a/herd/tests/instructions/AArch64.kvm/P019.litmus.expected b/herd/tests/instructions/AArch64.kvm/P019.litmus.expected
@@ -1,7 +1,7 @@
 Test P019 Allowed
 States 2
-[x]=0; [PTE(x)]=(oa:PA(x), af:0, db:0, dbm:1); Fault(P0,x,MMU:Permission);
-[x]=0; [PTE(x)]=(oa:PA(x), db:0, dbm:1); Fault(P0,x,MMU:Permission);
+[x]=0; [PTE(x)]=(oa:PA(x), af:0, db:0, dbm:1); Fault(P0,x,D-MMU:Permission);
+[x]=0; [PTE(x)]=(oa:PA(x), db:0, dbm:1); Fault(P0,x,D-MMU:Permission);
 Ok
 Witnesses
 Positive: 3 Negative: 6
diff --git a/herd/tests/instructions/AArch64.kvm/R019.litmus.expected b/herd/tests/instructions/AArch64.kvm/R019.litmus.expected
@@ -1,7 +1,7 @@
 Test R019 Allowed
 States 2
-[x]=42; [PTE(x)]=(oa:PA(x), af:0, db:0, dbm:1); Fault(P0,x,MMU:Permission);
-[x]=42; [PTE(x)]=(oa:PA(x), db:0, dbm:1); Fault(P0,x,MMU:Permission);
+[x]=42; [PTE(x)]=(oa:PA(x), af:0, db:0, dbm:1); Fault(P0,x,D-MMU:Permission);
+[x]=42; [PTE(x)]=(oa:PA(x), db:0, dbm:1); Fault(P0,x,D-MMU:Permission);
 Ok
 Witnesses
 Positive: 3 Negative: 6
diff --git a/herd/tests/instructions/AArch64.vmsa+ifetch/A006.litmus.expected b/herd/tests/instructions/AArch64.vmsa+ifetch/A006.litmus.expected
@@ -7,5 +7,5 @@ Positive: 1 Negative: 0
 Flag combining-vmsa-and-ifetch-is-not-supported
 Condition forall (fault(P0:Page0,I-MMU:Translation))
 Observation A006 Always 1 0
-Hash=e8bde7e3620aef33ad527b86e16a3165
+Hash=cc91e34143390ee14eeb05a9c0da6e90
 
diff --git a/herd/tests/instructions/AArch64.vmsa+ifetch/A008.litmus.expected b/herd/tests/instructions/AArch64.vmsa+ifetch/A008.litmus.expected
@@ -7,5 +7,5 @@ Positive: 1 Negative: 0
 Flag combining-vmsa-and-ifetch-is-not-supported
 Condition forall (fault(P0:Page0,I-MMU:AccessFlag))
 Observation A008 Always 1 0
-Hash=0c8f5aa3cdb65d2dccba1bdd75aa8203
+Hash=7c04c1b58c33689204712ff757a621ff
 
diff --git a/herd/tests/instructions/AArch64.vmsa+ifetch/A010.litmus.expected b/herd/tests/instructions/AArch64.vmsa+ifetch/A010.litmus.expected
@@ -6,5 +6,6 @@ Witnesses
 Positive: 1 Negative: 0
 Flag combining-vmsa-and-ifetch-is-not-supported
 Condition forall (fault(P0:Page0,I-MMU:Permission))
-Observation A008 Always 1 0
-Hash=cb0a8561acabcc5a329a5e61f8d9d457
+Observation A010 Always 1 0
+Hash=cb0a8561acabcc5a329a5e61f8d9d457
+
diff --git a/herd/tests/instructions/AArch64.vmsa+ifetch/A011.litmus.expected b/herd/tests/instructions/AArch64.vmsa+ifetch/A011.litmus.expected
@@ -6,5 +6,6 @@ Witnesses
 Positive: 1 Negative: 0
 Flag combining-vmsa-and-ifetch-is-not-supported
 Condition forall (0:X0=1)
-Observation A007 Always 1 0
-Hash=664b4fb6731a307c4de1b8e71c757cb3
+Observation A011 Always 1 0
+Hash=9c258d3306eb6bfbf71ce598a396a20e
+
diff --git a/herd/tests/instructions/AArch64.vmsa+mte/A011.litmus.expected b/herd/tests/instructions/AArch64.vmsa+mte/A011.litmus.expected
@@ -1,7 +1,7 @@
 Test A011 Allowed
 States 3
 [x]=0; Fault(P0:L0,x:red,TagCheck);
-[x]=0; Fault(P0:L0,x:red,MMU:Permission);
+[x]=0; Fault(P0:L0,x:red,D-MMU:Permission);
 [x]=1;  ~Fault(P0:L0,x);
 Ok
 Witnesses
diff --git a/herd/tests/instructions/AArch64.vmsa+mte/A012.litmus.expected b/herd/tests/instructions/AArch64.vmsa+mte/A012.litmus.expected
@@ -1,7 +1,7 @@
 Test A012 Allowed
 States 3
 [x]=0; Fault(P0:L0,x:red,TagCheck);
-[x]=0; Fault(P0:L0,x:red,MMU:Permission);
+[x]=0; Fault(P0:L0,x:red,D-MMU:Permission);
 [x]=1;  ~Fault(P0:L0,x);
 Ok
 Witnesses
