曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
for MPF
We notice that the number of points-to relations is constant.
The major improvement concerns the numerical invariants.
Although the points-to table may seem very small
compared to the size of the code, the points-to relations
recorded there are pervasively used throughout the code.
During the development of the tool we noticed that improving
the precision of few critical entries in this table could
resolve thousands of checks at once.
6. RELATED WORK
There are two bodies of work that are directly related to
our work. The first one is the commercial tool PolySpace C
Verifier [22]. At the time of writing, the tool is available in
three versions: C, C++ and Ada. We do not have any information
about the C++ version. The Ada version seems to
scale quite well, even though we do not have any practical
experience with it. The C version however does not really
scale. Our experiments, using PolySpace C Verifier, on MPF
and DS1 showed that the tool could only process the code
in chunks no bigger than 40 KLOC. Still, PolySpace Verifier
was useful and found quite a few bugs (mainly uninitialized
variables, out-of-bound array accesses, and overflows).
Unfortunately, it also produced a large amount of warnings
which deters developers.
The second body of work precisely addresses the problem
of generating too many warnings. In [3] the authors
describe a static analyzer (also based on abstract interpretation)
that can analyze 75,000 lines of C code in a couple
of hours with a high level of precision (11 false alarms on
the code used for their experiment). Like for CGS, the authors
specialized their algorithms for a family of software
with the following characteristics: many global and static
variables, no recursive functions nor gotos, and simple data
structures. Furthermore, the authors mentioned than the
alias information is trivial in the code they analyze.
There are many analyses that can now scale to large programs
[24, 2, 1, 14, 18], but none of those offer the level
of precision that can meet our requirements. For example,
none of those analyses can track offsets (in arrays or complex
data structures) with sufficient precision. Moreover, all
these analyses have been designed for sequential programs.
More precise analyses, such as those used in shape analysis
[23], exist but they fail to scale to large programs. In fact, it
is extremely difficult to design an analysis that scales with
high precision for any C program. However, as we demonstrate
here, high precision can be achieved on large programs
that share the same basic structure.
7. CONCLUSION
We have shown in this paper that the array bound checking
of large C programs can be performed with a high level
of precision (around 80%) in nearly the same time as compilation.
The key to achieve this result is the specialization of
the analysis towards a particular family of software. Most
importantly, this experience emphasizes the importance of
specializing the algorithms (the domain of adaptive DBMs)
and dismisses the use of general solutions (parallelization).
This approach has a major drawback however: developing a
specialized static analyzer is a huge effort that requires an
important expertise, which limits the impact of these techniques
in the software industry.
CGS is currently being applied to other kinds of NASA
software. It has been recently run with success on several
pieces of software operating in the International Space Station.
This is an interesting process that will give us information
on how a specialized analyzer behaves on programs that
do not belong to its primary scope. The first results show
noticeable variations in the precision. However, the scalability
of the tool remains remarkably intact and CGS is able
to analyze small programs of 20 KLOC in few minutes.
8. REFERENCES
[1] A. Aiken and M. F¨ahndrich. Program analysis using
mixed term and set constraints. In Proceedings of 4th
International Static Analyses Symposium (SAS’97),
1997.
[2] L. Andersen. Program Analysis and Specialization for
the C Programming Language. PhD thesis, DIKU,
University of Copenhagen, 1994.
[3] B. Blanchet, P. Cousot, R. Cousot, J. Feret,
L. Mauborgne, A. Min´e, D. Monniaux, and X. Rival.
A static analyzer for large safety-critical software. In
Proceedings of the ACM SIGPLAN 2003 Conference
on Programming Language Design and
Implementation (PLDI’03), pages 196–207, San Diego,
California, USA, June 7–14 2003. ACM Press.
[4] F. Bourdoncle. Efficient chaotic iteration strategies
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料36(67)
