Analysing Switch-Case Code with Abstract Execution

Holsti, Niklas; Gustafsson, Jan; Källberg, Linus; Lisper, Björn

doi:10.4230/OASIcs.WCET.2015.85

File

OASIcs.WCET.2015.85.pdf

Filesize: 441 kB
10 pages

Document Identifiers

DOI: 10.4230/OASIcs.WCET.2015.85
URN: urn:nbn:de:0030-drops-52598

Author Details

Niklas Holsti

Jan Gustafsson

Linus Källberg

Björn Lisper

Cite AsGet BibTex

Niklas Holsti, Jan Gustafsson, Linus Källberg, and Björn Lisper. Analysing Switch-Case Code with Abstract Execution. In 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015). Open Access Series in Informatics (OASIcs), Volume 47, pp. 85-94, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/OASIcs.WCET.2015.85

Abstract

Constructing the control-flow graph (CFG) of machine code is made difficult by dynamic transfers of control (DTC), where the address of the next instruction is computed at run-time. Switchcase statements make compilers generate a large variety of machine-code forms with DTC. Two analysis approaches are commonly used: pattern-matching methods identify predefined instruction patterns to extract the target addresses, while analytical methods try to compute the set of target addresses using a general value-analysis. We tested the abstract execution method of the SWEET tool as a value analysis for switch-case code. SWEET is here used as a plugin to the Bound-T tool: thus our work can also be seen as an experiment in modular tool design, where a general value-analysis tool is used to aid the CFG construction in a WCET analysis tool. We find that the abstract-execution analysis works at least as well as the switch-case analyses in Bound-T itself, which are mostly based on pattern-matching. However, there are still some weaknesses: the abstract domains available in SWEET are not well suited to representing sets of DTC target addresses, which are small but sparse and irregular. Also, in some cases the abstract-execution analysis fails because the used domain is not relational, that is, does not model arithmetic relationships between the values of different variables. Future work will be directed towards the design of abstract domains eliminating these weaknesses.

Keywords

ynamic control flow
indexed branch
machine-code analysis
WCET analysis

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

References

The Atmel AVR. URL: http://en.wikipedia.org/wiki/Atmel_AVR.
Gogul Balakrishnan and Thomas Reps. WYSINWYX: What you see is not what you execute. ACM Trans. Program. Lang. Syst., 32(6):23:1-23:84, August 2010.
C. Cifuentes and M. Van Emmerik. Recovery of jump table case statements from binary code. In Proc. Seventh International Workshop on Program Comprehension, pages 192-199, 1999.
Philippe Granger. Static analysis of arithmetical congruences. International Journal of Computer Mathematics, 3:165-199, 1989.
Jan Gustafsson, Andreas Ermedahl, Björn Lisper, Christer Sandberg, and Linus Källberg. ALF - a language for WCET flow analysis. In Niklas Holsti, editor, WCET'09, pages 1-11, Dublin, Ireland, June 2009. OCG.
Jan Gustafsson, Andreas Ermedahl, Christer Sandberg, and Björn Lisper. Automatic derivation of loop bounds and infeasible paths for WCET analysis using abstract execution. In Proc. 27^th IEEE Real-Time Systems Symposium (RTSS'06), pages 57-66, Rio de Janeiro, Brazil, December 2006. IEEE Computer Society.
Niklas Holsti. Analysing switch-case tables by partial evaluation. In Proc. 7^th International Workshop on Worst-Case Execution Time Analysis (WCET'07), 2007.
Niklas Holsti. Computing time as a program variable: a way around infeasible paths. In Proc. 8^th International Workshop on Worst-Case Execution Time Analysis (WCET'08), Prague, Czech Republic, July 2008.
Niklas Holsti, Jan Gustafsson, Linus Källberg, and Björn Lisper. Combining Bound-T and SWEET to analyse dynamic control flow in machine-code programs. Technical report, Mälardalen Real-Time Research Centre, Mälardalen University, November 2014.
Björn Lisper. SWEET - a tool for WCET flow analysis (extended abstract). In Tiziana Margaria and Bernhard Steffen, editors, Proc. 6^th International Symposium on Leveraging Applications of Formal Methods (ISOLA'14), volume 8803 of Lecture Notes in Computer Science, pages 482-485, Corfu, Crete, October 2014. Springer-Verlag.
Tidorum Ltd. Bound-T time and stack analyser. URL: http://www.bound-t.com.
Hex-Rays SA. IDA disassembler. URL: https://www.hex-rays.com/products/ida.
Rathijit Sen and Y. N. Srikant. Executable analysis using abstract interpretation with circular linear progressions. In Proc. 5th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE'07), pages 39-48, Washington, DC, USA, 2007. IEEE Computer Society.
Henrik Theiling. Extracting safe and precise control flow from binaries. In Proc. 7th International Conference on RealTime Computing Systems and Applications (RTCSA'00), pages 23-30, Cheju Island, South Korea, 2000. IEEE.
Arnaud Venet. Abstract cofibered domains: Application to the alias analysis of untyped programs. In Radhia Cousot and David A. Schmidt, editors, Proc. Third International Symposium on Static Analysis (SAS'96), volume 1145 of Lecture Notes in Computer Science, pages 366-382. Springer Berlin Heidelberg, Aachen, Germany, 1996.
W. Pugh et al. The Omega Project: Frameworks and algorithms for the analysis and transformation of scientific programs. URL: http://www.cs.umd.edu/projects/omega.