Componential set-based analysis

Set-based analysis (SBA) produces good predictions about the behavior of fu nctional and object-oriented programs. The analysis proceeds by inferring c onstraints that characterize the data flow relationships of the analyzed pr ogram. Experiences with MrSpidey, a static debugger based on SEA, indicate that SEA can adequately deal with programs of up to a couple of thousand li nes of code. SEA fails. however, to cope with larger programs because it ge nerates systems of constraints that are at least linear, and possibly quadr atic, in the size of the analyzed program. This article presents theoretica l and practical results concerning methods for reducing the size of constra int systems. The theoretical results include a proof-theoretic characteriza tion of the observable behavior of constraint systems for program component s, and a complete algorithm for deciding the observable equivalence of cons traint systems. In the course of this development we establish a close conn ection between the observable equivalence of constraint systems and the equ ivalence of regular-tree grammars. We then exploit this connection to adapt a variety of algorithms for simplifying grammars to the problem of simplif ying constraint systems. Based on the resulting algorithms, we have develop ed componential set-based analysis, a modular and polymorphic variant of SE A. Experimental results verify the effectiveness of the simplification algo rithms and the componential analysis. The simplified constraint systems are typically an order of magnitude smaller than the original systems. These r eductions in size produce significant gains in the speed of the analysis.