% vim: spell spelllang=en

\documentclass[12pt,xcolor={usenames,dvipsnames}]{beamer}
\usetheme{Warsaw}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{booktabs}
\usepackage{makecell}
\usepackage{ifthen}
\usepackage{colortbl}
\usepackage{tabularx}
\usepackage{pifont}
\usepackage{multirow}
\usepackage[many]{tcolorbox}
\usepackage[absolute,overlay]{textpos}
\usetikzlibrary{arrows.meta,shapes}

\usepackage{texlib/my_listings}
\usepackage{texlib/specific}
\usepackage{texlib/common}
\usepackage{texlib/todo}

\usepackage{inconsolata}
\lstset{basicstyle=\footnotesize\ttfamily}

\renewcommand\theadalign{c}
\renewcommand\theadfont{\scriptsize\bfseries}

\setbeamertemplate{navigation symbols}{}
\setbeamertemplate{headline}{}

\definecolor{infoboxbg}{HTML}{f3e7ac}
\definecolor{infoboxborder}{HTML}{de9758}

\definecolor{alertboxbg}{HTML}{ffc6c7}
\definecolor{alertboxborder}{HTML}{ea2f61}

\newcommand{\cmark}{\color{OliveGreen}\ding{52}}
\newcommand{\xmark}{\color{BrickRed}\ding{56}}

%\let\tempone\itemize
%\let\temptwo\enditemize
%\renewenvironment{itemize}{\tempone\addtolength{\itemsep}{0.5\baselineskip}}{\temptwo}



\newcommand{\sectiontitleframe}{
    \begin{frame}
        \vfill
        \centering
        \begin{beamercolorbox}[sep=8pt,center,shadow=true,rounded=true]{title}
            \usebeamerfont{title}\insertsectionhead\par%
        \end{beamercolorbox}
        \vfill
\end{frame}}

\lstdefinelanguage{gdb}{
    morekeywords={gdb},
    sensitive=false,
}
\lstdefinelanguage{cfiasm}{
    morekeywords={cfi_startproc,cfi_def_cfa_offset,cfi_offset,cfi_def_cfa_register},
    sensitive=false,
}

