Merge pull request #552 from pq-code-package/wconversion

Resolve -Wconversion and -Wsign-conversion warnings

Author: mkannwischer

examples/basic/Makefile

@@ -59,6 +59,8 @@ CFLAGS := \
 	-Werror \
 	-Wpointer-arith \
 	-Wredundant-decls \
+	-Wconversion \
+	-Wsign-conversion \
 	-Wno-long-long \
 	-Wno-unknown-pragmas \
 	-Wno-unused-command-line-argument \

mldsa/ct.h

@@ -111,18 +111,67 @@ __contract__(ensures(return_value == b))
 }
 #endif /* MLD_USE_ASM_VALUE_BARRIER */
 
-
-/*
- * The mld_ct_sel_int32 function below makes deliberate use of unsigned
- * to signed integer conversion, which is implementation-defined
- * behaviour. Here, we assume that uint16_t -> int16_t is inverse
- * to int16_t -> uint16_t.
- */
 #ifdef CBMC
 #pragma CPROVER check push
 #pragma CPROVER check disable "conversion"
 #endif
 
+/*************************************************
+ * Name:        mld_cast_uint32_to_int32
+ *
+ * Description: Cast uint32 value to int32
+ *
+ * Returns:     For uint32_t x, the unique y in int32_t
+ *              so that x == y mod 2^32.
+ *
+ *              Concretely:
+ *              - x <  2^31: returns x
+ *              - x >= 2^31: returns x - 2^31
+ *
+ **************************************************/
+static MLD_ALWAYS_INLINE int32_t mld_cast_uint32_to_int32(uint32_t x)
+{
+  /*
+   * PORTABILITY: This relies on uint32_t -> int32_t
+   * being implemented as the inverse of int32_t -> uint32_t,
+   * which is implementation-defined (C99 6.3.1.3 (3))
+   * CBMC (correctly) fails to prove this conversion is OK,
+   * so we have to suppress that check here
+   */
+  return (int32_t)x;
+}
+
+#ifdef CBMC
+#pragma CPROVER check pop
+#endif
+
+
+/*************************************************
+ * Name:        mld_cast_int64_to_uint32
+ *
+ * Description: Cast int64 value to uint32 as per C standard.
+ *
+ * Returns:     For int64_t x, the unique y in uint32_t
+ *              so that x == y mod 2^32.
+ **************************************************/
+static MLD_ALWAYS_INLINE uint32_t mld_cast_int64_to_uint32(int64_t x)
+{
+  return (uint32_t)(x & (int64_t)UINT32_MAX);
+}
+
+/*************************************************
+ * Name:        mld_cast_int32_to_uint32
+ *
+ * Description: Cast int32 value to uint32 as per C standard.
+ *
+ * Returns:     For int32_t x, the unique y in uint32_t
+ *              so that x == y mod 2^32.
+ **************************************************/
+static MLD_ALWAYS_INLINE uint32_t mld_cast_int32_to_uint32(int32_t x)
+{
+  return mld_cast_int64_to_uint32((int64_t)x);
+}
+
 /*************************************************
  * Name:        mld_ct_sel_int32
  *
@@ -137,35 +186,17 @@ __contract__(ensures(return_value == b))
  *
  **************************************************/
 static MLD_INLINE int32_t mld_ct_sel_int32(int32_t a, int32_t b, uint32_t cond)
-/* TODO: proof */
 __contract__(
   requires(cond == 0x0 || cond == 0xFFFFFFFF)
   ensures(return_value == (cond ? a : b))
 )
 {
-  uint32_t au = a, bu = b;
+  uint32_t au = mld_cast_int32_to_uint32(a);
+  uint32_t bu = mld_cast_int32_to_uint32(b);
   uint32_t res = bu ^ (mld_value_barrier_u32(cond) & (au ^ bu));
-  return (int32_t)res;
+  return mld_cast_uint32_to_int32(res);
 }
 
