\documentclass[11pt]{article}

\usepackage{homework}
\usepackage{proof}
\usepackage{amsmath}
\setlength{\inferLineSkip}{4pt}
\newcommand{\wild}{\mbox{\tt\char"5F}}

\newcommand{\assdate}{Thursday, October 29, 2015 (23:00pm)}
\newcommand{\assnum}{4}
\newcommand{\asstitle}{Semantics}
\newcommand{\lecturer}{Rob Simmons \\ Will Crichton, Grant Della Silva, Matt Bryant, Anshu Bansal}

\newcommand{\semi}{;}
\newcommand{\stepsto}{\rightarrow}
\newcommand{\uscore}{\rule{1.2ex}{.5pt}}
\newcommand{\comma}{,}
\newcommand{\m}[1]{\texttt{#1}}
\newcommand{\logand}{\texttt{\&\&}}
\newcommand{\brhd}{\blacktriangleright}

\begin{document}
\maketitle

\noindent\textbf{Reminder:} Assignments are individual assignments,
not done in pairs.  The work must be all your own.
Please hand in your solution electronically in PDF format and refer to
the late policy for written assignments on the course web pages.

\section*{Problem 1: Generalized Ifs (15 points)}

In this problem, assume we're using a subset of the restricted abstract syntax used in lecture, and the corresponding statics and dynamics.
For your convenience, these are reproduced below.

\subsection*{Language}

\[\begin{array}{llcl}
\mbox{Operators} & \oplus & {::=} & + \mid < \\[1ex]
\mbox{Expressions} & e & {::=} & n \mid x \mid e_1 \oplus e_2 \mid e_1 \logand e_2 \\[1ex]
\mbox{Statements} & s & {::=} & \m{assign}(x,e) \mid \m{if}(e, s_1, s_2) \mid \m{while}(e,s) \\
& & & \mid \m{return}(e) \mid \m{nop} \mid \m{seq}(s_1,s_2) \mid \m{decl}(x, \tau, s)
\end{array}\]

\subsection*{Statics}

\[\begin{array}{c}
\infer{\Gamma \vdash x : \tau}
      {\Gamma(x) = \tau}
\hspace{2em}
\infer{\Gamma \vdash n : \m{int}}
      {\mathstrut}
\hspace{2em}
\infer{\Gamma \vdash \m{true} : \m{bool}}
      {\mathstrut}
\hspace{2em}
\infer{\Gamma \vdash \m{false} : \m{bool}}
      {\mathstrut}
\\[1em]
\infer{\Gamma \vdash e_1 + e_2 : \m{int}}
      {\Gamma \vdash e_1 : \m{int} &
        \Gamma \vdash e_2 : \m{int}}
\hspace{3em}
\infer{\Gamma \vdash e_1 < e_2 : \m{bool}}
      {\Gamma \vdash e_1 : \m{int} &
        \Gamma \vdash e_2 : \m{int}}
\hspace{3em}
\infer{\Gamma \vdash e_1 \logand e_2 : \m{bool}}
      {\Gamma \vdash e_1 : \m{bool} &
        \Gamma \vdash e_2 : \m{bool}}
\end{array}\]

\[\begin{array}{c}
\infer{\Gamma \vdash \m{assign}(x,e) : [\tau]}
      {\Gamma(x) = \tau' & \Gamma \vdash e : \tau'}
\hspace{3em}
\infer{\Gamma \vdash \m{if}(e, s_1, s_2) : [\tau]}
      {\Gamma \vdash e : \m{bool} &
        \Gamma \vdash s_1 : [\tau] &
        \Gamma \vdash s_2 : [\tau]}
\\[1em]
\infer{\Gamma \vdash \m{while(e, s)} : [\tau]}
      {\Gamma \vdash e : \m{bool} &
       \Gamma \vdash s : [\tau]}
\hspace{3em}
\infer{\Gamma \vdash \m{return}(e) : [\tau]}
      {\Gamma \vdash e : \tau}
\\[1em]
\infer{\Gamma \vdash \m{nop} : [\tau]}
      {\mathstrut}
\hspace{3em}
\infer{\Gamma \vdash \m{seq}(s_1, s_2) : [\tau]}
      {\Gamma \vdash s_1 : [\tau] &
        \Gamma \vdash s_2 : [\tau]}
\\[1em]
\infer{\Gamma \vdash \m{decl}(x, \tau', s) : [\tau]}
      {\Gamma, x{:}\tau' \vdash s : [\tau]}
\end{array}\]

\subsection*{Dynamics}

\[
\begin{array}{lcll}
\eta \vdash e_1 \oplus e_2 \rhd K &
\stepsto &
\eta \vdash e_1 \rhd (\uscore \oplus e_2 \comma K) \\
\eta \vdash c_1 \rhd (\uscore \oplus e_2 \comma K) &
\stepsto &
\eta \vdash e_2 \rhd (c_1 \oplus \uscore \comma K) \\
\eta \vdash c_2 \rhd (c_1 \oplus \uscore \comma K) &
\stepsto &
\eta \vdash c \rhd K \qquad (c = c_1 \oplus c_2) \\[1em]

\eta \vdash e_1 \logand e_2 \rhd K &
\stepsto &
\eta \vdash e_1 \rhd (\uscore \logand e_2 \comma K) \\
\eta \vdash \m{false} \rhd (\uscore \logand e_2 \comma K) &
\stepsto &
\eta \vdash \m{false} \rhd K \\
\eta \vdash \m{true} \rhd (\uscore \logand e_2 \comma K) &
\stepsto &
\eta \vdash e_2 \rhd K \\[1em]

\eta \vdash x \rhd K &
\stepsto &
\eta \vdash \eta(x) \rhd K \\[1em]

\eta \vdash \m{assign}(x,e) \brhd K &
\stepsto &
\eta \vdash e \rhd (\m{assign}(x,\uscore) \comma K) \\
\eta \vdash c \rhd (\m{assign}(x,\uscore) \comma K)
& \stepsto &
\eta[x \mapsto c] \vdash \m{nop} \brhd K \\[1em]

\eta \vdash \m{decl}(x, \tau, s) \brhd K &
\stepsto &
\eta[x\mapsto\m{nothing}] \vdash s \brhd K \\[1em]

\eta \vdash \m{if}(e, s_1, s_2) \brhd K & \stepsto & \eta \vdash e \rhd (\m{if}(\uscore, s_1, s_2) \comma K) \\
\eta \vdash \m{true} \rhd (\m{if}(\uscore, s_1, s_2), K) & \stepsto & \eta \vdash s_1 \brhd K \\
\eta \vdash \m{false} \rhd (\m{if}(\uscore, s_1, s_2), K) & \stepsto & \eta \vdash s_2 \brhd K \\[1em]

\eta \vdash \m{while}(e, s) \brhd K & \stepsto & \eta \vdash \m{if}(e, \m{seq}(s, \m{while}(e, s)), \m{nop}) \brhd K \\[1em]

\eta \vdash \m{return}(e) \brhd K &
\stepsto &
\eta \vdash e \rhd (\m{return}(\uscore) \comma K) \\
\eta \vdash v \rhd (\m{return}(\uscore) \comma K) &
\stepsto &
\m{value}(v)
\end{array}
\]
Thinking about C, Anshu realizes how convenient it would be to have conditionals operate on any type by
implicitly casting them to booleans.
For example, we would expect the code fragment
\begin{verbatim}
if (7) { do_something_fun(); }
else { do_something_not_fun(); }
\end{verbatim}
to call \verb'do_something_fun()' in C, as 7 is non-zero.
However, in C0 we only have a judgement for when the expression being compared upon is a boolean.
To solve this problem, Anshu adds a new typing rule
\[
	\infer{\Gamma \vdash \mathtt{if}(e, s_1, s_2) : [\tau]}
	{\Gamma \vdash e : \mathtt{int} & \Gamma \vdash s_1 : [\tau] & \Gamma \vdash s_2 : [\tau]}
\]
However, when he compiles a small program using the feature and tries to run it, his program refuses to terminate.
\begin{verbatim}
if (7) {
    return 1;
} else {
    return 0;
}
\end{verbatim}

\begin{enumerate}
	\item What could be wrong?

	\item Provide a trace in the format from lecture exposing the problem.

	\item Help Anshu out and provide a fix for this issue that will allow \verb'if' statements to function as he desires.
		Ensure that your fix does not break any other features of this language.\\
		(Note: there are solutions to this that involve fixing either the statics or dynamics or both.  Simple (but correct!) approaches are preferred).
\end{enumerate}

\section*{Problem 2: $C_0^\lambda$ Revisited (10 points)}

After Matt's language $C_0^\lambda$ failed to gain traction among programmers, Will stepped in to help.
As you may recall, $C_0^\lambda$ has the following syntax:
\begin{align*}
	\mbox{Type  } \tau & ::= \text{int} \mid (\tau \times \tau \rightarrow \tau) \\
	\mbox{Expression  } e & ::= n \mid x \mid (\lambda (x, y).e) \mid (e \oplus e) \mid (e(e, e))
\end{align*}
You should be familiar with the expression $\lambda (x, y). e$, though perhaps not in the same format.
In \verb'SML', this would be written as \verb'fn (x, y) => e'.\\
Once he read these rules, Will realized that Matt forgot to do something -- he never specified the semantics for his new language!
Noticing that the typing judgements for this language are fairly simple, Will quickly wrote the following rules:
\[
\begin{array}{c}
	\infer{\Gamma \vdash n : \text{int}}{}
	\hspace{3em}
	\infer{\Gamma \vdash x : \tau}{\Gamma(x) = \tau}
	\hspace{3em}
	\infer{\Gamma \vdash (e_1 \oplus e_2) : \text{int}}{\Gamma \vdash e_1 : \text{int} & \Gamma \vdash e_2 : \text{int}}
	\\ \\
	\infer{\Gamma \vdash e_1(e_2, e_3) : \tau_3}{\Gamma \vdash e_1 : (\tau_1 \times \tau_2 \rightarrow \tau_3) & \Gamma \vdash e_2 : \tau_1 & \Gamma \vdash e_3 : \tau_2}
	\hspace{3em}
	\infer{\Gamma \vdash \lambda (x, y).e : (\tau_1 \times \tau_2 \rightarrow \tau_3)}{x : \tau_1, y : \tau_2 \vdash e : \tau_3}
\end{array}
\]
However, these rules are significantly more limiting than you might first think.
\begin{enumerate}
	\item Give a short program that one might want to write but are unable to write in this language.
		\verb'Ocaml' or \verb'SML' would be good languages to provide examples in.
		{\sl (Note: this is not related to the number of arguments functions take).}
	\item What might be difficult if you were to implement these statics?  {\sl (Hint: think about modes)}.
\end{enumerate}

\section*{Problem 3: The Next Iteration of C0 (15 points)}

Grant, utterly disgusted by the thought of using a language without statements, refused to help Will and Matt.
Instead, he decided to add a new feature to C0, \verb'iter'.
\[
	\begin{array}{rl}
		\text{iter}(0, b, f) &\cong b\\
		\text{iter}(n < 0, b, f) &\cong \text{error}\\
		\text{iter}(1 + n, b, f) &\cong f(\text{iter}(n, b, f))\\
	\end{array}
\]
You may find that this function looks similar to \verb'fold', and it can be useful in many ways.
For example, the following mostly-C0 code creates a linked list of length $n$.
\begin{verbatim}
struct list {
    void* data;
    struct list* next;
};
struct list* list_cons(struct list* old) {
    struct list* new = alloc(struct list);
    new->data = NULL;
    new->next = old;
    return new;
}
struct list* list = iter(n, NULL, list_cons);
\end{verbatim}
For this problem, you will be building upon C0.
You may assume the existing statics and dynamics for C0, as given in lectures 12 and 13.
\begin{enumerate}
	\item Help Grant out by providing him with statics for this new feature.
	\item Give the corresponding dynamics.
	\item Write a small but hopefully interesting program using this feature.
\end{enumerate}


\section*{Problem 4: Polymorphism (20 points)}

The C0 language provides only a very weak form of polymorphism,
essentially using \verb'struct s*' in a library header, where
\verb'struct s' has not yet been defined.  C provides a more
expressive, but inherently unsafe mechanism by allowing pointers of
type \verb'void*'.  A pointer of this type can reference data of any
type.  We then use implicit or explicit casts to convert to and from
this type.  Some discussion and examples can be found in the notes on
\href{http://www.cs.cmu.edu/~fp/courses/15122-f12/lectures/19-poly.pdf}{Lecture
  19} in the course on \emph{Principles of Imperative Computation}.
In this problem we explore a safe version of \verb'void*' which implements
dynamic checking of polymorphic types and has made its way into C1.

\subsection*{Tagging and Untagging Data}

The key to making the type \verb'void*' safe is to tag pointers of
this type with their actual type.  When we cast values of this type to
actual types we can then compare tags to make sure the operation is
type-safe.  We have new tagging and untagging constructs
\[
\begin{array}{lcl}
e & ::= & \ldots \mid \mathtt{tag}(\tau{*}, e) \mid \mathtt{untag}(\tau{*}, e)
\end{array}
\]
with the following typing rules
\[
\begin{array}{c}
  \infer{\Gamma \vdash \mathtt{tag}(\tau{*}, e) : \mathtt{void}{*}}
        {\Gamma \vdash e : \tau{*}}
  \hspace{3em}
  \infer{\Gamma \vdash \mathtt{untag}(\tau{*}, e) : \tau{*}}
        {\Gamma \vdash e : \mathtt{void}{*}}
\end{array}
\]
Tagging is always safe: we can forget that $e$ references a value of
type $\tau$ and just weaken its type to \verb'void*'.  Untagging will
signal a runtime error if the tag of $e$ is different from $\tau{*}$.
For example, if $p : \mathtt{int}*$ then the expression
\[
\mathtt{untag}(\mathtt{bool}*, \mathtt{tag}(\mathtt{int}*, p))
\]
will type-check, but should yield a runtime error while untagging
since $\mathtt{bool}{*} \neq \mathtt{int}{*}$.

\subsection*{A Safe Implementation}

In the safe implementation, a value of type $\mathtt{void}{*}$ will always
be either null (0), or a pointer to 16 bytes of memory on the heap.
The first 8 bytes represent the actual type $\tau{*}$, the second 8
represent the actual value of type $\tau{*}$, which must be an
address.  We assume we can calculate $\mathtt{tprep}(\tau{*}) = w$, where
$w$ is a 8-byte tag value uniquely representing the type $\tau{*}$.
The default value for type $\mathtt{void}{*}$ is null (0).

\begin{enumerate}
\item[(a)] Provide the evaluation rules for $\mathtt{tag}(\tau{*}, e)$.
  You should define new transition rules for the abstract
  machine with state $H \mathrel{;} S \mathrel{;} \eta \vdash e \rhd K$
  as defined in lecture.

  Your rules do not need to check whether memory is exhausted.
  You should also describe the evaluation of $\mathtt{tag}(\tau{*}, e)$
  informally, which will help us assign partial credit in case your rules
  are not entirely correct.

\item[(b)] Provide the evaluation rules for $\mathtt{untag}(\tau{*}, e)$.
  This should fail if the tag of $e$ does not match $\tau{*}$, in which
  case you should raise a $\mathtt{tag}$ exception.  You should define new
  transition rules for the abstract machine as in part (a), and accompany
  them with an informal description.

\item[(c)] Describe code generation for the $\mathtt{tag}$ and $\mathtt{untag}$
  expression forms in the style we used for arrays in lecture 14.
  You may use function calls
  \[
  \begin{array}{l}
    t^{64} \leftarrow \mathtt{malloc}(s^{64})
  \end{array}
  \]
  to obtain the address $t$ of $s$ bytes of uninitialized memory, and
  use the jump target \verb'raise_tag' to signal a tag exception.
\end{enumerate}

\subsection*{An Unsafe Implementation}

The unsafe implementation should forego tag checking.  As a result, we
do not need to tag or untag at all, since we trust the programmer that
tags would have been correct.  In other words, $\mathtt{tag}(\tau{*}, e)$
would be like \verb'(void*)e' in C, and $\mathtt{untag}(\tau{*}, e)$ like
$(\tau*) \mathtt{e}$, relevant only at the type-checking phase.

\begin{enumerate}
\item[(d)] Explain why compiling $e_1 \mathrel{\mbox{\tt ==}} e_2$ for
  pointers $e_1$ and $e_2$ to a naive pointer comparison is not always
  correct in \emph{safe} mode.

\item[(e)] Explain how to compile $e_1 \mathrel{\mbox{\tt ==}} e_2$ in
  both safe and unsafe modes so that program behavior is the same for
  both modes (assuming, of course, that the program is indeed safe and
  will not raise an exception). Code is not necessary if the
  implementation is clear enough from your description.
\end{enumerate}

\end{document}
