fix: UB in shifts

Author: hargoniX

src/Init/Data/SInt/Basic.lean

@@ -96,9 +96,9 @@ def Int8.lor (a b : Int8) : Int8 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
 @[extern "lean_int8_xor"]
 def Int8.xor (a b : Int8) : Int8 := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
 @[extern "lean_int8_shift_left"]
-def Int8.shiftLeft (a b : Int8) : Int8 := ⟨⟨a.toBitVec <<< (mod b 8).toBitVec⟩⟩
+def Int8.shiftLeft (a b : Int8) : Int8 := ⟨⟨a.toBitVec <<< (b.toBitVec.smod 8)⟩⟩
 @[extern "lean_int8_shift_right"]
-def Int8.shiftRight (a b : Int8) : Int8 := ⟨⟨BitVec.sshiftRight' a.toBitVec (mod b 8).toBitVec⟩⟩
+def Int8.shiftRight (a b : Int8) : Int8 := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 8)⟩⟩
 @[extern "lean_int8_complement"]
 def Int8.complement (a : Int8) : Int8 := ⟨⟨~~~a.toBitVec⟩⟩
 
@@ -193,9 +193,9 @@ def Int16.lor (a b : Int16) : Int16 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
 @[extern "lean_int16_xor"]
 def Int16.xor (a b : Int16) : Int16 := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
 @[extern "lean_int16_shift_left"]
-def Int16.shiftLeft (a b : Int16) : Int16 := ⟨⟨a.toBitVec <<< (mod b 16).toBitVec⟩⟩
+def Int16.shiftLeft (a b : Int16) : Int16 := ⟨⟨a.toBitVec <<< (b.toBitVec.smod 16)⟩⟩
 @[extern "lean_int16_shift_right"]
-def Int16.shiftRight (a b : Int16) : Int16 := ⟨⟨BitVec.sshiftRight' a.toBitVec (mod b 16).toBitVec⟩⟩
+def Int16.shiftRight (a b : Int16) : Int16 := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 16)⟩⟩
 @[extern "lean_int16_complement"]
 def Int16.complement (a : Int16) : Int16 := ⟨⟨~~~a.toBitVec⟩⟩
 
@@ -294,9 +294,9 @@ def Int32.lor (a b : Int32) : Int32 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
 @[extern "lean_int32_xor"]
 def Int32.xor (a b : Int32) : Int32 := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
 @[extern "lean_int32_shift_left"]
-def Int32.shiftLeft (a b : Int32) : Int32 := ⟨⟨a.toBitVec <<< (mod b 32).toBitVec⟩⟩
+def Int32.shiftLeft (a b : Int32) : Int32 := ⟨⟨a.toBitVec <<< (b.toBitVec.smod 32)⟩⟩
 @[extern "lean_int32_shift_right"]
-def Int32.shiftRight (a b : Int32) : Int32 := ⟨⟨BitVec.sshiftRight' a.toBitVec (mod b 32).toBitVec⟩⟩
+def Int32.shiftRight (a b : Int32) : Int32 := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 32)⟩⟩
 @[extern "lean_int32_complement"]
 def Int32.complement (a : Int32) : Int32 := ⟨⟨~~~a.toBitVec⟩⟩
 
@@ -399,9 +399,9 @@ def Int64.lor (a b : Int64) : Int64 := ⟨⟨a.toBitVec ||| b.toBitVec⟩⟩
 @[extern "lean_int64_xor"]
 def Int64.xor (a b : Int64) : Int64 := ⟨⟨a.toBitVec ^^^ b.toBitVec⟩⟩
 @[extern "lean_int64_shift_left"]
-def Int64.shiftLeft (a b : Int64) : Int64 := ⟨⟨a.toBitVec <<< (mod b 64).toBitVec⟩⟩
+def Int64.shiftLeft (a b : Int64) : Int64 := ⟨⟨a.toBitVec <<< (b.toBitVec.smod 64)⟩⟩
 @[extern "lean_int64_shift_right"]
-def Int64.shiftRight (a b : Int64) : Int64 := ⟨⟨BitVec.sshiftRight' a.toBitVec (mod b 64).toBitVec⟩⟩
+def Int64.shiftRight (a b : Int64) : Int64 := ⟨⟨BitVec.sshiftRight' a.toBitVec (b.toBitVec.smod 64)⟩⟩
 @[extern "lean_int64_complement"]
 def Int64.complement (a : Int64) : Int64 := ⟨⟨~~~a.toBitVec⟩⟩
 

