…
AArch64 NT-20-ctrl
TTHM=P1:HA
Variant=precise
{
int x=1; int y;
pte_x=(af:0,valid:0);
0:X2=y;
0:X6=pte_x;
0:X9=(oa:phy_x,af:0,valid:1);
0:X3=(oa:phy_y);
1:X2=y; 1:X4=x;
}
P0 | P1 ;
SWP X9,X7,[X6] | LDR W0,[X2] ;
LDR X5,[X6] | DMB LD ;
CMP X5,X3 |L0: ;
B.EQ Lover | LDR W1,[X4] ; (* Branch never taken *)
MOV W0,#1 | ;
STR W0,[X2] | ;
Lover: | ;
exists (0:X7=(oa:PA(x), valid:0, af:0) /\ 1:X0=1 /\ 1:X1=0 /\ fault(P1:L0,x,MMU:Translation))