From ef6d68b36e0269f980b014f15f992213b8e04dad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= Date: Sun, 19 Aug 2018 14:10:30 +0200 Subject: [PATCH] Add open Expr in I --- report/report.tex | 18 +++++++++++------- shared/specific.sty | 1 + 2 files changed, 12 insertions(+), 7 deletions(-) diff --git a/report/report.tex b/report/report.tex index fd21ca3..0f0b2f3 100644 --- a/report/report.tex +++ b/report/report.tex @@ -398,9 +398,9 @@ parse the relevant FDE from its start, until it finds the row it was seeking. We will now define semantics covering most of the operations used for FDEs described in the DWARF standard~\cite{dwarf5std}, such as seen in Listing~\ref{lst:ex1_dwraw}, with the exception of DWARF expressions. These are -not exhaustively treated because they form a rich language and would take a lot -of time and space to formalize, and in the meantime are only seldom used (see -the DWARF statistics regarding this). +not treated here, because they form a rich language and would take a lot +of time and space to formalize, while in the meantime being seldom used --~see +Section~\ref{ssec:instr_cov}. These semantics are defined with respect to the well-formalized C language, and are passing through an intermediary language. The DWARF language can read the @@ -489,6 +489,7 @@ Its grammar is as follows: \values &::= \bot & \text{Values: undefined,}\\ &\quad\vert~\valaddr{\spexpr} & \text{at address $x$},\\ &\quad\vert~\valval{\spexpr} & \text{of value $x$} \\ + &\quad\vert~\valexpr{??} & \text{of expression $x$, see in text} \\ \spexpr &::= \regs \times \mathbb{Z} & \text{A ``simple'' expression $\reg{reg} + \textit{offset}$} \\ \end{align*} @@ -510,7 +511,9 @@ value $x$, $x$ being here a simple expression consisting of $\reg{reg} + \textit{offset}$. The CFA is considered a simple register here. For instance, to define $\reg{rax}$ to the value contained in memory 16 bytes below the CFA, we would have $\reg{rax} \mapsto \valaddr{\reg{CFA}, -16}$, since the stack -grows downwards. +grows downwards. We also leave open the possibility to extend the language with +DWARF expressions support as $\valexpr{}$, although we \emph{do not} specify +them here. \subsection{Target language: a C function body} @@ -632,9 +635,10 @@ we omit those two operations, we can plainly remove the stack. \subsection{From $\intermedlang$ to C} -\textit{This only defines the semantics, with respect to standard C, of DWARF -as interpreted by \ehelf\@. The actual DWARF to C compiler is not implemented -this way.} +\emph{The C code provided thereafter is a correct but inefficient reference +implementation, which is only provided for formalization, to specify DWARF +\wrt{} C. In particular, the actual compiler is \emph{not} implemented this +way.} \medskip diff --git a/shared/specific.sty b/shared/specific.sty index 3150265..15bea13 100644 --- a/shared/specific.sty +++ b/shared/specific.sty @@ -24,6 +24,7 @@ \newcommand{\valaddr}[1]{\operatorname{Addr}\left(#1\right)} \newcommand{\valval}[1]{\operatorname{Val}\left(#1\right)} +\newcommand{\valexpr}[1]{\operatorname{Expr}\left(#1\right)} \newcommand{\intermedlang}{\mathcal{I}}