Article

Free access

Parametric shape analysis via 3-valued logic

Authors:

Reinhard WilhelmAuthors Info & Claims

POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 105 - 118

https://doi.org/10.1145/292540.292552

Published: 01 January 1999 Publication History

Abstract

We present a family of abstract-interpretation algorithms that are capable of determining "shape invariants" of programs that perform destructive updating on dynamically allocated storage. The main idea is to represent the stores that can possibly arise during execution using three-valued logical structures.

Questions about properties of stores can be answered by evaluating predicate-logic formulae using Kleene's semantics of three-valued logic:

If a formula evaluates to true, then the formula holds in every store represented by the three-valued structure.

If a formula evaluates to false, then the formula does not hold in any store represented by the three-valued structure.

If a formula evaluates to unknown, then we do not know if this formula always holds, never holds, or sometimes holds and sometimes does not hold in the stores represented by the three-valued structure.

Three-valued logical structures are thus a conservative representation of memory stores.

The approach described is a parametric framework: It provides the basis for generating a family of shape-analysis algorithms by varying the vocabulary used in the three-valued logic.

References

[1]

U. Assmann and M. Weinhardt. Interprocedural heap analysis for parallelizing imperative programs. In W. K. Giloi, S. J~ihnichen, and B. D. Shriver, editors, Programming Models For Massively Parallel Computers, pages 74-82, Washington, DC, September 1993. IEEE Press.

[2]

D.R. Chase, M. Wegman, and F. Zadeck. Analysis of pointers and structures. In SIGPLAN Conf. on Prog. Lang. Design and lmpl., pages 296-310, New York, NY, 1990. ACM Press.

Digital Library

[3]

P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Syrup. on Princ. of Prog. Lang., pages 269-282, New York, NY, 1979. ACM Press.

[4]

A. Deutsch. A storeless model for aliasing and its abstractions using finite representations of right-regular equivalence relations. In IEEE International Conference on Computer Languages, pages 2-13, Washington, DC, 1992. IEEE Press.

[5]

A. Deutsch. Interprocedural may-alias analysis for pointers: Beyond k-limiting. In SIGPLAN Conf. on Prog. Lang. Design and Impl., pages 230-241, New York, NY, 1994. ACM Press.

Digital Library

[6]

L. Hendren. Parallelizing Programs with Recursive Data Structures. PhD thesis, CorneI1 Univ., Ithaca, NY, Jan 1990.

Digital Library

[7]

L. Hendren, J. Hummel, and A. Nicolau. Abstractions for recursive pointer data structures: Improving the analysis and the transformation of imperative programs. In SIGPLAN Conf. on Prog. Lang. Design and lmpl., pages 249-260, New York, NY, June 1992. ACM Press.

Digital Library

[8]

L. Hendren and A. Nicolau. Parallelizing programs with recursive data structures. IEEE Trans. on Par. and Dist. Syst., 1(1):35-47, January 1990.

Digital Library

[9]

C.A.R. Hoare. Recursive data structures. Int. d. of Comp. and Inf. Sci., 4(2):105-132, 1975.

[10]

S. Horwitz, P. Pfeiffer, and T. Reps. Dependence analysis for pointer variables. In SIGPLAN Conf. on Prog. Lang. Design and lmpl., pages 28-40, New York, NY, 1989. ACM Press.

Digital Library

[11]

N.D. Jones and S.S. Muchnick. Flow analysis and optimization of Lisp-like structures. In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 4, pages 102-131. Prentice-Hall, Englewood Cliffs, NJ, 1981.

[12]

N.D. Jones and S.S. Muchnick. A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In Syrup. on Princ. of Prog. Lang., pages 66-74, New York, NY, 1982. ACM Press.

[13]

S.C. Kleene. Introduction to Metamathematics. North- Holland, second edition, 1987.

[14]

W. Landi and B.G. Ryder. Pointer induced aliasing: A problem classification. In Syrup. on Princ. of Prog. Lang., pages 93-103, New York, NY, January 1991. ACM Press.

[15]

J.R. Larus and P.N. Hilfinger. Detecting conflicts between structure accesses. In SIGPLAN Conf. on Prog. Lang. Design and Impl., pages 21-34, New York, NY, 1988. ACM Press.

Digital Library

[16]

J. Plevyak, A.A. Chien, and V. Karamcheti. Analysis of dynamic structures for efficient parallel execution, in U. Banerjee, D. Gelernter, A. Nicolau, and D. Padua, editors, Languages and Compilers .for Parallel Computing, volume 768 of Lec. Notes in Comp. Sci., pages 37-57, Portland, OR, August 1993. Springer-Verlag.

[17]

M. Sagiv, T. Reps, and R. Wilhelm. Solving shape-analysis problems in languages with destructive updating. In Syrup. on Princ. of Prog. Lang., New York, NY, January 1996. ACM Press.

Digital Library

[18]

M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. Tech. Rep. TR-1383, Comp. Sci. Dept., Univ. of Wisconsin, Madison, WI, July 1998. Available at "http://www.cs.wisc.edu/wpis/papers/parametric.ps".

[19]

M. Sagiv, T. Reps, and R. Wilhelm. Solving shape-analysis problems in languages with destructive updating. 7~ns. on Prog. Lang. and Syst., 20(1):1-50, January 1998.

Digital Library

[20]

S. Sagiv, N. Francez, M. Rodeh, and R. Wilhelm. A logic-based approach to data flow analysis problems. Acta Inf., 35(6):457- 504, June 1998.

