Improving Dynamic Code Analysis by Code Abstraction

A major problem in presence of dynamic code generation is that static analysis becomes extremely hard if not impossible. This happens because program data structures, such as the control-flow graph and the system of recursive equations associated with the program in question, are themselves dynamically mutating objects. Recently [4], the problem of analyzing dynamic code has been tackled by treating code as any other dynamic structure that can be statically analyzed by abstract interpretation, and to treat the abstract interpreter as any other program function that can be recursively called. In particular, in [4], we provide a static analyzer architecture for a core dynamic language, containing non-removable eval statements, that still has some limitation in terms of precision but provides the necessary ground for studying more precise solutions to the problem. In particular,

• $\bullet$

  We have designed an automata-based string abstract domain [5] for analyzing string values during execution. Automata (FA) provide the perfect choice for abstracting strings that may be executed by eval since they allow us to over-approximate the set of possible values of string variables by keeping enough information for both analyzing properties of string variables that are never executed by an eval during computation and for extracting the potential executable sub-language.

• $\bullet$

  In order to statically analyze the code potentially executed by an eval, we have designed a systematic process for extracting from the (abstract) argument of eval (i.e., from the FA collection of its potential arguments) an over-approximation of executable code that this collection contains. Clearly, this approximation must keep a form that the analyzer can interpret.

• $\bullet$

  We designed a static analyzer for dynamic languages performing a recursive call of the interpreter on the (over-approximated) code that eval may execute.

This analysis provides a first step towards the analysis of dynamic languages but still has some important precision loss [4]. In particular, there are particular forms of FA (which occur when the string is dynamically generated by loops) avoiding the possibility of generating a control flow graph ($\mathsf{CFG}$) able to approximate the code executed by an eval. For instance, when the FA accepts a language such as ${{\left\{\leavevmode\nobreak\ \mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}=(5)}}}}^{n}\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers;}}}}\left|\begin{array}[]{l}n>0\end{array}\right.\!\right\}$, the analysis in [4] cannot extract, from the FA, the $\mathsf{CFG}$ approximating the eval argument. In order to better explain the problem, consider the code in Fig. 1, where the value of i is statically unknown. In Fig. 1, we draw the automaton $A$ representing the abstract value of str before the eval execution. The problem is that $A$ has a cycle not involving a whole statement [4]. This situation makes the analyzer unable to build a $\mathsf{CFG}$ over-approximating the code potentially executed since, intuitively, such a $\mathsf{CFG}$ should be infinite. Indeed, only an infinite $\mathsf{CFG}$ could capture all the possible assignments described by the FA, namely all the assignments of any possible number formed only by ${\tt 5}$ to the variable ${\tt x}$ (i.e., x=5;,x=55;,x=555;$\dots$).

In order to make it possible to overcome this limitation, at least for a set of potential eval patterns, we propose to define a form of abstract $\mathsf{CFG}$ able to finitely represent a potential infinite set of $\mathsf{CFG}$s, e.g., we look for a $\mathsf{CFG}$ representing x=5^∗.
Unfortunately, things are not so easy as it may seem, since this abstract code representation has to be built in such a way that the analyzer may still be able to interpret it.

The main contributions for tackling the problem above are:

• $\bullet$

  We first define the notion of abstract $\mathsf{CFG}$, based on the idea of making it possible to still perform a given analysis. The idea is to leave the control structure unchanged while approximating the edge labels (the statements to execute) to sets of labels, i.e., those sharing a fixed abstract property.

• $\bullet$

  We show how completeness of code abstraction w.r.t. the semantic observation models the possibility, for the static analyzer, of interpreting also the abstract code, and we show how we can make any code abstraction complete.

• $\bullet$

  We provide a systematic approach, based on the one proposed in [4], allowing us to analyze also the eval patterns described above, for which, instead, the analysis in [4] loses precision.