\newcommand{\thenalert}[1]{\only<1>{#1}\only<2>{\alert{#1}}}
\newcommand{\slidecountline}{
    \ifthenelse{\theframenumber = 0}
        {}
        {\insertframenumber/\inserttotalframenumber}}

\setbeamertemplate{footline}
{
  \leavevmode%
  \hbox{%
      \hskip0.9\paperwidth
  %\begin{beamercolorbox}[wd=.4\paperwidth,ht=2.25ex,dp=1ex,center]{author in head/foot}%
  %  \usebeamerfont{author in head/foot}\insertshortauthor
  %\end{beamercolorbox}%
      \begin{beamercolorbox}[center, wd=.1\paperwidth,ht=2.25ex,dp=1ex,center]{title in head/foot}%
          \slidecountline{}
  \end{beamercolorbox}}%
  \vskip0pt%
}

\setbeamercolor{block title}{use=structure,fg=white,bg=structure.fg!75!black}
\setbeamercolor{block title alerted}{use=alerted text,fg=white,bg=alerted
text.fg!75!black}
\setbeamercolor{block title example}{use=example text,fg=white,bg=example
text.fg!75!black}

%\setbeamertemplate{frametitle}{
%  \leavevmode%
%  \hbox{%
%  \begin{beamercolorbox}[wd=\paperwidth,ht=2.25ex,dp=1ex,center]{title in head/foot}%
%    \usebeamerfont{author in head/foot}\insertframetitle
%  \end{beamercolorbox}%
%  }
%  \vskip0pt%
%    %\color{black}\bfseries\insertframetitle\par\vskip-6pt\hrulefill
%}


\newcolumntype{b}{X}
\newcolumntype{s}{>{\hsize=.43\hsize}X}

\newcommand{\lstinl}
{\lstinline[language=C, keepspaces=true, basicstyle=\ttfamily]}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title[] {Reliable and Fast DWARF-based Stack Unwinding}
\author[\slidecountline]{\alert{\textbf{Théophile Bastian}}\\
    \textbf{Stephen Kell} \\
\textbf{Francesco Zappa Nardelli}}
\date{}
%\subject{}
%\logo{}
\institute{ENS Paris, University of Kent, Inria}

\begin{document}

\begin{frame}
    \addtocounter{framenumber}{-1}
	\titlepage{}

    \vspace{-2em}


    \begin{columns}
        \begin{column}{0.55\textwidth}
            \begin{tcolorbox}[halign=center, colframe=blue]
                \textbf{Webpage} (incl. slides)

                \smallskip
                \vspace{0.5em}
                {\small\url{https://huit.re/frdwarf}}\\
                \vspace{0.5em}
            \end{tcolorbox}
        \end{column}

        \begin{column}{0.55\textwidth}
            \begin{tcolorbox}[colframe=blue]
                \begin{center}\textbf{Funding}\end{center}
                \vspace{-1em}

                \smallskip
                ONR VerticA \\
                Google Research Fellowship
            \end{tcolorbox}
        \end{column}
    \end{columns}

    \begin{textblock*}{0.22\textwidth}[0.5,0](0.15\paperwidth,0.38\paperheight)%
        \includegraphics[width=\linewidth]{img/stephen_circ.jpg}
    \end{textblock*}
    \begin{textblock*}{0.22\textwidth}[0.5,0](0.85\paperwidth,0.38\paperheight)%
        \includegraphics[width=\linewidth]{img/fzn_circ.jpg}
    \end{textblock*}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{DWARF and stack unwinding data}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Introduction}

\begin{frame}[fragile]{}
    \begin{columns}[c]
        \begin{column}{0.65\textwidth}
            \begin{lstlisting}[basicstyle=\tt,language=gdb, numbers=none, escapechar=|]
$ ./a.out
Segmentation fault.

|\pause|(gdb) backtrace
#0   |0x54625| in fct_b
#1   |\color{blue}0x54663| in fct_a
#2   |\color{red}0x54674| in main
            \end{lstlisting}
            \pause{}
            \begin{center}
                \textbf{\Large How does it work?}
            \end{center}
        \end{column}
        \hfill
        \begin{column}{0.35\textwidth}
        \end{column}
    \end{columns}

    \only<4->{
        \begin{textblock*}{0.35\textwidth}[1,0.5](0.9\paperwidth,0.5\paperheight)%
            \includegraphics[width=0.95\linewidth]{img/call_stack}
        \end{textblock*}
    }
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Stack frames and unwinding}

\begin{frame}
    \begin{columns}[c]
        \begin{column}{0.55\textwidth}
            \begin{center}
                \large\bf
                How do we get\\
                the return address?

                \vspace{2em}

                \onslide<2>{What if we only have \reg{rsp}?}

            \end{center}
        \end{column}
        \hfill
        \begin{column}{0.35\textwidth}
        \end{column}
    \end{columns}

    \begin{textblock*}{0.35\textwidth}[1,0.5](0.9\paperwidth,0.5\paperheight)%
        \includegraphics[width=0.95\linewidth]{img/call_stack}
    \end{textblock*}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{DWARF tables}

\newcolumntype{a}{>{\columncolor{RedOrange}}l}

\begin{frame}{DWARF unwinding data}
    \tt \footnotesize
    \begin{center}
        \begin{tabular}{
                >{\columncolor{YellowGreen}}l
                >{\columncolor{Thistle}}l
                l l l l l l
                >{\columncolor{Apricot}}l}
~PC & CFA & rbx & rbp & r12 & r13 & r14 & r15 & ra \\
0084950 & rsp+8 & u & u & u & u & u & u & c-8 \\
0084952 & rsp+16 & u & u & u & u & u & c-16 & c-8 \\
0084954 & rsp+24 & u & u & u & u & c-24 & c-16 & c-8 \\
0084956 & rsp+32 & u & u & u & c-32 & c-24 & c-16 & c-8 \\
0084958 & rsp+40 & u & u & c-40 & c-32 & c-24 & c-16 & c-8 \\
0084959 & rsp+48 & u & c-48 & c-40 & c-32 & c-24 & c-16 & c-8 \\
\rowcolor{Aquamarine} 008495a & rsp+56 & c-56 & c-48 & c-40 & c-32 & c-24 & c-16 & c-8 \\
0084962 & rsp+64 & c-56 & c-48 & c-40 & c-32 & c-24 & c-16 & c-8 \\
0084a19 & rsp+56 & c-56 & c-48 & c-40 & c-32 & c-24 & c-16 & c-8 \\
0084a1d & rsp+48 & c-56 & c-48 & c-40 & c-32 & c-24 & c-16 & c-8 \\
0084a1e & rsp+40 & c-56 & c-48 & c-40 & c-32 & c-24 & c-16 & c-8 \\
        \end{tabular}
    \end{center}

    \only<1>{\vspace{19mm}}
    \begin{columns}
        \begin{column}{0.50\textwidth}
            \onslide<2->{
                \begin{tcolorbox}[enhanced, halign=center, frame hidden, colback=YellowGreen]
                    \textbf{For each instruction\ldots}\\
                    (identified by its program counter)
                \end{tcolorbox}
            }
        \end{column}
        \begin{column}{0.50\textwidth}
            \onslide<3->{
                \begin{tcolorbox}[enhanced, halign=center, frame hidden,
                        interior style={right color=Apricot, left color=Thistle}]
                        \textbf{\ldots{}an expression to compute its return address
                        location on the stack}
                \end{tcolorbox}
            }
        \end{column}
    \end{columns}
\end{frame}

\begin{frame}[t, fragile]{The real DWARF}
    \begin{lstlisting}[numbers=none, language=]
30 24 34 FDE pc=004020..004040
  DW_CFA_def_cfa_offset: 16
  DW_CFA_advance_loc: 6 to 0000000000004026
  DW_CFA_def_cfa_offset: 24
  DW_CFA_advance_loc: 10 to 0000000000004030
  DW_CFA_def_cfa_expression (DW_OP_breg7 (rsp): 8; DW_OP_breg16 (rip): 0; DW_OP_lit15; DW_OP_and; DW_OP_lit11; DW_OP_ge; DW_OP_lit3; DW_OP_shl; DW_OP_plus)
  [...]
    \end{lstlisting}

    \pause{}
    \vfill

    \begin{itemize}
            \bf
        \item[\textbf{$\longrightarrow$}] \alert{bytecode} for a
            \alert{Turing-complete stack machine}
        \item[\textbf{$\longrightarrow$}] which is \alert{interpreted on
            demand at runtime}\\to reconstruct the table
    \end{itemize}
\end{frame}

\begin{frame}{What does this imply?}
    \begin{center}
        \textbf{Your compiler generates code for \alert{two machines}:\\
        your processor and the DWARF VM\@.}
    \end{center}

    \vfill{}
    \begin{columns}
        \begin{column}{0.45\textwidth}
            \begin{center}
                \begin{tikzpicture}
                    \begin{scope}[every node/.style={rectangle,thick,draw,scale=0.95}]
                        \node (cmd) at (0, 3.0) {
                            \lstbash{\$ gcc -S foo.c}
                        };
                        \node (asm) at (0, 0) {
                            \lstinputlisting[numbers=none, language=cfiasm]{src/main_cfi.s}
                        };
                    \end{scope}
                    \begin{scope}[>={Stealth[black]},
                        every path/.style={draw=black,very thick}]
                        \path [->] (cmd) -- (asm);
                    \end{scope}
                \end{tikzpicture}
                %\vspace{0.2em}

                \textbf{\lstc{.cfi_*}: \alert{inline DWARF!}}
            \end{center}
        \end{column}

        \pause{}

        \begin{column}{0.55\textwidth}
            \begin{itemize}
                \item[$\implies$] \alert{Cumbersome} to generate for the
                    \alert{compiler}
                    \begin{itemize}
                        \item[$\leadsto$] might do it wrong
                        \item[$\leadsto$] might not do it at all
                    \end{itemize}

                \item[$\implies$] If you write \alert{inline asm}, \alert{you} must write
                    inline DWARF\@!
            \end{itemize}

        \end{column}
    \end{columns}
    \vfill{}
\end{frame}

\begin{frame}
    \lstinputlisting[language=bash,numbers=none,basicstyle=\tt\fontsize{8pt}{9pt}\selectfont]{src/lowlevellock_dw_extr.c}

    \only<2>{
        \begin{textblock*}{0.60\textwidth}[0.5,0.5](0.5\paperwidth,0.5\paperheight)%
            \begin{tcolorbox}[halign=center, colframe=infoboxborder, colback=infoboxbg]
                In \prog{glibc}, \prog{lowlevellock.h}:
                \alert{off by one error in unwinding data}.

                \lstinputlisting[language=gdb,numbers=none]{src/lowlevellock_backtrace}
            \end{tcolorbox}
        \end{textblock*}
    }

    \only<3->{
        \begin{textblock*}{0.90\textwidth}[0.5,0](0.5\paperwidth,0.10\paperheight)%
            \begin{tcolorbox}[halign=center, colframe=alertboxborder, colback=alertboxbg]
                \bf \LARGE
                Complex \,\& \,slow
            \end{tcolorbox}
        \end{textblock*}
    }

    \only<4->{
        \begin{textblock*}{0.90\textwidth}[0.5,0](0.5\paperwidth,0.30\paperheight)%
            \begin{tcolorbox}[halign=center, colframe=alertboxborder, colback=alertboxbg]
                \LARGE
                \textbf{Pervasive:}\\ relied upon by profilers, debuggers,
                aaand\ldots{}
                \onslide<5->{
                    C++ exceptions. \\
                    \medskip{}
                \textbf{$\leadsto$ not only for debuggers!}}
            \end{tcolorbox}
        \end{textblock*}
    }
    \end{frame}

    \newcommand{\LinusMailOne}{
        ``Sorry, but last time was too f\dots painful. The whole (and
        only) point of unwinders is to make debugging easy
        when a bug occurs. But \alert{the dwarf unwinder had bugs}
        itself, or \alert{our dwarf information had bugs}, and in either
        case it actually turned several trivial bugs into a \alert{total
        undebuggable hell}.''
    }
    \newcommand{\LinusMailTwo}{
        ``If you can \alert{mathematically prove that the unwinder is
        correct} — even in the presence of bogus and actively
        incorrect unwinding information — and never ever
        follows a bad pointer, \alert{I’ll reconsider}.''
    }
    \newcommand{\LinusSource}{
        \hfill ---~Linus Torvalds, 2012
    }
    \begin{frame}
        \begin{columns}
            \begin{column}{0.75\textwidth}
                \LinusMailOne{}
            \end{column}
            \begin{column}{0.25\textwidth}
                \includegraphics[width=\textwidth]{img/roundtorvalds.png}
            \end{column}
        \end{columns}

        \only<1-2>{
            \vspace{1em}
            \LinusSource{}
        }

        \vspace{1em}
        \only<2>{
            \begin{center}
                \Large\bf
                \alert{This is where we still are!}
            \end{center}
        }

        \only<3>{
            \LinusMailTwo{}

            \vspace{1em}
            \LinusSource{}
        }
    \end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    \section{Correctness by construction:\\*\textbf{synthesis of unwinding tables}}
    \sectiontitleframe{}

    \newcommand{\tblrowval}[4]{#1 & #2 & \only<2->{#3} & \only<2->{#4} \\}
    \newcommand{\blknote}[1]
    {\begin{block}{}
            \centering\large
            #1
    \end{block}}
    \newcommand{\blklnote}[1]
    {\begin{block}{}
            \large
            #1
    \end{block}}
    \newcommand{\tblhl}{\rowcolor{Tan}}

    \begin{frame}
        \newcommand{\firsttblrows}{
            \tblrowval{\hspace{-2ex}<{\bf foo}>:}{}{\textbf{CFA}}{\textbf{ra}}
            \rowonly<4>{\tblhl{}}  \tblrowval{push}{\%r15}{rsp+8}{c-8}
            \rowonly<5>{\tblhl{}} \tblrowval{push}{\%r14}{rsp+16}{c-8}
            \rowonly<6>{\tblhl{}} \tblrowval{mov}{\$0x3,\%eax}{rsp+24}{c-8}
            \rowonly<7>{\tblhl{}} \tblrowval{push}{\%r13}{rsp+24}{c-8}
            \tblrowval{push}{\%r12}{rsp+32}{c-8}
            \tblrowval{push}{\%rbp}{rsp+40}{c-8}
            \tblrowval{push}{\%rbx}{rsp+48}{c-8}
            \tblrowval{sub}{\$0x68,\%rsp}{rsp+56}{c-8}
        }


        {\only<3>{
                \begin{textblock*}{\textwidth}[0.5,0.5](0.5\paperwidth,0.5\paperheight)%
                    \begin{tcolorbox}[halign=center, colframe=alertboxborder, colback=alertboxbg]
                        \large
                        \alert{\bf Assumptions}
                        \vspace{0.6em}
                        \begin{itemize}
                            \item the compiler generated the unwinding data
                            \item we have a reliable DWARF interpreter
                        \end{itemize}

                    \end{tcolorbox}
                \end{textblock*}
	}}
    \only<-9>{
        \begin{table}
            \ttfamily\large
            \begin{tabularx}{0.9\linewidth}{
                    l
                    b
                    >{\columncolor{SkyBlue}}s
                    >{\columncolor{SkyBlue}}s
                }
\firsttblrows{}%
\tblrowval{add}{\$0x68,\%rsp}{rsp+160}{c-8}
\tblrowval{pop}{\%rbx}{rsp+56}{c-8}
            \end{tabularx}
        \end{table}
        \blknote{
            \centering
        \begin{overlayarea}{0.9\textwidth}{2.6em}
            \only<4>{Upon function call, \alert{ra = *(\reg{rsp})}}
            \only<5>{\texttt{push} decreases \reg{rsp} by 8: %
                \alert{ra = *(\reg{rsp} + 8)}}
            \only<6>{and again: %
                \alert{ra = *(\reg{rsp} + 16)}}
            \only<7>{This \texttt{mov} leaves \reg{rsp} untouched: \\%
                \alert{ra = *(\reg{rsp} + 16)}}
            \only<8>{The unwinding table captures an \alert{abstract execution}
            of the code\ldots}
            \only<9>{\ldots and thus is \alert{redundant with the binary}.}
        \end{overlayarea}
    }
    }
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Unwinding data synthesis from binaries}

\begin{frame}{Synthesis strategy}
    \begin{itemize}
        \item Upon entering a function, we know
            \[ \cfa = \reg{rsp} - 8
            \qquad \ra = \cfa + 8 \]
        \item The semantics of each instruction specifies \alert{how it changes
            the \cfa}.
            \begin{itemize}
                \item Heuristic to decide whether we index with \reg{rbp} or
                    \reg{rsp}
            \end{itemize}
        \item With a \alert{symbolic execution} with an abstract semantics,\\
            we can \alert{synthesize the
            unwinding table} line by line.
        \item Control flow: forward data-flow analysis
        \item The fixpoints are immediate, cf article
    \end{itemize}

    \vspace{1em}
    \begin{tcolorbox}[halign=center, colframe=infoboxborder, colback=infoboxbg]
        \large
        Implemented on top of CMU's \prog{BAP}
    \end{tcolorbox}
\end{frame}

\begin{frame}{}
    \vfill
    \centering
    \begin{beamercolorbox}[sep=8pt,center,shadow=true,rounded=true]{title}
        \Large
        Demo time!
    \end{beamercolorbox}
    \vfill
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Unwinding data compilation}

\begin{frame}
    \begin{center}
        \Huge
        Unwinding data is
        \textsc{slo\pause{}o\pause{}o\pause{}o\pause{}o\pause{}o\pause{}o\pause{}o\pause{}w}.
    \end{center}
    \vspace{2em}

    \pause{}

    So much that \prog{perf} cannot unwind online!

    It must \alert{copy to disk the whole call stack} every few instants and
    \alert{analyze it later} at report time!
\end{frame}

\sectiontitleframe{}

\subsection{Compilation ahead-of-time}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[shrink]
    \vspace{0.5cm}
    \begin{tikzpicture}
        \begin{scope}[every node/.style={rectangle,thick,draw,scale=0.95}]
            \node (dwarf) at (0, 0) {
                \lstinputlisting[basicstyle=\tiny\tt,numbers=none,language=]{src/dw_plt_abbr}
            };

            \onslide<2->{
                \node (table) at (0.5\textwidth, -0.23\textheight) {
                    \tiny\tt
                    \begin{tabular}{
                            >{\columncolor{YellowGreen}}l
                            >{\columncolor{Thistle}}l
                            l l
                        >{\columncolor{Apricot}}l}
                        ~PC & CFA & rbx & rbp & ra \\
                        0084950 & rsp+8 & u & u & c-8 \\
                        0084952 & rsp+16 & u & u & c-8 \\
                        0084954 & rsp+24 & u & u & c-8 \\
                        0084956 & rsp+32 & u & u & c-8 \\
                    \end{tabular}
                };
            }
            \onslide<3->{
                \node (csrc) at (0, -0.6\textheight) {
                    \lstinputlisting[basicstyle=\tiny,numbers=none,language=C]{src/fib7/fib7.eh_elf_basic.c}
                };
                \node (ehelf) at (0.55\textwidth, -0.75\textheight) {
                    ELF file:
                    ``\ehelf{}''
                };
            }
        \end{scope}

        \begin{scope}[>={Stealth[black]},
                every node/.style={fill=white,rectangle},
                every path/.style={draw=black,very thick}]
            \only<2->{\path [->] (dwarf) -| node {runtime} (table);}
            \only<3->{
                \path [->] (dwarf) edge node {ahead of time} (csrc);
                \path [->] (csrc) -| node {gcc, AoT} (ehelf);
            }
        \end{scope}
    \end{tikzpicture}
\end{frame}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}
    \begin{itemize}
        \item \alert{libunwind}: most common library for
            unwinding

            \bigskip{}

        \item \alert{\texttt{libunwind-eh\_elf}}: modified version to support
            \ehelfs{}

        \item[$\leadsto$] Same API, almost \alert{``relink-and-play''} for existing projects!
    \end{itemize}
