Judgment borrow_check_expr
judgment_fn! {
/// Prove that any loans issued in this value expression are respected, and return its type.
pub fn borrow_check_expr(
env: TypeckEnv,
assumptions: Predicates,
state: FlowState,
expr: Expr,
places_live_on_exit: LivePlaces,
) => (Ty, FlowState) {
/* rules omitted */
}
}Source: crates/formality-rust/src/check/borrow_check/nll.rs:371
The number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.
parenthesized| Line | Coverage | Source |
|---|---|---|
| 383 | ✗ | (borrow_check_expr(env, assumptions, state, expr, places_live_on_exit) => (ty, state)) |
| ──────── ("parenthesized") | ||
| 385 | 5 | (borrow_check_expr(env, assumptions, state, Expr::Parens(expr), places_live_on_exit) => (ty, state)) |
multiplication| Line | Coverage | Source |
|---|---|---|
| 389 | N/A | (let expr = Expr::BinOp { lhs: lhs.clone(), op: BinOpKind::Mul, rhs: rhs.clone() }) |
| 390 | 2 | (borrow_check_expr(env, assumptions, state, expr, places_live_on_exit) => (ty, state)) |
| ──────── ("multiplication") | ||
| 392 | 7 | (borrow_check_expr(env, assumptions, state, Expr::Mul { lhs, rhs }, places_live_on_exit) => (ty, state)) |
assign| Line | Coverage | Source |
|---|---|---|
| 397 | 1 | (borrow_check_expr( env, assumptions, state, expr, Assignment(place).live_before(env, &state, places_live_on_exit), ) => (value_ty, state)) |
| 406 | 2 | (borrow_check_place_expr( env, assumptions, state, place, ) => (place, state)) |
| 414 | 1 | (prove_assignable(env, assumptions, state, value_ty, &place.ty) => state) |
| 416 | 11 | (access_permitted( env, assumptions, state, Access::new(AccessKind::Write, place), places_live_on_exit, ) => state) |
| 424 | N/A | (let state = kill_loans(place, state)) |
| 425 | N/A | (let state = state.with_initialized(&place.to_place_expression())) |
| ──────── ("assign") | ||
| 427 | 27 | (borrow_check_expr(env, assumptions, state, Expr::Assign { place, expr }, places_live_on_exit) => (Ty::unit(), state)) |
assign-op| Line | Coverage | Source |
|---|---|---|
| 432 | 1 | (borrow_check_expr( env, assumptions, state, rhs, Seq(place, Assignment(place)).live_before(env, &state, places_live_on_exit), ) => (rhs_ty, state)) |
| 439 | N/A | (let places_live_before_write = Assignment(place).live_before(env, &state, places_live_on_exit)) |
| 441 | ✗ | (borrow_check_place_expr(env, assumptions, state, place) => (place, state)) |
| 442 | ✗ | (prove_ty_is_rigid(env, assumptions, state, &place.ty) => (RigidTy { name: RigidName::ScalarId(scalar), parameters: _ }, state)) |
| 443 | 1 | (if scalar.is_int()) |
| 444 | 1 | (prove_assignable(env, assumptions, state, rhs_ty, &place.ty) => state) |
| 446 | 2 | (access_permitted(env, assumptions, state, Access::new(AccessKind::Read, place), places_live_before_write) => state) |
| 447 | 1 | (access_permitted(env, assumptions, state, Access::new(AccessKind::Write, place), places_live_on_exit) => state) |
| 448 | N/A | (let state = kill_loans(place, state)) |
| ──────── ("assign-op") | ||
| 450 | 7 | (borrow_check_expr(env, assumptions, state, Expr::AssignOp { place, op: _, rhs }, places_live_on_exit) => (Ty::unit(), state)) |
call| Line | Coverage | Source |
|---|---|---|
| 455 | 6 | (borrow_check_expr( env, assumptions, state, callee, args.live_before(env, &state, places_live), ) => (callee_ty, state)) |
| 464 | ✗ | (prove_ty_is_rigid(env, assumptions, state, callee_ty) => (RigidTy { name: RigidName::FnDef(fn_id), parameters }, state)) |
| 467 | ✗ | (let Fn { id: _, safety, binder } = env.crates().fn_named(fn_id)?) |
| 469 | ✗ | (ProvenSet::singleton((safety, ProofTree::leaf("safety"))) => Safety::Safe) |
| 470 | ✗ | (let FnBoundData { input_args, output_ty, where_clauses, body: _ } = binder.instantiate_with(parameters)?) |
| 474 | N/A | (let input_tys: Vec<Ty> = input_args.iter().map(|a| a.ty.clone()).collect()) |
| 475 | 1 | (if input_tys.len() == args.len()) |
| 477 | ✗ | (for_all(i in 0..args.len()) with(state) (borrow_check_expr_has_ty(env, assumptions, state, &args[i], &input_tys[i], places_live) => state)) |
| 480 | ✗ | (prove_where_clauses(env, assumptions, state, where_clauses) => state) |
| ──────── ("call") | ||
| 482 | 41 | (borrow_check_expr(env, assumptions, state, Expr::Call { callee, args }, places_live) => (output_ty, state)) |
binop| Line | Coverage | Source |
|---|---|---|
| 485 | 1 | (borrow_check_expr(env, assumptions, state, lhs, rhs.live_before(env, &state, places_live_on_exit)) => (lhs_ty, state)) |
| 486 | ✗ | (prove_ty_is_rigid(env, assumptions, state, &lhs_ty) => (RigidTy {name: RigidName::ScalarId(scalar), parameters: _}, state)) |
| 487 | 1 | (if scalar.is_int()) |
| 488 | 3 | (borrow_check_expr_has_ty(env, assumptions, state, rhs, &lhs_ty, places_live_on_exit) => state) |
| ──────── ("binop") | ||
| 490 | 23 | (borrow_check_expr(env, assumptions, state, Expr::BinOp{lhs, op: _, rhs}, places_live_on_exit) => (lhs_ty, state)) |
literal| Line | Coverage | Source |
|---|---|---|
| ──────── ("literal") | ||
| 495 | 114 | (borrow_check_expr(_env, _assumptions, state, Literal { value: _, ty }, _places_live_on_exit) => (ty, state)) |
true| Line | Coverage | Source |
|---|---|---|
| ──────── ("true") | ||
| 500 | 28 | (borrow_check_expr(_env, _assumptions, state, Expr::True, _places_live_on_exit) => (ScalarId::Bool, state)) |
false| Line | Coverage | Source |
|---|---|---|
| ──────── ("false") | ||
| 505 | 7 | (borrow_check_expr(_env, _assumptions, state, Expr::False, _places_live_on_exit) => (ScalarId::Bool, state)) |
ref| Line | Coverage | Source |
|---|---|---|
| 509 | ✗ | (borrow_check_place_expr( env, assumptions, state, place, ) => (place, state)) |
| 517 | N/A | (let access_kind = match kind { RefKind::Shared => AccessKind::Read, RefKind::Mut => AccessKind::Write, }) |
| 521 | 8 | (access_permitted( env, assumptions, state, Access::new(access_kind, place), places_live_on_exit, ) => state) |
| 530 | N/A | (let state = state.with_loan(Loan::new(lt, place, kind))) |
| 531 | N/A | (let state = state.with_outlives(&reborrow_constraints(place, lt))) |
| 538 | 1 | (verify_universal_outlives(env, assumptions, &state.current.outlives) => ()) |
| 539 | N/A | (let ty = place.ty.ref_ty_of_kind(kind, lt)) |
| ──────── ("ref") | ||
| 541 | 41 | (borrow_check_expr(env, assumptions, state, Expr::Ref { kind, lt, place }, places_live_on_exit) => (ty, state)) |
place| Line | Coverage | Source |
|---|---|---|
| 545 | 2 | (borrow_check_place_expr(env, assumptions, state, place) => (place, state)) |
| 546 | ✗ | (access_kind_for_place_use(env, assumptions, state, place) => (access_kind, state)) |
| 547 | 17 | (access_permitted(env, assumptions, state, Access::new(access_kind, place), places_live_on_exit) => state) |
| 548 | N/A | (let state = if matches!(access_kind, AccessKind::Move) { state.with_uninit(&place.to_place_expression()) } else { state.clone() }) |
| 549 | 3 | (prove_place_is_movable(env, assumptions, state, place) => state) |
| ──────── ("place") | ||
| 551 | 100 | (borrow_check_expr(env, assumptions, state, Expr::Place(place), places_live_on_exit) => (&place.ty, state)) |
fn-name| Line | Coverage | Source |
|---|---|---|
| 557 | ✗ | (if let PlaceExpr::Var(id) = place) |
| 558 | ✗ | (if !state.has_local(id)) |
| 559 | 2 | (borrow_check_fn_ref(env, assumptions, state, id, Vec::<Parameter>::new()) => (ty, state)) |
| ──────── ("fn-name") | ||
| 561 | 14 | (borrow_check_expr(env, assumptions, state, Expr::Place(place), _places_live_on_exit) => (ty, state)) |
turbofish| Line | Coverage | Source |
|---|---|---|
| 566 | 6 | (borrow_check_fn_ref(env, assumptions, state, id, args) => (ty, state)) |
| ──────── ("turbofish") | ||
| 568 | 30 | (borrow_check_expr(env, assumptions, state, Expr::Turbofish { id, args }, _places_live_on_exit) => (ty, state)) |
struct| Line | Coverage | Source |
|---|---|---|
| 588 | 1 | (let Struct { id: _, binder } = env.crates().struct_named(&adt_id)?) |
| 589 | ✗ | (if turbofish.parameters.len() == binder.len()) |
| 590 | ✗ | (let StructBoundData { where_clauses, fields } = binder.instantiate_with(&turbofish.parameters)?) |
| 593 | N/A | (let expected_names: Set<FieldName> = for_all field in fields => field.name) |
| 594 | N/A | (let provided_names: Set<FieldName> = for_all field in field_exprs => field.name) |
| 595 | ✗ | (if expected_names == provided_names) |
| 599 | 1 | (if field_exprs.len() == provided_names.len()) |
| 602 | ✗ | (for_all(i in 0..field_exprs.len()) with(state) (field in fields) (if field.name == field_exprs[i].name) (borrow_check_expr_has_ty(env, assumptions, state, &field_exprs[i].value, &field.ty, places_live_on_exit) => state)) |
| 607 | ✗ | (prove_where_clauses(env, assumptions, state, where_clauses) => state) |
| 609 | N/A | (let ty = RigidTy::new(adt_id, &turbofish.parameters)) |
| ──────── ("struct") | ||
| 611 | 19 | (borrow_check_expr(env, assumptions, state, Expr::Struct { adt_id, turbofish, field_exprs }, places_live_on_exit) => (ty, state)) |