Probably safe donut
Pascal Cuoq - 17th Sep 2011Introduction
In the first post in the obfuscated animated donut series my colleague Anne pointed out that:
The alarm about : assert \valid(". -~:;=!*#$@"+tmp_7); seems strange because the analysis tells us that tmp_7 ∈
[0..40]at this point... How can this be valid ?
It is only safe to use an offset between 0 and 11 when accessing inside the quantization string ". -~:;=!*#$@". The value analysis determined that the offset was certainly between 0 and 40 so the analyzer can't be sure that the memory access is safe and emits an alarm. Of course [0..40] is only a conservative approximation for the value of the offset at that point. This approximation is computed with model functions sin() and cos() only known to return values in [-1.0 .. 1.0]. These model functions completely lose the relation between the sine and the cosine of a same angle. The computation we are interested in is more clearly seen in the function below which was extracted using Frama-C's slicing plug-in.
/*@ ensures 0 <= \esult <= 11 ; */
int compute(float A float B float i float j)
{
float c=sin(i) l=cos(i);
float d=cos(j) f=sin(j);
float g=cos(A) e=sin(A);
float m=cos(B) n=sin(B);
int N=8*((f*e-c*d*g)*m-c*d*e-f*g-l*d*n);
return N>0?N:0;
}
Both the sine and the cosine of each argument are computed and eventually used in the same formula. Surely the analyzer would do better if it could just remember that sin(x)²+cos(x)²=1. Alas it doesn't. It just knows that each is in [-1.0 .. 1.0].
Making progress
But the Nitrogen release will have more precise sin() and cos() modelizations! Focusing only on the sub-computation we are interested in we can split the variation domains for arguments A B i j of function compute() until it is clear whether or not N may be larger than 11.
I suggest to use the program below (download) where the code around compute() creates the right analysis context. Just like in unit testing there are stubs and witnesses in addition to the function under test.
...
/*@ ensures 0 <= \esult <= 11 ; */
int compute(float A float B float i float j)
{
float c=sin(i) l=cos(i);
float d=cos(j) f=sin(j);
float g=cos(A) e=sin(A);
float m=cos(B) n=sin(B);
int N=8*((f*e-c*d*g)*m-c*d*e-f*g-l*d*n);
Frama_C_dump_each();
return N>0?N:0;
}
main(){
int An Bn in jn;
float A B i j;
for (An=-26; An<26; An++)
{
A = Frama_C_float_interval(An / 8. (An + 1) / 8.);
for (Bn=-26; Bn<26; Bn++)
{
B = Frama_C_float_interval(Bn / 8. (Bn + 1) / 8.);
for (in=-26; in<26; in++)
{
i = Frama_C_float_interval(in / 8. (in + 1) / 8.);
for (jn=-26; jn<26; jn++)
{
j = Frama_C_float_interval(jn / 8. (jn + 1) / 8.);
compute(A B i j);
}
}
}
}
}
Each for loop only covers the range [-3.25 .. 3.25]. In the real program A and B vary in much wider intervals. If target functions sin() and cos() use a decent argument reduction algorithm (and incidentally use the same one) the conclusions obtained for [-3.25 .. 3.25] should generalize to all finite floating-point numbers. This is really a property of the target platform that we cannot do anything about at this level other than clearly state that we are assuming it.
In fact the programs I analyzed were not exactly like above: this task is trivial to run in parallel so I split the search space in four and ran four analyzers at the same time:
$ for i in 1 2 3 4 ; do ( time bin/toplevel.opt -val share/builtin.c \ an$i.c -obviously-terminates -no-val-show-progress \ -all-rounding-modes ) > log$i 2>&1 & disown %1 ; done
After a bit less than two hours (YMMV) I got files log1 ... log4 that contained snapshots of the memory state just after variable N had been computed:
[value] DUMPING STATE of file an1.c line 24
...
c ∈ [-0.016591893509 .. 0.108195140958]
l ∈ [-1. .. -0.994129657745]
d ∈ [-1. .. -0.994129657745]
f ∈ [-0.016591893509 .. 0.108195140958]
g ∈ [-1. .. -0.994129657745]
e ∈ [-0.016591893509 .. 0.108195140958]
m ∈ [-1. .. -0.994129657745]
n ∈ [-0.016591893509 .. 0.108195140958]
N ∈ {-1; 0; 1}
An ∈ {-26}
Bn ∈ {-26}
in ∈ {-26}
jn ∈ {-26}
A ∈ [-3.25 .. -3.125]
B ∈ [-3.25 .. -3.125]
i ∈ [-3.25 .. -3.125]
j ∈ [-3.25 .. -3.125]
=END OF DUMP==
an1.c:15:[value] Function compute: postcondition got status valid.
[value] DUMPING STATE of file an1.c line 24
...
c ∈ [-0.016591893509 .. 0.108195140958]
l ∈ [-1. .. -0.994129657745]
d ∈ [-0.999862372875 .. -0.989992439747]
f ∈ [-0.141120016575 .. -0.0165918916464]
g ∈ [-1. .. -0.994129657745]
e ∈ [-0.016591893509 .. 0.108195140958]
m ∈ [-1. .. -0.994129657745]
n ∈ [-0.016591893509 .. 0.108195140958]
N ∈ {-2; -1; 0; 1}
An ∈ {-26}
Bn ∈ {-26}
in ∈ {-26}
jn ∈ {-25}
A ∈ [-3.25 .. -3.125]
B ∈ [-3.25 .. -3.125]
i ∈ [-3.25 .. -3.125]
j ∈ [-3.125 .. -3.]
=END OF DUMP==
[value] DUMPING STATE of file an1.c line 24
...
Some input sub-intervals for A B i j make the analyzer uncertain about the post-condition N ≤ 11. Here are the first such inputs obtained by searching for "unknown" in the log:
...
[value] DUMPING STATE of file an1.c line 24
...
c ∈ [-0.850319802761 .. -0.778073191643]
l ∈ [-0.628173649311 .. -0.526266276836]
d ∈ [0.731688857079 .. 0.810963153839]
f ∈ [0.585097253323 .. 0.681638777256]
g ∈ [-1. .. -0.994129657745]
e ∈ [-0.016591893509 .. 0.108195140958]
m ∈ [-1. .. -0.994129657745]
n ∈ [-0.016591893509 .. 0.108195140958]
N ∈ {8; 9; 10; 11; 12}
An ∈ {-26}
Bn ∈ {-26}
in ∈ {-18}
jn ∈ {5}
A ∈ [-3.25 .. -3.125]
B ∈ [-3.25 .. -3.125]
i ∈ [-2.25 .. -2.125]
j ∈ [0.625 .. 0.75]
=END OF DUMP==
an1.c:15:[value] Function compute: postcondition got status unknown.
...
Here is the complete list of value sets obtained for variable N on the entire search space:
$ cat log? | grep "N " | sort | uniq
N ∈ {0; 1}
N ∈ {0; 1; 2}
N ∈ {0; 1; 2; 3}
N ∈ {0; 1; 2; 3; 4}
N ∈ {0; 1; 2; 3; 4; 5}
N ∈ {0; 1; 2; 3; 4; 5; 6}
N ∈ {-1; 0}
N ∈ {-1; 0; 1}
N ∈ {10; 11}
N ∈ {10; 11; 12}
N ∈ {-1; 0; 1; 2}
N ∈ {-1; 0; 1; 2; 3}
N ∈ {-1; 0; 1; 2; 3; 4}
N ∈ {-10; -9}
N ∈ {-10; -9; -8}
N ∈ {-10; -9; -8; -7}
N ∈ {-10; -9; -8; -7; -6}
N ∈ {-10; -9; -8; -7; -6; -5}
N ∈ {-10; -9; -8; -7; -6; -5; -4}
N ∈ {-11; -10}
N ∈ {-11; -10; -9}
N ∈ {-11; -10; -9; -8}
N ∈ {-11; -10; -9; -8; -7}
N ∈ {-11; -10; -9; -8; -7; -6}
N ∈ {-11; -10; -9; -8; -7; -6; -5}
N ∈ {1; 2}
N ∈ {-12; -11; -10}
N ∈ {-12; -11; -10; -9}
N ∈ {-12; -11; -10; -9; -8}
N ∈ {-12; -11; -10; -9; -8; -7}
N ∈ {-12; -11; -10; -9; -8; -7; -6}
N ∈ {1; 2; 3}
N ∈ {1; 2; 3; 4}
N ∈ {1; 2; 3; 4; 5}
N ∈ {1; 2; 3; 4; 5; 6}
N ∈ {1; 2; 3; 4; 5; 6; 7}
N ∈ {-13; -12; -11; -10; -9}
N ∈ {-13; -12; -11; -10; -9; -8}
N ∈ {-13; -12; -11; -10; -9; -8; -7}
N ∈ {-2; -1}
N ∈ {-2; -1; 0}
N ∈ {-2; -1; 0; 1}
N ∈ {-2; -1; 0; 1; 2}
N ∈ {-2; -1; 0; 1; 2; 3}
N ∈ {2; 3}
N ∈ {2; 3; 4}
N ∈ {2; 3; 4; 5}
N ∈ {2; 3; 4; 5; 6}
N ∈ {2; 3; 4; 5; 6; 7}
N ∈ {2; 3; 4; 5; 6; 7; 8}
N ∈ {-3; -2}
N ∈ {-3; -2; -1}
N ∈ {-3; -2; -1; 0}
N ∈ {-3; -2; -1; 0; 1}
N ∈ {-3; -2; -1; 0; 1; 2}
N ∈ {3; 4}
N ∈ {3; 4; 5}
N ∈ {3; 4; 5; 6}
N ∈ {3; 4; 5; 6; 7}
N ∈ {3; 4; 5; 6; 7; 8}
N ∈ {3; 4; 5; 6; 7; 8; 9}
N ∈ {-4; -3}
N ∈ {-4; -3; -2}
N ∈ {-4; -3; -2; -1}
N ∈ {-4; -3; -2; -1; 0}
N ∈ {-4; -3; -2; -1; 0; 1}
N ∈ {4; 5}
N ∈ {4; 5; 6}
N ∈ {4; 5; 6; 7}
N ∈ {4; 5; 6; 7; 8}
N ∈ {4; 5; 6; 7; 8; 9}
N ∈ {4; 5; 6; 7; 8; 9; 10}
N ∈ {-5; -4}
N ∈ {-5; -4; -3}
N ∈ {-5; -4; -3; -2}
N ∈ {-5; -4; -3; -2; -1}
N ∈ {-5; -4; -3; -2; -1; 0}
N ∈ {5; 6}
N ∈ {5; 6; 7}
N ∈ {5; 6; 7; 8}
N ∈ {5; 6; 7; 8; 9}
N ∈ {5; 6; 7; 8; 9; 10}
N ∈ {5; 6; 7; 8; 9; 10; 11}
N ∈ {-6; -5}
N ∈ {-6; -5; -4}
N ∈ {-6; -5; -4; -3}
N ∈ {-6; -5; -4; -3; -2}
N ∈ {-6; -5; -4; -3; -2; -1}
N ∈ {-6; -5; -4; -3; -2; -1; 0}
N ∈ {6; 7}
N ∈ {6; 7; 8}
N ∈ {6; 7; 8; 9}
N ∈ {6; 7; 8; 9; 10}
N ∈ {6; 7; 8; 9; 10; 11}
N ∈ {6; 7; 8; 9; 10; 11; 12}
N ∈ {-7}
N ∈ {7}
N ∈ {-7; -6}
N ∈ {-7; -6; -5}
N ∈ {-7; -6; -5; -4}
N ∈ {-7; -6; -5; -4; -3}
N ∈ {-7; -6; -5; -4; -3; -2}
N ∈ {-7; -6; -5; -4; -3; -2; -1}
N ∈ {7; 8}
N ∈ {7; 8; 9}
N ∈ {7; 8; 9; 10}
N ∈ {7; 8; 9; 10; 11}
N ∈ {7; 8; 9; 10; 11; 12}
N ∈ {7; 8; 9; 10; 11; 12; 13}
N ∈ {-8; -7}
N ∈ {-8; -7; -6}
N ∈ {-8; -7; -6; -5}
N ∈ {-8; -7; -6; -5; -4}
N ∈ {-8; -7; -6; -5; -4; -3}
N ∈ {-8; -7; -6; -5; -4; -3; -2}
N ∈ {8; 9}
N ∈ {8; 9; 10}
N ∈ {8; 9; 10; 11}
N ∈ {8; 9; 10; 11; 12}
N ∈ {8; 9; 10; 11; 12; 13}
N ∈ {9; 10}
N ∈ {9; 10; 11}
N ∈ {9; 10; 11; 12}
N ∈ {9; 10; 11; 12; 13}
N ∈ {-9; -8}
N ∈ {-9; -8; -7}
N ∈ {-9; -8; -7; -6}
N ∈ {-9; -8; -7; -6; -5}
N ∈ {-9; -8; -7; -6; -5; -4}
N ∈ {-9; -8; -7; -6; -5; -4; -3}
The above is pretty cute and it is just short enough for manual inspection. The inspection reveals that all the lines with dangerous values for N contain the number 12 so that we can grep for that. We arrive at the following list of dangerous value sets for N:
N ∈ {10; 11; 12}
N ∈ {6; 7; 8; 9; 10; 11; 12}
N ∈ {7; 8; 9; 10; 11; 12}
N ∈ {7; 8; 9; 10; 11; 12; 13}
N ∈ {8; 9; 10; 11; 12}
N ∈ {8; 9; 10; 11; 12; 13}
N ∈ {9; 10; 11; 12}
N ∈ {9; 10; 11; 12; 13}
Note: it is normal that each dangerous line contains
12: if the safety property that we are trying to establish is true then there must be a safe value (say10) in each set. And the sets contain several values as the result of approximations in interval arithmetics so that sets of values forNare intervals of integers. Any interval that contains both a safe value and an unsafe value must contain the largest safe value11and the smallest unsafe value12.
Conclusion
We have improved our estimate of the maximum value of N from 40 to 13. That's pretty good although it is not quite enough to conclude that the donut program is safe.
In conclusion to this post now that we have ascertained that a dangerous set for N was a set that contains 12 we can compute the ratio of the search space for which we haven't yet established that the program was safe. We are exploring a dimension-4 cube by dividing it in sub-cubes. There are 52⁴ = 7 311 616 sub-cubes. Of these this many are still not known to be safe:
$ cat log? | grep "N " | grep " 12" | wc -l 360684
We are 95% there. The remaining 5% shouldn't take more than another 95% of the time.