# Static Analysis for ECMAScript String Manipulation Programs
## 5 Abstract Semantics of ECMAScript String Operations
### Abstract Semantics of Substring  
In this section we define the abstract semantics of substring. In particular, we define the operator \(\operatorname{SS}^{\sharp}:\operatorname{DFA}/_{\equiv}\times\operatorname{ Const}\times\operatorname{Const}\to\operatorname{DFA}/_{\equiv}\), that takes as input an automaton and two constant integer indexes \(i,j\in\operatorname{Const}\), and computes the automaton recognizing the set of all substrings of the input automata language between the two provided integer indexes. Since the abstract semantics has to take into account the swaps when the initial index is greater than the final one, several cases arise when one of the two integer parameters is unknown, namely when it is equal to \(\top_{\mathsf{Const}}\). Indeed, the abstract semantics \(\operatorname{SS}^{\sharp}\) is divided in four cases that are reported in Table 1. Consider \(A\in\operatorname{DFA}/_{\equiv},i,j\in\operatorname{Const}\) (for the sake of readability we denote by \(\sqcup\) the automata lub \(\sqcup_{\operatorname{DFA}}\), and by \(\sqcap\) the glb \(\sqcap_{\operatorname{DFA}}\)). As in the concrete semantics of substring, negative integer values are treated as zero. 1. If \(i,j\in\mathbb{Z}\) (second row, second column of Table 1) we have to compute the language of all the substrings between the initial index \(i\) and a final index in \(j\), i.e., \(\operatorname{SS}(\mathcal{L}(A),i,j)\). For example, let \(L=\{a\}^{*}\cup\{hello,bc\}\), the set of its substrings from \(1\) to \(3\) is \(\operatorname{SS}(L,1,3)=\{e,a,aa,el,c\}\). When \(i<j\), as in the example, the automaton accepting this language is computed by the operator \[\operatorname{SS}(A,i,j)\stackrel{{\text{\tiny{\sf def}}}}{{=}}( \operatorname{RQ}(\operatorname{SU}(A,i),\operatorname{SU}(A,j))\sqcap\operatorname{ Min}(\Sigma^{j-i}))\sqcup(\operatorname{SU}(A,i)\sqcap\operatorname{Min}(\Sigma^{<j-i}))\] If \(j>i\), the integer arguments are simply swapped, as in the Table 1.
2. When both integer parameters correspond to \(\top_{\mathsf{Const}}\), the result is the automaton of all possible factors of \(A\) (third row, third column), i.e., \(\operatorname{FA}(A)\). When \(i\) is defined and \(j=\top_{\mathsf{Const}}\) (second row, third column), we have to compute the automaton recognizing all the substrings of \(\mathcal{L}(\mathsf{A})\) from \(0\) to \(i\) and any substring starting from \(i\). For example, let us consider \(\mathsf{SS}^{\sharp}(\mathsf{Min}(\{\mathit{l}elloworld\}),5,\top_{\mathsf{Const}})\). Due to the semantics of substring reported in Section 3, we need to compute the substring from \(a\in[0,5]\) to \(5\) and then any substring with initial index equal to \(5\). The automata recognizing any substring starting at a specific index \(l\) is defined as \(\mathsf{SS}^{\sharp}(\mathsf{A},l)\stackrel{{\text{\tiny def}}}{{ =}}\mathsf{FA}(\mathsf{SU}(\mathsf{A},l))\). The abstract semantics returns the least upper bound of all the automata of substrings from \(a\) in \([0,i]\) to the automata recognizing any substring with initial index equals to \(i\). 4. Similarly to the previous case, when \(j\) is defined and \(i=\top_{\mathsf{Const}}\) (third row, second column), we have to compute the automaton recognizing all the substring of \(\mathcal{L}(\mathsf{A})\) from \(0\) to \(j\) and any substring starting from \(j\). Let us consider \(\mathsf{SS}^{\sharp}(\mathsf{Min}(\{\mathit{l}elloworld\}),\top_{\mathsf{Const} },5)\). Similarly to the previous case, we compute the substrings from \(a\in[0,5]\) to \(5\) and then any substring with initial index equal to \(5\). The abstract semantics therefore returns the least upper bound of all the automata of substrings from \(a\) in \([0,j]\) to the automata recognizing any substring with initial index equal to \(j\). In Figure 7 we report an example obtained applying the rules in the table. **Theorem 2**. : \(\mathsf{SS}^{\sharp}\) _is sound and complete.