[kernel] Fixes issue 1494

Closes #1494

See merge request frama-c/frama-c!4931

Feature/libc/assigns trace h

See merge request frama-c/frama-c!4929

[libc] add some tests based on manpages

See merge request frama-c/frama-c!4928

Rewriting [Floating_point] module

See merge request frama-c/frama-c!4696

Only changes the rounding mode if needed (if the new rounding mode is different
from the current one).

Maxime Jacquemin authored 1 month ago and David Bühler committed 1 month ago

As the format is not supported for now, we have removed it.
Witnesses are provided to represent the fact that long
floats are encoded as double. The doc is not yet updated.

Also renames round_to_single_precision_float into round_to_single_precision.

Floating_point contains utilitary functions over ocaml float.
Typed_float provides a typed representation of floating-point numbers, which
encodes the format of the represented number.

Maxime Jacquemin authored 5 months ago and David Bühler committed 1 month ago

The parser used to always assign the [lower], [nearest] and [upper]
to the same constant for any hexadecimal float. Which is obviously
wrong.

It is fixed by using [float_of_string] and rounding modes to compute
upper and lower bounds.

Maxime Jacquemin authored 5 months ago and David Bühler committed 1 month ago

Asked as a helper function to minimize modifications and ensures
backward compatibility. Will be removed when every thing relies
and the typed floats, which means probably never.

Maxime Jacquemin authored 5 months ago and David Bühler committed 1 month ago

The loops use to adjust the exponent, the numerator and the denominator
can take a long time (more than 200000 iterations) for numbers with a
large exponent, for instance 1e99999. This is trivially not
representable as a double but the loops are too long to figure it out.

Those loops are here because the actual fast and correct way to make
the adjustement requires to compute a number δ using binary logarithms,
and more specifically the ceiling of the difference of two binary logs.
This computation cannot be done exactly, as Zarith only provides (which
is absolutly normal, don't get me wrong) a rounded down approximation of
the binary log of any given integer. However, it can still be used to
compute an underapproximation of the exponent that will be produced by
the loops. And computing this underapproximation is trivially fast.
We can thus use this underapproximation to check if the number will
be a positive infinite in no time, avoiding the loop and thus the DoS.

An important point is that this method is correct. Proving that the
proposition "δ is larger than the maximal exponent" implies that
"the parsed number is infinity" is not hard and is underlined in the
comments of the parsing function.

Maxime Jacquemin authored 6 months ago and David Bühler committed 1 month ago

Plus a little fix (a Kernel.failure that became a Kernel.log)

Maxime Jacquemin authored 6 months ago and David Bühler committed 1 month ago

- Renaming [round_to] as [change_format] to avoid confusion with [round]
- Renaming [of_float] as [represents ~float ~in_format] to better convey
  the goal of this module and why we hide the float type
- Adding [@@noalloc] to external functions [set_rounding_mode] and
  [get_rounding_mode] as a (rather small) optimisation

Maxime Jacquemin authored 6 months ago and David Bühler committed 1 month ago

- Bug fix in [single_precision_of_string]
- Removing unused [frama_c_sqrt]
- Adding default cases to all switch to catch erronous inputs

Maxime Jacquemin authored 7 months ago and David Bühler committed 1 month ago

The module now handles explicitly the floating point formats using the
type system, thus ensuring strict manipulation of float numbers.

Regroup all arithmetic modules in one place

See merge request frama-c/frama-c!4923

- Using Q.mul_2exp for pow2
- Simpler and correct implementation for log2
- Declaring the ten constant only once