Frama-C:
Plug-ins:
Libraries:

Frama-C API - IEEE754

The goal of this module is to provide a way to build a sound overapproximation of the semantics of IEEE-754 correctly rounded operations for floating-point formats supported by the C language.

To do so, set of floating-point numbers are soundly abstracted by a triplet composed of:

  • an abstraction \mathbb{R}(x) of the theoretical computation of x using real numbers;
  • an abstraction \varepsilon_a^f(x) of the absolute errors committed when computing x using floating-point numbers in the format f;
  • an abstraction \varepsilon_r^f(x) of the relative errors committed when computing x using floating-point numbers in fhe format f.

Two sound abstract overapproximations of sets of real numbers are required to build a sound overapproximation of IEEE-754 semantics. The first one, called \mathbb{A}, is used to abstract the real numbers and the absolute floating-point errors. As absolute error semantics is mostly linear, it is preferable to provide an abstraction as precise as possible on linear operations, like affine forms for example. The second required abstraction, called \mathbb{M}, is used to abstract the relative errors. As their semantics heavily relies on multiplications and divisions, it is preferable to provide an abstraction as precise as possible on those operations, like the relative forms described here. Moreover, the relative error semantics for additions and subtractions is defined based on an expression of the form (ax \pm by) / (x \pm y). This expression can be precisely computed even in intervals, as described here, and is optimal if there is no relation between a, b, x and y. Thus, an implementation of this computation is also required.

Another key part of the precision of the built semantics is the relations between absolute and relative errors. Indeed, each one can be derived from the other as follows:

  • \varepsilon_a^f(x) = \mathbb{R}(x) \varepsilon_r^f(x)
  • \varepsilon_r^f(x) = \varepsilon_a^f(x) / \mathbb{R}(x)

Thus, a sound abstraction of those computations are required to define a correct reduced product between the two error abstractions. As one may need to partially or totally disable this reduced product, for experimentation purposes for instance, two functions are required to build the semantics, returning true if the absolute (resp. relative) error should be reduced using the other.

Finally, as relational abstractions may need to keep track of each source of floating-point errors (i.e. each elementary error), one is also asked to provide a constructor for absolute and relative abstractions, that returns a symmetric and tracked if needed abstraction based on a given positive bound.

All the required components form together an abstract Model, as described by the Modeling signature described in IEEE754_sig. Note that both in this file and in IEEE754_sig, the types use to represent the exact and the absolute errors semantics are required to be the same. It is, in theory, not mandatory. However, in practice it complexifies quite a lot both the signatures and the implementation without providing much use.

All necessary types and signatures are declared in a separated file to avoid duplications, and included here to simplify their use.

include module type of IEEE754_sig

Miscellaneous definitions.

type 'a correctly_rounded_expression =
  1. | Cast of 'a
  2. | Sqrt of 'a
  3. | Add of 'a * 'a
  4. | Sub of 'a * 'a
  5. | Mul of 'a * 'a
  6. | Div of 'a * 'a

Type encoding correctly rounded operations. Values of this type are provided to the model when asked to represent elementary rounding errors. Relational abstractions may use them to keep track of the relations between rounding errors during the analysis.

type resulting_format =
  1. | Format : 'f Frama_c_kernel.Typed_float.format -> resulting_format

Existential type on format.

module type Computation = sig ... end

Abstract values may be context dependent, which can be easily represented using a monad. This signature extends monads signature with a resolve function, that must be able to concretize a monadic computation on a given context.

Abstract representation of subsets over a field.

module type Abstraction = sig ... end

Modeling used to abstract the IEEE-754 semantics.

module type Modeling = sig ... end

Functor building the IEEE-754 abstract semantic.

module Make (Model : Modeling) : sig ... end