Systematic design of program transformation frameworks by abstract interpretation

ABSTRACT

We introduce a general uniform language-independent framework for designing online and offline source-to-source program transformations by abstract interpretation of program semantics. Iterative source-to-source program transformations are designed constructively by composition of source-to-semantics, semantics-to-transformed semantics and semantics-to-source abstractions applied to fixpoint trace semantics. The correctness of the transformations is expressed through observational and performance abstractions. The framework is illustrated on three examples: constant propagation, program specialization by online and offline partial evaluation and static program monitoring.

REFERENCES

• 1: Charles Consel , Olivier Danvy, Tutorial notes on partial evaluation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.493-501, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158707]
• 2: C.ConselandS.Khoo.On-line and off-line partial evaluation:Semantics specifications and correctness proofs.J. Func.Prog.,5(4):461 -500,1995.
• 3: P.Cousot.Constructive design of a hierarchy of semantics of atransition system by abstract interpretation.ENTCS ,6,25 p.,1997.http://www.elsevier.nl/locate/entcs/volume6. html .
• 4: 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]
• 5: P.Cousot and R.Cousot.Static determination of dynamic properties of recursive procedures.IFIP Conf.on Formal Description of Programming Concepts ,237 -277,1977, North-Holland.
• 6: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• 7: Patrick Cousot , Radhia Cousot, Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, p.269-295, August 26-28, 1992
• 8: P.Cousot and R.Cousot.A case study in abstract interpretation based program transformation:Blocking command elimination.ENTCS ,45,2001.http://www.elsevier.nl/ locate/entcs/volume45.html ,23p.
• 9: Luca de Alfaro , Zohar Manna, Temporal Verification by Diagram Transformations, Proceedings of the 8th International Conference on Computer Aided Verification, p.288-299, August 03, 1996
• 10: Úlfar Erlingsson , Fred B. Schneider, SASI enforcement of security policies: a retrospective, Proceedings of the 1999 workshop on New security paradigms, p.87-95, September 22-24, 1999, Caledon Hills, Ontario, Canada [doi>10.1145/335169.335201]
• 11: Nicolas Halbwachs , Fabienne Lagnier , Pascal Raymond, Synchronous Observers and the Verification of Reactive Systems, Proceedings of the Third International Conference on Methodology and Software Technology: Algebraic Methodology and Software Technology, p.83-96, June 21-25, 1993
• 12: Guohua Jin , Zhiyuan Li , Fujie Chen, A theoretical foundation for program transformations to reduce cache thrashing due to true data sharing, Theoretical Computer Science, v.255 n.1-2, p.449-481, March 28, 2001 [doi>10.1016/S0304-3975(99)00313-8]
• 13: Neil D. Jones, Abstraction interpretation and partial evaluation in functional and logic programming, Proceedings of the 1994 International Symposium on Logic programming, p.17-22, November 1994, Symposia, Melbourne
• 14: Neil D. Jones, An introduction to partial evaluation, ACM Computing Surveys (CSUR), v.28 n.3, p.480-503, Sept. 1996 [doi>10.1145/243439.243447]
• 15: Neil D. Jones, Combining Abstract Interpretation and Partial Evaluation (Brief Overview), Proceedings of the 4th International Symposium on Static Analysis, p.396-405, September 08-10, 1997
• 16: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 17: Neil D. Jones , Alan Mycroft, Data flow analysis of applicative programs using minimal function graphs, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.296-306, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512672]
• 18: Gary A. Kildall, A unified approach to global program optimization, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.194-206, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512945]
• 19: David Monniaux, Abstract Interpretation of Probabilistic Semantics, Proceedings of the 7th International Symposium on Static Analysis, p.322-339, June 29-July 01, 2000
• 20: R. Paige, Symbolic finite differencing, part I (invited lecture), Proceedings of the third European symposium on programming on ESOP '90, p.36-56, May 1990, Copenhagen, Denmark
• 21: R. Paige, Future directions in program transformations, ACM SIGPLAN Notices, v.32 n.1, p.94-98, Jan. 1997 [doi>10.1145/251595.251609]
• 22: A.Pnueli,O.Shtrichman,andM.Siegel.The code validation tool CVT:Automatic veri .cation of a compilation process.STTT ,2(2):192 -201,1998.
• 23: John C. Reynolds, The discoveries of continuations, Lisp and Symbolic Computation, v.6 n.3-4, p.233-248, Nov. 1993 [doi>10.1007/BF01019459]
• 24: David Sands, Proving the correctness of recursion-based automatic program transformations, Theoretical Computer Science, v.167 n.1-2, p.193-233, Oct. 30, 1996
• 25: Fred B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security (TISSEC), v.3 n.1, p.30-50, Feb. 2000 [doi>10.1145/353323.353382]
• 26: P.Steckler and M.Wand.Selective thunkification.SAS '94 , LNCS 864,162 -178.Springer,1994.
• 27: Moshe Y Vardi , Pierre Wolper, Automata-Theoretic techniques for modal logics of programs, Journal of Computer and System Sciences, v.32 n.2, p.183-221, April 1986 [doi>10.1016/0022-0000(86)90026-7]
• 28: Franck Védrine, Binding-Time Analysis and Strictness Analysis by Abstract Interpretation, Proceedings of the Second International Symposium on Static Analysis, p.400-417, September 25-27, 1995
• 29: Philip Wadler, Deforestation: transforming programs to eliminate trees, Theoretical Computer Science, v.73 n.2, p.231-248, June 22, 1990
• 30: M.Weiser.Program slicing.IEEE Trans.Software Engrg., SE-10(4):352 -357,1984.
• 31: H.Yang and Y.Sun.Reverse engineering and reusing Cobol programs:A program transformation approach.IWFM '97 , Electronic Workshops in Computing,1997.http://ewic. org.uk/ewic/workshop/view.cfm/IWFM-97.