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

channels
Principe
J·K]
1 can use an information X]
2 computed by D]
2
X]
2 not necessarily representable in D]
1
less systematic than the reduced product D]
1 × D]
2
Application: numerical filtering domain
Intervals used as pivot information:
input: filter initialization from an interval
(not found by the filter domain)
output: interval bounding the filter output
(usable by other domains)
Antoine Min´e Building a specialized static analyzer p. 92 / 112
Design of Astr´ee Partitioning domains
Partitioning domains
Antoine Min´e Building a specialized static analyzer p. 93 / 112
Design of Astr´ee Partitioning domains
Boolean decision trees
Issue
In our programs, control-flow is often encoded in booleans
Example
B = (X > 0);
...
long code
...
if (B) Y = 1/X;
(B = 1 ^ X > 0) _ (B = 0 ^ X  0) not convex
We need to partition wrt. the value of B
Antoine Min´e Building a specialized static analyzer p. 94 / 112
Design of Astr´ee Partitioning domains
Boolean decision trees
0
0 1 0 1
1
􀀀􀀀
􀀀􀀀






􀀀
􀀀
􀀀






􀀀􀀀
􀀀􀀀



X

􀀀
􀀀
􀀀

Y
X
Y
X
Y
X
Y
B
B1
B2
BDD
Domaines numériques abstraits
2
booleans in nodes
numerical domains at leaves (intervals, octagons)
opportunistic sharing (e.g. B=?), not maximal
packing, using local dependency pre-analysis
Antoine Min´e Building a specialized static analyzer p. 95 / 112
Design of Astr´ee Partitioning domains
Trace partitioning: test partitioning
Idea
A program transformation to improve the analysis precision
Example
if (...) i=0;
else i=1;
X=a[i]+b[i];
=)
if (...) { i=0; X=a[i]+b[i]; }
else { i=1; X=a[i]+b[i]; }
Unlike boolean partitioning: control, not data criterion
Antoine Min´e Building a specialized static analyzer p. 96 / 112
Design of Astr´ee Partitioning domains
Trace partitioning: loop partitioning
We can also partition finite loops
Before transformation
for (i = 0;i < 10 && x  X[i ];i++);
y = A[i ] + B[i ](x − X[i ]);
After transformation
if (x > X[0]) y = A[0] + B[0](x − X[0]);
else if (x > X[1]) y = A[1] + B[1](x − X[1]);
...
else y = A[10] + B[10](x − X[10]);
The control after the loop exit is partitioning wrt. the number of
loop iterations
Antoine Min´e Building a specialized static analyzer p. 97 / 112
Design of Astr´ee Partitioning domains
Formalizing trace partitioning
We do not actually use a program transformation
Semantical formalization
control points L
concrete trace semantics: Dt = (L × (Var ! Z))
abstraction: D]
t ' (L]) ! D]
abstract control points L]:
L] = {ifl = true, ifl = false, loopl = i , loopl  i | l 2 L}
Intuition: program states are enriched with an (abstract) history of
the control flow
A local dependency pre-analysis is used to determine the abstract
points (L]) of interest
(cost / precision trade-off)
Antoine Min´e Building a specialized static analyzer p. 98 / 112
Design of Astr´ee Memory domain
Memory domain
Antoine Min´e Building a specialized static analyzer p. 99 / 112
Design of Astr´ee Memory domain
Basic memory model
Memory abstraction: in extension
Abstracted as P(Var ! T), Var fixed:
one cell per scalar variable
recursively split arrays and structures
we can also smash big arrays on a single ’summary’ cell
Made possible as there is no dynamic memory allocation
and the stack is fully known
Pointers
Concrete pointer = base 2 Var + offset 2 Z
abstracted separately:
base abstracted as a set  Var
offset abstracted using a synthetic integer variable
Antoine Min´e Building a specialized static analyzer p. 100 / 112
Design of Astr´ee Memory domain
Pointer analysis example
ptr.c
1 struct { int a; int b; } s;
2 void main() {
3 int b, *p = (int*)&s;
4 if (b) p++;
5 *p = 12;
6 __ASTREE_log_vars((p,s;inter,cong,ptr));
7 }
Analysis result
% astree ptr.c --exec-fn main | egrep "WARN| in |="
base(p) = { s }
off(p) in [0, 4] ^ (4Z)
　
中國航空網 www.k6050.com
航空翻譯 www.aviation.cn
本文鏈接地址：航空資料41(103)