Towards device emulation code generation

ABSTRACT

For non-embedded software, binary translation has shown to be a successful method for retargeting legacy software onto new platforms. To apply binary translation to embedded software, two issues must be considered. First of all, embedded software often involves real-time constraints that must still be met after translation. Secondly, embedded software contains a significant amount of code dedicated to peripheral device communication which necessitates device emulation. This paper focuses on the last aspect.

Usually, device emulation code is handcrafted which is tedious and error-prone. This paper presents a method to automatically generate device emulation code from a formal specification of source and target device operations. At the heart of the device operation semantics lie quantifier-free formulae in the theory of fixed width bit vector arithmetic which is a decidable fragment of first-order logic. To the best of our knowledge, this is the first attempt to generate device emulation code from a formal specification.

REFERENCES

• 1: Sorav Bansal and Alex Aiken. Binary translation using peephole superoptimizers. In ph8th USENIX Symposium on Operating System Design and Implementation (OSDI 2008), December 2008.
• 2: Paul Barham , Boris Dragovic , Keir Fraser , Steven Hand , Tim Harris , Alex Ho , Rolf Neugebauer , Ian Pratt , Andrew Warfield, Xen and the art of virtualization, ACM SIGOPS Operating Systems Review, v.37 n.5, December 2003
• 3: Clark Barrett and Cesare Tinelli. CVC3. In Werner Damm and Holger Hermanns, editors, phProceedings of the 19th International Conference on Computer Aided Verification (CAV'07), volume 4590 of phLecture Notes in Computer Science, pages 298--302. Springer-Verlag, July 2007. Berlin, Germany.
• 4: Clark Barrett, Roberto Sebastiani, Sanjit Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Armin Biere, Hans van Maaren, and Toby Walsh, editors, phHandbook of Satisfiability, volume 4, chapter 8. IOS Press, February 2009. ISBN 978-1-58603-929-5.
• 5: Fabrice Bellard, QEMU, a fast and portable dynamic translator, Proceedings of the annual conference on USENIX Annual Technical Conference, p.41-41, April 10-15, 2005, Anaheim, CA
• 6: Marco Benedetti and Hratch Mangassarian. QBF-based formal verification: Experience and perspectives. phJournal on Satisability, Boolean Modeling and Computation, 5: 133--191, 2008.
• 7: Roberto Bruttomesso , Alessandro Cimatti , Anders Franzén , Alberto Griggio , Roberto Sebastiani, The MathSAT 4 SMT Solver, Proceedings of the 20th international conference on Computer Aided Verification, July 07-14, 2008, Princeton, NJ, USA [doi>10.1007/978-3-540-70545-1_28]
• 8: Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, and Bryan Brady. Deciding bit-vector arithmetic with abstraction. In phProc. TACAS 2007, March 2007.
• 9: Cristina Cifuentes , Vishv M. Malhotra, Binary Translation: Static, Dynamic, Retargetable?, Proceedings of the 1996 International Conference on Software Maintenance, p.340-349, November 04-08, 1996
• 10: Cristina Cifuentes , Mike Van Emmerik , Norman Ramsey, The Design of a Resourceable and Retargetable Binary Translator, Proceedings of the Sixth Working Conference on Reverse Engineering, p.280, October 06-08, 1999
• 11: Bryce Howard Cogswell. Timing insensitive binary-to-binary translation. PhD thesis, Carnegie Mellon University, Pittsburgh, Pennsylvania 15213, April 1995.
• 12: Christopher L. Conway , Stephen A. Edwards, NDL: a domain-specific language for device drivers, Proceedings of the 2004 ACM SIGPLAN/SIGBED conference on Languages, compilers, and tools for embedded systems, June 11-13, 2004, Washington, DC, USA
• 13: Patrick Cousot and Radhia Cousot. Static determination of dynamic properties of programs. In phProceedings of the Second International Symposium on Programming, pages 106--130. Dunod, Paris, France, 1976.
• 14: Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4963 of Lecture Notes in Computer Science, pages 337--340. Springer, 2008.
• 15: Vijay Ganesh , David L. Dill, Decision procedures for bit-vectors, arrays and integers, Stanford University, Stanford, CA, 2007
• 16: Vijay Ganesh and David L. Dill. A decision procedure for bit-vectors and arrays. In Computer Aided Verification (CAV'07), Berlin, Germany, July 2007. Springer-Verlag.
• 17: Yeting Ge , Clark Barrett , Cesare Tinelli, Solving Quantified Verification Conditions Using Satisfiability Modulo Theories, Proceedings of the 21st international conference on Automated Deduction: Automated Deduction, July 17-20, 2007, Bremen, Germany [doi>10.1007/978-3-540-73595-3_12]
• 18: Peter S. Magnusson , Magnus Christensson , Jesper Eskilson , Daniel Forsgren , Gustav Hållberg , Johan Högberg , Fredrik Larsson , Andreas Moestedt , Bengt Werner, Simics: A Full System Simulation Platform, Computer, v.35 n.2, p.50-58, February 2002 [doi>10.1109/2.982916]
• 19: Fabrice Mérillon , Laurent Réveillère , Charles Consel , Renaud Marlet , Gilles Muller, Devil: an IDL for hardware programming, Proceedings of the 4th conference on Symposium on Operating System Design & Implementation, p.2-2, October 22-25, 2000, San Diego, California
• 20: Leonardo Moura , Nikolaj Bjørner, Efficient E-Matching for SMT Solvers, Proceedings of the 21st international conference on Automated Deduction: Automated Deduction, July 17-20, 2007, Bremen, Germany [doi>10.1007/978-3-540-73595-3_13]
• 21: Manish Prasad and Tzi-cker Chiueh. A binary rewriting defense against stack-based buffer overflow attacks. In Proceedings of the USENIX Annual Technical Conference, pages 211--224, 2003.
• 22: Alexander Schrijver, Theory of linear and integer programming, John Wiley & Sons, Inc., New York, NY, 1986
• 23: Richard L. Sites , Anton Chernoff , Matthew B. Kirk , Maurice P. Marks , Scott G. Robinson, Binary translation, Communications of the ACM, v.36 n.2, p.69-81, Feb. 1993 [doi>10.1145/151220.151227]
• 24: Jun Sun , Wanghong Yuan , Mahesh Kallahalla , Nayeem Islam, HAIL: a language for easy and correct device access, Proceedings of the 5th ACM international conference on Embedded software, September 18-22, 2005, Jersey City, NJ, USA [doi>10.1145/1086228.1086230]
• 25: Henrik Theiling. phControl Flow Graphs For Real-Time Systems Analysis. PhD thesis, Saarland University, 2002.
• 26: er(2004)}troeger_bintransJens Tröger. Specification-Driven Dynamic Binary Translation. PhD thesis, Queensland University of Technology, Brisbane, Australia, December 2004.
• 27: Reinhard Wilhelm. Determining bounds on execution times. In R. Zurawski, editor, phHandbook on Embedded Systems, pages 14--1, 14-23. CRC Press, 2005.
• 28: Lea Wittie, Chris Hawblitzel, and Derrin Pierret. Generating a statically-checkable device driver I/O interface. In phProceedings of the Workshop on Automatic Program Generation for Embedded Systems (APGES), October 2007.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Code generation

Additional Classification:
  B. Hardware
  B.4 INPUT/OUTPUT AND DATA COMMUNICATIONS
      B.4.2 Input/Output Devices
          Subjects: Channels and controllers

General Terms:
Algorithms, Theory

Keywords:
binary translation, bit vector arithmetic, code generation, device emulation, satisfiability modulo theories