Test FJ

AArch64 FJ
{
0:X1=(oa:PA(x),valid:1);
0:X2=PTE(x);
[PTE(x)]=(valid:0);
0:X4=x; 0:X6=y;
1:X4=x; 1:X6=y;
}

  P0             |  P1                 ;
 STR X1,[X2]     | LDR  W1,[X6]        ;
 DSB ISH         | AND W5,W1,#2        ;
 LSR X8,X4,#12   | MOV W3,#1           ;
 TLBI VAAE1IS,X8 |L0:                  ;
 DSB ISH         | STR W3,[X4,W5,SXTW] ;  
 MOV W3,#1       |                     ;
 STR W3,[X6]     |                     ; 
exists (1:X1=1 /\ fault(P1:L0,x,MMU:Translation))