Final Project

Let's start by giving a slightly different grammar for FR:

<expr>  ::= '{' { <stmt> '⨟' } [<expr>] '}'
          | 'Box::new' '(' <expr> ')'
          | <lval>
          | '&' ['mut'] <lval>
          | <int>

<stmt>  ::= <expr>
          | 'let' 'mut' <var> '=' <expr>
          | <lval> '=' <expr>

<lval>  ::= <var>
          | '*' <lval>

<prog>  ::=

The biggest different between this syntax and the given one is that we distinguish between expressions and statements.³

From this grammar we get a natural AST (which we can put into the file src/utils.rs):

type Ident = String;
enum Copyable {Yes, No}
enum Mutable {Yes, No}

struct Lifetime(usize);

struct Lval {
    ident: Ident,
    derefs: usize,
}

enum Expr {
    Unit,
    Int(i32),
    Lval(Lval, Copyable),
    Box(Box<Expr>),
    Borrow(Lval, Mutable),
    Block(Vec<Stmt>, Box<Expr>, Lifetime),
}

enum Stmt {
    Assign(Lval, Expr),
    LetMut(Ident, Expr),
    Expr(Expr),
}

Next we need some machinary to define the notion of a program store. A quick reminder of definitions (see the FR paper (pg. 13-15) for more details):

• A location is an abstract entity that is either named or unnamed. In reality, unnnamed locations still need unique identifers, but they don't correspond to any variable name in the program.
• A value is:
  • unit (\(\epsilon\));
  • an integer;
  • a reference, which a location that is either owned (\(\ell^\bullet\)) or borrowed (\(\ell^\circ\)).
• A partial value is either a value or undefined (\(\bot\)).
• A slot value is a partial value together with a lifetime (\(\langle v \rangle^m\)).
• The program store (\(\mathcal S\)) is a map from locations to slots values.

We can do a pretty direct translation of these constructs, and put them in src/eval.rs:

Location = Ident;
enum Owned {Yes, No}


enum Value {
    Unit,
    Int(i32),
    Ref(Location, Owned),
}

type Pvalue = Option<Value>;

struct Slot {
    value: Pvalue,
    lifetime: Lifetime,
}

struct Store(HashMap<Location, Slot>);

We'll take unnamed locations to be locations given fresh identifiers.

The semantics of FR is presented against an interface of functions on program stores (write returns the old value in the slot):

impl Store {
    fn locate(&self, w: &Lval) -> &Location { todo!() }
    fn read(&self, x: &Lval) -> &Slot { todo!() }
    fn write(&mut self, x: &Lval, v: Pvalue) -> Pvalue { todo!() }
    fn drop(&mut self, values: Vec<Pvalue>) { todo! () }
}

Finally, the evaluation context is a structure with a program store, along with whatever other data we need in order to perform evaluation:

struct Context {
    store: Store,
    // TODO: anything else you need
}

All that's left to do is implement two evaluation functions, one for expressions and one for statements:

impl Context {
    pub fn eval_expr(&mut self, expr: &Expr, l: Lifetime) -> Value { todo!() }
    pub fn eval_stmt(&mut self, stmt: &Stmt, l: Lifetime) { todo!() }
}

Evaluating an expression returns a value, whereas evaluating a statement only modifies the evaluation context (i.e., the program store). This is a bit more natural compared to what is done in the FR paper, in which statements need to artificially be given values in order to define the semantics.

The trick is that we won't implement the semantics given in the FR paper, but instead its equivalent big-step semantics.

I'm going to leave this as part of the challenge of the project, but hopefully a couple examples will get you thinking about how to come up with the right big-step semantics for FR.

Example: Take the rule \(\text{R-Box}\) and it's associated rule in \(\text{R-Sub}\):

\begin{align*} \frac {\ell_n \not \in \mathbf{dom}(\mathcal S_1) \qquad \mathcal S_2 = \mathcal S_1 [\ell_n \mapsto \langle v \rangle^*] } {\langle \ \mathcal S_1 \vartriangleright \texttt{box} \ v \longrightarrow \mathcal S_2 \vartriangleright \ell_n^\bullet \ \rangle^l} \ (\text{R-Box}) \end{align*} \begin{align*} \frac {\langle \ \mathcal S_1 \vartriangleright t_1 \longrightarrow \mathcal S_2 \vartriangleright t_2 \ \rangle^l} {\langle \ \mathcal S_1 \vartriangleright \texttt{box} \ t_1 \longrightarrow \mathcal S_2 \vartriangleright \texttt{box} \ t_2 \ \rangle^l} \ (\text{R-Sub}) \end{align*}

