Search code examples
static-analysisframa-c

Introduce maths-functions specifications with ACSL/Frama-C

Is it possible to implement specifications in ACSL for functions usually called at compiling with -lm, as sqrt ? I am using it for Frama-C's plug-in WP.

Here is a small example to illustrate what I would want to do.

/*@ requires sqrt_spec: \forall float x; 
             \model(sqrt(x)) * \model(sqrt(x)) == \model(x);  
    ensures [...] */  

void f (...) {
double y = sqrt x;
[...]
}

Obviously, if I do this WP cries because sqrt doesn't exist when I use it in annotations.

[kernel] user error: unbound function sqrt in annotation

So I would like to define an abstract sqrt, but none of my tests worked :

#define sqrt(x) (...)

For this one I don't see what I could put in (...) as I want a abstract definition instead of re-implementing the whole float sqrt.

/*@  axiomatic SqrtSpec {
logic real sqrt (real x);
} */

And this one doesn't solve my problem :

Neither code nor specification for function sqrt, generating default assigns from the prototype.

Solution

  • Frama-C has a built-in logic function \sqrt that operates over real number (note that built-in functions and predicates usually are prefixed with a backslash \ to avoid any collision with existing C identifiers). That said, it is not that difficult to provide an axiomatic definition for sqrt:

    axiomatic Sqrt {
  logic real sqrt(real);
  axiom real_def: \forall real x; x >= 0 ==> x == sqrt(x) * sqrt(x);
}

    Note in addition that Gappa (http://gappa.gforge.inria.fr/) is about the only automated prover that knows about floating-points (as opposed to real numbers), but even if you have installed it, discharging proof obligations dealing with floating point computations can be very hard.

    Update

    If you want to axiomatize double sqrt(double) (and/or float sqrt(float)), the idea would be to characterize the error relative to the result of \sqrt operating on reals, i.e. something akin to

    axiomatic Sqrt {
  logic float sqrt(float sqrt);
  axiom sqrt_def: \forall float x; \is_finite(x) && x>= 0.0 ==> sqrt(x) ==  (float)\sqrt(x);
}

    Of course, this characterization might be a bit restrictive. You might want something like \abs(sqrt(x) - \sqrt(x)) <= err_bound * \sqrt(x), but I have to admit that I'm not fluent enough in floating-point computations to give the appropriate value of err_bound from the top of my head.

    Update 2

    Assuming that you have a logic sqrt that has the properties you want, saying that the C sqrt has the same behavior is simply a matter of giving a contract to it:

    /*@ requires \is_finite(x); //unless you want to play with NaN or infinities 
    assigns \nothing;
    ensures \result == sqrt(x);
 */
extern float sqrt(float x);

    Specifications of a function are merged during the link phase, so that it does not matter whether this contract is written in math.h (NB: in the standard header sqrt takes (and returns) a double, it is sqrtf that operates on float) or in your own file.