Test coRR-pte9-ob

AArch64 coRR-pte9-ob
{
0:X1=x; 1:X1=x; 2:X1=x;
1:X3=pte_x; 2:X3=pte_x; 3:X3=pte_x;
pte_x=(db:1);
3:X4=(oa:phy_y,db:1);
y=1;
1:X0=(oa:phy_x,valid:0,db:1);
 
1:X6=1; 2:X8=1;
1:X5=v; 2:X5=v;
2:X7=w; 3:X7=w;
}
P0             | P1             | P2             | P3             ;
L1:LDR W2,[X1] | STR X0,[X3]    | LDR W6,[X5]    | LDR W8,[X7]    ;
L0:LDR W4,[X1] | DMB ST         | DSB ISH        | DMB SY         ;
               | STR W6,[X5]    | LSR X9,X1,#12  | STR X4,[X3]    ;
               |                | TLBI VAAE1IS,X9|                ;
               |                | DSB ISH        |                ;
               |                | STR W8,[X7]    |                ;
exists (0:X2=1 /\ 0:X4=0 /\ 2:X6=0 /\ 3:X8=1 /\ ~fault(P0:L0,x)) \/ (0:X2=1 /\ 0:X4=0 /\ 2:X6=0 /\ 3:X8=1 /\ fault(P0:L0,x,MMU:Translation)) \/ (0:X2=1 /\ 0:X4=0 /\ 2:X6=1 /\ 3:X8=1 /\ fault(P0:L0,x,MMU:Translation))