The concrete semantics of our language Imp is intuitive and it is fully reported in [3]. Since our aim is to analyze Imp programs by analyzing their $\mathsf{CFG}$s, we focus here only on the interpretation of $\mathsf{CFG}$’s labels [28]. In particular, we have to specify the semantics associated with each possible edge of the $\mathsf{CFG}$. In other words, we have to formalize how each statement transforms a current state, which is represented as a store, namely as an association between identifiers and values. It is well known that static program analysis works by computing (abstract) collecting semantics, namely, for each program point $\ell$ and for each variable x, it computes the set of values that the variable x can have in any computation at the program point $\ell$. Hence, we define (collecting) memories $\mathbb{m}$, associating with each variable a set of values. The basic values of Imp are integers, booleans and strings, hence we define the set of memories as $\mathbb{M}\mbox{\raisebox{0.0pt}[4.30554pt][4.30554pt]{$\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;=\;}}$}}\textsf{Var}\rightarrow(\wp(\mathbb{Z})\cup\mathsf{Bool}\cup\wp(\Sigma^{*}))$, ranged over the meta-variable $\mathbb{m}$, where $\mathsf{Bool}=\wp(\{{\tt false},{\tt true}\})$. Let us denote by $\mathbb{V}$ this domain of collections of values $\wp(\mathbb{Z})\cup\mathsf{Bool}\cup\wp(\Sigma^{*})$. The update of memory $\mathbb{m}$ for a variable x with set of values $v$ is denoted ${\mathbb{m}[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}}}}}/v]$. The partial order $\sqsubseteq$ between memories is defined as ${{{\mathbb{m}_{\_}1\sqsubseteq\mathbb{m}_{\_}2\Leftrightarrow\forall\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}}}}}\in\mathsf{Id}.\>\mathbb{m}_{\_}1(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}}}}})\subseteq\mathbb{m}_{\_}2(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}}}}})$. Finally, lub and glb of memories are computed point-wise, i.e., ${{{\mathbb{m}_{\_}1\sqcup\mathbb{m}_{\_}2\mbox{\raisebox{0.0pt}[4.30554pt][4.30554pt]{$\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;=\;}}$}}\lambda\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}}}}}.\>\mathbb{m}_{\_}1(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}}}}})\cup\mathbb{m}_{\_}2(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}}}}})$ and ${{{\mathbb{m}_{\_}1\sqcap\mathbb{m}_{\_}2\mbox{\raisebox{0.0pt}[4.30554pt][4.30554pt]{$\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;=\;}}$}}\lambda\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}}}}}.\>\mathbb{m}_{\_}1(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}}}}})\cap\mathbb{m}_{\_}2(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}}}}})$.
The collecting (input/output) semantics of statements $\mbox{\tt c}\in\Psi$ is defined as the function ${\llbracket\mbox{\tt c}\rrbracket}:\mathbb{M}\mbox{\raisebox{0.0pt}[4.30554pt][4.30554pt]{$\mathrel{\mathop{\hskip 1.0pt\longrightarrow\hskip 1.0pt}\limits^{\,{}_{\mbox{\tiny}}}}$}}\mathbb{M}$. We denote by ${\llparenthesis\hskip 0.86108pt\cdot\hskip 0.86108pt\rrparenthesis}$ the collecting semantics of expressions, defined as additive lift⁴⁴4Let $f:S\rightarrow S$ be a generic function, by additive lift we mean its extension to sets of elements, i.e., $\forall X\subseteq S$ we define $f(X)\mbox{\raisebox{0.0pt}[4.30554pt][4.30554pt]{$\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;=\;}}$}}\left\{\leavevmode\nobreak\ f(x)\left|\begin{array}[]{l}x\in S\end{array}\right.\!\right\}$. If $f:S\rightarrow\wp(S)$, then its lift to sets of memories is $f(X)\mbox{\raisebox{0.0pt}[4.30554pt][4.30554pt]{$\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;=\;}}$}}\bigcup\left\{\leavevmode\nobreak\ f(x)\left|\begin{array}[]{l}x\in S\end{array}\right.\!\right\}$ to sets of memories of the standard expression semantics. We abuse notation by denoting as ${\llbracket\cdot\rrbracket}$ also its additive lift to sets of statements.

where $\Cap$ is the intersection in the set of Imp programs. By computing the traces of application of this transfer function, starting from any possible input memory, we precisely compute the maximal trace semantics [23].

