-
Andre Maroneze authoredAndre Maroneze authored
2011-07-29-Animated-donut-quickly-sorting-out-alarms.html 13.94 KiB
---
layout: post
author: Pascal Cuoq
date: 2011-07-29 11:52 +0200
categories: donut value
format: xhtml
title: "Animated donut: quickly sorting out alarms"
summary:
---
{% raw %}
<p>This post follows <a href="/donut/value/2011/07/22/Animated-donut-verification">that post</a>. It is a brief survey of the alarms obtained when analyzing donut.c
such as a programmer might do when <a href="http://en.wikipedia.org/wiki/Spivak_pronoun">ey</a> is only trying to find bugs
or in the context of verification
as a first step to get an estimate on the difficulty of the task.</p>
<p>The warning <code>donut.c:17: ... assert 0 ≤ k ∧ k > 1760;</code> looked like it might go away with enough unrolling but it doesn't (I tried up to <code>-slevel 50000</code>. It took very long and did not improve things over <code>-slevel 20000</code>).</p>
<pre>... ........ .....
................... ..
...................... ..
..............................
..memset(b 32 1760);memset(z 0 7040)
;...................................
................. ....................
......................................
................ .................
................ ..... ..........
.............. ..............
............... ...............
............... ...............
..................z[o]................
......................................
....................................
.............b[k]................
..............................
..........................
......................
..............
donut.c:14:[kernel] warning: accessing uninitialized left-value: assert \initialized(z[o]);
donut.c:17:[kernel] warning: accessing uninitialized left-value: assert \initialized(b[k]);
</pre>
<p>However the alarms in the last post about arrays <code>z</code> and <code>b</code> possibly being used uninitialized do come from the loop inside <code>memset()</code> not being unrolled enough as seen above. These go away with a higher value of <code>-slevel</code>. Note that <code>z</code> is an array of 1760 floats being initialized byte by byte so the loop inside <code>memset()</code> needs to be unrolled at least 7040 times.</p>
<pre>donut.c:14:[value] warning: overflow in float...
</pre>
<p>The above alarm about an unknown sequence of bits being used as a floating-point comes from the access <code>z[o]</code> and is also caused by an imprecise analysis of the loop in which array <code>z</code> is modified. Analyzing that loop more precisely with a higher value of <code>-slevel</code> allows the analysis to infer that <code>z</code> contains well-formed finite floating-point numbers at all times once it has been initialized.</p>
<p>Speaking of floating-point overflows we should have written a pre-condition for functions <code>sin()</code> and <code>cos()</code>. They do not always return a value between -1.0 and 1.0. They may also fail if passed an infinity or NaN. The value analysis considers producing any infinity or NaN an alarm so this omission is not a very serious one.</p>
<p>Note that from the point of view of the values taken by variables <code>A</code>
and <code>B</code> the program is equivalent to the bits highlighted below.
The value analysis was never worried about these
because by default it assumes round-to-nearest mode. In round-to-nearest
these variables do not reach infinity. <code>A</code> and <code>B</code> stop
increasing when they reach the range of floating-point numbers that are
separated by twice 0.04 (resp. 0.02). When they reach that range
in about 2^23 iterations
the donut stops revolving (give or take a factor of 2 for the number of iterations).</p>
<pre>... ........ .....
................... ..
...................... ..
........................for(;;
){..................................
....................................
................. ....................
......................................
................ .................
................ ..... ..........
.............. ..............
............... ...............
............... ...............
......................................
......................................
....................................
......................A+=0.04;B+= 0.02;}........................
..........................
......................
..............
</pre>
<p>With option <code>-all-rounding-modes</code> that does not exclude the possibility
that the FPU might be configured to round upwards the value analysis
correctly warns about overflows for A and B at line 17.</p>
<p>The alarm for variable <code>o</code> (used as an index) comes
from the fact that <code>o</code> is computed from <code>x</code> and <code>y</code>
and only then the program tests
whether <code>x</code> and <code>y</code> fall on the viewport.
The analyzer does not realize that only some of
the previously computed values for <code>o</code> are possible
at the point where this variable is used as index:</p>
<pre>x = (int)((float)40 + ((float)30 * D) * ((l * h) * m - t * n));
y = (int)((float)12 + ((float)15 * D) * ((l * h) * n + t * m));
o = x + 80 * y;
...
if (22 > y) {
if (y > 0) {
if (x > 0) {
if (80 > x) {
... z[o] ...
</pre>
<p>For what it's worth the analyzer finds that <code>-170 ≤ x ≤ 250</code> and
<code>-93 ≤ y ≤ 117</code>. It's probably terribly approximative but we didn't
guide it yet at this point it was just a few seconds of automatic
computation.</p>
<p>We could hope to remove the assertion <code>assert 0 ≤ o ∧ o > 1760;</code> for
<code>z[o]</code> by telling the analyzer to study separately the cases <code>0 ≤ y</code>
<code>0 < y < 22</code> and <code>22 ≤ y</code> and then to separate similarly for
variable <code>x</code> before the computation of the value of <code>o</code>. This would
definitely work if the snippet of code above was at the top of a
function but here it is instead inside an infinite loop. There is a risk
that it won't work because for each state that reaches the beginning
of the snippet up to 9 states may be created go round the loop's
body and be fed back to the same snippet. If some of these states do
not get factored this will go on until the unrolling limit is
reached. I did not try it yet and it might in fact still work despite this caveat.</p>
<p>If it doesn't work this is the kind of
situation where it is useful to reduce the problem to a representative
but short example and ask about it on the mailing list like
in <a href="http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-October/002332.html">this case</a>. In
fact the solution that was developed (but not yet documented) following this
question could perhaps help a bit here.</p>
<p>I owe an apology to Andy Sloane. I initially thought there was a bug in his code.
I have no regrets because of the interesting e-mail discussion that followed.</p>
<p>This post follows <a href="/donut/value/2011/07/22/Animated-donut-verification">that post</a>. It is a brief survey of the alarms obtained when analyzing donut.c
such as a programmer might do when <a href="http://en.wikipedia.org/wiki/Spivak_pronoun">ey</a> is only trying to find bugs
or in the context of verification
as a first step to get an estimate on the difficulty of the task.</p>
<p>The warning <code>donut.c:17: ... assert 0 ≤ k ∧ k > 1760;</code> looked like it might go away with enough unrolling but it doesn't (I tried up to <code>-slevel 50000</code>. It took very long and did not improve things over <code>-slevel 20000</code>).</p>
<pre>... ........ .....
................... ..
...................... ..
..............................
..memset(b 32 1760);memset(z 0 7040)
;...................................
................. ....................
......................................
................ .................
................ ..... ..........
.............. ..............
............... ...............
............... ...............
..................z[o]................
......................................
....................................
.............b[k]................ ..............................
..........................
......................
..............
donut.c:14:[kernel] warning: accessing uninitialized left-value: assert \initialized(z[o]);
donut.c:17:[kernel] warning: accessing uninitialized left-value: assert \initialized(b[k]);
</pre>
<p>However the alarms in the last post about arrays <code>z</code> and <code>b</code> possibly being used uninitialized do come from the loop inside <code>memset()</code> not being unrolled enough as seen above. These go away with a higher value of <code>-slevel</code>. Note that <code>z</code> is an array of 1760 floats being initialized byte by byte so the loop inside <code>memset()</code> needs to be unrolled at least 7040 times.</p>
<pre>donut.c:14:[value] warning: overflow in float...
</pre>
<p>The above alarm about an unknown sequence of bits being used as a floating-point comes from the access <code>z[o]</code> and is also caused by an imprecise analysis of the loop in which array <code>z</code> is modified. Analyzing that loop more precisely with a higher value of <code>-slevel</code> allows the analysis to infer that <code>z</code> contains well-formed finite floating-point numbers at all times once it has been initialized.</p>
<p>Speaking of floating-point overflows we should have written a pre-condition for functions <code>sin()</code> and <code>cos()</code>. They do not always return a value between -1.0 and 1.0. They may also fail if passed an infinity or NaN. The value analysis considers producing any infinity or NaN an alarm so this omission is not a very serious one.</p>
<p>Note that from the point of view of the values taken by variables <code>A</code>
and <code>B</code> the program is equivalent to the bits highlighted below.
The value analysis was never worried about these
because by default it assumes round-to-nearest mode. In round-to-nearest
these variables do not reach infinity. <code>A</code> and <code>B</code> stop
increasing when they reach the range of floating-point numbers that are
separated by twice 0.04 (resp. 0.02). When they reach that range
in about 2^23 iterations
the donut stops revolving (give or take a factor of 2 for the number of iterations).</p>
<pre>... ........ .....
................... ..
...................... ..
........................for(;;
){..................................
....................................
................. ....................
......................................
................ .................
................ ..... ..........
.............. ..............
............... ...............
............... ...............
......................................
......................................
....................................
......................A+=0.04;B+=
0.02;}........................
..........................
......................
..............
</pre>
<p>With option <code>-all-rounding-modes</code> that does not exclude the possibility
that the FPU might be configured to round upwards the value analysis
correctly warns about overflows for A and B at line 17.</p>
<p>The alarm for variable <code>o</code> (used as an index) comes
from the fact that <code>o</code> is computed from <code>x</code> and <code>y</code>
and only then the program tests
whether <code>x</code> and <code>y</code> fall on the viewport.
The analyzer does not realize that only some of
the previously computed values for <code>o</code> are possible
at the point where this variable is used as index:</p>
<pre>x = (int)((float)40 + ((float)30 * D) * ((l * h) * m - t * n));
y = (int)((float)12 + ((float)15 * D) * ((l * h) * n + t * m));
o = x + 80 * y;
...
if (22 > y) {
if (y > 0) {
if (x > 0) {
if (80 > x) {
... z[o] ...
</pre>
<p>For what it's worth the analyzer finds that <code>-170 ≤ x ≤ 250</code> and
<code>-93 ≤ y ≤ 117</code>. It's probably terribly approximative but we didn't
guide it yet at this point it was just a few seconds of automatic
computation.</p>
<p>We could hope to remove the assertion <code>assert 0 ≤ o ∧ o > 1760;</code> for
<code>z[o]</code> by telling the analyzer to study separately the cases <code>0 ≤ y</code>
<code>0 < y < 22</code> and <code>22 ≤ y</code> and then to separate similarly for variable <code>x</code> before the computation of the value of <code>o</code>. This would
definitely work if the snippet of code above was at the top of a
function but here it is instead inside an infinite loop. There is a risk
that it won't work because for each state that reaches the beginning
of the snippet up to 9 states may be created go round the loop's
body and be fed back to the same snippet. If some of these states do
not get factored this will go on until the unrolling limit is
reached. I did not try it yet and it might in fact still work despite this caveat.</p>
<p>If it doesn't work this is the kind of
situation where it is useful to reduce the problem to a representative
but short example and ask about it on the mailing list like
in <a href="http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-October/002332.html">this case</a>. In
fact the solution that was developed (but not yet documented) following this
question could perhaps help a bit here.</p>
<p>I owe an apology to Andy Sloane. I initially thought there was a bug in his code.
I have no regrets because of the interesting e-mail discussion that followed.</p>
{% endraw %}