text:
\section{Tests (Datenflussanalysen)}

Im Folgenden wird die Analyse als Beispiel für den Worklistalgorithmus \glqq Naiv\grqq\ angegeben.
%%Der Fixpunkt bei der Anwendung anderer Algorithmen ist gleich.
In diesem Beispiel wird davon ausgegangen, dass das erweiterte Java-Subset implementiert wurde.
Der CFG wird exemplarisch in Java-Code angegeben und nicht in Zwischencode wie in der implementierten Analyse.
%Hierbei wird angenommen, dass bei einer Verzweigung der linke Pfad bei einer wahren Bedingung und der rechte Pfad bei einer nicht erfüllten Bedingung genommen wird.

\subsection{Constant Folding}

Zu analysierender Code: \par

\begin{lstlisting}[frame=single]
int constFolding(int n) {
	int x = 6;
	int y = 2 * n;
	while (n > 0) {
		y = y - x;
		x = 3 * (x % 4);
		n = n - 1;
	}
	return y;
}
\end{lstlisting}

\par

\begin{figure}[H]

\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=1cm,
noname/.style={%
	ellipse,
	minimum width=5em,
	minimum height=3em,
	draw
}
]

\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In = {$n= \top, x = \perp, y = \perp$}
[*int x = 6;
int y = 2 * n;*]
Out = {$n= \top, x = \perp, y = \perp$}
\end{lstlisting}
};

\node [draw] (2) [below =of 1] {
\begin{lstlisting}[numbers=none]
In = {$n= \top, x = \perp, y = \perp$}
[*if (n > 0)*]
Out = {$n= \top, x = \perp, y = \perp$}
\end{lstlisting}
};

\node[draw] (3) [below left = 5 cm and 1 cm =of 2] {
\begin{lstlisting}[numbers=none]
In = {$n= \top, x = \perp, y = \perp$}
[*return y;*]
Out = {$n= \top, x = \perp, y = \perp$}
\end{lstlisting}
};

\node[draw] (4) [below right = 5 cm and 1 cm =of 2] {
\begin{lstlisting}[numbers=none]
In = {$n= \top, x = \perp, y = \perp$}
[*y = y - x;
x = 3 * (x % 4);
n = n - 1;*]
Out = {$n= \top, x = \perp, y = \perp$}
\end{lstlisting}
};

\path (1) edge node {} (2);
\path (2) edge [bend right=20pt] node {} (3);
\path (2) edge [bend right=20pt] node {} (4);
\path (4) edge [bend right=20pt] node {} (2);
\end{tikzpicture}

\caption{CFG im initialen Zustand der Constant-Folding-Analyse}
\end{figure}

\begin{figure}[H]
\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance= 1cm,
noname/.style={%
	ellipse,
	minimum width=5em,
	minimum height=3em,
	draw
}
]

\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In = {$n= \top, x = \perp, y = \perp$}
[*int x = 6;
int y = 2 * n;*]
Out = {$n= \top, x = 6, y = \top$}
\end{lstlisting}
};

\node [draw] (2) [below =of 1] {
\begin{lstlisting}[numbers=none]
In = {$n= \top, x = \perp, y = \perp$}
[*if (n > 0)*]
Out = {$n= \top, x = \perp, y = \perp$}
\end{lstlisting}
};

\node[draw] (3) [below left  = 5 cm and 1 cm =of 2] {
\begin{lstlisting}[numbers=none]
In = {$n= \top, x = \perp, y = \perp$}
[*return y;*]
Out = {$n= \top, x = \perp, y = \perp$}
\end{lstlisting}
};

\node[draw] (4) [below right = 5 cm and 1 cm=of 2] {
\begin{lstlisting}[numbers=none]
In = {$n= \top, x = \perp, y = \perp$}
[*y = y - x;
x = 3 * (x % 4);
n = n - 1;*]
Out = {$n= \top, x = \perp, y = \perp$}
\end{lstlisting}
};

\path (1) edge node {} (2);
\path (2) edge [bend right=20pt] node {} (3);
\path (2) edge [bend right=20pt] node {} (4);
\path (4) edge [bend right=20pt] node {} (2);
\end{tikzpicture}
\caption{CFG nach Abarbeitung des ersten Blocks der Constant-Folding-Analyse}
\end{figure}

\par

\begin{figure}[H]

\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=1cm,
noname/.style={%
	ellipse,
	minimum width=5em,
	minimum height=3em,
	draw
}
]

\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In = {$n= \top, x = \perp, y = \perp$}
[*int x = 6;
int y = 2 * n;*]
Out = {$n= \top, x = 6, y = \top$}
\end{lstlisting}
};

\node [draw] (2) [below =of 1] {
\begin{lstlisting}[numbers=none]
In = {$n= \top, x = 6, y = \top$}
[*if (n > 0)*]
Out = {$n= \top, x = 6, y = \top$}
\end{lstlisting}
};

\node[draw] (3) [below left  = 5 cm and 1 cm=of 2] {
\begin{lstlisting}[numbers=none]
In = {$n= \top, x = 6, y = \top$}
[*return y;*]
Out = {$n= \top, x = 6, y = \top$}
\end{lstlisting}
};

\node[draw] (4) [below right  = 5 cm and 1 cm=of 2] {
\begin{lstlisting}[numbers=none]
In = {$n= \top, x = 6, y = \top$}
[*y = y - x;
x = 3 * (x % 4);
n = n - 1;*]
Out = {$n= \top, x = 6, y = \top$}
\end{lstlisting}
};

\path (1) edge node {} (2);
\path (2) edge [bend right=20pt] node {} (3);
\path (2) edge [bend right=20pt] node {} (4);
\path (4) edge [bend right=20pt] node {} (2);
\end{tikzpicture}
\caption{CFG im Fixpunkt der Constant-Folding-Analyse}
\end{figure}

\newpage

\subsection{Constant Bits}

Zu analysierender Code: \par

\begin{lstlisting}[frame=single]
int constantBits(int p) {
	int x = 8 * p;
	int y = 0;
	if (p > 0) {
		y = x % 2;
	} else {
		y = x % 4;
	}
	return x + y;
}
\end{lstlisting}

\par

\begin{figure}[H]
\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=1cm,
noname/.style={%
ellipse,
minimum width=5em,
minimum height=3em,
draw
}
]
\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In$_1$ = $\{p=\top, x=\perp, y=\perp \}$
[*int x = 8 * p;
int y = 0;*]
Out$_1$ = $\{p=\top, x=\perp, y=\perp \}$
\end{lstlisting}
};

\node [draw] (2) [below=of 1] {
\begin{lstlisting}[numbers=none]
In$_2$ = $\{p=\top, x=\perp, y=\perp \}$
[*if (p > 0)*]
Out$_2$ = $\{p=\top, x=\perp, y=\perp \}$
\end{lstlisting}
};

\node[draw] (3) [below left=1cm and -2cm of 2]   {
\begin{lstlisting}[numbers=none]
In$_3$ = $\{p=\top, x=\perp, y=\perp \}$
[*y = x % 2;*]
Out$_3$ = $\{p=\top, x=\perp, y=\perp \}$
\end{lstlisting}
};

