The Virtual Recency Abstraction

We start with a relational analysis that performs naive strong updates on local variables. Local variables are managed in the call frame. The concrete call frame is a mapping from local variables of a function to their assigned values ($\mathrm{𝖢𝖺𝗅𝗅𝖥𝗋𝖺𝗆𝖾}=\mathrm{𝖬𝖺𝗉}[\mathrm{𝖵𝖺𝗋},\mathrm{𝖵𝖺𝗅}]$). For the sake of a simpler presentation, we focus on languages with integer values for now ($\mathrm{𝖵𝖺𝗅}=\mathbb{Z}$), but our relational analyses for Tip and WebAssembly have to abstract over values of different types (Section 5). A relational analysis abstracts call frames with a numerical relational abstraction over local variables such as convex Polyhedra [15] or Octagons [40] (${\widehat{\mathrm{𝖢𝖺𝗅𝗅𝖥𝗋𝖺𝗆𝖾}}}_1=\mathrm{𝖱𝖾𝗅}[\mathrm{𝖵𝖺𝗋},\mathbb{Z}]$).¹¹1We use hats to distinguish abstract definitions from their same named concrete definitions without a hat. The number in the subscript after call frames distinguishes different versions of the call frame introduced throughout this section. In case of convex Polyhedra, $\mathrm{𝖱𝖾𝗅}[\mathrm{𝖵𝖺𝗋},\mathbb{Z}]$ contains linear equalities and inequalities over variables in the program ($a_1{𝚡}_1+\mathrm{\dots }{a}_n{𝚡}_n\le c$). Octagons sacrifice some precision compared to Polyhedra by limiting equalities and inequalities to two variables with unit coefficients ($\pm {𝚡}_1\pm {𝚡}_2\le c$), in order to gain an exponential performance speedup. The inner working of these abstract domains is not relevant here and we refer interested readers to the primary sources listed above.

The abstract call frame defines three key operations: variable assignment, variable lookup, and assertion checking.

Operation $\widehat{\mathrm{𝖺𝗌𝗌𝗂𝗀𝗇}}(x,v,\mathrm{𝑐𝑎𝑙𝑙𝐹𝑟𝑎𝑚𝑒})$ strongly updates variable $x$ within the relational abstract domain by overwriting its prior value. Operation $\widehat{\mathrm{𝗅𝗈𝗈𝗄𝗎𝗉}}(x,\mathrm{𝑐𝑎𝑙𝑙𝐹𝑟𝑎𝑚𝑒})$ returns a symbolic reference to variable $x$ if it is bound in $\mathrm{𝑐𝑎𝑙𝑙𝐹𝑟𝑎𝑚𝑒}$ and $\perp$ otherwise. Operation $\widehat{\mathrm{𝖺𝗌𝗌𝖾𝗋𝗍}}(\mathrm{𝑐𝑜𝑛𝑠},\mathrm{𝑐𝑎𝑙𝑙𝐹𝑟𝑎𝑚𝑒})$ asserts if $\mathrm{𝑐𝑎𝑙𝑙𝐹𝑟𝑎𝑚𝑒}$ does or does not satisfy a given constraint $\mathrm{𝑐𝑜𝑛𝑠}$. These operations are defined on numeric values abstracted with symbolic numeric expressions over local variables (${\widehat{\mathrm{𝖵𝖺𝗅}}}_1=\mathrm{𝖱𝖾𝗅𝖤𝗑𝗉𝗋}[\mathrm{𝖵𝖺𝗋}]$) and boolean values abstracted with symbolic boolean expressions (${\widehat{\mathrm{𝖡𝗈𝗈𝗅𝖵𝖺𝗅}}}_1=\mathrm{𝖱𝖾𝗅𝖢𝗈𝗇𝗌}[\mathrm{𝖵𝖺𝗋}]$). Symbolic expressions are computed by the analysis as overapproximations of program expressions. For example, the abstract interpreter evaluates program expression $\mathrm{𝚊𝚋𝚜}(𝚡)$ to symbolic expression $𝚡$ in case $x\ge 0$ and $𝚡\bigsqcup \mathrm{𝖭𝖾𝗀𝖺𝗍𝖾}(𝚡)$ otherwise.

With these call frame operations we reproduce the unsoundness problem of ${\mathrm{𝖠𝗇𝖺𝗅𝗒𝗌𝗂𝗌}}_1$ in the first example of Section 1:

The abstract stack is a list of abstract values, where operation $\mathrm{𝗉𝗎𝗌𝗁}:{\widehat{\mathrm{𝖵𝖺𝗅}}}_1\times \widehat{\mathrm{𝖲𝗍𝖺𝖼𝗄}}[{\widehat{\mathrm{𝖵𝖺𝗅}}}_1]\to \widehat{\mathrm{𝖲𝗍𝖺𝖼𝗄}}[{\widehat{\mathrm{𝖵𝖺𝗅}}}_1]$ pushes an element on top of the stack and operation $\mathrm{𝗉𝖾𝖾𝗄}:\widehat{\mathrm{𝖲𝗍𝖺𝖼𝗄}}[{\widehat{\mathrm{𝖵𝖺𝗅}}}_1]\times \mathbb{N}\to {\widehat{\mathrm{𝖵𝖺𝗅}}}_1$ retrieves the element on the stack at a given index. The assertion in the last line confirms that the top two elements on the stack are equal in the latest call frame $c_3$. This is unsound because the value of variable $𝚡$ has been overwritten line 4, so we would expect that top two elements on the stack refer to different values and are not equal. However, because both elements on the stack refer to the same symbolic expression $𝚡$, the assertion holds. The problem is that the naive strong update overwrites the value of $𝚡$, however, this also changes the value of symbolic expression $𝚡$ on the stack, which is unsound.

A sound solution would be to weakly update local variables, joining newly assigned values into prior values: $\widehat{\mathrm{𝖺𝗌𝗌𝗂𝗀𝗇}}(x,v,\mathrm{𝑐𝑎𝑙𝑙𝐹𝑟𝑎𝑚𝑒})=\mathrm{𝑐𝑎𝑙𝑙𝐹𝑟𝑎𝑚𝑒}\bigsqcup [x\mapsto v]$. With weak updates, $c_3$ in the example above would be $[𝚢\le 𝚡\le 2𝚢,y\in [0,5]]$ and the assertion would return $\top$. This is sound, but imprecise because weak updates loose many benefits that relational analyses have over non-relational, making the performance trade-off not worth it.

The previous subsection has shown that naive strong updates to local variables also changes the value of references to these variables in other analysis components, which is unsound. This problem can be solved by implementing a call frame in which references to variables remain constant throughout the analysis. This is achieved by allocating a fresh reference – i.e, an abstract address – whenever a variable assignment is analyzed. This way references to variables via addresses remain constant.

To ensure that the analysis never runs out of addresses and can always assign new values to a freshly-generated addresses, the analysis defines addresses as the variable name paired with a natural number (${\widehat{\mathrm{𝖠𝖽𝖽𝗋}}}_2=\mathrm{𝖵𝖺𝗋}\times \mathbb{N}$). These abstract addresses are added to the call frame (${\widehat{\mathrm{𝖢𝖺𝗅𝗅𝖥𝗋𝖺𝗆𝖾}}}_2=\mathrm{𝖬𝖺𝗉}[\mathrm{𝖵𝖺𝗋},𝒫({\widehat{\mathrm{𝖠𝖽𝖽𝗋}}}_2)]\times \mathrm{𝖱𝖾𝗅}[{\widehat{\mathrm{𝖠𝖽𝖽𝗋}}}_2,\mathbb{Z}]$) [51] and to abstract values (${\widehat{\mathrm{𝖵𝖺𝗅}}}_2=\mathrm{𝖱𝖾𝗅𝖤𝗑𝗉𝗋}[{\widehat{\mathrm{𝖠𝖽𝖽𝗋}}}_2]$, ${\widehat{\mathrm{𝖡𝗈𝗈𝗅𝖵𝖺𝗅}}}_2=\mathrm{𝖱𝖾𝗅𝖢𝗈𝗇𝗌}[{\widehat{\mathrm{𝖠𝖽𝖽𝗋}}}_2]$). The powerset ($𝒫({\widehat{\mathrm{𝖠𝖽𝖽𝗋}}}_2)$) ensures that call frames can be joined if different addresses have been assigned to the same variable.

The operations on the new call frame are now defined as follows:

Operation $\mathrm{𝗅𝗈𝗈𝗄𝗎𝗉}$ returns a reference to the addresses assigned to a local variable. If the call frame assigns multiple addresses to the variable, helper function $\mathrm{𝗃𝗈𝗂𝗇}:𝒫(\widehat{\mathrm{𝖵𝖺𝗅}})\times {\widehat{\mathrm{𝖢𝖺𝗅𝗅𝖥𝗋𝖺𝗆𝖾}}}_2\to \widehat{\mathrm{𝖵𝖺𝗅}}\times {\widehat{\mathrm{𝖢𝖺𝗅𝗅𝖥𝗋𝖺𝗆𝖾}}}_2$ allocates a fresh address and joins the value of the other addresses into the fresh address. Operation $\mathrm{𝖺𝗌𝗌𝗂𝗀𝗇}$ allocates a fresh address to hold the new value, which avoids overwriting values of symbolic expressions that reference the variable.

Going back to our running example with this new call frame, we now obtain a sound result: the strong update to variable $𝚡$ does not change the value of symbolic expression ${𝚡}_1$ on the stack.