The rule \(\text{R-Sub}\) states that we need to evaluate the argument of a box constructor before evaluating the box expression itself (the '\(v\)' in \(\text{R-Box}\) is a value). We can package this into a single big-step rule:

\begin{align*} &\frac {\langle \ \mathcal S_1 \vartriangleright e \Downarrow \mathcal S_2 \vartriangleright v \ \rangle^l \qquad \ell_n \not \in \mathbf{dom}(\mathcal S_2) \qquad \mathcal S_3 = \mathcal S_2 [\ell_n \mapsto \langle v \rangle^*] } {\langle \ \mathcal S_1 \vartriangleright \texttt{box} \ e \Downarrow \mathcal S_3 \vartriangleright \ell_n^\bullet \ \rangle^l} \ (\text{R-Box-Big}) \end{align*}

Note that "\(\ell_n \not \in \mathbf{dom}(\mathcal S_2)\)" is just a freshness condition, expressing that \(n\) is a fresh unique identifier.

Example: In the case of statements, consider the rules \(\text{R-Declare}\) and its associated rule in \(\text{R-Sub}\):

\begin{align*} \frac {\mathcal S_2 = \mathcal S_1[\ell_x \mapsto \langle v \rangle^l]} {\langle \ \mathcal S_1 \vartriangleright \texttt{let mut} \ x \ \texttt{=} \ v \longrightarrow \mathcal S_2 \vartriangleright \epsilon \ \rangle^l} \ (\text{R-Declare}) \end{align*} \begin{align*} \frac {\langle \ \mathcal S_1 \vartriangleright t_1 \longrightarrow \mathcal S_2 \vartriangleright t_2 \ \rangle^l} {\langle \ \mathcal S_1 \vartriangleright \texttt{let mut} \ x \ \texttt{=} \ t_1 \longrightarrow \mathcal S_2 \vartriangleright \texttt{let mut} \ x \ \texttt{=} \ t_2 \ \rangle^l} \ (\text{R-Sub}) \end{align*}

We can package this into a single big-step rule, except now there is no need to return a value, just a new store:

\begin{align*} \frac { \langle \ \mathcal S_1 \vartriangleright e \Downarrow \mathcal S_2 \vartriangleright v \ \rangle^l \qquad \mathcal S_3 = \mathcal S_2[\ell_x \mapsto \langle v \rangle^l] } {\langle \ \mathcal S_1 \vartriangleright \texttt{let mut} \ x \ \texttt{=} \ v \Downarrow \mathcal S_3 \rangle^l} \ (\text{R-Declare-Big}) \end{align*}

The name of the game is determining how to do this translation for the remaining rules. It's a bit more work conceptually, but I think a fair amount easier in the implementation.

