Fix semantics of SHLD_16 and SHRD_16

When the (masked) shift amount is larger than the operand size, the
result is undefined. This is soundly approximated in the semantics by
throwing a type error.

Note that it is not necessary to fix the EasyCrypt model: it is meant to
be correct for safe executions only.

CHANGELOG.md

@@ -26,6 +26,9 @@
 
 ## Bug fixes
 
+- Fix semantics of the `SHLD_16` and `SHRD_16` 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 type 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).