# Static Analysis for ECMAScript String Manipulation Programs
## 5 Abstract Semantics of ECMAScript String Operations  
In this section, we define the abstract semantics of the language \(\mu\)JS over the abstract domain \(\mathbb{V}^{\sharp}\). In particular, we have to define the expressions abstract semantics \([\![\cdot]\!]^{\sharp}:\text{Exp}\times\text{States}\rightarrow\mathbb{V}^{\sharp}\), abstracting the collecting semantics (The string collecting semantics (fully reported in Appendix A) is defined lifting to \(\wp(\mathbb{V})\) the concrete one reported in Section 3. For example, the collecting semantics of substring is, abusing notation, \(\text{Ss}:\wp(\Sigma^{*})\times\wp(\mathbb{Z})\times\wp(\mathbb{Z}) \rightarrow\wp(\Sigma^{*})\) defined as  
Figure 6: Coalesced sum abstract domain for \(\mu\)JS.  
\(\operatorname{SS}(L,I,J)=\{\;\operatorname{SS}(\sigma,i,j)\;|\;\sigma,\in L,i\in I,j \in J\;\}\).), which is standard except for the string operations that will be explicitly provided by describing the algorithms for computing them. Let us first recall some important notions on regular languages, useful for the algorithms we will provide.  
**Definition 2** (Suffixes and prefixes [12]).: _Let \(L\in\wp(\Sigma^{*})\) be a regular language. The suffixes of \(L\) are \(\operatorname{SU}(L)\stackrel{{\text{\tiny{\sf def}}}}{{=}}\{\;y \in\Sigma^{*}\;|\;\exists x\in\Sigma^{*}.\;x\cdot y\in L\;\}\), and the prefixes of \(L\) are \(\operatorname{Pr}(L)\stackrel{{\text{\tiny{\sf def}}}}{{=}}\{\;x \in\Sigma^{*}\;|\;\exists y\in\Sigma^{*}.\;xy\in L\;\}\)._  
We can define the suffixes from a position, namely given \(i\in\mathbb{N}\), the set of suffixes from \(i\) is \(\operatorname{SU}(L,i)\stackrel{{\text{\tiny{\sf def}}}}{{=}}\{\;y \in\Sigma^{*}\;|\;\exists x\in\Sigma^{*}.\;x\cdot y\in L,|x|=i\;\}\). For instance, let \(L=\{abc,hello\}\), then \(\operatorname{SU}(L,2)=\{c,llo\}\).  
**Definition 3** (Right quotient [12]).: _Let \(L_{1},L_{2}\in\Sigma^{*}\) be regular languages. The right quotient of \(L_{1}\) w.r.t \(L_{2}\) is \(\operatorname{RQ}(L_{1},L_{2})\stackrel{{\text{\tiny{\sf def}}}}{{= }}\{\;x\in\Sigma^{*}\;|\;\exists y\in L_{2}.\;x\cdot y\in L_{1}\;\}\)._  
For example, let \(L_{3}=\{xab,yab\}\) and \(L_{4}=\{b,ab\}\). The right quotient of \(L_{3}\) w.r.t \(L_{4}\) is \(\operatorname{RQ}(L_{3},L_{4})=\{xa,ya,x,y\}\).  
**Definition 4** (Substrings/Factors [34]).: _Let \(L\in\wp(\Sigma^{*})\) be a regular language. The set of its substrings/factors is \(\operatorname{FA}(L)\stackrel{{\text{\tiny{\sf def}}}}{{=}}\{\;y \in\Sigma^{*}\;|\;\exists x,z\in\Sigma^{*}.\;x\cdot y\cdot z\in L\;\}\)._  
These operations are all defined as transformations of regular languages. In [12], the corresponding algorithms on \(\operatorname{FA}\) are provided. In particular, let \(A,A_{1}\in\operatorname{DFA}/_{\equiv}\) and \(i\in\mathbb{N}\), then \(\operatorname{SU}(A)\), \(\operatorname{PR}(A)\), \(\operatorname{SU}(A,i)\), \(\operatorname{FA}(A)\) and \(\operatorname{RQ}(A,A_{1})\) are the algorithms corresponding to the transformations \(\operatorname{SU}(L(A))\), \(\operatorname{Pr}(L(A))\), \(\operatorname{SU}(\mathcal{L}(A),i)\), \(\operatorname{FA}(\mathcal{L}(A))\) and \(\operatorname{RQ}(\mathcal{L}(A),\mathcal{L}(A_{1}))\), respectively. Namely, \(\forall A,A_{1}\in\operatorname{DFA}/_{\equiv},i\in\mathbb{N}\), the following facts holds:  
\[\begin{array}{l}\operatorname{SU}(\mathcal{L}(A))=\mathcal{L}(\operatorname {SU}(A))\quad\operatorname{Pr}(\mathcal{L}(A))=\mathcal{L}(\operatorname{PR}( A))\quad\operatorname{FA}(\mathcal{L}(A))=\mathcal{L}(\operatorname{FA}(A))\\ \operatorname{RQ}(\mathcal{L}(A),\mathcal{L}(A_{1}))=\mathcal{L}(\operatorname {RQ}(A,A_{1}))\quad\operatorname{SU}(\mathcal{L}(A),i)=\mathcal{L}( \operatorname{SU}(A,i))\end{array}\]