曝光臺 注意防騙 網曝天貓店富美金盛家居專營店坑蒙拐騙欺詐消費者

Instruction blocks:
sequential evaluation Ji1; . . . ; inK] = JinK]  · · ·  Ji1K]
Conditionals: if (expr) iT else iF
evaluate both branches, then join:
JifK](X]) = JiT K](Jexpr ! = 0?K](X])) []
JiF K](Jexpr == 0?K](X]))
where
(X] [] Y ]) 
(X]) [
(Y ])
Function calls:
inline all function calls
=) high precision (full stack context sensitivity)
costly, no recursivity
Antoine Min´e Building a specialized static analyzer p. 33 / 112
Design of Astr´ee Iterator
Analysis of conditionals example
cond.c
1 void main() {
2 int b;
3 float x; __ASTREE_log_vars((x;interv));
4 if (b) { x = 0; __ASTREE_log_vars((x;interv)); }
5 else { x = 10; __ASTREE_log_vars((x;interv)); }
6 __ASTREE_log_vars((x;interv));
7 }
Analysis result
% astree cond.c --exec-fn main | egrep "up |x in"
cond.c:3.11-40: log: x in [-3.4028235e+38, 3.4028235e+38]
cond.c:4.18-47: log: x in {0.}
cond.c:5.17-46: log: x in {10.}
cond.c:6.2-31: log: x in [0., 10.]
%
Antoine Min´e Building a specialized static analyzer p. 34 / 112
Design of Astr´ee Iterator
Context-sensitive analysis example
fun.c
1 int f(int b) { return 1/b; }
2
3 void main() {
4 f(2);
5 f(0);
6 f(0);
7 }
Analysis result
% astree fun.c --exec-fn main | egrep WARN
fun.c:1.22-25::[call#main@3:call#f@5:]: WARN:
integer division by zero {0}
%
Antoine Min´e Building a specialized static analyzer p. 35 / 112
Design of Astr´ee Iterator
Function stub example
nostub.c
1 extern double acos(double d);
2 void main() {
3 double x;
4 double y = acos(x);
5 __ASTREE_log_vars((x,y;interv));
6 }
Analysis result
% astree nostub.c --exec-fn main | egrep "WARN| in "
nostub.c:1.14-17: WARN: stub log called
x in [-1.7976932e+308, 1.7976932e+308]
y in [-1.7976932e+308, 1.7976932e+308]
%
Antoine Min´e Building a specialized static analyzer p. 36 / 112
Design of Astr´ee Iterator
Function stub example (corrected)
stub.c
1 double acos(double d) {
2 double r;
3 __ASTREE_assert((d>=-1 && d<=1));
4 __ASTREE_known_fact((r>=0 && r<=3.2));
5 return r;
6 }
Analysis result
% astree nostub.c stub.c --exec-fn main | egrep "WARN| in "
stub.c:3.19-32::[call#main@2:call#acos@4:]:
WARN: assert failure
x in [-1., 1.]
y in [0., 3.2000001]
%
Antoine Min´e Building a specialized static analyzer p. 37 / 112
Design of Astr´ee Iterator
Loop analysis
Loops: while (expr) i
Concrete semantics: fixpoint
JwhileK(X) = Jexpr == 0?K(lfp Y 7! X [ (JiK Jexpr ! = 0?K)(Y ))
Abstract semantics: iterations with widening
JwhileK](X]) = Jexpr == 0?K(X]
n)
where 8>
<>
:
X]
0 = X] (start)
X]
i+1 = X]
i O (JiK]  Jexpr ! = 0?K])(X]
i ) (up iteration)
X]
n+1 = X]
n (fix-point)
O is an extrapolation operator

(X]) [
(Y ]) 
(X] O Y ])
O enforces termination
(e.g., start with [], enlarge unstable bounds to threshold, then max-type)
Antoine Min´e Building a specialized static analyzer p. 38 / 112
Design of Astr´ee Iterator
Loop analysis example
fltloop.c
1 void main() {
2 float x = 0.1;
3 while (1) {
4 int r;
5 if (r) x = 0.2; else x = 0.9*x + 0.1;
6 __ASTREE_log_vars((x;interv));
7 }
8 }
Analysis result
% astree fltloop.c --exec-fn main --unroll 0
| egrep "up |x in"
x in [0.18999993, 0.20000001]
...
Antoine Min´e Building a specialized static analyzer p. 40 / 112
Design of Astr´ee Iterator
Loop analysis example
fltloop.c
1 void main() {
2 float x = 0.1;
3 while (1) {
4 int r;
5 if (r) x = 0.2; else x = 0.9*x + 0.1;
6 __ASTREE_log_vars((x;interv));
7 }
8 }
Analysis result
fltloop.c:3.2-9.3:up iteration #0
x in [0.18999993, 0.28000004]
fltloop.c:3.2-9.3:up iteration #1
x in [0.18999993, 0.35200006]
...
Antoine Min´e Building a specialized static analyzer p. 40 / 112
Design of Astr´ee Iterator
Loop analysis example
fltloop.c
1 void main() {
2 float x = 0.1;
3 while (1) {
4 int r;
5 if (r) x = 0.2; else x = 0.9*x + 0.1;
6 __ASTREE_log_vars((x;interv));
7 }
8 }
Analysis result
fltloop.c:3.2-9.3:up iteration #2
　
中國航空網 www.k6050.com
航空翻譯 www.aviation.cn
本文鏈接地址：航空資料41(94)