diff --git a/my_hyperref.sty b/my_hyperref.sty new file mode 100644 index 0000000..21c5f45 --- /dev/null +++ b/my_hyperref.sty @@ -0,0 +1,25 @@ +\usepackage{hyperref} +\usepackage{xcolor} + +\definecolor{link_blue}{RGB}{0,0,97} + +\hypersetup{ +% bookmarks=true, % show bookmarks bar? +% unicode=false, % non-Latin characters in Acrobat’s bookmarks +% pdftoolbar=true, % show Acrobat’s toolbar? +% pdfmenubar=true, % show Acrobat’s menu? +% pdffitwindow=false, % window fit to page when opened +% pdfstartview={FitH}, % fits the width of the page to the window +% pdftitle={My title}, % title +% pdfauthor={Author}, % author +% pdfsubject={Subject}, % subject of the document +% pdfcreator={Creator}, % creator of the document +% pdfproducer={Producer}, % producer of the document +% pdfkeywords={keyword1} {key2} {key3}, % list of keywords +% pdfnewwindow=true, % links in new PDF window + colorlinks=true, % false: boxed links; true: colored links + linkcolor=link_blue, % color of internal links (change box color with linkbordercolor) + citecolor=green, % color of links to bibliography + filecolor=magenta, % color of file links + urlcolor=link_blue % color of external links +} diff --git a/my_listings.sty b/my_listings.sty new file mode 100644 index 0000000..f720a6d --- /dev/null +++ b/my_listings.sty @@ -0,0 +1,63 @@ +\usepackage{listings} +\usepackage{algorithmicx} +\usepackage{algpseudocode} +\usepackage{color} +\usepackage{xcolor} +\usepackage{courier} +\definecolor{color_comment}{HTML}{2D6F19} +\definecolor{color_linenum}{HTML}{9E9E9E} +\definecolor{color_strings}{HTML}{D300F3} + + +\lstset{ % +% backgroundcolor=\color{white}, % choose the background color; you must add \usepackage{color} or \usepackage{xcolor} + basicstyle=\footnotesize\ttfamily, % the size of the fonts that are used for the code + breakatwhitespace=false, % sets if automatic breaks should only happen at whitespace + breaklines=true, % sets automatic line breaking + captionpos=b, % sets the caption-position to bottom + commentstyle=\color{color_comment}, % comment style +% deletekeywords={...}, % if you want to delete keywords from the given language +% escapeinside={\%*}{*)}, % if you want to add LaTeX within your code + extendedchars=true, % lets you use non-ASCII characters; for 8-bits encodings only, does not work with UTF-8 + frame=none, % adds a frame around the code + keepspaces=true, % keeps spaces in text, useful for keeping indentation of code (possibly needs columns=flexible) + keywordstyle=\color{blue}, % keyword style + morekeywords={*,...}, % if you want to add more keywords to the set + numbers=left, % where to put the line-numbers; possible values are (none, left, right) + numbersep=5pt, % how far the line-numbers are from the code + numberstyle=\tiny\color{color_linenum}, % the style that is used for the line-numbers + rulecolor=\color{black}, % if not set, the frame-color may be changed on line-breaks within not-black text (e.g. comments (green here)) + showspaces=false, % show spaces everywhere adding particular underscores; it overrides 'showstringspaces' + showstringspaces=false, % underline spaces within strings only + showtabs=false, % show tabs within strings adding particular underscores + stepnumber=1, % the step between two line-numbers. If it's 1, each line will be numbered + stringstyle=\color{color_strings}, % string literal style + tabsize=4, % sets default tabsize to 2 spaces +% title=\lstname, % show the filename of files included with \lstinputlisting; also try caption instead of title +% inputencoding=utf8/latin1 % To accept utf8 encoding +} + +\lstset{literate= + {á}{{\'a}}1 {é}{{\'e}}1 {í}{{\'i}}1 {ó}{{\'o}}1 {ú}{{\'u}}1 + {Á}{{\'A}}1 {É}{{\'E}}1 {Í}{{\'I}}1 {Ó}{{\'O}}1 {Ú}{{\'U}}1 + {à}{{\`a}}1 {è}{{\`e}}1 {ì}{{\`i}}1 {ò}{{\`o}}1 {ù}{{\`u}}1 + {À}{{\`A}}1 {È}{{\'E}}1 {Ì}{{\`I}}1 {Ò}{{\`O}}1 {Ù}{{\`U}}1 + {ä}{{\"a}}1 {ë}{{\"e}}1 {ï}{{\"i}}1 {ö}{{\"o}}1 {ü}{{\"u}}1 + {Ä}{{\"A}}1 {Ë}{{\"E}}1 {Ï}{{\"I}}1 {Ö}{{\"O}}1 {Ü}{{\"U}}1 + {â}{{\^a}}1 {ê}{{\^e}}1 {î}{{\^i}}1 {ô}{{\^o}}1 {û}{{\^u}}1 + {Â}{{\^A}}1 {Ê}{{\^E}}1 {Î}{{\^I}}1 {Ô}{{\^O}}1 {Û}{{\^U}}1 + {œ}{{\oe}}1 {Œ}{{\OE}}1 {æ}{{\ae}}1 {Æ}{{\AE}}1 {ß}{{\ss}}1 + {ű}{{\H{u}}}1 {Ű}{{\H{U}}}1 {ő}{{\H{o}}}1 {Ő}{{\H{O}}}1 + {ç}{{\c c}}1 {Ç}{{\c C}}1 {ø}{{\o}}1 {å}{{\r a}}1 {Å}{{\r A}}1 + {€}{{\EUR}}1 {£}{{\pounds}}1 {¬}{{$\lnot$}}1 {∞}{{$\infty$}}1 +} + +\newcommand{\true}{\lstinline$true$} +\newcommand{\false}{\lstinline$false$} + +\newcommand{\lstbash}[1]{\lstinline[language=bash]$#1$} +\newcommand{\lstocaml}[1]{\lstinline[language=Caml]$#1$} +\newcommand{\lstcpp}[1]{\lstinline[language=C++]$#1$} +\newcommand{\lstc}[1]{\lstinline[language=C]$#1$} +\newcommand{\lstpython}[1]{\lstinline[language=python]$#1$} + diff --git a/semantics.tex b/semantics.tex index 7886962..1d400a1 100644 --- a/semantics.tex +++ b/semantics.tex @@ -11,6 +11,9 @@ \usepackage{mathtools} \usepackage[utf8]{inputenc} +\usepackage{my_listings} +\usepackage{my_hyperref} + \newcommand{\dwcfa}[1]{\texttt{DW\_CFA\_#1}} \newcommand{\reg}[1]{\%#1} @@ -19,6 +22,7 @@ \newcommand{\FDE}{\operatorname{FDE}} \newcommand{\dwrow}{\operatorname{Row}} \newcommand{\spexpr}{\mathbb{E}} +\newcommand{\dwexpr}{\bar{\mathbb{E}}} \newcommand{\regs}{\mathbb{R}} \newcommand{\values}{\mathbb{V}} @@ -28,6 +32,8 @@ \newcommand{\intermedlang}{\mathcal{I}} \newcommand{\semI}[2]{{\left\llbracket{} #1 \right\rrbracket}^\intermedlang_{#2}} +\newcommand{\semC}[1]{{\left\llbracket{} #1 \right\rrbracket}^{C}} +\newcommand{\semR}[1]{{\left\llbracket{} #1 \right\rrbracket}^{R}} \newcommand{\rowstack}{\mathbb{S}} @@ -36,6 +42,8 @@ \newcommand{\contsem}[1]{\semI{d}{s}\left(#1\right)} +\newcommand{\ehelf}{\texttt{EH\_ELF}} + \begin{document} \maketitle @@ -99,6 +107,8 @@ formats to handle various operands formatting, to optimize space). & \text{A DWARF row} \\ \spexpr &:= \regs \times \mathbb{Z} & \text{A ``simple'' expression $\reg{reg} + offset$} \\ + \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} @@ -188,6 +198,51 @@ $F\left[0 \ldots |F|-2\right] \extrarrow{reg} \bullet$. \section{From $\intermedlang$ to C} -(Quite straightforward?) +\textit{This only defines the semantics, with respect to standard C, of DWARF +as interpreted by \ehelf\@. It is not implemented this way.} + +We now define $\semC{\bullet} : \DWARF \to C$. + +These semantics are to be interpreted in the following context~: + +\lstinputlisting[language=C]{src/c_context.c} + +Then, the function \lstc{unwind_frame}, given an instruction pointer and the +state of the registers in the previous call frame, returns the state of +registers after the current call frame is unwinded. In other words, assuming +the C language is capable of formal operations, a call to +\lstc{unwind_frame(ip, {reg_0, reg_1, ..., reg_N-1})} should return something +equivalent to the corresponding DWARF row. + +The translation from $\intermedlang$ to C is defined as follows: + +\begin{itemize} + \item $\semC{\varepsilon} =$ \\ + \begin{lstlisting}[language=C, mathescape=true] + else { + for(int reg=0; reg < NB_REGS; ++reg) + new_ctx[reg] = $\semR{\bot}$; + } + \end{lstlisting} + + \item $\semC{(\text{loc}, \text{row}) \cdot t} = C\_code + \semC{t}$, where + $C\_code$ is + \begin{lstlisting}[language=C, mathescape=true] + if(ip >= $loc$) { + for(int reg=0; reg < NB_REGS; ++reg) + new_ctx[reg] = $\semR{row[reg]}$; + goto end_ifs; // Avoid if/else if problems + } + \end{lstlisting} +\end{itemize} + +and $\semR{\bullet}$ is defined as +\begin{align*} + \semR{\bot} &= \text{\lstc{ERROR_VALUE}} \\ + \semR{\valaddr{\text{reg}, \text{offset}}} &= + \text{\lstc{*(old_ctx[reg] + offset)}} \\ + \semR{\valval{\text{reg}, \text{offset}}} &= + \text{\lstc{(old_ctx[reg] + offset)}} \\ +\end{align*} \end{document} diff --git a/src/c_context.c b/src/c_context.c new file mode 100644 index 0000000..6cbad00 --- /dev/null +++ b/src/c_context.c @@ -0,0 +1,18 @@ +#include +#include +#include + +#define NB_REGS 32 /* put the number of registers of your platform here */ + +typedef uintptr_t* regs_t; // Array of size at least NB_REGS + +regs_t unwind_frame(uintptr_t ip, regs_t old_ctx) { + regs_t new_ctx = (regs_t) malloc(sizeof(uintptr_t) * NB_REGS); + assert(new_ctx != NULL); + + // ===== INSERT GENERATED CODE HERE ===== + +end_ifs: + + return new_ctx; +}