\node[draw] (4) [below right=1cm and -2cm of 2]   {
\begin{lstlisting}[numbers=none]
In$_4$ = $\{p=\top, x=\perp, y=\perp \}$
[*y = x % 4;*]
Out$_4$ = $\{p=\top, x=\perp, y=\perp \}$
\end{lstlisting}
};

\node[draw] (5) [below left=1cm and -2cm of 4]   {
\begin{lstlisting}[numbers=none]
In$_5$ = $\{p=\top, x=\perp, y=\perp \}$
[*return x + y;*]
Out$_5$ = $\{p=\top, x=\perp, y=\perp \}$
\end{lstlisting}
};

\path (1) edge node {} (2);
\path (2) edge node {} (3);
\path (2) edge node {} (4);
\path (3) edge node {} (5);
\path (4) edge node {} (5);

\end{tikzpicture}
\caption{CFG im Initialzustand der Constant-Bits-Analyse}
\end{figure}

\par

\begin{figure}[H]
\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=1cm,
noname/.style={%
ellipse,
minimum width=5em,
minimum height=3em,
draw
}
]
\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In$_1$ = $\{p=\top, x=\perp, y=\perp \}$
[*int x = 8 * p;
int y = 0;*]
Out$_1$ = $\{p=\top, x=(\top,..., \top,0,0,0), y=(0,...,0) \}$
\end{lstlisting}
};

\node [draw] (2) [below=of 1] {
\begin{lstlisting}[numbers=none]
In$_2$ = $\{p=\top, x=(\top,..., \top,0,0,0), y=(0,...,0) \}$
[*if (p > 0)*]
Out$_2$ = $\{p=\top, x=(\top,..., \top,0,0,0), y=(0,...,0) \}$
\end{lstlisting}
};

\node[draw] (3) [below left=1cm and -4cm of 2]   {
\begin{lstlisting}[numbers=none]
In$_3$ = $\{p=\top, x=\perp, y=\perp \}$
[*y = x % 2;*]
Out$_3$ = $\{p=\top, x=\perp, y=\perp \}$
\end{lstlisting}
};

\node[draw] (4) [below right=1cm and -4cm of 2]   {
\begin{lstlisting}[numbers=none]
In$_4$ = $\{p=\top, x=\perp, y=\perp \}$
[*y = x % 4;*]
Out$_4$ = $\{p=\top, x=\perp, y=\perp \}$
\end{lstlisting}
};

\node[draw] (5) [below left=1cm and -2cm of 4]   {
\begin{lstlisting}[numbers=none]
In$_5$ = $\{p=\top, x=\perp, y=\perp \}$
[*return x + y;*]
Out$_5$ = $\{p=\top, x=\perp, y=\perp \}$
\end{lstlisting}
};

\path (1) edge node {} (2);
\path (2) edge node {} (3);
\path (2) edge node {} (4);
\path (3) edge node {} (5);
\path (4) edge node {} (5);

\end{tikzpicture}
\caption{CFG nach 2 Schritten der Constant-Bits-Analyse}
\end{figure}

\par

\begin{figure}[H]
\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=1cm,
noname/.style={%
ellipse,
minimum width=5em,
minimum height=3em,
draw
}
]
\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In$_1$ = $\{p=\top, x=\perp, y=\perp \}$
[*int x = 8 * p;
int y = 0;*]
Out$_1$ = $\{p=\top, x=(\top,..., \top,0,0,0), y=(0,...,0) \}$
\end{lstlisting}
};

\node [draw] (2) [below=0.8 cm of 1] {
\begin{lstlisting}[numbers=none]
In$_2$ = $\{p=\top, x=(\top,..., \top,0,0,0), y=(0,...,0) \}$
[*if (p > 0)*]
Out$_2$ = $\{p=\top, x=(\top,..., \top,0,0,0), y=(0,...,0) \}$
\end{lstlisting}
};

\node[draw] (3) [below left=0.8cm and -4cm of 2]   {
\begin{lstlisting}[numbers=none]
In$_3$ = $\{p=\top, x=(\top,..., \top,0,0,0), y=(0,...,0) \}$
[*y = x % 2;*]
Out$_3$ = $\{p=\top, x=(\top,..., \top,0,0,0), y=(0,...,0) \}$
\end{lstlisting}
};

\node[draw] (4) [below right=0.8cm and -4cm of 3]   {
\begin{lstlisting}[numbers=none]
In$_4$ = $\{p=\top, x=(\top,..., \top,0,0,0), y=(0,...,0) \}$
[*y = x % 4;*]
Out$_4$ = $\{p=\top, x=(\top,..., \top,0,0,0), y=(0,...,0) \}$
\end{lstlisting}
};

\node[draw] (5) [below left=0.8cm and -4cm of 4]   {
\begin{lstlisting}[numbers=none]
In$_5$ = $\{p=\top, x=(\top,..., \top,0,0,0), y=(0,...,0) \}$
[*return x + y;*]
Out$_5$ = $\{p=\top, x=(\top,..., \top,0,0,0), y=(0,...,0) \}$
\end{lstlisting}
};

\path (1) edge node {} (2);
\path (2) edge node {} (3);
\path (2) edge node {} (4);
\path (3) edge node {} (5);
\path (4) edge node {} (5);

\end{tikzpicture}
\caption{CFG im Fixpunkt der Constant-Bits-Analyse}
\end{figure}

\subsection{Reaching Definitions}

Zu analysierender Code: \par

\begin{lstlisting}[frame=single]
int reachingDefs(boolean c) {
	int a, b;
	a = 1;
	b = 2;
	a = 2;
	if (c) {
	  a = 3;
	} else {
	  a = 5;
	  b = 10;
	}
	return b;
}
\end{lstlisting}

\par

\begin{figure}[H]

\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=1cm,
noname/.style={%
	ellipse,
	minimum width=5em,
	minimum height=3em,
	draw
}
]

\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In = {}
[*int a, b;
a = 1;
b = 2;
a = 2;*]
Out = {}
\end{lstlisting}
};

\node [draw] (5) [below = 1 of 1] {
\begin{lstlisting}[numbers=none]
In = {}
[*if (c)*]
Out = {}
\end{lstlisting}
};

\node [draw] (2) [below left = 3.7 cm and 4 cm =of 5] {
\begin{lstlisting}[numbers=none]
In = {}
[*a = 3;*]
Out = {}
\end{lstlisting}
};

\node[draw] (3) [below right = 3.5 cm and 4 cm =of 5] {
\begin{lstlisting}[numbers=none]
In = {}
[*a = 5;
b = 10;*]
Out = {}
\end{lstlisting}
};

\node[draw] (4) [below = 1 of 5] {
\begin{lstlisting}[numbers=none]
In = {}
[*return b;*]
Out = {}
\end{lstlisting}
};

\path (1) edge node {} (5);
\path (5) edge node {} (2);
\path (5) edge node {} (3);
\path (3) edge node {} (4);
\path (2) edge node {} (4);
\end{tikzpicture}

\caption{CFG im Initialzustand der Reaching-Definitions-Analyse}
\end{figure}

\par

\begin{figure}[H]