It is well known that when we perform static analysis on a $\mathsf{CFG}$, we interpret, on the corresponding abstract domain, all the edges, and more specifically all the labels (in $\Psi$) [28]. This is also a quite standard approach, but we recall it here for fixing the notation used. We suppose to abstract values on the coalesced sum [3] of the $\mathsf{Sign}$ abstract domain for integers, of the concrete domain for booleans and of the (deterministic) finite state automata abstract domain for strings [3]⁵⁵5A string static analyzer using finite state automata abstract domain has been developed and it is available in [3].. Let us consider an abstraction $\rho\in\mbox{\it uco}(\mathbb{V})$⁶⁶6For the sake of simplicity here we abuse notation by considering a unique $\rho$ which is indeed the coalesced sum of three abstractions, one for integers, one for booleans and one for strings. of the values manipulated by our language, we denote by $\mathbb{M}^{\rho}:\textsf{Var}\mbox{\raisebox{0.0pt}[4.30554pt][4.30554pt]{$\mathrel{\mathop{\hskip 1.0pt\longrightarrow\hskip 1.0pt}\limits^{\,{}_{\mbox{\tiny}}}}$}}\rho(\mathbb{V})$ the set of (collecting) memories, where sets of values are abstracted by $\rho$, ranged over $\mathbb{m}^{\rho}$. In the following, we abuse notation by applying $\rho$ to memories in $\mathbb{M}$, simply by defining $\rho(\mathbb{m})\in\mathbb{M}^{\rho}$ as ${{\rho(\mathbb{m}):\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}}}}}\in\textsf{Var}\mapsto\rho(\mathbb{m}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}}}}}))$⁷⁷7For the sake of simplicity of presentation and implementation, we have considered here non-relational abstractions of data, anyway we believe that it is possible to easy extend our work to relational abstractions.. In this way, we can see abstract memories as sets of concrete memories, and therefore as particular collecting memories, i.e., $\mathbb{M}^{\rho}\subseteq\mathbb{M}$. Finally, we can define the abstract edge effect ${\llbracket\cdot\rrbracket}^{\rho}$ [28] telling us how to abstractly interpret each edge of the $\mathsf{CFG}$:

where ${\llparenthesis\hskip 0.86108pt\cdot\hskip 0.86108pt\rrparenthesis}^{\rho}\mbox{\raisebox{0.0pt}[4.30554pt][4.30554pt]{$\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;=\;}}$}}\rho\comp{\llparenthesis\hskip 0.86108pt\cdot\hskip 0.86108pt\rrparenthesis}\comp\rho$.The semantics of a path in the $\mathsf{CFG}$ is the composition of the interpretation of each edge, and the interpretation of an edge is the interpretation, given above, of its label [28].

This is clearly, what happens when the $\mathsf{CFG}$ is not abstracted, namely when the edge labels are single statements. Finally, since we deal with potential abstract $\mathsf{CFG}$, we have to say how we execute them, potentially on an abstract semantics. The idea is simple, since we move from executing single statements to executing sets of statements, we simply take as execution of the abstract $\mathsf{CFG}$ the additive lift of the single statements executions. Since the semantics is always additive⁸⁸8A function is said to be additive if it commutes with least upper bound., in order to guarantee that everything works, also the semantic abstraction $\rho$ must be additive. Hence, in the following of the paper we always require $\rho$ to be additive.

