Skip to content

feat: support while let stmt for rust_to_vir_expr. #2482

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
ziqiaozhou wants to merge 1 commit into
base: main
Choose a base branch
from
+100 −41
Open

feat: support while let stmt for rust_to_vir_expr. #2482

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
120 changes: 79 additions & 41 deletions source/rust_verify/src/rust_to_vir_expr.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1846,6 +1846,43 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
mk_expr(ExprX::Const(c))
};

let cond_let_expr_to_vir_match = |cond: &Expr<'tcx>,
lhs_body,
lhs_span,
rhs_body,
rhs_span|
-> Result<ExprX, VirErr> {
let ExprKind::Let(LetExpr { pat, init: expr, .. }) = &cond.kind else {
panic!("Expected let expression");
};
// if let
let vir_place = expr_to_vir_place(bctx, expr)?;
let vir_place = simplify_place_by_cancelling(&vir_place);
let mut vir_arms: Vec<vir::ast::Arm> = Vec::new();
/* lhs */
{
let pattern = pattern_to_vir(bctx, pat)?;
let guard =
bctx.spanned_typed_new(expr.span, &bool_typ(), ExprX::Const(Constant::Bool(true)));
let vir_arm = ArmX { pattern, guard, body: lhs_body };
vir_arms.push(bctx.spanned_new(lhs_span, vir_arm));
}
/* rhs */
{
let pat_typ = vir_arms[0].x.pattern.typ.clone();
let pattern = bctx.spanned_typed_new(cond.span, &pat_typ, PatternX::Wildcard(false));
{
let mut erasure_info = bctx.ctxt.erasure_info.borrow_mut();
erasure_info.hir_vir_ids.push((cond.hir_id, pattern.span.id));
}
let guard =
bctx.spanned_typed_new(expr.span, &bool_typ(), ExprX::Const(Constant::Bool(true)));
let vir_arm = ArmX { pattern, guard, body: rhs_body };
vir_arms.push(bctx.spanned_new(rhs_span, vir_arm));
}
Ok(ExprX::Match(vir_place, Arc::new(vir_arms)))
};

let expr_attrs = bctx.ctxt.tcx.hir_attrs(expr.hir_id);
let expr_vattrs = bctx.ctxt.get_verifier_attrs(expr_attrs)?;
if expr_vattrs.truncate {
Expand Down Expand Up @@ -2659,46 +2696,22 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
ExprKind::If(cond, lhs, rhs) => {
let cond = cond.peel_drop_temps();
match cond.kind {
ExprKind::Let(LetExpr { pat, init: expr, ty: _, span: _, recovered: _ }) => {
// if let
let vir_place = expr_to_vir_place(bctx, expr)?;
let vir_place = simplify_place_by_cancelling(&vir_place);
let mut vir_arms: Vec<vir::ast::Arm> = Vec::new();
/* lhs */
{
let pattern = pattern_to_vir(bctx, pat)?;
let guard = bctx.spanned_typed_new(
expr.span,
&bool_typ(),
ExprX::Const(Constant::Bool(true)),
);
let body = expr_to_vir_consume(bctx, &lhs)?;
let vir_arm = ArmX { pattern, guard, body };
vir_arms.push(bctx.spanned_new(lhs.span, vir_arm));
}
/* rhs */
{
let pat_typ = vir_arms[0].x.pattern.typ.clone();
let pattern =
bctx.spanned_typed_new(cond.span, &pat_typ, PatternX::Wildcard(false));
{
let mut erasure_info = bctx.ctxt.erasure_info.borrow_mut();
erasure_info.hir_vir_ids.push((cond.hir_id, pattern.span.id));
}
let guard = bctx.spanned_typed_new(
expr.span,
&bool_typ(),
ExprX::Const(Constant::Bool(true)),
);
let body = if let Some(rhs) = rhs {
expr_to_vir_consume(bctx, &rhs)?
} else {
mk_expr(ExprX::Block(Arc::new(Vec::new()), None))?.expect_expr()
};
let vir_arm = ArmX { pattern, guard, body };
vir_arms.push(bctx.spanned_new(lhs.span, vir_arm));
}
mk_expr(ExprX::Match(vir_place, Arc::new(vir_arms)))
ExprKind::Let(_) => {
let (rhs_vir, rhs_span) = if let Some(rhs) = rhs {
(expr_to_vir_consume(bctx, &rhs)?, rhs.span)
} else {
(
mk_expr(ExprX::Block(Arc::new(Vec::new()), None))?.expect_expr(),
cond.span,
)
};
mk_expr(cond_let_expr_to_vir_match(
cond,
expr_to_vir_consume(bctx, &lhs)?,
lhs.span,
rhs_vir,
rhs_span,
)?)
}
_ => {
let vir_cond = expr_to_vir_consume(bctx, cond)?;
Expand Down Expand Up @@ -2828,9 +2841,34 @@ pub(crate) fn expr_to_vir_innermost<'tcx>(
} else {
unsupported_err!(expr.span, "loop else");
}
let cond = Some(expr_to_vir_consume(bctx, cond)?);
let body_span = body.span;
let mut body = expr_to_vir_consume(bctx, body)?;
let header = vir::headers::read_header(&mut body, &vir::headers::HeaderAllows::Loop)?;
let (cond, body) = match &cond.peel_drop_temps().kind {
ExprKind::Let(_) => {
let body_ty = body.typ.clone();
let wildcard_body = bctx.spanned_typed_new(
cond.span,
&body_ty,
ExprX::BreakOrContinue { label: None, is_break: true },
);
(
None,
bctx.spanned_typed_new(
cond.span,
&body_ty,
cond_let_expr_to_vir_match(
cond,
body,
body_span,
wildcard_body,
cond.span,
)?,
),
)
}
_ => (Some(expr_to_vir_consume(bctx, cond)?), body),
};
let label = label.map(|l| l.ident.to_string());
Ok(ExprOrPlace::Expr(bctx.spanned_typed_new(
*header_span,
Expand Down
21 changes: 21 additions & 0 deletions source/rust_verify_test/tests/loops.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,27 @@ test_verify_one_file! {
} => Ok(())
}

test_verify_one_file! {
#[test] while_let_loop verus_code! {
enum MaybeU64 {
Some(u64),
None,
}

fn test1() {
let mut i: u64 = 0;
while let MaybeU64::Some(x) = if i < 1 { MaybeU64::Some(i) } else { MaybeU64::None }
invariant i <= 1
decreases 1 - i
{
assert(x == i);
i = i + 1;
}
assert(i <= 1);
}
} => Ok(())
}

test_verify_one_file! {
#[test] basic_while_fail1 verus_code! {
fn test1() {
Expand Down