Test STRx+LDR-STRptex+db

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