• One thing we're hand-waving here is our definition of Lifetime. The only thing that's required of lifetimes for the semantics is that every block is labeled with a unique lifetime. This is so the semantics of dropping is correct (we don't want to drop values from the wrong block).

• In the \(\text{R-Box-Big}\) rule, you'll need to use the global lifetime. The easiest way to deal with this for now is to define an method for Lifetime:

  impl Lifetime {
      pub fn global() -> Lifetime {
          Lifetime(0)
      }
  }
  

  Then when we update the definition of Lifetime for our type/borrow checker, we won't need to update the evaluator at all.

• There are many small missing details even in this description of the code. It'll be worthwhile to create some methods, derive some traits, the usual things we need when putting together a Rust project.
• One way you might want to extend your implementation to be more useful is to carry metadata in the expression to make error messages more useful.
• A quick reminder that this is the first iteration of this course, so I don't really know what y'all are going to struggle with the most. Please ask questions, because it helps me out too!

We start with an enumeration for types. This will already be a departure from the FR specification; it will be more convenient if our notion of type includes partial types:

enum Type {
    Unit,
    Int,
    Box(Box<Type>),
    Ref(Lval, Mutable),
    Undefined(Box<Type>),
}

We will think of the Undefined constructor as a way of "walling off" part of a type as undefined.⁴

The typing environment is a mapping from identifiers to slotted types (i.e., (partial) types labeled with lifetimes), very similar to our program store from the previous part:

struct Slot {
  tipe: Type,
  lifetime: Lifetime,
}

struct Env(HashMap<Ident, Slot>);

For now, you are not required to give meaningful type errors. We can set up an enumeration for errors with a single constructor:

enum Error {
    Dummy,
}

type TypeResult<T> = Result<T, Error>;

The environment should implement functions that appear in the spec.

impl Env {
    fn insert(&mut self, var: &str, tipe: Type, lifetime: Lifetime) { todo!() }

    fn type_lval(&self, lval: &Lval) -> TypeResult<Slot> { todo!() }

    // Returns the type under the boxes of a type, given that the
    // underlying type is defined
    fn contained(&self, var: &Ident) -> Option<&Type> { todo!() }

    fn read_prohibited(&self, lval: &Lval) -> bool { todo!() }

    fn write_prohibited(&self, lval: &Lval) -> bool { todo!() }

    // "move" is a keyword in Rust
    fn moove(&mut self, lval: &Lval) -> TypeResult<()> { todo!() }

    // so is "mut"
    fn muut(&self, lval: &Lval) -> bool { todo!() }

    fn compatible(&self, t1: &Type, t2: &Type) -> bool { todo!() }

    fn write(&mut self, w: &Lval, tipe: Type) -> TypeResult<()> { todo!() }

    fn drop(&mut self, l: Lifetime) { todo!() }
}

Most of the functions take a mutable reference to self. This is all we really mean when we say that we're implementing a flow-sensitive type system: the typing environment changes throughout the process of type checking. This also means you have to make sure that you check premises in the correct order!

A lot of these functions are straightforward translations of the definitions given in the spec. There are couple worth expanding on:

Definition: (Type Containment) The type contained in a partial type (a.k.a. the contained type) is defined inductively as follows:

• the type contained in \(\epsilon\) (i.e., the unit type) is \(\epsilon\);
• the type contained in int is int;
• the type contained in &[mut] w is &[mut] w;
• the type contained in \(\square \tau\) is the type contained in \(\tau\);
• otherwise, the contained type is undefined.

That is, the contained type is the full type under any number of partial boxes, given that it is defined.

The type contained in the identifier \(x\) with respect to the typing environment \(\Gamma\) is the type contained in \(\sigma\) where \(\Gamma(x) = \langle \sigma \rangle^l\), given that \(x \in \mathsf{dom}(\Gamma)\) and \(\sigma\) contains a type. It's undefined otherwise.

That is, the contained type of an identifier is the contained type of its partial type in the typing environment, if it's defined.

Definition: (Strong Update) We define the (partial) strong update function and the (partial) write function as follows:

\begin{align*} \mathsf{update}(\Gamma, \epsilon , \tau_1, \tau_2) &= (\Gamma, \tau_2) \\ \mathsf{update}(\Gamma, *\pi , \square \tau_1, \tau_2) &= (\Gamma', \square \tau_1') &(\Gamma', \tau_1') = \mathsf{update}(\Gamma, \pi , \tau_1, \tau_2) \\ \mathsf{update}(\Gamma, *\pi , \&\mathsf{mut} \ u, \tau_2) &= (\Gamma', \&\mathsf{mut} \ u) &\Gamma' = \mathsf{write}(\Gamma, \pi u, \tau_2) \end{align*} \begin{align*} \mathsf{write}(\Gamma, w, \tau) &= \Gamma'[x \mapsto \langle \sigma' \rangle^l] \text{ where} \\ w &= \pi \ | \ x \\ \Gamma(x) &= \langle \sigma \rangle^l \\ (\Gamma', \sigma') &= \mathsf{update}(\Gamma, \pi, \sigma, \tau) \end{align*}

write is by far the most difficult functions in the above interface to implement, particularly if you want to avoid unnecessary cloning. As a hint, think about how strong update can be implemented using a mutable reference to a type, which can be used to write the given argument tipe.

• Because we're implementing strong updates, we are ignoring all issues regarding type/environment strengthing/joins.
• Many of the above functions depend on working with paths. This is, in part, why we defined l-values as we did, with a usize representing the number of dereferences on a variable. You can use this number as a path.
• The functions moove and write, in theory, have the potential to fail, but don't return TypeResult<()>. This is because they should not fail given that the other premises hold. As discussed during lecture, this will require checking that types are not partial in some cases. That was a lie, my apologies. We do need to return errors for moves and writes, e.g., in the cases there is an attempt to move or write through an immutable reference.

As with evaluation, we need more than an environment to perform type/borrow checking. We'll create a typing context to maintain this information.

pub struct Context {
    env: Env,
    // TODO: anything else you need
}

This typing context should implement the following interface:

impl Context {
    // l ≥ m, the ordering relation on liftimes (Note (2) pg. 13)
    fn lifetime_contains(&self, l: Lifetime, m: Lifetime) -> bool { todo!() }

    // Γ ⊢ T ≥ l (Definition 3.21)
    fn well_formed(&self, tipe: &Type, l: Lifetime) -> bool { todo!() }

    fn type_expr(&mut self, expr: &mut Expr) -> TypeResult<Type> { todo!() }

    fn type_stmt(&mut self, stmt: &mut Stmt) -> TypeResult<()> { todo!() }
}

Now that we're putting together the full type/borrow checker, we're gonna fill in our type errors. There are a lot of ways that the type/borrow checker can fail. If you're following along with the structure we've defined here, I'd recommend the following enumeration for type errors:

enum Error {
    UnknownVar(String),
    CannotDeref(Type),
    MovedOut(Lval),
    MoveBehindRef(Lval),
    UpdateBehindImmRef(Lval),
    CopyAfterMutBorrow(Lval),
    MoveAfterBorrow(Lval),
    MutBorrowBehindImmRef(Lval),
    MutBorrowAfterBorrow(Lval),
    BorrowAfterMutBorrow(Lval),
    Shadowing(String),
    IncompatibleTypes(Type, Type),
    LifetimeTooShort(Expr),
    AssignAfterBorrow(Lval),
}

Feel free to add more error kinds if you'd like. Each one roughly captures failing a side condition in a typing rule.

• You'll need some information to keep track of what lifetimes you're contained in during type/borrow checking. I'd recommend a stack of lifetimes. (Important: Contrary to what I eluded to previously, we're going to keep identifying each lifetime with a usize.)
• It may be useful to keep around the Dummy constructor in Error as you work through the type/borrow checker and fill in the actual errors later.
• Remember that you should update the expression itself in the case that you see an l-value that is copyable. In the parsing phase, we'll mark everything as movable.
• The coding here is a bit shorter than that of Part 2.1, but is more error prone. Work through the rules carefully.

