Information Technology Reference
In-Depth Information
1
int
last;
2
int
*
new_inversed(
int
len,
int
*
v) {
3
int
i,
*
p;
__store_block(&v,
sizeof
(
int
*
)); __full_init(&v);
4
if
(!( __valid(v,
sizeof
(
int
)) && __offset(v)+len
*
sizeof
(
int
) <= __block_length(v) ))
5
e_acsl_fail("new_inversed","assert","line 4");
6
p = __malloc(
sizeof
(
int
)
*
len);
7
for
(i=0; i<len; i++)
8
p[i] = v[len-i-1];
9
__delete_block(&v);
10
return
p;
11
12
}
13
int
main() {
14
int
v1[3]={1,2,3},
*
v2;
__store_block(v1,3
*
sizeof
(
int
)); __full_init(v1);
15
if
(! __valid(v1+2,
sizeof
(
int
)) ) e_acsl_fail("main","assert","line 13");
16
last = v1[2];
17
v2 = new_inversed(3, v1);
18
last = v2[2];
19
if
(!( last == 1 )) e_acsl_fail("main","assert","line 17");
20
__free(v2);
21
__delete_block(v1); __clean();
22
23
}
Fig. 8.
Simplified instrumentation of the file
vector.c
of Fig. 7 with e-acsl2c
these e-acsl annotations, the analysis goes backwards in the code in order to
find where the monitored variables
v
and
v1
are assigned and where aliases are
potentially created.
More precisely, the analysis starts from the end of the program with
σ
=
,
and goes backwards up to the beginning, analyzing statements, annotations and
called functions in order to collect memory locations to be monitored into
σ
.For
the example of Fig. 7, it collects nothing until the assertion at line 5 in function
new_inversed
called from the line 15 (still in a context with
σ
=
∅
). At this point,
it remembers that
v
has to be monitored. Going back to the callsite (line 15), as
the formal parameter
v
has to be monitored, the corresponding argument
v1
is
also collected into
σ
. For the assertion of line 13, the analysis computes that
v1
has to be monitored (actually, it is already in
σ
, so nothing new is discovered).
Finally the analysis concludes that
v
and
v1
have to be monitored, leading to the
optimized instrumentation of Fig 8. We notice that variables
last
,
len
,
i
,
p
and
v2
are not monitored, unlike in the unoptimized instrumentation.
If
v1
was a pointer referring to another array
v3
(e.g. if the line 12 was
int
v3[3]={1,2,3},
*
v1=v3,
*
v2;
), the analysis would deduce from the assignment
v1=v3
that
v3
should be monitored as well.
Experiments.
In the tested examples, the optimization based on dataflow anal-
ysis reduced the total execution time of instrumented code by 66% in average. It
is due to a smaller number of monitored variables (decreasing by 78% in average)
and hence a smaller number of records and queries to the store (number of calls
to
gtCommonPrefixMask
throughout the execution decreased by 71% in average).
The analysis was rather fast: no example has been slowed down by integrating
this optimization.
∅
