ARM: added UMLAL, SMULL, SMLAL, SMMUL & SMMULR instructions

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

@@ -0,0 +1,29 @@
+export
+fn smlal(reg u32 arg0, reg u32 arg1) -> reg u32 {
+    reg u32 x, y;
+    x, y = #SMLAL(x, y, arg0, arg1);
+
+    // Set flags.
+    reg bool n, z, c, v;
+    n, z, c, v = #CMP(x, 0);
+
+    // Conditions.
+    x, y = #SMLALcc(x, y, x, arg0, z, x, y);            // EQ
+    x, y = #SMLALcc(x, y, x, arg0, !z, x, y);           // NE
+    x, y = #SMLALcc(x, y, x, arg0, c, x, y);            // CS
+    x, y = #SMLALcc(x, y, x, arg0, !c, x, y);           // CC
+    x, y = #SMLALcc(x, y, x, arg0, n, x, y);            // MI
+    x, y = #SMLALcc(x, y, x,arg0, !n, x, y);           // PL
+    x, y = #SMLALcc(x, y, x,arg0, v, x, y);            // VS
+    x, y = #SMLALcc(x, y, x, arg0, !v, x, y);           // VC
+    x, y = #SMLALcc(x, y, x, arg0, c && !z, x, y);      // HI
+    x, y = #SMLALcc(x, y, x, arg0, !c || z, x, y);      // LS
+    x, y = #SMLALcc(x, y, x, arg0, n == v, x, y);       // GE
+    x, y = #SMLALcc(x, y, x, arg0, n != v, x, y);       // LT
+    x, y = #SMLALcc(x, y, x, arg0, !z && n == v, x, y); // GT
+    x, y = #SMLALcc(x, y, x, arg0, z || n != v, x, y);  // LE
+
+    reg u32 res;
+    res = x;
+    return res;
+}

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

@@ -0,0 +1,30 @@
+export
+fn smmul(reg u32 arg0, reg u32 arg1) -> reg u32 {
+    reg u32 x;
+    x = #SMMUL(arg0, arg1);
+
+    // Set flags.
+    reg bool n, z, c, v;
+    n, z, c, v = #CMP(x, 0);
+
+    // Conditions.
+    x = #SMMULcc(x, arg0, z, x);            // EQ
+    x = #SMMULcc(x, arg0, !z, x);           // NE
+    x = #SMMULcc(x, arg0, c, x);            // CS
+    x = #SMMULcc(x, arg0, !c, x);           // CC
+    x = #SMMULcc(x, arg0, n, x);            // MI
+    x = #SMMULcc(x, arg0, !n, x);           // PL
+    x = #SMMULcc(x, arg0, v, x);            // VS
+    x = #SMMULcc(x, arg0, !v, x);           // VC
+    x = #SMMULcc(x, arg0, c && !z, x);      // HI
+    x = #SMMULcc(x, arg0, !c || z, x);      // LS
+    x = #SMMULcc(x, arg0, n == v, x);       // GE
+    x = #SMMULcc(x, arg0, n != v, x);       // LT
+    x = #SMMULcc(x, arg0, !z && n == v, x); // GT
+    x = #SMMULcc(x, arg0, z || n != v, x);  // LE
+
+    reg u32 res;
+    res = x;
+    return res;
+}
+

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

@@ -0,0 +1,30 @@
+export
+fn smmulr(reg u32 arg0, reg u32 arg1) -> reg u32 {
+    reg u32 x;
+    x = #SMMULR(arg0, arg1);
+
+    // Set flags.
+    reg bool n, z, c, v;
+    n, z, c, v = #CMP(x, 0);
+
+    // Conditions.
+    x = #SMMULRcc(x, arg0, z, x);            // EQ
+    x = #SMMULRcc(x, arg0, !z, x);           // NE
+    x = #SMMULRcc(x, arg0, c, x);            // CS
+    x = #SMMULRcc(x, arg0, !c, x);           // CC
+    x = #SMMULRcc(x, arg0, n, x);            // MI
+    x = #SMMULRcc(x, arg0, !n, x);           // PL
+    x = #SMMULRcc(x, arg0, v, x);            // VS
+    x = #SMMULRcc(x, arg0, !v, x);           // VC
+    x = #SMMULRcc(x, arg0, c && !z, x);      // HI
+    x = #SMMULRcc(x, arg0, !c || z, x);      // LS
+    x = #SMMULRcc(x, arg0, n == v, x);       // GE
+    x = #SMMULRcc(x, arg0, n != v, x);       // LT
+    x = #SMMULRcc(x, arg0, !z && n == v, x); // GT
+    x = #SMMULRcc(x, arg0, z || n != v, x);  // LE
+
+    reg u32 res;
+    res = x;
+    return res;
+}
+

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

