曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
H is an abstract heap. An abstract heap is a set of points-to
relations h(a,O) 7→ (a′,O′, S)i where a, a′ are addresses and
O,O′, S are intervals. Such a relation expresses that there
may be references in the block a within the range of offsets
O to the elements within the range of offsets O′ in the block
a′, the size of which lies in the interval S. Furthermore, we
impose that there are no two distinct points-to relations in
H with the same addresses a and a′. We perform two additional
approximations that are crucial for the tractability
of this model:
1. Abstract environments are field-insensitive, i.e. we do
not distinguish between the values of fields within a
compound local variable.
2. Local variables that are address-taken (i.e. modified
through a pointer reference) are globalized, i.e. they
are represented in the abstract heap H. This means
that we cannot distinguish the value of such a variable
between different execution contexts.
These approximations ensure that the domain of an abstract
environment E only contains variable names without any
offset information, and that any modification of the value of
a variable v in E may only be performed by an assignment
operation in which v explicitly appears. Even though local
structures and address-taken variables are quite common in
the MPF family, they rarely concern variables that carry
pointers. Thus the impact of these approximations on the
precision is low whereas they greatly simplify the design of
the analyzer.
As is, the classical abstract interpretation framework that
assigns an abstract memory configuration (E,H) at each
control point is not applicable to heavily multithreaded programs,
since this requires considering all possible thread interleavings.
A solution would be to use a flow-insensitive
analysis, which can obviously cover all possible thread interleavings
at a low cost. However, the array bound checking
absolutely requires precise loop invariants, which cannot be
obtained without flow-sensitivity. Our solution consists of
using a mixed framework similar to that of [26] in which the
abstract environment E is computed in a flow-sensitive way
whereas the abstract memory heap H is constructed in a
flow-insensitive way.
More precisely, let H be an abstract heap that is a conservative
approximation of all possible heaps that can be generated
by the program at any point of any execution. We
perform a flow-sensitive analysis by keeping the second component
of the abstract memory configurations equal to H.
In this case we do not have to consider any thread interleaving
at all since the variables in the domain of the abstract
environments are thread-local. We simply analyze the program
as if it were sequential, the initial states being given
by all the thread entry points. During the analysis memory
reads are always performed on H and memory writes are
never taken into account. More precisely, if p = *q is a read
operation that fetches a pointer from the heap, we get the
abstract memory reference (A,O, S) associated to q at this
stage of the computation. The result of the read operation
is the join of all memory references ({a′},O′, S′) for which
there exists a points-to relation h(a,O′′) 7→ (a′,O′, S′)i in
H such that a ∈ A & O ∩ O′′ 6= ∅.
At the end of the analysis, we consider all memory write
operations of the program. For each such operation *p = q
that may carry a pointer we retrieve the abstract memory
reference (A,O, S) associated to p and the abstract memory
reference (A′,O′, S′) associated to q at this point. For each
a in A and each a’ in A′, we generate a points-to relation
h(a,O) 7→ (a′,O′, S′)i. We gather all the points-to relations
generated this way to form a new abstract heap H′. The
abstract heap H′ satisfies two properties:
1. H′ is a conservative flow-insensitive approximation of
all actual heaps of the program.
2. H′ refines H, denoted by H′ ⊑ H: for all h(a,O1) 7→
(a′,O′
1, S1)i in H′, there is a points-to relation h(a,O2)
7→ (a′,O′
2, S2)i such that O1 ⊆ O2,O′
1 ⊆ O′
2 & S1 ⊆
S2.
This provides us with a process for incrementally refining
the abstract heap. We start with a coarse flow-insensitive
approximation of the heap H0 and we construct a decreasing
sequence H0 ⊒ H1 ⊒ · · · ⊒ Hn of abstract heaps with
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料36(58)
