DFA-Aliasanalyse erweitert

verfahren.tex

@@ -28,6 +28,8 @@
 %\pdfminorversion=7 % Import-Unterstützung für PDFs bis Version 1.7
 %\pgfplotsset{compat=1.16} % verhindern, dass pgfplots im Rückwärtskompatibilitätsmodus arbeitet
 
+% TODO: MathOperators verwenden
+% TODO: Code in \texttt{} setzen
 
 \setlist[enumerate,1]{label={\arabic*.}}
 \setlist[enumerate,2]{label={\alph*)}}
@@ -210,7 +212,7 @@
 		\item Vorverarbeitung: und sowie Wertgleichheit
 	\end{itemize}
 	\item Kopienfortschreibung: \begin{itemize}
-		\item Eine Bitposition pro aus Kopieren entstandener Wergleichtheitsbeziehung
+		\item Eine Bitposition pro aus Kopieren entstandener Wertgleichtheitsbeziehung
 		\item Setzen bei Kopieroperation
 		\item Zurücksetzen wenn Original oder Kopie mindestens schwach definiert wird
 		\item Anfangsbelegung: false
@@ -314,6 +316,51 @@
 		\item Falls $t$ in unbesuchten Blöcken nicht geändert wurde, $\mathrm{wn}_Z(t) = \phi'(\mathrm{wn}_X(t),\mathrm{wn}_Y(t))$ löschen und alle Verwendungen von $\mathrm{wn}_Z(t)$ durch $\mathrm{wn}_X(t)$ ersetzen
 	\end{itemize}
 \end{itemize}
+\newpage
+\subsubsection{Wertnummerierungsverfahren nach Click/Braun (aus Übung)}
+\begin{algorithmic}
+	\Function{Visit}{Basisblock $b$}
+		\State Wertnummerierung mit ReadVar/WriteVar durchführen
+		\ForAll{KFG-Nachfolger $s$ von $b$}
+			\If{$b$ ist letzter Vorgänger (höchste Tiefensuchnummer) von $s$}
+				\State \Call{Seal}{$s$}
+			\EndIf
+			\If{$s$ noch nicht besucht}
+				\State \Call{Visit}{$s$}
+			\EndIf
+		\EndFor
+	\EndFunction
+	\Statex
+	\Function{Seal}{Basisblock $b$}
+		\ForAll{vorläufige $\phi$-Funktion für Variable $v$ in $b$}
+			\ForAll{KFG-Vorgänger $p$ von $b$}
+				\State \Call{ReadVar}{$v$, $p$} als Operand zu $\phi$-Funktion hinzufügen
+			\EndFor
+		\EndFor
+	\EndFunction
+	\Statex
+	\Function{WriteVar}{Variable $v$, Basisblock $b$}
+		\State \Return nächste frische Wertnummer für $v$
+	\EndFunction
+	\Statex
+	\Function{ReadVar}{Variable $v$, Basisblock $b$}
+		\If{$b$ enthält bereits Wertnummer für $v$}
+			\State \Return Wertnummer für $v$ in $b$
+		\EndIf
+		\If{$b$ ist noch nicht versiegelt}
+			\State vorläufige $\phi$-Funktion mit nächster Wertnummer für $v$ in $b$ einfügen
+			\State \Return Wertnummer der $\phi$-Funktion
+		\ElsIf{$b$ hat nur einen Vorgänger $p$}
+			\State \Return \Call{ReadVar}{$v$, $p$}
+		\Else
+			\State $phi$-Funktion mit nächster Wertnummer für $v$ in $b$ in einfügen
+			\ForAll{KFG-Vorgänger $p$ von $b$}
+				\State \Call{ReadVar}{$v$, $p$} als Operand zu $\phi$-Funktion hinzufügen
+			\EndFor
+			\State \Return Wertnummer der $\phi$-Funktion
+		\EndIf
+	\EndFunction
+\end{algorithmic}
 
 \subsection{Optimierungen auf SSA-Form}
 \begin{itemize}