\end{frame}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Results}

\begin{frame}{Performances}
    \begin{center}
        \Large\bf Unwinding speedup vs.\ libunwind:
        \begin{tabular}{rl}
            \alert{x15} &on \prog{\tt{}perf gzip}\\
            \alert{x25} &on \prog{\tt{}perf hackbench}\\
        \end{tabular}
    \end{center}

    \vfill

    \begin{center}
        \Large\bf Space overhead vs. DWARF:\\
        \alert{x2.6 -- x3}
    \end{center}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section*{Conclusion}
\setcounter{section}{0}

\begin{frame}{}
    \vfill
    \centering
    \begin{beamercolorbox}[sep=8pt,center,shadow=true,rounded=true]{title}
        \Large
        What's next?
    \end{beamercolorbox}
    \vfill
\end{frame}

\begin{frame}{}
    \begin{itemize}
        \item{} Synthesis + compare = verification of unwinding data!
        \item{} Integrate synthesis into compilers \& debuggers\\
            $\rightarrow$ support for inline assembly, fallback method, \ldots
        \item{} Integrate into \prog{perf} for online unwinding
        \item{} Probably many more cool projects!
    \end{itemize}

    \vspace{1em}

    \begin{center}
        Come and chat if interested! \texttt{:)}
    \end{center}