Following the standard approach for abstracting objects, we should abstract each $\mathsf{CFG}$ in a set of $\mathsf{CFG}$s sharing an invariant property, i.e., an equivalence class of $\mathsf{CFG}$s. In particular, since we aim at abstracting code ($\mathsf{CFG}$) without changing the analysis performed on the code, we choose to abstract $\mathsf{CFG}$ by abstracting edge labels, and by leaving unchanged the control structure of the $\mathsf{CFG}$. In other words, an abstract $\mathsf{CFG}$, denoted $\mathsf{CFG}^{\#}$, is a pair $\langle\mbox{\sl Nodes},\mbox{\sl Edges}^{\#}\rangle$, where we leave the nodes unchanged, while the edge labels are abstracted to sets of labels. Formally, $\mbox{\sl Edges}^{\#}\subseteq\mbox{\sl Nodes}\times\wp(\Psi)\times\mbox{\sl Nodes}$, where $\Psi$ is the $\mathsf{CFG}$ label language.

Given $\eta\in\mbox{\it uco}(\wp(\Psi))$, $\mathtt{G}^{\eta}\mbox{\raisebox{0.0pt}[4.30554pt][4.30554pt]{$\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;=\;}}$}}\langle\mbox{\sl Nodes}(\mathtt{G}),\mbox{\sl Edges}^{\eta}(\mathtt{G})\rangle$ is the $\mathsf{CFG}^{\#}$ built from a $\mathsf{CFG}$ $\mathtt{G}$ in terms of $\eta$, where $\mbox{\sl Edges}^{\eta}(\mathtt{G})\subseteq\mbox{\sl Nodes}(\mathtt{G})\times\eta(\wp(\Psi))\times\mbox{\sl Nodes}(\mathtt{G})$.

As previously noted, we aim at characterizing code abstractions, for dynamically generated code, for which the given analysis works precisely. Formally, let us consider the following equation:

If this equality does not hold it means that the abstract semantic interpretation ${\llbracket\cdot\rrbracket}^{\rho}$ merges predicates distinguished by $\eta$. Namely, when the program is observed by means of its (abstract) semantics the actual abstraction of predicates is not precisely $\eta$, but it is $\eta$ affected in some way by ${\llbracket\cdot\rrbracket}^{\rho}$. By changing the point of view, we have that, in this case, the analysis cannot precisely interpret the abstract code, since $\eta$ abstracts the code by distinguishing information that $\rho$ cannot distinguish.
As an example, consider the sign domain above, when ${{\eta(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}:=5}}}})=\left\{\leavevmode\nobreak\ \mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}:={\@listingGroup{ltx_lst_identifier}{n}}}}}}\left|\begin{array}[]{l}1\leq n\leq 5\end{array}\right.\!\right\}$ the equation does not hold since the concrete semantics of this set does not take any positive value for x. While, if ${{\eta(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}:=5}}}})=\left\{\leavevmode\nobreak\ \mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}:={\@listingGroup{ltx_lst_identifier}{n}}}}}}\left|\begin{array}[]{l}n\in\mathbb{Z}^{+}\cup\{0\}\end{array}\right.\!\right\}$, then Eq. 1 holds since its concrete semantics is precisely the set of non-negative values. It is worth noting that Eq. 1 is a forward completeness [16] of the code abstraction w.r.t. the semantic interpretation, meaning that the semantic abstraction does not add imprecision to the code one.
In order to investigate the relation existing between the code abstraction $\eta$ and the semantic abstraction $\rho$, we observe that, whenever we have a semantic abstraction $\rho$, we have a natural code abstraction induced by $\rho$. Namely, by only observing (abstract) information about the computation, we cannot distinguish statements with the same (abstract) semantics, independently from what any possible code abstraction does. For instance, if we analyze parity of program variables, we are unable to distinguish x:=2 from x:=4, independently from how a potential code abstraction $\eta$ is defined on x:=2. The first step consists in defining a code abstraction for expressions in terms of semantic one. Consider $\rho\in\mbox{\it uco}(\mathbb{V})$, we define $\widehat{\rho}(\mbox{\sf e})$ inductively on the expressions structure

At this point, we can characterize the $\mathsf{CFG}$ labels abstraction $\overline{\Upsilon}[\rho]:\wp(\Psi)\longrightarrow\wp(\Psi)$, as the additive lift of the function

where ${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{eval}}}}}}(\widehat{\rho}({\sf s}))$ is treated as the implicit representation of all the statements that it can execute, namely it represents the (potentially infinite) set $\left\{\leavevmode\nobreak\ \mathtt{c}\left|\begin{array}[]{l}{\llbracket\mathtt{c}\rrbracket}\mathbb{m}\sqsubseteq{\llbracket{\llparenthesis\hskip 0.86108pt{\sf s}\hskip 0.86108pt\rrparenthesis}^{\rho}\Cap\textsf{Imp}\rrbracket}^{\rho}\mathbb{m}\end{array}\right.\!\right\}$.

Finally, in order to show that this code abstraction can be used to force satisfiability of Eq. 1, we have first to characterize the meaning of interpreting an edge label abstracted by $\overline{\Upsilon}[\rho]$:

