[herd][AArch64] Fix GCS fault propagation

herd/AArch64Sem.ml

@@ -1564,7 +1564,7 @@ module Make
  * +iico_data dependency between the event `ma` and `mop` or `mfault`, and an
  * iico_data dependency between `mv` and `mop` in case of a success.
  *)
-      let lift_pac_virt mop ma dir an ii domain =
+      let lift_pac_virt mop ma dir an ii branch domain =
         (* Addresses of memory operations must be canonical for the construction
          * of the rf, co and fr maps... *)
         let mfault ma a ft =
@@ -1574,7 +1574,7 @@ module Make
             None ii
           >>! B.fault [AArch64Base.elr_el1, lbl_v]
         in
-        let mok ma = mop ma >>= M.ignore >>= B.next1T in
+        let mok ma = mop ma |> branch in
         check_pac_va_range mok ma mfault ii domain
 
       let lift_memtag_phy dir mop ma an ii mphy =
@@ -1719,9 +1719,9 @@ Arguments:
             M.short (is_this_reg rA) (E.is_pred_txt (Some "color")) m
           else if checked then
             let mop ma = lift_memtag_virt mop ma dir an ii branch in
-            if pac then lift_pac_virt mop ma dir an ii domain else mop ma
+            if pac then lift_pac_virt mop ma dir an ii Fun.id domain else mop ma
           else if pac then
-            lift_pac_virt (mop Access.VIR) ma dir an ii domain
+            lift_pac_virt (mop Access.VIR) ma dir an ii branch domain
           else
             mop Access.VIR ma |> branch
 
@@ -2264,13 +2264,13 @@ Arguments:
           (rmw_to_read rmw)
           ii
 
-      let do_cas_fail do_wb sz an rn ma mv mop tagcheck ii =
+      let do_cas_fail_with lift do_wb sz an rn ma mv mop tagcheck ii =
         let action checked ma =
           let do_action updatedb checked ma =
               (* Dir.W would force check for dbm bit:                  *)
               (* - if set then either update or not db bit per R_TXGHB *)
               (* - if unset raise Permission fault                     *)
-              lift_memop ~tag:"FAIL" rn Dir.W updatedb checked mop (to_perms "rw" sz) ma mv an ii
+              lift ~tag:"FAIL" rn Dir.W updatedb checked mop (to_perms "rw" sz) ma mv an ii
           in
           if do_wb then
             do_action true checked ma
@@ -2304,14 +2304,13 @@ Arguments:
         else
           action memtag ma
 
-      let do_cas_fail_with_wb = do_cas_fail true
-      let do_cas_fail_no_wb = do_cas_fail false
-
-      let do_cas sz an rn ma mv mop_success mop_fail_with_wb mop_fail_no_wb tagcheck ii =
+      let do_cas_with lift sz an rn ma mv mop_success mop_fail_with_wb mop_fail_no_wb tagcheck ii =
+        let do_cas_fail_with_wb = do_cas_fail_with lift true in
+        let do_cas_fail_no_wb = do_cas_fail_with lift false in
         M.altT (
           (* CAS succeeds and generates an Explicit Write Effect *)
           (* there must be an update to the dirty bit of the TTD *)
-          lift_memop ~tag:"CAS" rn Dir.W true tagcheck mop_success (to_perms "rw" sz) ma mv an ii
+          lift ~tag:"CAS" rn Dir.W true tagcheck mop_success (to_perms "rw" sz) ma mv an ii
         )( (* CAS fails *)
           M.altT (
             (* CAS generates an Explicit Write Effect              *)
@@ -2322,6 +2321,8 @@ Arguments:
           )
         )
 
+      let do_cas = do_cas_with (fun ~tag -> lift_memop ~tag)
+
       let cas sz rmw rs rt rn ii =
         let an = rmw_to_read rmw in
         let read_rs = read_reg_data_sz sz rs ii
@@ -3818,7 +3819,7 @@ Arguments:
             in
             (* Write to Rd depends on read from Shadow Stack *)
             M.short (E.is_mem_load) (is_this_reg rd) m in
