Frama-C-discuss mailing list archives

boris at yakobowski.org (Boris Yakobowski) · Thu, 21 Apr 2016 18:13:22 +0200

Hello,

I'm going to complement LoÃ¯c's answer by explaining how to set up Value so
that everything gets proven automatically. Value is not able to prove the
precondition of sqrt because f computes a non-linear expression (x*x+y*y).
This kind of expression cannot be analysed precisely by the interval
analysis that Value uses for floating-point values.

That being said, an option is available to improve precision on such
formulas: -val-subdivide-non-linear. This option instructs Value to
subdivide variables that appear multiple times in an expression into a
disjoint union of intervals, and to perform the evaluation pointwise. By
setting N high enough, it becomes possible to prove that e.g. x*x is always
positive. The option was originally named -subdivide-float-var, but was
renamed because it now also applies to integers. You will find more
information on the original option there:
http://blog.frama-c.com/index.php?q=subdivide.

Regarding the expressiveness of this option, the current versions of
Frama-C are not able to handle expressions that are non-linear on multiple
variables, such as x*x+y*y. Support for these expressions will be available
in Frama-C Silicon, though. (We actually added this support in the last
month.) The current versions of Value are able to prove your second version
of f (with intermediate variables), because each temporary is linear on one
variable.

Finally, notice there exists a Value builtin for sqrt, that can be
activated through option -val-builtin sqrt:Frama_C_sqrt. This way, you will
get tighter bounds for the results of sqrt. For technical reasons, this
builtin does *not* check the preconditions present in the source, but
verify by itself the domain of its argument.

Hope this helps!

On Thu, Apr 21, 2016 at 4:34 PM, Maurice Bremond <Maurice.Bremond at inria.fr>
wrote:

>
> 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

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

Frama-C-discuss mailing list archives

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