% !TEX program = xelatex\documentclass{article}\usepackage{../style}\usepackage{../langs}\usepackage{../graphics}\usepackage{../grammar}\begin{document}\fnote{\copyright{} Christian Urban, King's College London, 2019, 2023}% CPS translations% https://felleisen.org/matthias/4400-s20/lecture17.html%% pattern matching resources%% https://www.reddit.com/r/ProgrammingLanguages/comments/g1vno3/beginner_resources_for_compiling_pattern_matching/\section*{Handout 9 (LLVM, SSA and CPS)}Reflecting on our two tiny compilers targetting the JVM, the codegeneration part was actually not so hard, no? Pretty much just somepost-traversal of the abstract syntax tree, yes? One of the reasonsfor this ease is that the JVM is a stack-based virtual machine and itis therefore not hard to translate deeply-nested arithmeticexpressions into a sequence of instructions manipulating thestack. The problem is that ``real'' CPUs, although supporting stackoperations, are not really designed to be \emph{stack machines}. Thedesign of CPUs is more like: Here are some instructions and a chunk ofmemory---compiler, or better compiler writers, do something withthem. Consequently, modern compilers need to go the extra mile inorder to generate code that is much easier and faster to process byactual CPUs, rather than running code on virtual machines thatintroduce an additional layer of indirection. To make this alltractable for this module, we target the LLVM IntermediateLanguage. In this way we can take advantage of the tools coming withLLVM.\footnote{\url{http://llvm.org}} For example we do not have toworry about things like register allocations. By using the LLVM-IR,however, we also have to pay price in the sense that generating codegets harder\ldots{}unfor\-tunately.\subsection*{LLVM and the LLVM-IR}\noindent LLVM is a beautiful examplethat projects from Academia can make a difference in the World. LLVMstarted in 2000 as a project by two researchers at the University ofIllinois at Urbana-Champaign. At the time the behemoth of compilers wasgcc with its myriad of front-ends for different programming languages (C++, Fortran,Ada, Go, Objective-C, Pascal etc). The problem was that gcc morphed overtime into a monolithic gigantic piece of m\ldots ehm complicatedsoftware, which youcould not mess about in an afternoon. In contrast, LLVM is designed tobe a modular suite of tools with which you can play around easily andtry out something new. LLVM became a big player once Apple hired one ofthe original developers (I cannot remember the reason why Apple did notwant to use gcc, but maybe they were also just disgusted by gcc's bigmonolithic codebase). Anyway, LLVM is now the big player and gcc is moreor less legacy. This does not mean that programming languages like C andC++ are dying out any time soon---they are nicely supported by LLVM.We will target the LLVM Intermediate Language, or LLVM IntermediateRepresentation (short LLVM-IR). The LLVM-IR looks very similar to theassembly language of Jasmin and Krakatau. Targetting LLVM-IR will alsoallow us to benefit from the modular structure of the LLVM compilerand we can let the compiler generate code for different CPUs, forexample X86 or ARM. That means we can be agnostic about where ourcode is actually going to run.\footnote{Anybody want to try to run our programs on Android phones?} We can also be somewhat ignorant aboutoptimising our code and about allocating memory efficiently---the LLVMtools will take care of all this.However, what we have to do in order to make LLVM to play ball is togenerate code in \emph{Static Single-Assignment} format (short SSA). Areason why LLVM uses the SSA-format, rather than JVM-like stackinstructions, is that stack instructions are difficult tooptimise---you cannot just re-arrange instructions without messingabout with what is calculated on the stack. Also it is hard to findout if all the calculations on the stack are actually necessary andnot by chance dead code. The JVM has for all these obstaclessophisticated machinery to make such ``high-level'' code still runfast, but let's say that for the sake of argument we do not want torely on it. We want to generate fast code ourselves. This means wehave to work around the intricacies of what instructions CPUs canactually process fast. This is what the SSA format is designed for.The main idea behind the SSA-format is to have sequences of verysimple variable assignments where every (tmp)variable is assigned onlyonce. The assignments need to be simple in the sense that they can bejust be primitive operations like addition, multiplication, jumps,comparisons, function calls and so on. Say, we have an expression$((1 + a) + (foo(3 + 2) + (b * 5)))$, then the corresponding sequenceof assignments in SSA-format are:\begin{lstlisting}[language=LLVMIR,numbers=left]let tmp0 = add 1 a inlet tmp1 = add 3 2 in let tmp2 = call foo(tmp1) let tmp3 = mul b 5 in let tmp4 = add tmp2 tmp3 in let tmp5 = add tmp0 tmp4 in return tmp5 \end{lstlisting}\noindent where every tmpX-variable is used only once (we could, forexample, not write \texttt{tmp1 = add tmp2 tmp3} in Line 5 even ifthis would not change the overall result). At the end we have areturn-instruction wich contains the final result of theexpression. As can be seen, the task we have to solve is to take apartcompound expressions as shown above and transfrom them into a sequenceof simple assignments. Note that this for example means we have tofix the order in which the expression is calculated. There are sophisticated algorithms for imperative languages, like C,that efficiently transform high-level programs into SSA-format. Butwe can ignore them here. We want to compile a functional language andthere things get much more interesting than just sophisticated. Wewill need to have a look at CPS translations, where the CPS stands for\emph{Continuation-Passing-Style}---basically black programming art orabracadabra programming. So sit tight.\subsection*{LLVM-IR}Before we start, let's however first have a look at the \emph{LLVM IntermediateRepresentation} in more detail. The LLVM-IR is in between the frontendsand backends of the LLVM framework. It allows compilation of multiplesource languages to multiple targets. It is also the place where most ofthe target independent optimisations are performed. What is good about our toy Fun-language is that it basically onlycontains expressions (be they arithmetic expressions, booleanexpressions or if-expressions). The exception are function definitions.Luckily, for them we can use the mechanism of defining functions in theLLVM-IR (this is similar to using JVM methods for functions in ourearlier compiler). For example the simple Fun-program \begin{lstlisting}[language=Scala,numbers=none]def sqr(x) = x * x\end{lstlisting}\noindentcan be compiled to the following LLVM-IR function:\begin{lstlisting}[language=LLVM]define i32 @sqr(i32 %x) { %tmp = mul i32 %x, %x ret i32 %tmp} \end{lstlisting}\noindent First notice that all ``local'' variable names, in this case\texttt{x} and \texttt{tmp}, are prefixed with \texttt{\%} in theLLVM-IR. Temporary variables can be named with an identifier, such as\texttt{tmp}, or numbers. In contrast, function names, since they are``global'', need to be prefixed with an @-symbol. Also, the LLVM-IR isa fully typed language. The \texttt{i32} type stands for 32-bitintegers. There are also types for 64-bit integers (\texttt{i64}),chars (\texttt{i8}), floats, arrays and even pointer types. In thecode above, \texttt{sqr} takes an argument of type \texttt{i32} andproduces a result of type \texttt{i32} (the result type is in front ofthe function name, like in C). Each arithmetic operation, for exampleaddition and multiplication, are also prefixed with the type theyoperate on. Obviously these types need to match up\ldots{} but sincewe have in our programs only integers, for the moment \texttt{i32}everywhere will do. We do not have to generate any other types, butobviously this is a limitation in our Fun-language (and which weare going to lift in the final CW).There are a few interesting instructions in the LLVM-IR which are quitedifferent than what we have seen in the JVM. Can you remember thekerfuffle we had to go through with boolean expressions and negating thecondition? In the LLVM-IR, branching if-conditions are implementeddifferently: there is a separate \texttt{br}-instruction as follows:\begin{lstlisting}[language=LLVM]br i1 %var, label %if_br, label %else_br\end{lstlisting}\noindentThe type \texttt{i1} stands for booleans. If the variable is true,then this instruction jumps to the if-branch, which needs an explicitlabel; otherwise it jumps to the else-branch, again with its ownlabel. This allows us to keep the meaning of the boolean expression``as is'' when compiling if's---thanks god no more negating ofbooleans.A value of type boolean is generated in the LLVM-IR by the\texttt{icmp}-instruction. This instruction is for integers (hence the\texttt{i}) and takes the comparison operation as argument. For example\begin{lstlisting}[language=LLVM]icmp eq i32 %x, %y ; for equalicmp sle i32 %x, %y ; signed less or equalicmp slt i32 %x, %y ; signed less thanicmp ult i32 %x, %y ; unsigned less than \end{lstlisting}\noindentNote that in some operations the LLVM-IR distinguishes between signed and unsigned representations of integers. I assume you know what this means,otherwise just ask.It is also easy to call another function in LLVM-IR: as can be seen from Figure~\ref{lli} we can just call a function with the instruction \texttt{call} and can also assign the result to a variable. The syntax is as follows\begin{lstlisting}[language=LLVM]%var = call i32 @foo(...args...)\end{lstlisting}\noindentwhere the arguments can only be simple variables and numbers, but not compoundexpressions.Conveniently, you can use the program \texttt{lli}, which comes withLLVM, to interpret programs written in the LLVM-IR. Type on the command line\begin{lstlisting}[language=bash,numbers=none]lli sqr.ll\end{lstlisting}\noindentand you can see the output of the pragram generated. This means you can easily check whether the code you produced actuallyworks. To get a running program that does something interesting youneed to add some boilerplate about printing out numbers and amain-function that is the entry point for the program (seeFigure~\ref{lli} for a complete listing of the square function). Againthis is very similar to the boilerplate we needed to add in our JVMcompiler.You can generate a binary for the program in Figure~\ref{lli} by usingthe \texttt{llc}-compiler and then \texttt{gcc}/\texttt{clang}, whereby \texttt{llc} generatesan object file and \texttt{gcc} (that is actually \texttt{clang} on my Mac) generates theexecutable binary:\begin{lstlisting}[language=bash,numbers=none]llc -filetype=obj sqr.llgcc sqr.o -o a.out./a.out> 25\end{lstlisting}\begin{figure}[t]\small \lstinputlisting[language=LLVM,numbers=left]{../progs/sqr.ll}\caption{An LLVM-IR program for calculating the square function. It calls the \texttt{sqr}-function in \texttt{@main} with the argument \texttt{5} (Line 20). The code for the \texttt{sqr}-function is in Lines 13 -- 16. The main-function stores the result of sqr in the variable called \texttt{\%1} and then prints out the contents of this variable in Line 21. The other code is boilerplate for printing out integers.\label{lli}}\end{figure} \subsection*{Our Own Intermediate Language}Let's get back to our compiler: Remember compilers have to solve theproblem of bridging the gap between ``high-level'' programs and``low-level'' hardware. If the gap is too wide for one step, then agood strategy is to lay a stepping stone somewhere in between. TheLLVM-IR itself is such a stepping stone to make the task of generatingand optimising code easier. Like a real compiler we will use our ownstepping stone which I call the \emph{K-language}.\begin{center} \begin{tikzpicture}[scale=0.9,font=\bf, node/.style={ rectangle,rounded corners=3mm, ultra thick,draw=black!50,minimum height=16mm, minimum width=20mm, top color=white,bottom color=black!20}] %\node (0) at (-3,0) {}; \node (A) at (0.0,0) [node,text width=1.6cm,text centered,label=above:{\small\it{}source}] {Fun-Language}; \node (B) at (3.5,0) [node,text width=1.6cm,text centered,label=above:{\small\it{}stepping stone}] {K-Language}; \node (C) at (7.0,0) [node,text width=1.6cm,text centered,label=above:{\small\it{}target}] {LLVM-IR}; \draw [->,line width=2.5mm] (A) -- node [above,pos=0.35] {} (B); \draw [->,line width=2.5mm] (B) -- node [above,pos=0.35] {} (C); \end{tikzpicture} \end{center} \noindent To see why we need a stepping stone for generating code in SSA-format, considder again arithmetic expressions such as $((1 + a) + (3 + (b * 5)))$. They need to be broken up into smaller ``atomic'' steps, like so\begin{lstlisting}[language=LLVMIR,numbers=none]let tmp0 = add 1 a in let tmp1 = mul b 5 in let tmp2 = add 3 tmp1 in let tmp3 = add tmp0 tmp2 in return tmp3 \end{lstlisting}\noindentHere \texttt{tmp3} will contain the result of what the wholeexpression stands for. In each individual step we can only perform an``atomic'' or ``trival'' operation, like addition or multiplication ofa number or a variable. We are not allowed to have for example anested addition or an if-condition on the right-hand side of anassignment. Such constraints are forced upon us because of how theSSA-format works in the LLVM-IR. To simplify matters we representassignments with two kinds of syntactic entities, namely\emph{K-values} and \emph{K-expressions}. K-values are all ``things''that can appear on the right-hand side of an equal. Say we have thefollowing definition for K-values:\begin{lstlisting}[language=Scala,numbers=none]enum KVal { case KVar(s: String) case KNum(n: Int) case KAop(op: String, v1: KVal, v2: KVal) case KCall(fname: String, args: List[KVal])}\end{lstlisting}\noindentwhere a K-value can be a variable, a number or a ``trivial'' binaryoperation, such as addition or multiplication. The two arguments of abinary operation need to be K-values as well. Finally, we havefunction calls, but again each argument of the function call needs tobe a K-value. One constraint we need to be careful about is that thearguments of the binary operations and function calls can only bevariables or numbers. For example\begin{lstlisting}[language=Scala,numbers=none]KAop("+", KAop("*", KNum(1), KNum(2)), KNum(3))KCall("foo", List(KAop("+", KNum(4), KNum(5))) \end{lstlisting}\noindentwhile perfect instances of K-values according to the types, are notallowed in the LLVM-IR. To encode this constraint into the type-systemof Scala, however, would make things overly complicated---to satisfythis constraint is therefore on us. For the moment this will be allK-values we are considdering. Later on, we will have some more for ourFun-language.Our K-expressions will encode the \texttt{let} and the \texttt{return}from the SSA-format (again for the moment we only consider these twoconstructors---later on we will have if-branches as well).\begin{lstlisting}[language=Scala,numbers=none]enum KExp { case KLet(x: String, v: KVal, e: KExp) case KReturn(v: KVal)}\end{lstlisting}\noindentBy having in \texttt{KLet} taking first a string (standing for atmp-variable) and second a value, we can fulfil the SSA constraint inassignments ``by con\-struction''---there is no way we could writeanything else than a K-value. Note that the third argument of a\texttt{KLet} is again a K-expression, meaning either another\texttt{KLet} or a \texttt{KReturn}. In this way we can construct asequence of computations and indicate what is the final result of thecomputations. According to the SSA-format, we also have to ensurethat all intermediary computations are given (fresh) names---we willuse an (ugly) counter for this.To sum up, K-values are the atomic operations that can be on theright-hand side of assignemnts. The K-language is restricted such thatit is easy to generate the SSA-format for the LLVM-IR. What remains tobe done is a translation of our Fun-language into the K-language. Themain difficulty is that we need to order the computation---in theK-language we only have linear sequence of instructions. Before weexplain this, we have a look at some programs in CPS-style.\subsection*{CPS-Translations}CPS stands for \emph{Continuation-Passing-Style}. It is a kind ofprogramming technique often used in advanced functional programmingand in particular in compilers. Before we delve into theCPS-translation for our Fun-language compiler, let us look atCPS-versions of some well-known functions. Consider\begin{lstlisting}[language=Scala, numbers=none]def fact(n: Int) : Int = if (n == 0) 1 else n * fact(n - 1) \end{lstlisting}\noindent This is clearly the usual factorial function. But now consider thefollowing slight variant of the factorial function:\begin{lstlisting}[language=Scala, numbers=left]def factC(n: Int, k: Int => Int) : Int = if (n == 0) k(1) else factC(n - 1, x => k(n * x)) factC(3, id)\end{lstlisting}\noindentThe function is is Lines 1--3. The function call is in Line 5. Wecall this function with a number, in this case 3, and theidentity-function (which returns just its input). The \texttt{k} isthe continuation in this function. The recursive calls are:\begin{lstlisting}[language=Scala, numbers=none]factC(2, x => id(3 * x))factC(1, x => id(3 * (2 * x)))factC(0, x => id(3 * (2 * (1 * x))))\end{lstlisting}\noindentHaving reached 0, we get out of the recursion and apply 1 to thecontinuation (see if-branch above in Line 2). This gives\begin{lstlisting}[language=Scala, numbers=none]id(3 * (2 * (1 * 1)))= 3 * (2 * (1 * 1))= 6\end{lstlisting}\noindentwhich is the expected result. If this looks somewhat familiar to you,than this is because functions with continuations can be seen as akind of generalisation of tail-recursive functions. So far, however,we did not look at this generalisation in earnest. Anyway notice howthe continuations is ``stacked up'' during the recursion and then``unrolled'' when we apply 1 to the continuation. Interestingly, wecan do something similar to the Fibonacci function where in thetraditional version we have two recursive calls. Consider thefollowing function\begin{lstlisting}[language=Scala, numbers=left]def fibC(n: Int, k: Int => Int) : Int = if (n == 0 || n == 1) k(1) else fibC(n - 1, r1 => fibC(n - 2, r2 => k(r1 + r2)))\end{lstlisting}\noindentHere the continuation (Lines 4--5) is a nested function essentially wrapping up the second recursive call plus the original continuation. Let us check how the recursion unfoldswhen called with 3 and the identity function:\begin{lstlisting}[language=Scala, numbers=none]fibC(3, id)fibC(2, r1 => fibC(1, r2 => id(r1 + r2)))fibC(1, r1 => fibC(0, r2 => fibC(1, r2a => id((r1 + r2) + r2a))))fibC(0, r2 => fibC(1, r2a => id((1 + r2) + r2a)))fibC(1, r2a => id((1 + 1) + r2a))id((1 + 1) + 1)(1 + 1) + 13\end{lstlisting}\noindentThe point of this section is that you should be playing around with thesesimple definitions and make sure they calculate the expected result.In the next step, you should understand \emph{how} these functionscalculate the result with the continuations. Now change the initialcontinuation which you call the function to\begin{lstlisting}[language=Scala, numbers=none]r => { println("The result plus 1 is:") ; r + 1 }\end{lstlisting}\noindentDoes this still calculate the expected result?\section*{Worked Example}Let us now come back to the CPS-translations for the Fun-language.Though we will start with a simpler subset containing only numbers,arithmetic expressions and function calls. The main difficulty ofgenerating instructions in SSA-format is that large compoundexpressions need to be broken up into smaller pieces and intermediateresults need to be chained into later instructions. To do thisconveniently, we use the CPS-translation mechanism. What continuationsessentially solve is the following problem: Given an expressions\begin{equation}\label{exp}(1 + 2) * (3 + 4)\end{equation} \noindentwhich of the subexpressions should be calculated first? We justarbitrarily going to decide that the calculation will be from left toright. Other languages make different choices---C famously is right toleft. In our case this means we have to tear the expression shown in\eqref{exp} apart as follows:\[(1 + 2) \qquad\text{and}\qquad \Box * (3 + 4)\] \noindentThe first subexpression can be easily calculated and will give us a result,but the second one is not really an expression that makes sense. Itwill only make sense as the next step in the computation when wefill-in the result of $1+2$ into the ``hole'' indicated by$\Box$. Such incomplete expressions can be represented in Scala asfunctions\begin{lstlisting}[language=Scala, numbers=none]r => r * (3 + 4)\end{lstlisting} \noindentwhere \texttt{r} will represent any result that has been computedearlier. By the way, in lambda-calculus notation we would write$\lambda r.\, r * (3 + 4)$ for the same function. To sum up, we usefunctions (``continuations'') to represent what is coming next in asequence of instructions. In our case, continuations are functions oftype \code{KVal} to \code{KExp}. They can be seen as a sequence of\code{KLet}s where there is a ``hole'' that needs to befilled. Consider for example\begin{lstlisting}[language=LLVMIR,numbers=left,escapeinside={(*@}{@*)}]let tmp0 = add 1 a in let tmp1 = mul (*@$\Box$@*) 5 in let tmp2 = add 3 tmp1 in let tmp3 = add tmp0 tmp2 in return tmp3 \end{lstlisting}\noindentwhere in the second line is a $\Box$ which still expects a \code{KVal}to be filled in before it becomes a ``proper'' \code{KExp}. When we apply an argument to the continuation (remember they are functions)we essentially fill something into the corresponding hole.Lets look at some concrete code. To simplify matters, suppose our source language consists just of three kinds of expressions\begin{lstlisting}[language=Scala,numbers=none]enum Expr { case Num(n: Int) case Aop(op: String, e1: Expr, e2: Expr) case Call(fname: String, args: List[Expr])}\end{lstlisting}\noindentThis allows us to generate SSA-instructions for expressions like\[1 + foo(bar(4 * 7), 3, id(12)) \]\noindentThe code of the CPS-translationthat generates these instructions is then of the form\begin{lstlisting}[language=Scala,numbers=none]def CPS(e: Exp)(k: KVal => KExp) : KExp = e match { ... }\end{lstlisting}\noindent where \code{k} is the continuation and \code{e} is the expression tobe compiled. The result of the function is a K-expression, which latercan be compiled into LLVM-IR code.In case we have numbers, then we can just pass them in CPS-translationto the continuations because numbers need not be further teared apartas they are already primitive. Passing the number to the continuationmeans we apply the continuation like\begin{lstlisting}[language=Scala,numbers=none] case Num(i) => k(KNum(i))\end{lstlisting}\noindent This would fill in the $\Box$ in a \code{KLet}-expression.Since \texttt{k} is a function from \texttt{KVar} to \texttt{KExp} wealso optain the correct type for CPS, namely \texttt{KExp}. There isno need to create a temporary variable for simple numbers. Moreinteresting is the case for arithmetic operations.\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=0mm]case Aop(op, e1, e2) => { val z = Fresh("tmp") CPS(e1)(r1 => CPS(e2)(r2 => KLet(z, KAop(op, r1, r2), k(KVar(z)))))}\end{lstlisting}\noindentWhat we essentially have to do in this case is the following: compilethe subexpressions \texttt{e1} and \texttt{e2}. They will produce someresult that is stored in two temporary variables (assuming they are morecomplicated than just numbers). We need to use these two temporaryvariables and feed them into a new assignment of the form\begin{lstlisting}[language=LLVMIR,numbers=none,escapeinside={(*@}{@*)}]let z = op (*@$\Box_\texttt{r1}$@*) (*@$\Box_\texttt{r2}$@*) in...\end{lstlisting}\noindentNote that this assignment has two ``holes'', one for the leftsubexpression and one for the right subexpression. We can fill bothholes by calling the CPS function twice---this is a bit of the blackart in CPS. We can use the second call of CPS as the continuationof the first call. The reason is that\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=0mm]r1 => CPS(e2)(r2 => KLet(z, KAop(op, r1, r2), k(KVar(z))))\end{lstlisting}\noindent is a function from \code{KVal} to \code{KExp}, which we needas type for the continuation. Once we created the assignment with thefresh temporary variable \texttt{z}, we need to ``communicate'' thatthe result of the computation of the arithmetic expression is storedin \texttt{z} to the computations that follow. In this way we applythe continuation \texttt{k} with this new variable (essentially we areplugging in a hole further down the line). Hope this makes sense.The last case we need to consider in our small expression language arefunction calls. For them remember each argument of the functioncall can in SSA-format only be a variable or a number.\begin{lstlisting}[language=Scala,numbers=left,xleftmargin=0mm]case Call(fname, args) => { def aux(args: List[Expr], vs: List[KVal]): KExp = args match { case Nil => { val z = Fresh("tmp") KLet(z, KCall(fname, vs), k(KVar(z))) } case a::as => CPS(a)(r => aux(as, vs ::: List(r))) } aux(args, Nil) }\end{lstlisting}\noindentFor this case we introduce an auxiliary function that compiles first allfunction arguments---remember in our source language we can have callssuch as $foo(3 + 4, g(3))$ where we first have to create temporaryvariables (and computations) for each argument. Therefore \texttt{aux}analyses the argument list from left to right. In case there is anargument \texttt{a} on the front of the list (the case \texttt{a::as}in Line 7), we call CPS recursively for the correspondingsubexpression. The temporary variable containing the result for thisargument we add to the end of the K-values we have already analysedbefore. Again very conveniently we can use the recursive call to\texttt{aux} as the continuation for the computations thatfollow. When we reach the end of the argument list (the\texttt{Nil}-case in Lines 3--6), then we collect all the K-values\texttt{v1} to \texttt{vn} and call the function in the K-languagelike so\begin{lstlisting}[language=LLVMIR,numbers=none,escapeinside={(*@}{@*)}]let z = call foo(v1,...,vn) in...\end{lstlisting}\noindentAgain we need to communicate the result of the function call, namely thefresh temporary variable \texttt{z}, to the rest of the computation. Thereforewe apply the continuation \texttt{k} with this variable.\begin{figure}[p]\small \lstinputlisting[numbers=left,firstline=1,lastline=24]{../progs/fun/simple-cps.sc} \hspace{10mm}... \lstinputlisting[numbers=left,firstline=32,firstnumber=32,lastline=51]{../progs/fun/simple-cps.sc}\caption{CPS-translation for a simple expression language.\label{cps}}\end{figure}The last question we need to answer in the code (see Figure~\ref{cps})is how we start the CPS-translation function, or more precisely withwhich continuation we should start CPS? It turns out that this initialcontinuation will be the last one that is called. What should be thelast step in the computation? Yes, we need to return the temporaryvariable where the last result is stored (if it is a simple number,then we can just return this number). Therefore we call CPS with thecode\begin{lstlisting}[language=Scala,numbers=none]def CPSi(e: Expr) : KExp = CPS(e)(KReturn(_))\end{lstlisting}\noindentwhere we give the function \code{KReturn(_)} as the continuation. Withthis we completed the translation of simple expressions into ourK-language. Play around with some more expressions and see how theCPS-translation generates the correct code. I know this is not easy tofollow code when you see it the first time. Figure~\ref{absfun} givesthe complete datatypes for the ASTs of the Fun-language and theK-values and K-expressions for the K-language. The completeCPS-translation you can find in the code.\section*{Next Steps}Having obtained a K-expression, it is relatively straightforward togenerate a valid program for the LLVM-IR. We leave this to theattentive reader. What else can we do? Well it should be relativelyeasy to apply some common optimisations to the K-expressions. Oneoptimisations is called constant folding---for example if we have anexpression $3 + 4$ then we can replace it by just $5$ instead ofgenerating code to compute $5$. Now this information needs to bepropagated to the next computation step to see whether any furtherconstant foldings are possible. Another useful technique is commonsubexpression elimination, meaning if you have twice a calculation ofa function $foo(a)$, then we want to call it only once and store theresult in a temporary variable that can be used instead of the second,or third, call to $foo(a)$. Again I leave this to the attentive readerto work out and implement.\begin{figure}[p]\small\begin{lstlisting}[language=Scala,numbers=none]// Fun language (expressions)abstract class Exp abstract class BExp case class Call(name: String, args: List[Exp]) extends Expcase class If(a: BExp, e1: Exp, e2: Exp) extends Expcase class Write(e: Exp) extends Expcase class Var(s: String) extends Expcase class Num(i: Int) extends Expcase class Aop(o: String, a1: Exp, a2: Exp) extends Expcase class Sequence(e1: Exp, e2: Exp) extends Expcase class Bop(o: String, a1: Exp, a2: Exp) extends BExp // K-language (K-expressions, K-values)abstract class KExpabstract class KValcase class KVar(s: String) extends KValcase class KNum(i: Int) extends KValcase class Kop(o: String, v1: KVal, v2: KVal) extends KValcase class KCall(o: String, vrs: List[KVal]) extends KValcase class KWrite(v: KVal) extends KValcase class KIf(x1: String, e1: KExp, e2: KExp) extends KExpcase class KLet(x: String, v: KVal, e: KExp) extends KExpcase class KReturn(v: KVal) extends KExp\end{lstlisting}\caption{Abstract syntax trees for the Fun-language and the K-language.\label{absfun}}\end{figure}\noindent\end{document}%%% Local Variables: %%% mode: latex%%% TeX-master: t%%% End: