Symbolic heap

We assume a fixed finite set \textsf{Vars} of program variables (ranged over by x,y,...x,y, ...) and an infinite set \textsf{Lvars} of logical variables (ranged over by x,y,...x',y',...)

Definition : A symbolic heap $\Pi| \Sigma $ consists of a finite set Π\Pi of equalities and a finite set Σ\Sigma of heap predicates. The equalities $E =F $ are between expressions EE and FF, which are variables xx, or primed variables xx', or \textrm{nil}. The elements of Σ\Sigma are of the form

E\mapsto F, \textrm{ls}(E,F), \textrm{junk}

The points-to assertion EFE\mapsto F can hold only in a singleton heap, where EE is the only active cell. Similarly, when a list segment \textrm{ls}(E,F) holds of a given heap, the path it traces out is unique, and goes through all cells in the heap.

For each symbolic heap ΠΣ\Pi| \Sigma, the Π\Pi is called pure part of ΠΣ\Pi| \Sigma, and Σ\Sigma spatial part of ΠΣ\Pi| \Sigma.

The \textrm{junk} predicate is used in the canonicalization phase to swallow up garbage.

\textsf{Values} = \textsf{Locations} \cup \{ \textsf{nil}\},

h \in \textsf{Heaps} = \textsf{Locations} \rightharpoonup_f \textsf{Values},
s \in \textsf{Stacks} = (\textsf{Vars} \cup \textsf{Lvars}) \rightarrow \textsf{Values},

\textsf{States} = \textsf{Stacks} \times \textsf{Heaps}

Static analysis

Trend one: the abstract domain uses formulae from the logic

For example, to do program analysis for linked list programs, the abstract domain uses formulae from separation logic. The partial order of abstract values is denoted by entailment of formulae. That is, if $\phi \Rightarrow \psi $ (ϕ\phi entails ψ\psi), then vϕvψv_{\phi} \sqsubseteq v_{\psi} (where vϕv_{\phi} and vψv_{\psi} are two abstract values represented by formula ϕ\phi and ψ\psi).