Shape Analysis with Structural Invariant Checkers

Bor-Yuh Evan Chang, Xavier Rival and George Necula

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2007-80
June 4, 2007

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-80.pdf

Developer-supplied data structure specifications are important to shape analyses, as they tell the analysis what information should be tracked in order to obtain the desired shape invariants. We observe that data structure checking code (e.g., used in testing or dynamic analysis) provides shape information that can also be used in static analysis. In this paper, we propose a lightweight, automatic shape analysis based on these developer-supplied structural invariant checkers. In particular, we set up a parametric abstract domain, which is instantiated with such checker specifications to summarize memory regions using both notions of complete and partial checker evaluations. The analysis then automatically derives a strategy for canonicalizing or weakening shape invariants.


BibTeX citation:

@techreport{Chang:EECS-2007-80,
    Author = {Chang, Bor-Yuh Evan and Rival, Xavier and Necula, George},
    Title = {Shape Analysis with Structural Invariant Checkers},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2007},
    Month = {Jun},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-80.html},
    Number = {UCB/EECS-2007-80},
    Abstract = {Developer-supplied data structure specifications are important to shape analyses, as they tell the analysis what information should be tracked in order to obtain the desired shape invariants.  We observe that data structure checking code (e.g., used in testing or dynamic analysis) provides shape information that can also be used in static analysis.  In this paper, we propose a lightweight, automatic shape analysis based on these developer-supplied structural invariant checkers. In particular, we set up a parametric abstract domain, which is instantiated with such checker specifications to summarize memory regions using both notions of complete and partial checker evaluations.  The analysis then automatically derives a strategy for canonicalizing or weakening shape invariants.}
}

EndNote citation:

%0 Report
%A Chang, Bor-Yuh Evan
%A Rival, Xavier
%A Necula, George
%T Shape Analysis with Structural Invariant Checkers
%I EECS Department, University of California, Berkeley
%D 2007
%8 June 4
%@ UCB/EECS-2007-80
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-80.html
%F Chang:EECS-2007-80