Unfortunately, the allocation of fresh addresses created a termination problem: the number of addresses that the analysis allocates is unbounded and hence the analysis does not terminate.

The previous subsection has shown that assigning new values to freshly-generated addresses to keep references to addresses constant, created a termination problem. To solve this termination problem, the set of addresses must be finite and addresses must be reused on assignment. This can be done by adapting the recency abstraction [3], which traditionally has been used to handle dynamic memory allocation with a good precision-performance ratio. The recency abstraction distinguishes the most recent allocation of an object ($x_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}$) from all prior allocations ($x_{\mathrm{𝗈𝗅𝖽}}$). Whenever a new allocation is performed for the same object, $x_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}$ is first retired with all other prior allocations, to make it usable through strong updates for the newly allocated object.

Here, we use the recency abstraction to abstract the addresses from the previous subsection (${\widehat{\mathrm{𝖠𝖽𝖽𝗋}}}_2=\mathrm{𝖵𝖺𝗋}\times \mathbb{N}$) into a finite set of addresses (${\widehat{\mathrm{𝖠𝖽𝖽𝗋}}}_3=\mathrm{𝖵𝖺𝗋}\times \{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍},\mathrm{𝗈𝗅𝖽}\}$) as shown with the following abstraction function:

Thanks to the recency abstraction, we can perform strong updates on recent local variables, while soundly referring to old values.

While the lookup and assertion operations stay mostly the same for the new call frame, variable assignment changes as follows:

Operation $\widehat{\mathrm{𝖺𝗌𝗌𝗂𝗀𝗇}}(x,v,\mathrm{𝑐𝑎𝑙𝑙𝐹𝑟𝑎𝑚𝑒},\mathrm{𝑠𝑡𝑎𝑐𝑘})$ joins the prior recent value $x_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}$ into address $x_{\mathrm{𝗈𝗅𝖽}}$ and then strongly updates address $x_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}$ to the newly assigned value $v$. The retirement of address $x_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}$ into $x_{\mathrm{𝗈𝗅𝖽}}$ is performed by the relational $\mathrm{𝖿𝗈𝗅𝖽}$ operator [23]. Afterwards, operation $\widehat{\mathrm{𝑎𝑠𝑠𝑖𝑔𝑛}}$ broadcasts this retirement to all other components of the analysis: this is a crucial step, which would otherwise make the analysis unsound. In particular, all references to addresses $x_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}$ on the stack are renamed into $x_{\mathrm{𝗈𝗅𝖽}}$.

We obtain a sound result on the running example:

The key difference to before is that the assignment of variable $𝚡$ in line 4 does not overwrite the old value referenced by a symbolic expression on the stack. Instead, the call frame assigns the new value to address ${𝚡}_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}$ and refers to the old value with ${𝚡}_{\mathrm{𝗈𝗅𝖽}}$. This way the assertion in the last line confirms that the top two values on the stack are not equal, because one refers to ${𝚡}_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}$ and the other to ${𝚡}_{\mathrm{𝗈𝗅𝖽}}$.

Unfortunately, the recency abstraction causes a new modularity problem: the retirement of address ${𝚡}_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}$ into ${𝚡}_{\mathrm{𝗈𝗅𝖽}}$ needs to be broadcast and applied to all analysis components of the analysis state. This is not only slow, but also breaks the interface of analysis components, which now need to implement an address retirement operation. Furthermore, existing soundness proofs for these components become invalid and need to be reestablished for relational abstractions.

To summarize, naive strong updates are unsound for relational abstractions, because they unsoundly change value to references in other analysis components. Assigning new values to freshly-generated addresses to keep references to other addresses constant is sound, but does not terminate because the number of addresses is unbounded. The recency abstraction is a finite abstraction over the infinite set of freshly-generated addresses and enables strong updates of local variables, however, the retirement of addresses requires to replace addresses in other analysis components, which is non-modular. We solve the final modularity problem by combining the recency abstraction with the generation of fresh addresses. Specifically, we add an extra layer of indirection between the two address types, similar to virtual memory in operating systems [19]. Therefore, we call this the Virtual Recency Abstraction.

The virtual recency abstraction defines a mapping between virtual addresses ($\mathrm{𝖵𝗂𝗋𝗍𝖠𝖽𝖽𝗋}=\mathrm{𝖵𝖺𝗋}\times \mathbb{N}$, addresses from Section 2.2) and symbolic expressions. Virtual addresses are first mapped to physical addresses ($\mathrm{𝖯𝗁𝗒𝗌𝖠𝖽𝖽𝗋}=\mathrm{𝖵𝖺𝗋}\times \{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}\times \mathrm{𝗈𝗅𝖽}\}$, addresses from Section 2.3), which are then used as variables in the relational domain. We call the mapping between virtual and physical addresses the address translation ($\widehat{\mathrm{𝖠𝖽𝖽𝗋𝖳𝗋𝖺𝗇𝗌}}=\mathrm{𝖬𝖺𝗉}[\mathrm{𝖵𝗂𝗋𝗍𝖠𝖽𝖽𝗋},𝒫(\mathrm{𝖯𝗁𝗒𝗌𝖠𝖽𝖽𝗋})]$). The call frame maps variables to virtual addresses, includes the address translation from virtual to physical addresses, and defines the relational abstract domain over physical addresses:

