# Static Analysis for ECMAScript String Manipulation Programs
## 5 Abstract Semantics of ECMAScript String Operations
### Abstract Semantics of Repeat  
The abstract semantics of repeat is defined by the function \(\mathsf{RT}^{\sharp}:\mathsf{DFA}_{/\equiv}\times\mathsf{Const}\to\mathsf{DFA}_{/\equiv}\) that, given as input an automaton \(\mathsf{A}\) and a constant integer value \(i\), returns an automaton that recognizes any string of \(\mathcal{L}(\mathsf{A})\) repeated \(i\) times. \(\mathsf{RT}^{\sharp}\) is computed by Algorithm 5 and we suppose that the abstract integer value \(i\) is positive or zero. Any non-positive value is treated as zero. The algorithm first checks some corner cases. If \(i=0\) or the input automaton only recognizes the empty string, then \(\mathsf{Min}(\varepsilon)\) is returned (lines 1-3). If the automaton has a cycle or \(i=\top_{\mathsf{Const}}\), it returns the Kleene-closure of the input automaton (lines 4-6). If none of these corner cases is detected then, for each string in \(\mathcal{L}(\mathsf{A})\), we concatenate it with itself \((i-1)\)-times using the already defined \(\mathsf{CC}^{\sharp}\). The result is the union of all the concatenated automata.  
```
Input :\(\mathsf{A}=(Q,\Sigma,\delta,q_{0},F)\), \(i\in\mathsf{Const}\) Output :\(\mathsf{RT}^{\sharp}(\mathsf{A},i)\) if\(i==0\lor\mathsf{A}==\mathsf{Min}(\{\varepsilon\})\)then return\(\mathsf{Min}(\{\varepsilon\})\);
1 end if
2 if\(\mathsf{hasCycle}(\mathsf{A})\lor i==\top_{\mathsf{Const}}\)then return\(\mathsf{Kleene}(\mathsf{A})\);
3 end if
4R\(\leftarrow\varnothing\);
5 foreach\(\mathsf{p}\in\mathsf{Paths}(\mathsf{A})\)do
6A\({}^{\prime}\leftarrow\mathsf{Min}(\mathsf{p})\);
7B\(\leftarrow\mathsf{A}^{\prime}\);
8 foreach\(k\in[1,i-1]\)do
9A\({}^{\prime}\leftarrow\mathsf{CC}^{\sharp}(\mathsf{A}^{\prime},\mathsf{B})\);
10
11 end if
12R\(\leftarrow\)R\(\cup\)A\({}^{\prime}\);
13
14 end foreach
15 returnR;
```  
**Algorithm 5**\(\mathsf{RT}^{\sharp}:\mathsf{DFA}_{/\equiv}\times\mathsf{Const}\to\mathsf{DFA}_{/ \equiv}\) algorithm  
Let us consider the automaton \(\mathsf{A}\) reported in Figure 12(a) and suppose to call \(\mathsf{RT}^{\sharp}(\mathsf{A},2)\). The resulting automaton, applying Algorithm 5, is reported in Figure 12(b). Let us suppose to call \(\mathsf{RT}^{\sharp}(\mathsf{A},\top_{\mathsf{Const}})\). In this case, since the input integer value is not determinate, Algorithm 5 returns the Kleene-star automaton of \(\mathsf{A}\) and the result is reported in Figure 12(c).  
**Theorem 9**.: \(\mathsf{RT}^{\sharp}\) _is sound but not complete. Formally,_  
\[\forall\mathsf{A}\in\mathsf{DFA}_{/\equiv},\forall i\in\mathsf{Const}. \,\mathsf{RT}(\mathcal{L}(\mathsf{A}),\gamma(i))\subsetneq\mathcal{L}( \mathsf{RT}^{\sharp}(\mathsf{A},i))\]As a counterexample to completeness, consider the automaton A s.t. \(\mathcal{L}(\texttt{A})=\{\ ab^{n}\ |\ n\in\mathbb{N}\ \}\). The completeness condition is not met, indeed  
\[\texttt{RT}(\mathcal{L}(\texttt{A}),2)=\{\ ab^{n}ab^{n}\ |\ n\in\mathbb{N}\ \}\
eq \texttt{RP}^{\sharp}(\texttt{A},2)=\{\ (ab^{n})^{m}\ |\ n,m\in\mathbb{N}\ \}\]  
since when the input automaton is cyclic, Algorithm 5 returns the Kleene closure of the input automaton.