## 6 Program Abstraction
### Syntactic Abstraction  
The first step of program abstraction performed by LART is a syntactic abstraction. Syntactic abstraction replaces LLVM instructions or whole functions with their abstract counterparts. Since we do not want to perform all operations abstractly, we need to classify only those operations that might obtain abstract values as their arguments. The abstract values emerge in the program as input values. From these values, LART computes all operations that might come into contact with abstract values using a combination of data flow and alias analyses. Finally, as a result of analyses, LART obtains a set of possibly abstract operations that are replaced by their abstract equivalents, e.g., strcat, strlen are replaced by abstract_strcat and abstract_strlen. Abstract operations then implement the manipulation with abstract values, in our case with M-Strings as described in Section 4, in other words the specific meaning of abstract instructions and abstract values then defines the semantic abstraction.  
For the precise formulation of syntactic abstraction, we take advantage of the static type system of LLVM. We leverage the fact that we can assign to each variable its type, which is either concrete or abstract. In this way, we can precisely set a boundary between concrete and abstract values.  
Figure 1: In the figure, we compare an abstract interpretation with a compilation-based approach. In the interpretation-based approach, the whole abstract interpretation is performed at runtime. The bitecode operations are interpreted abstractely by a virtual machine (VM) which maintains an abstract state. In this way, an abstract state-space is generated for a model-checking algorithm (MC). The compilation-based approach is different. The abstract operations are instrumented into the compiled program and their implementation is provided as a library. Then, the virtual machine executes the instrumented program as a regular bitcode [7].  
Figure 2: Syntactic abstraction.  
Let us consider a simplified version of LIVM. It defines a set of _concrete scalar types_ S. The set of all possible types is given by a map \(\Gamma\) that inductively defines all finite (non-recursive) algebraic types over the set of given scalars. To be precise, the set of all possible types \(\Gamma(T)\) derived from a set of scalars \(T\) is defined as follows:  
1. \(T\subseteq\Gamma(T)\), meaning each scalar type is included in \(\Gamma(T)\),
2. if \(t_{1},\ldots,t_{n}\in\Gamma(T)\) then also the _product type_ is in \(\Gamma(T)\): \((t_{1},\ldots,t_{n})\in\Gamma(T),n\in\mathbb{N}\),
3. if \(t_{1},\ldots,t_{n}\in\Gamma(T)\) then also _disjoint union_ is in \(\Gamma(T)\): \(t_{1}\mid t_{2}\mid\cdots\mid t_{n}\in\Gamma(T),n\in\mathbb{N}\),
4. if \(t\in\Gamma(T)\) then \(t^{*}\in\Gamma(T)\), where \(t^{*}\) denotes pointer type.  
In a concrete LIVM program, the set of admissible types comprise those derived from concrete scalars S, i.e., \(\Gamma(S)\). In syntactic abstraction, we need to extend admissible types by abstract types. From these, we generate all possible types using \(\Gamma\). Depending on the type of abstraction, we use a different set of basic abstract types. In the case of scalar abstraction, a set of basic abstract types contains abstract scalar types \(\overline{S}\). Correspondence between abstract and concrete scalars is given by a bijective map \(\Lambda:S\to\overline{S}\). Finally, each value, which exists in the abstracted program, has an assigned type of \(\Gamma(S\cup\overline{S})\). Specifically, this implies that the abstraction works with _mixed types_--products and unions might contain both concrete and abstract fields. Moreover, it is possible to create pointers to both abstract or mixed values.