曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
s.b in [0, 12] ^ (12Z)
s.a in [0, 12] ^ (12Z)
%
Antoine Min´e Building a specialized static analyzer p. 101 / 112
Design of Astr´ee Memory domain
Advanced memory model
Dealing with union types, pointer arithmetic and pointer casts
There may be aliasing at the byte level
Example
union {
struct { uint8 al,ah,bl,bh; } b;
struct { uint16 ax,bx; } w;
} r;
r.w.ax = 0; r.b.ah = 2;
0 1 2 3
w ax
b al ah bl bh
bx
0 2
512
Solution
=) as before, we abstract the memory as P(V ! T), V fixed
allocate cells of arbitrary scalar type at arbitrary offset
when cells overlap, use an intersection semantics
create only as needed, using reduction
Antoine Min´e Building a specialized static analyzer p. 102 / 112
Design of Astr´ee Memory domain
Memory copy example
memcpy.c
void memcpy(char* dst, const char* src, unsigned size) {
int i;
__ASTREE_unroll((10))
for (i=0;i<size;i++) dst[i] = src[i];
}
void main() {
float x = 10, y;
memcpy(&y,&x,sizeof(y));
__ASTREE_log_vars((x,y;inter,mem));
}
Generic (untyped) byte-per-byte memory copy function
Antoine Min´e Building a specialized static analyzer p. 103 / 112
Design of Astr´ee Memory domain
Memory copy result
Analysis result
% astree memcpy.c --exec-fn main
| egrep "WARN| in |equality"
memory equality: y[0-3]=x[0-3]
x@3:u_char in [0, 255], x@2:u_char in [0, 255]
x@1:u_char in [0, 255], x@0:u_char in [0, 255]
y@3:u_char in [0, 255], y@2:u_char in [0, 255]
y@1:u_char in [0, 255], y@0:u_char in [0, 255]
x in {10.}, y in {10.}
%
i-th unrolled iteration:
materializes ((char*)&x)[i] as [0, 255]
creates ((char*)&y)[i] and store [0, 255]
updates a predicate: i-th first bytes of x and y are equal
At the end of the loop, the memory equality predicate gives y=x.
Antoine Min´e Building a specialized static analyzer p. 104 / 112
Results
Results
Antoine Min´e Building a specialized static analyzer p. 105 / 112
Results Numbers
Analyses
analyses of industrial avionic codes
performed on a AMD Opteron 248, 64-bit, mono-processor
# lines times memory alarms
370 3.1s 16 MB 0
9 500 160s 80 MB 8
70 000 1h 16mn 582 MB 0
226 000 8h 5mn 1.3 GB 1
400 000 13h 52mn 2.2 GB 0
On the last versions: 0 alarm
=) the absence of run-time errors is proved
Antoine Min´e Building a specialized static analyzer p. 106 / 112
Results Numbers
Analysis parametrization
Parameters
which domains to activate (22 available)
iteration parameters (unrolling, widening, etc.)
partitioning parameters
packing parameters
130 analysis options, 26 code directives
Automated parametrization
octagon and boolean partition packing
trace partitioning
Antoine Min´e Building a specialized static analyzer p. 107 / 112
Results Numbers
Analysis parallelization
Idea
When the control-flow is not statically deterministic,
the analysis must explore all paths
=) we can distribute the cases on several CPUs
Example: sequencer
while (1) {
(f[i])();
i = (i+1) mod 12;
__ASTREE_wait_for_clock();
}
After some iterations, i 2 [0; 11]
all f [i ] are analyzed at each iteration
Antoine Min´e Building a specialized static analyzer p. 108 / 112
Results Numbers
Analysis parallelization
Results
huge cost for communication invariants (despite compression)
=) only worth for large computations between split and join
(e.g., sequencers, not local if)
CPU load is difficult to predict
=) we randomize tasks
time cost is about 0.75/n + 0.25 for n CPUs
=) most useful for n = 3 or 4
Antoine Min´e Building a specialized static analyzer p. 109 / 112
Results Numbers
Interactive invariant visualisation
Web-based interface
% astree filter.c --exec-fn main --export-invariant stat
% astree --reload invariant.data --web-visu &
% firefox http://localhost:8080 &
invariant.data can grow large
=) does not scale-up well to large programs
Antoine Min´e Building a specialized static analyzer p. 110 / 112
Results Conclusion
Conclusion
Conclusion
It is possible to build a static analyzer that is:
efficient in time, memory, and development cost
very precise on a given (infinite) class of programs
Recipe
start from a simple analyzer
while there are false alarms
find their cause, and either
tune analysis parameters, or
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料41(104)