Let $\rho$ be a static analysis performing in particular $\rho_{\mbox{\tiny\sl S}}\in uco(\wp(\mathbb{S}))$ on strings, where $\mathbb{S}=\mathcal{K}^{*}$ denotes strings over a finite alphabet $\mathcal{K}$. Note that, our analyzer has to work on any (abstract) $\mathsf{CFG}$ that can be dynamically generated, hence it has to be designed with this purpose in mind. In particular, as we will show, we will generate only abstract $\mathsf{CFG}$s with a code abstraction $\eta$ complete w.r.t. $\rho$. This means, by construction, that $\eta$ must be more abstract than $\overline{\Upsilon}[\rho]$, which means that each set of elements in $\eta$ corresponds to a subset of the elements (abstract predicates) of $\overline{\Upsilon}[\rho]$. Hence, in order to guarantee to interpret predicates in any $\eta$ complete, it is sufficient to design the analyzer soundly interpreting any abstract predicate in $\overline{\Upsilon}[\rho]$. For instance, $\overline{\Upsilon}[\mathsf{Sign}]$ is the abstraction containing all the predicates, involving integers, of the form x:=S, x<S, etc, with ${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{S}}}}}}\in\mathsf{Sign}$, e.g., an abstract predicate is ${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}:=}}}}\mathbb{Z}^{+}$, and the analyzer for $\mathsf{Sign}$ should be able to interpret also such abstract predicates.
Let x be the input string parameter of an eval statement, we denote by ${\mathcal{S}^{\rho_{\mbox{\tiny\sl S}}}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}}}}})$ the abstract value for x computed by the analysis on $\rho_{\mbox{\tiny\sl S}}$. For example, suppose that the collection of values for the string x before the eval is ${{\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{a}}:=0}}}},\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{a}}:=1}}}}\}$. By defining $\rho_{\mbox{\tiny\sl S}}$ as the $k$-bounded string set abstract domain [2], with $k=2$, ${{{\mathcal{S}^{\rho_{\mbox{\tiny\sl S}}}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}}}}})=\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{a}}:=0}}}},\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{a}}:=1}}}}\}$, while by using the prefix abstract domain $\overline{\mathcal{PR}}$  [9], ${{\mathcal{S}^{\mbox{\tiny$\overline{\mathcal{PR}}$}}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}}}}})=\left\{\leavevmode\nobreak\ \mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{a}}:={\@listingGroup{ltx_lst_identifier}{s}}}}}}\left|\begin{array}[]{l}s\in\mathbb{S}\end{array}\right.\!\right\}$. When the abstracted string and the abstraction is clear from the context, we simply denote this set by $\mathcal{S}$ and we assume (for the sake of simplicity) that any string in $\mathcal{S}$ is an executable language statement¹⁰¹⁰10Note that, this assumption corresponds to a decidable condition, hence it is possible to check it and to implement ad hoc solutions when it does not hold.. In the following, we abuse notation by denoting $\mathcal{S}$ also the automaton recognizing the language.
Consider for example, the program reported in Fig. 5(a), a program building and manipulating the string str at run-time, which is, afterwards, interpreted as executable code, being the input parameter of the string-to-code statement eval. Since the value of N is unknown at compile-time, we cannot predict the precise number of iterations of the while-loop. In this case, a suitable string abstract analysis would approximate the value of str, before the eval execution, to an abstract value corresponding to an over-approximation of the possible values for str, which may be also, due to abstraction, an infinite set of strings, and therefore an infinite set of possible programs.

For instance, in the example, if we abstract strings into the regular expression abstract domain [8] (or equivalently into the finite state automata abstract domain [3]), the value of str after the while loop will be the abstract value $\mathtt{x:=5(5)^{*};}$ corresponding to an infinite set of programs, i.e., x:=5;, x:=55, x:=555;…. In this case, the common practice for analyzing eval is simply to give up with the analysis, for example by halting the analysis throwing an exception [17] or forbidding its usage [18].

