曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
some functions more than 30 pointers were active in the
body of a loop. Moreover, the abstract syntax tree representation
provided by the front-end introduces numerous
internal variables since all statements are broken down into
a 3-address format.
Some numerical relational lattices have been developed
recently that showed good promises of scalability [20, 21].
However they are not expressive enough for representing the
kind of linear inequalities in which we are interested. They
can only express linear inequalities between two variables
and the coefficients of these variables may only be 1 or -1.
Our solution consists of modifying the form of our numerical
constraints by introducing additional variables so that the
overall expressiveness of a system of numerical constraints
is kept constant, whereas the class of numerical relations
required to achieve this expressiveness is simpler.
More precisely, it appears that the main source of complexity
comes from the byte-based representation of offsets.
An array access p[i] is transformed into an arithmetic expression
in which we multiply the index by the size of an
array element expressed in bytes. We extend the representation
of a pointer p by attaching additional metavariables
δ1(p), . . . , δk(p) and u1(p), ..., uk(p) for a fixed k. A pair
(δi(p), ui(p)) represents an offset expressed in a different unit
than the byte. δi(p) is the relative offset and ui(p) is the
base. The actual offset in bytes denoted by this representation
is given by the following formula:
Op +
k
X
i=1
δi(p) ∗ ui(p)
We call the representation Wp = hOp, (δ1(p), u1(p)), . . . ,
(δk(p), uk(p))i a sliding window. We call Op the base offset.
The associated sliding operation slide(Wp, δ, u) is defined as
follows:
slide(Wp, δ, u) = hOp + δ1(p) ∗ u1(p), (δ2(p), u2(p)), . . . ,
(δk−1(p), uk−1(p)), (δ, u)i
The initial values of the sliding window for metavariables
associated to inputs of the function, i.e. the parameters and
the return values of a memory read or a function call, are
set to 0 except for the base offset and uk. The base offset is
the one associated to the metavariable and uk is the size of
the element pointed to by the variable as it appears in the
type inferred by the C front-end.
The sliding operation is used for handling a type cast operation
p = (T∗)q. When analyzing this operation we first
retrieve the range of uk(q) from the current system of inequalities.
If it is a singleton and it is equal to the size t
of T then Wp = Wq, otherwise Wp = slide(Wq, 0, t). This
way uk always represents the size of the element currently
pointed-to by the variable. Whenever a pointer arithmetic
operation p = q + n is analyzed, the sliding window Wp is
equated to Wq except for δk(p) for which the constraint
δk(p) = δk(q) + In is generated. Now if we analyze the
function equate with sliding windows of size k = 2 and the
abstract numerical domain of difference-bound matrices [20],
we obtain the following system of constraints for the loop
invariant:
Sa = Sp@equate
Oa = Op@equate
δ1(a) = u1(a) = 0
0 ≤ δ2(a) ≤ In@equate − 1
u2(a) = 8
Sb = Sq@equate
Ob = Oq@equate
δ1(b) = u1(b) = 0
0 ≤ δ2(b) ≤ In@equate − 1
u2(b) = 8
We can express the exact loop invariant with a less powerful
abstract lattice and more variables.
We chose the domain of difference-bound matrices [20]
(DBMs for short) for expressing numerical constraints between
variables. In this domain a constraint may only have
the form x − y ≤ c where c is an integer. The fundamental
operation on a DBM is the normalization that refines
constraints by repeated application of the following rule:
x − y ≤ c
y − z ≤ c′
x − z ≤ c′′
⇒ x − z ≤ min(c + c′, c′′)
Our choice was motivated by the observation that DBMs
have a sufficient expressiveness for our purpose and by the
existence of an efficient quadratic algorithm devised by Johnson
[6] for the normalization of sparse systems of constraints.
We assumed indeed that the systems of constraints would
be rather sparse, since it would be very unlikely to have all
variables in a function related at the same time. Our first implementation
used Floyd-Warshall’s algorithm [6] for computing
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料36(62)
