Article

Free access

Symbolic bounds analysis of pointers, array indices, and accessed memory regions

Authors:

Martin RinardAuthors Info & Claims

PLDI '00: Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation

Pages 182 - 195

https://doi.org/10.1145/349299.349325

Published: 01 May 2000 Publication History

Abstract

This paper presents a novel framework for the symbolic bounds analysis of pointers, array indices, and accessed memory regions. Our framework formulates each analysis problem as a system of inequality constraints between symbolic bound polynomials. It then reduces the constraint system to a linear program. The solution to the linear program provides symbolic lower and upper bounds for the values of pointer and array index variables and for the regions of memory that each statement and procedure accesses. This approach eliminates fundamental problems associated with applying standard fixed-point approaches to symbolic analysis problems. Experimental results from our implemented compiler show that the analysis can solve several important problems, including static race detection, automatic parallelization, static detection of array bounds violations, elimination of array bounds checks, and reduction of the number of bits used to store computed values.

References

[1]

S. Amarasinghe, J. Anderson, M. Lam, and A. Lim. An overview of a compiler for scalable parallel machines. In Proceedings of the Sixth Workshop on Languages and Compilers for Parallel Computing, Portland, OR, August 1993.]]

Digital Library

[2]

C. Scott Ananian. Silicon C: A hardware backend for SUIF. Available from http://flex-compiler.lcs.mit.edu/SiliconC/ paper.pdf, May 1998.]]

[3]

W. Blume, R. Eigenmann, K. Faigin, J. Grout, J. Hoeflinger, D. Padua, P. Petersen, W. Pottenger, L. Raughwerger, P. Tu, and S. Weatherford. Effective automatic parallelization with Polaris. In International Journal of Parallel Programming, May 1995.]]

[4]

R. Blumofe, C. Joerg, B. Kuszmaul, C. Leiserson, K. Randall, and Y. Zhou. Cilk: An efficient multithreaded runtime system. Journal of Parallel and Distributed Computing, 37(1):55-69, August 1996.]]

Digital Library

[5]

R. Bodik, R. Gupta, and V. Sarkar. ABCD: Eliminating array bounds checks on demand. In Proceedings of the SIGPLAN '00 Conference on Program Language Design and Implementation, Vancouver, Canada, June 2000.]]

Digital Library

[6]

M. Budiu, S. Goldstein, M. Sakr, and K. Walker. BitValue inference: Detecting and exploiting narrow bitwidth computations. In Proceedings of the EuroPar 2000 European Conference on Parallel Computing. Munich, Germany, August 2000.]]

Digital Library

[7]

D. Chase, M. Wegman, and F. Zadek. Analysis of pointers and structures. In Proceedings of the SICPLAN '90 Conference on Program Language Design and Implementation, pages 296-310, White Plains, NY, June 1990. ACM, New York.]]

Digital Library

[8]

S. Chatterjee, A. Lebeck, P. Patnala, and M. Thottethodi. Recursive array layouts and fast matrix multiplication. In Proceedings of the 11th Annual ACM Symposium on Parallel Algorithms and Architectures, Saint Malo, France, June 1999.]]

Digital Library

[9]

G. Cheng, M. Feng, C. Leiserson, K. Randall, and A. Stark. Detecting data races in Cilk programs that use locks. In Proceedings of the lOth Annual ACM Symposium on Parallel Algorithms and Architectures, June 1998.]]

Digital Library

[10]

D. Detlefs, K. R. Leino, G. Nelson, and J. Saxe. Extended static checking. Technical Report 159, Compaq Systems Research Center, 1998.]]

[11]

A. Dinning and E. Schonberg. Detecting access anomalies in programs with critical sections. In Proceedings of the A CM//ONt Workshop on Parallel and Distributed Debugging, Santa Cruz, CA, May 1991.]]

Digital Library

[12]

C. Flanagan and S. Freund. Type-based race detection for java. In Proceedings of the SIGPLAN '00 Conference on Program Language Design and Implementation, Vancouver, Canada, June 2000.]]

Digital Library

[13]

J. Frens and D. Wise. Auto-blocking matrix-multiplication or tracking BLAS3 performance from source code. In Proceedings of the 6th A CM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Las Vegas, NV, June 1997.]]

Digital Library

[14]

M. Frigo, C. Leiserson, and K. Randall. The implementation of the Cilk-5 multithreaded language. In Proceedings of the SIG- PLAN '98 Conference on Program Language Design and Implementation, Montreal, Canada, June 1998.]]

Digital Library

[15]

M. Gupta, S. Mukhopadhyay, and N. Sinha. Automatic parallelization of recursive procedures. In Proceedings of the 1999 Conference on Parallel Algorithms and Compilation Techniques (PACT) '99, Newport Beach, CA, October 1999.]]

Digital Library

[16]

F. Gustavson. Recursion leads to automatic variable blocking for dense linear-algebra algorithms. IBM Journal of Research and Development, 41(6):737-755, November 1997.]]

Digital Library

[17]

M. W. Hall, S. Hiranandani, K. Kennedy, and C. Tseng. Interprocedural compilation of Fortran D for MIMD distributedmemory machines. In Proceedings of Supercomputing '92, Minneapolis, MN, November 1992. IEEE Computer Society Press, Los Alamitos, Calif.]]

Digital Library

[18]

P. Havlak and K. Kennedy. An implementation of interprocedural bounded regular section analysis. IEEE Transactions on Parallel and Distributed Systems, 2(3):350-360, July 1991.]]

Digital Library

[19]

P. Kolte and M. Wolfe. Elimination of redundant array subscript range checks. In Proceedings of the SIGPLAN '95 Conference on Program Language Design and Implementation, San Diego, CA, June 1995.]]

Digital Library

[20]

V. Markstein, J. Cocke, and P. Markstein. Optimization of range checking. In Proceedings of the SIGPLAN '82 Symposium on Compiler Construction, Boston, MA, June 1982.]]

Digital Library

[21]

F. Nielson, H. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 1999.]]

Digital Library

[22]

J. Patterson. Accurate static branch prediction by value range propagation. In Proceedings of the SIGPLAN '95 Conference on Program Language Design and Implementation, San Diego, CA, June 1995. ACM, New York.]]

Digital Library

[23]

M. Rinard and P. Diniz. Commutativity analysis: A new analysis technique for parallelizing compilers. ACM Transactions on Programming Languages and Systems, 19(6):941-992, November 1997.]]

Digital Library

[24]

R. Rugina and M. Rinard. Automatic parallelization of divide and conquer algorithms. In Proceedings of the 7th A CM SIG- PLAN Symposium on Principles and Practice of Parallel Programming, Atlanta, GA, May 1999.]]

Digital Library

[25]

R. Rugina and M. Rinard. Pointer analysis for multithreaded programs. In Proceedings of the SICPLAN '99 Conference on Program Language Design and Implementation, Atlanta, GA, May 1999.]]

Digital Library

[26]

M. Sagiv, T. Reps, and R. Wilhelm. Solving shape-analysis problems in languages with destructive updating. A CM Transactions on Programming Languages and Systems, 20(1):1-50, January 1998.]]

Digital Library

[27]

M. Stephenson, J. Babb, and S. Amarasinghe. Bitwidth analysis with application to silicon compilation. In Proceedings of the SIGPLAN '00 Conference on Program Language Design and Implementation, Vancouver, Canada, June 2000.]]

Digital Library

[28]

N. Sterling. Warlock: A static data race analysis tool. In Proceedings of the 1993 Winter Usenix Conference, January 1994.]]

Cited By

Swierzy BBoes FPohl TBungartz CMeier M(2024)SoK: Automated Software Testing for TLS LibrariesProceedings of the 19th International Conference on Availability, Reliability and Security10.1145/3664476.3670871(1-12)Online publication date: 30-Jul-2024
https://dl.acm.org/doi/10.1145/3664476.3670871
Küchler AWenning LWendland F(2023)AbsIntIO: Towards Showing the Absence of Integer Overflows in Binaries using Abstract InterpretationProceedings of the 2023 ACM Asia Conference on Computer and Communications Security10.1145/3579856.3582814(247-258)Online publication date: 10-Jul-2023
https://dl.acm.org/doi/10.1145/3579856.3582814
Wang YLiu JZhang DQiu XLee JPetrank E(2021)Reasoning about recursive tree traversalsProceedings of the 26th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming10.1145/3437801.3441617(47-61)Online publication date: 17-Feb-2021
https://dl.acm.org/doi/10.1145/3437801.3441617
Show More Cited By

Index Terms

Symbolic bounds analysis of pointers, array indices, and accessed memory regions
1. Computing methodologies
  1. Symbolic and algebraic manipulation
    1. Computer algebra systems
2. Hardware
  1. Hardware validation

Recommendations

Symbolic bounds analysis of pointers, array indices, and accessed memory regions

This article presents a novel framework for the symbolic bounds analysis of pointers, array indices, and accessed memory regions. Our framework formulates each analysis problem as a system of inequality constraints between symbolic bound polynomials. It ...
Symbolic bounds analysis of pointers, array indices, and accessed memory regions

