From 3c93b56c05790eeb5b616b5341ba8c5b245a1e06 Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Fri, 1 Nov 2024 16:05:30 -0700 Subject: [PATCH 1/2] Support bool to integer --- source/rust_verify/src/fn_call_to_vir.rs | 8 ++++++++ source/rust_verify/src/rust_to_vir_expr.rs | 6 ++++++ 2 files changed, 14 insertions(+) diff --git a/source/rust_verify/src/fn_call_to_vir.rs b/source/rust_verify/src/fn_call_to_vir.rs index 70e100606..1cdabc98e 100644 --- a/source/rust_verify/src/fn_call_to_vir.rs +++ b/source/rust_verify/src/fn_call_to_vir.rs @@ -1053,6 +1053,14 @@ fn verus_item_to_vir<'tcx, 'a>( let expr_vattrs = bctx.ctxt.get_verifier_attrs(expr_attrs)?; Ok(mk_ty_clip(&to_ty, &source_vir, expr_vattrs.truncate)) } + ((TypX::Bool, _), TypX::Int(_)) => { + let expr_attrs = bctx.ctxt.tcx.hir().attrs(expr.hir_id); + let expr_vattrs = bctx.ctxt.get_verifier_attrs(expr_attrs)?; + let zero = mk_expr(ExprX::Const(vir::ast_util::const_int_from_u128(0)))?; + let one = mk_expr(ExprX::Const(vir::ast_util::const_int_from_u128(1)))?; + let cast_to_integer = mk_expr(ExprX::If(source_vir, one, Some(zero)))?; + Ok(mk_ty_clip(&to_ty, &cast_to_integer, expr_vattrs.truncate)) + } ((_, true), TypX::Int(IntRange::Int)) => { mk_expr(ExprX::Unary(UnaryOp::CastToInteger, source_vir)) } diff --git a/source/rust_verify/src/rust_to_vir_expr.rs b/source/rust_verify/src/rust_to_vir_expr.rs index 992d7e6c0..71820d33b 100644 --- a/source/rust_verify/src/rust_to_vir_expr.rs +++ b/source/rust_verify/src/rust_to_vir_expr.rs @@ -1674,6 +1674,12 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( (TypX::Int(_), TypX::Int(_)) => { Ok(mk_ty_clip(&to_vir_ty, &source_vir, expr_vattrs.truncate)) } + (TypX::Bool, TypX::Int(_)) => { + let zero = mk_expr(ExprX::Const(vir::ast_util::const_int_from_u128(0)))?; + let one = mk_expr(ExprX::Const(vir::ast_util::const_int_from_u128(1)))?; + let cast_to_integer = mk_expr(ExprX::If(source_vir, one, Some(zero)))?; + Ok(mk_ty_clip(&to_vir_ty, &cast_to_integer, expr_vattrs.truncate)) + } _ => { let source_ty = bctx.types.expr_ty_adjusted(source); let to_ty = bctx.types.expr_ty(expr); From 100e7b6bde7712e9d6f4430ee3cc9490534dc785 Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Wed, 13 Nov 2024 16:09:45 -0800 Subject: [PATCH 2/2] Add unit tests --- source/rust_verify_test/tests/integers.rs | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/source/rust_verify_test/tests/integers.rs b/source/rust_verify_test/tests/integers.rs index 6514571bb..31e6f1833 100644 --- a/source/rust_verify_test/tests/integers.rs +++ b/source/rust_verify_test/tests/integers.rs @@ -496,3 +496,13 @@ test_verify_one_file! { } } => Ok(()) } + +test_verify_one_file! { + #[test] test_bool_to_int verus_code! { + fn test1() { + assert(true as usize == 1); + assert(false as usize == 0); + assert(false as int == 0); + } + } => Ok(()) +}