Skip to content

Commit 6be31f3

Browse files
ShaleXIONGShaleXIONG
committed
[gen] Add CI for diyone7 for invalid and valid annotations.
1 parent 2007388 commit 6be31f3

File tree

1 file changed

+54
-224
lines changed

1 file changed

+54
-224
lines changed

‎gen/tests/diyone7-check.t‎

Lines changed: 54 additions & 224 deletions
Original file line numberDiff line numberDiff line change
@@ -1,234 +1,64 @@
1-
vmsa-neg-exists
2-
$ diyone7 -arch AArch64 -variant kvm Amo.Cas TLBI-sync.ISHdWW PteV1 PteAF0 PteOA Rfe Pte PodRW PteHD Rfe -neg true -info "User-define=User-define"
3-
AArch64 LB+popteptehd+amo.cas-tlbi-sync.ishppteoa.v1.af0
4-
Variant=vmsa
1+
valid-cycle-with-p-annotation
2+
$ diyone7 -arch AArch64 PodWR P Fre PodWR Fre
3+
AArch64 SB
4+
"PodWR Fre PodWR Fre"
55
Generator=diyone7 (version 7.58+1)
6-
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
7-
Com=Rf Rf
8-
Orig=Amo.Cas TLBI-sync.ISHdWWPPteOA.V1.AF0 RfePteOA.V1.AF0Pte PodRWPtePteHD RfePteHDP
9-
TTHM=HD
10-
User-define=User-define
11-
"Amo.Cas TLBI-sync.ISHdWWPPteOA.V1.AF0 RfePteOA.V1.AF0Pte PodRWPtePteHD RfePteHDP"
12-
{
13-
[x]=1;
14-
[PTE(x)]=(oa:PA(x), db:0, dbm:1);
15-
[y]=5;
16-
[PTE(y)]=(oa:PA(y), valid:0);
17-
0:X0=x; 0:X3=PTE(y); 0:X4=(oa:PA(x), af:0);
18-
1:X0=x; pteval_t 1:X1=0; 1:X3=PTE(y);
19-
}
20-
P0 | P1 ;
21-
MOV W1,#2 | LDR X1,[X3] ;
22-
MOV W2,#3 | MOV W2,#2 ;
23-
L01: CAS W1,W2,[X0] | L00: STR W2,[X0] ;
24-
DSB ISH | ;
25-
LSR X5,X0,#12 | ;
26-
TLBI VAAE1IS,X5 | ;
27-
DSB ISH | ;
28-
STR X4,[X3] | ;
29-
30-
~exists ([x]=3 /\ 0:X1=2 /\ 1:X1=(oa:PA(x), af:0) /\ not (fault(P0:L01,x)) /\ not (fault(P1:L00,x)))
31-
vmsa-forall
32-
$ diyone7 -arch AArch64 -variant kvm Amo.Cas TLBI-sync.ISHdWW PteV1 PteAF0 PteOA Rfe Pte PodRW PteHD Rfe -info "User-define=User-define" -cond observe
33-
AArch64 LB+popteptehd+amo.cas-tlbi-sync.ishppteoa.v1.af0
34-
Variant=vmsa
35-
Generator=diyone7 (version 7.58+1)
36-
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
37-
Com=Rf Rf
38-
Orig=Amo.Cas TLBI-sync.ISHdWWPPteOA.V1.AF0 RfePteOA.V1.AF0Pte PodRWPtePteHD RfePteHDP
39-
TTHM=HD
40-
User-define=User-define
41-
"Amo.Cas TLBI-sync.ISHdWWPPteOA.V1.AF0 RfePteOA.V1.AF0Pte PodRWPtePteHD RfePteHDP"
42-
{
43-
[x]=1;
44-
[PTE(x)]=(oa:PA(x), db:0, dbm:1);
45-
[y]=5;
46-
[PTE(y)]=(oa:PA(y), valid:0);
47-
0:X0=x; 0:X3=PTE(y); 0:X4=(oa:PA(x), af:0);
48-
1:X0=x; pteval_t 1:X1=0; 1:X3=PTE(y);
49-
}
50-
P0 | P1 ;
51-
MOV W1,#2 | LDR X1,[X3] ;
52-
MOV W2,#3 | MOV W2,#2 ;
53-
L01: CAS W1,W2,[X0] | L00: STR W2,[X0] ;
54-
DSB ISH | ;
55-
LSR X5,X0,#12 | ;
56-
TLBI VAAE1IS,X5 | ;
57-
DSB ISH | ;
58-
STR X4,[X3] | ;
59-
60-
locations [x; 0:X1; 1:X1; fault(P0:L01,x); fault(P1:L00,x);]
61-
forall (true)
62-
vmsa-location
63-
$ diyone7 -arch AArch64 -variant kvm Amo.Cas TLBI-sync.ISHdWW PteV1 PteAF0 PteOA Rfe Pte PodRW PteHD Rfe -info "User-define=User-define" -cond unicond
64-
AArch64 LB+popteptehd+amo.cas-tlbi-sync.ishppteoa.v1.af0
65-
Variant=vmsa
66-
Generator=diyone7 (version 7.58+1)
67-
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
68-
Com=Rf Rf
69-
Orig=Amo.Cas TLBI-sync.ISHdWWPPteOA.V1.AF0 RfePteOA.V1.AF0Pte PodRWPtePteHD RfePteHDP
70-
TTHM=HD
71-
User-define=User-define
72-
"Amo.Cas TLBI-sync.ISHdWWPPteOA.V1.AF0 RfePteOA.V1.AF0Pte PodRWPtePteHD RfePteHDP"
73-
{
74-
[x]=1;
75-
[PTE(x)]=(oa:PA(x), db:0, dbm:1);
76-
[y]=5;
77-
[PTE(y)]=(oa:PA(y), valid:0);
78-
0:X0=x; 0:X3=PTE(y); 0:X4=(oa:PA(x), af:0);
79-
1:X0=x; pteval_t 1:X1=0; 1:X3=PTE(y);
80-
}
81-
P0 | P1 ;
82-
MOV W1,#2 | LDR X1,[X3] ;
83-
MOV W2,#3 | MOV W2,#2 ;
84-
L01: CAS W1,W2,[X0] | L00: STR W2,[X0] ;
85-
DSB ISH | ;
86-
LSR X5,X0,#12 | ;
87-
TLBI VAAE1IS,X5 | ;
88-
DSB ISH | ;
89-
STR X4,[X3] | ;
90-
91-
forall (not (fault(P0:L01,x)) /\ not (fault(P1:L00,x)) /\ ([y]=(oa:PA(x), af:0) /\ (0:X1=2 /\ ([x]=3 /\ (1:X1=(oa:PA(x), af:0) \/ 1:X1=0)) \/ 0:X1=0 /\ (1:X1=(oa:PA(x), af:0) /\ ([x]=3 \/ [x]=2) \/ 1:X1=0 /\ ([x]=3 \/ [x]=2)))))
92-
memtag
93-
$ diyone7 -arch AArch64 -variant memtag DpDatadW T PosWW T Rfe PodRW Rfe T -info "Variant=memtag"
94-
AArch64 LB+po+dataWtt-postt
95-
Variant=memtag memtag
96-
Generator=diyone7 (version 7.58+1)
97-
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
98-
Com=Rf Rf
99-
Orig=DpDatadWTT PosWWTT RfeTP PodRW RfePT
100-
"DpDatadWTT PosWWTT RfeTP PodRW RfePT"
6+
Prefetch=0:x=F,0:y=T,1:y=F,1:x=T
7+
Com=Fr Fr
8+
Orig=PodWR Fre PodWR Fre
1019
{
102-
0:X1=x:green; 0:X3=y:red; 0:X5=y:green; 0:X6=y:blue;
103-
1:X1=x:green; 1:X6=y:blue;
10+
0:X1=x; 0:X2=y;
11+
1:X2=y; 1:X1=x;
10412
}
105-
P0 | P1 ;
106-
MOV X0,X1 | L00: LDR W0,[X6] ;
107-
LDG X0,[X1] | MOV W2,#1 ;
108-
EOR X2,X0,X0 | STR W2,[X1] ;
109-
ADD X4,X3,W2,SXTW | ;
110-
STG X4,[X5] | ;
111-
STG X6,[X3] | ;
112-
113-
exists ([tag(y)]=:blue /\ 0:X0=x:green /\ 1:X0=0 /\ not (fault(P1:L00,y)))
114-
ifetch
115-
$ diyone7 -arch AArch64 -variant ifetch CacheSyncStrongIsbdWRPI FreIP PodWR Fre
116-
AArch64 SB+cachesyncstrongisbpi+po
117-
Variant=ifetch
13+
P0 | P1 ;
14+
MOV W0,#1 | MOV W0,#1 ;
15+
STR W0,[X1] | STR W0,[X2] ;
16+
LDR W3,[X2] | LDR W3,[X1] ;
17+
exists (0:X3=0 /\ 1:X3=0)
18+
valid-cycle-with-duplicate-annotations
19+
$ diyone7 -arch AArch64 PodWR A A Fre PodWR Fre
20+
AArch64 SB+po+popa
21+
"PodWRPA FreAP PodWR Fre"
11822
Generator=diyone7 (version 7.58+1)
23+
Prefetch=0:x=F,0:y=T,1:y=F,1:x=T
11924
Com=Fr Fr
120-
Orig=CacheSyncStrongIsbdWRPI FreIP PodWR Fre
121-
"CacheSyncStrongIsbdWRPI FreIP PodWR Fre"
25+
Orig=PodWRPA FreAP PodWR Fre
12226
{
123-
0:X1=x; 0:X3=P0:Lself00;
124-
1:X0=instr:"NOP"; 1:X1=x; 1:X3=P0:Lself00;
27+
0:X1=x; 0:X2=y;
28+
1:X2=y; 1:X1=x;
12529
}
126-
P0 | P1 ;
127-
MOV W0,#1 | STR W0,[X3] ;
128-
STR W0,[X1] | LDR W2,[X1] ;
129-
DC CIVAC,X3 | ;
130-
DSB ISH | ;
131-
IC IVAU,X3 | ;
132-
DSB ISH | ;
133-
ISB | ;
134-
Lself00: B .+12 | ;
135-
MOV W2,#2 | ;
136-
B .+8 | ;
137-
MOV W2,#1 | ;
138-
139-
exists (0:X2=1 /\ 1:X2=0)
140-
base-int64-and-array
141-
$ diyone7 -arch AArch64 -type int64_t X PodWW Coe PodWR Pa Fre
142-
AArch64 R+poxp+poppa
30+
P0 | P1 ;
31+
MOV W0,#1 | MOV W0,#1 ;
32+
STR W0,[X1] | STR W0,[X2] ;
33+
LDAR W3,[X2] | LDR W3,[X1] ;
34+
exists (0:X3=0 /\ 1:X3=0)
35+
$ diyone7 -arch AArch64 PodWR A A A Fre PodWR Fre
36+
AArch64 SB+po+popa
37+
"PodWRPA FreAP PodWR Fre"
14338
Generator=diyone7 (version 7.58+1)
144-
Prefetch=0:x=F,0:y=W,1:y=F,1:x=T
145-
Com=Co Fr
146-
Orig=PodWWXP Coe PodWRPPa FrePaX
147-
"PodWWXP Coe PodWRPPa FrePaX"
39+
Prefetch=0:x=F,0:y=T,1:y=F,1:x=T
40+
Com=Fr Fr
41+
Orig=PodWRPA FreAP PodWR Fre
14842
{
149-
int64_t x[2]={0,0};
150-
int64_t y=0;
151-
0:X0=x; int64_t 0:X2=0; 0:X5=y;
152-
1:X0=x; int64_t 1:X2=0; 1:X5=y;
153-
}
154-
P0 | P1 ;
155-
MOV X1,#1 | MOV X1,#2 ;
156-
Loop00: | STR X1,[X5] ;
157-
LDXR X2,[X0] | LDP X2,X3,[X0] ;
158-
STXR W3,X1,[X0] | ADD X2,X2,X3 ;
159-
CBNZ X3,Loop00 | ;
160-
MOV X4,#1 | ;
161-
STR X4,[X5] | ;
162-
163-
exists (x={1,0} /\ [y]=2 /\ 0:X2=0 /\ 1:X2=0)
164-
C-exists
165-
$ diyone7 -arch C PodWW Coe PodWR Fre
166-
Warning: optimised conditions are not supported by C arch
167-
C R
168-
"PodWW Coe PodWR Fre"
169-
Generator=diyone7 (version 7.58+1)
170-
Prefetch=0:x=F,0:y=W,1:y=F,1:x=T
171-
Com=Co Fr
172-
Orig=PodWW Coe PodWR Fre
173-
174-
{}
175-
176-
P0 (volatile int* y,volatile int* x) {
177-
*x = 1;
178-
*y = 1;
179-
}
180-
181-
P1 (volatile int* y,volatile int* x) {
182-
*y = 2;
183-
int r0 = *x;
184-
}
185-
186-
exists ([y]=2 /\ 1:r0=0)
187-
C-neg-exists
188-
$ diyone7 -arch C FencedWW Rfe DpAddrdW Coe
189-
Warning: optimised conditions are not supported by C arch
190-
C S+fencesc+addr
191-
"FenceScdWW Rfe DpAddrdW Coe"
192-
Generator=diyone7 (version 7.58+1)
193-
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
194-
Com=Rf Co
195-
Orig=FenceScdWW Rfe DpAddrdW Coe
196-
197-
{}
198-
199-
P0 (volatile int* y,volatile int* x) {
200-
*x = 2;
201-
atomic_thread_fence(memory_order_seq_cst);
202-
*y = 1;
203-
}
204-
205-
P1 (volatile int* y,volatile int* x) {
206-
int r0 = *y;
207-
*(x + (r0 & 128)) = 1;
208-
}
209-
210-
exists ([x]=2 /\ 1:r0=1)
211-
C-forall
212-
$ diyone7 -arch C FencedWW Sc Rfe Acq PodRW Coe -cond unicond
213-
Warning: optimised conditions are not supported by C arch
214-
C S+fencescnasc+poacqna
215-
"FenceScdWWNaSc RfeScAcq PodRWAcqNa Coe"
216-
Generator=diyone7 (version 7.58+1)
217-
Prefetch=0:x=F,0:y=W,1:y=F,1:x=W
218-
Com=Rf Co
219-
Orig=FenceScdWWNaSc RfeScAcq PodRWAcqNa Coe
220-
221-
{}
222-
223-
P0 (atomic_int* y,volatile int* x) {
224-
*x = 2;
225-
atomic_thread_fence(memory_order_seq_cst);
226-
atomic_store_explicit(y,1,memory_order_seq_cst);
227-
}
228-
229-
P1 (atomic_int* y,volatile int* x) {
230-
int r0 = atomic_load_explicit(y,memory_order_acquire);
231-
*x = 1;
43+
0:X1=x; 0:X2=y;
44+
1:X2=y; 1:X1=x;
23245
}
233-
234-
forall (true /\ ([y]=1 /\ ([x]=2 /\ (1:r0=1 \/ 1:r0=0) \/ [x]=1 /\ (1:r0=1 \/ 1:r0=0))))
46+
P0 | P1 ;
47+
MOV W0,#1 | MOV W0,#1 ;
48+
STR W0,[X1] | STR W0,[X2] ;
49+
LDAR W3,[X2] | LDR W3,[X1] ;
50+
exists (0:X3=0 /\ 1:X3=0)
51+
invalid-cycle-with-incorrect-annotations
52+
$ diyone7 -arch AArch64 PodWR A L Fre PodWR Fre
53+
diyone7: Fatal error: Annotations mismatch between A L.
54+
[2]
55+
$ diyone7 -arch AArch64 PodWR L A Fre PodWR Fre
56+
diyone7: Fatal error: Annotations mismatch between L A.
57+
[2]
58+
$ diyone7 -arch AArch64 PodWR L Fre PodWR Fre
59+
diyone7: Fatal error: Test SB+po+popl [PodWRPL FreLP PodWR Fre] failed:
60+
annotation mismatch on edge FreLP, annotation 'L' on R
61+
[2]
62+
$ diyone7 -arch AArch64 PodWR A L A Fre PodWR Fre
63+
diyone7: Fatal error: Invalid extra annotation L
64+
[2]

0 commit comments

Comments
 (0)