We now define the abstract operations for the call frame of the virtual recency abstraction (Figure 1). Operation $\mathrm{𝗅𝗈𝗈𝗄𝗎𝗉}(x,\mathrm{𝑐𝑎𝑙𝑙𝐹𝑟𝑎𝑚𝑒})$ returns a fresh virtual address that refers to all physical addresses that correspond to $x$ within the address translation. Operation $\mathrm{𝖺𝗌𝗌𝗂𝗀𝗇}(x,v,\mathrm{𝑐𝑎𝑙𝑙𝐹𝑟𝑎𝑚𝑒})$ first converts the virtual addresses contained in value $v$ to physical addresses with helper function $\mathrm{𝗍𝗈𝖯𝗁𝗒𝗌𝖤𝗑𝗉𝗋}$. It then points variable $x$ to a freshly generated virtual address, assigns this virtual address to $x_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}$ in the address translation, folds $x_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}$ into $x_{\mathrm{𝗈𝗅𝖽}}$ in the relational abstract domain, and finally assigns the converted value to $x_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}$. Helper function $\mathrm{𝗍𝗈𝖯𝗁𝗒𝗌𝖤𝗑𝗉𝗋}$ replaces virtual addresses in symbolic expression with physical addresses, such that the resulting expression can be assigned to the relational abstract domain. In case virtual address $x_n$ points to multiple physical addresses $\{x_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}},x_{\mathrm{𝗈𝗅𝖽}}\}$, $\mathrm{𝗍𝗈𝖯𝗁𝗒𝗌𝖤𝗑𝗉𝗋}$ joins $x_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}$ into $x_{\mathrm{𝗈𝗅𝖽}}$ in the relational abstract domain and replaces virtual address $x_n$ with physical address $x_{\mathrm{𝗈𝗅𝖽}}$ in the symbolic expression. Similarly, operation $\mathrm{𝖺𝗌𝗌𝖾𝗋𝗍}$ first converts constraints over virtual addresses to constraints over physical addresses and afterwards decides if the resulting constraint is satisfied by the relational abstract domain.

To demonstrate that the virtual recency abstraction solves the unsoundness and modularity problem, we again reproduce the running example:

The analysis in this example is sound because the assignment in line 4 does not overwrite the prior value of virtual address ${𝚡}_1$, but moves it from physical address ${𝚡}_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}$ to ${𝚡}_{\mathrm{𝗈𝗅𝖽}}$. The new value for virtual address ${𝚡}_2$ is then written to a physical address ${𝚡}_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}$. Furthermore, the analysis is modular, because virtual address ${𝚡}_1$ is retired to ${𝚡}_{\mathrm{𝗈𝗅𝖽}}$ by adjusting the address translation, without the need to change addresses on the stack.

To summarize, the virtual recency abstraction solves all the issues of soundness, termination and modularity illustrated in the previous subsections. The next sections will provide further details on the features of our virtual recency abstraction:

Termination

The virtual recency abstraction terminates, thanks to an ordering of the call frame based on physical addresses, which is a finite set. We detail this claim in Section 3.

Soundness

The virtual recency abstraction enables sound strong updates by assigning to $\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}$ addresses and retiring references to $\mathrm{𝗈𝗅𝖽}$. We prove soundness formally in Section 4.

Modularity

The virtual recency abstraction solves the modularity problem, allowing to reuse existing analysis components as-is. For example, our relational analysis for WebAssembly reuses existing analysis components for the stack, memory, global variables, function tables, exceptions, and failures, which were originally designed for a non-relational analysis (Section 5).

In the following parts of the paper, we keep the callframe abstraction described in this subsection: $\widehat{\mathrm{𝖢𝖺𝗅𝗅𝖥𝗋𝖺𝗆𝖾}}={\widehat{\mathrm{𝖢𝖺𝗅𝗅𝖥𝗋𝖺𝗆𝖾}}}_4$.

One problem that threatens termination of the analysis is the unbounded number of virtual addresses in the call frame. To solve this problem, we define an ordering on call frames that does not compare virtual addresses directly. Instead, the ordering maps virtual addresses to physical addresses, which is a finite set.

This pre-order on call frames is not anti-symmetric ($c_1\begin{array}{c}⊑\\ ⊒\end{array}{c}_2$ does not imply $c_1=c_2$), e.g.,

