Merge branch 'main' into for-loop

dependencies/syn/src/item.rs

@@ -2237,7 +2237,13 @@ pub mod parsing {
     impl Parse for ItemUnion {
         fn parse(input: ParseStream) -> Result<Self> {
             let attrs = input.call(Attribute::parse_outer)?;
+
             let vis = input.parse::<Visibility>()?;
+
+            if input.peek(Token![tracked]) || input.peek(Token![ghost]) {
+                return Err(input.error("a 'union' can only be exec-mode"));
+            }
+
             let union_token = input.parse::<Token![union]>()?;
             let ident = input.parse::<Ident>()?;
             let generics = input.parse::<Generics>()?;

source/builtin/src/lib.rs

@@ -255,6 +255,13 @@ pub fn get_variant_field<Adt, Field>(_a: Adt, _variant: &str, _field: &str) -> F
     unimplemented!();
 }
 
+#[cfg(verus_keep_ghost)]
+#[rustc_diagnostic_item = "verus::builtin::get_union_field"]
+#[verifier::spec]
+pub fn get_union_field<Adt, Field>(_a: Adt, _field: &str) -> Field {
+    unimplemented!();
+}
+
 #[cfg(verus_keep_ghost)]
 #[rustc_diagnostic_item = "verus::builtin::assume_"]
 #[verifier::proof]

source/builtin_macros/src/syntax.rs

@@ -14,15 +14,15 @@ use syn_verus::token::{Brace, Bracket, Paren, Semi};
 use syn_verus::visit_mut::{
     visit_block_mut, visit_expr_loop_mut, visit_expr_mut, visit_expr_while_mut, visit_field_mut,
     visit_impl_item_method_mut, visit_item_const_mut, visit_item_enum_mut, visit_item_fn_mut,
-    visit_item_static_mut, visit_item_struct_mut, visit_local_mut, visit_specification_mut,
-    visit_trait_item_method_mut, VisitMut,
+    visit_item_static_mut, visit_item_struct_mut, visit_item_union_mut, visit_local_mut,
+    visit_specification_mut, visit_trait_item_method_mut, VisitMut,
 };
 use syn_verus::{
     braced, bracketed, parenthesized, parse_macro_input, AttrStyle, Attribute, BareFnArg, BinOp,
     Block, DataMode, Decreases, Ensures, Expr, ExprBinary, ExprCall, ExprLit, ExprLoop, ExprTuple,
     ExprUnary, ExprWhile, Field, FnArgKind, FnMode, Global, Ident, ImplItem, ImplItemMethod,
     Invariant, InvariantEnsures, InvariantNameSet, InvariantNameSetList, Item, ItemConst, ItemEnum,
-    ItemFn, ItemImpl, ItemMod, ItemStatic, ItemStruct, ItemTrait, Lit, Local, ModeSpec,
+    ItemFn, ItemImpl, ItemMod, ItemStatic, ItemStruct, ItemTrait, ItemUnion, Lit, Local, ModeSpec,
     ModeSpecChecked, Pat, Path, PathArguments, PathSegment, Publish, Recommends, Requires,
     ReturnType, Signature, SignatureDecreases, SignatureInvariants, Stmt, Token, TraitItem,
     TraitItemMethod, Type, TypeFnSpec, UnOp, Visibility,
@@ -2638,6 +2638,12 @@ impl VisitMut for Visitor {
         self.filter_attrs(&mut item.attrs);
     }
 
+    fn visit_item_union_mut(&mut self, item: &mut ItemUnion) {
+        item.attrs.push(mk_verus_attr(item.span(), quote! { verus_macro }));
+        visit_item_union_mut(self, item);
+        self.filter_attrs(&mut item.attrs);
+    }
+
     fn visit_item_struct_mut(&mut self, item: &mut ItemStruct) {
         item.attrs.push(mk_verus_attr(item.span(), quote! { verus_macro }));
         visit_item_struct_mut(self, item);

source/pervasive/std_specs/control_flow.rs

@@ -0,0 +1,72 @@
+use crate::prelude::*;
+use core::ops::Try;
+use core::ops::ControlFlow;
+use core::ops::FromResidual;
+use core::convert::Infallible;
+
+verus!{
+
+#[verifier(external_type_specification)]
+#[verifier::accept_recursive_types(B)]
+#[verifier::reject_recursive_types_in_ground_variants(C)]
+pub struct ExControlFlow<B, C>(ControlFlow<B, C>);
+
+#[verifier(external_type_specification)]
+#[verifier(external_body)]
+pub struct ExInfallible(Infallible);
+
+
+#[verifier::external_fn_specification]
+pub fn ex_result_branch<T, E>(result: Result<T, E>) -> (cf: ControlFlow<<Result<T, E> as Try>::Residual, <Result<T, E> as Try>::Output>)
+    ensures
+        cf === match result {
+            Ok(v) => ControlFlow::Continue(v),
+            Err(e) => ControlFlow::Break(Err(e)),
+        },
+{
+    result.branch()
+}
+
+#[verifier::external_fn_specification]
+pub fn ex_option_branch<T>(option: Option<T>) -> (cf: ControlFlow<<Option<T> as Try>::Residual, <Option<T> as Try>::Output>)
+    ensures
+        cf === match option {
+            Some(v) => ControlFlow::Continue(v),
+            None => ControlFlow::Break(None),
+        },
+{
+    option.branch()
+}
+
+#[verifier::external_fn_specification]
+pub fn ex_option_from_residual<T>(option: Option<Infallible>) -> (option2: Option<T>)
+    ensures
+        option.is_none(),
+        option2.is_none(),
+{
+    Option::from_residual(option)
+}
+
+pub spec fn spec_from<S, T>(value: T, ret: S) -> bool;
+
+#[verifier::broadcast_forall]
+#[verifier::external_body]
+pub proof fn spec_from_blanket_identity<T>(t: T, s: T)
+    ensures
+        spec_from::<T, T>(t, s) ==> t == s
+{
+}
+
+#[verifier::external_fn_specification]
+pub fn ex_result_from_residual<T, E, F: From<E>>(result: Result<Infallible, E>)
+      -> (result2: Result<T, F>)
+    ensures
+        match (result, result2) {
+            (Err(e), Err(e2)) => spec_from::<F, E>(e, e2),
+            _ => false,
+        },
+{
+    Result::from_residual(result)
+}
+
+}

source/pervasive/std_specs/core.rs

@@ -59,4 +59,9 @@ pub fn ex_intrinsics_unlikely(b: bool) -> (c: bool)
     core::intrinsics::unlikely(b)
 }
 
+#[verifier::external_type_specification]
+#[verifier::external_body]
+#[verifier::reject_recursive_types_in_ground_variants(V)]
+pub struct ExManuallyDrop<V: ?Sized>(core::mem::ManuallyDrop<V>);
+
 }

source/pervasive/std_specs/mod.rs

@@ -5,6 +5,7 @@ pub mod result;
 pub mod option;
 pub mod atomic;
 pub mod bits;
+pub mod control_flow;
 
 #[cfg(feature = "alloc")]
 pub mod vec;

source/rust_verify/src/config.rs

@@ -114,6 +114,7 @@ pub fn enable_default_features_and_verus_attr(
         "register_tool",
         "tuple_trait",
         "custom_inner_attributes",
+        "try_trait_v2",
     ] {
         rustc_args.push("-Z".to_string());
         rustc_args.push(format!("crate-attr=feature({})", feature));

source/rust_verify/src/fn_call_to_vir.rs

@@ -21,7 +21,7 @@ use air::ast_util::str_ident;
 use rustc_ast::LitKind;
 use rustc_hir::def::Res;
 use rustc_hir::{Expr, ExprKind, Node, QPath};
-use rustc_middle::ty::{GenericArgKind, TyKind};
+use rustc_middle::ty::{GenericArg, GenericArgKind, TyKind};
 use rustc_span::def_id::DefId;
 use rustc_span::source_map::Spanned;
 use rustc_span::Span;
@@ -30,10 +30,10 @@ use vir::ast::{
     ArithOp, AssertQueryMode, AutospecUsage, BinaryOp, BitwiseOp, BuiltinSpecFun, CallTarget,
     ChainedOp, ComputeMode, Constant, ExprX, FieldOpr, FunX, HeaderExpr, HeaderExprX, InequalityOp,
     IntRange, IntegerTypeBoundKind, Mode, ModeCoercion, MultiOp, Quant, Typ, TypX, UnaryOp,
-    UnaryOpr, VarAt, VirErr,
+    UnaryOpr, VarAt, VariantCheck, VirErr,
 };
 use vir::ast_util::{const_int_from_string, typ_to_diagnostic_str, types_equal, undecorate_typ};
-use vir::def::positional_field_ident;
+use vir::def::field_ident_from_rust;
 
 pub(crate) fn fn_call_to_vir<'tcx>(
     bctx: &BodyCtxt<'tcx>,
@@ -96,9 +96,6 @@ pub(crate) fn fn_call_to_vir<'tcx>(
                 ),
             );
         }