We can start with an token enumeration in the lexer file:

pub enum Token {
    Lparen,
    Rparen,
    Lbracket,
    Rbracket,
    Eq,
    Ampersand,
    Star,
    Comma,
    Semicolon,
    Fn,
    Let,
    Mut,
    Box,
    Int(i32),
    Var(String),
}

It is useful to delineate the lexemes in a single constant array:

const LEXEMES : [(&str, Token); 13] = [
    ("(", Token::Lparen),
    (")", Token::Rparen),
    ("{", Token::Lbracket),
    ("}", Token::Rbracket),
    ("=", Token::Eq),
    ("&", Token::Ampersand),
    ("*", Token::Star),
    (",", Token::Comma),
    (";", Token::Semicolon),
    ("fn", Token::Fn),
    ("let", Token::Let),
    ("mut", Token::Mut),
    ("Box::new", Token::Box),
];

We'll assume ASCII (no unicode). We can then use a similar structured lexer to what was used in our assignment on S-expressions:

struct Lexer<'a> {
    contents: Lines<'a>,
    curr_line_num: usize,
    curr_col_num: usize,
    curr_line: &'a str,
}

enum Error {
    Unknown(usize, usize),
}

type LexResult = Result<Token, Error>;

Hint: It's easiest to assume that curr_line is "" if contents is empty. I would then recommend the following interface for the lexer:

