# Static Analysis for ECMAScript String Manipulation Programs
## 4 An Abstract Domain for String Manipulation  
### The Finite State Automata Abstract Domain for Strings  
In this section, we describe the finite state automata abstract domain for strings [19; 20; 21], namely the domain of regular languages over \(\wp(\Sigma^{*})\). In particular our goal is to exploit automata, and therefore regular languages, for approximating string values collected during analysis. The idea is to approximate strings as regular languages represented by the minimum DFA [12] recognizing them. In general, we have more DFA than regular languages, hence the domain of automata is indeed the quotient \(\textsc{DFA}_{/=}\) w.r.t. the equivalence relation induced by language equality: \(\forall\mathtt{A}_{1},\mathtt{A}_{2}\in\textsc{DFA}_{/=}.\mathtt{A}_{1} \equiv\mathtt{A}_{2}\Leftrightarrow\mathscr{L}(\mathtt{A}_{1})=\mathscr{L}( \mathtt{A}_{2})\). Therefore any equivalence class is composed by automata that recognize the same regular language. We abuse notation by representing these classes in the domain \(\textsc{DFA}_{/=}\) w.r.t. \(\equiv\) using one of its automata (usually the minimum), i.e., when we write \(\mathtt{A}\in\textsc{DFA}_{/=}\) we mean \([\mathtt{A}]_{=}\). The partial order \(\sqsubseteq_{\textsc{DFA}_{\mathit{n}}}\) is induced by language inclusion, i.e., \(\forall\mathtt{A}_{1},\mathtt{A}_{2}\in\textsc{DFA}_{/=}.\mathtt{A}_{1} \sqsubseteq_{\textsc{DFA}_{2}}\Leftrightarrow\mathscr{L}(\mathtt{A}_{1}) \subseteq\mathscr{L}(\mathtt{A}_{2})\), which is well defined since automata in the same \(\equiv\)-equivalence class recognize the same language. The corresponding least upper bound, \(\sqcup_{\textsc{DFA}_{/=}}\times\textsc{DFA}_{/=}\to\textsc{DFA}_{/=}\) on the domain \(\textsc{DFA}_{/=}\), is the standard union between automata: \(\forall\mathtt{A}_{1},\mathtt{A}_{2}\in\textsc{DFA}_{/=}.\mathtt{A}_{1}\sqcup _{\textsc{DFA}_{2}}\stackrel{{\mathit{id}}}{{=}}\text{Min}( \mathscr{L}(\mathtt{A}_{1})\cup\mathscr{L}(\mathtt{A}_{2}))\). It is the minimum automaton recognizing the union of the languages \(\mathscr{L}(\mathtt{A}_{1})\) and \(\mathscr{L}(\mathtt{A}_{2})\). This is a well-defined notion since regular languages are closed under union. As example consider Figure 4, where the automaton in Figure 4 is the least upper bound of \(\mathtt{A}_{1}\) and \(\mathtt{A}_{2}\) given in Figure 4,b, respectively. Figure 3: \(\mu\)JS implicit type conversion functions. The (finite) greatest lower bound \(\sqcap_{\text{Dfa}}:\text{Dfa}_{/=}\times\text{Dfa}_{/=}\to\text{Dfa}_{/=}\) corresponds to automata intersection (since regular languages are closed under finite intersection): \(\forall\text{A}_{1},\text{A}_{2}\in\text{Dfa}_{/=}.\text{A}_{1}\sqcap_{\text{Dfa}} \text{A}_{2}\stackrel{{\text{\tiny def}}}{{=}}\text{Min}( \mathcal{L}(\text{A}_{1})\sqcap\mathcal{L}(\text{A}_{2}))\). Theorem 1.1: \(\langle\text{Dfa}_{/=},\sqsubseteq_{\text{Dfa}},\sqcup_{\text{Dfa}},\sqcap_{ \text{Dfa}},\text{Min}(\varnothing),\text{Min}(\Sigma^{*})\rangle\) _is a sub-lattice but not a complete meet-sub-semilattice of \(\wp(\Sigma^{*})\)._  
In other words, it cannot exists a Galois connection between \(\text{Dfa}_{/=}\) and \(\wp(\Sigma^{*})\), i.e., there may be no minimal automaton abstracting a language. Note that some works [22; 23; 24] have studied automatic procedures to compute, given an input language \(L\), the regular cover of \(L\)[23] (i.e., an automaton containing the language \(L\)). Some of them [22; 23] studied regular covers guaranteeing that the automaton obtained is the best w.r.t. a minimal relation (but not minimum). However this is not a concern since the relation between concrete semantics and abstract semantics can be weakened still ensuring soundness [14]. A well known example is the convex polyhedra domain [25]. Widening  
The domain \(\text{Dfa}_{/=}\) is an infinite domain, and it is not ACC, i.e., it contains infinite ascending chains.