-        Some(RustItem::TryTraitBranch) => {
-            return err_span(expr.span, "Verus does not yet support the ? operator");
-        }
         Some(RustItem::Clone) => {
             // Special case `clone` for standard Rc and Arc types
             // (Could also handle it for other types where cloning is the identity
@@ -167,6 +164,8 @@ pub(crate) fn fn_call_to_vir<'tcx>(
     // If the resolution is statically known, we record the resolved function for the
     // to be used by lifetime_generate.
 
+    let node_substs = fix_node_substs(tcx, bctx.types, node_substs, rust_item, &args, expr);
+
     let target_kind = if tcx.trait_of_item(f).is_none() {
         vir::ast::CallTargetKind::Static
     } else {
@@ -740,6 +739,33 @@ fn verus_item_to_vir<'tcx, 'a>(
                         variant: str_ident(&variant_name),
                         field: variant_field.unwrap(),
                         get_variant: true,
+                        check: VariantCheck::None,
+                    }),
+                    adt_arg,
+                ))
+            }
+            ExprItem::GetUnionField => {
+                record_spec_fn_allow_proof_args(bctx, expr);
+                assert!(args.len() == 2);
+                let adt_arg = expr_to_vir(bctx, &args[0], ExprModifier::REGULAR)?;
+                let field_name = get_string_lit_arg(&args[1], &f_name)?;
+
+                let adt_path = check_union_field(
+                    bctx,
+                    expr.span,
+                    args[0],
+                    &field_name,
+                    &bctx.types.expr_ty(expr),
+                )?;
+
+                let field_ident = str_ident(&field_name);
+                mk_expr(ExprX::UnaryOpr(
+                    UnaryOpr::Field(FieldOpr {
+                        datatype: adt_path,
+                        variant: field_ident.clone(),
+                        field: field_ident_from_rust(&field_ident),
+                        get_variant: true,
+                        check: VariantCheck::None,
                     }),
                     adt_arg,
                 ))
@@ -1652,6 +1678,33 @@ fn mk_is_smaller_than<'tcx>(
     return Ok(dec_exp);
 }
 