-/* Put unsigned-to-signed warnings in CBMC back into scope */
-#ifdef CBMC
-#pragma CPROVER check pop
-#endif
-
-
-
-/*
- * The mld_ct_cmask_neg_i32 function below makes deliberate use of
- * signed to unsigned integer conversion, which is fully defined
- * behaviour in C. It is thus safe to disable this warning.
- */
-#ifdef CBMC
-#pragma CPROVER check push
-#pragma CPROVER check disable "conversion"
-#endif
-
-
 /*************************************************
  * Name:        mld_ct_cmask_neg_i32
  *
@@ -174,22 +205,16 @@ __contract__(
  * Arguments:   int32_t x: Value to be converted into a mask
  *
  **************************************************/
-/* TODO: proof */
 static MLD_INLINE uint32_t mld_ct_cmask_neg_i32(int32_t x)
 __contract__(
   ensures(return_value == ((x < 0) ? 0xFFFFFFFF : 0))
 )
 {
   int64_t tmp = mld_value_barrier_i64((int64_t)x);
   tmp >>= 31;
-  return (uint32_t)tmp;
+  return mld_cast_int64_to_uint32(tmp);
 }
 
-/* Put signed-to-unsigned warnings in CBMC back into scope */
-#ifdef CBMC
-#pragma CPROVER check pop
-#endif
-
 /*************************************************
  * Name:        mld_ct_abs_i32
  *
@@ -198,7 +223,6 @@ __contract__(
  * Arguments:   int32_t x: Input value
  *
  **************************************************/
-/* TODO: proof */
 static MLD_INLINE int32_t mld_ct_abs_i32(int32_t x)
 __contract__(
   requires(x >= -INT32_MAX)

mldsa/fips202/fips202.c

@@ -94,9 +94,12 @@ __contract__(
     mld_keccakf1600_permute(s);
     pos = 0;
   }
-  mld_keccakf1600_xor_bytes(s, in, pos, inlen);
+  /* Safety: At this point, inlen < r, so the truncation to unsigned is safe. */
+  mld_keccakf1600_xor_bytes(s, in, pos, (unsigned)inlen);
 
-  return pos + inlen;
+  /* Safety: At this point, inlen < r and pos <= r so the truncation to unsigned
+   * is safe. */
+  return (unsigned)(pos + inlen);
 }
 
 /*************************************************
@@ -177,7 +180,8 @@ __contract__(
       mld_keccakf1600_permute(s);
       pos = 0;
     }
-    i = bytes_to_go < r - pos ? bytes_to_go : r - pos;
+    /* Safety: If bytes_to_go < r - pos, truncation to unsigned is safe. */
+    i = bytes_to_go < r - pos ? (unsigned)bytes_to_go : r - pos;
     mld_keccakf1600_extract_bytes(s, out + out_offset, pos, i);
     bytes_to_go -= i;
     pos += i;

mldsa/fips202/fips202x4.c

@@ -53,19 +53,21 @@ __contract__(
     inlen -= r;
   }
 
+  /* Safety: At this point, inlen < r, so the truncations to unsigned are safe
+   * below. */
   if (inlen > 0)
   {
-    mld_keccakf1600x4_xor_bytes(s, in0, in1, in2, in3, 0, inlen);
+    mld_keccakf1600x4_xor_bytes(s, in0, in1, in2, in3, 0, (unsigned)inlen);
   }
 
   if (inlen == r - 1)
   {
     p |= 128;
-    mld_keccakf1600x4_xor_bytes(s, &p, &p, &p, &p, inlen, 1);
+    mld_keccakf1600x4_xor_bytes(s, &p, &p, &p, &p, (unsigned)inlen, 1);
   }
   else
   {
-    mld_keccakf1600x4_xor_bytes(s, &p, &p, &p, &p, inlen, 1);
+    mld_keccakf1600x4_xor_bytes(s, &p, &p, &p, &p, (unsigned)inlen, 1);
     p = 128;
     mld_keccakf1600x4_xor_bytes(s, &p, &p, &p, &p, r - 1, 1);
   }

mldsa/native/aarch64/meta.h

@@ -54,14 +54,16 @@ static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len,
   {
     return -1;
   }
