Several "unit" tests

Co-authored by: Luc Maranget
herd · Sep 9, 2023 · 1381c6f · 1381c6f
1 parent 328f7c8
commit 1381c6f
Show file tree

Hide file tree

Showing 6 changed files with 84 additions and 0 deletions.
diff --git a/herd/tests/instructions/AArch64/AK001.litmus b/herd/tests/instructions/AArch64/AK001.litmus
@@ -0,0 +1,16 @@
+AArch64 AK001 (* LB+rel+br-ctrl *)
+{
+ins_t *y;
+0:X2=x; 0:X4=y; 0:X3=P1:L0;
+1:X2=x; 1:X4=y;
+}
+P0           |P1           ;
+LDR W1,[X2]  | ADR X5,L1   ;
+STLR X3,[X4] | STR X5,[X4] ;
+             | LDR X3,[X4] ;
+             | BR X3       ;
+             |L0:          ;
+             | MOV W0,#1   ;
+             | STR W0,[X2] ;
+             |L1:          ;
+exists (0:X1=1 /\ 1:X0=1)
diff --git a/herd/tests/instructions/AArch64/AK001.litmus.expected b/herd/tests/instructions/AArch64/AK001.litmus.expected
@@ -0,0 +1,11 @@
+Test AK001 Allowed
+States 2
+0:X1=0; 1:X0=0;
+0:X1=0; 1:X0=1;
+No
+Witnesses
+Positive: 0 Negative: 3
+Condition exists (0:X1=1 /\ 1:X0=1)
+Observation AK001 Never 0 3
+Hash=7967e5120b4f97d2a96964ef4e3b026a
+
diff --git a/herd/tests/instructions/AArch64/AK002.litmus b/herd/tests/instructions/AArch64/AK002.litmus
@@ -0,0 +1,17 @@
+AArch64 AK002 (* MP+rel+br-ctrlisb-1 *)
+{
+ins_t *y;
+0:X2=x; 0:X4=y; 0:X3=P1:L0;
+1:X2=x; 1:X4=y;
+}
+P0           | P1          ;
+MOV W1,#1    | ADR X5,L1   ;
+STR W1,[X2]  | STR X5,[X4] ;
+STLR X3,[X4] | LDR X3,[X4] ;
+             | BR  X3      ;
+             |L0:          ; 
+             | ISB         ;
+             | MOV W0,#1   ;
+             | LDR W1,[X2] ;
+             |L1:          ;
+exists (1:X0=1 /\ 1:X1=0)
diff --git a/herd/tests/instructions/AArch64/AK002.litmus.expected b/herd/tests/instructions/AArch64/AK002.litmus.expected
@@ -0,0 +1,11 @@
+Test AK002 Allowed
+States 2
+1:X0=0; 1:X1=0;
+1:X0=1; 1:X1=1;
+No
+Witnesses
+Positive: 0 Negative: 3
+Condition exists (1:X0=1 /\ 1:X1=0)
+Observation AK002 Never 0 3
+Hash=c4340862f7579b543222fa925b3531ea
+
diff --git a/herd/tests/instructions/AArch64/AK003.litmus b/herd/tests/instructions/AArch64/AK003.litmus
@@ -0,0 +1,17 @@
+AArch64 AK003 (* MP+rel+br-ctrlisb-2 *)
+{
+ins_t *y;
+0:X2=x; 0:X4=y; 0:X3=P1:L0;
+1:X2=x; 1:X4=y;
+}
+P0           | P1          ;
+MOV W1,#1    | ADR X5,L1   ;
+STR W1,[X2]  | STR X5,[X4] ;
+STLR X3,[X4] | LDR X3,[X4] ;
+             | BR  X3      ;
+             |L0:          ;
+             | ISB         ;
+             | MOV W0,#1   ;
+             |L1:          ;
+             | LDR W1,[X2] ;
+exists (1:X0=1 /\ 1:X1=0)
diff --git a/herd/tests/instructions/AArch64/AK003.litmus.expected b/herd/tests/instructions/AArch64/AK003.litmus.expected
@@ -0,0 +1,12 @@
+Test AK003 Allowed
+States 3
+1:X0=0; 1:X1=0;
+1:X0=0; 1:X1=1;
+1:X0=1; 1:X1=1;
+No
+Witnesses
+Positive: 0 Negative: 5
+Condition exists (1:X0=1 /\ 1:X1=0)
+Observation AK003 Never 0 5
+Hash=f1ea3d37edb778d976084e71b2bbafc9
+