Merge branch 'main' into sct-for-live

Author: eponier

CHANGELOG.md

@@ -9,6 +9,11 @@
   ([PR #1219](https://github.com/jasmin-lang/jasmin/pull/1219));
   fixes [#1218](https://github.com/jasmin-lang/jasmin/issues/1218)).
 
+## Other changes
+
+- The deprecated x86 intrinsic `#VPBLENDVB` has been removed
+  ([PR #1208](https://github.com/jasmin-lang/jasmin/pull/1208)).
+
 # Jasmin 2025.06.0 — Nancy, 2025-06-18
 
 ## New features

compiler/src/pretyping.ml

@@ -1607,7 +1607,6 @@ Deprecated intrinsic operators map (old name -> new name)
 *)
 let deprecated_intrinsic =
   let m = Ms.empty in
-  let m = Ms.add "VPBLENDVB" "BLENDV" m in
   Ms.add "VPMOVMSKB" "MOVEMASK" m
 
 (**

compiler/src/x86_arch_full.ml

@@ -158,7 +158,6 @@ module X86_core = struct
     | VPANDN _ -> true
     | VPAVG _ -> true
     | VPBLEND _ -> true
-    | VPBLENDVB _ -> true
     | VPBROADCAST _ -> true
     | VPCLMULQDQ _ -> true
     | VPCMPEQ _ -> true

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

@@ -6,13 +6,13 @@ fn test_vpblendvb(reg u64 rp) {
   f0 = #set0_256();
   f1 = #set0_256();
   m = #set0_256();
-  f0 = #VPBLENDVB_256(f0, f1, m);
+  f0 = #BLENDV_32u8(f0, f1, m);
   [:u256 rp] = f0;
 
   h0 = #set0_128();
   h1 = #set0_128();
   n = #set0_128();
-  h0 = #VPBLENDVB_128(h0, h1, n);
+  h0 = #BLENDV_16u8(h0, h1, n);
   [:u128 rp + 32] = h0;
 }
 

eclib/JModel_x86.ec

@@ -552,25 +552,18 @@ abbrev [-printing] VPBLEND_8u32 = VPBLENDD_256.
 
 (* ------------------------------------------------------------------- *)
 (*
-| VPBLENDVB `(wsize)
+| BLENDV of velem & vsize
 *)
-op VPBLENDVB_128 (v1 v2 m: W128.t) : W128.t =
+op BLENDV_16u8 (v1 v2 m: W128.t) : W128.t =
   let choose = fun n =>
     let w = if msb (m \bits8 n) then v2 else v1 in
     w \bits8 n in
   pack16 [choose 0; choose 1; choose 2; choose 3; choose 4; choose 5; choose 6; choose 7;
           choose 8; choose 9; choose 10; choose 11; choose 12; choose 13; choose 14; choose 15].
 
-op VPBLENDVB_256 (v1 v2 m: W256.t) : W256.t =
-  pack2 [VPBLENDVB_128 (v1 \bits128 0) (v2 \bits128 0) (m \bits128 0);
-         VPBLENDVB_128 (v1 \bits128 1) (v2 \bits128 1) (m \bits128 1)].
-
-(* ------------------------------------------------------------------- *)
-(*
-| BLENDV of velem & vsize
-*)
-abbrev BLENDV_16u8 = VPBLENDVB_128.
-abbrev BLENDV_32u8 = VPBLENDVB_256.
+op BLENDV_32u8 (v1 v2 m: W256.t) : W256.t =
+  pack2 [BLENDV_16u8 (v1 \bits128 0) (v2 \bits128 0) (m \bits128 0);
+         BLENDV_16u8 (v1 \bits128 1) (v2 \bits128 1) (m \bits128 1)].
 
 op BLENDV_4u32 (v1 v2 m: W128.t) : W128.t =
   let choose = fun n =>

proofs/compiler/x86_instr_decl.v

@@ -130,7 +130,6 @@ Variant x86_op : Type :=
 | VPSHUFHW `(wsize)
 | VPSHUFLW `(wsize)
 | VPBLEND  `(velem) `(wsize)
-| VPBLENDVB `(wsize) (* Deprecated: use BLENDV instead *)
 | BLENDV of velem & wsize (* vpblendvb, vblendvps, vblendvpd *)
 | VPACKUS  `(velem) `(wsize)
 | VPACKSS  `(velem) `(wsize)
@@ -1559,17 +1558,6 @@ Definition Ox86_VPBLEND_instr :=
 
 Definition check_xmm_xmm_xmmm_xmm (_:wsize) := [:: [:: xmm; xmm; xmmm true; xmm]].
 
-(* TODO: remove in 2025.AA.0 *)
-Definition x86_VPBLENDVB sz (x y m: word sz) : tpl (w_ty sz) :=
-  wpblendvb x y m.
-
-(* TODO: remove in 2025.AA.0 *)
-Definition Ox86_VPBLENDVB_instr :=
-  (fun sz => mk_instr_safe
-               (pp_sz "VPBLENDVB" sz) (w3_ty sz) (w_ty sz) [:: Eu 1; Eu 2; Eu 3] [:: Eu 0] MSB_CLEAR
-               (@x86_VPBLENDVB sz) (check_xmm_xmm_xmmm_xmm sz) 4 (size_128_256 sz)
-               (pp_name "vpblendvb" sz), ("VPBLENDVB"%string, prim_128_256 VPBLENDVB)).
-
 Definition x86_BLENDV ve sz (x y m: word sz) : tpl (w_ty sz) :=
   blendv ve x y m.
 
@@ -2214,7 +2202,6 @@ Definition x86_instr_desc o : instr_desc_t :=
   | VPUNPCKH sz sz'    => Ox86_VPUNPCKH_instr.1 sz sz'
   | VPUNPCKL sz sz'    => Ox86_VPUNPCKL_instr.1 sz sz'
   | VPBLEND ve sz      => Ox86_VPBLEND_instr.1 ve sz
-  | VPBLENDVB sz       => Ox86_VPBLENDVB_instr.1 sz
   | BLENDV ve sz       => Ox86_BLENDV_instr.1 ve sz
   | VPACKUS ve sz      => Ox86_VPACKUS_instr.1 ve sz
   | VPACKSS ve sz      => Ox86_VPACKSS_instr.1 ve sz
@@ -2371,7 +2358,6 @@ Definition x86_prim_string :=
    Ox86_VPUNPCKH_instr.2;
    Ox86_VPUNPCKL_instr.2;
    Ox86_VPBLEND_instr.2;
-   Ox86_VPBLENDVB_instr.2;
    Ox86_BLENDV_instr.2;
    Ox86_VPACKUS_instr.2;
    Ox86_VPACKSS_instr.2;