\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=1cm,
noname/.style={%
	ellipse,
	minimum width=5em,
	minimum height=3em,
	draw
}
]

\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In = {}
[*int a, b;
a = 1;
b = 2;
a = 2;*]
Out = {b = 2, a = 2}
\end{lstlisting}
};

\node [draw] (5) [below = 1 of 1] {
\begin{lstlisting}[numbers=none]
In = {}
[*if (c)*]
Out = {}
\end{lstlisting}
};

\node [draw] (2) [below left = 3.7 cm and 4 cm =of 5] {
\begin{lstlisting}[numbers=none]
In = {}
[*a = 3;*]
Out = {}
\end{lstlisting}
};

\node[draw] (3) [below right = 3.5 cm and 4 cm =of 5] {
\begin{lstlisting}[numbers=none]
In = {}
[*a = 5;
b = 10;*]
Out = {}
\end{lstlisting}
};

\node[draw] (4) [below = 1 of 5] {
\begin{lstlisting}[numbers=none]
In = {}
[*return b;*]
Out = {}
\end{lstlisting}
};

\path (1) edge node {} (5);
\path (5) edge node {} (2);
\path (5) edge node {} (3);
\path (3) edge node {} (4);
\path (2) edge node {} (4);
\end{tikzpicture}

\caption{CFG nach dem 1. Schritt der Reaching-Definitions-Analyse}
\end{figure}

\par

\begin{figure}[H]

\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=1cm,
noname/.style={%
	ellipse,
	minimum width=5em,
	minimum height=3em,
	draw
}
]

\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In = {}
[*int a, b;
a = 1;
b = 2;
a = 2;*]
Out = {b = 2, a = 2}
\end{lstlisting}
};

\node [draw] (5) [below = 1 of 1] {
\begin{lstlisting}[numbers=none]
In = {b = 2, a = 2}
[*if (c)*]
Out = {b = 2, a = 2}
\end{lstlisting}
};

\node [draw] (2) [below left = 5.2 cm and 2 cm =of 5] {
\begin{lstlisting}[numbers=none]
In = {b = 2, a = 2}
[*a = 3;*]
Out = {a = 3, b = 2}
\end{lstlisting}
};

\node[draw] (3) [below right = 5 cm and 2 cm =of 5] {
\begin{lstlisting}[numbers=none]
In = {b = 2, a = 2}
[*a = 5;
b = 10;*]
Out = {a = 5, b = 10}
\end{lstlisting}
};

\node[draw] (4) [below = 3.5 of 5] {
\begin{lstlisting}[numbers=none]
In = {a = 3, b = 2, a = 5, b = 10}
[*return b;*]
Out = {a = 3, b = 2, a = 5, b = 10}
\end{lstlisting}
};

\path (1) edge node {} (5);
\path (5) edge node {} (2);
\path (5) edge node {} (3);
\path (3) edge node {} (4);
\path (2) edge node {} (4);
\end{tikzpicture}

\caption{CFG im Fixpunkt der Reaching-Definitions-Analyse}
\end{figure}

\subsection{Taint-Analyse}

Zu analysierender Code: \par

\begin{lstlisting}[frame=single]
void taintAnalysis(int z) {
	int y = 3;
	int x = foo();
	_taint(x)
	if(z > 0) {
		_clean(x);
	}
	y = x + 5;
	_sensitive(y);
}
\end{lstlisting}

\par

\begin{figure}[H]

\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=1cm,
noname/.style={%
	ellipse,
	minimum width=5em,
	minimum height=3em,
	draw
}
]

\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In = {taint = $\emptyset$, violation = false}
[*int y = 3;
int x = foo();
_taint(x);*]
Out = {taint = $\emptyset$, violation = false}
\end{lstlisting}
};

\node [draw] (2) [below =of 1] {
\begin{lstlisting}[numbers=none]
In = {taint = $\emptyset$, violation = false}
[*if ( z > 0)*]
Out = {taint = $\emptyset$, violation = false}
\end{lstlisting}
};

\node[draw] (3) [below left = 5.5 cm and 0 cm = of 2] {
\begin{lstlisting}[numbers=none]
In = {taint = $\emptyset$, violation = false}
[*_clean(x);*]
Out = {taint = $\emptyset$, violation = false}
\end{lstlisting}
};

\node[draw] (4) [below right = 8.5 cm and -5 cm =of 2] {
\begin{lstlisting}[numbers=none]
In = {taint = $\emptyset$, violation = false}
[*y = x + 5;
_sensitive(y);*]
Out = {taint = $\emptyset$, violation = false}
\end{lstlisting}
};

\path (1) edge node {} (2);
\path (2) edge [bend right=20pt] node {} (3);
\path (2) edge [bend left=20pt] node {} (4);
\path (3) edge [bend right=20pt] node {} (4);
\end{tikzpicture}

\caption{CFG im initialen Zustand der Taint-Analyse}
\end{figure}

\par

\begin{figure}[H]

\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=1cm,
noname/.style={%
	ellipse,
	minimum width=5em,
	minimum height=3em,
	draw
}
]

\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In = {taint = $\emptyset$, violation = false}
[*int y = 3;
int x = foo();
_taint(x);*]
Out = {taint = {x}, violation = false}
\end{lstlisting}
};

\node [draw] (2) [below =of 1] {
\begin{lstlisting}[numbers=none]
In = {taint = {x}, violation = false}
[*if ( z > 0)*]
Out = {taint = {x}, violation = false}
\end{lstlisting}
};

\node[draw] (3) [below left = 5.5 cm and 0 cm = of 2] {
\begin{lstlisting}[numbers=none]
In = {taint = {x}, violation = false}
[*_clean(x);*]
Out = {taint = $\emptyset$, violation = false}
\end{lstlisting}
};

\node[draw] (4) [below right = 8.5 cm and -5 cm =of 2] {
\begin{lstlisting}[numbers=none]
In = {taint = $\emptyset$, violation = false}
[*y = x + 5;
_sensitive(y);*]
Out = {taint = $\emptyset$, violation = false}
\end{lstlisting}
};

\path (1) edge node {} (2);
\path (2) edge [bend right=20pt] node {} (3);
\path (2) edge [bend left=20pt] node {} (4);
\path (3) edge [bend right=20pt] node {} (4);
\end{tikzpicture}

\caption{CFG nach Abarbeitung des dritten Blocks der Taint-Analyse}
\end{figure}

\par

\begin{figure}[H]

\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=1cm,
noname/.style={%
	ellipse,
	minimum width=5em,
	minimum height=3em,
	draw
}
]

\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In = {taint = $\emptyset$, violation = false}
[*int y = 3;
int x = foo();
_taint(x);*]
Out = {taint = {x}, violation = false}
\end{lstlisting}
};

\node [draw] (2) [below =of 1] {
\begin{lstlisting}[numbers=none]
In = {taint = {x}, violation = false}
[*if ( z > 0)*]
Out = {taint = {x}, violation = false}
\end{lstlisting}
};

\node[draw] (3) [below left = 5.5 cm and 0 cm = of 2] {
\begin{lstlisting}[numbers=none]
In = {taint = {x}, violation = false}
[*_clean(x);*]
Out = {taint = $\emptyset$, violation = false}
\end{lstlisting}
};

