On The Boolean Algebra of Shape Analysis Constraints
Shape analysis is a promising technique for statically verifyingand extracting properties of programs that manipulatecomplex data structures. We introduce a new characterizationof constraints that arise in parametric shapeanalysis based on manipulation of three-valued structuresas dataflow facts.We...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Language: | en_US |
| Published: |
2005
|
| Online Access: | http://hdl.handle.net/1721.1/30409 |
| _version_ | 1826195168415449088 |
|---|---|
| author | Kuncak, Viktor Rinard, Martin |
| author2 | Computer Architecture |
| author_facet | Computer Architecture Kuncak, Viktor Rinard, Martin |
| author_sort | Kuncak, Viktor |
| collection | MIT |
| description | Shape analysis is a promising technique for statically verifyingand extracting properties of programs that manipulatecomplex data structures. We introduce a new characterizationof constraints that arise in parametric shapeanalysis based on manipulation of three-valued structuresas dataflow facts.We identify an interesting syntactic class of first-orderlogic formulas that captures the meaning of three-valuedstructures under concretization. This class is broader thanpreviously introduced classes, allowing for a greater flexibilityin the formulation of shape analysis constraints inprogram annotations and internal analysis representations.Three-valued structures can be viewed as one possible normalform of the formulas in our class.Moreover, we characterize the meaning of three-valuedstructures under Âtight concretizationÂ. We show that theseemingly minor change from concretization to tight concretizationincreases the expressive power of three-valuedstructures in such a way that the resulting constraints areclosed under all boolean operations. We call the resultingconstraints boolean shape analysis constraints.The main technical contribution of this paper is a naturalsyntactic characterization of boolean shape analysis constraintsas arbitrary boolean combinations of first-order sentencesof certain form, and an algorithm for transformingsuch boolean combinations into the normal form that correspondsdirectly to three-valued structures.Our result holds in the presence of arbitrary shape analysisinstrumentation predicates. The result enables the reduction(without any approximation) of the entailment andthe equivalence of shape analysis constraints to the satisfiabilityof shape analysis constraints. When the satisfiabilityof the constraints is decidable, our result implies that theentailment and the equivalence of the constraints are alsodecidable, which enables the use of constraints in a compositionalshape analysis with a predictable behavior. |
| first_indexed | 2024-09-23T10:08:48Z |
| id | mit-1721.1/30409 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T10:08:48Z |
| publishDate | 2005 |
| record_format | dspace |
| spelling | mit-1721.1/304092019-04-12T08:26:02Z On The Boolean Algebra of Shape Analysis Constraints Kuncak, Viktor Rinard, Martin Computer Architecture Shape analysis is a promising technique for statically verifyingand extracting properties of programs that manipulatecomplex data structures. We introduce a new characterizationof constraints that arise in parametric shapeanalysis based on manipulation of three-valued structuresas dataflow facts.We identify an interesting syntactic class of first-orderlogic formulas that captures the meaning of three-valuedstructures under concretization. This class is broader thanpreviously introduced classes, allowing for a greater flexibilityin the formulation of shape analysis constraints inprogram annotations and internal analysis representations.Three-valued structures can be viewed as one possible normalform of the formulas in our class.Moreover, we characterize the meaning of three-valuedstructures under Âtight concretizationÂ. We show that theseemingly minor change from concretization to tight concretizationincreases the expressive power of three-valuedstructures in such a way that the resulting constraints areclosed under all boolean operations. We call the resultingconstraints boolean shape analysis constraints.The main technical contribution of this paper is a naturalsyntactic characterization of boolean shape analysis constraintsas arbitrary boolean combinations of first-order sentencesof certain form, and an algorithm for transformingsuch boolean combinations into the normal form that correspondsdirectly to three-valued structures.Our result holds in the presence of arbitrary shape analysisinstrumentation predicates. The result enables the reduction(without any approximation) of the entailment andthe equivalence of shape analysis constraints to the satisfiabilityof shape analysis constraints. When the satisfiabilityof the constraints is decidable, our result implies that theentailment and the equivalence of the constraints are alsodecidable, which enables the use of constraints in a compositionalshape analysis with a predictable behavior. 2005-12-19T23:09:23Z 2005-12-19T23:09:23Z 2003-08-22 MIT-CSAIL-TR-2003-012 MIT-LCS-TR-916 http://hdl.handle.net/1721.1/30409 en_US Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory 18 p. 30231553 bytes 1304355 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Kuncak, Viktor Rinard, Martin On The Boolean Algebra of Shape Analysis Constraints |
| title | On The Boolean Algebra of Shape Analysis Constraints |
| title_full | On The Boolean Algebra of Shape Analysis Constraints |
| title_fullStr | On The Boolean Algebra of Shape Analysis Constraints |
| title_full_unstemmed | On The Boolean Algebra of Shape Analysis Constraints |
| title_short | On The Boolean Algebra of Shape Analysis Constraints |
| title_sort | on the boolean algebra of shape analysis constraints |
| url | http://hdl.handle.net/1721.1/30409 |
| work_keys_str_mv | AT kuncakviktor onthebooleanalgebraofshapeanalysisconstraints AT rinardmartin onthebooleanalgebraofshapeanalysisconstraints |