+pub(crate) fn fix_node_substs<'tcx, 'a>(
+    tcx: rustc_middle::ty::TyCtxt<'tcx>,
+    types: &'tcx rustc_middle::ty::TypeckResults<'tcx>,
+    node_substs: &'tcx rustc_middle::ty::List<rustc_middle::ty::GenericArg<'tcx>>,
+    rust_item: Option<RustItem>,
+    args: &'a [&'tcx Expr<'tcx>],
+    expr: &'a Expr<'tcx>,
+) -> &'tcx rustc_middle::ty::List<rustc_middle::ty::GenericArg<'tcx>> {
+    match rust_item {
+        Some(RustItem::TryTraitBranch) => {
+            // I don't understand why, but in this case, node_substs is empty instead
+            // of having the type argument. Let's fix it here.
+            // `branch` has type `fn branch(self) -> ...`
+            // so we can get the Self argument from the first argument.
+            let generic_arg = GenericArg::from(types.expr_ty_adjusted(&args[0]));
+            tcx.mk_args(&[generic_arg])
+        }
+        Some(RustItem::ResidualTraitFromResidual) => {
+            // `fn from_residual(residual: R) -> Self;`
+            let generic_arg0 = GenericArg::from(types.expr_ty(expr));
+            let generic_arg1 = GenericArg::from(types.expr_ty_adjusted(&args[0]));
+            tcx.mk_args(&[generic_arg0, generic_arg1])
+        }
+        _ => node_substs,
+    }
+}
+
 fn mk_typ_args<'tcx>(
     bctx: &BodyCtxt<'tcx>,
     substs: &rustc_middle::ty::List<rustc_middle::ty::GenericArg<'tcx>>,
@@ -1771,11 +1824,6 @@ fn check_variant_field<'tcx>(
         }
     };
 
-    let variant_opt = adt.variants().iter().find(|v| v.ident(tcx).as_str() == variant_name);
-    let Some(variant) = variant_opt else {
-        return err_span(span, format!("no variant `{variant_name:}` for this datatype"));
-    };
-
     let vir_adt_ty = mid_ty_to_vir(tcx, &bctx.ctxt.verus_items, bctx.fun_id, span, &ty, false)?;
     let adt_path = match &*vir_adt_ty {
         TypX::Datatype(path, _, _) => path.clone(),
@@ -1784,9 +1832,34 @@ fn check_variant_field<'tcx>(
         }
     };
 