\node[draw] (4) [below right = 8.5 cm and -5 cm =of 2] {
\begin{lstlisting}[numbers=none]
In = {taint = {x}, violation = false}
[*y = x + 5;
_sensitive(y);*]
Out = {taint = {x, y}, violation = true}
\end{lstlisting}
};

\path (1) edge node {} (2);
\path (2) edge [bend right=20pt] node {} (3);
\path (2) edge [bend left=20pt] node {} (4);
\path (3) edge [bend right=20pt] node {} (4);
\end{tikzpicture}

\caption{CFG im Fixpunkt der Taint-Analyse}
\end{figure}

\subsection{Live Variables [opt]}

Zu analysierender Code: \par

\begin{lstlisting}[frame=single]
int liveVariables(int x) {
	int y = 2 * x;
	int z = 1 - x;
	if (y > 0) {
		z = y + 1;
	} else {
		z = 1 - y;
	}
	return z;
}
\end{lstlisting}

\par

\begin{figure}[H]
\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=1cm,
noname/.style={%
ellipse,
minimum width=5em,
minimum height=3em,
draw
}
]
\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In$_1$ = $\{ \}$
[*int y = 2 * x;
int z = 1 - x;*]
Out$_1$ = $\{ \}$
\end{lstlisting}
};

\node [draw] (2) [below=of 1] {
\begin{lstlisting}[numbers=none]
In$_2$ = $\{ \}$
[*if (y > 0)*]
Out$_2$ = $\{ \}$
\end{lstlisting}
};

\node[draw] (3) [below left=of 2]   {
\begin{lstlisting}[numbers=none]
In$_3$ = $\{ \}$
[*z = y + 1;*]
Out$_3$ = $\{ \}$
\end{lstlisting}
};

\node[draw] (4) [below right=of 2]   {
\begin{lstlisting}[numbers=none]
In$_4$ = $\{ \}$
[*z = 1 - y;*]
Out$_4$ = $\{ \}$
\end{lstlisting}
};

\node[draw] (5) [below left=of 4]   {
\begin{lstlisting}[numbers=none]
In$_5$ = $\{ \}$
[*return z;*]
Out$_5$ = $\{ \}$
\end{lstlisting}
};

\path (1) edge node {} (2);
\path (2) edge node {} (3);
\path (2) edge node {} (4);
\path (3) edge node {} (5);
\path (4) edge node {} (5);

\end{tikzpicture}
\caption{CFG im Initialzustand der Live-Variables-Analyse}
\end{figure}

\par

\begin{figure}[H]
\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=1cm,
noname/.style={%
ellipse,
minimum width=5em,
minimum height=3em,
draw
}
]
\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In$_1$ = $\{ \}$
[*int y = 2 * x;
int z = 1 - x;*]
Out$_1$ = $\{x \}$
\end{lstlisting}
};

\node [draw] (2) [below=of 1] {
\begin{lstlisting}[numbers=none]
In$_2$ = $\{x \}$
[*if (y > 0)*]
Out$_2$ = $\{x,y \}$
\end{lstlisting}
};

\node[draw] (3) [below left=of 2]   {
\begin{lstlisting}[numbers=none]
In$_3$ = $\{ \}$
[*z = y + 1;*]
Out$_3$ = $\{ \}$
\end{lstlisting}
};

\node[draw] (4) [below right=of 2]   {
\begin{lstlisting}[numbers=none]
In$_4$ = $\{ \}$
[*z = 1 - y;*]
Out$_4$ = $\{ \}$
\end{lstlisting}
};

\node[draw] (5) [below left=of 4]   {
\begin{lstlisting}[numbers=none]
In$_5$ = $\{ \}$
[*return z;*]
Out$_5$ = $\{ \}$
\end{lstlisting}
};

\path (1) edge node {} (2);
\path (2) edge node {} (3);
\path (2) edge node {} (4);
\path (3) edge node {} (5);
\path (4) edge node {} (5);

\end{tikzpicture}
\caption{CFG nach 2 Schritten Live-Variables-Analyse}
\end{figure}

\par

\begin{figure}[H]
\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=1cm,
noname/.style={%
ellipse,
minimum width=5em,
minimum height=3em,
draw
}
]
\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In$_1$ = $\{ \}$
[*int y = 2 * x;
int z = 1 - x;*]
Out$_1$ = $\{x \}$
\end{lstlisting}
};

\node [draw] (2) [below=of 1] {
\begin{lstlisting}[numbers=none]
In$_2$ = $\{x \}$
[*if (y > 0)*]
Out$_2$ = $\{x,y \}$
\end{lstlisting}
};

\node[draw] (3) [below left=of 2]   {
\begin{lstlisting}[numbers=none]
In$_3$ = $\{x,y \}$
[*z = y + 1;*]
Out$_3$ = $\{x,y \}$
\end{lstlisting}
};

\node[draw] (4) [below right=of 2]   {
\begin{lstlisting}[numbers=none]
In$_4$ = $\{x,y \}$
[*z = 1 - y;*]
Out$_4$ = $\{x,y \}$
\end{lstlisting}
};

\node[draw] (5) [below left=of 4]   {
\begin{lstlisting}[numbers=none]
In$_5$ = $\{x,y \}$
[*return z;*]
Out$_5$ = $\{x,y,z \}$
\end{lstlisting}
};

\path (1) edge node {} (2);
\path (2) edge node {} (3);
\path (2) edge node {} (4);
\path (3) edge node {} (5);
\path (4) edge node {} (5);

\end{tikzpicture}
\caption{CFG im Fixpunkt der Live-Variables-Analyse}
\end{figure}

\subsection{Definite Assignment [opt]}
Zu analysierender Code: \par

\begin{lstlisting}[frame=single]
void definiteAssignmentAnalysis(int r) {
	int x, y;
	if (r > 0){
		y = 5;
	}
	x = r + 1;
}
\end{lstlisting}

d.a. $\hat{=}$ definitely assigned \\
d.u. $\hat{=}$ definitely unassigned \\
unk. $\hat{=}$ unknown

\begin{figure}[H]

\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=0.5cm,
noname/.style={%
	ellipse,
	minimum width=5em,
	minimum height=3em,
	draw
}
]

\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In$_1$ = {r = unk., x = unk., y = unk.}
[*int x,y;*]
Out$_1$ = [{r = unk. x = unk., y = unk.}
\end{lstlisting}
};

\node [draw] (2) [below=of 1] {
\begin{lstlisting}[numbers=none]
In$_2$ = = {r = unk., x = unk., y = unk.}
[*if (r > 0)*]
Out$_2$ = = {r = unk., x = unk., y = unk.}
\end{lstlisting}
};

\node[draw] (3) [below left=3.7cm and -1cm=of 2]   {
\begin{lstlisting}[numbers=none]
In$_3$ = = {r = unk., x = unk., y = unk.}
[*y = 5;*]
Out$_3$ = = {r = unk., x = unk., y = unk.}
\end{lstlisting}
};

