Applet 7.2 denies ReadObject on a symmetric key object that was created
with no policy attached, so the shared secret written into the derive
target by Se05x_API_ECDHGenerateSharedSecret_InObject could not be
exported: sss_key_store_get_key failed with SW 0x6986 (command not
allowed) on SE05x applet >= 7.2 hardware.
Create the derive target with an attached common policy granting read,
write and delete. An attached policy replaces the applet default
entirely, so write (the ECDH engine storing the result) and delete (the
cleanup path) must be granted explicitly alongside read. Guarded by
SSS_HAVE_SE05X_VER_GTE_07_02 so builds against older middleware keep
creating the object with no policy attached.
Align se050_curve25519_shared_secret with the ECC path: set
deriveKeyCreated only after sss_key_store_set_key succeeds, so the
cleanup path cannot erase or free a derive key object whose handle
was never allocated.
Middleware built for SE05x applet >= 07_02 (required for SE052) derives
the ECDH shared secret with Se05x_API_ECDHGenerateSharedSecret_InObject,
which requires TLV[TAG_7] to reference an existing HMACKey object sized
exactly to the shared secret; otherwise the applet returns SW 0x6985
(conditions not satisfied). The port never created this object, so ECDH
offload failed with WC_HW_E on such builds.
Create the derive target as an HMACKey object of the exact secret size
before the derive, for both ECC and Curve25519 shared secrets. Read the
result back as AES type since sss_se05x_key_store_get_key has no HMAC
read case.
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).
The caller obligation the guard used to restate is recorded in the function's
header comment instead.
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.
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: 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 is still refused, by
ed448_is_small_order rather than by this byte walk, and every other encoding
takes the same path as before. The table's y = p row is therefore what enforces
the upper end of the Y range; ed448_is_small_order carries a note saying so, so
the dependency is stated where the invariant is produced as well as where it is
consumed.
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: 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.
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: 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).
The other two math backends already implement this API exactly this way, so the
resulting shape is the tree's majority convention rather than a new one:
sp_int.c's sp_init_multi (mp_init_multi under the SP backend, sp_int.h:1361)
NULL-guards each operand, calls the void _sp_init_size and returns MP_OKAY
unconditionally, and tfm.c:4390 does the same with fp_init. The call sites that
test the result -- integer.c:1089, :1233 and the rest -- are therefore already
testing a constant in every default and fastmath build.
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, so mp_init_multi now depends 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. Note that sp_init has the same shape today -- MP_VAL for a NULL
argument, MP_OKAY otherwise -- so no backend in the tree has an init that can
fail on a non-NULL operand.
The mp_init calls themselves are kept although the XMEMSET above them already
produces the state mp_init writes: dp = NULL, used = 0, alloc = 0,
sign = MP_ZPOS (0), and under HAVE_WOLF_BIGINT wc_bigint_init only zeroes raw.
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: 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_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.
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: `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_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: 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: 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: 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: 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: 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: 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: 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: 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: 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: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.
The assembly/SP generators had been modified but not all output files were
generated.
All files now are up to date with the latest generator scripts, that were fixed.
wolfevent.c (the wolfEvent completion queue) only compiled under
--enable-asynccrypt: AM_CONDITIONAL([BUILD_WOLFEVENT],...) tested only
ENABLED_ASYNCCRYPT. But HAVE_WOLF_EVENT is a user-settable macro that
internal.c/ssl.c gate their wolfEventQueue_* references on, so a
--enable-usersettings build that defines HAVE_WOLF_EVENT referenced the
queue API while the object was never built -> link error (undefined
wolfEventQueue_Init/Free). BUILD_WOLFEVENT was also the only BUILD_*
conditional missing the standard "|| ENABLED_USERSETTINGS = yes" escape
hatch that lets a header-driven build compile a source and defer the
decision to the file's own #ifdef.
Add that clause (matching BUILD_FALCON/BUILD_MLKEM/etc.) so usersettings
builds compile wolfevent.c; its internal #ifdef HAVE_WOLF_EVENT still
gates whether the code is active, so non-event builds get an empty object.
Also silence wolfEvent_Poll's unused-parameter -Werror in non-async builds
(event/flags are consumed only by the async hardware poll), which the
above change surfaces now that the file compiles without WOLFSSL_ASYNC_CRYPT.
Restore the original short-circuit XMALLOC chains and leave the zeroing to
mp_init_multi(). On a partial allocation failure mp_init_multi() is skipped,
so nothing is initialized: free whatever was allocated right there and NULL
the pointers, so the shared cleanup at the end of the function never calls
mp_clear()/mp_forcezero() on an allocated-but-uninitialized mp_int.
No extra mp_init() calls, no XMEMSET, and the returned error codes are
unchanged.
Andrew Hutchings
Tobias Frauenschläger
Daniele Lacamera
David Garske
Daniel Pouzzner
Sean Parkinson
Anthony Hu