\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section*{Extra slides}

\begin{frame}[noframenumbering]
\end{frame}

\begin{frame}[noframenumbering]{Fixpoint upon control flow merge}
    \begin{columns}
        \begin{column}{0.3\textwidth}
            \begin{tikzpicture}
                \begin{scope}[every node/.style={rectangle,thick,draw,scale=0.95}]
                    \node (if) at (0, 5) {\lstbash{if cnd}};
                    \node (then) at (-1, 3) { \lstbash{then A} };
                    \node (else) at (1, 3) { \lstbash{else B} };
                    \node (after) at (0, 1) { \lstbash{C} };
                \end{scope}
                \node [circle, thick, draw, minimum size=3em, color=red] (circafter) at (0, 1) {};
                \begin{scope}[>={Stealth[black]}, every path/.style={draw=black,very thick}]
                    \path [->] (if) -- (then);
                    \path [->] (if) -- (else);
                    \path [->] (then) -- (after);
                    \path [->] (else) -- (after);
                \end{scope}
            \end{tikzpicture}
        \end{column}
        \begin{column}{0.6\textwidth}
            \begin{center}
                If eg.
                \[
                    CFA(A) = c-48 \qquad CFA(B) = c-52
                \]
                no possible unwinding data for C, \alert{even for the
                compiler}!

                \vspace{1em}
                Also, \alert{no possible clean function postlude}!

                \vspace{2em}
                $\implies$ $CFA(A) = CFA(B)$ and merge is immediate
            \end{center}
        \end{column}
    \end{columns}
