ES_PASS

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.