[herd] Faulting GCSPOPM instruction does not stop control flow

[fsestini]

Consider this litmus test:

AArch64 GCSPOPM-fault
variant=shadowstack,fatal
{
  SS(x,1) = ssval_t: {1};
  0:GCSPR_EL1=&x[0];
}

 P0          ;
L0:          ;
 GCSPOPM X1  ;
 MOV X2,#1   ;

exists fault(P0:L0,GCS:POPM) /\ 0:X2=1

We would expect this to be forbidden, since if GCSPOPM faults then the following MOV should not get executed. However, currently herd7 reports with as allowed, with the following execution:

gcspopm.dot.pdf

[murzinv]

It seems that the issue is caused by lift_memop discarding B.Fault and replacing it with B.Next1T:

let lift_memop ?(tag = "") rA (* Base address register *)
      dir updatedb checked mop perms ma mv an ii =
  let domain = DISide.Data in
  do_lift_memop ~tag rA dir updatedb checked mop perms ma mv an ii
    (fun a -> a >>= M.ignore >>= B.next1T) domain

Therefore, calling do_lift_memop directly appears to fix GCSPOPM:

@@ -3818,7 +3820,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,7 +3830,9 @@ Arguments:
           (M.unitT a_virt)
           mzero
           an
-          ii in
+          ii
+          (fun m -> m)
+          DISide.Data in
         (* Value written to GCSPR depends on the 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

However, other instructions are also affected. In particular, GCSSS1 shares common code with CAS, so fixing it may require more careful consideration.

[murzinv]

#1950