• 热门标签

当前位置: 主页 > 航空资料 > 国外资料 >

时间:2010-09-06 01:00来源:蓝天飞行翻译 作者:admin
曝光台 注意防骗 网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者

bootstrap makes the design of the interprocedural propagation
algorithms tremendously simpler. In order to achieve
efficiency we break down the interprocedural propagation
into two phases:
1. A backward propagation phase computes transformers
relating the parameters of a function with its return
value. These transformers are expressed using the domain
of adaptive DBMs.
2. A forward propagation phase uses the transformers
computed in the previous phase to propagate abstract
memory references and ranges using the lattice of intervals.
The transformers computed during the backward propagation
phase are used during the forward propagation to solve
a function call without having to analyze the body of the
called function. The return operations are used at this
moment to propagate the constraints between the return
value and the arguments of the call. A coarse version of the
transformers are computed during the bootstrap in order to
enable the first forward propagation phase. Using a classical
resolution scheme would have implied iterating over interprocedural
cycles induced by the two-way dependencies
between a caller and a callee (function parameters/return
value), which is completely unrealistic for large programs.
The interprocedural propagation phase of CGS can be
context-sensitive. We implemented call-site sensitivity, i.e.
the invariants of a function are duplicated depending on the
syntactic call site. This level of context-sensitivity is sufficient
for the MPF family, since it handles the common situation
where a pointer to some part of a big structure (typically
an array of double representing a vector or a matrix) is
transmitted to a mathematical function. Context sensitivity
is not applied uniformly, but only to functions which have
a pointer in their signature, since this is the only situation
where the analysis is able to distinguish between different
call contexts. Context-sensitivity is extremely important for
precision. Arrays of double, which are the main data structures
manipulated by the MPF family codes, are usually
transmitted together with an integer parameter containing
the size of the array like in the equate example above. Since
the numerical call contexts computed by CGS only are made
of intervals, they cannot express a relation between the size
of the array and the integer parameter. The only way to
capture this information is to enumerate all call contexts.
Hence, without context-sensitivity the tool would be unable
to perform any precise array bound checking on this large
family of functions.
4. ARCHITECTURE OF CGS
The algorithmic core of C Global Surveyor consists of
20,000 lines of C code. The tool is architected around three
main phases:
1. The build. This phase computes the points-to constraints
and the numerical inequalities for each function
in the program.
2. The bootstrap. This phase performs a flow-insensitive
pointer analysis and a coarse context-independent
resolution of the numerical inequalities, in order to
obtain a first approximation of all memory accesses.
These results are used to construct the call graph and
an initial approximation of the heap.
3. The solve. This phase consists of performing a forward
or backward interprocedural propagation of numerical
invariants. The results obtained at the end of
this phase are used to compute a new abstract heap
that refines the previous one. This phase should be repeated
until a satisfactory level of precision has been
attained.
There are two additional satellite phases:
• The initialization. This phase is performed at the
very beginning and collects general information about
the program, like the table of global variables, the table
of functions, etc.
• The array-bound check (abc). This phase can be
executed at any time after the bootstrap and checks
the safety of all memory accesses from the results of
the analysis available at this moment. The precision
computed at the end of this phase is the main criterion
for deciding whether to continue refining the results or
stop at this point.
A very important decision in the initial design of a static
analyzer is the choice of the front-end. We chose the Edison
Design Group’s C/C++ front-end [15], a commercial
front-end which supports a large variety of C dialects. Moreover,
the Green Hills’ compiler [17], which is widely used at
NASA especially for developing flight software, is based on
this front-end. This is a relevant factor when considering the
application of the tool to other types of programs developed
 
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址:航空资料36(64)