Fix mulx

CHANGELOG.md

@@ -25,7 +25,14 @@
 - Notation for string literals; there is no implicit zero terminator;
   ([PR #517](https://github.com/jasmin-lang/jasmin/pull/517)).
 
+- Add the instruction MULX_hi,
+     hi = #MULX(x, y); is equivalent to (hi, _) = #MULX(x, y);
+  but the compiler do not needs an extra register for the "_".
+
 ## Bug fixes
+- Fix semantics of the `MULX` instructions
+  ([PR #531](https://github.com/jasmin-lang/jasmin/pull/531);
+  fixes [#525](https://github.com/jasmin-lang/jasmin/issues/525).
 
 - Fix semantics of the `IMUL`, `IMULr`, and `IMULri` instructions
   ([PR #528](https://github.com/jasmin-lang/jasmin/pull/528);

compiler/tests/success/x86-64/mulx.jazz

@@ -0,0 +1,55 @@
+export fn test (reg u64 x, reg u64 y) -> reg u64 {
+   reg u64 hi, lo, z1, z2;
+   x = x;
+   (hi,lo) = #MULX(x, y);
+   z1 = hi << 1;
+   z1 += lo;
+   return z1;
+
+}
+
+/* FAIL
+export fn test_ (reg u64 x, reg u64 y) -> reg u64 {
+   reg u64 hi, lo, z1, z2;
+   x = x;
+   (lo,lo) = #MULX(x, y);
+   z1 = lo;
+   z1 = lo << 1;
+   z1 += lo;
+   return z1;
+
+}
+*/
+
+export fn test_lo_hi (reg u64 x, reg u64 y) -> reg u64 {
+   reg u64 hi, lo, z1, z2;
+   x = x;
+   (lo,hi) = #MULX_lo_hi(x, y);
+   z1 = hi << 1;
+   z1 += lo;
+   return z1;
+
+}
+
+export fn test_hi (reg u64 x, reg u64 y) -> reg u64 {
+   reg u64 hi, lo, z1, z2;
+   x = x;
+   hi = #MULX_hi(x, y);
+   z1 = hi << 1;
+   return z1;
+
+}
+
+/* success, but mulx still use 2 differents registers for destination */
+/* But the extraction fail */ 
+/*
+export fn test_lo_hi_ (reg u64 x, reg u64 y) -> reg u64 {
+   reg u64 hi, lo, z1, z2;
+   x = x;
+   (lo,lo) = #MULX_lo_hi(x, y);
+   z1 = lo;
+   z1 = z1 << 1;
+   z1 += lo;
+   return z1;
+}
+*/

eclib/JWord.ec

@@ -1585,6 +1585,8 @@ op ADCX_XX (v1 v2: t) (c:bool) = addc v1 v2 c.
 op ADOX_XX (v1 v2: t) (c:bool) = addc v1 v2 c.
 
 op MULX_XX (v1 v2: t) = mulu v1 v2.
+op MULX_lo_hi_XX (v1 v2: t) = let (hi,lo) = mulu v1 v2 in (lo, hi).
+op MULX_hi_XX (v1 v2: t) = (mulu v1 v2).`1.
 
 op sub_borrow (x y c: int) : t =
   of_int (x - y - c).

proofs/compiler/x86_extra.v

@@ -53,10 +53,15 @@ Variant x86_extra_op : Type :=
 | Oset0     of wsize  (* set register + flags to 0 (implemented using XOR x x or VPXOR x x) *)
 | Oconcat128          (* concatenate 2 128 bits word into 1 256 word register *)   
 | Ox86MOVZX32
+| Ox86MULX  of wsize
+| Ox86MULX_hi of wsize
+
 | Ox86SLHinit
 | Ox86SLHupdate
 | Ox86SLHmove
-| Ox86SLHprotect of wsize.
+| Ox86SLHprotect of wsize
+
+.
 
 Scheme Equality for x86_extra_op.
 
@@ -105,6 +110,30 @@ Definition Ox86MOVZX32_instr :=
            (λ x : u32, ok (zero_extend U64 x)) 
            [::].
 
+Definition x86_MULX sz (v1 v2: word sz) : ex_tpl (w2_ty sz sz) :=
+  Let _ := check_size_32_64 sz in
+  ok (wumul v1 v2).
+
+Definition Ox86MULX_instr sz :=
+   let name := "MULX"%string in
+   mk_instr_desc (pp_sz name sz)
+        (w2_ty sz sz) [::ADImplicit (to_var RDX); E 2]
+        (w2_ty sz sz) [:: E 0; E 1] (* hi, lo *)
+        (@x86_MULX sz) [::].
+
+Definition x86_MULX_hi sz (v1 v2: word sz) : ex_tpl (w_ty sz) :=
+  Let _ := check_size_32_64 sz in
+  let '(hi,lo) := wumul v1 v2 in
+  ok hi.
+
+Definition Ox86MULX_hi_instr sz :=
+   let name := "MULX_hi"%string in
+   mk_instr_desc (pp_sz name sz)
+        (w2_ty sz sz) [::ADImplicit (to_var RDX); E 1]
+        (w_ty sz) [:: E 0] 
+        (@x86_MULX_hi sz) [::].
+
+
 Definition Ox86SLHinit_str := append "Ox86_" SLHinit_str.
 Definition Ox86SLHinit_instr :=
   mk_instr_desc (pp_s Ox86SLHinit_str)
@@ -176,17 +205,21 @@ Definition get_instr_desc o :=
   | Oset0 ws         => Oset0_instr ws
   | Oconcat128       => Oconcat128_instr
   | Ox86MOVZX32      => Ox86MOVZX32_instr
+  | Ox86MULX ws      => Ox86MULX_instr ws
+  | Ox86MULX_hi ws   => Ox86MULX_hi_instr ws
+
   | Ox86SLHinit       => Ox86SLHinit_instr
   | Ox86SLHupdate     => Ox86SLHupdate_instr
   | Ox86SLHmove       => Ox86SLHmove_instr
   | Ox86SLHprotect ws => Ox86SLHprotect_instr ws
   end.
 
 Definition prim_string :=
-  [::
-    ("set0"%string, primP Oset0);
-    ("concat_2u128"%string, primM Oconcat128)
-    (* Ox86MOVZX32 is ignored on purpose *)
+  [:: ("set0"%string, primP Oset0)
+    ; ("concat_2u128"%string, primM Oconcat128)
+      (* Ox86MOVZX32 is ignored on purpose *)
+    ; ("MULX"%string, prim_32_64 Ox86MULX)
+    ; ("MULX_hi"%string, prim_32_64 Ox86MULX_hi) 
     (* SLH operators are ignored on purpose. *)
   ].
 
@@ -266,11 +299,29 @@ Definition assemble_extra ii o outx inx : cexec (seq (asm_op_msb_t * lexprs * re
     ok [:: outx ::= (MOV U32) inx ]
   | Oconcat128 =>
     Let inx :=
-        match inx with
-        | [:: h; Rexpr (Fvar _) as l] => ok [:: l; h; re8_1]
-        |  _ => Error (E.error ii "Oconcat: assert false")
-        end in
+      match inx with
+      | [:: h; Rexpr (Fvar _) as l] => ok [:: l; h; re8_1]
+      |  _ => Error (E.error ii "Oconcat: assert false")
+      end in
     ok [:: outx ::= VINSERTI128 inx ]
+  | Ox86MULX sz => 
+    Let outx := 
+      match outx with 
+      | [:: LLvar hi; LLvar lo] => 
+          Let _ := assert (v_var lo != v_var hi) (E.error ii "Ox86MULX: lo = hi") in
+          ok [:: LLvar lo; LLvar hi]
+      | _ => Error (E.error ii "Ox86MULX: assert false")
+      end in
+    ok [:: outx ::= (MULX_lo_hi sz) inx]
+
+  | Ox86MULX_hi sz => 
+    Let outx := 
+      match outx with 
+      | [:: LLvar hi] => ok [::LLvar hi; LLvar hi]
+      | _ => Error (E.error ii "Ox86MULX_hi: assert false")
+      end in
+    ok [:: outx ::= (MULX_lo_hi sz) inx]
+
   | Ox86SLHinit => assemble_slh_init outx
   | Ox86SLHupdate => assemble_slh_update ii outx inx
   | Ox86SLHmove => ok [:: outx ::= (MOV Uptr) inx ]

proofs/compiler/x86_instr_decl.v

@@ -71,7 +71,7 @@ Variant x86_op : Type :=
 | SAR    of wsize    (*   signed / right *)
 | SHLD   of wsize    (* unsigned (double) / left *)
 | SHRD   of wsize    (* unsigned (double) / right *)
-| MULX    of wsize  (* mul unsigned, doesn't affect arithmetic flags *)
+| MULX_lo_hi of wsize  (* mul unsigned, doesn't affect arithmetic flags *)
 | ADCX    of wsize  (* add with carry flag, only writes carry flag *)
 | ADOX    of wsize  (* add with overflow flag, only writes overflow flag *)
 
@@ -464,9 +464,10 @@ Definition x86_ADCX sz (v1 v2: word sz) (c:bool) : ex_tpl (bw_ty sz) :=
   let (c,w) := waddcarry v1 v2 c in
   ok (Some c, w).
 
-Definition x86_MULX sz (v1 v2: word sz) : ex_tpl (w2_ty sz sz) :=
+Definition x86_MULX_lo_hi sz (v1 v2: word sz) : ex_tpl (w2_ty sz sz) :=
   Let _ := check_size_32_64 sz in
-  ok (wumul v1 v2).
+  let '(hi,lo) := wumul v1 v2 in
+  ok (lo, hi).
 
 Definition sub_borrow sz (x y c: Z) : word sz :=
   wrepr sz (x - y - c).
@@ -1354,13 +1355,13 @@ Definition Ox86_ADOX_instr :=
   mk_instr_w2b_bw "ADOX" x86_ADCX OF check_adcx (prim_32_64 ADOX) (pp_iname "adox").
 
 Definition check_mulx := [:: [::r;r;rm true]].
-Definition Ox86_MULX_instr :=
-  let name := "MULX"%string in
+Definition Ox86_MULX_lo_hi_instr :=
+  let name := "MULX_lo_hi"%string in
    ((fun (sz:wsize) =>
      mk_instr (pp_sz name sz) (w2_ty sz sz) (w2_ty sz sz)
-         [::R RDX; E 2] [:: E 0; E 1] (reg_msb_flag sz)
-         (@x86_MULX sz) check_mulx 3 [::] (pp_iname "mulx" sz)),
-    (name, prim_32_64 MULX)).
+         [::R RDX; E 2] [:: E 1; E 0] (* lo, hi *) (reg_msb_flag sz)
+         (@x86_MULX_lo_hi sz) check_mulx 3 [::] (pp_iname "mulx" sz)),
+    (name, prim_32_64 MULX_lo_hi)).
 
 Definition check_neg (_:wsize) := [::[::rm false]].
 Definition Ox86_NEG_instr               :=
@@ -1919,7 +1920,7 @@ Definition x86_instr_desc o : instr_desc_t :=
   | ADC sz             => Ox86_ADC_instr.1 sz
   | ADCX sz            => Ox86_ADCX_instr.1 sz
   | ADOX sz            => Ox86_ADOX_instr.1 sz
-  | MULX sz            => Ox86_MULX_instr.1 sz
+  | MULX_lo_hi sz      => Ox86_MULX_lo_hi_instr.1 sz
   | SBB sz             => Ox86_SBB_instr.1 sz
   | NEG sz             => Ox86_NEG_instr.1 sz
   | INC sz             => Ox86_INC_instr.1 sz
@@ -2056,7 +2057,7 @@ Definition x86_prim_string :=
    Ox86_ADC_instr.2;
    Ox86_ADCX_instr.2;
    Ox86_ADOX_instr.2;
-   Ox86_MULX_instr.2;
+   Ox86_MULX_lo_hi_instr.2;
    Ox86_SBB_instr.2;
    Ox86_NEG_instr.2;
    Ox86_INC_instr.2;

proofs/compiler/x86_params_proof.v

@@ -775,6 +775,49 @@ Proof.
     apply: (lom_eqv_write_reg _ _ hlow).
     by right.
 
+  (* Ox86MULX *)
+  + move=> sz. rewrite /exec_sopn /sopn_sem /=.
+    case lvs => // -[] // hi [] // [] // lo [] //.
+    t_xrbindP => hargs whilo hwhilo <- /=.
+    t_xrbindP => _ _ /set_varP [hdb1 htr1 ->] <- _ _ /set_varP [hdb2 htr2 ->] <- <- _ hne <- <- /=.
+    t_xrbindP => -[op' asm_args] hass <- hlow /=.
+    assert (h1 := assemble_asm_opI hass); case: h1 => hca hcd hidc -> /= {hass}.
+    have hex: exec_sopn (Oasm (BaseOp (None, MULX_lo_hi sz))) xs = ok [:: Vword whilo.2; Vword whilo.1].
+    + rewrite /exec_sopn /sopn_sem /=.
+      case: (xs) hwhilo => // v1; t_xrbindP => -[] // v2; t_xrbindP => -[] // w1 -> w2 ->.
+      by rewrite /x86_MULX /x86_MULX_lo_hi; t_xrbindP => -> /= <- /=. 
+    have hw' :
+       write_lexprs [:: LLvar lo; LLvar hi] [:: Vword whilo.2; Vword whilo.1] m =
+       ok (with_vm m ((evm m).[lo <- Vword whilo.2]).[hi <- Vword whilo.1]).
+    + by rewrite /= /set_var hdb1 htr1 hdb2 htr2 /= with_vm_idem.
+    have [s' {hw' hex hca hcd hidc} /=] := 
+      compile_asm_opn_aux eval_assemble_cond hargs hex hw' hca hcd hidc hlow.
+    rewrite /eval_op /= => -> /= hlow'.
+    exists s' => //; apply: lom_eqv_ext hlow' => /= z.
+    by rewrite !Vm.setP; case eqP => [<- | //]; rewrite (negbTE hne).
+
+  (* Ox86MULX_hi *)
+  + move=> sz. rewrite /exec_sopn /sopn_sem /=.
+    case lvs => // -[] // hi [] //.
+    t_xrbindP => hargs whi hwhi <- /=.
+    t_xrbindP => _ _ /set_varP [hdb1 htr1 ->] <- <- _ <- <- /=.
+    t_xrbindP => -[op' asm_args] hass <- hlow /=.
+    assert (h1 := assemble_asm_opI hass); case: h1 => hca hcd hidc -> /= {hass}.
+    case: xs hargs hwhi => // v1; t_xrbindP => -[] // v2; t_xrbindP => -[] // hargs w1 hv1 w2 hv2.
+    rewrite /x86_MULX_hi; t_xrbindP => hsz. 
+    case heq :(wumul) => [whi' wlo] [?]; subst whi'.
+    have hex: exec_sopn (Oasm (BaseOp (None, MULX_lo_hi sz))) [:: v1; v2] = ok [:: Vword wlo; Vword whi].
+    + by rewrite /exec_sopn /sopn_sem /= hv1 hv2 /= /x86_MULX_lo_hi hsz heq.
+    have hw' :
+       write_lexprs [:: LLvar hi; LLvar hi] [:: Vword wlo; Vword whi] m =
+       ok (with_vm m ((evm m).[hi <- Vword wlo]).[hi <- Vword whi]).
+    + by rewrite /= /set_var hdb1 htr1 /=; move: htr1 => /=; case: vtype.
+    have [s' {hw' hex hca hcd hidc} /=] := 
+      compile_asm_opn_aux eval_assemble_cond hargs hex hw' hca hcd hidc hlow.
+    rewrite /eval_op /= => -> /= hlow'.
+    exists s' => //; apply: lom_eqv_ext hlow' => /= z.
+    by rewrite !Vm.setP; case eqP.
+
   (* SLHinit *)
   + rewrite /exec_sopn /= /sopn_sem /assemble_slh_init /=; t_xrbindP.
     case: xs => // hargs _ [<-] <-.