Skip to content

Commit ee8eecc

Browse files
ShaleXIONGShaleXIONG
committed
[gen] Add litmus tests syntax check in CI.
Add a new test for litmus tests syntax check via `diyone7-check.t`. This test using `diyone7` as the entry point. Yet it will also cover tests generated by `diycross7` and `diy7` since those tools share the same litmus test generator.
1 parent 578a194 commit ee8eecc

3 files changed

Lines changed: 260 additions & 0 deletions

File tree

‎Makefile‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -694,10 +694,16 @@ test.vmsa+ifetch:
694694
@ echo "herd7 AArch64 VMSA+ifetch instructions tests: OK"
695695

696696
### Diy tests, includes
697+
### - A `diyone7` generated syntax check
697698
### - A `diy7` with `cycleonly` instance checks the cycle generations
698699
### - Several `diycross7` + `herd7` instances, check if the generated litmus tests
699700
### are equivalent based on `herd7` result.
700701
diy-test:: | build
702+
diy-test:: diyone-basic-test
703+
diyone-basic-test:
704+
@ echo
705+
dune test gen/tests
706+
@ echo "diyone7 basic test: OK"
701707
diy-test:: diy-baseline-cycleonly
702708
diy-baseline-cycleonly::
703709
@ echo

‎gen/tests/diyone7-check.t‎

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

‎gen/tests/dune‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
(cram
2+
(package herdtools7)
3+
(deps %{bin:diyone7}))

0 commit comments

Comments
 (0)