曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
computing two fixpoint iterations, the first one with widening
the second with narrowing. These calculations should
be performed on the whole program, i.e. hundreds of thousands
lines of C, at each step of the heap refinement process
described in the previous section. In practice, we measured
that at least five global iterations over the program are
needed to achieve a good level of precision. It was unrealistic
to perform a full-strength fixpoint iteration at each step;
it would severely impair the efficiency of the analyzer. We
decided to first compute a summary of each function of the
program by using a relational numerical lattice as described
in [11].
As for the points-to inclusion constraints, given a function
f of the program, we associate two numerical metavariables
Op and Sp to each local variable p of f that may carry a
pointer. The metavariables Op and Sp represent respectively
the offset and size ranges of the abstract memory reference
carried by the variable. We also associate a metavariable
In to each integer valued local variable n. Recall that local
variables that are address-taken are globalized and never occur
in an abstract environment. We also attach two anchor
metavariables Oℓ and Sℓ to each location ℓ of a memory
read/write operation or a function call that may return a
pointer. The metavariables Oℓ and Sℓ represent respectively
the offset and size ranges of the abstract memory reference
returned by the operation at that point. We similarly attach
special anchors Ox@f and Sx@f (resp. Ix@f) to each
pointer-valued (resp. integer-valued) formal parameter x of
f. .
We could also attach anchor metavariables Iℓ to each location
ℓ of a memory read operation or a function call that
returns an integer. CGS actually has command-line options
to generate such anchors. The representation of integer values
in the abstract heap is identical to that of pointers, i.e.
it consists of mapping a memory location ha,O, Si to an interval
[a, b]. Some extra care is required when reading an
integer from the heap in order to ensure that the offset of
the read operation is aligned with the offset of the integer
in the memory block, otherwise this would result into returning
a truncated value. Similarly we have to make sure
that the sizes match, for example if we try to read a byte
from the location of an integer, otherwise the results would
be inconsistent. We address these issues in a very simple
way: whenever we encounter a read operation of an integer
of size s from the address a at the offset O′ and there is
a mapping ha,O, Si 7→ [a, b] in the abstract heap, we return
the interval [a, b] if and only if O and S are singletons
and O = O′, S = [s, s]. We return [−∞,+∞] otherwise.
Surprisingly enough, the experiments showed no noticeable
gain in precision on the MPF family with this option of CGS
enabled.
Now we need to choose a relational abstract domain for
representing relationships between the numerical metavariables.
Consider for example the following function which is
representative of the matrix computations performed in the
programs of the MPF family:
void equate (double *p, double *q, int n) {
int i;
for (i = 0; i < n; i++)
p[i] = q[i];
}
In the abstract syntax tree of this function the body of the
loop is represented by the three following statements:
a = p + i;
b = q + i;
c = *b;
*a = c;
The variables a, b and c are internal names generated by
the front-end. If we assume that the size of a double is 8
bytes, the exact loop invariant is given by
Sa = Sp@equate
0 ≤ Oa − Op@equate ≤ 8 ∗ In@equate − 8
Sb = Sq@equate
0 ≤ Ob − Oq@equate ≤ 8 ∗ In@equate − 8
where we have eliminated all metavariables associated to
local integer variables of the function, since they are just
used for storing the result of intermediate computations. It
immediately appears in this simple example that we need
general linear inequalities in order to be precise. The only
abstract domain that is expressive enough for representing
this kind of invariants is the lattice of convex polyhedra [12].
Unfortunately, because of the complexity of the underlying
algorithms this lattice cannot be used for representing relationships
between more than 20 variables in practice. The
functions in the codes of the MPF family can be quite large
and use many pointers simultaneously. We found that in
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料36(61)
