ARM: Add Signed Multiply word by halfword

CHANGELOG.md

@@ -39,7 +39,7 @@
   fixes [#618](https://github.com/jasmin-lang/jasmin/issues/618)).
 
 - Add signed multiply halfwords instructions `SMULBB`, `SMULBT`, `SMULTB`,
-  `SMULTT`, `SMLABB`, `SMLABT`, `SMLATB`, and `SMLATT`
+  `SMULTT`, `SMLABB`, `SMLABT`, `SMLATB`, `SMLATT`, `SMULWB`, and `SMULWT`
   ([PR #644](https://github.com/jasmin-lang/jasmin/pull/644)).
 
 ## Bug fixes

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

@@ -0,0 +1,14 @@
+export
+fn smulw_hw(reg u32 x y) -> reg u32 {
+    reg u32 r;
+    r = #SMULWB(x, y);
+    r = #SMULWT(r, y);
+
+    inline bool b;
+    ?{ "<s" = b } = #CMP(r, y);
+    r = #SMULWBcc(r, y, b, r);
+    r = #SMULWTcc(r, y, b, r);
+
+    r = r;
+    return r;
+}

eclib/JModel_m4.ec

@@ -260,6 +260,18 @@ op SMLATBcc x y acc g o = if g then SMLATB x y acc else o.
 op SMLATT x y acc = SMULTT x y + acc.
 op SMLATTcc x y acc g o = if g then SMLATT x y acc else o.
 
+op smulw_hw (is_hi: bool) (x y: W32.t) : W32.t =
+  let wn = sigextu64 x in
+  let wm = sigextu64 (get_hw y is_hi) in
+  let r = wn * wm in
+  truncateu32 (sar r 16).
+
+op SMULWB = smul_hw false.
+op SMULWBcc x y g o = if g then SMULWB x y else o.
+
+op SMULWT = smul_hw true.
+op SMULWTcc x y g o = if g then SMULWT x y else o.
+
 op UXTB (x: W32.t) (n: W8.t) : W32.t =
   andw (ror x (to_uint n)) (W32.of_int 255).
 op UXTBcc x n g o = if g then UXTB x n else o.

proofs/compiler/arm_instr_decl.v

@@ -118,6 +118,7 @@ Variant arm_mnemonic : Type :=
 
 | SMULBB | SMULBT | SMULTB | SMULTT (* Signed Multiply halfwords. *)
 | SMLABB | SMLABT | SMLATB | SMLATT (* Signed Multiply Accumulate halfwords. *)
+| SMULWB | SMULWT                   (* Signed Multiply word by halfword. *)
 
 (* Logical *)
 | AND                            (* Bitwise AND *)
@@ -179,6 +180,7 @@ Canonical arm_mnemonic_eqType := @ceqT_eqType _ eqTC_arm_mnemonic.
 Definition arm_mnemonics : seq arm_mnemonic :=
   [:: ADD; ADC; MUL; MLA; MLS; SDIV; SUB; RSB; UDIV; UMULL; UMAAL; UMLAL; SMULL; SMLAL; SMMUL; SMMULR
     ; SMULBB; SMULBT; SMULTB; SMULTT; SMLABB; SMLABT; SMLATB; SMLATT
+    ; SMULWB; SMULWT
     ; AND; BIC; EOR; MVN; ORR
     ; ASR; LSL; LSR; ROR; REV; REV16; REVSH
     ; ADR; MOV; MOVT; UBFX; UXTB; UXTH; SBFX
@@ -276,6 +278,8 @@ Definition string_of_arm_mnemonic (mn : arm_mnemonic) : string :=
   | SMLABT => "SMLABT"
   | SMLATB => "SMLATB"
   | SMLATT => "SMLATT"
+  | SMULWB => "SMULWB"
+  | SMULWT => "SMULWT"
   | AND => "AND"
   | BIC => "BIC"
   | EOR => "EOR"
@@ -1083,7 +1087,7 @@ Definition arm_smul_hw_instr hwn hwm : instr_desc_t :=
     id_pp_asm := pp_arm_op mn opts;
   |}.
 
-Definition arm_smla_hw_semi (hwn hwm : bool) (wn wm acc: wreg) : exec wreg :=
+Definition arm_smla_hw_semi (hwn hwm : bool) (wn wm acc : wreg) : exec wreg :=
   ok (get_hw wn hwn * get_hw wm hwm + acc)%R.
 
 Definition arm_smla_hw_instr hwn hwm : instr_desc_t :=
@@ -1095,7 +1099,7 @@ Definition arm_smla_hw_instr hwn hwm : instr_desc_t :=
   {|
     id_msb_flag := MSB_MERGE;
     id_tin := [:: sreg; sreg; sreg ];
-    id_in := [:: E 1; E 2; E 3];
+    id_in := [:: E 1; E 2; E 3 ];
     id_tout := [:: sreg ];
     id_out := [:: E 0 ];
     id_semi := arm_smla_hw_semi hwn hwm;
@@ -1110,6 +1114,32 @@ Definition arm_smla_hw_instr hwn hwm : instr_desc_t :=
     id_pp_asm := pp_arm_op mn opts;
   |}.
 
+Definition arm_smulw_hw_semi (is_hi : bool) (wn wm : wreg) : exec wreg :=
+  let wn := sign_extend U64 wn in
+  let wm := sign_extend U64 (get_hw wm is_hi) in
+  let res := (wn * wm)%R in
+  ok (zero_extend U32 (wsar res 16)).
+
+Definition arm_smulw_hw_instr is_hi : instr_desc_t :=
+  let mn := if is_hi then SMULWT else SMULWB in
+  {|
+    id_msb_flag := MSB_MERGE;
+    id_tin := [:: sreg; sreg ];
+    id_in := [:: E 1; E 2 ];
+    id_tout := [:: sreg ];
+    id_out := [:: E 0 ];
+    id_semi := arm_smulw_hw_semi is_hi;
+    id_nargs := 3;
+    id_args_kinds := ak_reg_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;
+  |}.
+
 Definition arm_bitwise_semi
   {ws : wsize}
   (op0 op1 : word ws -> word ws)
@@ -1781,6 +1811,8 @@ Definition mn_desc (mn : arm_mnemonic) : instr_desc_t :=
   | SMLABT => arm_smla_hw_instr false true
   | SMLATB => arm_smla_hw_instr true false
   | SMLATT => arm_smla_hw_instr true true
+  | SMULWB => arm_smulw_hw_instr false
+  | SMULWT => arm_smulw_hw_instr true
   | AND => arm_AND_instr
   | BIC => arm_BIC_instr
   | EOR => arm_EOR_instr