Remove dead/unreachable code - #11028
Open
danielinux wants to merge 22 commits into
Open
Conversation
Premise: coding.c:127 `if (len == 0) { return BUFFER_E; }` establishes len >= 1
on every path that continues.
Claim: coding.c:137 `if (len && (curChar == '\r' || curChar == '\n'))` --
the `len` operand.
Proof: len is only written between :127 and :137 by the loop at :132,
`while (len > 1 && curChar == ' ') { ...; len--; }`, whose guard
admits the decrement only when len > 1. So the loop preserves
len >= 1, and len >= 1 => the `len` operand is invariantly true.
Its false half, and therefore its MC/DC independence pair, is
unreachable.
Scope: no #if/#ifdef occurs between :120 and :166; the whole function sits
inside one uniform WOLFSSL_BASE64_DECODE block. The argument holds
in every configuration that compiles the function.
Evidence: llvm-cov MC/DC records this condition's pair as uncovered
(reports/coding/GAPS.md row 137:9:137:52:0).
The later `if (len)` at :141/:151 and `while (len && ...)` at :155 stay: the
decrements at :139/:143 can drive len to 0 before those are evaluated.
Compiler cross-check: gcc -O2 emits byte-identical code for this file before
and after this commit -- the optimiser had already folded the removed
condition, independently confirming it was dead.
Premise: coding.c:177 (Base64_Decode_nonCT) and coding.c:298 (Base64_Decode)
both open with
if ((in == NULL && inLen > 0) || out == NULL || outLen == NULL)
return BAD_FUNC_ARG;
which establishes out != NULL for the rest of each function.
Claim: coding.c:281 and coding.c:395, `if (out && *outLen > i)` -- the `out`
operand in both.
Proof: out is a parameter and is never reassigned in either function; the
only uses between the entry check and the null-terminator write are
subscripted stores (out[i]). Reaching :281 / :395 therefore implies
out != NULL, so the operand is invariantly true and its independence
pair is unreachable.
Scope: neither function contains an #if/#ifdef in the span. Base64_Decode_nonCT
is compiled under !BASE64_NO_TABLE and aliased to Base64_Decode under
BASE64_NO_TABLE (:404-408); both variants carry the same entry check,
so the argument holds either way.
Evidence: llvm-cov MC/DC records both conditions' pairs as uncovered
(reports/coding/GAPS.md rows 281:9:281:27:0 and 395:9:395:27:0).
Deliberately untouched: the textually identical line in DoBase64_Encode
(coding.c:608). There out == NULL is the documented size-query mode
(`getSzOnly = (out == NULL)` at :520, returning LENGTH_ONLY_E), so that operand
is live and load-bearing -- base64_test exercises it.
Compiler cross-check: gcc -O2 emits byte-identical code for this file before
and after this commit -- the optimiser had already folded the removed
condition, independently confirming it was dead.
Premise: coding.c:660 `if (in == NULL || out == NULL || outLen == NULL)
return BAD_FUNC_ARG;` establishes in != NULL unconditionally -- note
it is stronger than the Base64 entry checks, which only reject a NULL
input when inLen > 0.
Claim: coding.c:663 `if (inLen == 1 && *outLen && in)` -- the `in` operand.
Proof: in is a parameter and is never reassigned; reaching :663 implies the
:660 check did not fire, hence in != NULL. The operand is invariantly
true and its independence pair is unreachable.
Scope: the whole function is inside a single WOLFSSL_BASE16 block with no
nested #if in the span, so the argument holds in every configuration
that compiles it.
Evidence: llvm-cov MC/DC records this condition's pair as uncovered
(reports/coding/GAPS.md row 663:9:663:36:2).
Compiler cross-check: gcc -O2 emits byte-identical code for this file before
and after this commit -- the optimiser had already folded the removed
condition, independently confirming it was dead.
Premise: md5.c:345 `if (md5 == NULL || (data == NULL && len > 0))
return BAD_FUNC_ARG;` establishes !(data == NULL && len > 0), i.e.
data != NULL || len == 0.
Claim: md5.c:361 `if (data == NULL && len == 0)` -- the `len == 0` operand.
Proof: under the left conjunct data == NULL, the premise forces len == 0.
len is word32, so !(len > 0) is exactly len == 0 -- no signed
wraparound case to consider. Neither data nor len is written between
:345 and :361. The operand is invariantly true when evaluated and its
independence pair is unreachable.
Scope: the intervening code is the
WOLFSSL_ASYNC_CRYPT && WC_ASYNC_ENABLE_MD5 block (:349-355), which
may return early but writes neither variable, and the buffLen range
check (:358). The argument holds in all four combinations of those
two macros.
Evidence: llvm-cov MC/DC records this condition's pair as uncovered
(reports/md5/GAPS.md row 361:9:361:33:1); it is the sole residual
holding md5.c at 12/13.
Proof check: gcc does not fold this (it does not propagate the
correlation between the entry guard's two operands across the branch), so the
implication was machine-checked instead: with data == NULL held true, all 2^32
word32 values of len were enumerated and every one that passes the :345 guard
has len == 0. Zero counterexamples -- exhaustive, not sampled.
Premise: each of the three functions opens with
if (<ctx> == NULL || (data == NULL && len > 0))
return BAD_FUNC_ARG;
(sha3.c:1185, :1864, :2162), establishing data != NULL || len == 0.
Claim: sha3.c:1189, :1868, :2166 `if (data == NULL && len == 0)` -- the
`len == 0` operand in all three.
Proof: under the left conjunct data == NULL the premise forces len == 0;
len is word32 so !(len > 0) is exactly len == 0. Nothing at all
executes between the entry guard and the claimed condition in any of
the three functions. The operand is invariantly true and its
independence pair is unreachable.
Scope: all three sites are inside PSOC6_HASH_SHA3 blocks (the static
wc_Sha3Update at :1158, wc_Shake128_Update at :1859,
wc_Shake256_Update at :2157) and contain no nested #if.
The four occurrences of the superficially similar three-way idiom
-- sha3.c:1123, :1285, :1967, :2263 -- are NOT affected: they follow
a bare `<ctx> == NULL` check and are themselves what makes the
following `data == NULL` return BAD_FUNC_ARG, so their `len == 0`
operand is load-bearing.
Not compile-verified: PSOC6_HASH_SHA3 needs the Cypress SDK, which is not
available on the host build matrix.
Compiler cross-check: not applicable -- PSOC6_HASH_SHA3 is not compiled on
the host, so there is nothing to compare.
Premise: tfm.c:5509 `if (fp_iszero(a) == FP_YES && fp_iszero(b) == FP_YES)
return FP_VAL;` establishes !(Za && Zb), writing Za for
fp_iszero(a) == FP_YES and Zb for fp_iszero(b) == FP_YES.
Claim: three consequences, all from that one premise:
(1) tfm.c:5514 `fp_iszero(b) == FP_NO` -- invariantly true;
(2) tfm.c:5518 `fp_iszero(a) == FP_NO` -- invariantly true;
(3) tfm.c:5523-5529, the whole `if (fp_iszero(a) == FP_YES)` block --
unreachable.
Proof: fp_iszero is the side-effect-free macro
`(((a)->used == 0) ? FP_YES : FP_NO)` (tfm.h:500) and neither a nor b
is written anywhere between :5509 and :5529.
(1) at :5514 the left operand already gives Za, and !(Za && Zb)
with Za forces !Zb -- the right operand cannot be false.
(2) symmetrically at :5518, Zb forces !Za.
(3) reaching :5526 requires !(Za&&Zb) && !(Za&&!Zb) && !(!Za&&Zb),
which is satisfiable only with !Za -- but the test there is Za.
The comment above it ("if a == 0 then b must equal zero too")
describes a state the :5509 guard has already rejected.
Scope: no #if/#ifdef occurs between :5508 and :5530. The WOLFSSL_SMALL_STACK
split above only chooses stack vs heap for u/v/r and is below the
removed code.
Evidence: llvm-cov MC/DC records the two operands' pairs as uncovered
(reports/bigint-tfm/GAPS.md rows 5514:8:5514:57:1 and
5518:8:5518:57:0).
Proof check: gcc does not fold this. fp_iszero is a side-effect-free
macro over ->used and neither operand is written in the span, so the decision
chain depends on exactly two booleans. All four (Za,Zb) states were enumerated:
:5514 and :5518 are each reached once with the dropped operand fixed true, the
:5526 block is reached only with Za false. Zero counterexamples -- the
enumeration is complete, not sampled.
Premise: integer.c:1769 `if (c->dp == NULL || c->alloc < max_ab + 1) {
if ((res = mp_grow(c, max_ab + 1)) != MP_OKAY) return res; }`.
Claim: integer.c:1796 `((tmpa == NULL) || (tmpb == NULL) || (tmpc == NULL))`
-- the `tmpc == NULL` operand, where tmpc = c->dp (:1792).
Proof: two cases, both giving c->dp != NULL at :1792.
Guard taken: mp_grow returned MP_OKAY, and mp_grow (:406-440) can only
return MP_OKAY with a->dp != NULL -- the grow branch assigns
a->dp = tmp only after rejecting tmp == NULL (:423-429), and the
non-grow branch has an explicit `else if (a->dp == NULL) return MP_VAL`
(:435-437).
Guard not taken: its first operand c->dp == NULL was false.
c->dp is not written between :1772 and :1792, so tmpc != NULL and the
operand's independence pair is unreachable. Note this needs no
data-structure invariant -- mp_grow's own post-condition suffices.
Scope: neither s_mp_add nor mp_grow contains an #if in the relevant span.
tmpa and tmpb keep their checks: a->dp / b->dp are caller-supplied
and a freshly mp_init'd operand legitimately has dp == NULL.
Evidence: llvm-cov MC/DC records this condition's pair as uncovered
(reports/bigint-integer/GAPS.md row 1795:9:1796:61:3).
Proof check: gcc does not fold this (it does not carry mp_grow's
post-condition across the call). mp_grow has exactly three exits, enumerated in
full: 'return MP_MEM' when XREALLOC yields NULL; 'return MP_VAL' in the
else-branch when a->dp == NULL; and the final 'return MP_OKAY', reachable only
after 'a->dp = tmp' with tmp already NULL-checked, or through the else-branch
that rejects a->dp == NULL. Hence MP_OKAY implies a->dp != NULL.
Premise: sp_int.c:18887 `if (err == MP_OKAY) {` opens the block that dominates
the claimed condition. The last thing that can set err is
ALLOC_SP_INT_SIZE at :18883, above that guard.
Claim: sp_int.c:18909, a second `if (err == MP_OKAY)` nested directly inside
the first.
Proof: control reaches :18909 only through the taken branch of :18887, so
err == MP_OKAY there. Between the two, err is neither assigned nor
passed by address: the span holds character stores into str and
`(void)sp_div_d(t, 10, t, &d)`, whose return value is explicitly
discarded. The inner test is therefore a tautology and its false
branch is unreachable.
Scope: the only preprocessor construct in the span is the
WOLFSSL_SP_INT_NEGATIVE sign-character block (:18888-18895); neither
arm writes err.
Evidence: llvm-cov MC/DC records this decision as never taking its false
branch; it is one of the two structural residuals noted for sp_int.c
in the sp-math baseline.
The remaining err checks in the function are live: ALLOC_SP_INT_SIZE writes err
(MP_VAL when the size exceeds SP_INT_DIGITS, MP_MEM in the malloc form) in both
its small-stack and static-stack expansions.
Compiler cross-check: gcc -O2 emits byte-identical code for this file before
and after this commit -- the optimiser had already folded the removed
condition, independently confirming it was dead.
Premise: sp_int.c:19947 `if (err == MP_OKAY) {`, immediately after
ALLOC_SP_INT_ARRAY (:19946) -- the last statement that can set err.
Claim: sp_int.c:19951, a second `if (err == MP_OKAY)` nested directly inside
it.
Proof: only two statements separate the two tests, `_sp_init_size(t[0], used)`
and `_sp_init_size(t[1], used)`, both returning void and neither
taking err's address. err is therefore still MP_OKAY, the inner test
is a tautology and its false branch is unreachable.
Scope: no #if occurs in the span, in either the small-stack or static-stack
expansion of DECL_SP_INT_ARRAY / ALLOC_SP_INT_ARRAY.
Evidence: llvm-cov MC/DC records this decision as never taking its false
branch; it is the second of the two structural residuals noted for
sp_int.c in the sp-math baseline.
The following `if (err == MP_OKAY)` stays live -- sp_gcd assigns err.
Compiler cross-check: gcc -O2 emits byte-identical code for this file before
and after this commit -- the optimiser had already folded the removed
condition, independently confirming it was dead.
Premise: memory.c:1337 `void* res = 0;` -- and every subsequent write to res
lies on a path that cannot reach the claimed condition.
Claim: memory.c:1414 `if (pt != NULL && res == NULL)` -- the `res == NULL`
operand.
Proof: res is assigned in exactly two places before :1414.
(a) :1353 `res = realloc(ptr, size)` sits inside the
`if (heap == NULL && globalHeapHint == NULL)` arm at :1348, while
:1414 sits inside that if's else arm -- mutually exclusive.
(b) :1394/:1397 sit in the fixed-IO-pool arm at :1387, while :1414
sits in the `/* general memory */` else arm at :1402 -- again
mutually exclusive.
Everything else on the path either returns (the WOLFSSL_HEAP_TEST
shortcut at :1342, the ptr == NULL case at :1371, the mutex-lock
failure at :1379) or writes only pt / i / mem->ava[]. So res still
holds its 0 initialiser at every evaluation of :1414: the operand is
invariantly true and its independence pair is unreachable.
Scope: checked against every combination of WOLFSSL_STATIC_MEMORY,
WOLFSSL_STATIC_MEMORY_LEAN, WOLFSSL_DEBUG_MEMORY, WOLFSSL_HEAP_TEST,
WOLFSSL_NO_MALLOC, SINGLE_THREADED and WOLFSSL_MALLOC_CHECK. Under
WOLFSSL_STATIC_MEMORY_LEAN the #ifndef at :1385 deletes both the
IO-pool arm and its else, making the :1402 block unconditional --
and deleting writes (b) along with it, so the argument only gets
stronger. XREALLOC overrides in types.h either route to this function
or replace it wholesale; neither can enter it mid-body.
Evidence: llvm-cov MC/DC records this condition's pair as uncovered
(reports/infra/GAPS.md row 1414:17:1414:42:1).
Compiler cross-check: gcc -O2 emits byte-identical code for this file before
and after this commit -- the optimiser had already folded the removed
condition, independently confirming it was dead.
Premise: wc_MlKemKey_EncodePublicKey ends with
if (ret == 0) { key->flags |= MLKEM_FLAG_H_SET; }
(wc_mlkem.c:2796-2799). It is the only definition of that function in
the tree and is unconditional inside WOLFSSL_HAVE_MLKEM.
Claim: wc_mlkem.c:1428-1431,
if ((ret == 0) && ((key->flags & MLKEM_FLAG_H_SET) == 0))
ret = BAD_STATE_E;
Proof: two cases at :1428.
(a) MLKEM_FLAG_H_SET was already set on entry: the block at :1398 is
skipped entirely and nothing clears the flag, so the second
operand is false.
(b) The flag was clear: reaching :1428 with ret == 0 requires
wc_MlKemKey_PublicKeySize to have succeeded, the (malloc build)
allocation to have succeeded, and wc_MlKemKey_EncodePublicKey to
have returned 0 -- which sets the flag. Again the second operand
is false.
{ret == 0, H unset} is therefore unreachable, the condition can never
be true, and BAD_STATE_E can never be returned from here.
Scope: both the WOLFSSL_NO_MALLOC and !WOLFSSL_NO_MALLOC arms of the block
funnel through the same EncodePublicKey call; the size-failure and
allocation-failure paths both leave ret != 0. The enclosing
!WOLFSSL_MLKEM_NO_ENCAPSULATE || !WOLFSSL_MLKEM_NO_DECAPSULATE gate
selects whether the function exists at all.
Evidence: llvm-cov MC/DC records both of this decision's conditions as
uncovered (reports/mlkem/GAPS.md rows 1373:9:1373:61:0 and :1, at the
pre-drift line numbers) -- they are the only two residuals holding
wc_mlkem.c at 66/68.
The comment called it an "implementation issue" check, i.e. an assertion
against a future encoder that forgets the flag; it is being removed rather than
retained because no call path can reach it.
Proof check: gcc does not fold this (the encoder call is not inlined).
Verified instead by enumerating every write to key->flags in the translation
unit -- all nine, at wc_mlkem.c:453, 621, 852, 1001, 1003, 2283, 2327, 2430 and
2794, living in Init, Free, MakeKeyWithRandom, DecodePrivateKey,
DecodePublicKey and EncodePublicKey. wc_mlkemkey_check_h calls only
wc_MlKemKey_PublicKeySize, XMALLOC, wc_MlKemKey_EncodePublicKey and XFREE, so
the sole flag write reachable from it is :2794, which SETS MLKEM_FLAG_H_SET on
ret == 0. No reachable path clears it.
Premise: `int ret = 1;` at wc_mldsa.c:5062, and mldsa_check_low (:5028-5046)
returns only 0 or 1.
Claim: wc_mldsa.c:5066 `for (i = 0; (ret == 1) && (i < l); i++)` -- the
`ret == 1` operand.
Proof: first evaluation: ret is its initialiser 1.
Re-evaluations: the body's only write is `ret = mldsa_check_low(...)`,
immediately followed by `if (ret == 0) { break; }` -- so the loop
condition is re-evaluated only on paths where ret is not 0, and
mldsa_check_low returns nothing but 0 or 1. Hence ret == 1 whenever
the operand is evaluated; its false half is unreachable and the
`break` alone terminates the loop.
Scope: the function is compiled under
!WOLFSSL_MLDSA_NO_VERIFY || (!WOLFSSL_MLDSA_NO_SIGN &&
!WOLFSSL_MLDSA_SIGN_SMALL_MEM); there is no #if inside it. The AVX2
alternative at :5089 is a separate function and is untouched.
Evidence: llvm-cov MC/DC records this condition as never false
(reports/mldsa/GAPS.md row 5048:17:5048:38:0, pre-drift numbering).
The guard is dropped rather than the `break`: keeping both would leave the same
dead operand.
Compiler cross-check: gcc -O2 emits byte-identical code for this file before
and after this commit -- the optimiser had already folded the removed
condition, independently confirming it was dead.
Premise: wc_mldsa.c:11544 `if (ret == 0) {` opens the block containing the
claimed condition.
Claim: wc_mldsa.c:11589 `if ((ret == 0) && (x != 0))` -- the `ret == 0`
operand.
Proof: :11544 dominates :11589 and nothing in between assigns ret: the block
decodes, NTTs, matrix-multiplies and XOR-accumulates into x through
mldsa_vec_decode_*, mldsa_vec_ntt_small_full, mldsa_matrix_mul,
mldsa_vec_red, mldsa_vec_invntt_full, mldsa_vec_add/sub/make_pos --
all void-returning. A grep of the span for `ret` finds only the two
conditions themselves. The operand is invariantly true and its
independence pair is unreachable.
Scope: the only preprocessor construct in the span is WOLFSSL_MLDSA_SMALL at
:11566, which adds another void call.
Evidence: llvm-cov MC/DC records this condition as never false
(reports/mldsa/GAPS.md row 11479:13:11479:35:0, pre-drift numbering).
The nearby `ret == 0` guards at :11485 and :11488 stay: prvKeySet / pubKeySet
are user-controlled and those decisions are live.
Compiler cross-check: gcc -O2 emits byte-identical code for this file before
and after this commit -- the optimiser had already folded the removed
condition, independently confirming it was dead.
Premise: wc_mldsa.c:8684 `int ret = 0;` in the WOLFSSL_MLDSA_SIGN_SMALL_MEM
arm of the sign path.
Claim: wc_mldsa.c:8730 `if ((ret == 0) && (*sigLen < params->sigSz))` -- the
`ret == 0` operand.
Proof: ret is not assigned anywhere between its initialiser and :8730 -- a
grep of the span for `ret` yields only the declaration and this
condition. The intervening code is the WOLFSSL_CHECK_MEM_ZERO
bookkeeping at :8724-8728 (an XMEMSET and a wc_MemZero_Add). This is
the operand's only evaluation, and it is invariantly true, so its
independence pair is unreachable.
Scope: the site is inside the #else arm selected by
WOLFSSL_MLDSA_SIGN_SMALL_MEM; the WOLFSSL_CHECK_MEM_ZERO block in the
span writes neither ret nor sigLen.
Evidence: llvm-cov MC/DC records this condition as never false
(reports/mldsa/GAPS.md row 8685:9:8685:48:0, pre-drift numbering).
Compiler cross-check: gcc -O2 emits byte-identical code for this file before
and after this commit -- the optimiser had already folded the removed
condition, independently confirming it was dead.
…oops
Premise: each of the two inner loops is entered only from an outer loop whose
own condition already established ret == 0 --
wc_mldsa.c:8097 `for (r = 0; (ret == 0) && (r < params->k); r++)`
wc_mldsa.c:8873 `for (; (ret == 0) && valid && (r < params->k); r++)`
-- and nothing between the outer condition and the inner one assigns
ret. (At :8884 the WC_MLDSA_FAULT_HARDEN check does write ret, but it
`break`s out of the outer loop, so it never reaches the inner one.)
Claim: the `ret == 0` operand of
wc_mldsa.c:8103 `for (s = 0; (ret == 0) && (s < params->l); s++)`
wc_mldsa.c:8895 `for (s = 0; (ret == 0) && (s < params->l); s++)`
Proof: first evaluation: ret == 0 by the premise.
Re-evaluations: every write to ret inside either body is immediately
followed by an unconditional `break` --
:8107 `ret = mldsa_rej_ntt_poly_ex(...)` / :8108 `if (ret != 0) break;`
:8899 the same, and the WC_MLDSA_FAULT_HARDEN write at :8907, also
followed by `break`.
A scan of both bodies finds no other assignment to ret. So the loop
condition is never re-evaluated with ret != 0, the operand is
invariantly true, and its independence pair is unreachable.
Scope: checked with and without WC_MLDSA_FAULT_HARDEN,
WOLFSSL_MLDSA_SMALL_MEM_POLY64, WOLFSSL_MLDSA_SMALL and
WOLFSSL_MLDSA_SIGN_SMALL_MEM_PRECALC_A -- every one of those either
adds a break-terminated write or none at all.
Evidence: llvm-cov MC/DC records both conditions as never false
(reports/mldsa/GAPS.md rows for 8103 and 8850, pre-drift numbering).
The two enclosing outer loops keep their `ret == 0` operand: they DO re-evaluate
after the inner `break`, so their false half is reachable.
Compiler cross-check: gcc -O2 emits byte-identical code for this file before
and after this commit -- the optimiser had already folded the removed
condition, independently confirming it was dead.
Premise: wc_lms_impl.c:3593 `priv_key->inited = 0;`, sitting under the SAME
#ifndef WOLFSSL_WC_LMS_SMALL gate as the claimed condition -- wherever
the check is compiled, so is the reset.
Claim: wc_lms_impl.c:3603 `if ((ret == 0) && (!priv_key->inited))` -- the
`!priv_key->inited` operand.
Proof: the only call between the reset and the check is
wc_hss_expand_private_key(state, priv_key->priv, priv_raw, 0), which
receives the priv buffer, not the key struct, and so cannot write the
`word8 inited:1` bitfield (wc_lms.h:741). inited is therefore still 0
and the operand is invariantly true; its independence pair is
unreachable.
Scope: the WOLFSSL_WC_LMS_SERIALIZE_STATE `if (pub_root != NULL)` at :3596
only decides whether the block runs at all; it does not touch inited.
Evidence: llvm-cov MC/DC records both of this decision's conditions as
uncovered (reports/lms/GAPS.md rows 3592:13:3592:46:0 and :1, recorded
against wc_lms.c before the impl-file split).
The `priv_key->inited = 0;` at :3593 goes with it: it was only ever observed by
this operand, and :3620 assigns inited unconditionally on every path out.
Proof check: gcc does not fold this -- it must assume the call may
alias the bitfield. It cannot: HssPrivKey declares 'byte* priv' as a POINTER
member (wc_lms.h:726) alongside 'word8 inited:1' (wc_lms.h:741), and
wc_hss_expand_private_key receives the pointer value, not the struct address.
Writes through it target the pointed-to buffer, a distinct object; reaching
inited that way would be an out-of-bounds write, i.e. undefined behaviour.
Premise: mp_init (integer.c:145-166) has exactly one non-MP_OKAY return,
`if (a == NULL) return MP_VAL;` at :150. Everything after it is
unconditional field initialisation ending in `return MP_OKAY;`.
Claim: the six guards at integer.c:114, 117, 122, 127, 132, 137 of the shape
if (x && ((res = mp_init(x)) != MP_OKAY)) { ...mp_clear...; return res; }
-- specifically the `!= MP_OKAY` operand of each, and the mp_clear
cascades they guard.
Proof: the left operand of each && establishes x != NULL, which excludes
mp_init's only failure path, so mp_init(x) == MP_OKAY and the second
operand is invariantly false. None of the six bodies can execute, so
the mp_clear cascades and the early `return res` are unreachable and
the function's only possible return value is MP_OKAY.
Scope: the sole preprocessor construct in mp_init is HAVE_WOLF_BIGINT
(:161-163), which adds the void call wc_bigint_init. The
`#define mp_init sp_init` in sp_int.h:1359 does not apply -- integer.c
is compiled only when integer.h is the math backend, and integer.h
declares mp_init as a plain prototype (:315).
Evidence: llvm-cov MC/DC records the `!= MP_OKAY` operand of all six as
uncovered (reports/bigint-integer/GAPS.md rows 114/117/122/127/132/137,
index 1).
Caveat, since this is the one proof here that rests on the callee's body rather
than a guard in the same function: mp_init is public API whose contract permits
failure, and the sibling SP backend's sp_init genuinely can fail. This makes
mp_init_multi depend on integer.c's mp_init staying failure-free. Kept as the
last commit of the non-FIPS group so it can be dropped on its own.
Compiler cross-check: gcc -O2 emits byte-identical code for this file before
and after this commit -- the optimiser had already folded the removed
condition, independently confirming it was dead.
Premise: aes.c:16444 `int bit = 7;` and the single update site inside the loop,
aes.c:16492-16498 `bit--; if (bit < 0) { ...; bit = 7U; ... }`.
Claim: aes.c:16507 `if (bit >= 0 && bit < 7)` -- the `bit >= 0` operand.
Proof: bit is written nowhere else in the function, and the decrement is
immediately normalised back to 7 whenever it would go negative, so
0 <= bit <= 7 holds at every loop-iteration boundary. The loop's only
other exit is the `break` taken when the block transform fails, which
happens before the `bit--` and leaves bit unchanged (and sets ret != 0,
so :16506 short-circuits anyway). sz == 0 is rejected at entry, so the
zero-trip case still has bit == 7. `bit >= 0` is therefore invariantly
true and its independence pair is unreachable.
Scope: there is exactly one definition of wc_AesFeedbackCFB1 in the tree
(:16438, called only from wc_AesCfb1Encrypt/Decrypt), all of it inside
#ifndef WOLFSSL_NO_AES_CFB_1_8. The only #ifdef in the function,
WC_AES_HAVE_PREFETCH_ARG at :16446, declares did_prefetches and
touches neither bit nor the control flow.
Evidence: llvm-cov MC/DC records this condition's pair as uncovered
(reports/aes/GAPS.md row 16469:13:16469:32:0, pre-drift numbering).
`bit < 7` stays and is load-bearing: when sz is a whole number of bits the loop
exits with bit == 7 and the trailing partial byte must not be written.
aes.c is inside the FIPS module boundary. Released FIPS flavours pin aes.c to a
tag and are unaffected; fips-dev/fips-ready build from master and recompute the
in-core hash.
Compiler cross-check: gcc -O2 emits byte-identical code for this file before
and after this commit -- the optimiser had already folded the removed
condition, independently confirming it was dead.
Premise: ed448.c:1517 `if ((ret == 0) && key->privKeySet) { ... }` -- the
sibling arm of the if/else this condition belongs to.
Claim: ed448.c:1524 `else if ((ret == 0) && (!key->privKeySet))` -- the
`!key->privKeySet` operand; and, as a direct consequence, the nested
`if (ret == 0)` that opened the arm's body.
Proof: entering the else arm means the sibling condition was false, i.e.
(ret != 0) || (!privKeySet). && short-circuits, so the else arm's own
`key->privKeySet` read happens only after `ret == 0` evaluated true --
and with ret == 0 the sibling's falsity forces !privKeySet. The
operand is therefore invariantly true. privKeySet is a plain bitfield,
not volatile, and no statement runs between the two conditions.
The nested `if (ret == 0)` follows from the same short-circuit: the
arm is entered only with ret == 0 and nothing precedes the nested test.
Scope: wc_ed448_check_key contains no #if/#ifdef, so this holds in every
configuration that compiles ed448.c.
Evidence: llvm-cov MC/DC records this condition's pair as uncovered
(reports/ed448/GAPS.md row 1503:14:1503:46:1, pre-drift numbering).
Reviewed with `git diff -w`: apart from the two removed lines the change is
pure de-indentation.
ed448.c is inside the FIPS module boundary. Released FIPS flavours pin ed448.c
to a tag and are unaffected; fips-dev/fips-ready build from master and
recompute the in-core hash.
Compiler cross-check: gcc -O2 emits byte-identical code for this file before
and after this commit -- the optimiser had already folded the removed
condition, independently confirming it was dead.
|
Contributor
There was a problem hiding this comment.
Pull request overview
This PR removes provably unreachable/dead conditional branches across wolfCrypt (crypto primitives, KDF/PBKDF helpers, big integer math, and memory helpers) to simplify control flow without changing behavior.
Changes:
- Simplifies loop/guard conditions that are dominated by earlier checks or immediate
breakpaths (e.g., ML-DSA, KDF CMAC loop, AES CFB1 bit check). - Removes redundant NULL/state checks that are already enforced by entry validation or guaranteed side-effects (e.g., Base64/Base16 decode, ML-KEM H flag, realloc bucket path).
- Streamlines math helpers by removing dominated branches (tfm
fp_gcd, sp_int decimal reverse / lcm setup, integer mp_init_multi and dp sanity checks).
Reviewed changes
Copilot reviewed 14 out of 14 changed files in this pull request and generated no comments.
Show a summary per file
| File | Description |
|---|---|
| wolfcrypt/src/wc_mlkem.c | Removes a redundant BAD_STATE re-check after public-key encoding sets MLKEM_FLAG_H_SET on success. |
| wolfcrypt/src/wc_mldsa.c | Removes dominated ret guards in loop headers and checks, relying on existing in-body breaks/outer guards. |
| wolfcrypt/src/wc_lms_impl.c | Removes a dead inited reset/check path; auth-path initialization remains controlled by ret == 0. |
| wolfcrypt/src/tfm.c | Simplifies fp_gcd zero-operand handling after the explicit (0,0) early return. |
| wolfcrypt/src/sp_int.c | Removes redundant err == MP_OKAY nesting where the surrounding block already enforces it. |
| wolfcrypt/src/sha3.c | Simplifies PSOC6 SHA3/SHAKE update NULL+len==0 checks based on the existing (data == NULL && len > 0) guard. |
| wolfcrypt/src/pwdbased.c | Removes a redundant NULL-argument check in internal DoPKCS12Hash that is satisfied by its call sites. |
| wolfcrypt/src/memory.c | Removes a redundant res == NULL conjunct in the bucket-allocation path. |
| wolfcrypt/src/md5.c | Simplifies wc_Md5Update NULL+len==0 handling based on the existing (data == NULL && len > 0) guard. |
| wolfcrypt/src/kdf.c | Removes redundant ret == 0 from the CMAC block loop condition (loop already breaks on ret != 0). |
| wolfcrypt/src/integer.c | Simplifies mp_init_multi and dp-pointer sanity checks based on guaranteed behavior of mp_init/mp_grow. |
| wolfcrypt/src/ed448.c | Removes dominated checks/branches in the public-key validation path while preserving existing rejection behavior (including non-canonical y=p / y=p-1 handling via ed448_is_small_order). |
| wolfcrypt/src/coding.c | Removes redundant operand checks already guaranteed by function preconditions in Base64/Base16 decoding. |
| wolfcrypt/src/aes.c | Removes redundant bit >= 0 check where bit is maintained to be non-negative at the post-loop point. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
wolfSSL-Fenrir-bot
left a comment
wolfSSL-Fenrir-bot
left a comment
There was a problem hiding this comment.
Fenrir Automated Review — PR #11028
Scan targets checked: wolfcrypt-bugs, wolfcrypt-src
No new issues found in the changed files. ✅
Premise: ed448.c:1511 `if ((ret == 0) && ed448_is_small_order(key->p)) {
...; ret = PUBLIC_KEY_E; }`, and ed448_is_small_order (:245-312),
which zeroes byte 56 of a copy of the input and memcmps it against a
table that explicitly includes the non-canonical y = p encoding
(:283-291: 0xff x28, 0xfe, 0xff x27, 0x00).
Claim: ed448.c:1554 `if ((ret == PUBLIC_KEY_E) && (key->p[0] < 0xff))` --
the `key->p[0] < 0xff` operand, whose false half is the Y == p case.
Proof: reaching :1554 requires the preceding range walk to have found
p[56..29] all 0xff (loop at :1533), p[28] == 0xfe (:1543) and
p[27..1] all 0xff (loop at :1546). If p[0] were also 0xff the input
would be exactly the y = p encoding modulo byte 56 -- which
ed448_is_small_order masks -- so :1511 would have set
ret = PUBLIC_KEY_E and the else-if arm containing :1554 would never
have been entered. The operand can only ever evaluate true, so its
independence pair is unreachable.
With that operand fixed true, the remaining `ret == PUBLIC_KEY_E`
operand no longer decides anything: when it is false the bottom loop
has already set ret = 0. Both paths end with ret == 0, so the whole
conditional collapses to `ret = 0;`.
Scope: neither wc_ed448_check_key nor ed448_is_small_order is conditionally
compiled, so this holds in every configuration that builds ed448.c.
Evidence: llvm-cov MC/DC records no covered pair for this condition in any
ed448 variant.
Rejection semantics are unchanged: y = p and y = p+1 are still refused, by
ed448_is_small_order rather than by this byte walk.
ed448.c is inside the FIPS module boundary. Released FIPS flavours pin ed448.c
to a tag and are unaffected; fips-dev/fips-ready build from master and
recompute the in-core hash.
With the last-byte test gone, the loop over p[27..1] can no longer affect the
outcome -- its only effects were setting ret = 0 and breaking -- so it goes too,
and the two surviving arms both yield ret = 0, collapsing to a single
`p[ED448_PUB_KEY_SIZE/2] <= 0xfe` test. The only input for which this differs
from the original is exactly the y == p encoding, which the proof below shows
never reaches here.
Proof check: gcc does not fold this (it cannot reason about the small-order
table). Machine-checked exhaustively instead: the byte walk pins 56 of the 57
public-key bytes before the final test, leaving p[0] as the only free variable,
so all 256 values were enumerated against the real ed448_is_small_order(). Two
values (p[0] = 0xff, y = p; and p[0] = 0xfe, y = p-1) are rejected early by the
table; the other 254 reach the final test and all satisfy p[0] < 0xff. Zero
counterexamples over the complete state space.
Also checked with clang's deadcode.DeadStores analyzer (the checker behind the
clang-tidy CI legs): clean on this file, with the two pre-existing sp_int.c
core.* findings unchanged from master.
Premise: kdf.c:1609 `int ret = 0;` and kdf.c:1666 `if (ret != 0) { break; }`,
an unconditional statement on every path through the loop body.
Claim: kdf.c:1636 `while (ret == 0 && len_rem >= WC_AES_BLOCK_SIZE)` -- the
`ret == 0` operand.
Proof: first evaluation: ret is its initialiser 0. Nothing between :1609 and
:1636 writes ret -- the four argument-check paths (:1612-1627) and the
WOLFSSL_SMALL_STACK allocation failure (:1630) all `return` instead.
Re-evaluations: the body contains no `continue` and no `goto`, so
every iteration reaches :1666, which breaks out whenever ret != 0.
Control therefore returns to the loop condition only with ret == 0:
the operand is invariantly true and its independence pair is
unreachable.
Scope: the only #if inside the body is WOLFSSL_DEBUG_KDF (:1639-1642),
containing a WOLFSSL_MSG_EX and nothing else; WOLFSSL_SMALL_STACK
only chooses heap vs stack for cmac, above the loop.
Evidence: llvm-cov MC/DC records this condition as never false
(reports/kdf/GAPS.md row 1616:12:1616:52:0, pre-drift numbering).
The `break` is what terminates the loop on error and is kept; ret is still
tested at :1672 and returned.
kdf.c is inside the FIPS module boundary (v5, v5-RC12, v6, v7+). Released FIPS
flavours pin kdf.c to a tag and are unaffected; fips-dev/fips-ready build from
master and recompute the in-core hash.
Compiler cross-check: gcc -O2 emits byte-identical code for this file before
and after this commit -- the optimiser had already folded the removed
condition, independently confirming it was dead.
Premise: DoPKCS12Hash is static with exactly two call sites, in the two
mutually exclusive WC_PKCS12_PBKDF_USING_MP_API variants of
wc_PKCS12_PBKDF_ex -- pwdbased.c:555 (buffer, Ai) and :771 (buffer, B).
Claim: pwdbased.c:376 `if ((buffer == NULL) || (Ai == NULL))
return BAD_FUNC_ARG;`
Proof: four paths reach the function (2 call sites x WOLFSSL_SMALL_STACK on
and off) and none can pass a NULL:
Ai / B -- SMALL_STACK: XMALLOC at :479 / :741, each immediately
followed by `if (... == NULL) return MEMORY_E;`. Otherwise a
stack array (`byte Ai[WC_MAX_DIGEST_SIZE]` :440,
`ALIGN8 byte B[WC_MAX_BLOCK_SIZE]` :685).
buffer -- initialised to staticBuffer (:431 / :687) and only
replaced by the XMALLOC at :513 / :748, each immediately followed
by `if (buffer == NULL) { ...free...; return MEMORY_E; }`.
Both operands are therefore invariantly false and neither
independence pair is reachable.
Scope: covers both WOLFSSL_SMALL_STACK settings and both
WC_PKCS12_PBKDF_USING_MP_API arms; the whole area is inside
HAVE_PKCS12.
Evidence: llvm-cov MC/DC records both conditions' pairs as uncovered
(reports/pwdbased/GAPS.md rows 358:9:358:41:0 and :1, pre-drift
numbering).
pwdbased.c is inside the FIPS module boundary for v6 and v7+. Released FIPS
flavours pin pwdbased.c to a tag and are unaffected; fips-dev/fips-ready build
from master and recompute the in-core hash.
Compiler cross-check: gcc -O2 emits byte-identical code for this file before
and after this commit -- the optimiser had already folded the removed
condition, independently confirming it was dead.
danielinux
force-pushed
the
mcdc-eliminate-dead-code
branch
from
July 31, 2026 19:37
25ca230 to
a219774
Compare
Member
Author
|
jenkins retest this please (build timeout) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
Eliminates all conditions that are impossible to reach from the existing wolfcrypt code.
Each dead condition is self-containerd and documented in a separate commit, with proof of death through object code comparison vs. gcc -O2:
Testing
These are leftover (uncoverable) conditions discovered during the the first four phases of MC/DC campaign
Proven by gcc -O2 object equivalence (15)
The optimiser had already folded the condition — compiling the file before and after the commit yields byte-identical code, so the removal is provably behaviour-preserving.
Proved by exhaustive enumeration [no optimizer can reach these] (6)
Compile-gated, no host evidence (1)