Information Technology Reference
In-Depth Information
1
#include
<stdlib.h>
2
int
last;
3
int
*
new_inversed(
int
len,
int
*
v) {
4
int
i,
*
p;
//@
assert \valid
(v) &&
\offset
(v)+len
*
sizeof
(
int
)<=
\block_length
(v);
5
p = malloc(
sizeof
(
int
)
*
len);
// allocate a new vector p
6
for
(i=0; i<len; i++)
7
p[i] = v[len-i-1];
// write inversed vector v into p
8
return
p;
9
10
}
11
void
main() {
12
int
v1[3]={1,2,3},
*
v2;
//@
assert \valid
(&v1[2]);
13
last = v1[2];
14
v2 = new_inversed(3, v1);
15
last = v2[2];
16
//@
assert
last == 1;
17
free(v2);
18
19
}
Fig. 7.
File
vector.c
where the function
new_inversed
allocates and returns a new vector
containing the inversed given vector
v
of
len
integers
instrumented code in average 2.7 times faster.Thisrategoesupto4.7timesfor
examples with intensive usage of the memory monitoring library.
6 Optimized Instrumentation Using Static Analysis
The instrumentation presented in Sec. 3 is sound and complete: the code in-
strumented by e-acsl2c reports an e-acsl annotation failure at runtime if
and only if this e-acsl annotation is indeed violated. However it has the ma-
jor drawback of being hugely verbose and time-consuming: for each variable,
each (de)allocation and each assignment, one or even several new statements are
generated. It is however su
cient to monitor the memory locations involved in
memory-related constructs in the provided e-acsl annotations.
To solve this drawback, we have designed an interprocedural backward data-
flow analysis which computes an over-approximated set
σ
of memory locations
that it is sucient to monitor in order to preserve soundness and completeness
of the instrumentation. Let us explain on the example of Fig. 7 how this analysis
works (for lack of space, we do not give its formal presentation here). Without
any analysis, we have to monitor every variable of the program and to record
when it is allocated, initialized and deallocated by systematically adding calls
to the recording primitives of Fig. 4 as explained in Sec. 3.2.
However, this monitoring is only required for memory blocks involved in
memory-related e-acsl constructs. In our example, they are
\valid
(v)
,
\offset
(v)
and
\block_length
(v)
at line 5, and
\valid
(&v1[2])
at line 13. So we need to monitor
the formal parameter
v
of function
new_inversed
and the location
&v1[2]
.Forthe
latter, we keep less precise information. Our current analysis is purely syntacti-
cal and does not perform any precise semantic aliasing analysis. To be sound, we
perform an over-approximation and monitor any information about the whole
local array
v1
of function
main
, including
*
(v1+i)
for any offset
i
. Basically, from
