曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
which are modified via pointer references passed to generic
functions. Therefore, our abstract memory model should
represent references as a triple (a, π, s) where a is the address
of a memory block, π is an access path into the block
and s is the size of the block. An address is either the address
of a variable &A, a constant character string stringℓ
that appears in the program at the program location ℓ, or
the dynamic allocation of a block mallocℓ at the program location
ℓ. Our model does not distinguish between instances
of a malloc in a loop simply because this situation never
occurs in the class of programs that we are considering, although
techniques exist that can cope with this problem [29,
26].
Without access path information it is impossible to perform
any precise array bound checking. We could use the
type information contained in the C program for representing
access paths symbolically. Unfortunately, the aggressive
type casting mechanism of C combined to pointer arithmetic
ruins this idea. Consider for example the following fragment
of code:
struct MsgHeader {
int id;
int length;
};
struct Msg_X {
struct MsgHeader header;
Data_X data;
};
/* Thread 1 */
struct Msg_X *msg = malloc (...);
...
sendMsg (Thread_2, msg);
...
/* Thread 2 */
struct MsgHeader *msg = readMsg (...);
if (msg->id == ID_OF_X) {
Data_X *data = (DataX *)(msg + 1);
...
This is in essence how the message passing mechanism for
thread communication is implemented in the MPF family.
All messages start with the same header which contains an
id that uniquely determines the type of the message. The
data are stored right after the header. The actual type of
the data is only known after the message id has been read,
which explains this seemingly odd construction. This piece
of code illustrates the overall object-oriented design of the
MPF family software. Messages are considered as objects
and this is nothing more than a manual encoding of virtual
method dispatch. However, this makes the manipulation
of symbolic access paths extremely difficult since we must
keep track of the actual layout of structure components in
memory in order to cope accurately with pointer arithmetic.
Our solution to this problem consists of choosing a uniform
offset-based representation of structure components instead
of symbolic access paths. A reference is then represented by
a triple (a, o, s) where o is an offset from the beginning of the
block expressed in bytes. With this numerical model, type
casting is no more an issue and becomes transparent for the
analysis. All architecture-dependent problems entailed by
this representation like memory alignment and padding are
completely resolved by the C front-end. Therefore, there is
no extra complexity in implementing this model.
For ensuring computability we approximate a set {(ai, oi,
si) | i ∈ I} of memory references by an abstract memory
reference ({ai | i ∈ I},O, S) where O and S are the smallest
intervals such that ∀i ∈ I : oi ∈ O & si ∈ S. This corresponds
to the notion of attribute-independent or cartesian
approximation [9]. We can gain precision by considering the
reduced product [8] between the powerset lattice of addresses
and the lattice of intervals. The size of memory blocks is
known at compile time for the address of a static memory
block, i.e. an address of type &A or string. We denote by
sz(a) the size of the block at address a. If a is the address
of a dynamically allocated block we set sz(a) = [−∞,+∞].
The reduced product consists of refininig the expressiveness
of each lattice by bringing information from the other one.
In practice this is performed by applying a reduction opera-
tion σ defined as follows:
σ(A,O, S) = {a ∈ A | sz(a) ∈ S},O, S ∩ ∪
a∈A
sz(a)
The effect of this operation is to remove spurious references
and reduce the size range, which results in better accuracy.
The reduction should always be performed on an abstract
memory reference before any operation is applied to it. In
practice reduction turned out to be very important, because
in many cases the numerical information was too coarse to
represent the size precisely.
An abstract memory configuration is thereby a couple
(E,H) where E is an abstract environment mapping each
local pointer variable of a function to an abstract memory
reference and each local integer variable to an interval, and
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料36(57)