-          lift_memop rA Dir.R false false
+          do_lift_memop rA Dir.R false false
           (fun ac ma _mv ->
             if Access.is_physical ac then
               M.bind_ctrldata ma (mop ac)
@@ -3828,43 +3829,15 @@ Arguments:
           (M.unitT a_virt)
           mzero
           an
-          ii in
+          ii
+          Fun.id
+          DISide.Data
+        in
         (* Value writen to GCSPR depends on previous read *)
         let read e = (is_this_reg rA e) && (E.is_reg_load e ii.A.proc)
         and write e = (is_this_reg rA e) && (E.is_reg_store e ii.A.proc) in
         M.short read write m
 
-      (*
-       * Basically copy of lift_memop which allows mop to drive control flow
-       * (handy for BL{R}/RET instructions with GCS enabled)
-       *)
-      let lift_shadow_stack dir updatedb mop ma mv an ii =
-        let domain = DISide.Data in
-        let mop = apply_mv mop mv in
-        if kvm then
-          let mphy ma a_virt =
-            let ma = get_oa a_virt ma in
-              mop Access.PHY ma
-          in
-          (* lift_kvm dir updatedb mop ma an ii mphy in *)
-          let mfault ma a ft = emit_fault (Some a) ma dir an ft None ii in
-          let maccess a ma =
-            check_ptw ii.AArch64.proc dir updatedb false a ma an ii
-            (mop (Access.PTE domain) ma)
-            mphy
-            mfault
-            domain in
-          M.delay_kont "shadow_stack"
-          ma
-          (fun a ma ->
-            match Act.access_of_location_std (A.Location_global a) with
-            | Access.VIR|Access.PTE _ when not (A.V.is_instrloc a) ->
-              maccess a ma
-            | ac ->
-              mop ac ma)
-        else
-          mop Access.VIR ma
-
       let blop v_ret write_linkreg branch bop ii =
         let open AArch64Base in
         let an = Annot.N
@@ -3875,7 +3848,7 @@ Arguments:
             GCSSem.write ac an a v ii >>|
             write_reg rA a_virt ii >>|
             write_linkreg >>= M.ignore in
-          lift_shadow_stack Dir.W true
+          do_lift_memop rA Dir.W true false
           (fun ac ma mv ->
             let m =
               if is_branching && Access.is_physical ac then
@@ -3887,18 +3860,21 @@ Arguments:
             let read e = (is_this_reg rA e) && (E.is_reg_load e ii.A.proc)
             and write e = (is_this_reg rA e) && (E.is_reg_store e ii.A.proc) in
             M.short read write m)
+          (to_perms "w" quad)
           (M.unitT a_virt)
           (M.unitT v_ret)
           an
           ii
+          Fun.id
+          DISide.Data
 
       let retop test i r ii =
         let open AArch64Base in
         let an = Annot.N
         and rA = SysReg GCSPR_EL1
         and off = MachSize.nbytes quad in
         read_reg_addr rA ii >>= fun a_virt ->
-          lift_shadow_stack Dir.R false
+          do_lift_memop rA Dir.R false false
           (fun ac ma mv ->
             let m =
               mv >>|
@@ -3928,10 +3904,13 @@ Arguments:
               let m = M.short read write m in
               (* Branch depends on destination register (or LR) *)
               M.short (is_this_reg r) (E.is_bcc) m)
+          (to_perms "r" quad)
           (M.unitT a_virt)
           (read_reg_ord r ii)
           an
           ii
+          Fun.id
+          DISide.Data
 
       let gcsss1 r ii =
         let open AArch64Base in
@@ -3951,7 +3930,7 @@ Arguments:
                 branch >>*=
                 fun () -> write_reg rA incoming ii >>= fun () -> B.nextSetT rA incoming in
               M.op Op.Eq data v >>= fun cond ->  (* if data == cmpoperand then                             *)
-              M.assertT cond mok >>= M.ignore   (*     SetCurrentGCSPointer(incoming_pointer[63:3]:'000'); *)
+              M.assertT cond mok                (*     SetCurrentGCSPointer(incoming_pointer[63:3]:'000'); *)
           in
           let fault data =
              GCSSem.make_valid incoming >>= fun v ->
@@ -3960,7 +3939,7 @@ Arguments:
               (fun cond action ->
                 let open FaultType.AArch64 in (*     GCSDataCheckException(GCSInstType_SS1);  *)
                 let mno = GCSSem.mk_fault action (GCSCheck SS1) ii in
-                M.assertT cond mno >>= M.ignore)
+                M.assertT cond mno)
           in
           let branch a =
             let cond1 = Some (Printf.sprintf "Valid([%s])" (V.pp_v a)) in
@@ -4008,7 +3987,9 @@ Arguments:
             )
           in
           let mv = read_reg_data rA ii in
-          do_cas quad Annot.N r ma mv mop_success mop_fail_with_wb mop_fail_no_wb false ii)
+          let lift_memop ~tag rA dir updatedb checked mop perms ma mv an ii =
+            do_lift_memop ~tag rA dir updatedb checked mop perms ma mv an ii Fun.id DISide.Data in
+          do_cas_with lift_memop quad Annot.N r ma mv mop_success mop_fail_with_wb mop_fail_no_wb false ii)
 
     let gcsss2 r ii =
       let open AArch64Base in
@@ -4058,7 +4039,7 @@ Arguments:
         (* Register write and write to other stack depend on load from Shadow Stack *)
         let store e = (E.is_mem_store e) || (is_this_reg r e) in
         M.short (E.is_mem_load) store m in
