Skip to content

Commit bce8290

Browse files
committed
Support StorageLive and StorageDead
1 parent 8b130f7 commit bce8290

File tree

3 files changed

+115
-7
lines changed

3 files changed

+115
-7
lines changed

crates/formality-check/src/mini_rust_check.rs

Lines changed: 34 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,7 @@ impl Check<'_> {
9494
declared_input_tys,
9595
callee_input_tys: Map::new(),
9696
crate_id: crate_id.clone(),
97+
fn_args: body.args.clone(),
9798
};
9899

99100
// (4) Check statements in body are valid
@@ -150,6 +151,24 @@ impl Check<'_> {
150151
self.check_place(typeck_env, place_expression)?;
151152
// FIXME: check that access the place is allowed per borrowck rules
152153
}
154+
minirust::Statement::StorageLive(local_id) => {
155+
// FIXME: We need more checks here after loan is introduced.
156+
if self.find_local_id(&typeck_env, local_id).is_none() {
157+
bail!("Statement::StorageLive: invalid local variable")
158+
}
159+
}
160+
minirust::Statement::StorageDead(local_id) => {
161+
// FIXME: We need more checks here after loan is introduced.
162+
let Some((local_id, _)) = self.find_local_id(&typeck_env, local_id) else {
163+
bail!("Statement::StorageDead: invalid local variable")
164+
};
165+
// Make sure function arguments and return place are not marked as dead.
166+
if local_id == typeck_env.ret_id
167+
|| typeck_env.fn_args.iter().any(|fn_arg| local_id == *fn_arg)
168+
{
169+
bail!("Statement::StorageDead: trying to mark function arguments or return local as dead")
170+
}
171+
}
153172
}
154173
Ok(())
155174
}
@@ -249,11 +268,7 @@ impl Check<'_> {
249268
match place {
250269
Local(local_id) => {
251270
// Check if place id is a valid local id.
252-
let Some((_, ty)) = env
253-
.local_variables
254-
.iter()
255-
.find(|(declared_local_id, _)| *declared_local_id == local_id)
256-
else {
271+
let Some((_, ty)) = self.find_local_id(env, local_id) else {
257272
bail!(
258273
"PlaceExpression::Local: unknown local name `{:?}`",
259274
local_id
@@ -265,6 +280,17 @@ impl Check<'_> {
265280
Ok(place_ty.clone())
266281
}
267282

283+
fn find_local_id(&self, env: &TypeckEnv, local_id: &LocalId) -> Option<(LocalId, Ty)> {
284+
if let Some((local_id, ty)) = env
285+
.local_variables
286+
.iter()
287+
.find(|(declared_local_id, _)| *declared_local_id == local_id)
288+
{
289+
return Some((local_id.clone(), ty.clone()));
290+
}
291+
return None;
292+
}
293+
268294
// Check if the value expression is well-formed, and return the type of the value expression.
269295
fn check_value(&self, typeck_env: &mut TypeckEnv, value: &ValueExpression) -> Fallible<Ty> {
270296
let value_ty;
@@ -373,4 +399,7 @@ struct TypeckEnv {
373399
/// We need this to access information about other functions
374400
/// declared in the current crate.
375401
crate_id: CrateId,
402+
403+
/// LocalId of function argument.
404+
fn_args: Vec<LocalId>,
376405
}

crates/formality-rust/src/grammar/minirust.rs

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -71,8 +71,10 @@ pub enum Statement {
7171
// SetDiscriminant
7272
// Validate
7373
// Deinit
74-
// StorageLive
75-
// StorageDead
74+
#[grammar(StorageLive($v0);)]
75+
StorageLive(LocalId),
76+
#[grammar(StorageDead($v0);)]
77+
StorageDead(LocalId),
7678
}
7779

7880
/// Based on [MiniRust terminators](https://github.com/minirust/minirust/blob/9ae11cc202d040f08bc13ec5254d3d41d5f3cc25/spec/lang/syntax.md#statements-terminators).

src/test/mir_fn_bodies.rs

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -227,6 +227,33 @@ fn test_place_mention_statement() {
227227
)
228228
}
229229

230+
/// Test valid StorageLive and StorageDead statements.
231+
#[test]
232+
fn test_storage_live_dead() {
233+
crate::assert_ok!(
234+
[
235+
crate Foo {
236+
fn foo (u32) -> u32 = minirust(v1) -> v0 {
237+
let v0: u32;
238+
let v1: u32;
239+
let v2: u32;
240+
241+
bb0: {
242+
statements {
243+
local(v0) = load(local(v1));
244+
StorageLive(v2);
245+
StorageDead(v2);
246+
}
247+
return;
248+
}
249+
250+
};
251+
}
252+
]
253+
expect_test::expect![["()"]]
254+
)
255+
}
256+
230257
// Test what will happen if the next block does not exist for Terminator::Call.
231258
#[test]
232259
fn test_no_next_bb_for_call_terminator() {
@@ -660,3 +687,53 @@ fn test_invalid_value_in_switch_terminator() {
660687
expect_test::expect!["The value used for switch must be an int."]
661688
)
662689
}
690+
691+
/// Test the behaviour of having return place in StorageDead.
692+
#[test]
693+
fn test_ret_place_storage_dead() {
694+
crate::assert_err!(
695+
[
696+
crate Foo {
697+
fn foo (u32) -> u32 = minirust(v1) -> v0 {
698+
let v0: u32;
699+
let v1: u32;
700+
701+
bb0: {
702+
statements {
703+
StorageDead(v1);
704+
}
705+
return;
706+
}
707+
708+
};
709+
}
710+
]
711+
[]
712+
expect_test::expect!["Statement::StorageDead: trying to mark function arguments or return local as dead"]
713+
)
714+
}
715+
716+
/// Test the behaviour of having function argument in StorageDead.
717+
#[test]
718+
fn test_fn_arg_storage_dead() {
719+
crate::assert_err!(
720+
[
721+
crate Foo {
722+
fn foo (u32) -> u32 = minirust(v1) -> v0 {
723+
let v0: u32;
724+
let v1: u32;
725+
726+
bb0: {
727+
statements {
728+
StorageDead(v0);
729+
}
730+
return;
731+
}
732+
733+
};
734+
}
735+
]
736+
[]
737+
expect_test::expect!["Statement::StorageDead: trying to mark function arguments or return local as dead"]
738+
)
739+
}

0 commit comments

Comments
 (0)