@@ -0,0 +1,30 @@
+export
+fn smull(reg u32 arg0, reg u32 arg1) -> reg u32 {
+    reg u32 x, y;
+    x, y = #SMULL(arg0, arg1);
+
+    // Set flags.
+    reg bool n, z, c, v;
+    n, z, c, v = #CMP(x, 0);
+
+    // Conditions.
+    x, y = #SMULLcc(x, arg0, z, x, y);            // EQ
+    x, y = #SMULLcc(x, arg0, !z, x, y);           // NE
+    x, y = #SMULLcc(x, arg0, c, x, y);            // CS
+    x, y = #SMULLcc(x, arg0, !c, x, y);           // CC
+    x, y = #SMULLcc(x, arg0, n, x, y);            // MI
+    x, y = #SMULLcc(x, arg0, !n, x, y);           // PL
+    x, y = #SMULLcc(x, arg0, v, x, y);            // VS
+    x, y = #SMULLcc(x, arg0, !v, x, y);           // VC
+    x, y = #SMULLcc(x, arg0, c && !z, x, y);      // HI
+    x, y = #SMULLcc(x, arg0, !c || z, x, y);      // LS
+    x, y = #SMULLcc(x, arg0, n == v, x, y);       // GE
+    x, y = #SMULLcc(x, arg0, n != v, x, y);       // LT
+    x, y = #SMULLcc(x, arg0, !z && n == v, x, y); // GT
+    x, y = #SMULLcc(x, arg0, z || n != v, x, y);  // LE
+
+    reg u32 res;
+    res = x;
+    return res;
+}
+

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

@@ -0,0 +1,29 @@
+export
+fn umlal(reg u32 arg0, reg u32 arg1) -> reg u32 {
+    reg u32 x, y;
+    x, y = #UMLAL(x, y, arg0, arg1);
+
+    // Set flags.
+    reg bool n, z, c, v;
+    n, z, c, v = #CMP(x, 0);
+
+    // Conditions.
+    x, y = #UMLALcc(x, y, x, arg0, z, x, y);            // EQ
+    x, y = #UMLALcc(x, y, x, arg0, !z, x, y);           // NE
+    x, y = #UMLALcc(x, y, x, arg0, c, x, y);            // CS
+    x, y = #UMLALcc(x, y, x, arg0, !c, x, y);           // CC
+    x, y = #UMLALcc(x, y, x, arg0, n, x, y);            // MI
+    x, y = #UMLALcc(x, y, x,arg0, !n, x, y);           // PL
+    x, y = #UMLALcc(x, y, x,arg0, v, x, y);            // VS
+    x, y = #UMLALcc(x, y, x, arg0, !v, x, y);           // VC
+    x, y = #UMLALcc(x, y, x, arg0, c && !z, x, y);      // HI
+    x, y = #UMLALcc(x, y, x, arg0, !c || z, x, y);      // LS
+    x, y = #UMLALcc(x, y, x, arg0, n == v, x, y);       // GE
+    x, y = #UMLALcc(x, y, x, arg0, n != v, x, y);       // LT
+    x, y = #UMLALcc(x, y, x, arg0, !z && n == v, x, y); // GT
+    x, y = #UMLALcc(x, y, x, arg0, z || n != v, x, y);  // LE
+
+    reg u32 res;
+    res = x;
+    return res;
+}

eclib/JModel_m4.ec