The lack of anti-symmetry is crucial for the virtual recency abstraction, because normalizing call frames to a unique representation would require updating virtual addresses in analysis components, which is not modular (Section 2.3).

Another problem that threatens termination are infinite ascending chains on relational abstract domains ($\mathrm{𝖱𝖾𝗅}[\mathrm{𝖯𝗁𝗒𝗌𝖠𝖽𝖽𝗋},\mathbb{Z}]$) contained within the call frame. To this end, we define a widening operator on call frames that applies a widening operator on the contained relational abstract domain. A widening operator [12] $\nabla :L\times L\to L$ computes an upper bound of its operands $x⊑x\nabla y⊒y$ and terminates an infinite ascending chain $x_1⊑x_2⊑x_3\mathrm{\dots }$ when folded over it: $x_1⊑x_1\nabla x_2⊑(x_1\nabla x_2)\nabla x_3⊑\mathrm{\dots }$ The widening operator on call frames is defined as follows:
$({\mathrm{𝑓𝑟𝑎𝑚𝑒}}_1,{\mathrm{𝑎𝑑𝑑𝑟𝑇𝑟𝑎𝑛𝑠}}_1,{\mathrm{𝑟𝑒𝑙𝑆𝑡𝑜𝑟𝑒}}_{\mathit{1}}){\nabla }_{\widehat{\mathrm{𝖢𝖺𝗅𝗅𝖥𝗋𝖺𝗆𝖾}}}({\mathrm{𝑓𝑟𝑎𝑚𝑒}}_2,{\mathrm{𝑎𝑑𝑑𝑟𝑇𝑟𝑎𝑛𝑠}}_2,{\mathrm{𝑟𝑒𝑙𝑆𝑡𝑜𝑟𝑒}}_2)=$ $\mathrm{𝐥𝐞𝐭}\mathrm{𝑓𝑟𝑎𝑚𝑒}=[x\mapsto {\mathrm{𝑓𝑟𝑎𝑚𝑒}}_1(x)\cup {\mathrm{𝑓𝑟𝑎𝑚𝑒}}_2(x)\mid x\in {\mathrm{𝑓𝑟𝑎𝑚𝑒}}_1\vee x\in {\mathrm{𝑓𝑟𝑎𝑚𝑒}}_2]$ $\mathrm{𝑎𝑑𝑑𝑟𝑇𝑟𝑎𝑛𝑠}=[v\mapsto {\mathrm{𝑎𝑑𝑑𝑟𝑇𝑟𝑎𝑛𝑠}}_1(v)\cup {\mathrm{𝑎𝑑𝑑𝑟𝑇𝑟𝑎𝑛𝑠}}_2(v)\mid v\in {\mathrm{𝑎𝑑𝑑𝑟𝑇𝑟𝑎𝑛𝑠}}_1\vee v\in {\mathrm{𝑎𝑑𝑑𝑟𝑇𝑟𝑎𝑛𝑠}}_2]$ $\mathrm{𝑟𝑒𝑙𝑆𝑡𝑜𝑟𝑒}={\mathrm{𝑟𝑒𝑙𝑆𝑡𝑜𝑟𝑒}}_1{\nabla }_{\mathrm{𝖱𝖾𝗅}[\mathrm{𝖯𝗁𝗒𝗌𝖠𝖽𝖽𝗋},\mathbb{Z}]}{\mathrm{𝑟𝑒𝑙𝑆𝑡𝑜𝑟𝑒}}_2$ $\mathrm{𝐢𝐧}(\mathrm{𝑓𝑟𝑎𝑚𝑒},\mathrm{𝑎𝑑𝑑𝑟𝑇𝑟𝑎𝑛𝑠},\mathrm{𝑟𝑒𝑙𝑆𝑡𝑜𝑟𝑒})$

This widening operator terminates an infinite ascending chain of call frames ${\mathrm{𝑐𝑎𝑙𝑙𝐹𝑟𝑎𝑚𝑒}}_1⊑{\mathrm{𝑐𝑎𝑙𝑙𝐹𝑟𝑎𝑚𝑒}}_2\mathrm{\dots }$, because the address frame after mapping virtual addresses to physical addresses is a lattice of finite height ($\mathrm{𝖬𝖺𝗉}[\mathrm{𝖵𝖺𝗋},𝒫(\mathrm{𝖯𝗁𝗒𝗌𝖠𝖽𝖽𝗋})]$). Furthermore, the relational abstract domain terminates by its own widening operator.

Lastly, we describe a fixpoint algorithm that iterates a monotone analysis function $\widehat{f}:P\to P$ over a pre-order $(P,⊑,\perp )$ with least element $\perp$ and ensures termination with a widening operator $\nabla :P\times P\to P$. The fixpoint algorithm iterates ${(x_i)}_{i\in \mathbb{N}}$ defined by $x_1=\perp$ and $x_{n+1}=x_n\nabla \widehat{f}(x_n)$ until the ascending chain terminates after $p\in \mathbb{N}$ steps with $x_p⊑x_{p-1}$. This final iteratee $x_p$ soundly overapproximates the least fixpoint of a concrete semantics function $f:L\to L$ over lattice $(L,⪯)$:

