[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 <[email protected]>
herd · Mar 19, 2024 · 4aa36f8 · 4aa36f8
1 parent 6cdf3cf
commit 4aa36f8
Show file tree

Hide file tree

Showing 6 changed files with 10 additions and 26 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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) ->