Fix semantics of SHLD_16, SHRD_16, and VPSxLV

CHANGELOG.md

@@ -26,6 +26,9 @@
 
 ## Bug fixes
 
+- Fix semantics of the `SHLD_16`, `SHRD_16`, `VPSLLV`, and `VPSRLV` instructions
+  ([PR #520](https://github.com/jasmin-lang/jasmin/pull/520)).
+
 - Handle the size parameter in LZCNT semantic
   ([PR #516](https://github.com/jasmin-lang/jasmin/pull/516);
   fixes [#515](https://github.com/jasmin-lang/jasmin/issues/515)).

compiler/tests/exec/sem_unit.expected

@@ -2,3 +2,5 @@ vpsllv_4u32(0X1; 0XF4240) = 0X0
 vpsllv_4u32(0X5A5A5A5A5A5A5A5A5A5A5A5A5A5A5A5A; 0X4000000030000000200000001) = 0XA5A5A5A0D2D2D2D069696968B4B4B4B4
 vpsllv_8u32(0X1; 0XF4240) = 0X0
 vpsllv_4u64(0XFFFF001248A00000FFFF001248A00000FFFF001248A00000FFFF001248A000; 0X2000000000000000400000000000000080000000000000010) = 0X3FFFC00492280000FFFF001248A0000FFFF001248A00000FF001248A0000000
+shrd_16(0X2; 0X9; 0X10) = 0X9
+shrd_16(0X2; 0X9; 0X11) failed with arithmetic error

compiler/tests/exec/sem_unit.jazz

@@ -15,3 +15,8 @@ fn vpsllv_4u64(reg u256 x y) -> reg u256 {
   z = #VPSLLV_4u64(x, y);
   return z;
 }
+
+fn shrd_16(reg u16 x y, reg u8 c) -> reg u16 {
+  ?{}, x = #SHRD_16(x, y, c);
+  return x;
+}

compiler/tests/exec/sem_unit.ml

@@ -3,6 +3,8 @@ open Execlib
 
 let w_of_z sz z = Values.Vword (sz, Conv.word_of_z sz z)
 let w_of_string sz n = w_of_z sz (Z.of_string n)
+let w8 i = w_of_string Wsize.U8 i
+let w16 i = w_of_string Wsize.U16 i
 let w128 i = w_of_string Wsize.U128 i
 let w256 i = w_of_string Wsize.U256 i
 
@@ -20,4 +22,6 @@ let () =
       w256 "0x00ffff001248a00000ffff001248a00000ffff001248a00000ffff001248a000";
       w256 "0x0000000000000002000000000000000400000000000000080000000000000010";
     ];
+  exec prog [] "shrd_16" [ w16 "2"; w16 "9"; w8 "16" ];
+  exec prog [] "shrd_16" [ w16 "2"; w16 "9"; w8 "17" ];
   ()

proofs/compiler/x86_instr_decl.v

@@ -645,9 +645,11 @@ Definition x86_SHLD sz (v1 v2: word sz) (i: u8) : ex_tpl (b5w_ty sz) :=
   if i == 0%R then
     ok (rflags_None_w v1)
   else
+    let j := (wsize_bits sz - wunsigned i)%Z in
+    if (j <? 0)%Z then Error ErrArith else
     let rc := msb (wshl v1 (wunsigned i - 1)) in
     let r1 := wshl v1 (wunsigned i) in
-    let r2 := wshr v2 (wsize_bits sz - (wunsigned i)) in
+    let r2 := wshr v2 j in
     let r  := wor r1 r2 in
     rflags_OF i r rc (msb r (+) rc).
 
@@ -667,9 +669,11 @@ Definition x86_SHRD sz (v1 v2: word sz) (i: u8) : ex_tpl (b5w_ty sz) :=
   if i == 0%R then
     ok (rflags_None_w v1)
   else
+    let j := (wsize_bits sz - wunsigned i)%Z in
+    if (j <? 0)%Z then Error ErrArith else
     let rc := lsb (wshr v1 (wunsigned i - 1)) in
     let r1 := wshr v1 (wunsigned i) in
-    let r2 := wshl v2 (wsize_bits sz - (wunsigned i)) in
+    let r2 := wshl v2 j in
     let r  := wor r1 r2 in
     rflags_OF i r rc (msb r (+) msb v1).
 
@@ -809,7 +813,7 @@ Definition x86_VPSRA (ve: velem) sz := x86_u128_shift ve sz (@wsar _).
 
 (* ---------------------------------------------------------------- *)
 Definition x86_u128_shift_variable ve sz op v1 v2 : ex_tpl (w_ty sz) :=
-  Let _ := check_size_32_64 ve in
+  Let _ := check_size_16_64 ve in
   Let _ := check_size_128_256 sz in
   ok (lift2_vec ve (λ v1 v2, op v1 (Z.min (wunsigned v2) (wsize_bits ve))) sz v1 v2).