Another problem that threatens the termination of the analysis is the unbounded number of abstract values ($\widehat{\mathrm{𝖵𝖺𝗅}}=\mathrm{𝖱𝖾𝗅𝖤𝗑𝗉𝗋}[\mathrm{𝖵𝗂𝗋𝗍𝖠𝖽𝖽𝗋}]$). To solve this problem, the ordering on abstract values does not compare symbolic expressions $v_1,v_2$ syntactically, but compares them semantically by evaluating them in the given call frames $c_1,c_2$:
$(v_1,c_1){⊑}_{\widehat{\mathrm{𝖵𝖺𝗅}}}(v_2,c_2)\text{ iff }{c}_1^{\prime }=\widehat{\mathrm{𝖺𝗌𝗌𝗂𝗀𝗇}}(\mathrm{𝑓𝑟𝑒𝑠ℎ},v_1,c_1)\wedge c_2^{\prime }=\widehat{\mathrm{𝖺𝗌𝗌𝗂𝗀𝗇}}(\mathrm{𝑓𝑟𝑒𝑠ℎ},v_2,c_2)\wedge c_1^{\prime }{⊑}_{\widehat{\mathrm{𝖢𝖺𝗅𝗅𝖥𝗋𝖺𝗆𝖾}}}{c}_2^{\prime }$

For example, expressions $\mathrm{𝖠𝖽𝖽}({𝚡}_1,{𝚢}_1)$ and $\mathrm{𝖬𝗎𝗅}({𝚡}_1,\mathrm{𝖢𝗈𝗇𝗌𝗍}(2))$ are indistinguishable by the value ordering in call frame $(\mathrm{\dots },[{𝚡}_1\mapsto \{{𝚡}_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}\},{𝚢}_1\mapsto \{{𝚢}_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}\}],[1\le {𝚡}_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}={𝚢}_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}\le 10])$.

The widening operator on abstract values takes two values and two call frames as input.

The full definition of the operator is given in Definition 2 in the supplementary material. In this section, we discuss the operator at a high-level. Depending on the expressions contained in the abstract values, the operator implements different widening strategies:

• $\mathrm{■}$

  In case the expressions are both constant, i.e. contain no variables, each expression is evaluated in the respective call frame and the resulting intervals are widened.

• $\mathrm{■}$

  In case the expressions are structurally equal, i.e. differ only in the recency of their addresses, the widening operator attempts a structural join. This happens often when the fixpoint algorithm widens two analysis states and handling this case avoids adding addresses to the relational abstract domain to hold the join of expressions. For example, the analysis of loop for(int i = 0; ...; i++) requires to widen two expressions for the incrementation of the index variable $𝚒$: $\mathrm{𝙰𝚍𝚍}({𝚒}_{n-1},\mathrm{𝖢𝗈𝗇𝗌𝗍}(1))$ where ${𝚒}_{n-1}$ is old and $\mathrm{𝙰𝚍𝚍}({𝚒}_n,\mathrm{𝖢𝗈𝗇𝗌𝗍}(1))$ where ${𝚒}_n$ is recent. The widening operator will join these two expressions into $\mathrm{𝙰𝚍𝚍}({𝚒}_{n+1},\mathrm{𝖢𝗈𝗇𝗌𝗍}(1))$, where ${𝚒}_{n+1}$ mapped to $\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}$ and $\mathrm{𝗈𝗅𝖽}$ by the address translation.

• $\mathrm{■}$

  In all other cases the operator assigns expressions $v_1,v_2$ to a join address ${\mathrm{𝑐𝑡𝑥}}_k$ in the respective call frame.

  	$(v_1,({\mathrm{𝑓𝑟𝑎𝑚𝑒}}_1,{\mathrm{𝑎𝑑𝑑𝑟𝑇𝑟𝑎𝑛𝑠}}_1,{\mathrm{𝑟𝑒𝑙𝑆𝑡𝑜𝑟𝑒}}_1)){\nabla }_{\widehat{\mathrm{𝖵𝖺𝗅}}}(v_2,({\mathrm{𝑓𝑟𝑎𝑚𝑒}}_2,{\mathrm{𝑎𝑑𝑑𝑟𝑇𝑟𝑎𝑛𝑠}}_2,{\mathrm{𝑟𝑒𝑙𝑆𝑡𝑜𝑟𝑒}}_2))=$

  The context of join address ${\mathrm{𝑐𝑡𝑥}}_n$ is decided by function $\mathrm{𝖺𝗅𝗅𝗈𝖼}$, which is an additional parameter of the widening operator. Depending on where operator ${\nabla }_{\widehat{\mathrm{𝖵𝖺𝗅}}}$ is called, different contexts may be allocated. For example, when two stack entries are widened, the allocator might return a context $\mathrm{𝖲𝗍𝖺𝖼𝗄}(\mathrm{𝑝𝑜𝑠𝑖𝑡𝑖𝑜𝑛},\mathrm{𝑖𝑛𝑠𝑡𝑟𝑢𝑐𝑡𝑖𝑜𝑛},\mathrm{𝑓𝑢𝑛𝑐𝑡𝑖𝑜𝑛})$ to indicate the position on the stack, the current instruction, and function where the widening occurred.