-      lift_memop rA Dir.R false false
+      do_lift_memop rA Dir.R false false
       (fun ac ma _mv ->
         if Access.is_physical ac then
           M.bind_ctrldata ma (mop ac)
@@ -4068,7 +4049,9 @@ Arguments:
       ma
       mzero
       an
-      ii) in
+      ii
+      Fun.id
+      DISide.Data) in
       (* Value writen to GCSPR depends on previous read *)
       let read e = (is_this_reg rA e) && (E.is_reg_load e ii.A.proc)
       and write e = (is_this_reg rA e) && (E.is_reg_store e ii.A.proc) in

herd/eventsMonad.ml

@@ -577,7 +577,7 @@ Monad type:
     let do_aarch64_cas_ok
         (is_physical:bool) (prov_data: [`DataFromRRs | `DataFromRx])
         (read_rn:'loc t) (read_rs:'v t) (read_rt: 'v t)
-        (write_rs:'v-> unit t)
+        (write_rs:'v-> 'a t)
         (read_mem: 'loc -> 'v t) (write_mem: 'loc -> 'v -> unit t)
         (branch: 'loc -> unit t)
         (req: 'v -> 'v -> unit t)
@@ -597,7 +597,7 @@ Monad type:
             let ov,cl_rm,es_rm = Evt.as_singleton_nospecul read_mem
             and (),cl_wm,es_wm= Evt.as_singleton_nospecul write_mem in
             let eiid,write_rs = write_rs ov eiid in
-            let (),cl_wrs,es_wrs = Evt.as_singleton_nospecul write_rs in
+            let r,cl_wrs,es_wrs = Evt.as_singleton_nospecul write_rs in
             let eiid,branch = branch a eiid in
             let (),cl_br,es_br =  Evt.as_singleton_nospecul branch in
             let eiid,eqm = req ov cv eiid in
@@ -606,7 +606,7 @@ Monad type:
             let es =
               E.aarch64_cas is_physical prov_data es_rn es_rs es_rt es_wrs es_rm es_wm es_br in
             let cls = cl_a@cl_cv@cl_nv@cl_rm@cl_wm@cl_wrs@cl_br@cl_eq  in
-            eiid,Evt.add ((),cls,es) acts)
+            eiid,Evt.add (r,cls,es) acts)
           acts_rn (eiid,Evt.empty) in
       eiid,(acts, None)
 
@@ -656,7 +656,7 @@ Monad type:
              write_mem)
 
     let aarch64_cas_ok (is_physical: bool) (read_rn: 'loc t) (read_rs: 'v t)