\node[draw] (4) [below=6cm and 10cm=of 2]   {
\begin{lstlisting}[numbers=none]
In$_4$ = = {r = unk., x = unk., y = unk.}
[*x = r + 1;*]
Out$_4$ = = {r = unk., x = unk., y = unk.}
\end{lstlisting}
};

\path (1) edge node {} (2);
\path (2) edge node {} (3);
\path (2) edge [bend left=60pt] node {} (4);
\path (3) edge node {} (4);
\end{tikzpicture}

\caption{CFG im Initialzustand der Definite-Assignment-Analyse}
\end{figure}

\begin{figure}[H]

\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=0.5cm,
noname/.style={%
	ellipse,
	minimum width=5em,
	minimum height=3em,
	draw
}
]

\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In$_1$ = {r = d.a., x = d.u., y = d.u.}
[*int x,y;*]
Out$_1$ = [{r = d.a. x = d.u., y = d.u.}
\end{lstlisting}
};

\node [draw] (2) [below=of 1] {
\begin{lstlisting}[numbers=none]
In$_2$ = = {r = unk., x = unk., y = unk.}
[*if (r > 0)*]
Out$_2$ = = {r = unk., x = unk., y = unk.}
\end{lstlisting}
};

\node[draw] (3) [below left=3.7cm and -1cm=of 2]   {
\begin{lstlisting}[numbers=none]
In$_3$ = = {r = unk., x = unk., y = unk.}
[*y = 5;*]
Out$_3$ = = {r = unk., x = unk., y = unk.}
\end{lstlisting}
};

\node[draw] (4) [below=6cm and 10cm=of 2]   {
\begin{lstlisting}[numbers=none]
In$_4$ = = {r = unk., x = unk., y = unk.}
[*x = r + 1;*]
Out$_4$ = = {r = unk., x = unk., y = unk.}
\end{lstlisting}
};

\path (1) edge node {} (2);
\path (2) edge node {} (3);
\path (2) edge [bend left=60pt] node {} (4);
\path (3) edge node {} (4);
\end{tikzpicture}

\caption{CFG nach einem Schritt der Definite-Assignment-Analyse}
\end{figure}

\begin{figure}[H]

\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=0.5cm,
noname/.style={%
	ellipse,
	minimum width=5em,
	minimum height=3em,
	draw
}
]

\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In$_1$ = {r = d.a., x = d.u., y = d.u.}
[*int x,y;*]
Out$_1$ = [{r = d.a. x = d.u., y = d.u.}
\end{lstlisting}
};

\node [draw] (2) [below=of 1] {
\begin{lstlisting}[numbers=none]
In$_2$ = = {r = d.a., x = d.u., y = d.u.}
[*if (r > 0)*]
Out$_2$ = = {r = d.a., x = d.u., y = d.u.}
\end{lstlisting}
};

\node[draw] (3) [below left=3.7cm and -1cm=of 2]   {
\begin{lstlisting}[numbers=none]
In$_3$ = = {r = d.a., x = d.u., y = d.u.}
[*y = 5;*]
Out$_3$ = = {r = d.a., x = d.a., y = d.u.}
\end{lstlisting}
};

\node[draw] (4) [below=6cm and 10cm=of 2]   {
\begin{lstlisting}[numbers=none]
In$_4$ = = {r = d.a., x = d.u., y = unk.}
[*x = r + 1;*]
Out$_4$ = = {r = d.a., x = d.a., y = unk.}
\end{lstlisting}
};

\path (1) edge node {} (2);
\path (2) edge node {} (3);
\path (2) edge [bend left=60pt] node {} (4);
\path (3) edge node {} (4);
\end{tikzpicture}

\caption{CFG im Fixpunkt der Definite-Assignment-Analyse}
\end{figure}

\subsection{Available Expressions [opt]}
Zu analysierender Code: \par

\begin{lstlisting}[frame=single]
int availableExpressions(int x, int y) {
	int s,t;
	if((x+1)*(x+1)==y){
		s=x+y;
	}
	if(x*x+2*x+1!=y){
		t=x+y;
	}
	return x+y;
}
\end{lstlisting}

\par

\begin{figure}[H]

\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=0.5cm,
noname/.style={%
	ellipse,
	minimum width=5em,
	minimum height=3em,
	draw
}
]

\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In$_1$ = {}
[*int s,t;*]
Out$_1$ = {}
\end{lstlisting}
};

\node [draw] (2) [below=of 1] {
\begin{lstlisting}[numbers=none]
In$_2$ = {}
[*if ((x+1) * (x+1) == y)*]
Out$_2$ = {}
\end{lstlisting}
};

\node[draw] (3) [below left=3.9cm and 0 cm=of 2]   {
\begin{lstlisting}[numbers=none]
In$_3$ = {}
[*s = x+y;*]
Out$_3$ = {}
\end{lstlisting}
};

\node[draw] (4) [below=6.3cm and 0 cm=of 2]   {
\begin{lstlisting}[numbers=none]
In$_4$ = {}
[*if (x*x + 2*x + 1 != y)*]
Out$_4$ = {}
\end{lstlisting}
};

\node[draw] (5) [below left=8.7cm and 0cm=of 4]   {
\begin{lstlisting}[numbers=none]
In$_5$ = {}
[*t = x+y;*]
Out$_5$ = {}
\end{lstlisting}
};

\node[draw] (6) [below=11.1cm and 0 cm=of 2]   {
\begin{lstlisting}[numbers=none]
In$_6$ = {}
[*return x+y;*]
Out$_6$ = {}
\end{lstlisting}
};

\path (1) edge node {} (2);
\path (2) edge [bend right=15pt]node {} (3);
\path (2) edge [bend left=25pt] node {} (4);
\path (3) edge [bend right=15pt]node {} (4);
\path (4) edge [bend right=15pt]node {} (5);
\path (5) edge [bend right=15pt]node {} (6);
\path (4) edge [bend left=25pt] node {} (6);
\end{tikzpicture}

\caption{CFG im Initialzustand der Available-Expression-Analyse}
\end{figure}

\par

\begin{figure}[H]

\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=0.5cm,
noname/.style={%
	ellipse,
	minimum width=5em,
	minimum height=3em,
	draw
}
]

\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In$_1$ = {$x,$ $y$}
[*int s,t;*]
Out$_1$ = In$_1$
\end{lstlisting}
};

\node [draw] (2) [below=of 1] {
\begin{lstlisting}[numbers=none]
In$_2$ = Out$_1$
[*if ((x+1) * (x+1) == y)*]
Out$_2$ = In$_2$ $\cup$ {$x+1,$ $(x+1)*(x+1),$ $(x+1)*(x+1)==y$}
\end{lstlisting}
};

\node[draw] (3) [below left=3.9cm and 0 cm=of 2]   {
\begin{lstlisting}[numbers=none]
In$_3$ = {}
[*s = x+y;*]
Out$_3$ = {}
\end{lstlisting}
};

\node[draw] (4) [below=6.3cm and 0 cm=of 2]   {
\begin{lstlisting}[numbers=none]
In$_4$ = {}
[*if (x*x + 2*x + 1 != y)*]
Out$_4$ = {}
\end{lstlisting}
};

