OASIcs.WCET.2015.95.pdf
- Filesize: 487 kB
- 10 pages
Document
Using SMT Solving for the Lookup of Infeasible Paths in Binary Programs
Authors
-
Part of:
Volume:
15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)
Series: Open Access Series in Informatics (OASIcs)
Conference: Workshop on Worst-Case Execution Time Analysis (WCET) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2015-07-06
Cite As Get BibTex
Jordy Ruiz and Hugues Cassé. Using SMT Solving for the Lookup of Infeasible Paths in Binary Programs. In 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015). Open Access Series in Informatics (OASIcs), Volume 47, pp. 95-104, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/OASIcs.WCET.2015.95
Abstract
Worst-Case Execution Time (WCET) is a key component to check temporal constraints of realtime systems. WCET by static analysis provides a safe upper bound. While hardware modelling is now efficient, loss of precision stems mainly in the inclusion of infeasible execution paths in the WCET calculation. This paper proposes a new method to detect such paths based on static analysis of machine code and the feasibility test of conditions using Satisfiability Modulo Theory (SMT) solvers. The experimentation shows promising results although the expected precision was slightly lowered due to clamping operations needed to cope with complexity explosion. An important point is that the implementation has been performed in the OTAWA framework and is independent of any instruction set thanks to its semantic instructions.
Subject Classification
Keywords
- WCET
- infeasible paths
- SMT
- machine code
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
C. Barrett, C. Conway, M. Deters, L. Hadarean, D. Jovanovic, T. King, A. Reynolds, and C. Tinelli. CVC4. In 23rd International Conference on Computer Aided Verification (CAV'11), volume 6806 of Lecture Notes in Computer Science. Springer, 2011.
-
C. Barrett, M. Deters, L. de Moura, A. Oliveras, and A. Stump. 6 Years of SMT-COMP. Journal of Automated Reasoning, 50(3):243-277, 2013.
-
H. Cassé, F. Birée, and P. Sainrat. Multi-architecture value analysis for machine code. In WCET'13, pages 42-52. OASICs, Dagstuhl Publishing, 2013.
-
J. Gustafsson, A. Betts, A. Ermedahl, and B. Lisper. The Mälardalen WCET Benchmarks: Past, Present And Future. WCET, 15:136-146, 2010.
-
J. Henry, M. Asavoae, D. Monniaux, and C. Maïza. How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics. SIGPLAN Not., 49(5):43-52, June 2014.
-
V. Suhendra, T. Mitra, A. Roychoudhury, and Ting C. Efficient detection and exploitation of infeasible paths for software timing analysis. In Design Automation Conference, 2006 43rd ACM/IEEE, pages 358-363, 2006.
-
N. Williams, B. Marre, P. Mouy, and M. Roger. PathCrawler: Automatic generation of path tests by combining static and dynamic analysis. In Dependable Computing - EDCC 5, volume 3463 of Lecture Notes in Computer Science, pages 281-292. Springer, 2005.