曝光臺 注意防騙
網曝天貓店富美金盛家居專營店坑蒙拐騙欺詐消費者
up iter #3: Y in [-1016., 1016.]
...
up iter #18: Y in [-3.4028235e+38, 3.4028235e+38]
rlim.c:7.11-14::[call#main@4:loop@5>=4:]: WARN:
float arithmetic range [-inf., +inf.]
not included in [-3.4028235e+38, 3.4028235e+38]
• Y = S − D =) minY = minY − maxD
• Y = S + D =) maxY = maxY − minD
• after control-flow join: Y ] = (S] +] [−16, 16]) [] [−128, 128]
Antoine Min´e Building a specialized static analyzer p. 61 / 112
Design of Astr´ee Numerical domains
Rate limiter example (octagon analysis)
Analysis result with octagons
% astree rlim.c --exec-fn main | egrep "iter|WARN|Y in"
unroll: Y in [-16.000016, 16.000016]
Y in [-32.000033, 32.000033]
...
up iter #0: Y in [-80.000096, 80.000096]
up iter #1: Y in [-96.000121, 96.000121]
up iter #2: Y in [-112.00015, 112.00015]
up iter #3: Y in [-1000., 1000.]
• we have an approximate octagon abstraction for
V [a0, b0] +P[ai , bi ]Vi
=) Y = S − D ) −16 Y − S 0
Y = S + D ) 0 Y − S 16
• any |Y | M with M 144 can be proved to be a loop invariant
=) iterations stop at the first widening threshold 144
Antoine Min´e Building a specialized static analyzer p. 62 / 112
Design of Astr´ee Numerical domains
Octagon packing
Cost in O(|Var|n) with n > 1 is too expensive!
Antoine Min´e Building a specialized static analyzer p. 63 / 112
Design of Astr´ee Numerical domains
Octagon packing
Cost in O(|Var|n) with n > 1 is too expensive!
Solution
Do not put all Var is a single large octagon,
but make many very small packs:
local dependency pre-analysis
link only variables manipulated together
cut dependencies at syntactic block boundaries
Result: on the kind of code we analyze
linear number of packs in |Var|, |P|
constant size of packs
Antoine Min´e Building a specialized static analyzer p. 63 / 112
Design of Astr´ee Numerical domains
Octagon packing statistics
# lines # variables # packs size qPsize2 3 qPsize3
370 100 20 3.6 4.8 6.2
9 500 1 400 200 3.1 4.6 6.6
70 000 14 000 2 470 3.5 5.2 7.8
226 000 47 500 7 429 3.5 4.5 5.8
400 000 82 000 12 964 3.3 4.1 5.3
Antoine Min´e Building a specialized static analyzer p. 64 / 112
Design of Astr´ee Numerical domains
Manual octagon packing
octpack.c
1 int X=10, Y=100;
2 void f() { Y--; }
3 void main() {
4 while (X >= 0) {
5 X--; f();
6 }
7 }
Analysis result with automatic packing
% astree octpack.c --exec-fn main --print-packs
| egrep "WARN|(X Y)"
octpack.c:2.11-14::[call#main@3:loop@4>=4:call#f@5:]: WARN:
signed int arithmetic range [-2147483649, 2147483646]
not included in [-2147483648, 2147483647]
%
Antoine Min´e Building a specialized static analyzer p. 65 / 112
Design of Astr´ee Numerical domains
Manual octagon packing
octpack2.c
1 int X=10, Y=100;
2 void f() { Y--; }
3 void main() {
4 __ASTREE_octagon_pack((X,Y));
5 while (X >= 0) {
6 X--; f();
7 }
8 }
Analysis result with manual packing
% astree octpack2.c --exec-fn main --print-packs
| egrep "WARN|(X Y)"
octpack2.c@4@1 X Y
%
Antoine Min´e Building a specialized static analyzer p. 66 / 112
Design of Astr´ee Numerical domains
Linearization
Issue
Relational domains are generally bad at non-linear expressions
(multiplications, logical, bit-wise operations, etc.)
Antoine Min´e Building a specialized static analyzer p. 67 / 112
Design of Astr´ee Numerical domains
Linearization
Issue
Relational domains are generally bad at non-linear expressions
(multiplications, logical, bit-wise operations, etc.)
Solution
Linearize expressions: put into the form
[a0; b0] +Pi [ai ; bi ]Vi
linear =) easy to manipulate
intervals =) express non-determinism
a powerful way to abstract
Antoine Min´e Building a specialized static analyzer p. 67 / 112
Design of Astr´ee Numerical domains
Linearization (cont.)
Linearization l : defined by induction on the syntax of expressions
l(e1 + e2) = l(e1) + l(e2)
l(e1 − e2) = l(e1) − l(e2)
l(e1 × e2) = either i(e1) × l(e2)
or i(e2) × l(e1)
l(e1/e2) = l(e1)/i(e2)
otherwise l(e) = i(e)
where
+, − are extended to linear expressions
×, / are extended to an expression and an interval
i(e) evaluates e using interval arithmetics
中國航空網 m.k6050.com
航空翻譯 www.aviation.cn
本文鏈接地址：
航空資料41(99)
