Test STRx+SWPptex+db2

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