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 u
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
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 t
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 mi
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
gen
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)
+
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 th
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 nu
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 min
