曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
Introduction Language and semantics
Run-time errors
Kinds of run-time errors
overflows in float, integer, enum arithmetic and cast
division, modulo by 0 on integers and floats
invalid right argument of bit-shift
out-of-bound array access
invalid pointer arithmetic or dereference
violation of user-specified assertions (__ASTREE_assert)
Antoine Min´e Building a specialized static analyzer p. 23 / 112
Introduction Language and semantics
Run-time errors (cont.)
Several semantics are possible after an error:
halt the program
division, modulo by zero
floating-point overflow
assertion failure
return all possible values in the type range
invalid bit-shift
well-defined result
modulo on integer arithmetics overflow
unpredictable behavior
invalid dereference
(Astr´ee treats this as halting the program)
Some alarm reporting and semantics is configurable through
command-line options
Antoine Min´e Building a specialized static analyzer p. 24 / 112
Introduction Language and semantics
Semantic configuration example
enum.c
1 enum { FALSE=0, TRUE=1 } B;
2 void main() {
3 __ASTREE_log_vars((B;interv));
4 B = B+1;
5 __ASTREE_log_vars((B;interv));
6 }
Default semantic parameters
% astree enum.c --exec-fn main | egrep "WARN|B in"
enum.c:3.2-31: log: B in {0}
enum.c:5.2-31: log: B in {1}
%
Antoine Min´e Building a specialized static analyzer p. 25 / 112
Introduction Language and semantics
Semantic configuration example (cont.)
No zero-initialization of globals
% astree enum.c --exec-fn main --no-global-initialization
| egrep "WARN|B in"
enum.c:3.2-31: log: B in [-2147483648, 2147483647]
enum.c:4.6-9::[call#main@2:]: WARN: signed int
arithmetic range [-2147483647, 2147483648]
not included in [-2147483648, 2147483647]
enum.c:4.2-9::[call#main@2:]: WARN: signed int->unnamed
enum conversion range [-2147483648, 2147483647]
not included in {0,1}
enum.c:5.2-31: log: B in [-2147483648, 2147483647]
%
Antoine Min´e Building a specialized static analyzer p. 26 / 112
Introduction Language and semantics
Semantic configuration example (cont.)
Enum clamping
% astree enum.c --exec-fn main --no-global-initialization
--clamp-enum | egrep "WARN|B in"
enum.c:3.2-31: log: B in [-2147483648, 2147483647]
enum.c:4.6-9::[call#main@2:]: WARN: signed int
arithmetic range [-2147483647, 2147483648]
not included in [-2147483648, 2147483647]
enum.c:4.2-9::[call#main@2:]: WARN: signed int->unnamed
enum conversion range [-2147483648, 2147483647]
not included in {0,1}
enum.c:5.2-31: log: B in [0,1]
%
Antoine Min´e Building a specialized static analyzer p. 27 / 112
Design of Astr´ee Architecture of Astr´ee
Architecture of Astr´ee
Antoine Min´e Building a specialized static analyzer p. 28 / 112
Design of Astr´ee Architecture of Astr´ee
Global view
preprocessor (cpp)
#
C99 parser
#
source-level linker
#
intermediate code generation and typing
#
constant propagation and code simplification
#
global dependency analysis
#
abstract interpreter
Antoine Min´e Building a specialized static analyzer p. 29 / 112
Design of Astr´ee Architecture of Astr´ee
Abstract interpreter
iterator
l
trace partitioning
l
memory model and alias analysis
l
(reduced product of) numerical abstract domains
l l l
...
intervals octagons decision trees . . .
l
intervals
Antoine Min´e Building a specialized static analyzer p. 30 / 112
Design of Astr´ee Iterator
Iterator
Antoine Min´e Building a specialized static analyzer p. 31 / 112
Design of Astr´ee Iterator
Syntax-directed interpreter
Astr´ee works as an interpreter:
start from a main function
follow the control-flow of the program
the current state X] 2 D] is an abstraction of an environment
set in D ' P(Var ! Val)
=) collecting semantics, compute reachable states
low memory cost: one environment per loop and if level
The interpretation is by induction on the syntax
Atomic instructions:
assignments JV expr K] : D] ! D] update environments
tests Jexpr == 0?K] : D] ! D] filter environments
add / remove variables
Antoine Min´e Building a specialized static analyzer p. 32 / 112
Design of Astr´ee Iterator
Syntax-directed interpreter (cont.)
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料41(93)