\end{frame}

\begin{frame}[noframenumbering]{Fixpoint upon loop control flow merge}
    \begin{columns}
        \begin{column}{0.3\textwidth}
            \begin{tikzpicture}
                \begin{scope}[every node/.style={rectangle,thick,draw,scale=0.95}]
                    \node (inbound) at (0, 7) {\lstbash{A}};
                    \node (while) at (0, 5) {\lstbash{for i in ...}};
                    \node (do) at (0, 3) { \lstbash{do a = array[i]; B} };
                    \node (done) at (0, 1) { \lstbash{C} };
                \end{scope}
                \node [ellipse, thick, draw, minimum width=10em, minimum height=3em, color=red] (circafter) at (0, 3) {};
                \begin{scope}[>={Stealth[black]}, every path/.style={draw=black,very thick}]
                    \path [->] (inbound) -- (while);
                    \path [->] (while) edge[bend right] (do);
                    \path [->] (do) -- (done);
                    \path [->] (do) edge[bend right] (while);
                \end{scope}
            \end{tikzpicture}
        \end{column}
        \begin{column}{0.6\textwidth}
            \begin{center}
                {\large\alert{Variable stack frame size!}}

                \vspace{1em}

                We cannot hope for a simple invariant\dots\\
                but the compiler cannot
                either.

                \vspace{1em}

                {
                    \large\alert{$\implies$} the compiler will\\
                        \alert{fallback to \reg{rbp}}\\
                }
                even with \lstbash{--fomit-frame-pointer}
            \end{center}
        \end{column}
    \end{columns}
\end{frame}

\end{document}