[21]

J. Stransky. A lattice for abstract interpretation of dynamic (Lisp-like) structures. Inf. and Comp., 101(1):70-102, Nov. 1992.

Digital Library

[22]

E. Y.-B. Wang. Analysis of Recursive Types in an Imperative Language. PhD thesis, Univ. of Calif., Berkeley, CA, 1994.

Digital Library

Cited By

Hong JRyu SFilkov VRay BZhou M(2024)To Tag, or Not to Tag: Translating C's Unions to Rust's Tagged UnionsProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3694985(40-52)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3694985
Grossman SToman JBakst AArora SSagiv MNandi C(2024)Practical Verification of Smart Contracts using Memory SplittingProceedings of the ACM on Programming Languages10.1145/36897968:OOPSLA2(2402-2433)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689796
Zanatta GFerrara PLisovenko TNegrini LCaiazza GWhite RDi Stefano L(2024)Sound Static Analysis for Microservices: Utopia? A Preliminary Experience with LiSAProceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3678721.3686229(5-10)Online publication date: 20-Sep-2024
https://dl.acm.org/doi/10.1145/3678721.3686229
Show More Cited By

Index Terms

Parametric shape analysis via 3-valued logic

Recommendations

Parametric shape analysis via 3-valued logic

Shape analysis concerns the problem of determining "shape invariants" for programs that perform destructive updating on dynamically allocated storage. This article presents a parametric framework for shape analysis that can be instantiated in different ...
Another Useful Four-Valued Logic
Knowledge Science, Engineering and Management
Abstract
We propose a four-valued logic with intuitive semantics by the connectives that is useful for understanding the contradictions in knowledge representation. The intuitive semantics reflects that any assertion has dual character by whose information ...
Three-valued Logics in Modal Logic

Every truth-functional three-valued propositional logic can be conservatively translated into the modal logic S5. We prove this claim constructively in two steps. First, we define a Translation Manual that converts any propositional formula of any three-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 1999

324 pages

ISBN:1581130953

DOI:10.1145/292540

Chairmen:
Andrew Appel
Princeton Univ., Princeton, NJ
,
Alex Aiken
Univ. of California, Berkeley

Copyright © 1999 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 January 1999

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL99

Sponsor:

POPL99: Symposium on Prinicples of Programming Languages 1999

January 20 - 22, 1999

Texas, San Antonio, USA

Acceptance Rates

POPL '99 Paper Acceptance Rate 24 of 136 submissions, 18%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

318
Total Citations
View Citations
1,165
Total Downloads

Downloads (Last 12 months)83
Downloads (Last 6 weeks)20

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Hong JRyu SFilkov VRay BZhou M(2024)To Tag, or Not to Tag: Translating C's Unions to Rust's Tagged UnionsProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3694985(40-52)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3694985
Grossman SToman JBakst AArora SSagiv MNandi C(2024)Practical Verification of Smart Contracts using Memory SplittingProceedings of the ACM on Programming Languages10.1145/36897968:OOPSLA2(2402-2433)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689796
Zanatta GFerrara PLisovenko TNegrini LCaiazza GWhite RDi Stefano L(2024)Sound Static Analysis for Microservices: Utopia? A Preliminary Experience with LiSAProceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3678721.3686229(5-10)Online publication date: 20-Sep-2024
https://dl.acm.org/doi/10.1145/3678721.3686229
Sun XGupta RZhou HMoreira JMueller FEtsion Y(2021)DSGENProceedings of the 35th ACM International Conference on Supercomputing10.1145/3447818.3460962(75-87)Online publication date: 3-Jun-2021
https://dl.acm.org/doi/10.1145/3447818.3460962
Nicole OLemerre MBardin SRival X(2021)No Crash, No Exploit: Automated Verification of Embedded Kernels2021 IEEE 27th Real-Time and Embedded Technology and Applications Symposium (RTAS)10.1109/RTAS52030.2021.00011(27-39)Online publication date: May-2021
https://doi.org/10.1109/RTAS52030.2021.00011
Sotoudeh MThakur AKell SVerna D(2020)Analogy-making as a Core primitive in the software engineering toolboxProceedings of the 2020 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3426428.3426918(101-121)Online publication date: 18-Nov-2020
https://dl.acm.org/doi/10.1145/3426428.3426918
Miltner APadhi SMillstein TWalker DDonaldson ATorlak E(2020)Data-driven inference of representation invariantsProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3385412.3385967(1-15)Online publication date: 11-Jun-2020
https://dl.acm.org/doi/10.1145/3385412.3385967
Neider DMadhusudan PSaha SGarg PPark D(2020)A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification EnginesJournal of Automated Reasoning10.1007/s10817-020-09570-zOnline publication date: 13-Jul-2020
https://doi.org/10.1007/s10817-020-09570-z
Usman MWang WWang KYelen CDini NKhurshid S(2020)A study of learning likely data structure properties using machine learning modelsInternational Journal on Software Tools for Technology Transfer10.1007/s10009-020-00577-wOnline publication date: 7-Jun-2020
https://doi.org/10.1007/s10009-020-00577-w
Mathur UMurali AKrogmeier PMadhusudan PViswanathan M(2019)Deciding memory safety for single-pass heap-manipulating programsProceedings of the ACM on Programming Languages10.1145/33711034:POPL(1-29)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371103
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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