Description
-
The Borrow Checker (15)
These exercises will give you practice with thinking about Rust’s ownership rules and the borrow checker.
For each of the following code snippets, answer the following questions in 1-2 sentences each:
-
Explain how the program breaks Rust’s rules in your own words|do not just copy the compiler error.
-
Why is the program bad? Suppose that Rust accepted this program. What could go possibly wrong?
-
fn foo(s: String) { /* … */ }
fn baz() {
let str_1 = String::from(“Hello”); let str_2 = str_1;
foo(str_1);
}
-
fn foo(s: &mut String) { /* … */ }
fn baz() {
let my_str = String::from(“Hello”); let my_ref_one: &String = &my_str; let my_ref_two: &String = &my_str;
foo(&my_ref_two);
/* … */
}
-
fn baz() {
let mut my_str = String::from(“Hello”);
let my_ref = &my_str;
my_str.push_str(” World!”);
println!(“What s here? {}”, my_ref);
}
-
fn foo(s: &mut String) { /* … */ }
fn baz() {
let mut my_str = String::from(“Hello”); let my_ref = &my_str;
let my_other_ref = &mut my_str;
foo(my_other_ref);
println!(“What s here? {}”, my_ref);
}
-
struct MyStruct {
my_str: String,
my_int: i32,
}
fn foo(s: String) { /* … */ }
fn baz() {
let my_struct = MyStruct {
my_str: String::from(“Hello”),
my_int: 42,
};
foo(my_struct.my_str);
foo(my_struct.my_str);
}
-
fn foo(s: String) { /* … */ }
fn bar(s: &String) {
let my_str: String = *s;
foo(my_str);
}
-
fn foo(s: String) { /* … */ }
fn bar(opt: Option<String>) { match opt {
None => println!(“Nothing!”), Some(my_str) => foo(my_str)
}
let opt_s = opt.unwrap_or(String::new());
println!(“What s here? {}”, opt_s);
}
-
fn foo< a>(s: String) -> & a String { &s
}
-
fn foo(s: &mut String) -> &mut String {
s.push_str(” World!”);
s
}
fn baz() {
let mut dummy = String::new();
let mut str_ref = &mut dummy;
{
let mut my_str = String::from(“Hello”);
str_ref = foo(&mut my_str);
}
println!(“What s here? {}”, str_ref);
}
-
fn foo< a>(s: & a String, t: & a String) -> & a String {
if s > t { s } else { t }
}
fn baz() {
let mut foo1 = String::from(“Hello”);
let mut str_ref: &String;
{
let mut foo2 = String::from(“World”);
str_ref = foo(&foo1, &foo2);
}
println!(“What s here? {}”, str_ref);
}
-
Lambda Calculus with References (15)
In the most recent homework WR4, we saw how to model a core imperative language where programs can read/write to mutable variables in a store. One might think that an imperative language is required to support mutable variables, since the lambda calculus we saw in the rst half of the course (WR1, WR2, and WR3) models functional languages without a store, but functional languages can also support mutable variables. In fact, most real-world functional languages (e.g., OCaml, Scheme, Lisp) allow reading or writing variables|Haskell is an exception.
In this part of the homework, we will outline one way to extend the lambda calculus with mutable references and a simple kind of heap. We will start with a basic lambda calculus with integers:
n ::= 0 j 1 j 2 j
v ::= x j x: e j n j ()
e ::= x j x: e j n j () j e1 e2 j e1 + e2 j if e > 0 then e1 else e2 j let x = e1 in e2
The special value unit () represents a value with no information; we can use this value to encode functions that take no arguments, and functions that don’t return anything interesting. We include let-bindings for
convenience, even though they can be encoded by function application. To allow stores, we rst extend our language with memory locations:
l ::= #0 j #1 j #2 j
-
::= j l e ::= j l
Locations are integers with a special tag # in front of them; this is to avoid confusing locations with regular integers. Locations are values. Then, we extend expressions with four more constructs:
e ::= j e j new(e) j e1 := e2 j e1 ; e2
The rst one reads (dereferences) a location, the second one allocates a new location with initial value e, the third one writes e2 to a location e1, and the fourth one runs e1, then continues with e2.
To give an operational semantics to this language, we will use the same idea we used for the imperative language: step pairs (e; s) of expressions and stores. For this language, our stores s will be nite lists of numbers. For instance, [ ] is the empty store where nothing has been allocated, while [5; 3] is the store where location #0 holds 5 and location #1 holds 3. We will use some notation for working with stores:
s :: n is the list from appending n to the end of s; size(s) is the length of the list s;
s[n] is the n-th element of the list s (s[0] is the rst element); s[n ! v] is the same as s, except position n holds v.
We give the step rules for the new constructs rst.
Dereference. To dereference, we rst step the expression to a location, then look up the location in the store if the address is in bounds:
-
-
-
(e; s) ! (e0 ; s0 )
l = #n n < size(s) v = s[n]
( e; s) ! ( e0 ; s0 )
( l; s) ! (v; s)
-
-
Allocation. To allocate, we rst step the initial expression to a value. Then, we extend the store by slot, and return the new index:
-
-
-
-
(e; s) !
(e0 ; s0 )
size(s) = n
s0 = s :: v
(new(e); s)
!
(new(e0 ); s0 )
(new(v); s)
!
(#n; s0 )
-
-
-
Write. To write, we rst step the left-hand-side to a location, then step the right-hand side to a value, then write the value to the location in the store if it is in bounds:
-
-
-
(e1; s) ! (e10 ; s0 )
(e2; s) ! (e20 ; s0 )
(
e
1
:= e
; s)
!
(
e0 := e ; s0 )
(
l := e
; s)
( l := e0
; s0 )
2
1
2
2
!
2
l = #n
n < size(s)
s0 = s[n
v]
7!
(
l := v; s)
!
((); s0 )
-
-
Sequence. The sequence step rules look like the rules for the imperative language. Note that the return value of the rst expression is discarded (just like in Rust):
(e1; s) ! (e01; s0 )
(e1 ; e2; s) ! (e01 ; e2; s0 ) (v ; e2; s) ! (e2; s)
The step rules for the lambda calculus features are almost the same as before, except we need to thread the store through the evaluation since evaluating an expression may change the store.
Application. We rst evaluate e1, then e2, then call the function:
-
(e1; s) ! (e10 ; s0 )
(e2; s) ! (e20 ; s0 )
(e
1
e
2
; s)
!
(e0 e
2
; s0 )
(( x: e
1
) e
2
; s)
!
(( x: e
1
) e0
; s0 )
(( x: e
1
) v ; s)
!
(e
1
[x
v
]; s)
1
2
2
7!2
Addition. We rst evaluate e1, then e2, then add:
-
-
(e1; s) ! (e10 ; s0 )
(e2; s) ! (e20 ; s0 )
n = n1 + n2
(e
1
+ e ; s)
!
(e0
+ e
; s0 )
(n
1
+ e
; s)
!
(n
1
+ e0
; s0 )
(n
1
+ n
; s)
!
(n; s)
2
1
2
2
2
2
-
If-then-else. We rst evaluate the guard e, then decide which branch to step to:
(e; s) ! (e0 ; s0 )
-
-
(if e > 0 then e1 else e2; s) ! (if
e0 > 0 then e1 else e2; s0 )
n > 0
n = 0
(if n > 0 then e1 else e2; s) ! (e1; s)
(if n > 0 then e1 else e2; s) ! (e2; s)
-
Let-binding. We rst evaluate e1, then substitute it for x in e2. This is very similar to function application.
2.1 Stepping expressions
Show how the following programs step, starting from the empty store [ ]. Your answer for each part should be a sequence of the form (e; [ ]) ! (e1; s1) ! ! (en; sn), where en cannot step further. We’ve done the rst one for you.
(a) let x = new(42) in x := x + 1
(let x = new(42) in x := x + 1; [ ])
!(let x = #0 in x := x + 1; [42])
!( (#0) := (#0) + 1; [42])
!( (#0) := 42 + 1; [42])
!( (#0) := 43; [42])
!((); [43])
-
let x = new(7) in (let y = new(0) in x := 0 ; y := y + 1)
-
let x = new(7) in (let y = x in x := 0 ; y := y + 1)
-
let x = new(4) in (if x > 0 then x := 500 else x := 2)
-
let x = new(39) in ( y: y := y + 1) x
-
( y: ( x: x () ; x ()) ( z: y := y + 1)) new(5)
The language we have described has a good property: as long as the programmer doesn’t put any raw locations (things of the form #n) into the program, there are no memory errors|it is not possible to read or write an unallocated location. Suppose we now try to add a deallocation instruction free(e). We allow locations to contain a special symbol ?, representing deallocated memory. Note that ? is not a value; for instance, the letter v can never refer to ?. Then to deallocate memory, we check the address is allocated, and if so, we set the store to contain ? at that location:
-
(e; s)
!
(e0
; s0 )
l = #n n < size(s)
s[n] =
s0 = s[n
]
6 ?
7! ?
(free(e); s)
!
(free(e0 ); s0 )
(free(l); s)
!
((); s0 )
|
In this section, we tweak the last rule for writes: |
|||||
|
l = #n n < size(s) |
s[n] = |
s0 = s[n v] |
|||
|
6 ? |
7! |
||||
|
( |
l := v; s) |
! |
((); s0 ) |
||
Unfortunately, our language can now have memory errors.
-
Write a small program that tries to read a freed location, also known as a use-after-free. Show how your program steps, and con rm that it gets stuck|it does not reach a value.
-
Write a small program that tries to free a location twice, also known as a double free. Show how your program steps, and con rm that it gets stuck|it does not reach a value.
7