This paper presents a novel framework for the symbolic bounds analysis of pointers, array indices, and accessed memory regions. Our framework formulates each analysis problem as a system of inequality constraints between symbolic bound polynomials. It ...
Symbolic range analysis of pointers
CGO '16: Proceedings of the 2016 International Symposium on Code Generation and Optimization

Alias analysis is one of the most fundamental techniques that compilers use to optimize languages with pointers. However, in spite of all the attention that this topic has received, the current state-of-the-art approaches inside compilers still face ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '00: Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation

August 2000

358 pages

ISBN:1581131992

DOI:10.1145/349299

Chairman:
Monica Lam

ACM SIGPLAN Notices Volume 35, Issue 5
May 2000
357 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/358438
Editor:
A. Michael Berman
Rowan Univ., Glassboro, NJ
Issue’s Table of Contents

Copyright © 2000 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 May 2000

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

PLDI00

Sponsor:

PLDI00: ACM SIGPLAN 2000 Conference on Programming Language and Design and Implementation

June 18 - 21, 2000

British Columbia, Vancouver, Canada

Acceptance Rates

PLDI '00 Paper Acceptance Rate 30 of 173 submissions, 17%;

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

141
Total Citations
View Citations
991
Total Downloads

Downloads (Last 12 months)106
Downloads (Last 6 weeks)25

Reflects downloads up to 24 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Swierzy BBoes FPohl TBungartz CMeier M(2024)SoK: Automated Software Testing for TLS LibrariesProceedings of the 19th International Conference on Availability, Reliability and Security10.1145/3664476.3670871(1-12)Online publication date: 30-Jul-2024
https://dl.acm.org/doi/10.1145/3664476.3670871
Küchler AWenning LWendland F(2023)AbsIntIO: Towards Showing the Absence of Integer Overflows in Binaries using Abstract InterpretationProceedings of the 2023 ACM Asia Conference on Computer and Communications Security10.1145/3579856.3582814(247-258)Online publication date: 10-Jul-2023
https://dl.acm.org/doi/10.1145/3579856.3582814
Wang YLiu JZhang DQiu XLee JPetrank E(2021)Reasoning about recursive tree traversalsProceedings of the 26th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming10.1145/3437801.3441617(47-61)Online publication date: 17-Feb-2021
https://dl.acm.org/doi/10.1145/3437801.3441617
Kim BHeo SLee GSong SKim JKim HAmaral JKulkarni M(2019)Spinal code: automatic code extraction for near-user computation in fogsProceedings of the 28th International Conference on Compiler Construction10.1145/3302516.3307356(87-98)Online publication date: 16-Feb-2019
https://dl.acm.org/doi/10.1145/3302516.3307356
Wang XYuan YZhou YCoats CHuang J(2019)Project AlmanacProceedings of the Fourteenth EuroSys Conference 201910.1145/3302424.3303983(1-16)Online publication date: 25-Mar-2019
https://dl.acm.org/doi/10.1145/3302424.3303983
Sui YFan XZhou HXue J(2018)Loop-Oriented Pointer Analysis for Automatic SIMD VectorizationACM Transactions on Embedded Computing Systems10.1145/316836417:2(1-31)Online publication date: 30-Jan-2018
https://dl.acm.org/doi/10.1145/3168364
Maalej MPaisante VMagno Quinto Pereira FGonnord L(2018)Combining range and inequality information for pointer disambiguationScience of Computer Programming10.1016/j.scico.2017.10.014152:C(161-184)Online publication date: 15-Jan-2018
https://dl.acm.org/doi/10.1016/j.scico.2017.10.014
da Silva JPereira F(2017)Demand-driven less-than analysisProceedings of the 21st Brazilian Symposium on Programming Languages10.1145/3125374.3125379(1-8)Online publication date: 21-Sep-2017
https://dl.acm.org/doi/10.1145/3125374.3125379
Blache GBaudry BCombemale BKienzle JPretschner A(2016)Handling index-out-of-bounds in safety-critical embedded C code using model-based developmentProceedings of the ACM/IEEE 19th International Conference on Model Driven Engineering Languages and Systems10.1145/2976767.2976803(143-149)Online publication date: 2-Oct-2016
https://dl.acm.org/doi/10.1145/2976767.2976803
Shaw AJalote PBriand LHoek A(2014)Program transformations to fix C buffer overflowsCompanion Proceedings of the 36th International Conference on Software Engineering10.1145/2591062.2591199(733-735)Online publication date: 31-May-2014
https://dl.acm.org/doi/10.1145/2591062.2591199
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents