Skip to content

Commit cdb6bb0

Browse files
mkannwischermkannwischer
committed
Resolve -Wconversion and -Wsign-conversion warnings
This commit enables additional warnings (-Wconversion, -Wsign-conversions) requiring more explicit casts. All of those casts should already be safe as checked by CBMC. Resolves #543 Signed-off-by: Matthias J. Kannwischer <[email protected]>
1 parent 447afbe commit cdb6bb0

File tree

23 files changed

+238
-200
lines changed

23 files changed

+238
-200
lines changed

‎examples/basic/Makefile‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,8 @@ CFLAGS := \
5959
-Werror \
6060
-Wpointer-arith \
6161
-Wredundant-decls \
62+
-Wconversion \
63+
-Wsign-conversion \
6264
-Wno-long-long \
6365
-Wno-unknown-pragmas \
6466
-Wno-unused-command-line-argument \

‎mldsa/fips202/fips202.c‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -94,9 +94,12 @@ __contract__(
9494
mld_keccakf1600_permute(s);
9595
pos = 0;
9696
}
97-
mld_keccakf1600_xor_bytes(s, in, pos, inlen);
97+
/* Safety: At this point, inlen < r, so the truncation to unsigned is safe. */
98+
mld_keccakf1600_xor_bytes(s, in, pos, (unsigned)inlen);
9899

99-
return pos + inlen;
100+
/* Safety: At this point, inlen < r and pos <= r so the truncation to unsigned
101+
* is safe. */
102+
return (unsigned)(pos + inlen);
100103
}
101104

102105
/*************************************************
@@ -177,7 +180,8 @@ __contract__(
177180
mld_keccakf1600_permute(s);
178181
pos = 0;
179182
}
180-
i = bytes_to_go < r - pos ? bytes_to_go : r - pos;
183+
/* Safety: If bytes_to_go < r - pos, truncation to unsigned is safe. */
184+
i = bytes_to_go < r - pos ? (unsigned)bytes_to_go : r - pos;
181185
mld_keccakf1600_extract_bytes(s, out + out_offset, pos, i);
182186
bytes_to_go -= i;
183187
pos += i;

‎mldsa/fips202/fips202x4.c‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -53,19 +53,21 @@ __contract__(
5353
inlen -= r;
5454
}
5555

56+
/* Safety: At this point, inlen < r, so the truncations to unsigned are safe
57+
* below. */
5658
if (inlen > 0)
5759
{
58-
mld_keccakf1600x4_xor_bytes(s, in0, in1, in2, in3, 0, inlen);
60+
mld_keccakf1600x4_xor_bytes(s, in0, in1, in2, in3, 0, (unsigned)inlen);
5961
}
6062

6163
if (inlen == r - 1)
6264
{
6365
p |= 128;
64-
mld_keccakf1600x4_xor_bytes(s, &p, &p, &p, &p, inlen, 1);
66+
mld_keccakf1600x4_xor_bytes(s, &p, &p, &p, &p, (unsigned)inlen, 1);
6567
}
6668
else
6769
{
68-
mld_keccakf1600x4_xor_bytes(s, &p, &p, &p, &p, inlen, 1);
70+
mld_keccakf1600x4_xor_bytes(s, &p, &p, &p, &p, (unsigned)inlen, 1);
6971
p = 128;
7072
mld_keccakf1600x4_xor_bytes(s, &p, &p, &p, &p, r - 1, 1);
7173
}

‎mldsa/native/aarch64/meta.h‎

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -54,14 +54,16 @@ static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len,
5454
{
5555
return -1;
5656
}
57+
58+
/* Safety: outlen is at most MLDSA_N, hence, this cast is safe. */
5759
return (int)mld_rej_uniform_asm(r, buf, buflen, mld_rej_uniform_table);
5860
}
5961