Finally, we describe a widening operator ${\nabla }_{\widehat{\mathrm{𝖲𝗍𝖺𝗍𝖾}}}$ on compound analysis states, whose type $\widehat{\mathrm{𝖲𝗍𝖺𝗍𝖾}}$ we do not specify for generality. Since two compound analysis states $S,S^{\prime }$ with respective call frames $c_1,c_1^{\prime }$ contain many values $v_1\mathrm{\dots }{v}_n$ and $v_1^{\prime }\mathrm{\dots }{v}_n^{\prime }$ that need to be widened pair-wise, we fold operator ${\nabla }_{\widehat{\mathrm{𝖵𝖺𝗅}}}$ over all values $(v_i,c_i){\nabla }_{\widehat{\mathrm{𝖵𝖺𝗅}}}(v_1^{\prime },c_i^{\prime })=(v_i^{\prime \prime },c_{i+1},c_{i+1}^{\prime })$ where $1\le i\le n$ and finally apply the widening operator on the two resulting call frames $c_n{\nabla }_{\widehat{\mathrm{𝖢𝖺𝗅𝗅𝖥𝗋𝖺𝗆𝖾}}}{c}_n^{\prime }$. This terminates infinite ascending chains of compound analysis states because abstract values are compared by evaluating them in respective call frames, which themselves are widened during every step.

In this subsection, we describe how the virtual recency abstraction terminates the analysis of recursive functions. To ensure termination of the analysis, we use an existing fixpoint algorithm [34], which we illustrate at the example of the recrusive sum function:

The graph to the top-right shows a trace of the analysis, where $(\mathrm{𝚜𝚞𝚖}\mathrm{@}\mathrm{𝑐𝑡𝑥},c)\Downarrow c^{\prime }$ can be read as function $\mathrm{𝚜𝚞𝚖}$ in calling context $\mathrm{𝑐𝑡𝑥}$ under input call frame $c$ evaluates to output call frame $c^{\prime }$. We use short-hand notation for the frame and address translation, e.g., $[{𝚡}_{1,2}\mapsto {𝚡}_{\mathrm{𝗈𝗅𝖽}}]$ stands for $[{𝚡}_1\mapsto \{{𝚡}_{\mathrm{𝗈𝗅𝖽}}\},{𝚡}_2\mapsto \{{𝚡}_{\mathrm{𝗈𝗅𝖽}}\}]$. The fixpoint algorithm first recursively analyzes function sum, widening consecutive input call frames after the function parameters have been assigned, until they do not grow any further at $c_4⊑c_3$. The algorithm then iterates between the recurrent recursive calls $\mathrm{𝚜𝚞𝚖}\mathrm{@}[7,7,7,3]$ and $\mathrm{𝚜𝚞𝚖}\mathrm{@}[7,7,3]$ until the widened output call frames $c_5,c_5\nabla c_6,(c_5\nabla c_6)\nabla c_7\mathrm{\dots }$ do not grow anymore. Once the iteration is finished, the algorithm returns to the top-most call with final result:

The inequalities ${𝚊}_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}\ge {𝚡}_{\mathrm{𝗈𝗅𝖽}}\ge {𝚡}_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}\ge 0$ show that parameter $𝚡$ decreases from $𝚊$ down to $0$. Furthermore, ${𝚢}_{\mathrm{𝗋𝖾𝖼𝖾𝗇𝗍}}={𝚡}_{\mathrm{𝗈𝗅𝖽}}+{𝚢}_{\mathrm{𝗈𝗅𝖽}}\ge {𝚡}_{\mathrm{𝗈𝗅𝖽}}$ show that the last result is the sum of any $𝚡$ with any result $𝚢$, which is greater than any input ${𝚡}_{\mathrm{𝗈𝗅𝖽}}$.

Typically, soundness would be proven with respect to Galois connections [12]. However, some relational abstract domains, such as polyhedra, do not enjoy Galois connections [41, Paragraph “Absence of Galois Connection”]. The problem is that the abstraction function $\alpha$, that computes the best possible approximation of a concrete property in the abstract domain, may not exist. Instead, we prove soundness with respect to monotone concretization functions $\gamma$ from abstract domain to concrete domain, which is also used in mechanized soundness proofs [31]. The full definitions of the concretization functions can be found in Definitions 3-5 in the supplementary material. Here we discuss the concretizations at a high-level by example.

