From 4aa36f8b1cf76c0eaa73430e81ac38eb9681a0a6 Mon Sep 17 00:00:00 2001 From: Vladimir Murzin Date: Mon, 18 Mar 2024 16:05:19 +0000 Subject: [PATCH] [all]: Rework LDUR to use k0 instead of k0_opt We can improve processing of LDUR instruction by eliminating special handling of the optional immediate. Parser provides `k0` rule which already handle absence of immediate offset by defaulting it to zero, so use it instead of `k0_opt`. Since there are no more users of `k0_opt` left, kill it for good. Signed-off-by: Vladimir Murzin --- herd/AArch64Sem.ml | 1 - herd/tests/instructions/AArch64/A19.litmus.expected | 2 +- jingle/AArch64Arch_jingle.ml | 12 +++--------- lib/AArch64Base.ml | 12 ++++-------- lib/AArch64Parser.mly | 6 +----- litmus/AArch64Compile_litmus.ml | 3 +-- 6 files changed, 10 insertions(+), 26 deletions(-) diff --git a/herd/AArch64Sem.ml b/herd/AArch64Sem.ml index 4db24525dc..189cff7f03 100644 --- a/herd/AArch64Sem.ml +++ b/herd/AArch64Sem.ml @@ -2498,7 +2498,6 @@ module Make ldrs sz (tr_variant v) rd rs e ii | I_LDUR(var,rd,rs,k) -> let sz = tr_variant var in - let k = match k with Some k -> k | None -> 0 in ldr sz rd rs (MemExt.k2idx k) ii | I_LDAR(var,t,rd,rs) -> let sz = tr_variant var in diff --git a/herd/tests/instructions/AArch64/A19.litmus.expected b/herd/tests/instructions/AArch64/A19.litmus.expected index 44cc2c53d2..7531df8327 100644 --- a/herd/tests/instructions/AArch64/A19.litmus.expected +++ b/herd/tests/instructions/AArch64/A19.litmus.expected @@ -6,5 +6,5 @@ Witnesses Positive: 1 Negative: 0 Condition forall (0:X0=2) Observation A19 Always 1 0 -Hash=513393febe8e91d350053aa3ce4fb159 +Hash=137ab50692552983823fd94b6906256f diff --git a/jingle/AArch64Arch_jingle.ml b/jingle/AArch64Arch_jingle.ml index 0c8b318e14..1537a7bfd7 100644 --- a/jingle/AArch64Arch_jingle.ml +++ b/jingle/AArch64Arch_jingle.ml @@ -170,9 +170,7 @@ include Arch.MakeArch(struct | Some(x),Some(_) -> Some(x) | _ -> None end >>> add_subs [Reg(sr_name r1,r1'); Reg(sr_name r2,r2')] - | I_LDUR(_,r1,r2,None),I_LDUR(_,r1',r2',None) - -> add_subs [Reg(sr_name r1,r1'); Reg(sr_name r2,r2')] subs - | I_LDUR(_,r1,r2,Some(k)),I_LDUR(_,r1',r2',Some(k')) + | I_LDUR(_,r1,r2,k),I_LDUR(_,r1',r2',k') -> match_kr subs (K k) (K k') >>> add_subs [Reg(sr_name r1,r1'); Reg(sr_name r2,r2')] @@ -431,15 +429,11 @@ include Arch.MakeArch(struct conv_reg r2 >> fun r2 -> MemExt.expl e >! fun e -> I_LDRS(v,r1,r2,e) - | I_LDUR(a,r1,r2,Some(k)) -> + | I_LDUR(a,r1,r2,k) -> conv_reg r1 >> fun r1 -> conv_reg r2 >> fun r2 -> find_cst k >! fun k -> - I_LDUR(a,r1,r2,Some(k)) - | I_LDUR(a,r1,r2,None) -> - conv_reg r1 >> fun r1 -> - conv_reg r2 >! fun r2 -> - I_LDUR(a,r1,r2,None) + I_LDUR(a,r1,r2,k) | I_LDP(t,a,r1,r2,r3,idx) -> conv_reg r1 >> fun r1 -> conv_reg r2 >> fun r2 -> diff --git a/lib/AArch64Base.ml b/lib/AArch64Base.ml index 0cfccde4d3..8a3def8353 100644 --- a/lib/AArch64Base.ml +++ b/lib/AArch64Base.ml @@ -1086,7 +1086,7 @@ type 'k kinstruction = (* Load and Store *) | I_LDR of variant * reg * reg * 'k MemExt.ext | I_LDRSW of reg * reg * 'k MemExt.ext - | I_LDUR of variant * reg * reg * 'k option + | I_LDUR of variant * reg * reg * 'k (* Neon Extension Load and Store*) | I_LD1 of reg list * int * reg * 'k kr | I_LDAP1 of reg list * int * reg * 'k kr @@ -1472,10 +1472,8 @@ let do_pp_instruction m = pp_mem_ext "LDRSW" V64 r1 r2 idx | I_LDRS ((v,bh),r1,r2,idx) -> pp_mem_ext (ldrs_memo bh) v r1 r2 idx - | I_LDUR (_,r1,r2,None) -> - sprintf "LDUR %s, [%s]" (pp_reg r1) (pp_reg r2) - | I_LDUR (_,r1,r2,Some(k)) -> - sprintf "LDUR %s, [%s, %s]" (pp_reg r1) (pp_reg r2) (m.pp_k k) + | I_LDUR (_,r1,r2,k) -> + sprintf "LDUR %s, [%s%s]" (pp_reg r1) (pp_reg r2) (pp_kr false false (K k)) | I_LDP (t,v,r1,r2,r3,idx) -> pp_memp (ldp_memo t) v r1 r2 r3 idx | I_LDPSW (r1,r2,r3,idx) -> @@ -2529,9 +2527,7 @@ module PseudoI = struct | I_LDR (v,r1,r2,idx) -> I_LDR (v,r1,r2,ext_tr idx) | I_LDRSW (r1,r2,idx) -> I_LDRSW (r1,r2,ext_tr idx) | I_LDRS (v,r1,r2,idx) -> I_LDRS (v,r1,r2,ext_tr idx) - - | I_LDUR (v,r1,r2,None) -> I_LDUR (v,r1,r2,None) - | I_LDUR (v,r1,r2,Some(k)) -> I_LDUR (v,r1,r2,Some(k_tr k)) + | I_LDUR (v,r1,r2,k) -> I_LDUR (v,r1,r2,k_tr k) | I_LDP (t,v,r1,r2,r3,idx) -> I_LDP (t,v,r1,r2,r3,idx_tr idx) | I_LDPSW (r1,r2,r3,idx) -> I_LDPSW (r1,r2,r3,idx_tr idx) | I_STP (t,v,r1,r2,r3,idx) -> I_STP (t,v,r1,r2,r3,idx_tr idx) diff --git a/lib/AArch64Parser.mly b/lib/AArch64Parser.mly index 6f2e2f6ec3..45780aeee7 100644 --- a/lib/AArch64Parser.mly +++ b/lib/AArch64Parser.mly @@ -261,10 +261,6 @@ k: | NUM { MetaConst.Int $1 } | META { MetaConst.Meta $1 } -k0_opt: -| { None } -| COMMA k { Some $2} - k0: | { MetaConst.zero } | COMMA k=k { k } @@ -533,7 +529,7 @@ instr: { let (v, s) = $2 and (ra,ext) = $4 in I_LDRS ((v,B),s,ra,ext) } | LDRSH reg COMMA mem_ea { let (v, s) = $2 and (ra,ext) = $4 in I_LDRS ((v,H),s,ra,ext) } -| LDUR reg COMMA LBRK cxreg k0_opt RBRK +| LDUR reg COMMA LBRK cxreg k0 RBRK { let v,r = $2 in I_LDUR (v,r,$5,$6)} | instr=ldp_instr r1=wreg COMMA r2=wreg COMMA ea=mem_idx diff --git a/litmus/AArch64Compile_litmus.ml b/litmus/AArch64Compile_litmus.ml index 14e8542536..8bbc98c61c 100644 --- a/litmus/AArch64Compile_litmus.ml +++ b/litmus/AArch64Compile_litmus.ml @@ -1256,8 +1256,7 @@ module Make(V:Constant.S)(C:Config) = (* Load and Store *) | I_LDR (v,r1,r2,idx) -> load "ldr" v r1 r2 idx::k | I_LDRSW (r1,r2,idx) -> load "ldrsw" V64 r1 r2 idx::k - | I_LDUR (v,r1,r2,Some(k')) -> load "ldur" v r1 r2 (MemExt.k2idx k')::k - | I_LDUR (v,r1,r2,None) -> load "ldur" v r1 r2 (MemExt.k2idx 0)::k + | I_LDUR (v,r1,r2,k') -> load "ldur" v r1 r2 (MemExt.k2idx k')::k | I_LDP (t,v,r1,r2,r3,idx) -> load_pair (ldp_memo t) v r1 r2 r3 idx::k | I_LDPSW (r1,r2,r3,idx) ->