[gen] Fix problems related to physical address change, annotation PteOA.

[ShaleXIONG]

This pull request (1) changes the behaviour of PteOA, which now always picks a fresh physical address now, and (2) ensure the memory access correctly to the underline physical address.

For example, diyone7 -arch AArch64 -variant kvm PteOA PodWR Fre PodWR Fre

AArch64 SB+po+popteoap
"PodWRPteOAP Fre PodWR FrePPteOA"
Generator=diyone7 (version 7.58+1)
Prefetch=0:x=F,0:y=T,1:y=F,1:x=T
Com=Fr Fr
Orig=PodWRPteOAP Fre PodWR FrePPteOA
{ int z=4;
0:X0=PTE(x); 0:X1=(oa:PA(z)); 0:X2=y;
1:X2=y; 1:X4=x;
}
 P0          | P1          ;
 STR X1,[X0] | MOV W3,#1   ;
 LDR W3,[X2] | STR W3,[X2] ;
             | LDR W5,[X4] ;
exists (0:X3=0 /\ 1:X5=0)

The first STR instruction in P0 writes a fresh location PA(z) to PTE(x) given the PteOA annotation. It was previously PA(y). Because the new strategy always picks a fresh location/variable, we no longer need to initialise existing variable in 1,5,9,... but now always initialise to 0. However the newly picked location z will be initialised to 4,8,.... To recall, this is for distinguishing read from the original variable, e.g. x, and new variable, e.g. z.

If multiple PteOA annotation apply to the same virtual location, it will always pick a fresh location for the OA. For example, diyone7 -arch AArch64 -variant kvm PteOA PosWW PteOA Coi -oneloc

AArch64 CoWW+pospteoapteoa-coipteoapteoa
"PosWWPteOAPteOA CoiPteOAPteOA"
Generator=diyone7 (version 7.58+1)
Com=Co
Orig=PosWWPteOAPteOA CoiPteOAPteOA
{ int y=4; int z=8;
0:X0=PTE(x); 0:X1=(oa:PA(z)); 0:X2=(oa:PA(y));
}
 P0          ;
 STR X1,[X0] ;
 STR X2,[X0] ;

Last, we fixed a long existing problem: the read after changing of PA. It now correctly checks the read value is from the new PA. For example, diyone7 -arch AArch64 -variant kvm PteOA PosWR Fre PteOA PosWR Fre -oneloc

AArch64 SB+pospteoaps
"PosWRPteOAP FrePPteOA PosWRPteOAP FrePPteOA"
Generator=diyone7 (version 7.58+1)
Com=Fr Fr
Orig=PosWRPteOAP FrePPteOA PosWRPteOAP FrePPteOA
{ int y=4; int z=8;
0:X0=PTE(x); 0:X1=(oa:PA(y)); 0:X2=x;
1:X0=PTE(x); 1:X3=(oa:PA(z)); 1:X2=x;
}
 P0          | P1          ;
 STR X1,[X0] | STR X3,[X0] ;
 LDR W3,[X2] | LDR W4,[X2] ;
exists (0:X3=4 /\ 1:X4=0)

Previously, it was 0:X3=1, which was incorrect.

[relokin]

I don't follow the logic of this code. Very few comments and where they exist they are stale.

This block would benefit from some comments and refactoring. As an example why the logic doesn't work take the produced by this:

$ diyone7 -metadata false -variant kvm -arch AArch64 PteOA TLBI-sync.ISHsWW PteOA TLBI-sync.ISHdWW Rfe DMB.LDdRR Fre

AArch64 MP+tlbi-sync.ishsWpteoapteoa-tlbi-sync.ishpteoap+dmb.ld
{ int z=5;
0:X0=PTE(x); 0:X1=(oa:PA(z)); 0:X2=(oa:PA(x)); 0:X4=y; 0:X5=x;
1:X4=y; 1:X5=x;
}
 P0              | P1          ;
 STR X1,[X0]     | LDR W3,[X4] ;
 DSB ISH         | DMB LD      ;
 LSR X6,X5,#12   | LDR W6,[X5] ;
 TLBI VAAE1IS,X6 |             ;
 DSB ISH         |             ;
 STR X2,[X0]     |             ;
 DSB ISH         |             ;
 LSR X6,X5,#12   |             ;
 TLBI VAAE1IS,X6 |             ;
 DSB ISH         |             ;
 MOV W3,#1       |             ;
 STR W3,[X4]     |             ;
exists ([PTE(x)]=(oa:PA(x)) /\ 1:X3=1 /\ 1:X6=0)

Why are we going from oa:PA(x) to oa:PA(z) back to oa:PA(x)?

Out of nowhere, the code introduces a constant 5 which is meant to be a good initial value for the fresh PA?

[ShaleXIONG]

I did the toggle behaviour on PteOA. However I checked the old behaviour which changes to the OA of a new location and never changes back. I will update to reflect this.

5 is a mistake, it should be 4, as the initial value is 0 now, and I preserve the old behaviour of gapping 4 so the read can reflect the value being read.

[ShaleXIONG]

I have updated the code, PteOA will always pick a new fresh location.

[relokin]

I think for n 26 this will return "x".

[ShaleXIONG]

ah yes, will fix with n<26

[relokin]

I am not sure I understand this comment can you please rephase this.

[ShaleXIONG]

I have updated. It is a function for PteOA, as it leads to different physical locations, so further read to the same virtual address should have a value check.