航空资料41(92)

曝光台 注意防骗 网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者

not included in [0, 4294967295]
%
Antoine Min´e Building a specialized static analyzer p. 13 / 112
Introduction First analyses
Example analysis (corrected)
loop2.c
1 void main() {
2 unsigned i;
3 for (i=10; i> 0; i--) {
4 /* */
5 }
6 }
Analysis result
% astree loop2.c --exec-fn main | egrep WARN
%
Antoine Min´e Building a specialized static analyzer p. 14 / 112
Introduction First analyses
False alarm example
false-alarm.c
1 void main() {
2 int x, y;
3 if ((-4681 < y) && (y < 4681) && (x < 32767) &&
4 (-32767 < x) && ((7*y*y-1) == x*x))
5 y = 1 / x;
6 }
Antoine Min´e Building a specialized static analyzer p. 16 / 112
Introduction First analyses
False alarm example
false-alarm.c
1 void main() {
2 int x, y;
3 if ((-4681 < y) && (y < 4681) && (x < 32767) &&
4 (-32767 < x) && ((7*y*y-1) == x*x))
5 y = 1 / x;
6 }
Analysis result
% astree false-alarm.c --exec-fn main | egrep WARN
false-alarm.c:5.8-13::[call#main@1:]: WARN:
integer division by zero [-32766, 32766]
%
Antoine Min´e Building a specialized static analyzer p. 16 / 112
Introduction First analyses
False alarm example
false-alarm.c
1 void main() {
2 int x, y;
3 if ((-4681 < y) && (y < 4681) && (x < 32767) &&
4 (-32767 < x) && ((7*y*y-1) == x*x))
5 y = 1 / x;
6 }
Actually, 7y2 − 1 = x2 has no integer solution
in [−32766; 32766] × [−4680; 4680]
=) the alarm is spurious
Astr´ee is not knowledgeable of Diophantine equations
(difficult theory, Matiyasevich’s Theorem)
Antoine Min´e Building a specialized static analyzer p. 16 / 112
Introduction First analyses
Reachability information
accum.c
1 void main() {
2 float x = 1.;
3 while (1) x = 0.9*x + 2.;
5 }
Analysis result
% astree accum.c --exec-fn main --dump-invariants
...
loop@3>=4:
x in [6.1489994, 78.320015]
...
Astr´ee shows an over-approximation of the range of x
(a loop invariant valid starting at the fourth iteration)
Antoine Min´e Building a specialized static analyzer p. 17 / 112
Introduction Language and semantics
Class of analyzed codes
synchronous reactive codes
compiled to C from a graphical language a la Scade / Simulink
avionics codes
Structure
initialize state variables
while ( clock  3 600 000 ) {
read input from sensors (volatile)
compute output and new state
write output to actuators
wait for clock tick
}
Antoine Min´e Building a specialized static analyzer p. 18 / 112
Introduction Language and semantics
Example
each box is a built-in C function
boxes have state variables (static)
input (volatile) are bounded by physical constraints
Antoine Min´e Building a specialized static analyzer p. 19 / 112
Introduction Language and semantics
Impact on the analysis
Difficult side
unstructured code
large code (50K–1M loc)
floating-point computation
many variables (10K–)
some complex (non-linear)
numerical invariants
Easy side
homogeneous code
simple algorithms
no recursion
simple data-structures
no dynamic allocation
Antoine Min´e Building a specialized static analyzer p. 20 / 112
Introduction Language and semantics
C subset
Handled
machine integers, enum
IEEE floats
structures, arrays
bitfields
pointers, aliases
pointer arithmetic
unions
tests (if)
loops (for, while)
break, return, forward goto
switch
Unhandled
dynamic allocation
recursivity
backward goto
longjmp
libraries (libc, etc.)
) stubs needed
concurrency (threads)
Antoine Min´e Building a specialized static analyzer p. 21 / 112
Introduction Language and semantics
Considered semantics
Definition of the semantics
C99 norm (portable programs)
IEEE 754-1985 norm (floating-point arithmetics)
platform-dependent choices:
range of types
bit-representation (sizeof, endianess, struct padding, etc.)
compiler- and linker-dependent choices:
automatic variable initialization (optional)
symbol redefinition (forbidden)
Some choices are configurable through command-line options
Antoine Min´e Building a specialized static analyzer p. 22 / 112
　
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：航空资料41(92)