Merge pull request herd#1614 from diaolo01/mte-async-bug

[herd] Bug fix: fault handler must not be entered when using MTE async

Author: relokin

herd/AArch64Sem.ml

@@ -1363,21 +1363,23 @@ module Make
 
       let lift_fault_memtag mfault mm dir ii =
         let lbl_v = get_instr_label ii in
-        if has_handler ii then
-          fun ma ->
-            M.bind_ctrldata ma (fun _ -> mfault >>| set_elr_el1 lbl_v ii) >>!
-            B.fault [AArch64Base.elr_el1, lbl_v]
-        else
-          let open Precision in
-          match C.mte_precision,dir with
-          | (Synchronous,_)|(Asymmetric,(Dir.R)) ->
-             fun ma ->  ma >>*= (fun _ -> mfault >>| set_elr_el1 lbl_v ii) >>!
-               B.fault [AArch64Base.elr_el1, lbl_v]
-          | (Asynchronous,_)|(Asymmetric,Dir.W) ->
-             fun ma ->
-             let set_tfsr = write_reg AArch64Base.tfsr V.one ii in
-             let ma = ma >>*== (fun a -> (set_tfsr >>| mfault) >>! a) in
-             mm ma >>! B.Next []
+        let open Precision in
+          match C.mte_precision, dir with
+          | (Synchronous, _)
+          | (Asymmetric, Dir.R) ->
+            let mexc _ =
+              mfault >>| set_elr_el1 lbl_v ii >>!
+              B.fault [AArch64Base.elr_el1, lbl_v] in
+            if has_handler ii then
+              fun ma -> M.bind_ctrldata ma mexc
+            else
+              fun ma -> ma >>*= mexc
+          | (Asynchronous,_)
+          | (Asymmetric,Dir.W) ->
+            fun ma ->
+              let set_tfsr = write_reg AArch64Base.tfsr V.one ii in
+              let ma = ma >>*== (fun a -> (set_tfsr >>| mfault) >>! a) in
+              mm ma >>! B.Next []
 
 (* KVM mode *)
 

herd/tests/instructions/AArch64.MTE/F001.litmus

@@ -0,0 +1,10 @@
+AArch64 F001
+(* test must not enter fault handler when mte_precision is async *)
+variant=mte,async
+{
+    [tag(x)]=:green;
+    0:X1=x:red;
+}
+P0           | P0.F           ;
+ STR W0,[X1] | MOV W2,#1    ;
+forall(0:X2=0)

herd/tests/instructions/AArch64.MTE/F001.litmus.expected

@@ -0,0 +1,10 @@
+Test F001 Required
+States 1
+0:X2=0;
+Ok
+Witnesses
+Positive: 1 Negative: 0
+Condition forall (0:X2=0)
+Observation F001 Always 1 0
+Hash=2d337b1db56e968a8b4aa52898d6683a
+

herd/tests/instructions/AArch64.MTE/F002.litmus

@@ -0,0 +1,10 @@
+AArch64 F002
+(* test must enter fault handler when mte_precision is default:sync *)
+variant=mte
+{
+    [tag(x)]=:green;
+    0:X1=x:red;
+}
+P0           | P0.F           ;
+ STR W0,[X1] | MOV W2,#1    ;
+forall(0:X2=1)

herd/tests/instructions/AArch64.MTE/F002.litmus.expected

@@ -0,0 +1,10 @@
+Test F002 Required
+States 1
+0:X2=1;
+Ok
+Witnesses
+Positive: 1 Negative: 0
+Condition forall (0:X2=1)
+Observation F002 Always 1 0
+Hash=2d337b1db56e968a8b4aa52898d6683a
+

herd/tests/instructions/AArch64.MTE/F003.litmus

@@ -0,0 +1,10 @@
+AArch64 F003
+Variant=mte,asym
+{
+ 0:X1=x:red;
+ 1:X1=x:red;
+}
+ P0          | P0.F         |  P1         | P1.F         ;
+ LDR W0,[X1] | MOV W2,#3    | MOV W0,#2   | MOV W2,#3    ;
+             |              | STR W0,[X1] |              ;
+forall(0:X2=3 /\ 1:X2=0)

herd/tests/instructions/AArch64.MTE/F003.litmus.expected

@@ -0,0 +1,10 @@
+Test F003 Required
+States 1
+0:X2=3; 1:X2=0;
+Ok
+Witnesses
+Positive: 1 Negative: 0
+Condition forall (0:X2=3 /\ 1:X2=0)
+Observation F003 Always 1 0
+Hash=c721899d1198ef9b8d0385d633e7bd6c
+