曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
6 double r1 = y - z;
7 double r2 = 2*a;
8 __ASTREE_log_vars((y,z,r1,r2;inter));
9 __ASTREE_assert((r1==r2));
10 }
Analysis (all roundings)
% astree double-a.c --exec-fn main | egrep " in | WARN"
y in {'1.1258999e+15}
z in {'1.1258999e+15}
r1 in {2.}
r2 in {2.}
%
Antoine Min´e Building a specialized static analyzer p. 76 / 112
Design of Astr´ee Numerical domains
Floating-point simplification example (mixed)
fltdbl-c.c
1 void main() {
2 float a = 1.0;
3 double x = 1125899973951488.0;
4 float y = (x + a);
5 float z = (x - a);
6 float r1 = y - z;
7 float r2 = 2*a;
8 assert(r1==a2);
9 }
Concrete execution (rounding to nearest)
y = 1125900041060352
z = 1125899906842624
r1 = 134217728
r2 = 2
a.out: fltdbl-c.c:15: main: Assertion ‘r1==r2’ failed.
Antoine Min´e Building a specialized static analyzer p. 77 / 112
Design of Astr´ee Numerical domains
Floating-point simplification example (mixed)
fltdbl-a.c
1 void main() {
2 float a = 1.0;
3 double x = 1125899973951488.0;
4 float y = (x + a);
5 float z = (x - a);
6 float r1 = y - z;
7 float r2 = 2*a;
8 __ASTREE_log_vars((y,z,r1,r2;interv));
9 __ASTREE_assert((r1==r2));
10 }
Analysis (all roundings)
% astree fltdbl-a.c --exec-fn main | egrep " in | WARN"
y in [1.1258999e+15, 1.1259001e+15]
z in [1.1258999e+15, 1.1259001e+15]
r1 in [-134217730., 134217730.]
r2 in {2.}
fltdbl-a.c:9.19-25::[call#main@1:]: WARN: assert failure
%Antoine Min´e Building a specialized static analyzer p. 78 / 112
Design of Astr´ee Numerical domains
Floating-point relational domains
Solution
keep reasoning in rationals: D] still abstracts P(Var ! Q)
translate float expressions into real expressions, making
rounding errors explicit
we use linearization, abstracting rounding using
non-deterministic intervals
Example
On 32-bit single precision floats:
relative error of magnitude 2−23 (normalized)
absolute error of magnitude 2−159 (denormalized)
Z X (0.25
X) is linearized into:
Z [0.749 · · · ; 0.750 · · · ] × X + 2.35 · · · 10−159[−1; 1]
Antoine Min´e Building a specialized static analyzer p. 79 / 112
Design of Astr´ee Numerical domains
Floating-point relational domains
We can implement J·K] fully in float:
round upper bounds towards +1, lower bounds towards −1
huge time gain (wrt. exact rationals)
(small) precision loss
Tower of abstractions
deterministic IEEE semantics
#
interval linear form
#
domain-specific abstractions J·K]
#
float implementation of J·K]
Antoine Min´e Building a specialized static analyzer p. 80 / 112
Design of Astr´ee Numerical domains
Numerical filters
2d order filter
In : input at time n
On : output at time n
On = On−1 + On−2+
aIn + bIn−1 + cIn−2
–100
–80
–60
–40
–20
0
20
40
60
80
100
y
–100 –80 –60 –40 –20 20 40 60 80 100
x
Ellipsoid domain
D] ' VX,Y2Var(Y 2 − aYX − bX2 c)
discovers the variables X,Y 2 Var
discovers stable values a, b, c 2 R
Antoine Min´e Building a specialized static analyzer p. 81 / 112
Design of Astr´ee Numerical domains
Numerical filter example
filter.c
1 int INIT = 1;
2 float P, X, E1,E2, S1,S2, INPUT;
3 __ASTREE_volatile_input((INPUT [-10,10]));
4
5 void filtre2 () {
6 if (INIT) P = S1 = E1 = X;
7 else P = (0.4677826 * X) -
8 (E1 * 0.7700725) + (E2 * 0.4344376) +
9 (S1 * 1.5419) - (S2 * 0.6740477);
10 E2 = E1; E1 = X; S2 = S1; S1 = P;
11 }
12
13 void main () {
14 while (1) {
15 X = INPUT; filtre2(); INIT = INPUT;
16 }
17 }
Antoine Min´e Building a specialized static analyzer p. 82 / 112
Design of Astr´ee Numerical domains
Numerical filter example analysis
Analysis with filter domain
% astree filter.c --exec-fn main --dump-invariants
| egrep "WARN|P in"
P in [-13.388927, 13.388927]
%
Analysis without filter domain
% astree filter.c --exec-fn main --no-filters --dump-invariants
| egrep "WARN|P in"
filter.c:7.8-9.44::[call#main@13:loop@14>=4:call#filtre2@15:]:
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料41(101)