Let $\rho_{\scriptscriptstyle\mathcal{CS}}$ be the abstract domain for all the possible values (integers, strings and booleans) [4]. Note that, $\overline{\Upsilon}[\rho_{\scriptscriptstyle\mathcal{CS}}]$ contains, for integers, predicates like the ones in the abstract $\mathsf{CFG}$ in Fig. 4.
The analysis $\rho_{\scriptscriptstyle\mathcal{CS}}$ at point $\ell_{\_}3$, due to widening¹¹¹¹11Widening is a fix-point accelerator used in infinite domains with infinite ascending chains, namely where the semantic fix-point computation may diverge. In this case we use a widening on automata defined in [8] applied in the analysis of the while loop [3], abstracts the value of str in the infinite language ${\left\{\leavevmode\nobreak\ \mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}:={\@listingGroup{ltx_lst_identifier}{s}}}}}}\left|\begin{array}[]{l}s\in(5)^{+}\end{array}\right.\!\right\}$ (namely x is assigned to any value represented by a finite sequence of $5$). Hence, at point $\ell_{\_}8$ the analysis abstracts str to the strings set ${\mathcal{S}_{\_}{\mathtt{str}}=\left\{\leavevmode\nobreak\ \mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{if}}({\@listingGroup{ltx_lst_identifier}{x}}\textless 5)\textbraceleft{\@listingGroup{ltx_lst_identifier}{x}}:={\@listingGroup{ltx_lst_identifier}{s}}\textbraceright{\@listingGroup{ltx_lst_identifier}{else}}\textbraceleft{\@listingGroup{ltx_lst_identifier}{x}}:=1\textbraceright}}}}\left|\begin{array}[]{l}s\in(5)^{+}\end{array}\right.\!\right\}$ meaning that, the true-branch of the string that may be transformed by eval may be either x:=5, or x:=55, or ${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}:=555}}}},\dots$. The automaton corresponding to the abstract value of str is reported in Fig. 6, and it denotes an infinite language, i.e., an infinite set of possible statements. Unfortunately, this is a problem for the analysis provided in [4], where the language containing all the possible strings would be returned, losing any precision.

At this point, we have the (potentially infinite) language of the eval argument (and hence an automaton $\mathcal{S}$), and the goal is to generate a $\mathsf{CFG}$ modeling an over-approximation of the executable code contained in the language of the automaton $\mathcal{S}$. The idea is to generate a $\mathsf{CFG}$ from a language of strings, i.e., from an automaton, by performing a parsing on the paths of the automaton. Indeed, we have defined and implemented an algorithm¹²¹²12In the following, we only discuss the main parts of the algorithm for space limitations., reported in Alg. 1, performing an abstract parser on automata that, given an automaton $\mathcal{S}$, returns the $\mathsf{CFG}$ $\mathcal{P}$ that over-approximates, for each $s\in\mathcal{S}$ (executable), the concrete execution of eval.

The idea of Alg. 1 is to perform a depth-first search on the automaton and, when a language statement is recognized, to generate an edge in the $\mathsf{CFG}$. This phase is handled by lines 3-13 of Alg. 1, building the set of nodes Nodes and the set of edges Edges of the resulting $\mathsf{CFG}$ $\mathcal{P}$. The set $W$ contains the states of the finite state automaton for which we still have to generate edges in the $\mathsf{CFG}$ and it is initialized, at line 2, with the initial state $q_{\_}0$. At this point, Alg. 1 looks for language statements readable from any path of the input automaton starting from a state $q$, taken from $W$, by means of the module $\mathrm{ReduceStmts}$ (line 5). In particular, $\mathrm{ReduceStmts}$ returns a set of triples $(q^{\prime},\mbox{\tt c},q^{\prime\prime})$, where each returned triple means that from $q^{\prime}\in Q$ to $q^{\prime\prime}\in Q$ a language statement c has been recognized.

The set returned by $\mathrm{ReduceStmts}$ corresponds to the set of statements of $\mathcal{P}$ readable from the state $q$, hence they are added to Edges, substituting the reached states with the corresponding labels by means of the function $\mathsf{lab}$ (lines 7-8). At this point, we need to look for the statements that can be read from $q^{\prime\prime}$, hence, $q^{\prime\prime}$ is added to $W$ in order to be eventually processed at the next iterations of the while loop at lines 3-13. When there are no more states of $\mathcal{S}$ to be processed, namely when $W$ is empty, the $\mathsf{CFG}$ $\mathcal{P}=\langle\mbox{\sl Nodes},\mbox{\sl Edges}\rangle$ is returned (line 14), with entry label $\mathsf{lab}(q_{\_}0)$ and exit labels the ones associated with the states in $F$.

