# Static Analysis for ECMAScript String Manipulation Programs
## 6 \(\mu\)Fasa Implementation
### Extension to Interval Abstract Domain  
For the presentation of this paper, in Section 4.1, we have chosen to abstract integer values to the constant integer abstract domain. Of course this affects the abstract semantics of those string operations that involve them, namely substring, charAt, repeat and length, while the other methods only use strings or booleans. Nevertheless, \(\mu\)Fasa abstracts integer values to the more precise interval abstract domain [9], i.e., to the set Intervals.  
\[\mathsf{Intervals}\stackrel{{\text{\tiny{\it ad}}}}{{=}}\big{\{} \ [a,b]\ |\ a,b\in\mathbb{Z}\cup\{-\infty,+\infty\},a\ \leq b\ \big{\}}\cup\{\bot\}\]  
The choice of presenting the automata-based abstract semantics with constant integers, rather than intervals, was driven by the will to not burden the definition of the abstract semantics of the string operations involving integers. Let us consider the interval-based substring abstract semantics. Since intervals can be unbounded (e.g., \([5,+\infty]\)), more than 20 different cases have been identified in its abstract semantics [8]. Given substr\((\mathsf{A},[a,b],[c,d])\), for some \(\mathsf{A}\in\mathsf{DFA}_{\mathit{1}}=\), many of these cases include \(b=+\infty\) and \(d\) definite value, \(b\) definite and \(d=+\infty\), \(b,d=+\infty\) and \(a,c\) definite values and \(a\leq c\), only to cite few. Moreover, the interval-based abstract semantics does not add any further important technical detail to our contribution since the cases cited above, met with an interval-based analysis, were handled in an ad hoc manner and would have made this paper harder to follow. In particular, being the constant integer abstract domain strictly contained into the intervals one, restricting the presentation to constant integers permitted us to report only the meaningful cases (from a technical point of view), avoiding the others (related to intervals) handled in specific ways (and relevant for the implementation).  
Nevertheless, \(\mu\)Fasa implements intervals (which include constant integers) and, accordingly, the abstract semantics based on them of substring, charAt, length and repeat, as reported in [8]. The abstract semantics of the other string operations remain unaffected by the change. Just as an example, in the following we report the abstract semantics of length on intervals.  
The constant integer domain leads to a big loss in precision in the abstract semantics of length, reported in Section 5.3. The idea behind the algorithm capturing its abstract semantics is to check if any string recognized by the input automata have the same length \(l\in\mathbb{N}\). If so, \(l\) is returned as result, otherwise \(\top_{\mathsf{Const}}\) is returned. Clearly, this is a forced choice given by the fact that the constant integer abstract domain is only able to track a single integer value. In this sense, the abstract semantics of length can be improved, from a precision point of view, when we deal with intervals rather than constant integers. Algorithm 7 reports the abstract semantics of length using the former abstract domain. We compute the minimum and the maximum path reaching each final state in the automaton and then we abstract the set of lengths obtained so far into intervals. Problems arise when the automaton contains cycles. In that case, we return the undefined interval starting from the minimum path, to a final state, to \(+\infty\).  
Clearly, using the interval abstract domain produces more precise results for certain operations, but it complicates the abstract semantics of others.