The concretization function for abstract call frames is the composition of two functions:

This two-step-concretization is needed because the concretization for values evaluates them in ${\mathrm{𝖢𝖺𝗅𝗅𝖥𝗋𝖺𝗆𝖾}}^{\prime }$. Concretization ${\gamma }_{\widehat{\mathrm{𝖢𝖺𝗅𝗅𝖥𝗋𝖺𝗆𝖾}}}$ expands the codomain of the relational abstraction to virtual addresses and then concretizes it. This is necessary to assign virtual addresses on the same physical address their own individual values. Concretization ${\gamma }_{{\mathrm{𝖢𝖺𝗅𝗅𝖥𝗋𝖺𝗆𝖾}}^{\prime }}$ maps to the result of the first to regular concrete call frames. To illustrate the concretization on call frames, consider the following example:

The concretization function for abstract values ($\widehat{\mathrm{𝖵𝖺𝗅}}=\mathrm{𝖱𝖾𝗅𝖤𝗑𝗉𝗋}[\mathrm{𝖵𝗂𝗋𝗍𝖠𝖽𝖽𝗋}]$) evaluates symbolic expressions in a given ${\mathrm{𝖢𝖺𝗅𝗅𝖥𝗋𝖺𝗆𝖾}}^{\prime }$:

Symbolic expressions are not evaluated in $\widehat{\mathrm{𝖢𝖺𝗅𝗅𝖥𝗋𝖺𝗆𝖾}}$ because this would loose the relations between variables, which makes the soundness proof meaningless [43]. To illustrate the concretization of abstract values, consider the interpretation of $(x_3-x_1)\ast [1,3]$ in a call frame $c^{\prime }\in {\gamma }_{\widehat{\mathrm{𝖢𝖺𝗅𝗅𝖥𝗋𝖺𝗆𝖾}}}(c)$:
$c^{\prime }=(\mathrm{\dots },[{𝚡}_1\mapsto 1,{𝚡}_2\mapsto 1,{𝚡}_3\mapsto 2])$ ${\gamma }_{\widehat{\mathrm{𝖵𝖺𝗅}}}(c^{\prime })(\mathrm{𝖬𝗎𝗅}(\mathrm{𝖲𝗎𝖻}({𝚡}_3,{𝚡}_1),\mathrm{𝖢𝗈𝗇𝗌𝗍}([1,3])))=\{(2-1)\ast 1,(2-1)\ast 2,(2-1)\ast 3\}=\{1,2,3\}$

Next, we describe the concretization of analysis components. To stay as generic as possible, we do not require any structure of analysis components. The only requirement is that analysis must be parametric in the type of values ($\widehat{\mathrm{𝖢𝗈𝗆𝗉𝗈𝗇𝖾𝗇𝗍}}[\widehat{\mathrm{𝖵𝖺𝗅}}]$), such that they can be reused in a relational analysis. Because components are parametric in the type of values, their concretization function is also parameterized by a concretization function for values:

As an example, consider the concretization function for a stack analysis component:

To use the concretization function for stacks, we apply it to the concretization function for abstract values:

Finally, we describe the concretization function on compound analysis states. The analysis state consists of multiple components together with the call frame of the virtual recency abstraction:

The concretization function ${\gamma }_{\widehat{\mathrm{𝖲𝗍𝖺𝗍𝖾}}}:\widehat{\mathrm{𝖲𝗍𝖺𝗍𝖾}}\to 𝒫(\mathrm{𝖲𝗍𝖺𝗍𝖾})$ partially applies a concretized call frame $c^{\prime }\in {\gamma }_{\widehat{\mathrm{𝖢𝖺𝗅𝗅𝖥𝗋𝖺𝗆𝖾}}}(\widehat{c})$ to the concretization function for values to obtain a concretization functions on components: ${\gamma }_{{\widehat{\mathrm{𝖢𝗈𝗆𝗉𝗈𝗇𝖾𝗇𝗍}}}_i}[\widehat{\mathrm{𝖵𝖺𝗅}}]({\gamma }_{\widehat{\mathrm{𝖵𝖺𝗅}}}({\mathrm{𝑐𝑎𝑙𝑙𝐹𝑟𝑎𝑚𝑒}}^{\prime })):{\widehat{\mathrm{𝖢𝗈𝗆𝗉𝗈𝗇𝖾𝗇𝗍}}}_i[\widehat{\mathrm{𝖵𝖺𝗅}}]\to 𝒫({\mathrm{𝖢𝗈𝗆𝗉𝗈𝗇𝖾𝗇𝗍}}_i)$.