Information Technology Reference
In-Depth Information
a)
b)
0010
****
0010
****
00100110
00101
***
0010011
*
00101
***
00101001
00101101
00100110 00100111
00101001 00101101
Fig. 5.
Example of a Patricia trie
a)
before, and
b)
after inserting
00100111
Thanks to these primitives, the (unoptimized) instrumentation for record-
ing in the store is mostly straightforward. To monitor the block of an argu-
ment or a local variable
v
of type
T
in function
f
, e-acsl2c adds the calls
__store_block(&v,
sizeof
(T))
in the beginning, and
__delete_block(&v)
at the end of
the scope of
v
. For a global variable, these calls are inserted in the beginning
and at the end of the function
main
. In addition to them, for global variables
(initialized by default to 0 in C) and function arguments (initialized by a func-
tion call), the
__store_block(&v,
sizeof
(T))
is followed by
__full_init(&v)
to mark
the whole block as initialized. To monitor an assignment
v = exp;
to a variable
(or a left value)
v
,acallto
__initialize(&v,
sizeof
(v));
is inserted. Literal strings
and initializers are easily handled as well. Finally, dynamic allocation functions
are simply replaced by their instrumented counterparts.
4 Optimized Storage for the Memory Monitoring Library
Ecient implementation of the store requires a data structure with a good time
and space complexity, since the instrumented code may perform frequent modi-
fications and lookups in the store. It is intuitively clear that the structure has to
be sorted: treating e-acsl constructs may require to access a block metadata di-
rectly by its base address as well as to find a block's predecessor or successor. For
example, the query
__base_addr(p)
searches the store for the closest to
p
base ad-
dress less than
p
(and checks the bounds afterwards). Thus, a hash table will not
fit. Lists are not ecient enough due to a linear worst-case complexity. Unbal-
anced binary search trees have a linear worst-case complexity too when inserted
base addresses are monotonically increasing, and this may be quite common.
Finally, the cost of balancing (e.g. in a self-balancing binary search tree) would
be amortized if the store modifications (that may lead to rebalancing) were less
frequent than simple queries (that take advantage of a balanced structure). For
tested examples of code instrumented by e-acsl2c this is not necessarily true.
Our implementation of the store is based on a
Patricia trie
[8], also known as
a
radix tree
or
compact prefix tree
, which is ecient even if the tree is unbalanced.
Node keys are base addresses (e.g. 32-bit or 64-bit words) or address prefixes.
Any leaf contains a block metadata with the block base address. Routing from
the root to a block metadata is ensured by internal nodes, each of them contains
the greatest common prefix of base addresses stored in its successors.
For instance, Fig. 5a shows a Patricia trie, for simplicity, over 8-bit addresses.
It contains three blocks in its leaves (only block base addresses are shown here),
and greatest common prefixes in internal nodes. A “
*
” denotes meaningless bits