Problems arise when the automaton contains cycles (namely, when the automaton denotes an infinite language). In this case, Alg. 1 first transforms, at line 1, the input automaton, over the alphabet $\mathcal{K}$, in an automaton without cycles, over the alphabet $\mathcal{K}\cup\wp(\mathcal{K}^{*})$, by means of the module $\mathrm{ReduceCycles}$. Given an input automaton $\mathcal{S}$, we retrieve the cycles of $\mathcal{S}$ using the well-known Tarjan’s algorithm [27] for identifying cycles. Then, for each detected cycle of $\mathcal{S}$, we check whether the string read by the cycle is a whole statement $\mathsf{r}$ or not. In the first case, we substitute the cycle of the string $\mathsf{r}$ in the automaton, i.e., $\mathsf{r}^{*}$, with the automaton reading the string corresponding to the statement while(true){ $\mathsf{r}$ } over the alphabet $\mathcal{K}$. Otherwise, if the cycle does not read a whole statement, the idea is to collapse the cycle in a single transition, labeled with the regular expression corresponding to what is read in the cycle, i.e., denoting a set of string on $\mathcal{K}$ ($\wp(\mathcal{K}^{*})$). Hence the resulting automaton is on the alphabet $\mathcal{K}\cup\wp(\mathcal{K}^{*})$. In Fig. 7 we report an example of application of $\mathrm{ReduceCycles}$ algorithm.

As example note that, by applying Alg. 1 to the automaton for $\mathcal{S}_{\_}{\mathtt{str}}$ in Fig. 6, we generate the $\mathsf{CFG}$ $\mathcal{P}_{\_}{\mathtt{str}}$, depicted in Fig. 5(b). It is worth noting that the $\mathsf{CFG}$ obtained so far may contain abstract expressions on edges, hence edges may represent an infinite collection of statements. At this point, we need to approximate these edges for making it possible to analyze the $\mathsf{CFG}$.

Let us recall that we have to perform the analysis $\rho$ also on the resulting code, in order to continue the static analysis. Hence, as observed before, we have to combine the code abstraction corresponding to the generated (abstract) $\mathsf{CFG}$ with the code abstraction induced by the semantic abstraction $\rho$, i.e., $\overline{\Upsilon}[\rho]$, which models, as code abstraction, the analysis.
First of all, we have to formally characterize the abstraction $\eta$ induced by the construction of the $\mathsf{CFG}$ given above, namely we characterize how the construction abstracts together different predicates. Let us build a code abstraction starting from the $\mathsf{CFG}$ $\mathcal{P}=\langle\mbox{\sl Nodes},\mbox{\sl Edges}\rangle$ built in Alg. 1: In particular, let $\mbox{\sl Merge}\mbox{\raisebox{0.0pt}[4.30554pt][4.30554pt]{$\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;=\;}}$}}\left\{\leavevmode\nobreak\ \left\{\leavevmode\nobreak\ \varphi\in\Psi\left|\begin{array}[]{l}\langle\ell^{\prime},\varphi,\ell^{\prime\prime}\rangle\in\mbox{\sl Edges}\end{array}\right.\!\right\}\left|\begin{array}[]{l}\ell^{\prime},\ell^{\prime\prime}\in\mbox{\sl Nodes}\end{array}\right.\!\right\}\subseteq\Psi$ be the set of collections of predicates between any pair of states in the $\mathsf{CFG}$, we define

Note that, this abstraction, being characterized starting from the $\mathsf{CFG}$ is defined only in terms of a finite subset of $\Psi$, namely on the predicates in the given $\mathsf{CFG}$, i.e., $\Psi^{\mathcal{P}}\mbox{\raisebox{0.0pt}[4.30554pt][4.30554pt]{$\stackrel{{\scriptstyle\mbox{\tiny def}}}{{\;=\;}}$}}\Psi\cap\left\{\leavevmode\nobreak\ \varphi\left|\begin{array}[]{l}\langle\ell^{\prime},\varphi,\ell^{\prime\prime}\rangle\in\mbox{\sl Edges}\end{array}\right.\!\right\}$.
In the example, ${{{{\Psi^{\mathcal{P}_{\_}{\mathtt{str}}(\wp(\Psi))}=\{\left\{\leavevmode\nobreak\ \mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}:={\@listingGroup{ltx_lst_identifier}{s}}}}}}\left|\begin{array}[]{l}s\in(5)^{+}\end{array}\right.\!\right\},\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}:=1}}}}\},\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers({\@listingGroup{ltx_lst_identifier}{x}}\textless 5)}}}}\},\{\neg\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers({\@listingGroup{ltx_lst_identifier}{x}}\textless 5)}}}}\}\}$, hence we have that $\eta^{\mathcal{P}_{\_}{\mathtt{str}}}=\wp(\Psi^{\mathcal{P}_{\_}{\mathtt{str}}})$, being $\Psi^{\mathcal{P}_{\_}{\mathtt{str}}}$ already a partition. In Fig. 8(a) this abstraction is partially depicted.

