## 7 Instantiating M-String
### Concrete Characters, Symbolic Bounds  
In the evaluation, we instantiate the M-String domain in two ways. The first simpler instantiation sets the domain of characters \(\overline{\mathbf{C}}\) to be the concrete domain (i.e., we let the characters be represented by themselves). We let the domain of segment bounds \(\overline{\mathbf{B}}\) to be a symbolic 32b integers. This instantiation balances between simplicity on the one hand (both domains we used for parameters were already present in DIVINE) and the ability to describe strings with undetermined length and structure. At the implementation level (as described in more detail in the following section), the domain remains generic: the particular domains we picked can be easily substituted by other domains. Compared to the theoretical description of M-String, the implementation uses a slightly simplified representation of segmentation by a pair of arrays (cf. Figure 3). The elements of these arrays are characters and bounds, whose type is derived from parametrization, i.e., from the scalar domains \(\overline{\mathbf{C}}\) and \(\overline{\mathbf{B}}\). The modification of the representation is just optimization for the implementation and does not affect the operations' semantics. The analysis with this representation is presented in Example 14. This instantiation of M-String is particularly suitable for representing strings with sequences of a single character of variable length, i.e., the strings of the form \(\mathrm{a}^{\mathrm{k}}\mathrm{b}^{\mathrm{l}}\mathrm{c}^{\mathrm{m}}\dots\) where relationships between \(\mathrm{k},\mathrm{l},\mathrm{m},\dots\) can be specified using standard arithmetic and relational operators and each of \(\mathrm{a},\mathrm{b},\mathrm{c}\) is a concrete letter. This, in turn, allows M-String to be used for the analysis of program behavior on broad classes of input strings described this way. A more detailed description of this approach can be found in Section 8. **Example 14**. : _Simple program analysis with symbolic bounds and concrete characters:_  
```
1 mstringstr=abstract_string(x,\(\overline{\mathbf{b}}_{1}\),\(\backslash 0\),\(\overline{\mathbf{b}}_{2}\),\(\overline{\mathbf{b}}_{3}\),\(\backslash 0\),\(\overline{\mathbf{b}}_{4}\));
2 symbolicidx=abstract_int();
3 if(idx<\(\overline{\mathbf{b}}_{4}\)){
4 str[idx]='y';
5 symboliclen=abstract_strlen(str);
6}
```  
_Imagine we are given symbolic bounds \(\overline{\mathbf{b}}_{1}<\overline{\mathbf{b}}_{2}<\overline{\mathbf{b}}_{3}< \overline{\mathbf{b}}_{4}\), then the first line of the transformed program creates mstring value with characters \([\mathrm{x},\backslash 0,\mathrm{y},\backslash 0]\) and bounds \([0,\overline{\mathbf{b}}_{1},\overline{\mathbf{b}}_{2},\overline{\mathbf{b}}_{3 },\overline{\mathbf{b}}_{4}]\). In the following, we describe mstring values as pairs of these two arrays. The second line creates a symbolic index of arbitrary value. On line 3, the program constraints the index to be smaller than mstring maximal length. Otherwise, the update on  
Figure 3: M-String value with symbolic bounds, where string of interest is from \(\overline{\mathbf{b}}_{1}\) to \(\overline{\mathbf{b}}_{3}\). the next line would yield an error. Next the program assigns to the position of abstract index a character \(\mathbf{y}\). The assignment is implemented as update operation on _mstring value_. Depending on the value of the \(\mathtt{idx}\), the operations results in the following strings \(\overline{\mathtt{str}_{\mathtt{x}}}\), as result we join all possibilities:  
1. if \(\mathtt{idx}<\overline{\mathbf{b}}_{1}:\mathtt{idx}\) falls to the first segment: \(\overline{\mathtt{str}_{1}}=([\mathtt{x},\mathtt{y},\mathtt{x},\backslash 0,\mathtt{y}, \backslash 0],[0,\mathtt{idx},\mathtt{idx}+1,\overline{\mathbf{b}}_{1}, \overline{\mathbf{b}}_{2},\overline{\mathbf{b}}_{3},\overline{\mathbf{b}}_{4}])\) and creates a new segment between \(\mathtt{idx}\) and \(\mathtt{idx}+1\) containing character \(\mathtt{y}\).