\node[draw] (5) [below left=8.7cm and 0cm=of 4]   {
\begin{lstlisting}[numbers=none]
In$_5$ = {}
[*t = x+y;*]
Out$_5$ = {}
\end{lstlisting}
};

\node[draw] (6) [below=11.1cm and 0 cm=of 2]   {
\begin{lstlisting}[numbers=none]
In$_6$ = {}
[*return x+y;*]
Out$_6$ = {}
\end{lstlisting}
};

\path (1) edge node {} (2);
\path (2) edge [bend right=15pt]node {} (3);
\path (2) edge [bend left=25pt] node {} (4);
\path (3) edge [bend right=15pt]node {} (4);
\path (4) edge [bend right=15pt]node {} (5);
\path (5) edge [bend right=15pt]node {} (6);
\path (4) edge [bend left=25pt] node {} (6);
\end{tikzpicture}

\caption{CFG nach 2 Schritten der Available-Expression-Analyse}
\end{figure}

\par

\begin{figure}[H]

\centering
\begin{tikzpicture}[%
->,
shorten >=2pt,
>=stealth,
node distance=0.5cm,
noname/.style={%
	ellipse,
	minimum width=5em,
	minimum height=3em,
	draw
}
]

\node [draw] (1) {
\begin{lstlisting}[numbers=none]
In$_1$ = {$x,$ $y$}
[*int s,t;*]
Out$_1$ = In$_1$
\end{lstlisting}
};

\node [draw] (2) [below=of 1] {
\begin{lstlisting}[numbers=none]
In$_2$ = Out$_1$
[*if ((x+1) * (x+1) == y)*]
Out$_2$ = In$_2$ $\cup$ {$x+1,$ $(x+1)*(x+1),$ $(x+1)*(x+1)==y$}
\end{lstlisting}
};

\node[draw] (3) [below left=3.9cm and 0 cm=of 2]   {
\begin{lstlisting}[numbers=none]
In$_3$ = Out$_2$
[*s = x+y;*]
Out$_3$ = In$_3$ $\cup$ {$x+y,$ $s$}
\end{lstlisting}
};

\node[draw] (4) [below=6.3cm and 0 cm=of 2]   {
\begin{lstlisting}[numbers=none]
In$_4$ = Out$_2$ $\cap$ Out$_3$ = Out$_2$
[*if (x*x + 2*x + 1 != y)*]
Out$_4$ = In$_4$ $\cup$ {$x*x,$ $2*x,$ $x*x+2*x,$ $x*x+2*x+1,$ $x*x+2*x+1!=y$}
\end{lstlisting}
};

\node[draw] (5) [below left=8.7cm and 0cm=of 4]   {
\begin{lstlisting}[numbers=none]
In$_5$ = Out$_4$
[*t = x+y;*]
Out$_5$ = In$_5$ $\cup$ {$x+y,$ $t$}
\end{lstlisting}
};

\node[draw] (6) [below=11.1cm and 0 cm=of 2]   {
\begin{lstlisting}[numbers=none]
In$_6$ = Out$_4$ $\cap$ Out$_5$ = Out$_4$
[*return x+y;*]
Out$_6$ = In$_6$ $\cup$ {$x+y$}
\end{lstlisting}
};

\path (1) edge node {} (2);
\path (2) edge [bend right=15pt]node {} (3);
\path (2) edge [bend left=25pt] node {} (4);
\path (3) edge [bend right=15pt]node {} (4);
\path (4) edge [bend right=15pt]node {} (5);
\path (5) edge [bend right=15pt]node {} (6);
\path (4) edge [bend left=25pt] node {} (6);
\end{tikzpicture}

\caption{CFG im Fixpunkt der Available-Expression-Analyse}
\end{figure}


text:
\documentclass{article}
\usepackage{haskell}