impl<'a> Lexer<'a> {
    fn unknown(&self) -> Error {
        Error::Unknown(self.curr_line_num, self.curr_col_num)
    }

    // remove `i` characters and remove any leading whitespace from the
    // result (including empty lines)
    fn consume(&mut self, i: usize) { todo!() }

    fn symbol_or_keyword(&mut self) -> LexResult { todo!() }
        for (lexeme, token) in LEXEMES {
            if self.curr_line.starts_with(lexeme) {
                self.consume(lexeme.len());
                return Ok(token);
            }
        }
        Err(self.unknown())
    }

    // similar to `symbol_or_keyword` but for variables
    fn variable(&mut self) -> LexResult { todo!() }

    // similar to `symbol_or_keyword` for but integer literals
    fn int(&mut self) -> LexResult { todo!() }
}

Finally, you should make Lexer and iterator:

impl<'a> Iterator for Lexer<'a> {
    type Item = LexResult;
    fn next(&mut self) -> Option<LexResult> { todo!() }
}

As we've done in the past, we'll give our parser a peekable version of our lexer. Hint: You may want to add to this structure…

pub struct Parser<'a> {
    lexer: Peekable<Lexer<'a>>,
    // TODO: anything else you need
}

pub enum Error {
    EndOfFile,
    Lexer(lexer::Error),
    Unexpected(lexer::Token),
}

type ParseResult<T> = Result<T, Error>;

Here's a little interface for Parser that I found useful:

impl<'a> Parser<'a> {
    fn next_token(&mut self) -> ParseResult<Token> {
        match self.lexer.next() {
            Some(Ok(token)) => Ok(token),
            Some(Err(err)) => Err(Error::Lexer(err)),
            None => Err(Error::EndOfFile),
        }
    }

    fn next_token_match(&mut self, t: Token) -> ParseResult<Token> {
        let token = self.next_token()?;
        if token != t {
            Err(Error::Unexpected(token))
        } else {
            Ok(token)
        }
    }

    fn next_token_var(&mut self) -> ParseResult<String> {
        let token = self.next_token()?;
        match token {
            Token::Var(ident) => Ok(ident.clone()),
            _ => Err(Error::Unexpected(token))
        }
    }

    fn peek_token(&mut self) -> Result<&Token, Error> {
        let token = self.lexer.peek();
        match token {
            Some(Ok(token)) => Ok(token),
            _ => Err(Error::EndOfFile),
        }
    }
}

What remains is to implement the parse function.

impl<'a> Parser<'a> {
    fn parse_block(&mut self) -> ParseResult<Expr> { todo!() }

    fn parse(&mut self) -> ParseResult<Expr> {
        self.next_token_match(Token::Fn)?;
        let main = self.next_token()?;
        match main {
            Token::Var(ident) if ident == "main" => {
                self.next_token_match(Token::Lparen)?;
                self.next_token_match(Token::Rparen)?;
                let out = self.parse_block();
                if self.peek_token().is_err() {
                    return out
                }
                Err(Error::Unexpected(self.next_token()?))
            }
            _ => Err(Error::Unexpected(main))
        }
    }
}

This function should take a program of the form:

fn main() {
    ...
}

and return the expression in which you read the bracketed part as a block-expression.

Again, as we've done the past, you should approach this in a recursive-descent fashion, writing mini-parsers for each individual construct. With the interface above, this can be quite clean, e.g.:

fn parse_box(&mut self) -> ParseResult<Expr> {
    self.next_token_match(Token::Box)?;
    self.next_token_match(Token::Lparen)?;
    let e = self.parse_expr()?;
    self.next_token_match(Token::Rparen)?;
    Ok(Expr::Box(Box::new(e)))
}

• Don't forget to handle comments in the lexer!
• Remember that every l-value expression should be parsed as not copyable. These should be made copyable in type/borrow checker.
• You'll probably want to add a field to the Parser to help you deal with lifetime annotations on blocks. The only thing that's required is that every block has a distinct lifetime annotation (which is also distinct from the global lifetime), since the ordering of lifetimes is dealt with in the type/borrow checker.