OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Multi-architecture Value Analysis for Machine Code

Cassé, Hugues and Birée, Florian and Sainrat, Pascal Multi-architecture Value Analysis for Machine Code. (2013) In: 13th International Workshop on Worst-Case Execution Time Analysis - WCET 2013, 9 July 2013 - 9 July 2013 (Paris, France).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: http://dx.doi.org/10.4230/OASIcs.WCET.2013.42


Safety verification of critical real-time embedded systems requires Worst Case Execution Time information (WCET). Among the existing approaches to estimate the WCET, static analysis at the machine code level has proven to get safe results. A lot of different architectures are used in real-time systems but no generic solution provides the ability to perform static analysis of values handled by machine instructions. Nonetheless, results of such analyses are worth to improve the precision of other analyzes like data cache, indirect branches, etc. This paper proposes a semantic language aimed at expressing semantics of machine instructions whatever the underlying instruction set is. This ensures abstraction and portability of the value analysis or any analysis based on the semantic expression of the instructions. As a proof of concept, we adapted and refined an existing analysis representing values as Circular-Linear Progression (CLP), that is, as a sparse integer interval effective to model pointers. In addition, we show how our semantic instructions allow to build back conditions of loop in order to refine the CLP values and improve the precision of the analysis. Both contributions have been implemented in our framework, OTAWA, and experimented on the Malardalen benchmark to demonstrate the effectiveness of the approach.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Schloss Dagstuhl editor. The original PDF of the article can be found at : http://dx.doi.org/10.4230/OASIcs.WCET.2013.42. Licensed under a Creative Commons license CC BY : http://creativecommons.org/licenses/by/3.0/. No changes were made.
HAL Id:hal-01148808
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Laboratory name:
Deposited On:30 Apr 2015 12:59

Repository Staff Only: item control page