曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
For ×, we need a strategy to choose between two linearizations
(e.g. minimize the interval factor)
Antoine Min´e Building a specialized static analyzer p. 68 / 112
Design of Astr´ee Numerical domains
Using linearization
Application:
octagons can handle interval linear expressions
e.g.: if Y 2 [0; 1], Z 0, then l(Y × Z) = [0; 1] × Z
JX Y × ZK] is abstracted as
JX [0; 1] × ZK]
=) octagons can infer that X Z
linearization provides symbolic simplification for free
e.g.: l(2X − X) = (X)
if X 2 [0; 1] plain intervals evaluate 2X − X to [−1; 2]
after linearization, we have [0; 1]
Linearization is an abstraction ) it can also lose precision
Antoine Min´e Building a specialized static analyzer p. 69 / 112
Design of Astr´ee Numerical domains
Symbolic constant propagation
Example
1 Y=[-100;100];
2 X=Y+10;
3 if (X<0) X=-X;
4 if (X<60) { · · · Y · · · }
How can we find a bound on Y . . . without octagons?
Antoine Min´e Building a specialized static analyzer p. 70 / 112
Design of Astr´ee Numerical domains
Symbolic constant propagation
Example
1 Y=[-100;100];
2 X=Y+10;
3 if (X<0) X=-X;
4 if (X<60) { · · · Y · · · }
How can we find a bound on Y . . . without octagons?
Alternate solution
Remember that X = Y + 10
and substitute X with Y + 10 at line 3 and on
The interval domain will find Y 2 [−70; 50]
Antoine Min´e Building a specialized static analyzer p. 70 / 112
Design of Astr´ee Numerical domains
Symbolic constant propagation
Comparison with a relational domain
Benefits
'linear cost (' vanilla constant propagation)
simple to implement
interacts well with linearization
(more opportunities for simplification)
Issues
no inference of non-syntactic properties (joins, loops)
not optimal, or even monotonic scheme
substitution strategies are fragile (wrt. code transformations)
Antoine Min´e Building a specialized static analyzer p. 71 / 112
Design of Astr´ee Numerical domains
Floating-point semantics and symbolic computations
Problem
Most algebraic rules valid in Z or Q
are no longer valid in floating-point
How can we:
perform sound floating-point linearization?
use relational domains on floating-point expressions?
Antoine Min´e Building a specialized static analyzer p. 72 / 112
Design of Astr´ee Numerical domains
Floating-point simplification example (float)
float-c.c
1 void main() {
2 float a = 1.0;
3 float x = 1125899973951488.0;
4 float y = (x + a);
5 float z = (x - a);
6 float r1 = y - z;
7 float r2 = 2*a;
8 assert(r1==a2);
9 }
Concrete execution (rounding to nearest)
y = 1125899906842624
z = 1125899906842624
r1 = 0
r2 = 2
a.out: float-c.c:15: main: Assertion ‘r1==r2’ failed.
Antoine Min´e Building a specialized static analyzer p. 73 / 112
Design of Astr´ee Numerical domains
Floating-point simplification example (float)
float-a.c
1 void main() {
2 float a = 1.0;
3 float x = 1125899973951488.0;
4 float y = (x + a);
5 float z = (x - a);
6 float r1 = y - z;
7 float r2 = 2*a;
8 __ASTREE_log_vars((y,z,r1,r2;interv));
9 __ASTREE_assert((r1==r2));
10 }
Analysis (all roundings)
% astree float-a.c --exec-fn main | egrep " in | WARN"
y in [1.1258999e+15, 1.1259002e+15]
z in [1.1258996e+15, 1.1259001e+15]
r1 in [-134217730., 335544320.]
r2 in {2.}
float-a.c:9.19-25::[call#main@1:]: WARN: assert failure
%Antoine Min´e Building a specialized static analyzer p. 74 / 112
Design of Astr´ee Numerical domains
Floating-point simplification example (double)
double-c.c
1 void main() {
2 double a = 1.0;
3 double x = 1125899973951488.0;
4 double y = (x + a);
5 double z = (x - a);
6 double r1 = y - z;
7 double r2 = 2*a;
8 assert(r1==r2);
9 }
Concrete execution (rounding to nearest)
y = 1125899973951489
z = 1125899973951487
r1 = 2
r2 = 2
Antoine Min´e Building a specialized static analyzer p. 75 / 112
Design of Astr´ee Numerical domains
Floating-point simplification example (double)
double-a.c
1 void main() {
2 double a = 1.0;
3 double x = 1125899973951488.0;
4 double y = (x + a);
5 double z = (x - a);
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料41(100)