@@ -182,6 +182,35 @@ op UMULL (x y: W32.t) : W32.t * W32.t =
   (lo, hi).
 op UMULLcc x y g o h = if g then UMULL x y else (o, h).
 
+op UMLAL (u v x y: W32.t) : W32.t * W32.t =
+  let (hi, lo) = mulu x y in
+  (lo + u, hi + v + of_int (b2i (carry_add lo u false)))%W32.
+op UMLALcc u v x y g o h= if g then UMLAL u v x y else (o, h).
+
+op SMULL (x y: W32.t) : W32.t * W32.t =
+  let lo = x * y in
+  let hi = wmulhs x y in
+  (lo, hi).
+op SMULLcc x y g o h = if g then SMULL x y else (o, h).
+
+op SMLAL (u v x y: W32.t) : W32.t * W32.t =
+  let lo = x * y in
+  let hi = wmulhs x y in
+  (lo + u, hi + v + of_int (b2i (carry_add lo u false)))%W32.
+op SMLALcc u v x y g o h= if g then SMLAL u v x y else (o, h).
+
+op SMMUL (x y: W32.t) : W32.t =
+  wmulhs x y.
+op SMMULcc x y g o = if g then SMMUL x y else o.
+
+op SMMULR (x y: W32.t) : W32.t =
+  let lo = x * y in
+  let hi = wmulhs x y in
+  if msb lo
+    then (hi + (W32.of_int 1))
+    else hi.
+op SMMULRcc x y g o = if g then SMMULR 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

@@ -106,6 +106,13 @@ Variant arm_mnemonic : Type :=
 | UDIV                           (* Unsigned division *)
 | UMULL                          (* Multiply and split the result in two
                                     registers *)
+| UMLAL                          (* Multiply and split the result to add it 
+                                    to the two destinations*)
+| SMULL                          (* Signed version of UMULL*)
+| SMLAL                          (* Signed version of UMLAL*)
+| SMMUL                          (* Signed multiplication, writes the most significant
+                                    32 bits of the result *)
+| SMMULR                         (* Rounding version of SMMUL *)
 
 (* Logical *)
 | AND                            (* Bitwise AND *)
@@ -162,7 +169,7 @@ Instance eqTC_arm_mnemonic : eqTypeC arm_mnemonic :=
 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
+  [:: ADD; ADC; MUL; MLA; MLS; SDIV; SUB; RSB; UDIV; UMULL; UMLAL; SMULL; SMLAL; SMMUL; SMMULR
     ; AND; BIC; EOR; MVN; ORR
     ; ASR; LSL; LSR; ROR
     ; ADR; MOV; MOVT; UBFX; UXTB; UXTH; SBFX
@@ -246,6 +253,11 @@ Definition string_of_arm_mnemonic (mn : arm_mnemonic) : string :=
   | RSB => "RSB"
   | UDIV => "UDIV"
   | UMULL => "UMULL"
+  | UMLAL => "UMLAL"
+  | SMULL => "SMULL"
+  | SMLAL => "SMLAL"
+  | SMMUL => "SMMUL"
+  | SMMULR => "SMMULR" 
   | AND => "AND"
   | BIC => "BIC"
   | EOR => "EOR"
@@ -854,10 +866,7 @@ Definition arm_UDIV_instr : instr_desc_t :=
   |}.
 
 Definition arm_UMULL_semi (wn wm : ty_r) : exec ty_rr :=
-  let res := (zero_extend U64 wn * zero_extend U64 wm)%R in
-  let lo := zero_extend U32 res in
-  let hi := zero_extend U32 (wshr res 32) in
-  ok (hi, lo).
+  ok (wumul wn wm).
 
 Definition arm_UMULL_instr : instr_desc_t :=
   let mn := UMULL in
@@ -879,6 +888,128 @@ Definition arm_UMULL_instr : instr_desc_t :=
     id_pp_asm := pp_arm_op mn opts;
   |}.
 
