From e16dbcc30ace3140122642182e021152562d52cf Mon Sep 17 00:00:00 2001 From: Vladimir Murzin Date: Mon, 3 Aug 2026 16:04:42 +0100 Subject: [PATCH 1/4] [herd] Preserve CAS write-result values The AArch64 CAS monad helpers currently force the write_rs callback and the overall operation to return unit. This prevents callers whose register-update step determines instruction control flow from propagating that result; in particular, a GCS CAS must retain either its normal Next result or a Fault result instead of discarding it and advancing unconditionally. Generalise only the callback result from unit to an arbitrary type and carry that value through the existing event structure. The generated events, constraints, dependencies, and all other callbacks are unchanged. Existing callers continue to instantiate the result as unit, making this a backward-compatible and safe relaxation of the helper interface. Signed-off-by: Vladimir Murzin --- herd/eventsMonad.ml | 14 +++++++------- herd/monad.mli | 8 ++++---- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/herd/eventsMonad.ml b/herd/eventsMonad.ml index 0156209200..5fec007e8b 100644 --- a/herd/eventsMonad.ml +++ b/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) diff --git a/herd/monad.mli b/herd/monad.mli index 0c0dfecc0e..1c1cfd10f1 100644 --- a/herd/monad.mli +++ b/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 From 9531498a0755d8f4e3fda5ff5b6e17599ed3c5cb Mon Sep 17 00:00:00 2001 From: Vladimir Murzin Date: Mon, 3 Aug 2026 16:11:13 +0100 Subject: [PATCH 2/4] [herd] Preserve GCS control flow results The generic lift_memop wrapper always discards the memory operation result and returns B.Next. That is correct for ordinary loads and stores, but not for GCS operations whose memory callbacks decide control flow. It caused GCS faults to be replaced by unconditional fall-through, and likewise prevented successful callbacks from carrying their own Next or branch state. Switch to direct use of do_lift_memop for GCSPOPM and GCSSS2 so their selected Fault or Next result is propagated. For GCSSS1, retain the result of both the successful register update and the fault assertion rather than mapping them to unit. GCSSS1 shares the CAS success/failure machinery with architectural CAS, so parameterise the common helper over its lifting function. Ordinary CAS continues through the existing lift_memop adapter and therefore keeps its established unconditional-next behaviour; GCSSS1 supplies a local adapter and can propagate its control flow result. Signed-off-by: Vladimir Murzin --- herd/AArch64Sem.ml | 36 +++++++++++-------- .../AArch64.gcs/G005.litmus.expected | 6 ++-- .../instructions/AArch64.gcs/G007.litmus | 13 +++++++ .../AArch64.gcs/G007.litmus.expected | 11 ++++++ .../instructions/AArch64.gcs/G008.litmus | 15 ++++++++ .../AArch64.gcs/G008.litmus.expected | 11 ++++++ .../instructions/AArch64.gcs/G009.litmus | 15 ++++++++ .../AArch64.gcs/G009.litmus.expected | 11 ++++++ .../instructions/AArch64.gcs/G010.litmus | 15 ++++++++ .../AArch64.gcs/G010.litmus.expected | 11 ++++++ 10 files changed, 127 insertions(+), 17 deletions(-) create mode 100644 herd/tests/instructions/AArch64.gcs/G007.litmus create mode 100644 herd/tests/instructions/AArch64.gcs/G007.litmus.expected create mode 100644 herd/tests/instructions/AArch64.gcs/G008.litmus create mode 100644 herd/tests/instructions/AArch64.gcs/G008.litmus.expected create mode 100644 herd/tests/instructions/AArch64.gcs/G009.litmus create mode 100644 herd/tests/instructions/AArch64.gcs/G009.litmus.expected create mode 100644 herd/tests/instructions/AArch64.gcs/G010.litmus create mode 100644 herd/tests/instructions/AArch64.gcs/G010.litmus.expected diff --git a/herd/AArch64Sem.ml b/herd/AArch64Sem.ml index 2743bc5cfe..766211e8f5 100644 --- a/herd/AArch64Sem.ml +++ b/herd/AArch64Sem.ml @@ -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,7 +3829,10 @@ 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 @@ -3951,7 +3955,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 +3964,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 +4012,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 +4064,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 +4074,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 diff --git a/herd/tests/instructions/AArch64.gcs/G005.litmus.expected b/herd/tests/instructions/AArch64.gcs/G005.litmus.expected index 16cdb9f402..7ab0a03680 100644 --- a/herd/tests/instructions/AArch64.gcs/G005.litmus.expected +++ b/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 diff --git a/herd/tests/instructions/AArch64.gcs/G007.litmus b/herd/tests/instructions/AArch64.gcs/G007.litmus new file mode 100644 index 0000000000..b0ef46f769 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/herd/tests/instructions/AArch64.gcs/G007.litmus.expected b/herd/tests/instructions/AArch64.gcs/G007.litmus.expected new file mode 100644 index 0000000000..0549122e0e --- /dev/null +++ b/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 + diff --git a/herd/tests/instructions/AArch64.gcs/G008.litmus b/herd/tests/instructions/AArch64.gcs/G008.litmus new file mode 100644 index 0000000000..440fcd935f --- /dev/null +++ b/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 \ No newline at end of file diff --git a/herd/tests/instructions/AArch64.gcs/G008.litmus.expected b/herd/tests/instructions/AArch64.gcs/G008.litmus.expected new file mode 100644 index 0000000000..d301debad2 --- /dev/null +++ b/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 + diff --git a/herd/tests/instructions/AArch64.gcs/G009.litmus b/herd/tests/instructions/AArch64.gcs/G009.litmus new file mode 100644 index 0000000000..666adf3421 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/herd/tests/instructions/AArch64.gcs/G009.litmus.expected b/herd/tests/instructions/AArch64.gcs/G009.litmus.expected new file mode 100644 index 0000000000..2be2a4b38c --- /dev/null +++ b/herd/tests/instructions/AArch64.gcs/G009.litmus.expected @@ -0,0 +1,11 @@ +Test G009 Required +States 1 +0:X2=0; Fault(P0:L0,GCS:SS1); +Ok +Witnesses +Positive: 2 Negative: 0 +Flag Guarded-Control-Stack-is-work-in-progress +Condition forall (fault(P0:L0,GCS:SS1) /\ 0:X2=0) +Observation G009 Always 2 0 +Hash=e3981f68ce692f53ca99113860aa2ef4 + diff --git a/herd/tests/instructions/AArch64.gcs/G010.litmus b/herd/tests/instructions/AArch64.gcs/G010.litmus new file mode 100644 index 0000000000..ad1f650225 --- /dev/null +++ b/herd/tests/instructions/AArch64.gcs/G010.litmus @@ -0,0 +1,15 @@ +AArch64 G010 +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: ; + GCSSS2 X0 ; + MOV X2,#1 ; + +forall fault(P0:L0,GCS:SS2) /\ 0:X2=0 \ No newline at end of file diff --git a/herd/tests/instructions/AArch64.gcs/G010.litmus.expected b/herd/tests/instructions/AArch64.gcs/G010.litmus.expected new file mode 100644 index 0000000000..0115efcada --- /dev/null +++ b/herd/tests/instructions/AArch64.gcs/G010.litmus.expected @@ -0,0 +1,11 @@ +Test G010 Required +States 1 +0:X2=0; Fault(P0:L0,GCS:SS2); +Ok +Witnesses +Positive: 1 Negative: 0 +Flag Guarded-Control-Stack-is-work-in-progress +Condition forall (fault(P0:L0,GCS:SS2) /\ 0:X2=0) +Observation G010 Always 1 0 +Hash=fe95805b028a64198d39c03774439baf + From 984e3ccd647753c942edd24ebc2498222912b83c Mon Sep 17 00:00:00 2001 From: Vladimir Murzin Date: Thu, 6 Aug 2026 10:00:51 +0100 Subject: [PATCH 3/4] [herd] Propagate control-flow result through PAC lift_pac_virt always discards the result of the memory operation and returns B.Next after a successful PAC range check. This differs from other lift operations, which propagate the control flow result returned by the caller. As a result, control-flow behavior can differ depending on whether PAC is enabled or not. Align lift_pac_virt with the other lift operations by propagating the control-flow result. Signed-off-by: Vladimir Murzin --- herd/AArch64Sem.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/herd/AArch64Sem.ml b/herd/AArch64Sem.ml index 766211e8f5..f5e871c354 100644 --- a/herd/AArch64Sem.ml +++ b/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 From 230625f586953c3596691e076a3adcc00de3b598 Mon Sep 17 00:00:00 2001 From: Vladimir Murzin Date: Mon, 3 Aug 2026 16:18:28 +0100 Subject: [PATCH 4/4] [herd] Use common memory lifting for GCS branches lift_shadow_stack duplicated an older subset of the AArch64 memory lifting path solely so BL, BLR, and RET could return their own control-flow result. Now that do_lift_memop accepts an explicit result transformer, the duplicate is unnecessary and risks diverging from future update in memory lifting path. Switch to do_lift_memop for GCS branch shadow-stack accesses. This retains their Jump or Fault result while reusing the common translation and permission checking machinery. Signed-off-by: Vladimir Murzin --- herd/AArch64Sem.ml | 41 ++++++++--------------------------------- 1 file changed, 8 insertions(+), 33 deletions(-) diff --git a/herd/AArch64Sem.ml b/herd/AArch64Sem.ml index f5e871c354..f11cf85292 100644 --- a/herd/AArch64Sem.ml +++ b/herd/AArch64Sem.ml @@ -3838,37 +3838,6 @@ Arguments: 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 @@ -3879,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 @@ -3891,10 +3860,13 @@ 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 @@ -3902,7 +3874,7 @@ Arguments: 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 >>| @@ -3932,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