Don't cast signed to unsigned before shifting

curve25519_32.c

@@ -39,7 +39,7 @@ static void fiat_25519_addcarryx_u26(uint32_t* out1, fiat_25519_uint1* out2, fia
  */
 static void fiat_25519_subborrowx_u26(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) {
   int32_t x1 = ((int32_t)(arg2 - arg1) - (int32_t)arg3);
-  fiat_25519_int1 x2 = (fiat_25519_int1)((uint32_t)x1 >> 26);
+  fiat_25519_int1 x2 = (fiat_25519_int1)(x1 >> 26);
   uint32_t x3 = (x1 & UINT32_C(0x3ffffff));
   *out1 = x3;
   *out2 = (fiat_25519_uint1)(0x0 - x2);
@@ -73,7 +73,7 @@ static void fiat_25519_addcarryx_u25(uint32_t* out1, fiat_25519_uint1* out2, fia
  */
 static void fiat_25519_subborrowx_u25(uint32_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) {
   int32_t x1 = ((int32_t)(arg2 - arg1) - (int32_t)arg3);
-  fiat_25519_int1 x2 = (fiat_25519_int1)((uint32_t)x1 >> 25);
+  fiat_25519_int1 x2 = (fiat_25519_int1)(x1 >> 25);
   uint32_t x3 = (x1 & UINT32_C(0x1ffffff));
   *out1 = x3;
   *out2 = (fiat_25519_uint1)(0x0 - x2);

curve25519_64.c

@@ -41,7 +41,7 @@ static void fiat_25519_addcarryx_u51(uint64_t* out1, fiat_25519_uint1* out2, fia
  */
 static void fiat_25519_subborrowx_u51(uint64_t* out1, fiat_25519_uint1* out2, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) {
   int64_t x1 = ((int64_t)(arg2 - (int64_t)arg1) - (int64_t)arg3);
-  fiat_25519_int1 x2 = (fiat_25519_int1)((uint64_t)x1 >> 51);
+  fiat_25519_int1 x2 = (fiat_25519_int1)(x1 >> 51);
   uint64_t x3 = (x1 & UINT64_C(0x7ffffffffffff));
   *out1 = x3;
   *out2 = (fiat_25519_uint1)(0x0 - x2);

p224_32.c

@@ -44,7 +44,7 @@ static void fiat_p224_addcarryx_u32(uint32_t* out1, fiat_p224_uint1* out2, fiat_
  */
 static void fiat_p224_subborrowx_u32(uint32_t* out1, fiat_p224_uint1* out2, fiat_p224_uint1 arg1, uint32_t arg2, uint32_t arg3) {
   int64_t x1 = ((arg2 - (int64_t)arg1) - arg3);
-  fiat_p224_int1 x2 = (fiat_p224_int1)((uint64_t)x1 >> 32);
+  fiat_p224_int1 x2 = (fiat_p224_int1)(x1 >> 32);
   uint32_t x3 = (uint32_t)(x1 & UINT32_C(0xffffffff));
   *out1 = x3;
   *out2 = (fiat_p224_uint1)(0x0 - x2);

p224_64.c

@@ -46,7 +46,7 @@ static void fiat_p224_addcarryx_u64(uint64_t* out1, fiat_p224_uint1* out2, fiat_
  */
 static void fiat_p224_subborrowx_u64(uint64_t* out1, fiat_p224_uint1* out2, fiat_p224_uint1 arg1, uint64_t arg2, uint64_t arg3) {
   fiat_p224_int128 x1 = ((arg2 - (fiat_p224_int128)arg1) - arg3);
-  fiat_p224_int1 x2 = (fiat_p224_int1)((fiat_p224_uint128)x1 >> 64);
+  fiat_p224_int1 x2 = (fiat_p224_int1)(x1 >> 64);
   uint64_t x3 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff));
   *out1 = x3;
   *out2 = (fiat_p224_uint1)(0x0 - x2);

p256_32.c

@@ -44,7 +44,7 @@ static void fiat_p256_addcarryx_u32(uint32_t* out1, fiat_p256_uint1* out2, fiat_
  */
 static void fiat_p256_subborrowx_u32(uint32_t* out1, fiat_p256_uint1* out2, fiat_p256_uint1 arg1, uint32_t arg2, uint32_t arg3) {
   int64_t x1 = ((arg2 - (int64_t)arg1) - arg3);
-  fiat_p256_int1 x2 = (fiat_p256_int1)((uint64_t)x1 >> 32);
+  fiat_p256_int1 x2 = (fiat_p256_int1)(x1 >> 32);
   uint32_t x3 = (uint32_t)(x1 & UINT32_C(0xffffffff));
   *out1 = x3;
   *out2 = (fiat_p256_uint1)(0x0 - x2);

p256_64.c

@@ -46,7 +46,7 @@ static void fiat_p256_addcarryx_u64(uint64_t* out1, fiat_p256_uint1* out2, fiat_
  */
 static void fiat_p256_subborrowx_u64(uint64_t* out1, fiat_p256_uint1* out2, fiat_p256_uint1 arg1, uint64_t arg2, uint64_t arg3) {
   fiat_p256_int128 x1 = ((arg2 - (fiat_p256_int128)arg1) - arg3);
-  fiat_p256_int1 x2 = (fiat_p256_int1)((fiat_p256_uint128)x1 >> 64);
+  fiat_p256_int1 x2 = (fiat_p256_int1)(x1 >> 64);
   uint64_t x3 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff));
   *out1 = x3;
   *out2 = (fiat_p256_uint1)(0x0 - x2);

p384_32.c

@@ -44,7 +44,7 @@ static void fiat_p384_addcarryx_u32(uint32_t* out1, fiat_p384_uint1* out2, fiat_
  */
 static void fiat_p384_subborrowx_u32(uint32_t* out1, fiat_p384_uint1* out2, fiat_p384_uint1 arg1, uint32_t arg2, uint32_t arg3) {
   int64_t x1 = ((arg2 - (int64_t)arg1) - arg3);
-  fiat_p384_int1 x2 = (fiat_p384_int1)((uint64_t)x1 >> 32);
+  fiat_p384_int1 x2 = (fiat_p384_int1)(x1 >> 32);
   uint32_t x3 = (uint32_t)(x1 & UINT32_C(0xffffffff));
   *out1 = x3;
   *out2 = (fiat_p384_uint1)(0x0 - x2);

p384_64.c

@@ -46,7 +46,7 @@ static void fiat_p384_addcarryx_u64(uint64_t* out1, fiat_p384_uint1* out2, fiat_
  */
 static void fiat_p384_subborrowx_u64(uint64_t* out1, fiat_p384_uint1* out2, fiat_p384_uint1 arg1, uint64_t arg2, uint64_t arg3) {
   fiat_p384_int128 x1 = ((arg2 - (fiat_p384_int128)arg1) - arg3);
-  fiat_p384_int1 x2 = (fiat_p384_int1)((fiat_p384_uint128)x1 >> 64);
+  fiat_p384_int1 x2 = (fiat_p384_int1)(x1 >> 64);
   uint64_t x3 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff));
   *out1 = x3;
   *out2 = (fiat_p384_uint1)(0x0 - x2);

p484_64.c

@@ -46,7 +46,7 @@ static void fiat_p484_addcarryx_u64(uint64_t* out1, fiat_p484_uint1* out2, fiat_
  */
 static void fiat_p484_subborrowx_u64(uint64_t* out1, fiat_p484_uint1* out2, fiat_p484_uint1 arg1, uint64_t arg2, uint64_t arg3) {
   fiat_p484_int128 x1 = ((arg2 - (fiat_p484_int128)arg1) - arg3);
-  fiat_p484_int1 x2 = (fiat_p484_int1)((fiat_p484_uint128)x1 >> 64);
+  fiat_p484_int1 x2 = (fiat_p484_int1)(x1 >> 64);
   uint64_t x3 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff));
   *out1 = x3;
   *out2 = (fiat_p484_uint1)(0x0 - x2);

p521_32.c

@@ -41,7 +41,7 @@ static void fiat_p521_addcarryx_u30(uint32_t* out1, fiat_p521_uint1* out2, fiat_
  */
 static void fiat_p521_subborrowx_u30(uint32_t* out1, fiat_p521_uint1* out2, fiat_p521_uint1 arg1, uint32_t arg2, uint32_t arg3) {
   int32_t x1 = ((int32_t)(arg2 - arg1) - (int32_t)arg3);
-  fiat_p521_int1 x2 = (fiat_p521_int1)((uint32_t)x1 >> 30);
+  fiat_p521_int1 x2 = (fiat_p521_int1)(x1 >> 30);
   uint32_t x3 = (x1 & UINT32_C(0x3fffffff));
   *out1 = x3;
   *out2 = (fiat_p521_uint1)(0x0 - x2);
@@ -75,7 +75,7 @@ static void fiat_p521_addcarryx_u31(uint32_t* out1, fiat_p521_uint1* out2, fiat_
  */
 static void fiat_p521_subborrowx_u31(uint32_t* out1, fiat_p521_uint1* out2, fiat_p521_uint1 arg1, uint32_t arg2, uint32_t arg3) {
   int32_t x1 = ((int32_t)(arg2 - arg1) - (int32_t)arg3);
-  fiat_p521_int1 x2 = (fiat_p521_int1)((uint32_t)x1 >> 31);
+  fiat_p521_int1 x2 = (fiat_p521_int1)((int64_t)x1 >> 31);
   uint32_t x3 = (x1 & UINT32_C(0x7fffffff));
   *out1 = x3;
   *out2 = (fiat_p521_uint1)(0x0 - x2);

p521_64.c

@@ -41,7 +41,7 @@ static void fiat_p521_addcarryx_u58(uint64_t* out1, fiat_p521_uint1* out2, fiat_
  */
 static void fiat_p521_subborrowx_u58(uint64_t* out1, fiat_p521_uint1* out2, fiat_p521_uint1 arg1, uint64_t arg2, uint64_t arg3) {
   int64_t x1 = ((int64_t)(arg2 - (int64_t)arg1) - (int64_t)arg3);
-  fiat_p521_int1 x2 = (fiat_p521_int1)((uint64_t)x1 >> 58);
+  fiat_p521_int1 x2 = (fiat_p521_int1)(x1 >> 58);
   uint64_t x3 = (x1 & UINT64_C(0x3ffffffffffffff));
   *out1 = x3;
   *out2 = (fiat_p521_uint1)(0x0 - x2);
@@ -75,7 +75,7 @@ static void fiat_p521_addcarryx_u57(uint64_t* out1, fiat_p521_uint1* out2, fiat_
  */
 static void fiat_p521_subborrowx_u57(uint64_t* out1, fiat_p521_uint1* out2, fiat_p521_uint1 arg1, uint64_t arg2, uint64_t arg3) {
   int64_t x1 = ((int64_t)(arg2 - (int64_t)arg1) - (int64_t)arg3);
-  fiat_p521_int1 x2 = (fiat_p521_int1)((uint64_t)x1 >> 57);
+  fiat_p521_int1 x2 = (fiat_p521_int1)(x1 >> 57);
   uint64_t x3 = (x1 & UINT64_C(0x1ffffffffffffff));
   *out1 = x3;
   *out2 = (fiat_p521_uint1)(0x0 - x2);

secp256k1_32.c

@@ -44,7 +44,7 @@ static void fiat_secp256k1_addcarryx_u32(uint32_t* out1, fiat_secp256k1_uint1* o
  */
 static void fiat_secp256k1_subborrowx_u32(uint32_t* out1, fiat_secp256k1_uint1* out2, fiat_secp256k1_uint1 arg1, uint32_t arg2, uint32_t arg3) {
   int64_t x1 = ((arg2 - (int64_t)arg1) - arg3);
-  fiat_secp256k1_int1 x2 = (fiat_secp256k1_int1)((uint64_t)x1 >> 32);
+  fiat_secp256k1_int1 x2 = (fiat_secp256k1_int1)(x1 >> 32);
   uint32_t x3 = (uint32_t)(x1 & UINT32_C(0xffffffff));
   *out1 = x3;
   *out2 = (fiat_secp256k1_uint1)(0x0 - x2);

secp256k1_64.c

@@ -46,7 +46,7 @@ static void fiat_secp256k1_addcarryx_u64(uint64_t* out1, fiat_secp256k1_uint1* o
  */
 static void fiat_secp256k1_subborrowx_u64(uint64_t* out1, fiat_secp256k1_uint1* out2, fiat_secp256k1_uint1 arg1, uint64_t arg2, uint64_t arg3) {
   fiat_secp256k1_int128 x1 = ((arg2 - (fiat_secp256k1_int128)arg1) - arg3);
-  fiat_secp256k1_int1 x2 = (fiat_secp256k1_int1)((fiat_secp256k1_uint128)x1 >> 64);
+  fiat_secp256k1_int1 x2 = (fiat_secp256k1_int1)(x1 >> 64);
   uint64_t x3 = (uint64_t)(x1 & UINT64_C(0xffffffffffffffff));
   *out1 = x3;
   *out2 = (fiat_secp256k1_uint1)(0x0 - x2);

src/CStringification.v

@@ -616,7 +616,7 @@ Module Compilers.
         Definition to_zrange (t : type) : zrange
           := let bw := bitwidth_of t in
              if is_signed t
-             then r[-2^bw ~> 2^(bw-1) - 1]
+             then r[-2^(bw-1) ~> 2^(bw-1) - 1]
              else r[0 ~> 2^bw - 1].
         Definition is_tighter_than (t1 t2 : type)
           := ZRange.is_tighter_than_bool (to_zrange t1) (to_zrange t2).
@@ -646,6 +646,9 @@ Module Compilers.
 
         Definition union (t1 t2 : type) : type := of_zrange_relaxed (ZRange.union (to_zrange t1) (to_zrange t2)).
 
+        Definition union_zrange (r : zrange) (t : type) : type
+          := of_zrange_relaxed (ZRange.union r (to_zrange t)).
+
         Fixpoint base_interp (t : base.type) : Set
           := match t with
              | base.type.Z => type
@@ -1100,8 +1103,12 @@ Module Compilers.
                               behavior to shift >= width of the type.
                               We should probably figure out how to not
                               generate these things in the first
-                              place... *)
-                       let '(e', rin') := Zcast_up_if_needed (Some (int.of_zrange_relaxed r[0~>2^offset]%zrange)) (e, rin) in
+                              place...
+
+                              N.B. We must preserve signedness of the
+                              value being shifted, because shift does
+                              not commute with mod. *)
+                       let '(e', rin') := Zcast_up_if_needed (option_map (int.union_zrange r[0~>2^offset]%zrange) rin) (e, rin) in
                        ret (cast_down_if_needed rout (Z_shiftr offset @@ e', rin'))
                      | None => inr ["Invalid right-shift by a non-literal"]%string
                      end
@@ -1117,11 +1124,15 @@ Module Compilers.
                               behavior to shift >= width of the type.
                               We should probably figure out how to not
                               generate these things in the first
-                              place... *)
-                       let rpre_out := int.of_zrange_relaxed r[0~>2^offset]%zrange in
+                              place...
+
+                              N.B. We make sure that we only
+                              left-shift unsigned values, since
+                              shifting into the sign bit is undefined
+                              behavior. *)
                        let rpre_out := match rout with
-                                       | Some rout => Some (ToString.C.int.union rout rpre_out)
-                                       | None => Some rpre_out
+                                       | Some rout => Some (int.union_zrange r[0~>2^offset] (int.unsigned_counterpart_of rout))
+                                       | None => Some (int.of_zrange_relaxed r[0~>2^offset]%zrange)
                                        end in
                        let '(e', rin') := Zcast_up_if_needed rpre_out (e, rin) in
                        ret (cast_down_if_needed rout (Z_shiftl offset @@ e', rin'))