Computing the index of the biggest bit

mpz_sizeinbase(x,2) if the binding is added in Zarith.

For the lowest non-zero bit the usual "x && ~(x-1)" could improve things.

The interesting functions:

mpz_odd_p
mpz_even_p
mpz_sizeinbase
mpz_scan0
mpz_scan1

Les essaies sont dans la MR !4

J'ai essayé d'optimiser truncate avec mais les tests ne passe plus:

let rec truncate m a p =
  if Z.equal a Z.zero then zero else
    let last = Z.findlastset a in (* of the absolute value *)
    let first = Z.findfirstset a in
    let i = max first (last-(m-1)) in
    (Z.shift_right_trunc a i,p+i)

let m32 = 24
let m64 = 53

let round_f32 (a,p) = truncate m32 a p
let round_f64 (a,p) = truncate m64 a p

let round ?(bits=80) (a,p) = truncate bits a p

Par contre pour oddify cela accélère bien.

Tu peux aussi utiliser Int64 directement je ne suis pas sûre que tu sois perdant.

Before having this binding, we can improve the current implementation with dichotomy in many places (see for instance log2 in F.ml).

A similar issue is about finding the lowest non-zero bit, which can speed the oddify normalizer in F.ml.

Added Feature label

Oui effectivement, j'attend avec impatience ces bindings.

first est inutile, c'est toujours 0. Je veux bien regarder le log si tu veux.

J'ai ajouté des benchs pour voir. Cf. https://git.frama-c.com/soprano/farith/tree/feature/truncate

Je reprends les lignes suivantes:

┌─────────────────────────────────────┬─────────────┬───────────┐
│ 1.00e+00+.1.00e-08/Farith.B64.add   │ 14_742.23ns │ 2_851.02w │
│ 1.00e+00+.1.00e-08/Farith.B64.round │  2_163.40ns │    86.00w │
│ 1.00e+00+.1.00e-08/F.add+F.round    │  1_385.94ns │   174.00w │
│ 1.00e+00+.1.00e-08/F.add            │     52.83ns │    15.00w │
│ 1.00e+00+.1.00e-08/F.round          │  1_336.67ns │   159.00w │
│ 1.00e+00+.1.00e-08/F.of_float       │ 14_370.68ns │ 1_390.00w │
│ 1.00e+00+.1.00e-08/Q.of_float       │    298.82ns │    16.00w │
└─────────────────────────────────────┴─────────────┴───────────┘

F.round est sans surprise assez coûteux, sans doute à cause du truncate bits-à-bits (Cf. !4)

La décomposition d'un rationnel Q en flottant est clairement la plus coûteuse. @melquiond tu connais un algo malin pour faire ça ?

À ma connaissance, il n'y a pas d'algorithme malin. La conversion d'un rationnel vers un flottant revient toujours tôt ou tard à faire une division entière entre un nombre de p + k bits par un nombre de k bits. Il y a quelques optimisations triviales qui prennent en compte les zéros présents à la fin des nombres afin d'éviter de diviser ou de décaler des nombres artificiellement grands. Il y a une optimisation beaucoup plus subtile qui consiste à détecter qu'il est possible de faire une division de p + k par k + 1, mais je ne crois pas qu'elle en vaille la peine au niveau performance.

Par contre, il y a évidemment toutes les optimisations de la division entière, mais ça c'est le boulot de GMP, ça ne nous concerne pas.

Pour F.of_float/to_float, autant utiliser du C et aller décoder le double de OCaml à main:

struct FP64
{
  unsigned long mantissa : 52;
  unsigned int exponent : 11;
  unsigned int sign : 1;
};

union FP { struct FP64 bits ; double value ; };

void decode(double u)
{
  union FP w ;
  w.value = u ;
  printf("S: %d\n", w.bits.sign);
  printf("E: %d\n", w.bits.exponent);
  printf("M: %lu\n", w.bits.mantissa);
}

C'est un peu tricky mais effectivement ça marche et c'est dans !8 (merged)

Computing the index of the biggest bit

Designs

Child items ...

Activity