Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] hint assertions and understanding cooperation between wp and value plugin
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Sun, 1 May 2016 22:24:40 +0200
  • In-reply-to: <87fuu82u9r.fsf@inria.fr>
  • References: <87fuu82u9r.fsf@inria.fr>
Hi again,

Regarding WP, as you understood, the Real model is unsound for your lemma
/*@ lemma sq_double: \forall real x; x*x - .2 * x + 0.01 >= 0.; */
You will have to use the Float model for such a proof. And then the proof
will fail (hopefully!), since this property is false.

> is verifiable and value analysis shows that x*x >= 0
> with -val-subdivide-non-linear 1094

This setting (1094) seems a bit high for such a simple formula. Out of
curiosity, what were the possible values for x?

> On the other side, (x - .1)*(x - .1) >= 0 is verifiable with -wp
> -wp-model float but I did not manage to verify it with the value plugin
> alone and -val-subdivide-non-linear (I stopped the computation after
> 99999)

Again, this is a bit strange. I'm able to analyse the following program and
prove that r >= -0. using -val-subdivide-non-linear 1080. You may obtain
different results with different bounds for x, because the subdivision
strategy depends on the initial interval. However, there should be no need
to go to extreme values such as 99999.

void main(double x) {
  double r = (x - .1)*(x - .1);
}


Regarding x*x - .2 * x + 0.01 >= 0., I tried to see if I could *dis*prove
it using Value, and then find the best possible bound, using
-val-subdivide-non-linear for both. These are the results of my
investigation:

1. the current algorithm is unsuitable for very high arguments (say >
10.000). From an algorithmic standpoint, the list of intervals that remain
to be considered should be replaced by a heap. We will improve this for
Frama-C Silicium. All my experiments were carried out with such a heap

2. the detection that no further improvement can be made to the final
result could also be improved. For example consider:

void main(float x) {
  float r = x * x - 0.2 * x + 0.01;
}

I believe that the tightest lower bound for r is -0x1.70a3d8p-32. The
current version of -val-subdivide-non-linear fails to notice that this
value must be in the result  and keeps subdividing intervals -- even though
their image is included in [ -0x1.70a3d8p-32 .. \infty]. This is
inefficient, as bigger arguments to -val-subdivide-non-linear will result
in longer analysis times without any final gain in precision.

3. Value and -val-subdivide-non-linear find values that refute x*x - .2 * x
+ 0.01 >= 0. ; for example r = -0x1.0p-59, obtained for x = 0x1.9999998p-4
after 43626 subdivisions. However,  this information is not available to
the user. This is due to the fact that -val-subdivide-non-linear is not
goal-directed. Also, Value is designed to over-approximate, while we need
an *under*-approximation in this case.

4. finding the tightest possible bound using variables of double type is
out-of-reach with this approach. The best results I obtained, after
2.500.000 subdivisions and around 1h30 of computation, were r >=
-0x1.3ad1000000000p-43 -- while I suspect the maximally negative value is
-0x1.0000000000000p-59. After 1.000.000 subdivisions (38 minutes), the best
bound is -0x1.994bffffff08dp-41. So the convergence is slow. This is to be
expected given the algorithm and the search space.

5. on the other hand, with variables of float type, an exhaustive search is
possible (and fast!) on this example: less than 3s. This is how I derived
the bound for point 2. This unfortunately does not generalize to
expressions such as x * x - 0.2 * x + 0.01 - (x-0.1)*(x-0.1) in which the
numeric "noise" is prominent, though.

In any case, thanks for this very interesting example!


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