Test LDR-BY2PTE-0

AArch64 LDR-BY2PTE-0
TTHM=HA
Variant=precise
{
  int x = 1 ;
  pte_x0 = (oa:phy_x, af:0) ;
  pte_x1 = (oa:phy_x, af:1) ;
  0:X2=x0 ;
  1:X2=x1 ;
  1:X4=pte_x0 ;
  1:X6= (oa:phy_x, valid:0) ;
}
  P0          |  P1         ;
 LDR W0,[X2]  | MOV W0,#2   ;
              | STR W0,[X2] ;
              | DMB SY      ;
              | SWP X6,X8,[X4] ;
exists 0:X0=1 /\ 1:X8=(oa:phy_x, af:0) /\ ~Fault(P0,x0)