ARM: Add CLZ

CHANGELOG.md

@@ -38,6 +38,9 @@
   ([PR #620](https://github.com/jasmin-lang/jasmin/pull/620);
   fixes [#618](https://github.com/jasmin-lang/jasmin/issues/618)).
 
+- Add instruction `CLZ` to arm-m4:
+  ([PR #641](https://github.com/jasmin-lang/jasmin/pull/641).
+
 ## Bug fixes
 
 - Type-checking rejects wrongly casted primitive operators

compiler/tests/success/arm-m4/intrinsic_clz.jazz

@@ -0,0 +1,6 @@
+export
+fn main(reg u32 x) -> reg u32 {
+    reg u32 y;
+    y = #CLZ(x);
+    return y;
+}

eclib/JModel_m4.ec

@@ -60,6 +60,9 @@ op ASR x s = let (_n, _z, _c, r) = ASRS x s in r.
 op ASRScc x s g n z c o = if g then ASRS x s else (n, z, c, o).
 op ASRcc x s g o = if g then ASR x s else o.
 
+op CLZ (x: W32.t) : W32.t =
+  W32.of_int (lzcnt (rev (w2bits x))).
+
 op CMP (x y: W32.t) : bool * bool * bool * bool =
   let r = x - y in
   nzcv r (to_uint x - to_uint y) (to_sint x - to_sint y).

proofs/compiler/arm_instr_decl.v

@@ -140,6 +140,7 @@ Variant arm_mnemonic : Type :=
 | UXTB                           (* Extract a byte and zero extend *)
 | UXTH                           (* Extract a halfword and zero extend *)
 | SBFX                           (* Extract a sub-word and sign extend *)
+| CLZ                            (* Count leading zeros. *)
 
 (* Comparison *)
 | CMP                            (* Compare *)
@@ -177,7 +178,7 @@ Definition arm_mnemonics : seq arm_mnemonic :=
   [:: ADD; ADC; MUL; MLA; MLS; SDIV; SUB; RSB; UDIV; UMULL; UMAAL; UMLAL; SMULL; SMLAL; SMMUL; SMMULR
     ; AND; BIC; EOR; MVN; ORR
     ; ASR; LSL; LSR; ROR; REV; REV16; REVSH
-    ; ADR; MOV; MOVT; UBFX; UXTB; UXTH; SBFX
+    ; ADR; MOV; MOVT; UBFX; UXTB; UXTH; SBFX; CLZ
     ; CMP; TST
     ; LDR; LDRB; LDRH; LDRSB; LDRSH
     ; STR; STRB; STRH
@@ -283,6 +284,7 @@ Definition string_of_arm_mnemonic (mn : arm_mnemonic) : string :=
   | UXTB => "UXTB"
   | UXTH => "UXTH"
   | SBFX => "SBFX"
+  | CLZ => "CLZ"
   | CMP => "CMP"
   | TST => "TST"
   | LDR => "LDR"
@@ -1682,6 +1684,26 @@ Definition arm_store_instr mn : instr_desc_t :=
     id_pp_asm := pp_arm_op mn opts;
   |}.
 
+Definition arm_CLZ_instr :=
+  let mn := CLZ in
+  {|
+    id_msb_flag := MSB_MERGE;
+    id_tin := [:: sreg ];
+    id_in := [:: E 1 ];
+    id_tout := [:: sreg ];
+    id_out := [:: E 0 ];
+    id_semi := fun w => ok (leading_zero w);
+    id_nargs := 2;
+    id_args_kinds := ak_reg_reg;
+    id_eq_size := refl_equal;
+    id_tin_narr := refl_equal;
+    id_tout_narr := refl_equal;
+    id_check_dest := refl_equal;
+    id_str_jas := pp_s (string_of_arm_mnemonic mn);
+    id_safe := [::];
+    id_pp_asm := pp_arm_op mn opts;
+  |}.
+
 
 (* -------------------------------------------------------------------- *)
 (* Description of instructions. *)
@@ -1723,6 +1745,7 @@ Definition mn_desc (mn : arm_mnemonic) : instr_desc_t :=
   | UXTB => arm_UXTB_instr
   | UXTH => arm_UXTH_instr
   | SBFX => arm_SBFX_instr
+  | CLZ => arm_CLZ_instr
   | CMP => arm_CMP_instr
   | TST => arm_TST_instr
   | LDR => arm_load_instr LDR

proofs/compiler/x86_instr_decl.v

@@ -497,17 +497,6 @@ Definition x86_DEC sz (w: word sz) : ex_tpl (b4w_ty sz) :=
     (w - 1)
     (wsigned w - 1)%Z).
 
-
-Fixpoint leading_zero_aux (n: Z) (k : nat) (sz : nat) :=
-  if (n <? 2^(sz - k))%Z then k 
-  else match k with 
-  | 0 => 0
-  | S k' => leading_zero_aux n k' sz
-  end.
-
-Definition leading_zero sz (w: word sz) : word sz := 
-  wrepr sz (leading_zero_aux (wunsigned w) sz sz).
-
 Definition x86_LZCNT sz (w: word sz) : ex_tpl (b5w_ty sz) := 
    Let _ := check_size_16_64 sz in
    let v := leading_zero w in 

proofs/lang/word.v

@@ -1376,6 +1376,20 @@ Fixpoint bitpdep sz (w:word sz) (i:nat) (mask:bitseq) :=
 Definition pdep sz (w1 w2: word sz) :=
  wrepr sz (t2w (in_tuple (bitpdep w1 0 (w2t w2)))).
 
+(* -------------------------------------------------------------------*)
+
+Fixpoint leading_zero_aux (n : Z) (res sz : nat) : nat :=
+  if (n <? 2 ^ (sz - res))%Z
+  then res
+  else
+    match res with
+    | O => O
+    | S res' => leading_zero_aux n res' sz
+    end.
+
+Definition leading_zero (sz : wsize) (w : word sz) : word sz :=
+  wrepr sz (leading_zero_aux (wunsigned w) sz sz).
+
 (* -------------------------------------------------------------------*)
 Definition halve_list A : seq A → seq A :=
   fix loop m := if m is a :: _ :: m' then a :: loop m' else m.