Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

Symbolic Analysis of Imperative Programming Languages

  • Conference paper

Part of the book series:Lecture Notes in Computer Science ((LNTCS,volume 4228))

Included in the following conference series:

  • 704Accesses

Abstract

We present a generic symbolic analysis framework for imperative programming languages. Our framework is capable of computing all valid variable bindings of a program at given program points. This information is invaluable for domain-specific static program analyses such as memory leak detection, program parallelisation, and the detection of superfluous bound checks, variable aliases and task deadlocks.

We employ path expression algebra to model the control flow information of programs. A homomorphism maps path expressions into the symbolic domain. At the center of the symbolic domain is a compact algebraic structure called supercontext. A supercontext contains the complete control and data flow analysis information valid at a given program point.

Our approach to compute supercontexts is based purely on algebra and is fully automated. This novel representation of program semantics closes the gap between program analysis and computer algebra systems, which makes supercontexts an ideal intermediate representation for all domain-specific static program analyses.

Our approach is more general than existing methods because it can derive solutions for arbitrary (even intra-loop) nodes of reducible and irreducible control flow graphs. We prove the correctness of our symbolic analysis method. Our experimental results show that the problem sizes arising from real-world applications such as the SPEC95 benchmark suite are tractable for our symbolic analysis framework.

This is a preview of subscription content,log in via an institution to check access.

