Test STRx+SWPptexForbid1

AArch64 STRx+SWPptexForbid1
TTHM=HA HD
{ 
pte_x=(valid:1,db:0,dbm:1,oa:phy_x); 
0:X2=x;
1:X1=(valid:0,oa:phy_x); 
1:X3=pte_x;
}
P0              |  P1             ; 
MOV W0,#1       | SWP X1, X4, [X3]; 
L0: STR W0,[X2] |                 ;
exists (1:X4=(oa:PA(x), dbm:1) /\ [PTE(x)]=(oa:PA(x), valid:0) /\ [x]=0 /\ fault(P0:L0,x,MMU:Translation))