[herd] Add test

The new test checks that size mismatches are delayed.

Currently, it also reveals a problem with
the ASL+VMSA mode.

Author: maranget

herd/tests/instructions/AArch64.kvm/A031.litmus

@@ -0,0 +1,15 @@
+AArch64 A031
+(* Test the delaying of size check *)
+TTHM=P1:HA
+{
+ int z=1;
+ int x=2;
+ [PTE(z)]=(oa:PA(z),af:0);
+ pteval_t 0:X15=(oa:PA(x),af:0); 0:X14=PTE(z);
+ 1:X6=p;
+ int *p = &z;
+}
+ P0             | P1                  ;
+ STR X15,[X14]  | LDR X4,[X6]         ;
+                | LDR W5,[X4]         ;
+~exists [PTE(z)]=(oa:PA(x), af:0) /\ 1:X5=2

herd/tests/instructions/AArch64.kvm/A031.litmus.expected

@@ -0,0 +1,13 @@
+Test A031 Forbidden
+States 3
+1:X5=1; [PTE(z)]=(oa:PA(x), af:0);
+1:X5=1; [PTE(z)]=(oa:PA(x));
+1:X5=2; [PTE(z)]=(oa:PA(x));
+Ok
+Witnesses
+Positive: 14 Negative: 0
+Flag requires-BBM
+Condition ~exists ([PTE(z)]=(oa:PA(x), af:0) /\ 1:X5=2)
+Observation A031 Never 0 14
+Hash=b49f887241d4043b0d917f97925e00ab
+

herd/tests/instructions/AArch64.kvm/asl-vmsa.cfg

@@ -17,3 +17,5 @@ nonames A006,F006
 nonames A024,A025
 # CAS fail - revisit semantic
 nonames A029,A030
+# Pending bug, some executions that should be rejected by model persist
+nonames A031