…
ARM MP+dmb+fri-rfi-ctrlisb+BIS+obs
"DMBdWW Rfe Fri Rfi DpCtrlIsbdR Fre + Some write + observation"
Prefetch=1:x=F,1:y=W,2:y=F,2:x=T
Com=Rf Fr
Orig=DMBdWW Rfe Fri Rfi DpCtrlIsbdR Fre
{
%y0=y;
%x1=x; %y1=y;
%y2=y; %x2=x;
%y3=y;
}
P0 | P1 | P2 | P3 ;
LDR R0,[%y0] | MOV R0,#1 | LDR R0,[%y2] | MOV R0,#3 ;
DMB | STR R0,[%x1] | MOV R1,#2 | STR R0,[%y3] ;
LDR R1,[%y0] | DMB | STR R1,[%y2] | ;
DMB | MOV R1,#1 | LDR R2,[%y2] | ;
LDR R2,[%y0] | STR R1,[%y1] | CMP R2,R2 | ;
| | BNE LC00 | ;
| | LC00: | ;
| | ISB | ;
| | LDR R3,[%x2] | ;
exists (0:R0=0 /\ 0:R1=0 /\ 0:R2=0 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=0 /\ 0:R1=0 /\ 0:R2=1 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=0 /\ 0:R1=0 /\ 0:R2=2 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=0 /\ 0:R1=0 /\ 0:R2=3 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=0 /\ 0:R1=1 /\ 0:R2=1 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=0 /\ 0:R1=1 /\ 0:R2=2 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=0 /\ 0:R1=1 /\ 0:R2=3 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=0 /\ 0:R1=2 /\ 0:R2=1 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=0 /\ 0:R1=2 /\ 0:R2=2 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=0 /\ 0:R1=2 /\ 0:R2=3 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=0 /\ 0:R1=3 /\ 0:R2=3 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=1 /\ 0:R1=1 /\ 0:R2=1 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=1 /\ 0:R1=1 /\ 0:R2=2 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=1 /\ 0:R1=1 /\ 0:R2=3 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=1 /\ 0:R1=2 /\ 0:R2=2 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=1 /\ 0:R1=2 /\ 0:R2=3 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=1 /\ 0:R1=3 /\ 0:R2=3 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=2 /\ 0:R1=1 /\ 0:R2=1 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=2 /\ 0:R1=1 /\ 0:R2=3 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=2 /\ 0:R1=2 /\ 0:R2=1 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=2 /\ 0:R1=2 /\ 0:R2=2 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=2 /\ 0:R1=2 /\ 0:R2=3 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=2 /\ 0:R1=3 /\ 0:R2=3 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3) \/ (0:R0=3 /\ 0:R1=3 /\ 0:R2=3 /\ 2:R0=0 /\ 2:R2=3 /\ 2:R3=0 /\ [y]=3)