Document Open Access Logo

Analysing Switch-Case Code with Abstract Execution

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

PDF
Thumbnail PDF

File

OASIcs.WCET.2015.85.pdf
  • Filesize: 441 kB
  • 10 pages

Document Identifiers

Author Details

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

Cite As Get 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.

Subject Classification

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

  1. The Atmel AVR. URL: http://en.wikipedia.org/wiki/Atmel_AVR.
  2. 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. Google Scholar
  3. 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. Google Scholar
  4. Philippe Granger. Static analysis of arithmetical congruences. International Journal of Computer Mathematics, 3:165-199, 1989. Google Scholar
  5. 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. Google Scholar
  6. 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. Google Scholar
  7. Niklas Holsti. Analysing switch-case tables by partial evaluation. In Proc. 7^th International Workshop on Worst-Case Execution Time Analysis (WCET'07), 2007. Google Scholar
  8. 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. Google Scholar
  9. 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. Google Scholar
  10. 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. Google Scholar
  11. Tidorum Ltd. Bound-T time and stack analyser. URL: http://www.bound-t.com.
  12. Hex-Rays SA. IDA disassembler. URL: https://www.hex-rays.com/products/ida.
  13. 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. Google Scholar
  14. 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. Google Scholar
  15. 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. Google Scholar
  16. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact