Test STRx-LDRx-ptex+db

AArch64 STRx-LDRx-ptex+db
TTHM=HD
{
int x; int y; 
pte_x=(oa:phy_x,db:0,dbm:1);
pte_y=(oa:phy_x,db:1,dbm:1);
0:X2=x; 1:X2=y;
1:X4=pte_x;
}
P0          | P1          ;
MOV W1,#1   | LDR W1,[X2] ;
STR W1,[X2] | DSB ISH     ;
            | LDR X3,[X4] ;
exists (1:X1=1 /\ 1:X3=(oa:PA(x), dbm:1, db:0) /\ [x]=1)