\hscommand{\vect}[1]{(#1)_v}
\hscommand{\lift}[2]{(#1)^{\uparrow#2}}
\hscommand{\liftn}[1]{(#1)^{\uparrow{n}}}

\hscommand{\patype}[1]{\mathsf{patype}\langle#1\rangle}
\hscommand{\pa}[1]{\mathsf{pa}\langle#1\rangle}

\hscommand{\capp}{\mathbin{{\$}{:}}}
\hscommand{\cappP}{\mathbin{{\$}{:}^\uparrow}}

\hscommand{\parr}[1]{[{:}{:}#1{:}{:}]}
\hscommand{\pparr}[1]{[{:}#1{:}]}

\hscommand{\Data}{\hskwd{data}}
\hscommand{\DataF}{\hskwd{data~family}}
\hscommand{\DataI}{\hskwd{data~instance}}
\hscommand{\NewtypeI}{\hskwd{newtype~instance}}

\setlength{\parindent}{0cm}

\begin{document}

\section*{Library}

\subsection*{Parallel arrays}

We distinguish between user-visible, parametric arrays (\<\pparr{\cdot}\>) and
flattened parallel arrays (\<\parr{\cdot}\>) which are internal to our
implementation. Operations on the former have purely sequential semantics.
During vectorisation, they are replaced by parallel arrays and operations.

\begin{haskell}
\Data \pparr{\alpha} = Array Int \alpha  \hscom{or similar} \\
\DataF \parr{\alpha}
\end{haskell}

\subsection*{\<PA\> dictionaries}

To avoid problems with using typeclasses in Core, we use explicit records for
representing dictionaries of type-dependent operations on parallel arrays:

\begin{haskell}
\Data PA \alpha = & PA \{
  \hsbody{lengthP & :: \parr{\alpha}\to{Int} \\
          replicateP & :: Int\to\alpha\to\parr{\alpha} \\
          \ldots \\ \}}
\end{haskell}

In vectorised code, polymorphic functions must be supplied with a \<PA\>
dictionary for each type varialbe. For instance, \<\Lambda\alpha.e\> turns
into \<\Lambda\alpha.\lambda{dPA_\alpha}::PA \alpha.e'\>.

For higher-kinded type variables, we expect a function of appropriate type
which computes the dictionary for a saturated application of the type
variable from the dictionaries of the arguments. For instance,
\<\Lambda{m}::{*}\to{*}.e\> turns into
\<\Lambda{m}::{*}\to{*}.\lambda{dPA_m}::(\forall\alpha::{*}.PA \alpha\to{PA}
(m a)).e'\>.
In general, the type of the \<dPA\> argument for a type \<\sigma::\kappa\> is
given by

\begin{haskell}
\patype{\sigma:{*}} & = PA \sigma \\
\patype{\sigma:\kappa_1\to\kappa_2} & =
\forall\alpha:\kappa_1.\patype{\alpha:\kappa_1}\to\patype{\sigma \alpha:\kappa_2}
\end{haskell}

For each user-defined or built-in type constructor \<T\> we
automatically define its dictionary \<dPA_T::\patype{T}\>. Moreover, for every
in-scope type variable \<\alpha\> we have its dictionary
\<dPA_\alpha::\patype{\alpha}\>. This allows us to compute the dictionary for
an arbitrary type as follows:

\begin{haskell}
\pa{T}           & = dPA_T \\
\pa{\alpha}      & = dPA_{\alpha} \\
\pa{\sigma \phi} & = \pa{\sigma}[\phi] \pa{\phi} \\
\pa{\forall\alpha::\kappa.\sigma} & =
\Lambda\alpha::\kappa.\lambda{dPA_{\alpha}}::\patype{\alpha::\kappa}.\pa{\sigma}
\end{haskell}

\subsection*{Closures}

Closures are represented as follows:

\begin{haskell}
\Data & Clo \alpha \beta & = \exists\gamma. Clo & (PA \gamma) \gamma
 & (\gamma\to\alpha\to\beta) (\parr{\gamma}\to\parr{\alpha}\to\parr{\beta}) \\
\DataI & \parr{Clo \alpha \beta} & = \exists\gamma. AClo & (PA \gamma)
  \parr{\gamma}
  & (\gamma\to\alpha\to\beta) (\parr{\gamma}\to\parr{\alpha}\to\parr{\beta})
\end{haskell}

Closure application is implemented by the following two operators:

\begin{haskell}
({\capp}) & :: Clo \alpha \beta \to \alpha \to \beta \\
({\cappP}) & :: \parr{Clo \alpha \beta} \to \parr{\alpha} \to \parr{\beta}
\end{haskell}

Note that \<({\cappP})\> is effectively the lifted version of \<({\capp})\>.

\subsection*{Flat array representation}

Some important instances of the \<\parr{\cdot}\> family:

\begin{haskell}
\hskwd{data} & \hskwd{instance} \parr{(\alpha_1,\ldots,\alpha_n)}
  & = ATup_n !Int \parr{\alpha_1} \ldots \parr{\alpha_n} \\
\hskwd{newtype}~ & \hskwd{instance} \parr{\alpha\to\beta}
  & = AFn (\parr{\alpha}\to\parr{\beta}) \\
\hskwd{newtype} & \hskwd{instance} \parr{PA \alpha}
  & = APA (PA \alpha)
\end{haskell}

The last two definitions are discussed later.

\section*{Vectorisation}

\subsection*{Types}

We assume that for each type constructor \<T\>, there exists a vectorised
version \<T_v\> (which can be the same as \<T\>). In particular, we have
\begin{haskell}
({\to}_v)       & = Clo \\
\pparr{\cdot}_v & = \parr{\cdot}
\end{haskell}

Vectorisation of types is defined as follows:

\begin{haskell}
\vect{T}      & = T_v \\
\vect{\alpha} & = \alpha \\
\vect{\sigma \phi} & = \vect{\sigma} \vect{\phi} \\
\vect{\forall\alpha:\kappa.\sigma} & = \forall\alpha:\kappa.\patype{\alpha:\kappa}\to\vect{\sigma}
\end{haskell}

\subsection*{Data type declarations}

\begin{haskell}
\vect{\hskwd{data} T = \overline{C t_1 \ldots t_n}} = \hskwd{data} T_v =
\overline{C_v \vect{t_1} \ldots \vect{t_n}}
\end{haskell}

\subsection*{Terms}

We distinguish between local variables (\<x\>) and global variables and
literals \<c\>.  We assume that we have the following typing judgement:

\begin{haskell}
\Delta,\Gamma\vdash{e}:\sigma
\end{haskell}

Here, \<\Delta\> assigns types to globals and \<\Gamma\> to locals. Moreover,
we assume that for each global variable \<c\>, there exists a
vectorised version \<c_v\>, i.e.,

\begin{haskell}
c:\sigma\in\Delta \Longrightarrow c_v:\vect{\sigma}\in\Delta
\end{haskell}

\subsubsection*{Vectorisation}

\begin{haskell}
\vect{c} & = c_v & c is global \\
\vect{x} & = x   & x is local \\
\vect{\Lambda\alpha:\kappa.e} & =
\Lambda\alpha:\kappa.\lambda{dPA_{\alpha}}:\patype{\alpha:\kappa}.\vect{e} \\
\vect{e[\sigma]} & = \vect{e}[\vect{\sigma}] \pa{\vect{\sigma}} \\
\vect{e_1 e_2} & = \vect{e_1}\capp\vect{e_2} \\
\vect{\lambda{x}:\sigma.e} & = Clo \vect{\sigma} \vect{\phi} \tau \pa{\tau}
                                   (y_1,\dots,y_n) \\
  &
\quad\quad(\lambda{ys}:\tau.
           \lambda{x}:\vect{\sigma}.
           \hskwd{case} ys \hskwd{of} (y_1,\dots,y_n) \to \vect{e}) \\
  &
\quad\quad(\lambda{ys}:\parr{\tau}.
           \lambda{x}:\parr{\vect{\sigma}}.
           \hskwd{case} ys \hskwd{of} ATup_n l y_1 \dots y_n \to \lift{e}{l})
\\
 \hswhere{e has type \phi \\
          \{y_1:\tau_1,\dots,y_n:\tau_n\} & = FVS(e)\setminus{x} \\
          \tau & = (\vect{\tau_1},\dots,\vect{\tau_n})}
% \\
%          e has type \phi}
\end{haskell}

Vectorisation maintains the following invariant:

\begin{haskell}
\Delta,\Gamma\vdash{e}:\sigma \Longrightarrow
      \Delta,\Gamma_v\vdash\vect{e}:\vect{\sigma}
\end{haskell}

where \<\Gamma_v\> is defined by

\begin{haskell}
x:\sigma\in\Gamma \Longleftrightarrow x:\vect{\sigma}\in\Gamma_v
\end{haskell}

\subsubsection*{Lifting}
\begin{haskell}
\liftn{c:\sigma} & = replicateP \pa{\vect{\sigma}} n c_v \\
\liftn{x}        & = x \\
\liftn{\Lambda\alpha:\kappa.e} & =
\Lambda\alpha:\kappa.\lambda{dPA_{\alpha}}:\patype{\alpha:\kappa}.\liftn{e} \\
\liftn{e[\sigma]} &  = \liftn{e}[\vect{\sigma}] \pa{\vect{\sigma}} \\
\liftn{e_1 e_2} & = \liftn{e_1} \cappP \liftn{e_2} \\
\liftn{\lambda{x}:\sigma.e} & = AClo \vect{\sigma} \vect{\phi} \vect{\tau}
                                   \pa{\vect{\tau}}
                                   (ATup_n y_1 \dots y_n) \\
  &
\quad\quad(\lambda{ys}:\vect{\tau}.
           \lambda{x}:\vect{\sigma}.
           \hskwd{case} ys \hskwd{of} (y_1,\dots,y_n) \to \vect{e}) \\
  &
\quad\quad(\lambda{ys}:\parr{\vect{\tau}}.
           \lambda{x}:\parr{\vect{\sigma}}.
           \hskwd{case} ys \hskwd{of} ATup_n l y_1 \dots y_n \to \lift{e}{l})
 \hswhere{e has type \phi \\
          \{y_1:\tau_1,\dots,y_n:\tau_n\} & = FVS(e)\setminus{x} \\
          \tau & = (\tau_1,\dots,\tau_n)}
\end{haskell}

Lifting maintains the following invariant:

\begin{haskell}
\Delta,\Gamma\vdash{e}:\sigma \Longrightarrow
  \Delta,\Gamma^\uparrow\vdash\liftn{e} : \parr{\sigma_v}
\end{haskell}

where

\begin{haskell}
x:\sigma\in\Gamma \Longleftrightarrow x:\parr{\vect{\sigma}}\in\Gamma^\uparrow
\end{haskell}

Note that this is precisely the reason for the \<\parr{\cdot}\> instances for
\<\alpha\to\beta\> and \<PA \alpha\>. A term of type \<\forall\alpha.\sigma\>
will be lifted to a term of type
\<\parr{\forall\alpha.PA \alpha\to\vect{\sigma}}\> which requires the
instances. Apart from closures, these are the only occurences of \<({\to})\> in
the transformed program, however.

\section*{What to vectorise?}

An expression is vectorisable if it only mentions globals and type constructors
which have a vectorised form. When vectorising, we look for maximal
vectorisable subexpressions and transform those. For instance, assuming that
\<print\> hasn't been vectorised, in

\begin{haskell}
main = \hsdo{
         print (sumP \pparr{\ldots}) \\
         print (mapP \ldots \pparr{\ldots})}
\end{haskell}

we would vectorise the arguments to \<print\>.  Note that this implies that we
never call non-vectorised code from vectorised code (is that a problem?).

Whenever we come out of a vectorised ``bubble'', we have to convert between
vectorised and unvectorised data types. The examples above would roughly
translate to

\begin{haskell}
main = \hsdo{
  print (unvect (sumP_v \parr{\ldots})) \\
  print (unvect (mapP_v \ldots \parr{\ldots}))}
\end{haskell}

For this, we have to have the following functions:

\begin{haskell}
vect_\sigma & :: \sigma\to\vect{\sigma} \\
unvect_\sigma & :: \vect{\sigma}\to\sigma
\end{haskell}

It is sufficient to have these functions only for a restricted set of types as
we can always vectorise less if the conversions becomes too complex.

Sometimes, it doesn't make sense to vectorise things. For instance, in

\begin{haskell}
foo f xs = print (f xs)
\end{haskell}

we wouldn't vectorise \<f xs\>. Unfortunately, this means that
\<foo (mapP f) xs\> will be purely sequential.

For each expression, the vectoriser gives one of the following answers.

\begin{tabular}{lp{10cm}}
\textbf{Yes} &
the expression can be (and has been) vectorised \\
\textbf{Maybe} &
the expression can be vectorised but it doesn't make sense to do so
unless it is used in a vectrorisable context (e.g., for \<f xs\> in \<foo\>)
\\
\textbf{No} &
the expression can't be vectorised (although parts of it can, so we
still get back a transformed expression)
\end{tabular}

\subsection*{Top-level definitions}

For a top-level definition of the form

\begin{haskell}
f :: \sigma = e
\end{haskell}

vectorisation proceeds as follows.

\begin{itemize}
\item If \<e\> can be fully vectorised, we generate
\begin{haskell}
f_v :: \vect{\sigma} = \vect{e}
\end{haskell}

\item If it doesn't always make sense to vectorise \<e\>, i.e., the vectoriser
returned \textbf{Maybe}, we leave the definition of \<f\> unchanged. Thus, we
would not change
\begin{haskell}
({\$}) = \lambda{f}.\lambda{x}.f x
\end{haskell}
but would additionaly generate
\begin{haskell}
({\$}_v) = Clo \ldots
\end{haskell}

\item Otherwise (if the vectoriser said \textbf{Yes}) and we have
\<unconv_\sigma\>, we change the definition of \<f\> to
\begin{haskell}
f :: \sigma = unconv_\sigma f_v
\end{haskell}

\item Otherwise (the vectoriser said \textbf{Yes} but we do not have
\<unconv_\sigma\> or if \<e\> couldn't be fully vectorised), we change the
definition of \<f\> to
\begin{haskell}
f :: \sigma = e'
\end{haskell}
where \<e'\> is obtaining by vectorising \<e\> as much as possible without
changing its type. For instance, for
\begin{haskell}
f = \lambda{g}.\lambda{x}.mapP (\ldots) (g x)
\end{haskell}
we would generate
\begin{haskell}
f & = \lambda{g}.\lambda{x}.unvect (mapP_v (\ldots) (vect (g x))) \\
f_v & = Clo \ldots
\end{haskell}
assuming we have the necessary conversions but cannot convert functions (i.e.,
\<g\>).
\end{itemize}

\end{document}

ext: tex

max_stars_repo_name: matchwood/ghc

max_issues_repo_name: ilyasergey/GHC-XAppFix

max_forks_repo_name: emorins/nahc


text:
%packages
\documentclass[11pt,oneside]{book}
\usepackage[margin=1.1 in]{geometry}
\usepackage[toc,page]{appendix}
\usepackage{graphicx}
\setlength{\parskip}{0.6em}
\usepackage{indentfirst}
\usepackage{natbib}
\usepackage{lipsum}
\usepackage{caption}
\usepackage{tabularx}

%titlepage

\begin{document}

\captionsetup[figure]{margin=1.5cm,font=small,labelfont={bf},name={Figure},labelsep=colon,textfont={it}}
\captionsetup[table]{margin=1.5cm,font=small,labelfont={bf},name={Table},labelsep=colon,textfont={it}}
\setlipsumdefault{1}

\begin{titlepage}

\begin{center}

{\LARGE \bfseries Hochschule für Telekommunikation Leipzig}\\[1.5cm]
\linespread{1}
\includegraphics[width=5cm]{HFTL.jpg}\\[1cm]

\linespread{1}\LARGE {\bfseries Software Engineering Specification-UX Design}\\[1.5cm]
{\Large Kaab Rustam}\\[1cm]
{\large \bfseries \emph{Supervisor:} Professorin Dr. Ing. Sabine Radomski}\\[1cm]
\large A report submitted in fulfilment of the requirements for the module\\
 \emph {Software Engineering Specification-UX Design} \\[0.3cm]
{\scriptsize in the Degree Program of}
\\[0.3cm]
 International Masters of Engineering in ICT \\[1cm]

\Large \bfseries {Topic: \emph {UX Design of ``Embold'' in the light of  User Centred Design (UCD) }}\\[0.5 cm]
\today \\[2 cm]

\small \emph {``Design is not just what it looks like and feels like. Design is how it works''}-{ \bfseries Steve Jobs}

\end{center}

\end{titlepage}

%table of contents and figures

\tableofcontents
\listoffigures

%chapters
%chapter 1
\chapter{Analysis}
\input{Chapter1.tex}

%chapter2
\chapter{User Requirements}
\input{Chapter2.tex}

%chapter3
\chapter{Product Design}
\input{Chapter3.tex}

%chapter4
\chapter{Evaluate the Design}
\input{Chapter4.tex}

%chapter5
\chapter{Conclusion}
\input{Chapter5.tex}

%bibligraphy
\addcontentsline{toc}{chapter}{Bibliography}
\bibliographystyle{plain}
\bibliography{UXbib}

\end{document}

max_stars_repo_path: UX LATEX/UX_Design.tex

max_issues_repo_path: UX LATEX/UX_Design.tex

max_forks_repo_path: UX LATEX/UX_Design.tex