TY - GEN
T1 - Local shape analysis for overlaid data structures
AU - Drǎgoi, Cezara
AU - Enea, Constantin
AU - Sighireanu, Mihaela
PY - 2013/9/26
Y1 - 2013/9/26
N2 - We present a shape analysis for programs that manipulate overlaid data structures which share sets of objects. The abstract domain contains Separation Logic formulas that (1) combine a per-object separating conjunction with a per-field separating conjunction and (2) constrain a set of variables interpreted as sets of objects. The definition of the abstract domain operators is based on a notion of homomorphism between formulas, viewed as graphs, used recently to define optimal decision procedures for fragments of the Separation Logic. Based on a Frame Rule that supports the two versions of the separating conjunction, the analysis is able to reason in a modular manner about non-overlaid data structures and then, compose information only at a few program points, e.g., procedure returns. We have implemented this analysis in a prototype tool and applied it on several interesting case studies that manipulate overlaid and nested linked lists.
AB - We present a shape analysis for programs that manipulate overlaid data structures which share sets of objects. The abstract domain contains Separation Logic formulas that (1) combine a per-object separating conjunction with a per-field separating conjunction and (2) constrain a set of variables interpreted as sets of objects. The definition of the abstract domain operators is based on a notion of homomorphism between formulas, viewed as graphs, used recently to define optimal decision procedures for fragments of the Separation Logic. Based on a Frame Rule that supports the two versions of the separating conjunction, the analysis is able to reason in a modular manner about non-overlaid data structures and then, compose information only at a few program points, e.g., procedure returns. We have implemented this analysis in a prototype tool and applied it on several interesting case studies that manipulate overlaid and nested linked lists.
U2 - 10.1007/978-3-642-38856-9_10
DO - 10.1007/978-3-642-38856-9_10
M3 - Conference contribution
AN - SCOPUS:84884493293
SN - 9783642388552
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 150
EP - 171
BT - Static Analysis - 20th International Symposium, SAS 2013, Proceedings
T2 - 20th International Static Analysis Symposium, SAS 2013
Y2 - 20 June 2013 through 22 June 2013
ER -