+    if adt.is_union() {
+        if field_name_typ.is_some() {
+            // Don't use get_variant_field with unions
+            return err_span(
+                span,
+                format!("this datatype is a union; consider `get_union_field` instead"),
+            );
+        }
+        let variant = adt.non_enum_variant();
+        let field_opt = variant.fields.iter().find(|f| f.ident(tcx).as_str() == variant_name);
+        if field_opt.is_none() {
+            return err_span(span, format!("no field `{variant_name:}` for this union"));
+        }
+
+        return Ok((adt_path, None));
+    }
+
+    // Enum case:
+
+    let variant_opt = adt.variants().iter().find(|v| v.ident(tcx).as_str() == variant_name);
+    let Some(variant) = variant_opt else {
+        return err_span(span, format!("no variant `{variant_name:}` for this datatype"));
+    };
+
     match field_name_typ {
         None => Ok((adt_path, None)),
         Some((field_name, expected_field_typ)) => {
+            // The 'get_variant_field' case
             let field_opt = variant.fields.iter().find(|f| f.ident(tcx).as_str() == field_name);
             let Some(field) = field_opt else {
                 return err_span(span, format!("no field `{field_name:}` for this variant"));
@@ -1807,18 +1880,65 @@ fn check_variant_field<'tcx>(
                 return err_span(span, "field has the wrong type");
             }
 
-            let field_ident = if field_name.as_str().bytes().nth(0).unwrap().is_ascii_digit() {
-                let i = field_name.parse::<usize>().unwrap();
-                positional_field_ident(i)
-            } else {
-                str_ident(&field_name)
-            };
+            let field_ident = field_ident_from_rust(&field_name);
 
             Ok((adt_path, Some(field_ident)))
         }
     }
 }
 
+fn check_union_field<'tcx>(
+    bctx: &BodyCtxt<'tcx>,
+    span: Span,
+    adt_arg: &'tcx Expr<'tcx>,
+    field_name: &String,
+    expected_field_typ: &rustc_middle::ty::Ty<'tcx>,
+) -> Result<vir::ast::Path, VirErr> {
+    let tcx = bctx.ctxt.tcx;
+
+    let ty = bctx.types.expr_ty_adjusted(adt_arg);
+    let ty = match ty.kind() {
+        rustc_middle::ty::TyKind::Ref(_, t, rustc_ast::Mutability::Not) => t,
+        _ => &ty,
+    };
+    let (adt, substs) = match ty.kind() {
+        rustc_middle::ty::TyKind::Adt(adt, substs) => (adt, substs),
+        _ => {
+            return err_span(span, format!("expected type to be datatype"));
+        }
+    };
+
+    if !adt.is_union() {
+        return err_span(span, format!("get_union_field expects a union type"));
+    }
+
+    let variant = adt.non_enum_variant();
+
+    let field_opt = variant.fields.iter().find(|f| f.ident(tcx).as_str() == field_name);
+    let Some(field) = field_opt else {
+        return err_span(span, format!("no field `{field_name:}` for this union"));
+    };
+
+    let field_ty = field.ty(tcx, substs);
+    let vir_field_ty =
+        mid_ty_to_vir(tcx, &bctx.ctxt.verus_items, bctx.fun_id, span, &field_ty, false)?;
+    let vir_expected_field_ty =
+        mid_ty_to_vir(tcx, &bctx.ctxt.verus_items, bctx.fun_id, span, &expected_field_typ, false)?;
+    if !types_equal(&vir_field_ty, &vir_expected_field_ty) {
+        return err_span(span, "field has the wrong type");
+    }
+
+    let vir_adt_ty = mid_ty_to_vir(tcx, &bctx.ctxt.verus_items, bctx.fun_id, span, &ty, false)?;
+    let adt_path = match &*vir_adt_ty {
+        TypX::Datatype(path, _, _) => path.clone(),
+        _ => {
+            return err_span(span, format!("expected type to be datatype"));
+        }
+    };
+
+    Ok(adt_path)
+}
+
 fn record_compilable_operator<'tcx>(bctx: &BodyCtxt<'tcx>, expr: &Expr, op: CompilableOperator) {
     let resolved_call = ResolvedCall::CompilableOperator(op);
     let mut erasure_info = bctx.ctxt.erasure_info.borrow_mut();