From 24b0b91d341359c62eac905e8496aa9c543a066f Mon Sep 17 00:00:00 2001 From: crvdgc Date: Wed, 18 Sep 2024 15:29:33 +0100 Subject: [PATCH] [herd] Fix load gather to use base, offsets as iico_data input --- herd/AArch64Sem.ml | 37 +++++++++++++++++++------------------ 1 file changed, 19 insertions(+), 18 deletions(-) diff --git a/herd/AArch64Sem.ml b/herd/AArch64Sem.ml index fb3eca94d..2e1807478 100644 --- a/herd/AArch64Sem.ml +++ b/herd/AArch64Sem.ml @@ -2928,24 +2928,25 @@ module Make let nelem = scalable_nelem r in let esize = scalable_esize r in let>= pred = read_reg_predicate false p ii in - let<>= (base, offsets) = - any_active p pred psize nelem ii (ma >>| mo) (M.unitT M.A.V.(zero, zero)) - in - let op idx = - let load = - let>= lane = scalable_getlane offsets idx esize in - let>= lane = demote lane in - let>= o = memext_sext e k lane in - let>= addr = M.add base o in - let>= v = do_read_mem_ret sz Annot.N aexp Access.VIR addr ii in - let>= v = promote v in - M.op1 (Op.LeftShift (idx * esize)) v - in - is_active_element p pred psize idx ii load (no_action ii >>! M.A.V.zero) - in - let ops = List.map op (Misc.interval 0 nelem) in - let>= result = para_fold_right (M.op Op.Or) ops mzero in - write_reg_scalable r result ii + M.data_input_union + (any_active p pred psize nelem ii (ma >>| mo) (M.unitT M.A.V.(zero, zero))) + begin fun (base, offsets) -> + let op idx = + let load = + let>= lane = scalable_getlane offsets idx esize in + let>= lane = demote lane in + let>= o = memext_sext e k lane in + let>= addr = M.add base o in + let>= v = do_read_mem_ret sz Annot.N aexp Access.VIR addr ii in + let>= v = promote v in + M.op1 (Op.LeftShift (idx * esize)) v + in + is_active_element p pred psize idx ii load (no_action ii >>! M.A.V.zero) + in + let ops = List.map op (Misc.interval 0 nelem) in + let>= result = para_fold_right (M.op Op.Or) ops mzero in + write_reg_scalable r result ii + end let store_scatter_predicated_elem_or_merge sz p ma mo rs e k ii = let r = List.hd rs in