Borrow checking
Borrow checking lives under check/borrow_check/. Its top-level judgment is borrow_check, which checks that the loans issued while executing a basic block are respected.
borrow_check
borrow_check(env: TypeckEnv, assumptions: Wcs, state: FlowState, block: Block,) => ()At the top level, borrow checking works over a TypeckEnv, a set of assumptions, a FlowState, and a Block. It delegates to borrow_check_block, which walks the block and updates the flow state statement by statement:
borrow_check_block(env: TypeckEnv, assumptions: Wcs, state: FlowState, block: Block, places_live_on_exit: LivePlaces,) => FlowStateStatements
borrow_check_statement handles each kind of statement. Here are some representative rules:
let bindings
(prove_ty_is_wf(env, assumptions, state, ty) => state)
(for_all(init in init.into_iter()) with (state) // FIXME: should make syntax for this
(let Init { expr } = init)
(borrow_check_expr_has_ty(env,
assumptions,
state,
expr,
ty,
LiveBefore::live_before(&Assignment(id), env, &state, &places_live_on_exit),
) => state))
(let state = state.with_local_in_scope(&env.env, label, id, ty)?)
------------------------------------------------------------ ("let")
(borrow_check_statement(env, assumptions, state, Stmt::Let { label, id, ty, init }, places_live_on_exit) => (env, state))if expressions
(borrow_check_expr_has_ty(
env,
assumptions,
state,
condition,
Ty::bool(),
Either(then_block, else_block).live_before(env, &state, places_live_on_exit),
) => state)
(borrow_check_block(env, assumptions, state, then_block, places_live_on_exit) => then_state)
(borrow_check_block(env, assumptions, state, else_block, places_live_on_exit) => else_state)
(let state: FlowState = Union((then_state, else_state)).upcast())
------------------------------------------------------------ ("if")
(borrow_check_statement(env, assumptions, state, Stmt::If { condition, then_block, else_block }, places_live_on_exit) => (env, state))loop
(let continue_live = Stmt::loop_(label, body).live_before(&env, &state, places_live_on_exit))
(let state = state.push_continue_scope(&env.env, label, places_live_on_exit, continue_live)?)
(borrow_check_loop(env, assumptions, state, body, places_live_on_exit) => state)
(let state = state.pop_scope(label))
------------------------------------------------------------ ("loop")
(borrow_check_statement(env, assumptions, state, Stmt::Loop { label, body }, places_live_on_exit) => (env, state))break and continue
(if state.scope_has_label(label))!
(let locals_to_drop = state.locals_dropped_to_label(label))
(drop_places(env, assumptions, state, locals_to_drop, places_live_on_exit) => state)
(let state = state.with_break(label))
(let state = state.diverges())
------------------------------------------------------------ ("break")
(borrow_check_statement(env, assumptions, state, Stmt::Break { label }, places_live_on_exit) => (env, state))(if state.scope_has_label(label))!
(if let Some(places_live_on_continue) = state.live_after_continue(label))
(let locals_to_drop = state.locals_dropped_to_label(label))
(drop_places(env, assumptions, state, locals_to_drop, places_live_on_continue) => state)
(let state = state.with_continue(label))
(let state = state.diverges())
------------------------------------------------------------ ("continue")
(borrow_check_statement(env, assumptions, state, Stmt::Continue { label }, places_live_on_exit) => (env, state))return
(borrow_check_expr(env, assumptions, state, expr, LivePlaces::default()) => (expr_ty, state))
(if let Some(output_ty) = &env.output_ty)
(prove_assignable(env, assumptions, state, expr_ty, output_ty) => state)
(let state = state.diverges())
------------------------------------------------------------ ("return")
(borrow_check_statement(env, assumptions, state, Stmt::Return { expr }, _places_live_on_exit) => (env, state))Expressions
Borrow checking of value expressions is handled by borrow_check_expr:
borrow_check_expr(env: TypeckEnv, assumptions: Wcs, state: FlowState, expr: Expr, places_live_on_exit: LivePlaces,) => (Ty, FlowState)Outlives
Borrow checking also accumulates pending outlives constraints. The outlives.rs code verifies these constraints:
verify_universal_outlives(env: TypeckEnv, assumptions: Wcs, outlives: Set<PendingOutlives>,) => ()Existential variables succeed trivially; universal variables must be justified by the assumptions:
only_assumed_outlives(env: TypeckEnv, assumptions: Wcs, outlives: Set<PendingOutlives>, v: Variable,) => ()