On Wed, Sep 13, 2017 at 8:09 AM, Niels Möller <[email protected]> wrote:
> [email protected] (Niels Möller) writes:
>
>> This code needs some careful analysis, to see under what conditions hi
>> might be used uninitialized, and in case there's some valid inputs for
>> which this could happen fix that, and if not, back up our assumptions
>> with asserts (which I hope the static analyzer will understand).
>
> It turns out analysis isn't that subtle. The thing is, the static
> analyzer thinks that the loop condition (rn >= 2*mn - bn) can be
> initially false.
>
> Now, rn is initialized to 2*mn, so this could be false only if the
> subtraction ounderflows. Which is doesn't do, since valid range for bn
> is 0 < bn < mn.
>
> Question is what's the best way to make thhat clear to compilers and
> analyzers.
>
> Loops could be rewritten as do {} while (0) loops. Or we could add more
> asserts, maybe it's sufficient to replace the somewhat weak
>
> assert (sn > 0);
>
> with
>
> assert (bn < mn);
>
> Since sn is size_t (unsigned), the former only checks that mn != bn.
I tried with few asserts() but couldn't eliminate this error. We may
be hitting an analyzer bug, or missing something there.
I've even added:
if (rn < 2 * mn - bn) <---NEW
abort(); <--- NEW
while (rn >= 2 * mn - bn)
prior to the while above, but the analyzer still thinks that the while
path can be skipped.
The only way I could eliminate the error was through the attached
patch which is ugly.
Maybe we should put this whole function in
#ifndef __clang_analyzer__
block to allow a smooth CI run.
regards,
Nikos
diff --git a/ecc-mod.c b/ecc-mod.c
index 5fee4c68..ab0d02e3 100644
--- a/ecc-mod.c
+++ b/ecc-mod.c
@@ -50,6 +50,7 @@ ecc_mod (const struct ecc_modulo *m, mp_limb_t *rp)
mp_size_t rn = 2*mn;
mp_size_t i;
unsigned shift;
+ unsigned hi_init = 0;
assert (sn > 0);
@@ -81,6 +82,7 @@ ecc_mod (const struct ecc_modulo *m, mp_limb_t *rp)
hi = mpn_add_n (rp + rn - sn, rp + rn - sn, rp + rn, sn);
hi = cnd_add_n (hi, rp + rn - mn, m->B, mn);
+ hi_init = 1;
assert (hi == 0);
}
}
@@ -95,9 +97,14 @@ ecc_mod (const struct ecc_modulo *m, mp_limb_t *rp)
hi = mpn_add_n (rp + bn, rp + bn, rp + mn, sn);
hi = sec_add_1 (rp + bn + sn, rp + bn + sn, mn - bn - sn, hi);
+
+ hi_init = 1;
}
+ assert(hi_init != 0);
shift = m->size * GMP_NUMB_BITS - m->bit_size;
+
+
if (shift > 0)
{
/* Combine hi with top bits, add in */
_______________________________________________
nettle-bugs mailing list
[email protected]
http://lists.lysator.liu.se/mailman/listinfo/nettle-bugs
