Re: Overflow in mpz_cmp
Le 17/02/2020 à 22:59, Marco Bodrato a écrit : >> The bug was noticed when formally verifying this function. > > Did you apply formal verification to other functions? Did they succeed? Just so that there is no misunderstanding, we did not formally verify GMP's C/ASM functions directly, but our understanding of them. More concretely, we first translated them into a more palatable programming language, and then we formally verified them. Here is the list of verified functions: mpz_set_ui, mpz_set_si, mpz_get_ui mpz_cmp, mpz_cmp_ui, mpz_cmpabs, mpz_cmpabs_ui mpz_add, mpz_add_ui, mpz_sub, mpz_sub_ui, mpz_ui_sub mpz_mul, mpz_mul_si, mpz_mul_ui mpz_mul2exp, mpz_tdiv_q_2exp mpn_cmp mpn_copyi, mpn_copyd mpn_zero_p, mpn_zero mpn_add, mpn_add_n, mpn_sub, mpn_sub_n mpn_mul, mpn_mul_n mpn_lshift, mpn_rshift mpn_powm mpn_get_str, mpn_set_str mpn_add_1, mpn_sub_1, mpn_mul_1, mpn_addmul_1, mpn_submul_1 mpn_divrem_1, mpn_tdiv_qr mpn_sqrtrem Note that multiplication is only verified up to Toom-3x2, and only the schoolbook version of division is verified. Also, in presence of conditional compilation, we only verified one possible version of the code (e.g., we assume that HAVE_NATIVE_mpn_redc_2 is not defined). So, what we have verified is kind of an intermediate code: more intricate than Mini-GMP, but not as intricate as GMP. A bit more details can be found there: https://gitlab.inria.fr/why3/whymp Best regards, Guillaume ___ gmp-devel mailing list gmp-devel@gmplib.org https://gmplib.org/mailman/listinfo/gmp-devel
Re: Overflow in mpz_cmp
Ciao, Il 2020-02-18 00:35 Guillaume Melquiond ha scritto: Le 17/02/2020 à 22:59, Marco Bodrato a écrit : Did you apply formal verification to other functions? Did they succeed? Here is the list of verified functions: mpn_powm mpn_sqrtrem Those are particularly interesting for me! I recently committed some special flavours of powm: special cases for base=2 or when the base is a single limb. It would be really interesting to check if they are formally correct. Moreover year ago, or maybe more, I wrote a possible variation for sqrt1. I never moved it to the main repository, because I did not have the time to analyse its correctness. Again, an instrument to check, would be nice. A bit more details can be found there: https://gitlab.inria.fr/why3/whymp I'll look into your work, thanks. Ĝis, m -- http://bodrato.it/papers/ ___ gmp-devel mailing list gmp-devel@gmplib.org https://gmplib.org/mailman/listinfo/gmp-devel
Re: Overflow in mpz_cmp
Ciao, Il 2020-02-13 08:54 Guillaume Melquiond ha scritto: Note that mpz_cmpabs does not have any overflow issue, since absolute sizes are subtracted there. So, except maybe for homogeneity with mpz_cmp, it can keep using the optimized version. I pushed a patch for both cmp and cmpabs. So that the second is ready for a change in the type of the field _mp_size for the mpz_t variables :-) But you are right, the patch to cmpabs is not needed for the current code. Il 2020-02-10 18:25 Guillaume Melquiond ha scritto: The bug was noticed when formally verifying this function. Did you apply formal verification to other functions? Did they succeed? Ĝis, m ___ gmp-devel mailing list gmp-devel@gmplib.org https://gmplib.org/mailman/listinfo/gmp-devel
Re: Overflow in mpz_cmp
Le 11/02/2020 à 14:22, Marco Bodrato a écrit :
>> When the operand sizes do not match, the mpz_cmp function function just
>> returns the difference of the signed sizes. Unfortunately, this
>> difference might not fit inside the "int" return type, when the numbers
>> are of opposite sign.
>
> In mini-gmp we defined a macro:
> #define GMP_CMP(a,b) (((a) > (b)) - ((a) < (b)))
>
> We may use the same idea here too. I mean something like the following:
> mpz_cmpabs (mpz_srcptr u, mpz_srcptr v) __GMP_NOTHROW
> {
> - dsize = usize - vsize;
> + cmp = (usize > vsize) - (usize < vsize);
Note that mpz_cmpabs does not have any overflow issue, since absolute
sizes are subtracted there. So, except maybe for homogeneity with
mpz_cmp, it can keep using the optimized version.
Best regards,
Guillaume
___
gmp-devel mailing list
gmp-devel@gmplib.org
https://gmplib.org/mailman/listinfo/gmp-devel
Re: Overflow in mpz_cmp
Ciao, Il 2020-02-11 14:56 Marc Glisse ha scritto: On Tue, 11 Feb 2020, Niels Möller wrote: if (usize != vsize) return (usize > vsize) ? 1 : -1; On x86_64, both gcc and clang optimize (usize > vsize) ? 1 : -1 to 2 * (usize > vsize) - 1 (as a single LEA for gcc, 2 ADD for llvm). So the generated code may be just as good with the simple code. We know, optimising is a complex task, and we are not writing a compiler here. But it is funnier to observe how the compilers translate the last line of mpz/cmp.c: return (usize >= 0 ? cmp : -cmp); in the branches where the compiler "knows" that cmp is zero :-) Ĝis, m ___ gmp-devel mailing list gmp-devel@gmplib.org https://gmplib.org/mailman/listinfo/gmp-devel
Re: Overflow in mpz_cmp
Ciao, Il 2020-02-11 14:42 ni...@lysator.liu.se ha scritto: Marco Bodrato writes: diff -r f5601c2a8b11 mpz/cmp.c --- a/mpz/cmp.c Sun Feb 09 16:16:19 2020 +0100 +++ b/mpz/cmp.c Tue Feb 11 14:20:39 2020 +0100 @@ -35,15 +35,15 @@ + cmp = (usize > vsize) - (usize < vsize); + if (cmp != 0) +return cmp; I would be tempted to keep it simple, if (usize != vsize) return (usize > vsize) ? 1 : -1; It's not clear to me if this is worth micro optimizing, and ensure we get only a single branch. I believe that current compilers on modern architectures should compile the (usize > vsize)?1:-1 expression with no branches. I tested gcc on amd64 and on arm64, and on both archs your code is compiled with the single (usize != vsize) branch. Your proposal is simpler to read too. Ĝis, m -- http://bodrato.it/papers/ ___ gmp-devel mailing list gmp-devel@gmplib.org https://gmplib.org/mailman/listinfo/gmp-devel
Re: Overflow in mpz_cmp
On Tue, 11 Feb 2020, Niels Möller wrote:
Marco Bodrato writes:
Ciao,
Il 2020-02-10 18:25 Guillaume Melquiond ha scritto:
When the operand sizes do not match, the mpz_cmp function function just
returns the difference of the signed sizes. Unfortunately, this
difference might not fit inside the "int" return type, when the numbers
are of opposite sign.
In mini-gmp we defined a macro:
#define GMP_CMP(a,b) (((a) > (b)) - ((a) < (b)))
We may use the same idea here too. I mean something like the following:
diff -r f5601c2a8b11 mpz/cmp.c
--- a/mpz/cmp.c Sun Feb 09 16:16:19 2020 +0100
+++ b/mpz/cmp.c Tue Feb 11 14:20:39 2020 +0100
@@ -35,15 +35,15 @@
int
mpz_cmp (mpz_srcptr u, mpz_srcptr v) __GMP_NOTHROW
{
- mp_size_t usize, vsize, dsize, asize;
+ mp_size_t usize, vsize, asize;
mp_srcptr up, vp;
intcmp;
usize = SIZ(u);
vsize = SIZ(v);
- dsize = usize - vsize;
- if (dsize != 0)
-return dsize;
+ cmp = (usize > vsize) - (usize < vsize);
+ if (cmp != 0)
+return cmp;
I would be tempted to keep it simple,
if (usize != vsize)
return (usize > vsize) ? 1 : -1;
It's not clear to me if this is worth micro optimizing, and ensure we
get only a single branch.
On x86_64, both gcc and clang optimize (usize > vsize) ? 1 : -1 to 2 *
(usize > vsize) - 1 (as a single LEA for gcc, 2 ADD for llvm). So the
generated code may be just as good with the simple code.
--
Marc Glisse
___
gmp-devel mailing list
gmp-devel@gmplib.org
https://gmplib.org/mailman/listinfo/gmp-devel
Re: Overflow in mpz_cmp
Marco Bodrato writes:
> Ciao,
>
> Il 2020-02-10 18:25 Guillaume Melquiond ha scritto:
>> When the operand sizes do not match, the mpz_cmp function function just
>> returns the difference of the signed sizes. Unfortunately, this
>> difference might not fit inside the "int" return type, when the numbers
>> are of opposite sign.
>
> In mini-gmp we defined a macro:
> #define GMP_CMP(a,b) (((a) > (b)) - ((a) < (b)))
>
> We may use the same idea here too. I mean something like the following:
>
> diff -r f5601c2a8b11 mpz/cmp.c
> --- a/mpz/cmp.c Sun Feb 09 16:16:19 2020 +0100
> +++ b/mpz/cmp.c Tue Feb 11 14:20:39 2020 +0100
> @@ -35,15 +35,15 @@
> int
> mpz_cmp (mpz_srcptr u, mpz_srcptr v) __GMP_NOTHROW
> {
> - mp_size_t usize, vsize, dsize, asize;
> + mp_size_t usize, vsize, asize;
>mp_srcptr up, vp;
>intcmp;
>
>usize = SIZ(u);
>vsize = SIZ(v);
> - dsize = usize - vsize;
> - if (dsize != 0)
> -return dsize;
> + cmp = (usize > vsize) - (usize < vsize);
> + if (cmp != 0)
> +return cmp;
I would be tempted to keep it simple,
if (usize != vsize)
return (usize > vsize) ? 1 : -1;
It's not clear to me if this is worth micro optimizing, and ensure we
get only a single branch.
Regardsa,
/Niels
--
Niels Möller. PGP-encrypted email is preferred. Keyid 368C6677.
Internet email is subject to wholesale government surveillance.
___
gmp-devel mailing list
gmp-devel@gmplib.org
https://gmplib.org/mailman/listinfo/gmp-devel
Re: Overflow in mpz_cmp
Ciao,
Il 2020-02-10 18:25 Guillaume Melquiond ha scritto:
When the operand sizes do not match, the mpz_cmp function function just
returns the difference of the signed sizes. Unfortunately, this
difference might not fit inside the "int" return type, when the numbers
are of opposite sign.
In mini-gmp we defined a macro:
#define GMP_CMP(a,b) (((a) > (b)) - ((a) < (b)))
We may use the same idea here too. I mean something like the following:
diff -r f5601c2a8b11 mpz/cmp.c
--- a/mpz/cmp.c Sun Feb 09 16:16:19 2020 +0100
+++ b/mpz/cmp.c Tue Feb 11 14:20:39 2020 +0100
@@ -35,15 +35,15 @@
int
mpz_cmp (mpz_srcptr u, mpz_srcptr v) __GMP_NOTHROW
{
- mp_size_t usize, vsize, dsize, asize;
+ mp_size_t usize, vsize, asize;
mp_srcptr up, vp;
intcmp;
usize = SIZ(u);
vsize = SIZ(v);
- dsize = usize - vsize;
- if (dsize != 0)
-return dsize;
+ cmp = (usize > vsize) - (usize < vsize);
+ if (cmp != 0)
+return cmp;
asize = ABS (usize);
up = PTR(u);
diff -r f5601c2a8b11 mpz/cmpabs.c
--- a/mpz/cmpabs.c Sun Feb 09 16:16:19 2020 +0100
+++ b/mpz/cmpabs.c Tue Feb 11 14:20:39 2020 +0100
@@ -36,15 +36,15 @@
int
mpz_cmpabs (mpz_srcptr u, mpz_srcptr v) __GMP_NOTHROW
{
- mp_size_t usize, vsize, dsize;
+ mp_size_t usize, vsize;
mp_srcptr up, vp;
intcmp;
usize = ABSIZ (u);
vsize = ABSIZ (v);
- dsize = usize - vsize;
- if (dsize != 0)
-return dsize;
+ cmp = (usize > vsize) - (usize < vsize);
+ if (cmp != 0)
+return cmp;
up = PTR(u);
vp = PTR(v);
Ĝis,
m
___
gmp-devel mailing list
gmp-devel@gmplib.org
https://gmplib.org/mailman/listinfo/gmp-devel
