In this paper we study constraints for specifying properties of data structures consisting of linked objects allocated in the heap. Motivated by heap summary graphs in role analysis and shape analysis we introduce the notion ofregular graph constraints. A regular graph constraint is a graph representing the heap summary; a heap satisfies a constraint if and only if the heap can be homomorphically mapped to the summary. Regular graph constraints form a very simple and natural fragment of the existential monadic second-order logic over graphs. One of the key problems in a compositional static analysis is proving that procedure preconditions are satisfied at every call site. For role analysis, precondition checking requires determining the validity of implication, i.e.,entailmentof regular graph constraints. The central result of this paper is the undecidability of regular graph constraint entailment. Theundecidabilityof theentailmentproblem is surprising because of the simplicity of regular graph constraints: in particular, thesatisfiabilityof regular graph constraints isdecidable. Our undecidability result implies that there is no complete algorithm for statically checking procedure preconditions or postconditions, simplifying static analysis results, or checking that given analysis results are correct. While incomplete conservative algorithms for regular graph constraint entailment checking are possible, we argue that heap specification languages should avoid second-order existential quantification in favor of explicitly specifying a criterion for summarizing objects.

@inproceedings{KuncakRinard03ExistentialHeapAbstractionEntailment, author = {Viktor Kuncak and Martin Rinard}, title = {Existential Heap Abstraction Entailment is Undecidable}, booktitle = {10th Annual International Static Analysis Symposium}, year = 2003, address = {San Diego, California}, month = {June}, series = {LNCS}, volume = {2694}, abstract = { In this paper we study constraints for specifying properties of data structures consisting of linked objects allocated in the heap. Motivated by heap summary graphs in role analysis and shape analysis we introduce the notion of \emph{regular graph constraints}. A regular graph constraint is a graph representing the heap summary; a heap satisfies a constraint if and only if the heap can be homomorphically mapped to the summary. Regular graph constraints form a very simple and natural fragment of the existential monadic second-order logic over graphs. One of the key problems in a compositional static analysis is proving that procedure preconditions are satisfied at every call site. For role analysis, precondition checking requires determining the validity of implication, i.e., \emph{entailment} of regular graph constraints. The central result of this paper is the undecidability of regular graph constraint entailment. The \emph{undecidability} of the \emph{entailment} problem is surprising because of the simplicity of regular graph constraints: in particular, the \emph{satisfiability} of regular graph constraints is \emph{decidable}. Our undecidability result implies that there is no complete algorithm for statically checking procedure preconditions or postconditions, simplifying static analysis results, or checking that given analysis results are correct. While incomplete conservative algorithms for regular graph constraint entailment checking are possible, we argue that heap specification languages should avoid second-order existential quantification in favor of explicitly specifying a criterion for summarizing objects. } }