Finally, we need to satisfy Eq. 1 (completeness) between the code abstraction $\eta^{\mathcal{P}}$, built so far, and the static analysis, modeled as a semantic abstraction $\rho$, performing $\rho_{\mbox{\tiny\sl S}}$ (introduced above) on strings. Clearly we have no guarantee that $\eta^{\mathcal{P}}$ satisfies Eq. 1, hence, we have to (further) abstract the $\mathsf{CFG}$ in order to guarantee completeness w.r.t. the performed static analysis, namely in order to make it possible to perform the given static analysis on the code in the generated $\mathsf{CFG}$. As observed in the previous section, in order to force completeness, we have to combine the desired abstraction $\eta^{\mathcal{P}}$ on predicates, with the code abstraction $\overline{\Upsilon}[\rho]$. Formally, in order to allow this operation, since $\eta^{\mathcal{P}}$ is defined on $\Psi^{\mathcal{P}}$, we have to restrict also $\overline{\Upsilon}[\rho]$ on $\Psi^{\mathcal{P}}$ (denoted $\overline{\Upsilon}[\rho]^{\mathcal{P}}$). This abstraction is obtained by intersecting the meaning of each one of its elements (i.e., its concretization) with the set of predicates in the $\mathsf{CFG}$. In the running example, we have to compute $\overline{\Upsilon}[\mathsf{\rho_{\scriptscriptstyle\mathcal{CS}}}]^{\mathcal{P}_{\_}{\mathtt{str}}}$, which is the code abstraction induced by the $\mathsf{Sign}$ on the predicates in $\mathcal{P}_{\_}{\mathtt{str}}$. For instance, all the predicates in ${\left\{\leavevmode\nobreak\ \mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}:={\@listingGroup{ltx_lst_identifier}{s}}}}}}\left|\begin{array}[]{l}s\in(5)^{+}\end{array}\right.\!\right\}$ and the predicate x:=1 cannot be distinguished when integers are abstracted by observing only their signs, hence the resulting abstraction is depicted in Fig. 8(b), where the abstract predicate x:=$\mathbb{Z}^{+}$ corresponds, in the concrete, to the set of predicates ${{\left\{\leavevmode\nobreak\ \mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}:={\@listingGroup{ltx_lst_identifier}{s}}}}}}\left|\begin{array}[]{l}s\in(5)^{+}\end{array}\right.\!\right\}\cup\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers{\@listingGroup{ltx_lst_identifier}{x}}:=1}}}}\}$, while x<$\mathbb{Z}^{+}$ and $\neg$(x<$\mathbb{Z}^{+}$) correspond, respectively, to ${\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers({\@listingGroup{ltx_lst_identifier}{x}}\textless 5)}}}}\}$ and to ${\{\neg\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers({\@listingGroup{ltx_lst_identifier}{x}}\textless 5)}}}}\}$ (all the other elements corresponds to $\bot$).

Finally, we aim at building a code abstraction which can be interpreted by the initial abstract interpreter $\rho$, namely, that satisfies Eq. 1. By Th. 3.4 such an abstraction is $\mbox{\raisebox{0.0pt}[4.30554pt][4.30554pt]{$\overline{\eta}_{\_}\uparrow^{\mathcal{P}}=\overline{\Upsilon}[\rho]^{\mathcal{P}}$}}\circ\eta^{\mathcal{P}}$.

A static analyzer based on finite state automata is available at [3]. Moreover, we have implemented Alg. 1 in order to validate our approach¹³¹³13Available at
https://github.com/SPY-Lab/java-fsm-library/tree/abstract-parser. The implementation of a static analysis of abstract $\mathsf{CFG}$s is in an early stage development and it is left as future work. Nevertheless, it is able to parse executable automata and to abstract them into abstract $\mathsf{CFG}$s, as we have previously described. In order to make these abstract $\mathsf{CFG}$s effectively analyzable, we are currently extending the static analyzer, and the underlying abstract interpreter, to parse, and thus analyze, also abstract predicates.