6062
static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
6163
const uint8_t *buf,
6264
unsigned buflen)
6365
{
64-
int outlen;
66+
unsigned int outlen;
6567
/* AArch64 implementation assumes specific buffer lengths */
6668
if (len != MLDSA_N || buflen != MLD_AARCH64_REJ_UNIFORM_ETA2_BUFLEN)
6769
{
@@ -75,17 +77,17 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
7577
* We declassify prior the input data and mark the outputs as secret.
7678
*/
7779
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
78-
outlen =
79-
(int)mld_rej_uniform_eta2_asm(r, buf, buflen, mld_rej_uniform_eta_table);
80+
outlen = mld_rej_uniform_eta2_asm(r, buf, buflen, mld_rej_uniform_eta_table);
8081
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
81-
return outlen;
82+
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
83+
return (int)outlen;
8284
}
8385

8486
static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
8587
const uint8_t *buf,
8688
unsigned buflen)
8789
{
88-
int outlen;
90+
unsigned int outlen;
8991
/* AArch64 implementation assumes specific buffer lengths */
9092
if (len != MLDSA_N || buflen != MLD_AARCH64_REJ_UNIFORM_ETA4_BUFLEN)
9193
{
@@ -99,10 +101,10 @@ static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
99101
* We declassify prior the input data and mark the outputs as secret.
100102
*/
101103
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
102-
outlen =
103-
(int)mld_rej_uniform_eta4_asm(r, buf, buflen, mld_rej_uniform_eta_table);
104+
outlen = mld_rej_uniform_eta4_asm(r, buf, buflen, mld_rej_uniform_eta_table);
104105
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
105-
return outlen;
106+
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
107+
return (int)outlen;
106108
}
107109

108110
static MLD_INLINE void mld_poly_decompose_32_native(int32_t *a1, int32_t *a0,

‎mldsa/native/aarch64/src/polyz_unpack_table.c‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -14,17 +14,17 @@
1414
/* Table of indices used for tbl instructions in polyz_unpack_{17,19}. */
1515

1616
MLD_ALIGN const uint8_t mld_polyz_unpack_17_indices[] = {
17-
0, 1, 2, -1, 2, 3, 4, -1, 4, 5, 6, -1, 6, 7, 8, -1,
18-
9, 10, 11, -1, 11, 12, 13, -1, 13, 14, 15, -1, 15, 16, 17, -1,
19-
2, 3, 4, -1, 4, 5, 6, -1, 6, 7, 8, -1, 8, 9, 10, -1,
20-
11, 12, 13, -1, 13, 14, 15, -1, 15, 16, 17, -1, 17, 18, 19, -1,
17+
0, 1, 2, 255, 2, 3, 4, 255, 4, 5, 6, 255, 6, 7, 8, 255,
18+
9, 10, 11, 255, 11, 12, 13, 255, 13, 14, 15, 255, 15, 16, 17, 255,
19+
2, 3, 4, 255, 4, 5, 6, 255, 6, 7, 8, 255, 8, 9, 10, 255,
20+
11, 12, 13, 255, 13, 14, 15, 255, 15, 16, 17, 255, 17, 18, 19, 255,
2121
};
2222

2323
MLD_ALIGN const uint8_t mld_polyz_unpack_19_indices[] = {
24-
0, 1, 2, -1, 2, 3, 4, -1, 5, 6, 7, -1, 7, 8, 9, -1,
25-
10, 11, 12, -1, 12, 13, 14, -1, 15, 16, 17, -1, 17, 18, 19, -1,
26-
4, 5, 6, -1, 6, 7, 8, -1, 9, 10, 11, -1, 11, 12, 13, -1,
27-
14, 15, 16, -1, 16, 17, 18, -1, 19, 20, 21, -1, 21, 22, 23, -1,
24+
0, 1, 2, 255, 2, 3, 4, 255, 5, 6, 7, 255, 7, 8, 9, 255,
25+
10, 11, 12, 255, 12, 13, 14, 255, 15, 16, 17, 255, 17, 18, 19, 255,
26+
4, 5, 6, 255, 6, 7, 8, 255, 9, 10, 11, 255, 11, 12, 13, 255,
27+
14, 15, 16, 255, 16, 17, 18, 255, 19, 20, 21, 255, 21, 22, 23, 255,
2828
};
2929

3030
#else /* MLD_ARITH_BACKEND_AARCH64 && !MLD_CONFIG_MULTILEVEL_NO_SHARED */

‎mldsa/native/x86_64/meta.h‎

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -59,14 +59,15 @@ static MLD_INLINE int mld_rej_uniform_native(int32_t *r, unsigned len,
5959
return -1;
6060
}
6161

62+
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
6263
return (int)mld_rej_uniform_avx2(r, buf);
6364
}
6465

6566
static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
6667
const uint8_t *buf,
6768
unsigned buflen)
6869
{
69-
int outlen;
70+
unsigned int outlen;
7071
/* AVX2 implementation assumes specific buffer lengths */
7172
if (len != MLDSA_N || buflen != MLD_AVX2_REJ_UNIFORM_ETA2_BUFLEN)
7273
{
@@ -81,16 +82,17 @@ static MLD_INLINE int mld_rej_uniform_eta2_native(int32_t *r, unsigned len,
8182
* We declassify prior the input data and mark the outputs as secret.
8283
*/
8384
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
84-
outlen = (int)mld_rej_uniform_eta2_avx2(r, buf);
85+
outlen = mld_rej_uniform_eta2_avx2(r, buf);
8586
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
86-
return outlen;
87+
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
88+
return (int)outlen;
8789
}
8890

8991
static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
9092
const uint8_t *buf,
9193
unsigned buflen)
9294
{
93-
int outlen;
95+
unsigned int outlen;
9496
/* AVX2 implementation assumes specific buffer lengths */
9597
if (len != MLDSA_N || buflen != MLD_AVX2_REJ_UNIFORM_ETA4_BUFLEN)
9698
{
@@ -105,9 +107,10 @@ static MLD_INLINE int mld_rej_uniform_eta4_native(int32_t *r, unsigned len,
105107
* We declassify prior the input data and mark the outputs as secret.
106108
*/
107109
MLD_CT_TESTING_DECLASSIFY(buf, buflen);
108-
outlen = (int)mld_rej_uniform_eta4_avx2(r, buf);
110+
outlen = mld_rej_uniform_eta4_avx2(r, buf);
109111
MLD_CT_TESTING_SECRET(r, sizeof(int32_t) * outlen);
110-
return outlen;
112+
/* Safety: outlen is at most MLDSA_N and, hence, this cast is safe. */
113+
return (int)outlen;
111114
}
112115

113116
static MLD_INLINE void mld_poly_decompose_32_native(int32_t *a1, int32_t *a0,

‎mldsa/native/x86_64/src/poly_chknorm_avx2.c‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ uint32_t mld_poly_chknorm_avx2(const __m256i *a, int32_t B)
4141
t = _mm256_or_si256(t, f);
4242
}
4343

44-
return _mm256_testz_si256(t, t) - 1;
44+
return (uint32_t)(_mm256_testz_si256(t, t) - 1);
4545
}
4646

4747
#else /* MLD_ARITH_BACKEND_X86_64_DEFAULT && !MLD_CONFIG_MULTILEVEL_NO_SHARED \

‎mldsa/native/x86_64/src/rej_uniform_avx2.c‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -93,13 +93,13 @@ unsigned int mld_rej_uniform_avx2(
9393
pos += 24;
9494

9595
tmp = _mm256_sub_epi32(d, bound);
96-
good = _mm256_movemask_ps((__m256)tmp);
96+
good = (uint32_t)_mm256_movemask_ps((__m256)tmp);
9797
tmp = _mm256_cvtepu8_epi32(
9898
_mm_loadl_epi64((__m128i *)&mld_rej_uniform_table[good]));
9999
d = _mm256_permutevar8x32_epi32(d, tmp);
100100

101101
_mm256_storeu_si256((__m256i *)&r[ctr], d);
102-
ctr += _mm_popcnt_u32(good);
102+
ctr += (unsigned)_mm_popcnt_u32(good);
103103
}
104104

105105
while (ctr < MLDSA_N && pos <= MLD_AVX2_REJ_UNIFORM_BUFLEN - 3)
@@ -111,7 +111,8 @@ unsigned int mld_rej_uniform_avx2(
111111

112112
if (t < MLDSA_Q)
113113
{
114-
r[ctr++] = t;
114+
/* Safe because t < MLDSA_Q. */
115+
r[ctr++] = (int32_t)t;
115116
}
116117
}
117118

‎mldsa/native/x86_64/src/rej_uniform_eta2_avx2.c‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ unsigned int mld_rej_uniform_eta2_avx2(
6060

6161
f1 = _mm256_sub_epi8(f0, bound);
6262
f0 = _mm256_sub_epi8(eta, f0);
63-
good = _mm256_movemask_epi8(f1);
63+
good = (uint32_t)_mm256_movemask_epi8(f1);
6464

6565
g0 = _mm256_castsi256_si128(f0);
6666
g1 = _mm_loadl_epi64((__m128i *)&mld_rej_uniform_table[good & 0xFF]);
@@ -70,7 +70,7 @@ unsigned int mld_rej_uniform_eta2_avx2(
7070
f2 = _mm256_mullo_epi16(f2, p);
7171
f1 = _mm256_add_epi32(f1, f2);
7272
_mm256_storeu_si256((__m256i *)&r[ctr], f1);
73-
ctr += _mm_popcnt_u32(good & 0xFF);
73+
ctr += (unsigned)_mm_popcnt_u32(good & 0xFF);
7474
good >>= 8;
7575
pos += 4;
7676

@@ -86,7 +86,7 @@ unsigned int mld_rej_uniform_eta2_avx2(
8686
f2 = _mm256_mullo_epi16(f2, p);
8787
f1 = _mm256_add_epi32(f1, f2);
8888
_mm256_storeu_si256((__m256i *)&r[ctr], f1);
89-
ctr += _mm_popcnt_u32(good & 0xFF);
89+
ctr += (unsigned)_mm_popcnt_u32(good & 0xFF);
9090
good >>= 8;
9191
pos += 4;
9292

@@ -102,7 +102,7 @@ unsigned int mld_rej_uniform_eta2_avx2(
102102
f2 = _mm256_mullo_epi16(f2, p);
103103
f1 = _mm256_add_epi32(f1, f2);
104104
_mm256_storeu_si256((__m256i *)&r[ctr], f1);
105-
ctr += _mm_popcnt_u32(good & 0xFF);
105+
ctr += (unsigned)_mm_popcnt_u32(good & 0xFF);
106106
good >>= 8;
107107
pos += 4;
108108

@@ -118,7 +118,7 @@ unsigned int mld_rej_uniform_eta2_avx2(
118118
f2 = _mm256_mullo_epi16(f2, p);
119119
f1 = _mm256_add_epi32(f1, f2);
120120
_mm256_storeu_si256((__m256i *)&r[ctr], f1);
121-
ctr += _mm_popcnt_u32(good);
121+
ctr += (unsigned)_mm_popcnt_u32(good);
122122
pos += 4;
123123
}
124124

@@ -130,12 +130,12 @@ unsigned int mld_rej_uniform_eta2_avx2(
130130
if (t0 < 15)
131131
{
132132
t0 = t0 - (205 * t0 >> 10) * 5;
133-
r[ctr++] = 2 - t0;
133+
r[ctr++] = (int32_t)(2 - t0);
134134
}
135135
if (t1 < 15 && ctr < MLDSA_N)
136136
{
137137
t1 = t1 - (205 * t1 >> 10) * 5;
138-
r[ctr++] = 2 - t1;
138+
r[ctr++] = (int32_t)(2 - t1);
139139
}
140140
}
141141

‎mldsa/native/x86_64/src/rej_uniform_eta4_avx2.c‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -58,14 +58,14 @@ unsigned int mld_rej_uniform_eta4_avx2(
5858

5959
f1 = _mm256_sub_epi8(f0, bound);
6060
f0 = _mm256_sub_epi8(eta, f0);
61-
good = _mm256_movemask_epi8(f1);
61+
good = (uint32_t)_mm256_movemask_epi8(f1);
6262

6363
g0 = _mm256_castsi256_si128(f0);
6464
g1 = _mm_loadl_epi64((__m128i *)&mld_rej_uniform_table[good & 0xFF]);
6565
g1 = _mm_shuffle_epi8(g0, g1);
6666
f1 = _mm256_cvtepi8_epi32(g1);
6767
_mm256_storeu_si256((__m256i *)&r[ctr], f1);
68-
ctr += _mm_popcnt_u32(good & 0xFF);
68+
ctr += (unsigned)_mm_popcnt_u32(good & 0xFF);
6969
good >>= 8;
7070
pos += 4;
7171

@@ -78,7 +78,7 @@ unsigned int mld_rej_uniform_eta4_avx2(
7878
g1 = _mm_shuffle_epi8(g0, g1);
7979
f1 = _mm256_cvtepi8_epi32(g1);
8080
_mm256_storeu_si256((__m256i *)&r[ctr], f1);
81-
ctr += _mm_popcnt_u32(good & 0xFF);
81+
ctr += (unsigned)_mm_popcnt_u32(good & 0xFF);
8282
good >>= 8;
8383
pos += 4;
8484

@@ -91,7 +91,7 @@ unsigned int mld_rej_uniform_eta4_avx2(
9191
g1 = _mm_shuffle_epi8(g0, g1);
9292
f1 = _mm256_cvtepi8_epi32(g1);
9393
_mm256_storeu_si256((__m256i *)&r[ctr], f1);
94-
ctr += _mm_popcnt_u32(good & 0xFF);
94+
ctr += (unsigned)_mm_popcnt_u32(good & 0xFF);
9595
good >>= 8;
9696
pos += 4;
9797

@@ -104,7 +104,7 @@ unsigned int mld_rej_uniform_eta4_avx2(
104104
g1 = _mm_shuffle_epi8(g0, g1);
105105
f1 = _mm256_cvtepi8_epi32(g1);
106106
_mm256_storeu_si256((__m256i *)&r[ctr], f1);
107-
ctr += _mm_popcnt_u32(good);
107+
ctr += (unsigned)_mm_popcnt_u32(good);
108108
pos += 4;
109109
}
110110

@@ -115,11 +115,11 @@ unsigned int mld_rej_uniform_eta4_avx2(
115115

116116
if (t0 < 9)
117117
{
118-
r[ctr++] = 4 - t0;
118+
r[ctr++] = (int32_t)(4 - t0);
119119
}
120120
if (t1 < 9 && ctr < MLDSA_N)
121121
{
122-
r[ctr++] = 4 - t1;
122+
r[ctr++] = (int32_t)(4 - t1);
123123
}
124124
}
125125

0 commit comments

Comments
 (0)