+
+  /* Safety: outlen is at most MLDSA_N, hence, this cast is safe. */
   return (int)mld_rej_uniform_asm(r, buf, buflen, mld_rej_uniform_table);
 }
 
 static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
                                                   const uint8_t *buf,
                                                   unsigned buflen)
 {
-  int outlen;
+  unsigned int outlen;
   /* AArch64 implementation assumes specific buffer lengths */
   if (len != MLDSA_N || buflen != MLD_AARCH64_REJ_UNIFORM_ETA2_BUFLEN)
   {
@@ -75,17 +77,17 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
    * We declassify prior the input data and mark the outputs as secret.
    */
   MLD_CT_TESTING_DECLASSIFY(buf, buflen);
-  outlen =
-      (int)mld_rej_uniform_eta2_asm(r, buf, buflen, mld_rej_uniform_eta_table);
+  outlen = mld_rej_uniform_eta2_asm(r, buf, buflen, mld_rej_uniform_eta_table);
   MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
-  return outlen;
+  /* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
+  return (int)outlen;
 }
 
 static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
                                                   const uint8_t *buf,
                                                   unsigned buflen)
 {
-  int outlen;
+  unsigned int outlen;
   /* AArch64 implementation assumes specific buffer lengths */
   if (len != MLDSA_N || buflen != MLD_AARCH64_REJ_UNIFORM_ETA4_BUFLEN)
   {
@@ -99,10 +101,10 @@ static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
    * We declassify prior the input data and mark the outputs as secret.
    */
   MLD_CT_TESTING_DECLASSIFY(buf, buflen);
-  outlen =
-      (int)mld_rej_uniform_eta4_asm(r, buf, buflen, mld_rej_uniform_eta_table);
+  outlen = mld_rej_uniform_eta4_asm(r, buf, buflen, mld_rej_uniform_eta_table);
   MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
-  return outlen;
+  /* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
+  return (int)outlen;
 }
 
 static MLD_INLINE void mld_poly_decompose_32_native(int32_t *a1, int32_t *a0,

mldsa/native/aarch64/src/polyz_unpack_table.c

@@ -14,17 +14,17 @@
 /* Table of indices used for tbl instructions in polyz_unpack_{17,19}. */
 
 MLD_ALIGN const uint8_t mld_polyz_unpack_17_indices[] = {
-    0,  1,  2,  -1, 2,  3,  4,  -1, 4,  5,  6,  -1, 6,  7,  8,  -1,
-    9,  10, 11, -1, 11, 12, 13, -1, 13, 14, 15, -1, 15, 16, 17, -1,
-    2,  3,  4,  -1, 4,  5,  6,  -1, 6,  7,  8,  -1, 8,  9,  10, -1,
-    11, 12, 13, -1, 13, 14, 15, -1, 15, 16, 17, -1, 17, 18, 19, -1,
+    0,  1,  2,  255, 2,  3,  4,  255, 4,  5,  6,  255, 6,  7,  8,  255,
+    9,  10, 11, 255, 11, 12, 13, 255, 13, 14, 15, 255, 15, 16, 17, 255,
+    2,  3,  4,  255, 4,  5,  6,  255, 6,  7,  8,  255, 8,  9,  10, 255,
+    11, 12, 13, 255, 13, 14, 15, 255, 15, 16, 17, 255, 17, 18, 19, 255,
 };
 
 MLD_ALIGN const uint8_t mld_polyz_unpack_19_indices[] = {
-    0,  1,  2,  -1, 2,  3,  4,  -1, 5,  6,  7,  -1, 7,  8,  9,  -1,
-    10, 11, 12, -1, 12, 13, 14, -1, 15, 16, 17, -1, 17, 18, 19, -1,
-    4,  5,  6,  -1, 6,  7,  8,  -1, 9,  10, 11, -1, 11, 12, 13, -1,
-    14, 15, 16, -1, 16, 17, 18, -1, 19, 20, 21, -1, 21, 22, 23, -1,
+    0,  1,  2,  255, 2,  3,  4,  255, 5,  6,  7,  255, 7,  8,  9,  255,
+    10, 11, 12, 255, 12, 13, 14, 255, 15, 16, 17, 255, 17, 18, 19, 255,
+    4,  5,  6,  255, 6,  7,  8,  255, 9,  10, 11, 255, 11, 12, 13, 255,
+    14, 15, 16, 255, 16, 17, 18, 255, 19, 20, 21, 255, 21, 22, 23, 255,
 };
 
 #else /* MLD_ARITH_BACKEND_AARCH64 && !MLD_CONFIG_MULTILEVEL_NO_SHARED */

mldsa/native/x86_64/meta.h

@@ -59,14 +59,15 @@ static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len,
     return -1;
   }
 
+  /* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
   return (int)mld_rej_uniform_avx2(r, buf);
 }
 
 static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
                                                   const uint8_t *buf,
                                                   unsigned buflen)
 {
-  int outlen;
+  unsigned int outlen;
   /* AVX2 implementation assumes specific buffer lengths */
   if (len != MLDSA_N || buflen != MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN)
   {
@@ -81,16 +82,17 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
    * We declassify prior the input data and mark the outputs as secret.
    */
   MLD_CT_TESTING_DECLASSIFY(buf, buflen);
-  outlen = (int)mld_rej_uniform_eta2_avx2(r, buf);
+  outlen = mld_rej_uniform_eta2_avx2(r, buf);
   MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
-  return outlen;
+  /* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
+  return (int)outlen;
 }
 
 static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
                                                   const uint8_t *buf,
                                                   unsigned buflen)
 {
-  int outlen;
+  unsigned int outlen;
   /* AVX2 implementation assumes specific buffer lengths */
   if (len != MLDSA_N || buflen != MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN)
   {
@@ -105,9 +107,10 @@ static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
    * We declassify prior the input data and mark the outputs as secret.
    */
   MLD_CT_TESTING_DECLASSIFY(buf, buflen);
-  outlen = (int)mld_rej_uniform_eta4_avx2(r, buf);
+  outlen = mld_rej_uniform_eta4_avx2(r, buf);
   MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
-  return outlen;
+  /* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
+  return (int)outlen;
 }
 
 static MLD_INLINE void mld_poly_decompose_32_native(int32_t *a1, int32_t *a0,

mldsa/native/x86_64/src/poly_chknorm_avx2.c

@@ -41,7 +41,7 @@ uint32_t mld_poly_chknorm_avx2(const __m256i *a, int32_t B)
     t = _mm256_or_si256(t, f);
   }
 
-  return _mm256_testz_si256(t, t) - 1;
+  return (uint32_t)(_mm256_testz_si256(t, t) - 1);
 }
 
 #else /* MLD_ARITH_BACKEND_X86_64_DEFAULT && !MLD_CONFIG_MULTILEVEL_NO_SHARED \

mldsa/native/x86_64/src/rej_uniform_avx2.c

@@ -93,13 +93,13 @@ unsigned int mld_rej_uniform_avx2(
     pos += 24;
 
     tmp = _mm256_sub_epi32(d, bound);
-    good = _mm256_movemask_ps((__m256)tmp);
+    good = (uint32_t)_mm256_movemask_ps((__m256)tmp);
     tmp = _mm256_cvtepu8_epi32(
         _mm_loadl_epi64((__m128i *)&mld_rej_uniform_table[good]));
     d = _mm256_permutevar8x32_epi32(d, tmp);
 
     _mm256_storeu_si256((__m256i *)&r[ctr], d);
-    ctr += _mm_popcnt_u32(good);
+    ctr += (unsigned)_mm_popcnt_u32(good);
   }
 
   while (ctr < MLDSA_N && pos <= MLD_AVX2_REJ_UNIFORM_BUFLEN - 3)
@@ -111,7 +111,8 @@ unsigned int mld_rej_uniform_avx2(
 
     if (t < MLDSA_Q)
     {
-      r[ctr++] = t;
+      /* Safe because t < MLDSA_Q. */
+      r[ctr++] = (int32_t)t;
     }
   }