曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
Design of Astr´ee Iterator
Loop unrolling example
initloop.c
1 void main() {
2 int I = 1, x;
3 while (1) {
4 __ASTREE_log_vars((I, x; interv));
5 if (I) { x = 0; I = 0; }
6 else { x++; if (x > 100) x = 0; }
7 }
8 }
Analysis result with unrolling
loop@3>=2: I in {0}, x in [0, 2]
initloop.c:3.2-7.3:up iteration #2
...
loop@3>=2: I in {0}, x in [0, 19]
initloop.c:3.2-7.3:up iteration #9
...
Antoine Min´e Building a specialized static analyzer p. 43 / 112
Design of Astr´ee Iterator
Loop unrolling example
initloop.c
1 void main() {
2 int I = 1, x;
3 while (1) {
4 __ASTREE_log_vars((I, x; interv));
5 if (I) { x = 0; I = 0; }
6 else { x++; if (x > 100) x = 0; }
7 }
8 }
Analysis result with unrolling
loop@3>=2: I in {0}, x in [0, 41]
initloop.c:3.2-7.3:up iteration #10
loop@3>=2: I in {0}, x in [0, 32767]
initloop.c:3.2-7.3:up iteration #11
...
Antoine Min´e Building a specialized static analyzer p. 43 / 112
Design of Astr´ee Iterator
Loop unrolling example
initloop.c
1 void main() {
2 int I = 1, x;
3 while (1) {
4 __ASTREE_log_vars((I, x; interv));
5 if (I) { x = 0; I = 0; }
6 else { x++; if (x > 100) x = 0; }
7 }
8 }
Analysis result with unrolling
loop@3>=2: I in {0}, x in [0, 32767]
initloop.c:3.2-7.3:down iteration #0
loop@3>=2: I in {0}, x in [0, 100]
initloop.c:3.2-7.3:down iteration #1
loop@3>=2: I in {0}, x in [0, 100]
%
Antoine Min´e Building a specialized static analyzer p. 43 / 112
Design of Astr´ee Iterator
Nested loops
nested.c
1 void main() {
2 int i,j,x[10][20];
3 for (i=0;i<10;i++)
4 for (j=0;j<20;j++) {
5 x[i][j] = 1;
6 __ASTREE_log_vars((i,j;interv));
7 }
8 }
Analysis result
% astree nested.c --exec-fn main --unroll 0
| egrep "i in|WARN"
i in {0}, j in {0}
i in {0}, j in [0, 1]
...
i in {0}, j in [0, 19]
Antoine Min´e Building a specialized static analyzer p. 45 / 112
Design of Astr´ee Iterator
Nested loops
nested.c
1 void main() {
2 int i,j,x[10][20];
3 for (i=0;i<10;i++)
4 for (j=0;j<20;j++) {
5 x[i][j] = 1;
6 __ASTREE_log_vars((i,j;interv));
7 }
8 }
Analysis result
i in [0, 1], j in {0}
i in [0, 1], j in [0, 1]
...
i in [0, 9], j in [0, 18]
i in [0, 9], j in [0, 19]
%
Antoine Min´e Building a specialized static analyzer p. 45 / 112
Design of Astr´ee Numerical domains
Numerical domains
Antoine Min´e Building a specialized static analyzer p. 46 / 112
Design of Astr´ee Numerical domains
Integer interval domain
Integer interval definition
D] = Var ! (Z[{−1})×(Z[{+1}) [{?}
maps variables to interval bounds
Benefits
can express the absence of (most) RTE
(overflow, out-of-bound access)
easy to implement
(e.g. assignments by induction on the syntax of expressions
[a; b] +] [c; d] = [a + c; b + d])
low memory and time cost (linear?)
Antoine Min´e Building a specialized static analyzer p. 47 / 112
Design of Astr´ee Numerical domains
Data-structures
Na¨ıve idea: arrays
fetch, update in O(1)
copy in O(|Var|) (tests and loops)
[] in O(|Var|)
=) cost of one iteration: ' O(|Var| × |P|) ' O(|P|2)
Antoine Min´e Building a specialized static analyzer p. 48 / 112
Design of Astr´ee Numerical domains
Data-structures
Na¨ıve idea: arrays
fetch, update in O(1)
copy in O(|Var|) (tests and loops)
[] in O(|Var|)
=) cost of one iteration: ' O(|Var| × |P|) ' O(|P|2)
Better idea: functional maps (balanced binary trees)
fetch, update in O(log |Var|)
copy in O(1)
[] in O(|Pi | log |Var|) (for i−th block)
=) cost of one iteration: ' O(|P| log |Var|) ' O(|P| log |P|)
Antoine Min´e Building a specialized static analyzer p. 48 / 112
Design of Astr´ee Numerical domains
Float interval domain
Concrete semantics: IEEE 754-1985 norm
compute over a finite set F Q
two-step evaluation
evaluate exactly in Q
round the result in F, in direction r 2 {0,+1,−1, n}
Jx r yK= Rr (JxK+ JyK)
R+1(x) = min {z 2 F | z x}
possibility of run-time errors: overflow and division by zero
(semantics halts with a RTE instead of constructing ±1 or NaN)
Abstract semantics:
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料41(96)
