曝光台 注意防骗
网曝天猫店富美金盛家居专营店坑蒙拐骗欺诈消费者
3. ABSTRACT SEMANTICS
The symbolic and numerical parts of an abstract memory
reference are independent, which means that we can compute
these two pieces of information separately. We just
need to perform a reduction operation σ whenever there is
a context change (function call) or an interaction with the
abstract heap (memory read). The choice of performing a
cartesian approximation for the abstract memory references
was mainly motivated by this simplifying assumption in the
abstract semantics.
We generate two separate sets of semantic equations for
each function in the program, one for the symbolic part in
the form of inclusion constraints between points-to sets, the
second as a system of numerical constraints between offset
and size variables. The resolution of these equations follows
the call graph by propagating call contexts made of points-to
sets and intervals. The symbolic and numerical systems associated
to a function f are solved separately for all possible
call contexts of f (depending on whether context-sensitivity
is enabled for this function or not). The resolution of these
two systems of equations is interleaved, interactions occurring
whenever some information is retrieved from the environment,
i.e. by a memory read. In this case we have
to combine the numerical and symbolic information in order
to query the memory graph H used at this step of the
resolution.
3.1 Pointsto
Inclusion Constraints
Given a function f of the program, we associate a metavariable
Ap to each local variable p of f that may carry a
pointer (either a pointer variable itself or a compound variable
with pointer-valued fields). These metavariables represent
the first component of an abstract memory reference,
i.e. a set of symbolic addresses. Following the model defined
in [26] we associate an anchor metavariable Aℓ to each location
ℓ of a memory read operation or a function call that may
return a pointer. The metavariable Aℓ represents the set of
addresses returned by the read operation or the function call.
We similarly assign a special anchor metavariable Ax@f to
each formal parameter x of f that may carry a pointer. This
anchor denotes the points-to set of the argument passed to
the function and is used during interprocedural propagation.
Following Andersen’s model [2] we use inclusion constraints
of the form Ap ⊇ Aq to relate the metavariables.
The generation of inclusion constraints is quite straightforward.
For all assignments p = q, p = q + n (pointer
arithmetic) or p = (T *)q (type cast), we generate a constraint
Ap ⊇ Aq. For all memory read operation p = *q or
function call p = f (...) at a location ℓ in the program
we generate a constraint Ap ⊇ Aℓ and we record a semantic
operation read(Aℓ,Aq) which is used during interprocedural
propagation for querying the abstract memory graph. A
memory write operation *p = q is not assigned an inclusion
constraint, it is simply assigned a semantic operation
write(Ap,Aq) which is used at the end of an analysis pass to
generate a new abstract heap, as described in the previous
section. Similarly a return p statement is recorded separately
as return(Ap) and is used for the construction of the
transformers in the backward propagation phase described
in Sect. 3.3. We must also add the constraints corresponding
to the implicit binding relations between formal and actual
parameters as follows: Ax ⊇ Ax@f, for all formal parameter
x of f.
The resolution of these constraints differs from Andersen’s
algorithm [2] since read operations retrieve data from
the abstract memory graph H and require some information
about the offset at which the memory block is read. Our algorithm
consists of a local fixpoint iteration that computes
a set of symbolic addresses for each metavariable of f and
launches the resolution of numerical constraints on demand
whenever a memory read is encountered. For efficiency the
resolution algorithm implemented in CGS first computes the
directed acyclic graph of strongly connected components of
the dependency graph of the system of inclusion constraints.
The iterations are then performed locally on each strongly
connected component following a weak topological ordering
of the metavariables [4].
3.2 Numerical Constraints
Classically, when building an abstract interpretation of
numerical computations, the abstract semantic equations
follow the program structure [12]. A loop statement in the
body of a function will appear as a recursive dependency in
the equations. Solving the system precisely usually requires
中国航空网 www.aero.cn
航空翻译 www.aviation.cn
本文链接地址：
航空资料36(60)
