Pluggable abstract domains for analyzing embedded software

ABSTRACT

Many abstract value domains such as intervals, bitwise, constants, and value-sets have been developed to support dataflow analysis. Different domains offer alternative tradeoffs between analysis speed and precision. Furthermore, some domains are a better match for certain kinds of code than others. This paper presents the design and implementation of cXprop, an analysis and transformation tool for C that implements "conditional X propagation," a generalization of the well-known conditional constant propagation algorithm where X is an abstract value domain supplied by the user. cXprop is interprocedural, context-insensitive, and achieves reasonable precision on pointer-rich codes. We have applied cXprop to sensor network programs running on TinyOS, in order to reduce code size through interprocedural dead code elimination, and to find limited-bitwidth global variables. Our analysis of global variables is supported by a novel concurrency model for interrupt-driven software. cXprop reduces TinyOS application code size by an average of 9.2% and predicts an average data size reduction of 8.2% through RAM compression.

REFERENCES

• 1: Phil Buonadonna, Joseph Hellerstein, Wei Hong, David Gay, and Samuel Madden. TASK: Sensor network in a box. In Proc. of the European Workshop on Wireless Sensor Networks, Istanbul, Turkey, 2005.
• 2: Caml language Web site. http://caml.inria.fr/.
• 3: Jong-Deok Choi , R. Cytron , J. Ferrante, On the Efficient Engineering of Ambitious Program Analysis, IEEE Transactions on Software Engineering, v.20 n.2, p.105-114, February 1994 [doi>10.1109/32.265631]
• 4: Michael Codish , Anne Mulkers , Maurice Bruynooghe , Maria García de la Banda , Manuel Hermenegildo, Improving abstract interpretations by combining domains, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.1, p.28-44, Jan. 1995 [doi>10.1145/200994.200998]
• 5: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 6: Crossbow Technology, Inc. http://xbow.com.
• 7: Ron Cytron , Jeanne Ferrante , Barry K. Rosen , Mark N. Wegman , F. Kenneth Zadeck, Efficiently computing static single assignment form and the control dependence graph, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.4, p.451-490, Oct. 1991 [doi>10.1145/115372.115320]
• 8: Matthew B. Dwyer , Lori A. Clarke, A flexible architecture for building data flow analyzers, Proceedings of the 18th international conference on Software engineering, p.554-564, March 25-29, 1996, Berlin, Germany
• 9: Matthew B. Dwyer , Lori A. Clarke , Jamieson M. Cobleigh , Gleb Naumovich, Flow analysis for verifying properties of concurrent software systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.13 n.4, p.359-430, October 2004 [doi>10.1145/1040291.1040292]
• 10: Chien-Liang Fok , Gruia-Catalin Roman , Chenyang Lu, Mobile agent middleware for sensor networks: an application case study, Proceedings of the 4th international symposium on Information processing in sensor networks, April 24-27, 2005, Los Angeles, California
• 11: David Gay , Philip Levis , Robert von Behren , Matt Welsh , Eric Brewer , David Culler, The nesC language: A holistic approach to networked embedded systems, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 12: Philippe Granger, Improving the Results of Static Analyses Programs by Local Decreasing Iteration, Proceedings of the 12th Conference on Foundations of Software Technology and Theoretical Computer Science, p.68-79, December 18-20, 1992
• 13: M. R. Guthaus , J. S. Ringenberg , D. Ernst , T. M. Austin , T. Mudge , R. B. Brown, MiBench: A free, commercially representative embedded benchmark suite, Proceedings of the Workload Characterization, 2001. WWC-4. 2001 IEEE International Workshop on, p.3-14, December 02-02, 2001 [doi>10.1109/WWC.2001.15]
• 14: John L. Henning, SPEC CPU2000: Measuring CPU Performance in the New Millennium, Computer, v.33 n.7, p.28-35, July 2000 [doi>10.1109/2.869367]
• 15: Ákos Lédeczi , András Nádas , Péter Völgyesi , György Balogh , Branislav Kusy , János Sallai , Gábor Pap , Sebestyén Dóra , Károly Molnár , Miklós Maróti , Gyula Simon, Countersniper system for urban warfare, ACM Transactions on Sensor Networks (TOSN), v.1 n.2, p.153-177, November 2005 [doi>10.1145/1105688.1105689]
• 16: Philip Levis, David Gay, Vlado Handziski, Jan-Hinrich Hauer, Ben Greenstein, Martin Turon, Jonathan Hui, Kevin Klues, Cory Sharp, Robert Szewczyk, Joe Polastre, Philip Buonadonna, Lama Nachman, Gilman Tolle, David Culler, and Adam Wolisz. T2: A Second Generation OS For Embedded Sensor Networks. Technical Report TKN-05-007, Telecommunication Network Group, Technische Universität Berlin, November 2005.
• 17: David Malan, Matt Welsh, and Michael Smith. A Public-Key Infrastructure for Key Distribution in TinyOS Based on Elliptic Curve Cryptography. In Proc. of the Intl. Conf. on Sensor and Ad hoc Communications and Networks (SECON), Santa Clara, CA, October 2004.
• 18: Florian Martin. PAG-An efficient program analyzer generator. International Journal on Software Tools for Technology Transfer, 2(1):46--67, 1998.
• 19: Antoine Miné, The Octagon Abstract Domain, Proceedings of the Eighth Working Conference on Reverse Engineering (WCRE'01), p.310, October 02-05, 2001
• 20: Moteiv Corporation. http://www.moteiv.com.
• 21: George C. Necula , Scott McPeak , Shree Prakash Rahul , Westley Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proceedings of the 11th International Conference on Compiler Construction, p.213-228, April 08-12, 2002
• 22: Alessandra Di Pierro , Herbert Wiklicky, Measuring the Precision of Abstract Interpretations, Selected Papers form the 10th International Workshop on Logic Based Program Synthesis and Transformation, p.147-164, July 24-28, 2000
• 23: John Regehr , Usit Duongsaa, Deriving abstract transfer functions for analyzing embedded software, Proceedings of the 2006 ACM SIGPLAN/SIGBED conference on Language, compilers and tool support for embedded systems, June 14-16, 2006, Ottawa, Ontario, Canada
• 24: Martin C. Rinard, Analysis of Multithreaded Programs, Proceedings of the 8th International Symposium on Static Analysis, p.1-19, July 16-18, 2001
• 25: Mark Stephenson , Jonathan Babb , Saman Amarasinghe, Bidwidth analysis with application to silicon compilation, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.108-120, June 18-21, 2000, Vancouver, British Columbia, Canada
• 26: Ben L. Titzer , Daniel K. Lee , Jens Palsberg, Avrora: scalable sensor network simulation with precise timing, Proceedings of the 4th international symposium on Information processing in sensor networks, April 24-27, 2005, Los Angeles, California
• 27: Bryan Turner. RandomProgramGenerator, 2005. http://www.fractalscape.org/RandomProgramGenerator.
• 28: Clark Verbrugge , Phong Co , Laurie J. Hendren, Generalized Constant Propagation: A Study in C, Proceedings of the 6th International Conference on Compiler Construction, p.74-90, April 24-26, 1996
• 29: Mark N. Wegman , F. Kenneth Zadeck, Constant propagation with conditional branches, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.2, p.181-210, April 1991 [doi>10.1145/103135.103136]
• 30: Daniel S. Wilkerson. Delta, 2003. http://delta.tigris.org/.
• 31: Andreas Zeller , Ralf Hildebrandt, Simplifying and Isolating Failure-Inducing Input, IEEE Transactions on Software Engineering, v.28 n.2, p.183-200, February 2002 [doi>10.1109/32.988498]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors

Additional Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Real-time and embedded systems

General Terms:
Languages, Performance

Keywords:
TinyOS, abstract interpretation, embedded software