Merge pull request #827 from herd/fix-stop

[all, aarch64] Parse ST<OP> on X registers Fix of an oversight in PR #803.
herd · Apr 10, 2024 · fa63f78 · fa63f78
2 parents a72b414 + 0cb78cf
commit fa63f78
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 0 deletions.
diff --git a/herd/tests/instructions/AArch64.ASL/STCLR00.litmus b/herd/tests/instructions/AArch64.ASL/STCLR00.litmus
@@ -0,0 +1,10 @@
+AArch64 STCLR00
+{
+uint64_t x=15;
+uint64_t 0:X0=5;
+0:X1=x;
+}
+   P0          ;
+ STCLR X0,[X1] ;
+
+forall [x]=10
diff --git a/herd/tests/instructions/AArch64.ASL/STCLR00.litmus.expected b/herd/tests/instructions/AArch64.ASL/STCLR00.litmus.expected
@@ -0,0 +1,10 @@
+Test STCLR00 Required
+States 1
+[x]=10;
+Ok
+Witnesses
+Positive: 1 Negative: 0
+Condition forall ([x]=10)
+Observation STCLR00 Always 1 0
+Hash=6dce510cf1ec8087064858128b894317
+
diff --git a/lib/AArch64Parser.mly b/lib/AArch64Parser.mly
@@ -849,6 +849,8 @@ instr:
    { let v,op,rmw = $1 in I_LDOPBH (op,v,rmw,$2,$4,$7) }
 | STOP wreg COMMA LBRK cxreg zeroopt RBRK
    { let op,w = $1 in I_STOP (op,V32,w,$2,$5) }
+| STOP xreg COMMA LBRK cxreg zeroopt RBRK
+   { let op,w = $1 in I_STOP (op,V64,w,$2,$5) }
 | STOPBH wreg COMMA LBRK cxreg zeroopt RBRK
    { let v,op,w = $1 in I_STOPBH (op,v,w,$2,$5) }
 /* Operations */