+Definition arm_UMLAL_semi (dlo dhi wn wm : ty_r) : exec ty_rr :=
+  let (hi, lo) := wumul wn wm in
+  ok(wdaddu dhi dlo hi lo).
+
+Definition arm_UMLAL_instr : instr_desc_t :=
+  let mn := UMLAL in
+  {|
+    id_msb_flag := MSB_MERGE;
+    id_tin := [:: sreg; sreg; sreg; sreg ];
+    id_in := [:: E 0; E 1; E 2; E 3 ];
+    id_tout := [:: sreg; sreg ];
+    id_out := [:: E 0; E 1 ];
+    id_semi := arm_UMLAL_semi;
+    id_nargs := 4;
+    id_args_kinds := ak_reg_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 := [::]; (* TODO_ARM: Complete. *)
+    id_pp_asm := pp_arm_op mn opts;
+  |}.
+
+Definition arm_SMULL_semi (wn wm : ty_r) : exec ty_rr :=
+  let (hi, lo) := wsmul wn wm in
+  ok (lo, hi).
+
+Definition arm_SMULL_instr : instr_desc_t :=
+  let mn := SMULL in
+  {|
+    id_msb_flag := MSB_MERGE;
+    id_tin := [:: sreg; sreg ];
+    id_in := [:: E 2; E 3 ];
+    id_tout := [:: sreg; sreg ];
+    id_out := [:: E 0; E 1 ];
+    id_semi := arm_SMULL_semi;
+    id_nargs := 4;
+    id_args_kinds := ak_reg_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 := [::]; (* TODO_ARM: Complete. *)
+    id_pp_asm := pp_arm_op mn opts;
+  |}.
+
+Definition arm_SMLAL_semi (dlo dhi wn wm : ty_r) : exec ty_rr :=
+  let (hi, lo) := wsmul wn wm in
+  ok(wdadds dhi dlo hi lo).
+
+
+Definition arm_SMLAL_instr : instr_desc_t :=
+  let mn := SMLAL in
+  {|
+    id_msb_flag := MSB_MERGE;
+    id_tin := [:: sreg; sreg; sreg; sreg ];
+    id_in := [:: E 0; E 1; E 2; E 3 ];
+    id_tout := [:: sreg; sreg ];
+    id_out := [:: E 0; E 1 ];
+    id_semi := arm_SMLAL_semi;
+    id_nargs := 4;
+    id_args_kinds := ak_reg_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 := [::]; (* TODO_ARM: Complete. *)
+    id_pp_asm := pp_arm_op mn opts;
+  |}.
+
+Definition arm_SMMUL_semi (wn wm : ty_r) : exec ty_r :=
+  ok (wmulhs wn wm).
+
+Definition arm_SMMUL_instr : instr_desc_t :=
+  let mn := SMMUL 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_SMMUL_semi;
+    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 := [::]; (* TODO_ARM: Complete. *)
+    id_pp_asm := pp_arm_op mn opts;
+  |}.
+
+
+Definition arm_SMMULR_semi (wn wm : ty_r) : exec ty_r :=
+  let (hi, lo) := wsmul wn wm in
+  ok ((hi + wrepr U32 (Z.b2z (msb lo)))%R).
+
+Definition arm_SMMULR_instr : instr_desc_t :=
+  let mn := SMMULR 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_SMMULR_semi;
+    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 := [::]; (* TODO_ARM: Complete. *)
+    id_pp_asm := pp_arm_op mn opts;
+  |}.
+
+
 Definition arm_bitwise_semi
   {ws : wsize}
   (op0 op1 : word ws -> word ws)
@@ -1505,6 +1636,11 @@ Definition mn_desc (mn : arm_mnemonic) : instr_desc_t :=
   | RSB => arm_RSB_instr
   | UDIV => arm_UDIV_instr
   | UMULL => arm_UMULL_instr
+  | UMLAL => arm_UMLAL_instr
+  | SMULL => arm_SMULL_instr
+  | SMLAL => arm_SMLAL_instr
+  | SMMUL => arm_SMMUL_instr
+  | SMMULR => arm_SMMULR_instr
   | AND => arm_AND_instr
   | BIC => arm_BIC_instr
   | EOR => arm_EOR_instr