-
Augustin Lemesle authoredAugustin Lemesle authored
2011-03-23-Helping-the-value-analysis-part-1.html 6.00 KiB
---
layout: post
author: Pascal Cuoq
date: 2011-03-23 17:00 +0200
categories: floating-point value
format: xhtml
title: "Helping the value analysis — part 1"
summary:
---
{% raw %}
<h2>Introduction</h2>
<p>This post introduces a new series about the
art of helping the value analysis to be more precise.
Until now, in the numerical precision series of this blog,
this was easy enough.
There was a single input variable and the obvious way to get
more precise output values was to subdivide the range for that
input variable. Sometimes, it is more complicated.</p>
<h2>The example</h2>
<p>The example we are going to look at in this series
is an interpolation function. It is similar to <a href="index.php?post/2011/02/10/Verifying-numerical-precision-part-2" hreflang="en">the sine example seen previously</a> but here the divisions of the function's
definition interval are not uniform. The sub-intervals on which the
function is implemented as a linear interpolation have been carefully
chosen by the designers to minimize the occupied memory while providing
appropriate precision.</p>
<pre>struct point { double x; double y; };
struct point t[] =
{ 0. 1.
0.125 1.00782267782571089
0.25 1.03141309987957319
0.5 1.1276259652063807
1. 1.54308063481524371
2. 3.76219569108363139
5. 74.2099485247878476
10. 11013.2329201033244 };
</pre>
<p>The interpolation function calls function <code>choose_segment</code> to get an index <code>i</code> indicating the segment to use. It then computes its result by interpolation
of <code>x</code> between the points <code>t[i]</code> and <code>t[i+1]</code>.</p>
<pre>/*@ requires 0. <= x <= 10. ; */
double interp(double x)
{
double x0 x1 y0 y1;
int i;
i = choose_segment(x);
x0 = t[i].x;
y0 = t[i].y;
x1 = t[i+1].x;
y1 = t[i+1].y;
return (y1 * (x - x0) + y0 * (x1 - x)) / (x1 - x0);
}
</pre>
<p>We are supposed to verify that function <code>interp</code> above is <strong>free of run-time errors</strong> but auxiliary function <code>choose_segment</code>
is not yet available for some reason. All we have is the specification it
is supposed to satisfy.</p>
<p>Part of the specification has been formally written in ACSL:</p>
<pre>/*@
requires 0. <= x <= 10. ;
assigns \
othing ;
ensures 0 <= \esult <= 6 ; */
int choose_segment(double x);
</pre>
<p>Of course this ACSL specification of <code>choose_segment</code> is partial: it
does not completely caracterize what the function is supposed to do (the function is supposed to
select the right segment not just any segment which is what the
ACSL contract says).
Nevertheless if we can verify the safety of function <code>interp</code> using
only this contract for function <code>choose_segment</code> it will be a
feather in our cap and we will only need to check that
<code>choose_segment</code> statisfies its own specification when it finally arrives.</p>
<h2>First analysis</h2>
<p>The first step is always to launch an imprecise analysis to gauge the
situation:</p>
<pre>frama-c -val -main interp interp.c
</pre>
<p>Four messages in the log are related to the verification process:</p>
<pre>interp.c:20:[value] Function interp: precondition got status unknown
</pre>
<p>This is the pre-condition for the function we are verifying. It is normal for this property not to be verified: it is <code>interp</code>'s callers' job to make sure that the condition expressed here is met.</p>
<pre>interp.c:24:[value] Function choose_segment: precondition got status valid
</pre>
<p>The value analysis has verified that auxiliary function <code>choose_segment</code> was called in the conditions defined by its contract.</p>
<pre>interp.c:24:[value] Function choose_segment: postcondition got status unknown
</pre>
<p>Again it is normal for the annotation here not to be verified: it is supposed to be ensured by <code>choose_segment</code>'s body which is not available.</p>
<pre>interp.c:28:[kernel] warning: float operation: assert \is_finite((double )((double )((double )(y1*(double )(x-x0))+(double ) (y0*(double )(x1-x)))/(double ) (x1-x0)));
</pre>
<p>Because of subtle differences between ACSL and C a lot of casts have been
inserted but this assertion means the analyzer is worried that the value
computed by the function to be returned might be an infinite or NaN.</p>
<p>Inspecting the toplevel operation in the formula (which is the
problematic one: the value analysis would warn individually about
sub-expressions if it thought one contained an additional problem) we
see it is a division by <code>x1 - x0</code>. An issue would be if this
expression was zero or unreasonably close to zero. Further inspection
shows that <code>x0 = t[i].x</code> and <code>x1 = t[i+1].x</code>. From this we deduce
that <code>x1</code> is always strictly greater than <code>x0</code> and more
specifically that <code>x1 - x0 >= 0.125</code> which should preclude any possibility
of overflow considering that the values for variables <code>y0</code> and <code>y1</code> cannot be unreasonably large themselves.</p>
<h2>What next?</h2>
<p>We could stop here if we wished: there was a single place the value analysis
was worried about and we have used a code review to check that the
dangerous-looking operation was indeed safe. This is a standard way
of proceeding especially for non-critical code. However the reasoning
we made to reach the conclusion that the division was safe is informal
and there could be a mistake in it. In a next post we will try to make the
analysis say that the division is safe which will be more satisfying.
<a href="/assets/img/blog/imported-posts/interp.c">Here is the file</a> in case you wish to try it at home. Another possible exercise if to complete the contract of <code>choose_segment</code> and/or implement it. If you do both you can check your implementation against your specification with a deductive verification plug-in.</p>
<p>This post is co-authored by Kerstin Hartig.</p>
{% endraw %}