# Static Analysis for ECMAScript String Manipulation Programs
## 5 Abstract Semantics of ECMAScript String Operations
### Abstract Semantics of Includes  
The abstract semantics of includes is defined by the function \(\texttt{IN}^{\sharp}:\texttt{Dfa}_{/\equiv}\times\texttt{Dfa}_{/\equiv} \rightarrow\mathbb{B}^{\sharp}\). It takes as input two automata A and A\({}^{\prime}\) and checks whether a string recognized by A\({}^{\prime}\) is a substring of a string recognized by A. The function \(\texttt{IN}^{\sharp}\) is computed by Algorithm 4, where, given a path p of an automaton A, we abuse notation denoting by \(\texttt{Min}(\texttt{p})\) the automaton that recognizes the string encoded by the path p (lines 11-12). The algorithm first checks some corner cases: if A\({}^{\prime}\) only recognizes the empty string, \(\{\texttt{true}\}\) is returned, since the empty string is always a substring of a non-empty automaton (lines 2-4), if none of the substring of A is contained in A\({}^{\prime}\), \(\{\texttt{false}\}\) is returned (lines 5-7) and if one of the input automata is cyclic, it returns \(\top_{\texttt{Bool}}\) (lines 8-10). When these corner cases are excluded, we check each string recognized by A. If the algorithm finds at least one string \(\sigma^{\prime}\) in \(\mathcal{L}(\texttt{A}^{\prime})\) that is not a substring of a string \(\sigma\) of A, \(\top_{\texttt{Bool}}\) is returned otherwise \(\{\texttt{true}\}\). This is done in lines 10-14 where, for each path p of A we create \(\texttt{Min}(\texttt{p})\) and check if its factorization with A\({}^{\prime}\) equals A\({}^{\prime}\), i.e., we check if it contains any string of A\({}^{\prime}\).  
```
Input : A = \((Q,\Sigma,\delta,q_{0},F)\), \(\mathsf{A}^{\prime}=(Q^{\prime},\Sigma,\delta^{\prime},q_{0}^{\prime},F^{ \prime})\) Output :IN\({}^{\sharp}(\mathsf{A},\mathsf{A}^{\prime})\)
1 if\(\mathsf{A}^{\prime}==\text{Min}(\{\varepsilon\})\)then
2 return\(\{\text{true}\}\);
3 end if
4 if\(\mathsf{FA}(\mathsf{A})\cap_{\text{\tiny Dra}}\mathsf{A}^{\prime}==\text{Min}( \varnothing)\)then
5 return\(\{\text{false}\}\);
6 end if
7 if\(\text{hasCycle}(\mathsf{A})\vee\text{hasCycle}(\mathsf{A}^{\prime})\)then
8 return\(\top_{\text{Bool}}\);
9 end if
10 foreach\(\mathsf{p}\in\text{Paths}(\mathsf{A})\)do
11 if\(\mathsf{A}^{\prime}\cap_{\text{\tiny Dra}}\mathsf{FA}(\text{Min}(\mathsf{p})) \
eq\mathsf{A}^{\prime}\)then
12 return\(\top_{\text{Bool}}\);
13 end if
14
15 end if
16 return\(\{\text{true}\}\);
```  
**Algorithm 4**IN\({}^{\sharp}\) : \(\text{Dra}_{/=}\times\text{Dra}_{/=}\to\mathbb{B}^{\sharp}\) algorithm  
For example, consider the automata \(\mathsf{A}\) and \(\mathsf{A}^{\prime}\) reported in Figure 11. The algorithm returns \(\top_{\text{Bool}}\) since the string \(fg\in\mathscr{L}(\mathsf{A}^{\prime})\) is not a substring of \(abc\in\mathsf{A}\). Another example is reported in Figure 12. The result of IN\({}^{\sharp}(\mathsf{A},\mathsf{A}^{\prime})\) returns \(\{\text{true}\}\) since \(\forall\sigma\in\mathscr{L}(\mathsf{A}),\forall\sigma^{\prime}\in\mathscr{L}( \mathsf{A}^{\prime})\). \(\sigma^{\prime}\) is a substring of \(\sigma\).  
**Theorem 8**.: IN\({}^{\sharp}\) _is sound but not complete. Formally,_  
\[\forall\mathsf{A},\mathsf{A}^{\prime}\in\text{Dra}_{/=}.\text{In}(\mathscr{L}( \mathsf{A}),\mathscr{L}(\mathsf{A}^{\prime}))\subsetneq\text{IN}^{\sharp}( \mathsf{A},\mathsf{A}^{\prime}).\]  
As a counterexample to completeness, consider the automaton \(\mathsf{A}\) s.t. \(\mathscr{L}(\mathsf{A})=\{\ a^{n}\ |\ n>1\ \}\) and the automaton \(\mathsf{A}^{\prime}\) s.t. \(\mathscr{L}(\mathsf{A}^{\prime})=\{a\}\). The completeness condition is not met, indeed  
\[\text{In}(\mathscr{L}(\mathsf{A}),\mathscr{L}(\mathsf{A}^{\prime}))=\{\text{ true}\}\
eq\text{IN}^{\sharp}(\mathsf{A},\mathsf{A}^{\prime})=\{\text{true},\text{false}\}\]  
since when one of the input automata is cyclic, Algorithm 4 returns \(\top_{\text{Bool}}\).