曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
WARN: double->float conversion range [-inf., +inf.]
not included in [-3.4028235e+38, 3.4028235e+38]
P in [-3.4028235e+38, 3.4028235e+38]
%
Antoine Min´e Building a specialized static analyzer p. 83 / 112
Design of Astr´ee Numerical domains
Synchronous hypothesis
Synchronous programs
the program has an implicit clock
the clock ticks for a (configurable) maximal count
clock-ok.c
1 int X, B;
2 __ASTREE_volatile_input((B));
3 __ASTREE_max_clock((3600));
4 void main() {
5 while (1) {
6 if (B) X+=2; else X=0;
7 __ASTREE_wait_for_clock(());
8 }
9 }
Antoine Min´e Building a specialized static analyzer p. 84 / 112
Design of Astr´ee Numerical domains
Clock relationship
Analysis with clock domain
% astree clock-ok.c --exec-fn main --dump-invariants
| egrep "WARN|X in|\|X\|"
X in [0, 7202]
|X| <= 0. + clock *2. <= 7202.
%
clock is an implicit variable incremented at clock tick
The clock domain infers relations of the form: |V| clock +
with a linear cost
which in turns gives bounds for |V|
Antoine Min´e Building a specialized static analyzer p. 85 / 112
Design of Astr´ee Numerical domains
Arithmetic-geometric progressions
arigeo-bad.c
1 void main() {
2 float X;
3 __ASTREE_known_fact((X>=0 && X <=100.));
4 while (1) {
5 X=X/101.;
6 X=X*101.;
7 }
8 }
Analysis result
% astree arigeo-bad.c --exec-fn main --dump-invariants
| egrep "WARN|X in"
arigeo-bad.c:6.4-12::[call#main@1:loop@4>=4:]: WARN:
double->float conversion range [0., +inf.]
not included in [-3.4028235e+38, 3.4028235e+38]
X in [0., 3.4028235e+38]
%
Antoine Min´e Building a specialized static analyzer p. 87 / 112
Design of Astr´ee Numerical domains
Arithmetic-geometric progressions
arigeo-bad.c
1 void main() {
2 float X;
3 __ASTREE_known_fact((X>=0 && X <=100.));
4 while (1) {
5 X=X/101.;
6 X=X*101.;
7 }
8 }
In float, X/101. × 101 6= X due to rounding-errors
=) X is enlarged at each iteration step
Antoine Min´e Building a specialized static analyzer p. 87 / 112
Design of Astr´ee Numerical domains
Arithmetic-geometric progressions (corrected)
arigeo-ok.c
1 void main() {
2 float X;
3 __ASTREE_known_fact((X>=0 && X <=100.));
4 while (1) {
5 X=X/101.;
6 X=X*101.;
7 __ASTREE_wait_for_clock(());
8 }
9 }
Analysis result
% astree arigeo-ok.c --exec-fn main --dump-invariants
| egrep "WARN|X in|\X\"
X in [0., 235.91632]
|X| <= (99.999988 + 5.9950219e-37/(1.0000002-1))*
(1.0000002)^clock - 5.9950219e-37/(1.0000002-1)
<= 235.91632
%
Antoine Min´e Building a specialized static analyzer p. 89 / 112
Design of Astr´ee Numerical domains
Arithmetic-geometric progressions (corrected)
arigeo-ok.c
1 void main() {
2 float X;
3 __ASTREE_known_fact((X>=0 && X <=100.));
4 while (1) {
5 X=X/101.;
6 X=X*101.;
7 __ASTREE_wait_for_clock(());
8 }
9 }
The arithmetic-geometric deviation domain infers constraints:
|V| (1 + a)clock +
which can provide bounds for V
Antoine Min´e Building a specialized static analyzer p. 89 / 112
Design of Astr´ee Numerical domains
Reduced product
Formalization
domain product D] = D]
1 × D]
2
1×2(x1, x2) =
1(x1) \
2(x2)
compute independently J·K]
1 and J·K]
2, and
reduce : D] ! D]
i ((x)i )
i (xi ) et
1×2((x)) =
1×2(x)
Applications
interval $ congruence reduction [1; 7] \ 2Z = [2; 6] \ 2Z
interval $ octagon partial reduction
Antoine Min´e Building a specialized static analyzer p. 90 / 112
Design of Astr´ee Numerical domains
Widening and reduced product
In D]
1 × D]
2:
X]
i+1 = X]
i O1×2 F](X]
i ) converges
X]
i+1 = (X]
i O1×2 F](X]
i )) may not converge
Solutions
do not reduce successive iterates
() precision loss)
define a new widening O for the product D]
1 × D]
2
() more work to do, and an extra proof of convergence)
Antoine Min´e Building a specialized static analyzer p. 91 / 112
Design of Astr´ee Numerical domains
Communications between domains
Abstract domain modules communicate invariants through
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：航空资料41(102)
