Skip to content

Commit 2007388

Browse files
Shale XiongShaleXIONG
Shale Xiong
authored and
ShaleXIONG
committed
[gen] Add diyone7 syntax check in CI.
1 parent 2b15284 commit 2007388

File tree

3 files changed

+243
-0
lines changed

3 files changed

+243
-0
lines changed

‎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: 234 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,234 @@
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
5+
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"
101+
{
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;
104+
}
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
118+
Generator=diyone7 (version 7.58+1)
119+
Com=Fr Fr
120+
Orig=CacheSyncStrongIsbdWRPI FreIP PodWR Fre
121+
"CacheSyncStrongIsbdWRPI FreIP PodWR Fre"
122+
{
123+
0:X1=x; 0:X3=P0:Lself00;
124+
1:X0=instr:"NOP"; 1:X1=x; 1:X3=P0:Lself00;
125+
}
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
143+
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"
148+
{
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;
232+
}
233+
234+
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)