Frama-C-discuss mailing list archives

loic.correnson at cea.fr (Loïc Correnson) · Thu, 21 Apr 2016 17:18:23 +0200

The reason for the needed cooperation of WP and Value on this example is quite simple :
 - WP fails into proving that the sum of squares is finite, while Value succeed provided they are positive
 - WP succeed into proving that a square is positive, while Value fails because of a `-0.0` lower bound (see the GUI)

Inserting the assertions make the separation of concerns explicit, and each plug-in works separately, recovering knowledge from each others.
Hence, combining the two, you succeed.

However, one may argue that there is surely something wrong with the `-0.0` lower bound.
Notice also that the default model for WP on float is to compute over reals, without any rounding...

Another way to ease the cooperation is to spread the properties over multiple ensures and requires :

/*@                                                                             
 requires \is_finite(x) ;                                                       
 requires x >= 0.;                                                              
 assigns \nothing;                                                              
 ensures \is_finite(\result);                                                   
 ensures 0. <= \result <= 1 + x;                                                
*/
extern double sqrt(double x);

/*@ requires -1.0e+6 <= x <= 1.0e+6;                                            
   requires -1.0e+6 <= y <= 1.0e+6;                                             
   assigns result[0];                                                           
   ensures \is_finite(result[0]); */
void f(double x, double y, double *result)
{
  *result = sqrt(x*x+y*y);
}

This, way, you donâ€™t need intermediate assertion at all.
Using the GUI, you can inspect which property has been proven by each plug-in.

	L.

> Le 21 avr. 2016 Ã  16:34, Maurice Bremond <Maurice.Bremond at inria.fr> a Ã©crit :
> 
> 
> Hello, 
> 
> Considering C implementations of some real-valued functions, I would
> like to have an automated proof that, for some correctly bounded
> numerical inputs within the function domain, only finite results are
> returned.
> 
> Here is a simple example with the implementation of the 2D Euclidian
> norm below:
> 
> void f(double x, double y, double *result)
> {
>  *result = sqrt(x*x+y*y);
> }
> 
> Being interested only on the [-1e6, 1e6]^2 domain and guessing that, on
> this domain, the computation should not overflow, my first attempt is to
> write:
> 
> #include <__fc_builtin.h>
> /*@
>  requires \is_finite(x) && x >= 0.;
>  assigns \nothing;
>  ensures \is_finite(\result) && 0. <= \result <= 1 + x;
> */
> extern double sqrt(double x);
> 
> 
> /*@ requires -1.0e+6 <= x <= 1.0e+6;
>    requires -1.0e+6 <= y <= 1.0e+6;
>    assigns result[0];
>    ensures \is_finite(result[0]); */
> void f(double x, double y, double *result)
> {
>  *result = sqrt(x*x+y*y);
> }
> 
> int main()
> {
>  double x =  Frama_C_double_interval(-1.0e+6, 1.0e+6);
>  double y =  Frama_C_double_interval(-1.0e+6, 1.0e+6);
>  double result[1];
>  f(x, y, result);
> }
> 
> 
> I run frama-c (Magnesium + alt-ergo 1.01) like this:
> 
> frama-c -val t.c -wp -wp-alt-ergo-opt="-backward-compat" -then -report
> 
> Unfortunately, the precondition on sqrt, x*x + y*y >= 0, cannot be
> verified. Trying with other solvers (z3, cvc4, cvc3, zenon) and
> incrementing the timeout does not help.
> 
> With the insertion of intermediate assertions, as hints, the wp plugin
> alone is not able to validate the sqrt precondition but is able to
> validate the assertions, the value plugin cannot validate the inserted
> assertions but, with the results of the wp plugin, is able to validate
> the sqrt precondition.
> 
> /*@ requires -1.0e+6 <= x <= 1.0e+6;
>    requires -1.0e+6 <= y <= 1.0e+6;
>    assigns result[0];
>    ensures \is_finite(result[0]); */
> void f(double x, double y, double *result)
> {
>  double x1 = x*x;
>  /*@ assert x1 >= 0; */
> 
>  double x2 = y*y;
>  /*@ assert x2 >= 0; */
> 
>  *result = sqrt(x1+x2);
> }
> 
> I have two questions: 
> 
> - this seems to show the necessary cooperation of the value plugin and
>   the wp plugin but it is not clear to me why such a cooperation is
>   needed, can you give me some hints to understand why the wp plugin
>   alone cannot validate the sqrt precondition and why the value plugin
>   is unable to validate the inserted assertions ? More generally,
>   should we explore the function expression tree to insert intermediate
>   variables with assertions on known facts that may probably be
>   verifiable by only the wp plugin ?
> 
> - the alt-ergo file for the second assertion is not the same as the
>   first one. I understand that the first assertion is "embeded" in
>   the second one (*). How to "isolate" each assertion from the other
>   one, or in other words, how to tell frama-c and the external
>   provers that, for me and the problem I consider, the order of
>   computation of x1 and x2 does not matter ? 
> 
> 
> Regards, 
> 
> Maurice Bremond
> 
> 
> (*) the alt-ergo files for the 2 assertions:
> 
> (* ---------------------------------------------------------- *)
> (* --- Assertion (file t.c, line 23)                      --- *)
> (* ---------------------------------------------------------- *)
> 
> goal f_assert:
>  forall r_1,r : real.
>  let r_2 = (r_1 * r_1) : real in
>  ((-1000000.0e0) <= r) ->
>  ((-1000000.0e0) <= r_1) ->
>  (r <= 1000000.0e0) ->
>  (r_1 <= 1000000.0e0) ->
>  is_float64(r) ->
>  is_float64(r_1) ->
>  is_float64(r_2) ->
>  (0.0 <= r_2)
> 
> 
> (* ---------------------------------------------------------- *)
> (* --- Assertion (file t.c, line 26)                      --- *)
> (* ---------------------------------------------------------- *)
> 
> goal f_assert_2:
>  forall r_1,r : real.
>  let r_2 = (r_1 * r_1) : real in
>  let r_3 = (r * r) : real in
>  ((-1000000.0e0) <= r) ->
>  ((-1000000.0e0) <= r_1) ->
>  (r <= 1000000.0e0) ->
>  (r_1 <= 1000000.0e0) ->
>  is_float64(r) ->
>  is_float64(r_1) ->
>  (0.0 <= r_2) ->
>  is_float64(r_3) ->
>  is_float64(r_2) ->
>  (0.0 <= r_3)
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160421/b4c90845/attachment-0001.html>

Frama-C-discuss mailing list archives

[Frama-c-discuss] hint assertions and understanding cooperation between wp and value plugin