-
Notifications
You must be signed in to change notification settings - Fork 94
Description
This issue records a problem with tests generated by diyone7. Currently @hugookeeffe intends to look into the issue, so this note is just to increase visibility.
Suppose you execute the following prompt:
diyone7 -arch AArch64 "DMB.SYdWW Rfe Amo.StClr DMB.LDdWR Fre"
... and get the following test:
AArch64 A
"DMB.SYdWW Rfe Amo.StClr DMB.LDdWR Fre"
Generator=diyone7 (version 7.57+1)
Prefetch=0:x=F,0:y=W,1:y=F,1:x=T
Com=Rf Fr
Orig=DMB.SYdWW Rfe Amo.StClr DMB.LDdWR Fre
{
0:X1=x; 0:X3=y;
1:X0=y; 1:X2=x;
}
P0 | P1 ;
MOV W0,#1 | MOV W1,#2 ;
STR W0,[X1] | STCLR W1,[X0] ;
DMB SY | DMB LD ;
MOV W2,#1 | LDR W3,[X2] ;
STR W2,[X3] | ;
exists ([y]=1 /\ 1:X3=0)
This test is not fit for its purpose, because its postcondition does not focus on an execution where STR W2,[X3] is read-from by STCLR W1,[X0] . Indeed, if the STCLR unsets the second bit of x, whether it happens before or after the store does not affect the postcondition.
In contrast, this manual edit of the test would achieve the goal:
AArch64 A-modified
{
0:X1=x; 0:X3=y;
1:X0=y; 1:X2=x;
}
P0 | P1 ;
MOV W0,#1 | MOV W1,#2 ;
STR W0,[X1] | STCLR W1,[X0] ;
DMB SY | DMB LD ;
MOV W2,#3 | LDR W3,[X2] ;
STR W2,[X3] | ;
exists ([y]=1 /\ 1:X3=0)
A successful solution of the issue does not need to feature the exact values used above, but it should enforce the reads-from relationship in the test.
P.S. It would be extra helpful to double check that similar issues do not arise in STADD, STEOR, STSET, STCLR.