曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
and uses a very restricted subset of C, we have to analyze
programs that are multithreaded and use the full power of
pointer arithmetic. Our main purpose is to achieve a level
of precision comparable to that of PolySpace C Verifier with
much lower execution times, since in our case this is the decisive
factor for having the technology adopted by missions
at NASA. C Global Surveyor checks for one type of runtime
errors: out-of-bounds array accesses. This is probably the
most critical category of runtime errors because it silently
corrupts the memory, causing nondeterministic behaviors
during the mission. CGS is specialized for the NASA software
following the Mars Path Finder (MPF) legacy, which
we call the MPF family. The flight software for the Deep
Space One mission (DS1) and the Mars Exploration Rover
mission (MER) all belong to the MPF family.
The programs of the MPF family share a unique feature
in the field of embedded applications: they are written in an
object-oriented style. This means that these programs contain
a myriad of small generic functions which are passed
pointers to the segments of data on which they shall operate.
This has two consequences on the structure of the analyzer.
First, context-sensitivity should be enabled in order
to distinguish between hundreds of calls to the same function.
Second, interprocedural propagation should be very
efficient. All decisions made in the design of CGS originate
from these two observations. We do not claim that the architecture
of CGS represents the optimal solution to this
problem. The experiments showed that some of our choices
were justified and some others were questionable. This paper
should be seen as the critical report of a practical experience
in implementing a large scale static analyzer
The paper is organized as follows. In Sect. 2 we introduce
the abstract interpretation framework underlying the
architecture of CGS. In particular we define the semantic
model of the memory in which the symbolic information produced
by the pointer analysis interacts with the numerical
invariants produced by the flow-sensitive analysis of loops.
Section 3 defines the abstract semantics of memory accesses
and the generation of semantic equations that are used during
the interprocedural propagation phase. In Sect. 4 we
describe the architecture of CGS and our implementation
choices. Section 5 summarizes the experimental results obtained
for the MPF and DS1 codes on a cluster of PC workstations.
We give a critical interpretation of these results
with respect to the design decisions. We discuss related
work in Sect. 6 and we end the paper with concluding remarks.
2. ABSTRACTINTERPRETATIONFRAMEWORK
Abstract Interpretation [7, 8, 10] is a theoretical framework
for the systematic construction of provably correct
static analyzers. Classically, the abstract interpretation of a
program consists of attaching to each program point an abstract
memory configuration that is a conservative approximation
of the actual memory configuration for all executions
of the program that reach that point. This information can
be automatically inferred by associating an abstract semantic
transformer to each basic operation of the program and
computing the composition of these transformers along all
possible executions paths in the control-flow graph. This
is achieved in practice by constructing a system of abstract
semantic equations that describes the flow of information
in the program and by applying appropriate fixpoint algorithms
for computing the solution of the system, usually
with the help of widening/narrowing operators in order to
ensure termination and/or rapid convergence.
In our case we are interested in discovering all possible
addresses that can flow through each pointer variable in
the program. Thus, we can check whether every memory
read or write operation of the program occurs within the
bounds of a memory block. We are not interested in checking
whether a pointer is NULL or contains an undetermined
value. This is a different problem that has to be treated
with a separate analysis. Therefore, in our abstract semantic
model the denotation of a pointer always contains NULL
and any undetermined value. We can nevertheless flag an
illegal memory access with certainty whenever our analysis
discovers an empty points-to set.
The C language authorizes creating a pointer to an object
inside a compound data structure, for example to the element
of an array. This construct is heavily used in the MPF
and DS1 codes, since data are organized in large structures
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料36(56)
