ES_PASS Workshop: Industrialization of Abstract Interpretation 2009
Oct. 28, 2009, Madrid, Spain
Generating Annotations for a Binary Analyzer from Source-Level Analysis.
Hard real-time systems are systems in which computations have
mandatory deadlines. In these systems, making sure that the system's
answers are computed in time is as important as making sure that the
answers are right (functional correctness). The time taken by a
computation cannot be computed from source-code alone: indeed, this
time very much depends on the way the source code is transformed into
assembly by the compiler. It also depends on the particular model of
processor on which the code executes, among all which implement this
instruction set.
AbsInt provides a suite of binary code analyzers (a3), including aiT,
which can give a precise bound on the worst-case execution time of a
task. Analyzing binary code is a difficult task. Some useful
information that was available at source level is difficult to
recover; the user typically must provide annotations to help the
analysis. Because this process can be tedious, usually, only the code
whose timing is important is analyzed, although it is possible to
analyze some of its calling context to extract useful information and
make the WCET estimation more precise.
Frama-C's value analysis is a source code analyzer for embedded C
code. Like a3, it computes supersets of possible values for the
variables of the analyzed program. Working at the source level gives
it two chances to be more precise than a3 at determining values of
variables in a same program. First, the source code has more
structure. Second, because source is easier to analyze, it becomes
possible to include more context in the analysis, yielding more
precise information on the state in which the task under analysis is
executed.
We show how these two tools can be interfaced concretely, in order to
improve the process of computing WCET using aiT. Among the results
computed by Frama-C's value analysis, those that seem likely to be
useful to a3 are picked up and exported in a file written in a3's
format for user annotations. This technique is implemented as a
Frama-C plug-in, with no modification to the value analysis. This new
plug-in makes use of the existing API for accessing the value
analysis' results.
Back to Program.