Marco
/
UE2-Verfahren
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

DFA-Aliasanalyse nach Muchnick zusammengefasst

This commit is contained in:
Marco Ammon 2020-08-14 11:23:59 +02:00
parent 73b3276984
commit a45ac896f0
2 changed files with 43 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

BIN
verfahren.pdf
View File

Binary file not shown.

46
verfahren.tex
View File

@ -402,11 +402,51 @@
\subsection{DFA-Ansatz zur intraprozeduralen, fluss-sensitiven may-Analyse nach Muchnick}
\begin{itemize}
\item Vorwärtsproblem mit minimalen Grundblöcken
\item Sprachabhängige lokale Flussfunktionen für unmittelbare Auswirkungen pro Instruktion (Sammler/Gatherer): \begin{itemize}
\item TODO (VL-07)
\item Sprachabhängige lokale Flussfunktionen für unmittelbare Auswirkungen pro Instruktion (Sammler/Gatherer), hier für C: \begin{itemize}
\item Programmpunkt $P$: Kante in KFG der minimalen Grundblöcke
\item $\mathit{stmt}(P)$: Instruktion an Quelle der $P$-Kante
\item o.B.d.A. Annahme, dass jeder Programmpunkt $P$ nur einen Vorgänger $P'$ besitzt (synthetisch für Vorverarbeitung erzeugen)
\item Speicherstelle des Datums $x$ an Punkt $P$ $\mathit{mem}_P(x)$ initialisieren auf \begin{itemize}
\item $\mathit{star}(o)$: Für $o$ statisch allozierter Speicherbereich
\item $\mathit{anon}$: Dynamisch allozierter Speicherbereich
\end{itemize}
\item $\mathit{any}$ als Menge aller Speicherbereiche
\item Notation für Funktionen des Aliaswissens:\begin{itemize}
\item $\mathit{ptr}_P(x)$: Menge der Speicherstellen, auf die $x$ an $P$ zeigen kann
\item $\mathit{ref}_P(x)$: Menge der Speicherstellen, die an $P$ von $x$ über beliebig viele Derefenzierungen erreicht werden können
\item $\mathit{ovr}_P(x)$: Menge der Speicherstellen, die $x$ an $P$ überdecken kann
\end{itemize}
\item Flussfunktionen:\begin{itemize}
\item \texttt{x = \&a}: $\mathit{ptr}_P(x) = \lbrace\mathit{mem}_P(a)\rbrace = \lbrace\mathit{mem}_{P'}(a)\rbrace$
\item \texttt{x = y}: \begin{equation*}
\mathit{ptr}_P(x) = \mathit{ptr}_P(y) = \begin{cases*}
\lbrace \mathit{mem}_0(*y)\rbrace & falls $P' = 0$\\
\mathit{ptr}_{P'}(y) & sonst
\end{cases*}
\end{equation*}
\item \texttt{*x = a}: $\mathit{ptr}_P(x) = \mathit{ptr}_{P'}(x)$, zusätzlich wenn \texttt{*x} Zeiger $\mathit{ptr}_P(*x) = \mathit{ptr}_{P'}(*x) \cup \mathit{ptr}_{P'}(a)$
\item \texttt{f(...)}: \begin{itemize}
\item $G$: Menge der global sichtbaren Zeiger
\item $L$: Menge der lokalen Variablen im Aufrufer, deren Adresse berechnet wurde
\item $\forall x \in G \cup L:\, \mathit{ptr}_P(x) = \left(\cup_{g \in (G \cup \mathit{mem}(G))} \mathit{ref}_{P'}(g)\right) \cup \left(\cup_{l\in L} \mathit{ref}_{P'}(l)\right)$
\end{itemize}
\end{itemize}
\end{itemize}
\item Sprachunabhängiger Fixpunktpunktalgorithmus (Verbreiter/Propagator): \begin{itemize}
\item TODO (VL-07)
\item Initialisierung aller Zeigervariablen $x$ mit \begin{equation*}
\mathit{Ptr}(P, x) = \begin{cases*}
\emptyset & falls $P = 0$ und $x$ ist lokale Variable\\
\mathit{any} & falls $P = 0$ und $x$ ist globale Variable\\
\lbrace \mathit{mem}_0(*x)\rbrace & falls $P = 0$ und $x$ ist Parameter\\
\emptyset & sonst
\end{cases*}
\end{equation*}
\item Berechnung des Aliaswissens:\begin{equation*}
\mathit{Ptr}(P, x) = \begin{cases*}
\mathit{ptr}_P(x) & falls $\mathit{stmt}(P)$ Zeiger $x$ beeinflusst\\
\mathit{Ptr}(P',x) & sonst
\end{cases*}
\end{equation*}
\end{itemize}
\end{itemize}