曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
Antoine Min´e Building a specialized static analyzer p. 56 / 112
Design of Astr´ee Numerical domains
Octagon domain
Algorithms
generalize DBMs (X − Y c)
representation: square matrix of constraints
constraint-propagation: based on shortest-path closure
exact abstraction for JX ±Y + cK, J±X ± Y cK Cost
memory: O(|Var|2) (full matrices)
time O(|Var|3) (closure)
Antoine Min´e Building a specialized static analyzer p. 57 / 112
Design of Astr´ee Numerical domains
The need for relational domains
rel.c
1 void main() {
2 int I, V=0;
3 for (I=10;I>=0;I--) {
4 int B;
5 if (B) V=V+1;
6 }
7 __ASTREE_log_vars((V));
8 }
Analysis result with standard domains
% astree rel.c --exec-fn main | egrep "WARN|V in"
V in [0, 11]
%
Antoine Min´e Building a specialized static analyzer p. 59 / 112
Design of Astr´ee Numerical domains
The need for relational domains
rel.c
1 void main() {
2 int I, V=0;
3 for (I=10;I>=0;I--) {
4 int B;
5 if (B) V=V+1;
6 }
7 __ASTREE_log_vars((V));
8 }
Analysis result without relational domains
% astree rel.c --exec-fn main --no-relational
| egrep "WARN|V in"
rel.c:5.13-16::[call#main@1:loop@4>=4:]: WARN: signed int
arithmetic range [-2147483647, 2147483648]
not included in [-2147483648, 2147483647]
V in [-2147483648, 2147483647]
%
Antoine Min´e Building a specialized static analyzer p. 59 / 112
Design of Astr´ee Numerical domains
The need for relational domains
rel.c
1 void main() {
2 int I, V=0;
3 for (I=10;I>=0;I--) {
4 int B;
5 if (B) V=V+1;
6 }
7 __ASTREE_log_vars((V));
8 }
V is not stable in the loop, and not bounded by any test
To bound V we must:
infer the loop invariant V + I 10
combine it with I = −1 at loop exit
Antoine Min´e Building a specialized static analyzer p. 59 / 112
Design of Astr´ee Numerical domains
The need for relational domains
rel.c
1 void main() {
2 int I, V=0;
3 for (I=10;I>=0;I--) {
4 int B;
5 if (B) V=V+1;
6 }
7 __ASTREE_log_vars((V));
8 }
Octagon invariant
% astree rel.c --exec-fn main | egrep "V <="
0 <= V <= 11, I = -1, -12 <= I-V <= -1, -1 <= I+V <= 10
%
Antoine Min´e Building a specialized static analyzer p. 59 / 112
Design of Astr´ee Numerical domains
The need for relational domains
rel.c
1 void main() {
2 int I, V=0;
3 for (I=10;I>=0;I--) {
4 int B;
5 if (B) V=V+1;
6 }
7 __ASTREE_log_vars((V));
8 }
The need for relational domains
Even when looking for a non-relational invariant at loop exit
a relational loop invariant is often needed
Antoine Min´e Building a specialized static analyzer p. 59 / 112
Design of Astr´ee Numerical domains
Rate limiter example
rlim.c
1 float x,d,R,S,Y;
2 __ASTREE_volatile_input((x [-128,128]));
3 __ASTREE_volatile_input((d [0,16]));
4 void main() {
5 while (1) {
6 float X=x,D=d;
7 S=Y; R=X-S; Y=X;
8 if (R<=-D) Y=S-D; else if (R>=D) Y=S+D;
9 __ASTREE_log_vars((Y));
10 }
11 }
|Y | is bounded by max(128, |S|) because either:
• Y = X 2 [−128, 128]
• Y = S − D S and X − S −D, so Y = S − D X −128
• Y = S + D S and X − S D, so Y = S + D X 128
) Y 2 [−128, 128]
Antoine Min´e Building a specialized static analyzer p. 60 / 112
Design of Astr´ee Numerical domains
Rate limiter example (interval analysis)
Analysis without octagons
% astree rlim.c --exec-fn main --no-octagon
| egrep "iter|WARN|Y in"
unroll: Y in [-128., 128.]
unroll: Y in [-144., 144.]
...
up iter #0: Y in [-192., 192.]
up iter #1: Y in [-208., 208.]
up iter #2: Y in [-224., 224.]
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料41(98)
