曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
intervals with float bounds in F
round upper bounds towards +1, lower bounds towards −1
[a, b] ] [c, d] = [a −1 c, b +1 d] \ [min F, max F]
Antoine Min´e Building a specialized static analyzer p. 49 / 112
Design of Astr´ee Numerical domains
Interval widening
Widening with threshold, parameterized by a finite set T:
[−; b] O [−; d] = −; b if b d
min{ t 2 T [ {+1} | t d } otherwise
Example
X=0;
while (1) {
if (?) X=[0;10];
X=0.1*X+[0;75]; /* X 2 [0; 83.33333587646484375] */
}
Range of X:
in rationals: X 83.333 · · ·
in floats (concrete semantics): X 83.33333587646484375
abstract float semantics with widening:
X min { t 2 T | t 83.33333587646484375 }
Antoine Maint´e most |T| iterBautilidoinng sa specialized static analyzer p. 50 / 112
Design of Astr´ee Numerical domains
Choice of widening thresholds
On floats
the precise bound is generally useless for RTE-detection
computations can be stable if the bound is overshot
(' attractive fixpoint)
=) use a sufficiently dense exponential ramp
On integers
The exact bound is important for array bound checking
Solutions:
some bounds can be discovered by decreasing iterations
static thresholds (e.g., array size)
dynamic thresholds: enrich TX when encountering
Jif (X c) · · ·K]
Antoine Min´e Building a specialized static analyzer p. 51 / 112
Design of Astr´ee Numerical domains
Interval widening delay
delay.c
1 void main() {
2 int X=0, Y=0;
3 while (1) {
4 __ASTREE_log_vars((X,Y;interv));
5 if (X<100) X++;
6 if (X>=60+Y) Y=20;
7 }
8 }
Analysis result
% astree delay.c --exec-fn main | egrep "up |WARN|X in"
up iter #0: X in [3, 4], Y in {0}
up iter #1: X in [3, 5], Y in {0}
up iter #2: X in [3, 6], Y in {0}
up iter #3: X in [3, 17], Y in {0}
Antoine Min´e Building a specialized static analyzer p. 53 / 112
Design of Astr´ee Numerical domains
Interval widening delay
delay.c
1 void main() {
2 int X=0, Y=0;
3 while (1) {
4 __ASTREE_log_vars((X,Y;interv));
5 if (X<100) X++;
6 if (X>=60+Y) Y=20;
7 }
8 }
Analysis result
...
up iter #8: X in [3, 43], Y in {0}
up iter #9: X in [3, 99], Y in {0}
up iter #10: X in [3, 100], Y in [0, 20]
%
Antoine Min´e Building a specialized static analyzer p. 53 / 112
Design of Astr´ee Numerical domains
Interval widening delay
delay.c
1 void main() {
2 int X=0, Y=0;
3 while (1) {
4 __ASTREE_log_vars((X,Y;interv));
5 if (X<100) X++;
6 if (X>=60+Y) Y=20;
7 }
8 }
O may be replaced with [ to increase precision:
use a per-variable, per-domain freshness counter
incremented when unstable, unchanged when stable
O only for certain counter values
and always after some value
Antoine Min´e Building a specialized static analyzer p. 53 / 112
Design of Astr´ee Numerical domains
Other non-relational domains
D] ' Var ! D]
b
Congruences
D]
b = {aZ + b} useful to:
check (multi-dimensional) array traversal
check pointer alignment constraints
Bit-fields
D]
b = [0; 31] ! P({0, 1})
useful to abstract bit-operations precisely &, |, <<, >>
also generate congruence information
Antoine Min´e Building a specialized static analyzer p. 54 / 112
Design of Astr´ee Numerical domains
Congruence analysis example
cong.c
1 void main() {
2 int i,x[100];
3 for (i=1;i<=100;i+=2) {
4 __ASTREE_log_vars((i;inter,cong));
5 x[i] = 1;
6 }
7 }
Analysis result
% astree cong.c --exec-fn main | egrep "i in|WARN"
i in {1}
i in {7}
i in [7, 9] ^ (2Z+1)
...
i in [7, 99] ^ (2Z+1)
%
Antoine Min´e Building a specialized static analyzer p. 55 / 112
Design of Astr´ee Numerical domains
Octagon domain
Definition
D] = ^ X,Y2Var
constraints ± X ± Y c
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料41(97)
