diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..06afc9e --- /dev/null +++ b/Makefile @@ -0,0 +1,7 @@ +all: semantics.pdf + +%.pdf: %.tex + latexmk -pdf $< + +upload: semantics.pdf + scp semantics.pdf www.tobast:/srv/httpd/tobast.fr/public_html/m2/ diff --git a/semantics.tex b/semantics.tex new file mode 100644 index 0000000..7886962 --- /dev/null +++ b/semantics.tex @@ -0,0 +1,193 @@ +\title{DWARF Semantics} +\author{Théophile Bastian} +\date{\today} + +\documentclass[11pt]{article} + +\usepackage[left=2cm,right=2cm,top=2cm,bottom=2cm]{geometry} +\usepackage{amsmath} +\usepackage{amssymb} +\usepackage{stmaryrd} +\usepackage{mathtools} +\usepackage[utf8]{inputenc} + +\newcommand{\dwcfa}[1]{\texttt{DW\_CFA\_#1}} +\newcommand{\reg}[1]{\%#1} + +\newcommand{\DWARF}{\operatorname{DWARF}} + +\newcommand{\FDE}{\operatorname{FDE}} +\newcommand{\dwrow}{\operatorname{Row}} +\newcommand{\spexpr}{\mathbb{E}} +\newcommand{\regs}{\mathbb{R}} +\newcommand{\values}{\mathbb{V}} + +\newcommand{\valaddr}[1]{\operatorname{Addr}\left(#1\right)} +\newcommand{\valval}[1]{\operatorname{Val}\left(#1\right)} + +\newcommand{\intermedlang}{\mathcal{I}} + +\newcommand{\semI}[2]{{\left\llbracket{} #1 \right\rrbracket}^\intermedlang_{#2}} + +\newcommand{\rowstack}{\mathbb{S}} + +\newcommand{\insarrow}[1]{\xleftarrow{\text{#1}}} +\newcommand{\extrarrow}[1]{\xrightarrow{\text{#1}}} + +\newcommand{\contsem}[1]{\semI{d}{s}\left(#1\right)} + +\begin{document} +\maketitle + +\section{DWARF CFI instructions} + +These instructions are up to variants (most instructions exist in multiple +formats to handle various operands formatting, to optimize space). + +\begin{itemize} + \item{} \dwcfa{set\_loc(loc)}~: + new DWARF row at address $loc$ + \item{} \dwcfa{advance\_loc(delta)}~: + new DWARF row at address $prev\_loc + delta$ + \item{} \dwcfa{def\_cfa(reg, offset)}~: + sets CFA at $(\reg{reg} + offset)$ + \item{} \dwcfa{def\_cfa\_register(reg)}~: + sets CFA at $(\reg{reg} + prev\_offset)$ + \item{} \dwcfa{def\_cfa\_offset(offset)}~: + sets CFA at $(\reg{prev\_reg} + offset)$ + \item{} \dwcfa{def\_cfa\_expression(expr)}~: + defines CFA as the result of $expr$ + \item{} \dwcfa{undefined(reg)}~: + sets \reg{reg} undefined in the current (last) row + \item{} \dwcfa{same\_value(reg)}~: + sets \reg{reg} in the current (last) row as it was in the previous row + \item{} \dwcfa{offset(reg, offset)}~: + \reg{reg} is stored in memory at the address $CFA + offset$ in the + current (last) row + \item{} \dwcfa{val\_offset(reg, offset)}~: + \reg{reg} is the value $CFA + offset$ in the current (last) row + \item{} \dwcfa{register(reg, model)}~: + \reg{reg} has in the current (last) row the value that had + $\reg{model}$ in the previous row + \item{} \dwcfa{expression(reg, expr)}~: + \reg{reg} is stored in memory at the address defined by $expr$ + \item{} \dwcfa{val\_expression(reg, expr)}~: + \reg{reg} has the value of $expr$ + \item{} \dwcfa{restore(reg)}~: + \reg{reg} has the same value as in this FDE's preamble (CIE) in the + current (last) row. This is \emph{not implemented in this semantics} + for simplicity and brevity (we would have to introduce CIE (preamble) + and FDE (body) independently). + \item{} \dwcfa{remember\_state()}~: + push the state of all the registers of the current (last) row in an + implicit stack + \item{} \dwcfa{restore\_state()}~: + pop an entry of the implicit stack, and set all registers in the + current (last) row accordingly. + \item{} \dwcfa{nop()}~: + do nothing (padding) +\end{itemize} + +\pagebreak + +\section{Intermediary language $\intermedlang$} + +\begin{align*} + \FDE &:= {\left(\mathbb{Z} \times \dwrow \right)}^{\ast} + & \text{FDE (set of rows)} \\ + \dwrow &:= \values ^ \regs + & \text{A DWARF row} \\ + \spexpr &:= \regs \times \mathbb{Z} + & \text{A ``simple'' expression $\reg{reg} + offset$} \\ + \regs &:= \left\{0, 1, \ldots, \operatorname{NB\_REGS - 1} \right\} + & \text{Machine registers} \\ + \values &:= \{\bot\} \cup \valaddr{\spexpr} \cup \valval{\spexpr} + & \text{Values: undefined, at address $x$, value $x$} \\ +\end{align*} + + +\section{From DWARF to $\intermedlang$} + +We define $\semI{\bullet}{s} : \DWARF \times \FDE \to \FDE$, for $s$ a stack of +$\dwrow$, that is, + +\begin{align*} + s \in \rowstack &:= \dwrow^\ast +\end{align*} + +Implicitly, $\semI{\bullet}{} := \semI{\bullet}{\varepsilon}$ + +For convenience, we define $\insarrow{reg}$, the operator changing the value of +a register for a given value in the last row, as + +\[ + \left(f \in \FDE\right) \insarrow{$r \in \regs$} (v \in values) + \quad := \quad + \left( f\left[0 \ldots |f| - 2\right] \right) \cdot \left\{ + \begin{array}{r l} + r' \neq r &\mapsto \left(f[-1]\right)(r') \\ + r &\mapsto v \\ + \end{array} \right. +\] + +The same way, we define $\extrarrow{reg}$ that \emph{extracts} the rule +currently applied for $\reg{reg}$, eg. $F \extrarrow{CFA} \valval{\reg{reg} + +\text{off}}$. If the rule currently applied in such a case is \emph{not} of the +form $\reg{reg} + \text{off}$, then the program is considered erroneous. + +More generally, we define ${\extrarrow{reg}}^{-k}$ as the same operation, but +extracting in the $k$-older row, ie. ${\extrarrow{reg}}^{0}$ is the same as +$\extrarrow{reg}$, and $F {\extrarrow{reg}}^{-1} \bullet$ is the same as +$F\left[0 \ldots |F|-2\right] \extrarrow{reg} \bullet$. + +\begin{align*} + \semI{\varepsilon}{s}(F) &:= F \\ + \semI{\dwcfa{set\_loc(loc)} \cdot d}{s}(F) &:= + \contsem{F \cdot \left(loc, F[-1].row \right)} \\ + \semI{\dwcfa{adv\_loc(delta)} \cdot d}{s}(F) &:= + \contsem{F \cdot \left(F[-1].addr + delta, F[-1].row \right)} \\ + \semI{\dwcfa{def\_cfa(reg, offset)} \cdot d}{s}(F) &:= + \contsem{F \insarrow{CFA} \valval{\reg{reg} + offset}} \\ + \semI{\dwcfa{def\_cfa\_register(reg)} \cdot d}{s}(F) &:= + \text{let F }\extrarrow{CFA} \valval{\reg{oldreg} + \text{oldoffset}} + \text{ in} \\ + &\quad \contsem{F \insarrow{CFA} \valval{\reg{reg} + oldoffset}} \\ + \semI{\dwcfa{def\_cfa\_offset(offset)} \cdot d}{s}(F) &:= + \text{let F }\extrarrow{CFA} \valval{\reg{oldreg} + \text{oldoffset}} + \text{ in} \\ + &\quad \contsem{F \insarrow{CFA} \valval{\reg{oldreg} + offset}} \\ + \semI{\dwcfa{def\_cfa\_expression(expr)} \cdot d}{s}(F) &:= + \text{TO BE DEFINED} &\textbf{CHECK ME?}\\ + \semI{\dwcfa{undefined(reg)} \cdot d}{s}(F) &:= + \contsem{F \insarrow{reg} \bot} \\ + \semI{\dwcfa{same\_value(reg)} \cdot d}{s}(F) &:= + \valval{\reg{reg}} &\textbf{CHECK ME}\\ + \semI{\dwcfa{offset(reg, offset)} \cdot d}{s}(F) &:= + \contsem{F \insarrow{reg} \valaddr{\reg{CFA} + \text{offset}}} \\ + \semI{\dwcfa{val\_offset(reg, offset)} \cdot d}{s}(F) &:= + \contsem{F \insarrow{reg} \valval{\reg{CFA} + \text{offset}}} \\ + \semI{\dwcfa{register(reg, model)} \cdot d}{s}(F) &:= + \text{let } F {\extrarrow{model}}^{-1} r \text{ in } + \contsem{F \insarrow{reg} r} \\ + \semI{\dwcfa{expression(reg, expr)} \cdot d}{s}(F) &:= + \text{TO BE DEFINED} &\textbf{CHECK ME?}\\ + \semI{\dwcfa{val\_expression(reg, expr)} \cdot d}{s}(F) &:= + \text{TO BE DEFINED} &\textbf{CHECK ME?}\\ +% \semI{\dwcfa{restore(reg)} \cdot d}{s}(F) &:= \\ %% NOT IMPLEMENTED + \semI{\dwcfa{remember\_state()} \cdot d}{s}(F) &:= + \semI{d}{s \cdot F[-1].row}\left(F\right) \\ + \semI{\dwcfa{restore\_state()} \cdot d}{s \cdot t}(F) &:= + \semI{d}{s}\left(F\left[0 \ldots |F|-2\right] \cdot + \left(F[-1].addr, t\right) \right) \\ + \semI{\dwcfa{nop()} \cdot d}{s}(F) &:= \contsem{F}\\ +\end{align*} + +(The stack is used for \texttt{remember\_state}, \texttt{restore\_state}, +\texttt{restore}) + + +\section{From $\intermedlang$ to C} + +(Quite straightforward?) + +\end{document}