@@ -447,6 +494,7 @@
 				\mathit{Ptr}(P',x) & sonst
 			\end{cases*}
 		\end{equation*}
+		\item Bei Flussfunktion $\mathit{ptr}_P(*c)$ für alle $k \in \mathit{Ptr}(P, c)$ Wissen $\mathit{Ptr}(P, k)$ berechnen
 	\end{itemize}
 \end{itemize}
 
@@ -493,6 +541,7 @@
 
 \subsection{Steensgards Algorithmus zur interprozeduralen, fluss-insensitiven may-Analyse}
 \begin{itemize}
+	\item kontext-insensitiv: vermischt Aliaswissen mehrerer Aufrufe der gleichen Funktion
 	\item Speichergraph: \begin{itemize}
 		\item Knoten: eine oder mehrere Speicherstellen
 		\item gerichtete Kante: \enquote{zeigt (möglicherweise) auf}-Beziehung, damit Alias: (*start, ziel)
@@ -507,24 +556,25 @@
 		\item $a = \&b$: Kante zwischen $a$ und $b$ einfügen; sofern bereits Kante zwischen $a$ und $x$ existiert, rekursives Verschmelzen von $x$ und $b$
 		\item $a = b$:\begin{itemize}
 			\item $b$ ist Zeiger: Verschmelzen der Ziele von $a$ und $b$, anschließend zeigen beide auf diesen Knoten
-			\item $b$ ist kein Zeiger bzw. noch nicht erkannt: Annotiere $b$ mit $(a:b)$ (Falls später Zeigerziel $y$ von $b$ entdeckt wird, muss Kante von $a$ nach $y$ ergänzt werden)
+			\item $b$ ist kein Zeiger bzw. noch nicht erkannt: Annotiere $b$ mit $\lbrace a = b\rbrace$ (Falls später Zeigerziel $y$ von $b$ entdeckt wird, muss Kante von $a$ nach $y$ ergänzt werden)
 		\end{itemize}
 		\item $a = *b$: \begin{itemize}
 			\item $b$, $*b$ haben bereits ausgehende Kanten: Kante zwischen $a$ und $**b$ ergänzen
-			\item sonst: analog zu $a = b$ mit adäquaten Annotationen (TODO: Übung)
+			\item sonst: analog zu $a = b$ mit adäquaten Annotationen
 		\end{itemize}
 		\item $*a = b$: \begin{itemize}
 			\item $a$, $*a$ mit ausgehenden Kanten: rekursives Verschmelzen von $*b$ und $**a$
-			\item sonst: TODO (Übung)
+			\item $a$ noch ohne ausgehende Kante: Annotation von $a$ mit $\lbrace *a = b\rbrace$
 		\end{itemize}
 		\item $a = b \oplus c$ mit $\oplus$ binärer Operation: \begin{itemize}
-			\item $a$, $b$, $c$ keine Zeiger: Annotation von $b$ und $c$ mit $(a:b)$ bzw. $(a:c)$
-			\item $b$ oder $c$ Zeiger: Kante von $a$ nach $*b$ hinzufügen, $c$ mit $(a:c)$ annotieren
-		\end{itemize}
-		\item $x = p(y_1, \textellipsis, y_n)$: \begin{itemize}
-			\item ggf. Speichergraph für $p$ berechnen
-			\item Zuweisungsregeln für $x$ und alle $y_i$ verwenden
+			\item $a$, $b$, $c$ nicht als Zeiger erkannt: Annotation von $b$ und $c$ mit $\lbrace a= b\rbrace$ bzw. $\lbrace a= c\rbrace$
+			\item $b$ oder $c$ Zeiger: Kante von $a$ nach $*b$ hinzufügen, $c$ mit $\lbrace a = b\rbrace$ annotieren
 		\end{itemize}
+		\item $x = p(y_1, \textellipsis, y_n)$ mit Funktion $p(z_1, \textellipsis, z_n)$ \begin{enumerate}
+			\item Zuweisungsregeln $z_i = y_i$ verwenden
+			\item ggf. Speichergraph für Anweisungen von $p$ berechnen
+			\item Zuweisungsregeln für $x$ verwenden
+		\end{enumerate}
 		\item Funktionszeiger: Bei Verschmelzen auf Typen achten
 	\end{itemize}
 \end{enumerate}
@@ -555,7 +605,7 @@
 		\item Bestimmung der Schleifenausgänge, also Knoten, die KFG-Nachfolger außerhalb der natürlichen Schleife besitzen
 		\item Alle Anforderungen an Zuweisungen müssen für Herausziehbarkeit gelten:\begin{itemize}
 			\item schleifeninvariant
-			\item in Grundblock, der alle Schleifenausgänge dominiert und alle die Variable nutzenden Blöcke strikt dominiert
+			\item in Grundblock, der alle Schleifenausgänge, nach denen die Variable lebendig ist, dominiert und alle die Variable nutzenden Blöcke strikt dominiert (oder in definierendem Block nach Definition auftritt)
 			\item einzige Zuweisung zu Variable in der ganzen Schleife
 		\end{itemize}
 		\item Herausziehen vor den Schleifenkopf in Breitensuchreihenfolge zur Bewahrung der Datenabhängigkeiten zwischen herausgezogenen Zuweisungen
@@ -661,7 +711,8 @@
 \subsection{Indexanalyse}
 \begin{itemize}
 	\item Bestimmung, ob 2 Array-Zugriffe selbe bzw. unterschiedliche Elemente ansprechen: Grundannahme pessimistisch (gleiches Element)
-	\item Für 2 Array-Zugriffe $S1: A[f_1(i_1, \textellipsis, i_d), \textellipsis, f_m(i_1, \textellipsis, i_d)]$ und $S2: A[f_1(i_1, \textellipsis, i_d), \textellipsis, f_m(i_1, \textellipsis, i_d)]$ gilt $S1 \delta S2$ $\Leftrightarrow$:\begin{itemize}
+	\item Für 2 Array-Zugriffe $S1$ $A[f_1(i_1, \textellipsis, i_d), \textellipsis, f_m(i_1, \textellipsis, i_d)]$ und\\
+	$S2$ $A[g_1(i_1, \textellipsis, i_d), \textellipsis, g_m(i_1, \textellipsis, i_d)]$ gilt $S1 \delta S2$ $\Leftrightarrow$:\begin{itemize}
 		\item mindestens ein Schreibzugriff
 		\item $\exists I, J: I=(i_1, \textellipsis, i_d) \angle J =(j_1, \textellipsis, j_d)$ mit $I, J$ innerhalb der Schleifengrenzen (Ungleichunssystem mit Nebenbedingungen)
 		\item $\forall p: f_p(I) = g_p(J)$ (Gleichungssystem mit Schleifenlaufvariablen als Variablen und Konstanten aus linearem Index-Ausdruck als Koeffizienten)
@@ -674,13 +725,16 @@
 			\item Für verschiedene Arten der Abhängigkeit in obige Kriterien einsetzen
 		\end{enumerate}
 		\item Ungleichungstest:\begin{enumerate}
-			\item Ungleichungen für verwendete Variablen aufstellen
+			\item Ungleichungen für im Code verwendete Variablen $i$ mit $i_\mathrm{w}$, $i_\mathrm{r}$ für Schreib- und Lesezugriff aufstellen:\begin{enumerate}
+				\item Ungleichungen für Schleifengrenzen
+				\item Ungleichungen für relative Beziehung von $i_\mathrm{w}$ und $i_\mathrm{r}$
+			\end{enumerate}
 			\item Gleichung für Zugriff aufstellen und so umstellen, dass 0 auf einer Seite steht
 			\item In Gleichung jeweils untere und obere Grenzwerte einsetzen und damit ein Intervall bestimmen
 			\item Sofern Intervall nicht 0 enthält, keine Abhängigkeit
 		\end{enumerate}
 		\item Fourier-Motzkin-Test: \begin{itemize}
-			\item Ungleichungssystem in kanonische Form überführen: \begin{itemize}
+			\item Ungleichungssystem in kanonische Form ($\le c$, $c$ Konstante) überführen \begin{itemize}
 				\item $\beta < b \cdot z$ untere Schranke für $z$ mit $\beta > 0$
 				\item $a \cdot z < \alpha$ obere Schranke für $z$ mit $\alpha > 0$
 			\end{itemize}
@@ -688,6 +742,22 @@
 			\begin{equation*}
 				a\cdot \beta \leq a \cdot z \cdot b \leq b\cdot \alpha \rightarrow a\cdot \beta \leq b\cdot \alpha
 			\end{equation*}
+			\item Algorithmus aus Übung: \begin{algorithmic}
+				\Repeat
+					\State Unbekannte $x_j$ auswählen
+					\State $L \gets \lbrace i \mid a_{ij} < 0 \rbrace$
+					\State $U \gets \lbrace i \mid a_{ij} > 0 \rbrace$
+					\ForAll{$i \in L \cup U$}
+						\State Reihe $i$ mit $\vert a_{ij}\vert$ normalisieren
+					\EndFor
+					\ForAll{$i \in L$}
+						\ForAll{$k \in U$}
+							\State Füge Ungleichung $A_{[i]} + A {[k]} \leq b_i + b_k$ hinzu
+						\EndFor
+					\EndFor
+					\State Ignoriere/Lösche alle Reihen aus $L \cup U$
+				\Until{System aus trivialen Ungleichungen}
+			\end{algorithmic}
 			\item Kleineres Problem $a\cdot \beta \leq b\cdot \alpha$ rekursiv lösen:\begin{itemize}
 				\item keine Lösung $\rightarrow$ unabhängig
 				\item Lösung existiert $\rightarrow$ Prüfung, ob auch ganzzahlige Lösung für $a\cdot z\cdot b$ existiert
@@ -699,7 +769,7 @@
 
 \subsection{Entfernung von schleifengetragenen Datenabhängigkeiten}
 \begin{itemize}
-	\item Legalität: Für jede Datenabhängigkeit muss die relative Reihenfolge auch nach Anwendung der Transformation bzw. Restrukturierung erhalten bleiben, die entstehenden Abhängigkeitsdistanzvektoren nicht lexikographisch sein
+	\item Legalität: Für jede Datenabhängigkeit muss die relative Reihenfolge auch nach Anwendung der Transformation bzw. Restrukturierung erhalten bleiben, d.h. die entstehenden Abhängigkeits\-distanz\-vektoren dürfen nicht lexikographisch negativ sein und müssen ihre Datenabhängigkeitsart behalten
 \end{itemize}
 
 \subsubsection{Schleifentransformationen}
@@ -790,11 +860,9 @@
 		\item ggf. Ermöglichung weiterer Optimierungen wie Verschmelzung
 	\end{itemize}
 	\item Neigen:\begin{itemize}
-		\item Schleifenneigen:\begin{itemize}
-			\item Verschiebung des Array-Indexbereichs der inneren Schleife um $f \cdot i$ mit $f$ Neigungsfaktor und $i$ Iterationsvariable der äußeren Schleife
-			\item Abzug von $f \cdot i$ bei Verwendungen der inneren Iterationsvariable
-			\item Abhängigkeit $(d_1, d_2)$ wird zu $(d_1, d_2 + f \cdot d_1)$ $\rightarrow$ Ermöglichung weiterer Restrukturierungen
-		\end{itemize}
+		\item Verschiebung des Array-Indexbereichs der inneren Schleife um $f \cdot i$ mit $f$ Neigungsfaktor und $i$ Iterationsvariable der äußeren Schleife
+		\item Abzug von $f \cdot i$ bei Verwendungen der inneren Iterationsvariable
+		\item Abhängigkeit $(d_1, d_2)$ wird zu $(d_1, d_2 + f \cdot d_1)$ $\rightarrow$ Ermöglichung weiterer Restrukturierungen
 	\end{itemize}
 	\item Allgemeiner Fall:\begin{itemize}
 		\item Transformation der Indexvektoren mit Matrix $U$ mit Eigenschaften (unimodular):\begin{itemize}