Pretyping converts vector suffixes to size suffixes (and warns)

CHANGELOG.md

@@ -21,6 +21,10 @@
   ([PR #290](https://github.com/jasmin-lang/jasmin/pull/290)).
   These get extracted to `|<<|` and `|>>|` in EasyCrypt.
 
+  - x86 intrinsics that accept a size suffix (e.g., `_128`) also accept, with a
+    warning, a vector suffix (e.g., `_4u32`)
+    ([PR #303](https://github.com/jasmin-lang/jasmin/pull/303)).
+
 ## Bug fixes
 
  - The x86 instructions `VMOVSHDUP` and `VMOVSLDUP` accept a size suffix (`_128`

compiler/src/pretyping.ml

@@ -1385,7 +1385,11 @@ let tt_prim asmOp ws id args =
     pr ws (match sz with
         | SAw sz -> sz 
         | SA -> d 
-        | SAv _ | SAvv _ -> rs_tyerror ~loc (PrimNotVector s)
+        | SAv (s, ve, sz) ->
+           warning SimplifyVectorSuffix (L.i_loc0 loc) "vector suffix simplified from %s to %a"
+             (PrintCommon.string_of_velem s sz ve) PrintCommon.pp_wsize sz;
+           sz
+        | SAvv _ -> rs_tyerror ~loc (PrimNotVector s)
         | SAx _ -> rs_tyerror ~loc (PrimNotX s))
   | PrimM pr -> if sz = SA then pr ws else rs_tyerror ~loc (PrimNoSize s)
   | PrimV pr -> (match sz with SAv (s, ve, sz) -> pr ws s ve sz | _ -> rs_tyerror ~loc (PrimIsVector s))

compiler/src/printCommon.mli

@@ -1,6 +1,7 @@
 val pp_string0 : Format.formatter -> char list -> unit
 val pp_wsize : Format.formatter -> Wsize.wsize -> unit
 val string_of_signess : Wsize.signedness -> string
+val string_of_velem : Wsize.signedness -> Wsize.wsize -> Wsize.velem -> string
 val string_of_op1 : Expr.sop1 -> string
 val string_of_op2 : Expr.sop2 -> string
 val pp_opn : 'asm Sopn.asmOp -> Format.formatter -> 'asm Sopn.sopn -> unit

compiler/src/utils.ml

@@ -401,6 +401,7 @@ type warning =
   | UseLea
   | IntroduceNone 
   | IntroduceArrayCopy
+  | SimplifyVectorSuffix
   | Always
 
 let warns = ref None

compiler/src/utils.mli

@@ -179,7 +179,8 @@ type warning =
   | ExtraAssignment 
   | UseLea
   | IntroduceNone
-  | IntroduceArrayCopy 
+  | IntroduceArrayCopy
+  | SimplifyVectorSuffix
   | Always
 
 val nowarning : unit -> unit