Access this chapter

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Aho, A.V., Sethi, R., Ullman, J.D.: Compilers—Principles, Techniques, and Tools. Addison-Wesley, Reading (1986)

    Google Scholar 

  2. Bachmann, O., Wang, P.S., Zima, E.V.: Chains of Recurrences — A Method to Expedite the Evaluation of Closed-Form Functions. In: Proc. of the Internat. Symposium on Symbolic and Algebraic Computation, pp. 242–249. ACM Press, New York (1994)

    Chapter  Google Scholar 

  3. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)

    Google Scholar 

  4. Blieberger, J.: Data-Flow Frameworks for Worst-Case Execution Time Analysis. Real-Time Systems 22, 183–227 (2002)

    Article MATH  Google Scholar 

  5. Blieberger, J.: Discrete Loops and Worst Case Performance. Computer Languages 20(3), 193–212 (1994)

    Article  Google Scholar 

  6. Blieberger, J., Burgstaller, B., Scholz, B.: Interprocedural Symbolic Evaluation of Ada Programs with Aliases. In: González Harbour, M., la de Puente, J.A. (eds.) Ada-Europe 1999. LNCS, vol. 1622, pp. 136–145. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  7. Blieberger, J., Burgstaller, B., Scholz, B.: Symbolic Data Flow Analysis for Detecting Deadlocks in Ada Tasking Programs. In: Keller, H.B., Plödereder, E. (eds.) Ada-Europe 2000. LNCS, vol. 1845, pp. 225–237. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  8. Blieberger, J., Fahringer, T., Scholz, B.: Symbolic Cache Analysis for Real-Time Systems. Real-Time Systems 18(2/3), 181–215 (2000)

    Article  Google Scholar 

  9. Burgstaller, B., Blieberger, J., Mittermayr, R.: Static Detection of Access Anomalies in Ada95. In: Pinho, L.M., González Harbour, M. (eds.) Ada-Europe 2006. LNCS, vol. 4006, pp. 40–55. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  10. Blume, W., Eigenmann, R.: Nonlinear and Symbolic Data Dependence Testing. IEEE Transactions on Parallel and Distributed Systems 9(12), 1180–1194 (1998)

    Article  Google Scholar 

  11. Burgstaller, B.: Symbolic Evaluation of Imperative Programming Languages. Technical Report 183/1-138, Department of Automation, Vienna University of Technology (June 2005),http://www.auto.tuwien.ac.at/~bburg/reports.html

  12. Burgstaller, B., Scholz, B., Blieberger, J.: Tour de Spec — A Collection of Spec95 Program Paths and Associated Costs for Symbolic Evaluation. Technical Report 183/1-137, Department of Automation, Vienna University of Technology (June 2004),http://www.auto.tuwien.ac.at/~bburg/reports.html

  13. Blieberger, J., Burgstaller, B.: Eliminating Redundant Range Checks in GNAT Using Symbolic Evaluation. In: Proc. of the Ada-Europe International Conference on Reliable Software Technologies, Toulouse, France, pp. 153–167 (June 2003)

    Google Scholar 

  14. http://www.it.usyd.edu.au/~bburg/symanalysis.html

  15. Clarke, L.A., Richardson, D.J.: Symbolic Evaluation Methods for Program Analysis. In: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications, pp. 264–300. Prentice-Hall, Englewood Cliffs (1981)

    Google Scholar 

  16. Cousot, P., Cousot, R.: Abstract Intrepretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proc. of POPL, pp. 238–252 (January 1977)

    Google Scholar 

  17. Fahringer, T., Scholz, B.: Advanced Symbolic Analysis for Compilers. In: Fahringer, T., Scholz, B. (eds.) Advanced Symbolic Analysis for Compilers. LNCS, vol. 2628. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  18. Geddes, K.O., Czapor, S.R., Labahn, G.: Algorithms for Computer Algebra. Kluwer Academic Publishers, Dordrecht (1992)

    Book MATH  Google Scholar 

  19. Gerlek, M.P., Stoltz, E., Wolfe, M.: Beyond Induction Variables: Detecting and Classifying Sequences Using a Demand-Driven SSA Form. TOPLAS 17(1), 85–122 (1995)

    Article  Google Scholar 

  20. Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.: Introducing OBJ. Draft, Oxford University Computing Laboratory, Oxford (1993)

    Google Scholar 

  21. Greene, D., Knuth, D.E.: Mathematics For the Analysis of Algorithms, 2nd edn. Birkhäuser, Basel (1982)

    Google Scholar 

  22. Haghighat, M.R., Polychronopoulos, C.D.: Symbolic Analysis for Parallelizing Compilers. TOPLAS 18(4), 477–518 (1996)

    Article  Google Scholar 

  23. Havlak, P.: Interprocedural Symbolic Analysis. Ph.D thesis, Dept. of Computer Science, Rice University (May 1994)

    Google Scholar 

  24. Hecht, M.S.: Flow Analysis of Computer Programs. Elsevier, Amsterdam (1977)

    MATH  Google Scholar 

  25. Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)

    MATH  Google Scholar 

  26. Lueker, G.S.: Some Techniques for Solving Recurrences. ACM Computing Surveys (CSUR) 12(4), 419–436 (1980)

    Article MathSciNet  Google Scholar 

  27. Menon, V., Pingali, K., Mateev, N.: Fractal Symbolic Analysis. TOPLAS 25(6), 776–813 (2003)

    Article  Google Scholar 

  28. Pugh, W.: The Omega Test: A Fast and Practical Integer Programming Algorithm for Dependence Analysis. Communications of the ACM 35(8), 102–114 (1992)

    Article  Google Scholar 

  29. Pugh, W.: Counting Solutions To Presburger Formulas: How and Why. In: Proc. of PLDI, pp. 121–134 (1994)

    Google Scholar 

  30. Pugh, W., Wonnacott, D.: Nonlinear Array Dependence Analysis. Technical report, College Park, MD, USA (1994)

    Google Scholar 

  31. Rugina, R., Rinard, M.: Symbolic Bounds Analysis of Pointers, Array Indices, and Accessed Memory Regions. In: Proc. of PLDI, pp. 182–195 (2000)

    Google Scholar 

  32. Scholz, B., Blieberger, J., Fahringer, T.: Symbolic Pointer Analysis for Detecting Memory Leaks. In: ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM 2000), Boston (January 2000)

    Google Scholar 

  33. SPEC CPU95 Benchmark Suite, Version 1.10 (August 1995)

    Google Scholar 

  34. Tarjan, R.E.: A Unified Approach to Path Problems. Journal of the ACM 28(3), 577–593 (1981)

    Article MATH MathSciNet  Google Scholar 

  35. Tu, P., Padua, D.A.: Gated SAA-Based Demand-Driven Symbolic Analysis for Parallelizing Compilers. In: International Conference on Supercomputing, pp. 414–423 (1995)

    Google Scholar 

  36. van Engelen, R.A.: The CR# Algebra and its Application in Loop Analysis and Optimization. Technical Report TR-041223, Department of Computer Science, Florida State University (December 2004)

    Google Scholar 

  37. van Engelen, R.A., Birch, J., Shou, Y., Walsh, B., Gallivan, K.A.: A Unified Framework for Nonlinear Dependence Testing and Symbolic Analysis. In: ICS 2004: Proc. of the 18th Annual International Conference on Supercomputing, pp. 106–115. ACM Press, New York (2004)

    Chapter  Google Scholar 

  38. Wolfram, S.: The Mathematica Book. Wolfram Media, Incorporated (2003)

    Google Scholar 

  39. Zima, E.V.: Simplification and Optimization Transformations of Chains of Recurrences. In: ISSAC 1995: Proc. of the 1995 International Symposium on Symbolic and Algebraic Computation, pp. 42–50. ACM Press, New York (1995)

    Chapter  Google Scholar 

  40. Zima, H., Chapman, B.: Supercompilers for Parallel and Vector Computers. ACM Press, New York (1991)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. The University of Sydney,  

    Bernd Burgstaller & Bernhard Scholz

  2. Technical University of Vienna,  

    Johann Blieberger

Authors
  1. Bernd Burgstaller

    You can also search for this author inPubMed Google Scholar

  2. Bernhard Scholz

    You can also search for this author inPubMed Google Scholar

  3. Johann Blieberger

    You can also search for this author inPubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Technology, Department of Computing, Oxford Brookes University, OX33 1HX, Oxford, UK

    David E. Lightfoot

  2. Microsoft, USA

    Clemens Szyperski

Rights and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Burgstaller, B., Scholz, B., Blieberger, J. (2006). Symbolic Analysis of Imperative Programming Languages. In: Lightfoot, D.E., Szyperski, C. (eds) Modular Programming Languages. JMLC 2006. Lecture Notes in Computer Science, vol 4228. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11860990_12

Download citation

Publish with us

[8]ページ先頭
©2009-2025 Movatter.jp