# Static Analysis for ECMAScript String Manipulation Programs
## 4 An Abstract Domain for String Manipulation
### The Finite State Automata Abstract Domain for Strings
For instance, consider the set of languages \(L_{i}=\{\ a^{j}b^{j}\ |\ 0\leq j\leq i\ \}\subseteq\wp(\Sigma^{*})\), indexed by a constant natural \(i\in\mathbb{N}\), forming an infinite ascending chain of finite regular languages. The set of the corresponding minimal automata trivially forms an ascending chain on \(\text{Dfa}_{/=}\). This clearly implies that any computation on \(\text{Dfa}_{/=}\) may lose convergence [14] (Most of the proposed abstract domains for strings [3; 4; 5; 26] trivially satisfy ACC being finite, but they may lose precision during the abstract computation [27].). As far as automata are concerned, existing widenings are defined in terms of a state equivalence relation merging states that recognize the same language, up to a fixed length \(n\) (set as parameter for tuning the widening precision) [28; 29]. We denote this parametric widening with \(\
abla_{n}:\text{Dfa}_{/=}\times\text{Dfa}_{/=}\rightarrow\text{Dfa}_{/=}\), with \(n\in\mathbb{N}\)[28] and it is defined in the following. Let \(\text{A}=(Q,\Sigma,\delta,q_{0},F)\) and \(\text{A}^{\prime}=(Q^{\prime},\Sigma,\delta^{\prime},q^{\prime}_{0},F^{\prime})\) be two finite state automata such that \(\mathcal{L}(\text{A})\subseteq\mathcal{L}(\text{A}^{\prime})\): the widening between A and A is formalized in terms of a relation \(R\subseteq Q\times Q^{\prime}\) between the sets of states of the two automata. The relation \(R\) is used to define an equivalence relation \(\equiv_{R}\subseteq Q^{\prime}\times Q^{\prime}\) over the states of \(\text{A}^{\prime}\), such that \(\equiv_{R}=R\circ R^{-1}\). The widening between A and A is then given by the quotient automaton of A' w.r.t. the partition induced by \(\equiv_{R}:\text{A}^{\prime}\
abla_{R}\text{A}^{\prime}=\text{A}^{\prime}_{ \equiv_{R}}\) (Given \(\text{A}\in\text{Dfa}_{/=}\) and a partition \(\pi\) over its states, we denote as \(\text{A}_{\pi}=(Q^{\prime},\delta^{\prime},q^{\prime}_{0},F^{\prime},\Sigma)\) the quotient automaton [12].). Thus, the widening operator merges the states of \(\text{A}^{\prime}\) that are equivalent by the relation \(\equiv_{R}\). By changing the relation \(R\), we obtain different widening operators [28]. It has been proved that convergence is guaranteed when the relation \(R_{n}\subseteq Q\times Q^{\prime}\) is such that \((q,q^{\prime})\in R_{n}\) iff \(q\) and \(q^{\prime}\) recognize the same language of strings of length at most \(n\)[28]. The parameter \(n\) therefore tunes the length of strings determining the equivalence of states used for merging them in the widening. It is worth noting that the smaller is \(n\), the more information will be lost by widening. In the following, given \(\mathtt{A},\mathtt{A}^{\prime}\in\textsc{DFA}_{/\equiv}\) (without any constraints on the languages they recognize), we define the widening operator on \(\textsc{DFA}_{/\equiv}\) parametric on \(n\in\mathbb{N}\) as follows. \[\mathtt{A}\
abla_{n}\mathtt{A}^{\prime}\stackrel{{\text{\tiny def}}}{{= }}\mathtt{A}\
abla_{R_{n}}(\mathtt{A}\sqcup_{\textsc{DFA}}\mathtt{A}^{\prime})\]  
In order to show how the defined widening operator works, let us discuss the following example. **Example 1**. : _Consider the following \(\mu\)JS fragment_  
_str=\"\"; while (x < 100) {str=str+\"a\"; x=x+1; }_  
_The value of the variable x is unknown and so is the number of iterations of the while-loop. In these cases, in order to guarantee soundness and termination, we apply the widening operator._  
_In Figure 5a we report the abstract value of the variable str at the beginning of the second iteration of the loop, while in Figure 5b the abstract value of the variable str at the end of the second iteration. Before starting a new iteration, in the example, we apply \(\
abla_{1}\) between the two automata, specifically we merge all the states having the same outgoing character. The minimization of the so obtained automaton is reported in Figure 5c. The next iteration will reach the fix-point, guaranteeing termination._