-        (read_rt: 'v t) (write_rs: 'v -> unit t) (read_mem: 'loc -> 'v t)
+        (read_rt: 'v t) (write_rs: 'v -> 'a t) (read_mem: 'loc -> 'v t)
         (write_mem: 'loc -> 'v -> unit t) (branch: 'loc -> unit t) (req: 'v -> 'v -> unit t) =
       let do_ prov_data =
         do_aarch64_cas_ok is_physical prov_data read_rn read_rs read_rt
@@ -665,7 +665,7 @@ Monad type:
       altT (do_ `DataFromRRs) (do_ `DataFromRx)
 
     let aarch64_cas_no (is_physical: bool) (read_rn: 'loc t)
-        (read_rs: 'v t) (write_rs: 'v -> unit t) (read_mem: 'loc -> 'v t)
+        (read_rs: 'v t) (write_rs: 'v -> 'a t) (read_mem: 'loc -> 'v t)
         (write_mem: 'loc -> 'v -> unit t) (branch: 'loc -> unit t) (rne: 'v -> 'v -> unit t)
         eiid =
       let eiid,read_rn = read_rn eiid in
@@ -681,7 +681,7 @@ Monad type:
             let eiid,write_mem = write_mem a ov eiid in
             let (),cl_wm,es_wm= Evt.as_singleton_nospecul write_mem in
             let eiid,write_rs = write_rs ov eiid in
-            let (),cl_wrs,es_wrs = Evt.as_singleton_nospecul write_rs in
+            let r,cl_wrs,es_wrs = Evt.as_singleton_nospecul write_rs in
             let eiid,branch = branch a eiid in
             let (),cl_br,es_br =  Evt.as_singleton_nospecul branch in
             let eiid,(acts_n,spec_n) = rne ov cv eiid in
@@ -700,7 +700,7 @@ Monad type:
                     es_wm
                     es_br in
                 let cls = cl_a@cl_cv@cl_rm@cl_wm@cl_wrs@cl_br@cl_ne  in
-                eiid,Evt.add ((),cls,es) acts) acts_n (eiid,acts))
+                eiid,Evt.add (r,cls,es) acts) acts_n (eiid,acts))
           acts_rn (eiid,Evt.empty) in
       eiid,(acts, None)
 

herd/monad.mli

@@ -208,16 +208,16 @@ module type S =
     val aarch64_cas_no :
           bool -> (* physical access *)
             'loc t -> 'v t ->
-              ('v -> unit t) -> ('loc -> 'v t) -> ('loc -> 'v -> unit t) ->
+              ('v -> 'a t) -> ('loc -> 'v t) -> ('loc -> 'v -> unit t) ->
               ('loc -> unit t) ->
-                ('v -> 'v -> unit t) -> unit t
+                ('v -> 'v -> unit t) -> 'a t
 
     val aarch64_cas_ok :
       bool -> (* physical access *)
         'loc t -> 'v t -> 'v t ->
-          ('v -> unit t) -> ('loc -> 'v t) -> ('loc -> 'v -> unit t) ->
+          ('v -> 'a t) -> ('loc -> 'v t) -> ('loc -> 'v -> unit t) ->
            ('loc -> unit t) ->
-            ('v -> 'v -> unit t) -> unit t
+            ('v -> 'v -> unit t) -> 'a t
     (* Temporary morello variation of CAS *)
     val aarch64_cas_ok_morello :
         'loc t -> 'v t -> 'v t -> ('loc -> 'v -> unit t) -> unit t

herd/tests/instructions/AArch64.gcs/G005.litmus.expected

@@ -1,12 +1,12 @@
 Test G005 Required
 States 2
-0:X1=0; Fault(P0,GCS:POPM); Fault(P0,GCS:SS2);
+0:X1=0; Fault(P0,GCS:SS2);
 0:X1=4;  ~Fault(P0);
 No
 Witnesses
-Positive: 2 Negative: 4
+Positive: 2 Negative: 2
 Flag Guarded-Control-Stack-is-work-in-progress
 Condition forall (0:X1=4 /\ not (fault(P0)))
-Observation G005 Sometimes 2 4
+Observation G005 Sometimes 2 2
 Hash=e49698900201be45b23a8f9f3ac0cb91
 

herd/tests/instructions/AArch64.gcs/G007.litmus

@@ -0,0 +1,13 @@
+AArch64 G007
+variant=shadowstack
+{
+  SS(x,1) = ssval_t: {1};
+  0:GCSPR_EL1=&x[0];
+}
+
+ P0          ;
+L0:          ;
+ GCSPOPM X1  ;
+ MOV X2,#1   ;
+
+forall fault(P0:L0,GCS:POPM) /\ 0:X2=0

herd/tests/instructions/AArch64.gcs/G007.litmus.expected

@@ -0,0 +1,11 @@
+Test G007 Required
+States 1
+0:X2=0; Fault(P0:L0,GCS:POPM);
+Ok
+Witnesses
+Positive: 1 Negative: 0
+Flag Guarded-Control-Stack-is-work-in-progress
+Condition forall (fault(P0:L0,GCS:POPM) /\ 0:X2=0)
+Observation G007 Always 1 0
+Hash=6a7093cbe2a7bbb87e5456efe4cf9513
+

herd/tests/instructions/AArch64.gcs/G008.litmus

@@ -0,0 +1,15 @@
+AArch64 G008
+variant=shadowstack
+{
+  SS(x,1) = ssval_t: {1};
+  0:GCSPR_EL1=&x[0];
+}
+
+ P0          ;
+ ADR X29,L1  ;
+L0:          ;
+ RET X29     ;
+ MOV X2,#1   ;
+L1:          ;
+
+forall fault(P0:L0,GCS:PRET) /\ 0:X2=0

herd/tests/instructions/AArch64.gcs/G008.litmus.expected

@@ -0,0 +1,11 @@
+Test G008 Required
+States 1
+0:X2=0; Fault(P0:L0,GCS:PRET);
+Ok
+Witnesses
+Positive: 1 Negative: 0
+Flag Guarded-Control-Stack-is-work-in-progress
+Condition forall (fault(P0:L0,GCS:PRET) /\ 0:X2=0)
+Observation G008 Always 1 0
+Hash=d714c8d3cf36a41866635546960ebdbb
+

herd/tests/instructions/AArch64.gcs/G009.litmus

@@ -0,0 +1,15 @@
+AArch64 G009
+variant=shadowstack
+{
+  SS(x,1) = ssval_t: {1};
+  SS(y,2) = ssval_t: {0, 0};
+  0:GCSPR_EL1=&x[0];
+  0:X0=&y[0]
+}
+
+ P0          ;
+L0:          ;
+ GCSSS1 X0   ;
+ MOV X2,#1   ;
+
+forall fault(P0:L0,GCS:SS1) /\ 0:X2=0