src/include/lean/lean.h

@@ -1954,16 +1954,16 @@ static inline uint8_t lean_int8_xor(uint8_t a1, uint8_t a2) {
 
 static inline uint8_t lean_int8_shift_right(uint8_t a1, uint8_t a2) {
     int8_t lhs = (int8_t)a1;
-    int8_t rhs = (int8_t)a2;
+    int8_t rhs = (((int8_t)a2 % 8) + 8) % 8; // this is smod 8
 
-    return (uint8_t)(lhs >> (rhs % 8));
+    return (uint8_t)(lhs >> rhs);
 }
 
 static inline uint8_t lean_int8_shift_left(uint8_t a1, uint8_t a2) {
     int8_t lhs = (int8_t)a1;
-    int8_t rhs = (int8_t)a2;
+    int8_t rhs = (((int8_t)a2 % 8) + 8) % 8; // this is smod 8
 
-    return (uint8_t)(lhs << (rhs % 8));
+    return (uint8_t)(lhs << rhs);
 }
 
 static inline uint8_t lean_int8_complement(uint8_t a) {
@@ -2094,16 +2094,16 @@ static inline uint16_t lean_int16_xor(uint16_t a1, uint16_t a2) {
 
 static inline uint16_t lean_int16_shift_right(uint16_t a1, uint16_t a2) {
     int16_t lhs = (int16_t)a1;
-    int16_t rhs = (int16_t)a2;
+    int16_t rhs = (((int16_t)a2 % 16) + 16) % 16; // this is smod 16
 
-    return (uint16_t)(lhs >> (rhs % 16));
+    return (uint16_t)(lhs >> rhs);
 }
 
 static inline uint16_t lean_int16_shift_left(uint16_t a1, uint16_t a2) {
     int16_t lhs = (int16_t)a1;
-    int16_t rhs = (int16_t)a2;
+    int16_t rhs = (((int16_t)a2 % 16) + 16) % 16; // this is smod 16
 
-    return (uint16_t)(lhs << (rhs % 16));
+    return (uint16_t)(lhs << rhs);
 }
 
 static inline uint16_t lean_int16_complement(uint16_t a) {
@@ -2233,16 +2233,16 @@ static inline uint32_t lean_int32_xor(uint32_t a1, uint32_t a2) {
 
 static inline uint32_t lean_int32_shift_right(uint32_t a1, uint32_t a2) {
     int32_t lhs = (int32_t)a1;
-    int32_t rhs = (int32_t)a2;
+    int32_t rhs = (((int32_t)a2 % 32) + 32) % 32; // this is smod 32
 
-    return (uint32_t)(lhs >> (rhs % 32));
+    return (uint32_t)(lhs >> rhs);
 }
 
 static inline uint32_t lean_int32_shift_left(uint32_t a1, uint32_t a2) {
     int32_t lhs = (int32_t)a1;
-    int32_t rhs = (int32_t)a2;
+    int32_t rhs = (((int32_t)a2 % 32) + 32) % 32; // this is smod 32
 
-    return (uint32_t)(lhs << (rhs % 32));
+    return (uint32_t)(lhs << rhs);
 }
 
 static inline uint32_t lean_int32_complement(uint32_t a) {
@@ -2372,16 +2372,16 @@ static inline uint64_t lean_int64_xor(uint64_t a1, uint64_t a2) {
 
 static inline uint64_t lean_int64_shift_right(uint64_t a1, uint64_t a2) {
     int64_t lhs = (int64_t)a1;
-    int64_t rhs = (int64_t)a2;
+    int64_t rhs = (((int64_t)a2 % 64) + 64) % 64; // this is smod 64
 
-    return (uint64_t)(lhs >> (rhs % 64));
+    return (uint64_t)(lhs >> rhs);
 }
 
 static inline uint64_t lean_int64_shift_left(uint64_t a1, uint64_t a2) {
     int64_t lhs = (int64_t)a1;
-    int64_t rhs = (int64_t)a2;
+    int64_t rhs = (((int64_t)a2 % 64) + 64) % 64; // this is smod 64
 
-    return (uint64_t)(lhs << (rhs % 64));
+    return (uint64_t)(lhs << rhs);
 }
 
 static inline uint64_t lean_int64_complement(uint64_t a) {