Information Technology Reference
In-Depth Information
verification
and conclude that “one of its main technical challenges is the syn-
thesis of ecient monitors from logical specifications” [4]. An ecient memory
monitoring for C programs is the purpose of the present work.
In this paper, we present the solution for memory monitoring of C programs
we have developed for runtime assertion checking in Frama-C [5], a platform
for analysis of C code. It includes an expressive executable specification lan-
guage e-acsl and a translator, called e-acsl2c in this paper, that automati-
cally translates an e-acsl specification into C code [6, 7]. In order to support
memory-related annotations for pointers and memory locations (such as being
valid, initialized, in a particular block, with a particular offset, etc.), we need to
keep track of relevant memory operations previously executed by the program.
Hence, we have developed a monitoring library for recording and retrieving va-
lidity and initialization information for the program's memory locations, as well
as an automatic instrumentation of source code in e-acsl2c inserting necessary
calls to the library during the translation of an e-acsl specification into C.
The proposed solution is designed both for
passive
and
active
monitoring,
though this paper discusses only passive monitoring, that is the default one.
Passive monitoring only aims at observing and reporting failures, while active
monitoring introduces new actions e.g. for recovery from detected erroneous
situations. Our solution implements a
non-invasive
source code instrumentation,
that is, monitoring routines do not change the observed behavior of the program.
In particular, it does not modify the memory layout and size of variables and
memory blocks already present in the original program, and may only record
additional monitoring data in a separate memory store.
The contributions of this paper include:
-
a detailed description of our solution of memory monitoring for runtime
assertion checking with Frama-C [5], allowing to automatically generate
monitors from assertions and function contracts written in the e-acsl spec-
ification language [6];
-
an ecient storage of memory related operations based on Patricia tries [8];
-
optimized records and queries in the store for faster recording and retrieving
information on memory blocks;
-
an optimized instrumentation reducing the amount of memory monitoring
for memory locations that are irrelevant with respect to the provided asser-
tions;
-
experiments illustrating the benefits of these optimizations and the capacity
of error detection using e-acsl.
The paper is organized as follows. Sec. 2 presents the context of this work,
including Frama-C and e-acsl. Sec. 3 gives a global overview of our solution
for memory monitoring, in particular, the instrumentation realized by e-acsl2c
and the basic primitives provided by our monitoring library. Optimized data
storage and search operations are described respectively in Sec. 4 and 5. Sec. 6
presents the optimization reducing irrelevant memory monitoring. Our initial
experiments are described in Sec. 7 and summarized at the end of Sec. 4, 5 and
6. Finally, Sec. 8 and 9 present respectively related work and the conclusion.
