diff --git a/source/rust_verify/src/automatic_derive.rs b/source/rust_verify/src/automatic_derive.rs index f843d45d4b..9b077299b0 100644 --- a/source/rust_verify/src/automatic_derive.rs +++ b/source/rust_verify/src/automatic_derive.rs @@ -1,11 +1,17 @@ use crate::context::Context; use crate::verus_items::RustItem; use rustc_hir::HirId; +use rustc_hir::def_id::DefId; +use rustc_middle::ty::TyKind; use rustc_span::Span; use std::sync::Arc; use vir::ast::{ - BinaryOp, Expr, ExprX, FunctionX, Mode, Place, PlaceX, SpannedTyped, VirErr, VirErrAs, + Arm, AutospecUsage, BinaryOp, BodyVisibility, CallTarget, CallTargetAttrs, CallTargetKind, + CrateId, Expr, ExprX, FieldOpr, Fun, Function, FunctionAttrsX, FunctionKind, FunctionX, + GenericBounds, Idents, ImplPaths, ItemKind, Mode, Opaqueness, ParamX, Path, Place, PlaceX, + SpannedTyped, Typ, TypX, UnaryOpr, VarIdent, VirErr, VirErrAs, Visibility, }; +use vir::ast_util::bool_typ; /// Traits with special handling #[derive(Clone, Copy, Debug)] @@ -68,18 +74,19 @@ pub fn modify_derived_item<'tcx>( hir_id: HirId, action: &AutomaticDeriveAction, function: &mut FunctionX, -) -> Result<(), VirErr> { + def_id: DefId, +) -> Result, VirErr> { let AutomaticDeriveAction::Special(special) = action else { - return Ok(()); + return Ok(None); }; match special { SpecialTrait::Clone => { if &*function.name.path.last_segment() == "clone" { - return clone_add_post_condition(ctxt, span, hir_id, function); + return clone_add_post_condition(ctxt, span, hir_id, function, def_id); } } } - Ok(()) + Ok(None) } fn clone_add_post_condition<'tcx>( @@ -87,7 +94,8 @@ fn clone_add_post_condition<'tcx>( span: Span, hir_id: HirId, functionx: &mut FunctionX, -) -> Result<(), VirErr> { + def_id: DefId, +) -> Result, VirErr> { let warn = |msg: &str| { ctxt.diagnostics .borrow_mut() @@ -95,17 +103,12 @@ fn clone_add_post_condition<'tcx>( }; let warn_unexpected = || { warn( - "autoderive Clone impl does not take the form Verus expects; continuing, but without adding a specification for the derived Clone impl", - ) - }; - let warn_unsupported = || { - warn( - "Verus does not (yet) support autoderive Clone impl when the clone is not a copy; continuing, but without adding a specification for the derived Clone impl", + "Internal error processing this auto-derived Clone impl; Verus is not adding a specification to the clone function", ) }; let Some(body) = &functionx.body else { - return Ok(()); + return Ok(None); }; let uses_copy; @@ -119,28 +122,24 @@ fn clone_add_post_condition<'tcx>( self_var = Some(last_expr.clone()); } _ => { - warn_unexpected(); - return Ok(()); + uses_copy = false; + self_var = None; } }, - ExprX::Ctor { .. } => { + _ => { uses_copy = false; self_var = None; } - _ => { - warn_unexpected(); - return Ok(()); - } }, _ => { warn_unexpected(); - return Ok(()); + return Ok(None); } } if functionx.ensure.0.len() != 0 { warn_unexpected(); - return Ok(()); + return Ok(None); } if uses_copy { @@ -159,11 +158,329 @@ fn clone_add_post_condition<'tcx>( let eq_expr = cleanup_span_ids(ctxt, span, hir_id, &eq_expr); functionx.ensure.0 = Arc::new(vec![eq_expr]); + Ok(None) } else { - warn_unsupported(); + // for a struct `S { x: X, y: Y }`, the clone function looks like + // `S { x: self.x.clone(), y: self.y.clone() }`. + // Basically we want the ensures clause to be something like: + // strictly_cloned(self.x, out.x) && strictly_cloned(self.y, out.y) + // However, some of the fields might be private. + // So we factor the ensures clause out into a separate spec function where we can + // configure the body visibility. + // So we end up with: + // + // spec fn helper_clone_fn(self: S, other: S) -> bool { + // strictly_cloned(self.x, out.x) && strictly_cloned(self.y, out.y) + // } + // + // impl Clone for S { + // fn clone(&self) -> (out: self) + // ensures helper_clone_fn(self, out) + // { ... } + // } + // + // For enums, it's similar, but there's a match statement to handle. + + let ExprX::Block(_, Some(expr)) = &body.x else { unreachable!() }; + let module_path = functionx.name.path.pop_segment().pop_segment(); + let spec_fn_name = vir::def::clone_spec_fn_name(&functionx.name.path.pop_segment()); + let other_ident = vir::ast_util::air_unique_var(vir::def::OTHER_PARAM_VALUE); + let other_var = SpannedTyped::new( + &expr.span, + &functionx.params[0].x.typ, + ExprX::Var(other_ident.clone()), + ); + let rel = match to_relation(expr, &other_var) { + Ok(rel) => rel, + Err(()) => { + warn_unexpected(); + return Ok(None); + } + }; + let rel = cleanup_span_ids(ctxt, span, hir_id, &rel); + let (datatype_visibility, datatype_body_visibility) = + get_visibilities(&expr.span, ctxt, def_id)?; + let function = mk_spec_function( + &expr.span, + spec_fn_name, + datatype_visibility.clone(), + datatype_body_visibility, + &module_path, + &functionx.typ_params, + &functionx.typ_bounds, + &functionx.params[0].x.typ, + &functionx.params[0].x.name, + &other_ident, + &rel, + ); + + let typ_args: Vec<_> = functionx + .typ_params + .iter() + .map(|param| Arc::new(TypX::TypParam(param.clone()))) + .collect(); + let ct = CallTarget::Fun( + CallTargetKind::Static, + function.x.name.clone(), + Arc::new(typ_args), + Arc::new(vec![]), + CallTargetAttrs { + autospec: AutospecUsage::Final, + const_var: false, + assume_external_allowed: false, + }, + ); + let self_var = SpannedTyped::new( + &expr.span, + &functionx.params[0].x.typ, + ExprX::Var(functionx.params[0].x.name.clone()), + ); + let ret_var = SpannedTyped::new( + &expr.span, + &functionx.ret.x.typ, + ExprX::Var(functionx.ret.x.name.clone()), + ); + let args = Arc::new(vec![self_var, ret_var]); + let ens_expr = SpannedTyped::new(&expr.span, &bool_typ(), ExprX::Call(ct, args, None)); + + let ens_expr = cleanup_span_ids(ctxt, span, hir_id, &ens_expr); + functionx.ensure.0 = Arc::new(vec![ens_expr]); + // TODO: Right now trait functions are always public, but the datatype might be private, + // so it's impossible to make this well-formed. So we fix the visibility here, but really, + // this should be fixed for all trait functions. + functionx.visibility = datatype_visibility; + Ok(Some(function)) + } +} + +fn to_relation(expr: &Expr, output: &Expr) -> Result { + match &expr.x { + ExprX::Match(scrutinee, arms) => { + let mut new_arms: Vec = vec![]; + for mut arm in arms.iter().cloned() { + let armx = Arc::make_mut(&mut arm); + armx.x.body = to_relation(&armx.x.body, output)?; + new_arms.push(arm); + } + Ok(SpannedTyped::new( + &expr.span, + &expr.typ, + ExprX::Match(scrutinee.clone(), Arc::new(new_arms)), + )) + } + ExprX::Ctor(dt, variant_ident, binders, None) => { + let mut conjuncts = vec![SpannedTyped::new( + &expr.span, + &bool_typ(), + ExprX::UnaryOpr( + UnaryOpr::IsVariant { datatype: dt.clone(), variant: variant_ident.clone() }, + output.clone(), + ), + )]; + for binder in binders.iter() { + let field_of_output = SpannedTyped::new( + &expr.span, + &binder.a.typ, + ExprX::UnaryOpr( + UnaryOpr::Field(FieldOpr { + datatype: dt.clone(), + variant: variant_ident.clone(), + field: binder.name.clone(), + get_variant: true, + check: vir::ast::VariantCheck::None, + }), + output.clone(), + ), + ); + let (clonee, impl_paths, clone_typ_arg) = match &binder.a.x { + ExprX::Call( + CallTarget::Fun( + CallTargetKind::DynamicResolved { .. } | CallTargetKind::Dynamic, + fun, + typs, + impl_paths, + _call_target_attrs, + ), + args, + None, + ) if fun == &vir::fun!(CrateId::Core => "clone", "Clone", "clone") => { + assert!(args.len() == 1); + (args[0].clone(), impl_paths.clone(), typs[0].clone()) + } + _ => { + return Err(()); + } + }; + conjuncts.push(strictly_cloned_call( + &clonee, + &field_of_output, + clone_typ_arg, + impl_paths, + )); + } + Ok(vir::ast_util::conjoin(&expr.span, &conjuncts)) + } + _ => Err(()), } +} + +fn strictly_cloned_call(e1: &Expr, e2: &Expr, typ: Typ, impl_paths: ImplPaths) -> Expr { + let fun = vir::fun!(CrateId::Vstd => "pervasive", "strictly_cloned"); + let ct = CallTarget::Fun( + CallTargetKind::Static, + fun, + Arc::new(vec![typ]), + impl_paths, + CallTargetAttrs { + autospec: AutospecUsage::Final, + const_var: false, + assume_external_allowed: false, + }, + ); + let args = Arc::new(vec![e1.clone(), e2.clone()]); + SpannedTyped::new(&e1.span, &bool_typ(), ExprX::Call(ct, args, None)) +} - Ok(()) +fn mk_spec_function( + span: &vir::messages::Span, + spec_fn_name: Fun, + datatype_visibility: Visibility, + datatype_body_visibility: Visibility, + module: &Path, + typ_params: &Idents, + typ_bounds: &GenericBounds, + self_typ: &Typ, + self_param_name: &VarIdent, + other_param_name: &VarIdent, + body: &Expr, +) -> Function { + let self_param = vir::def::Spanned::new( + span.clone(), + ParamX { + name: self_param_name.clone(), + typ: self_typ.clone(), + mode: Mode::Spec, + unwrapped_info: None, + user_mut: false, + }, + ); + let other_param = vir::def::Spanned::new( + span.clone(), + ParamX { + name: other_param_name.clone(), + typ: self_typ.clone(), + mode: Mode::Spec, + unwrapped_info: None, + user_mut: false, + }, + ); + let ret_param = vir::def::Spanned::new( + span.clone(), + ParamX { + name: vir::ast_util::air_unique_var(vir::def::RETURN_VALUE), + typ: bool_typ(), + mode: Mode::Spec, + unwrapped_info: None, + user_mut: false, + }, + ); + vir::def::Spanned::new( + span.clone(), + FunctionX { + name: spec_fn_name, + proxy: None, + kind: FunctionKind::Static, + visibility: datatype_visibility, + body_visibility: BodyVisibility::Visibility(datatype_body_visibility.clone()), + opaqueness: Opaqueness::Revealed { visibility: datatype_body_visibility.clone() }, + owning_module: Some(module.clone()), + mode: Mode::Spec, + typ_params: typ_params.clone(), + typ_bounds: typ_bounds.clone(), + params: Arc::new(vec![self_param, other_param]), + ret: ret_param, + ens_has_return: false, + require: Arc::new(vec![]), + ensure: (Arc::new(vec![]), Arc::new(vec![])), + returns: None, + decrease: Arc::new(vec![]), + decrease_when: None, + decrease_by: None, + fndef_axioms: None, + mask_spec: None, + unwind_spec: None, + item_kind: ItemKind::Function, + attrs: Arc::new(FunctionAttrsX { + uses_ghost_blocks: true, + inline: false, + hidden: Arc::new(vec![]), + broadcast_forall: false, + broadcast_forall_only: false, + no_auto_trigger: false, + auto_ext_equal: vir::ast::AutoExtEqual { + assert: false, + assert_by: false, + ensures: false, + invariant: false, + }, + autospec: None, + bit_vector: false, + atomic: false, + integer_ring: false, + is_decrease_by: false, + check_recommends: false, + nonlinear: false, + spinoff_prover: false, + memoize: false, + rlimit: None, + print_zero_args: false, + print_as_method: false, + prophecy_dependent: false, + size_of_broadcast_proof: false, + is_type_invariant_fn: false, + is_external_body: false, + is_unsafe: false, + exec_assume_termination: false, + exec_allows_no_decreases_clause: false, + tracked_swap: false, + tracked_take_option: false, + is_async: false, + }), + body: Some(body.clone()), + extra_dependencies: vec![], + async_ret: None, + }, + ) +} + +/// Given the DefId of the clone impl, returns: +/// (i) visiblity of the datatype +/// (ii) visiblity of the interior of the datatype +fn get_visibilities<'tcx>( + span: &vir::messages::Span, + ctxt: &Context<'tcx>, + def_id: DefId, +) -> Result<(Visibility, Visibility), VirErr> { + let fn_sig = ctxt.tcx.fn_sig(def_id).skip_binder(); + let self_ty = fn_sig.output().skip_binder(); + let adt_def = match self_ty.kind() { + TyKind::Adt(adt_def, _args) => adt_def, + _ => { + return Err(vir::messages::error( + span, + "Verus Internal Error: handling auto-derive Clone, expected TyKind::Adt", + )); + } + }; + let datatype_vis = crate::rust_to_vir_base::mk_visibility(ctxt, adt_def.did()); + let mut inner_vis = datatype_vis.clone(); + for variant_def in adt_def.variants().iter() { + for field_def in variant_def.fields.iter() { + let vis = crate::rust_to_vir_base::mk_visibility_from_vis(ctxt, field_def.vis); + inner_vis = inner_vis.join(&vis); + } + } + Ok((datatype_vis, inner_vis)) } // TODO better place for this diff --git a/source/rust_verify/src/rust_to_vir_func.rs b/source/rust_verify/src/rust_to_vir_func.rs index 41ebedd5f0..c74d06a40c 100644 --- a/source/rust_verify/src/rust_to_vir_func.rs +++ b/source/rust_verify/src/rust_to_vir_func.rs @@ -2107,13 +2107,17 @@ pub(crate) fn check_item_fn<'tcx>( if let Some(action) = autoderive_action { if let Some(body_hir_id) = body_hir_id { - crate::automatic_derive::modify_derived_item( + let new_function = crate::automatic_derive::modify_derived_item( ctxt, sig.span, body_hir_id, action, &mut func, + id, )?; + if let Some(new_function) = new_function { + functions.push(new_function); + } } } diff --git a/source/rust_verify/src/verus_items.rs b/source/rust_verify/src/verus_items.rs index 41ef2041a6..d9d24cff88 100644 --- a/source/rust_verify/src/verus_items.rs +++ b/source/rust_verify/src/verus_items.rs @@ -363,6 +363,7 @@ pub(crate) enum VstdItem { VecIndex, VecIndexMut, SharedReference, + StrictlyCloned, } #[derive(PartialEq, Eq, Debug, Clone, Copy, Hash)] @@ -677,6 +678,7 @@ fn verus_items_map() -> Vec<(&'static str, VerusItem)> { ("verus::vstd::raw_ptr::cast_str_ptr_to_slice_ptr", VerusItem::Vstd(VstdItem::CastStrPtrToSlicePtr, Some(Arc::new("raw_ptr::cast_str_ptr_to_slice_ptr".to_owned())))), ("verus::vstd::raw_ptr::cast_ptr_to_usize", VerusItem::Vstd(VstdItem::CastPtrToUsize, Some(Arc::new("raw_ptr::cast_ptr_to_usize".to_owned())))), ("verus::vstd::raw_ptr::SharedReference", VerusItem::Vstd(VstdItem::SharedReference, Some(Arc::new("raw_ptr::SharedReference".to_owned())))), + ("verus::vstd::pervasive::strictly_cloned", VerusItem::Vstd(VstdItem::StrictlyCloned, Some(Arc::new("pervasive::strictly_cloned".to_owned())))), ("verus::vstd::float::float_cast", VerusItem::Vstd(VstdItem::FloatCast, Some(Arc::new("float::float_cast".to_owned())))), // SeqFn(vir::interpreter::SeqFn::Last ))), diff --git a/source/rust_verify_test/tests/std.rs b/source/rust_verify_test/tests/std.rs index 9a095a8754..76cce92788 100644 --- a/source/rust_verify_test/tests/std.rs +++ b/source/rust_verify_test/tests/std.rs @@ -926,3 +926,124 @@ test_verify_one_file! { } } => Err(err) => assert_fails(err, 7) } + +test_verify_one_file! { + #[test] autoderive_clone_structs_enums verus_code! { + use vstd::prelude::*; + + #[derive(Clone)] + pub struct Single { + } + + fn test1() { + let x = Single { }; + let y = x.clone(); + assert(y == Single { }); + } + + #[derive(Clone)] + pub struct X { + pub a: u64 + } + + fn test2() { + let x = X { a: 20 }; + let y = x.clone(); + assert(y.a == 20); + } + + #[derive(Clone)] + pub struct X2 { + pub x: X, + } + + fn test3() { + let x2 = X2 { x: X { a: 20 } }; + let y = x2.clone(); + assert(y.x.a == 20); + } + + #[derive(Clone)] + pub enum Option { + Some(A), + None, + } + + fn test4() { + let x = Option::::None; + let y = x.clone(); + assert(y == Option::::None); + } + + fn test5() { + let x = Option::Some(X2 { x: X { a: 5 } }); + let y = x.clone(); + assert(y == Option::Some(X2 { x: X { a: 5 } })); + } + + pub trait Tr { + type R: Clone; + } + + #[derive(Clone)] + pub enum ComplexOption { + Some(A::R), + None, + } + + #[derive(Clone)] + pub struct Z; + + impl Tr for Z { + type R = X2; + } + + fn test6() { + let x = ComplexOption::::Some(X2 { x: X { a: 5 } }); + let y = x.clone(); + assert(y == ComplexOption::::Some(X2 { x: X { a: 5 } })); + } + } => Ok(()) +} + +test_verify_one_file! { + #[test] autoderive_clone_with_visibility verus_code! { + #[derive(Clone)] + pub struct X { + pub a: u64 + } + + #[derive(Clone)] + pub struct X2 { + pub x: X, + } + + mod inner_mod { + use vstd::prelude::*; + use super::X2; + use super::X; + + #[derive(Clone)] + pub(crate) struct Foo { + pub j: u64, + x: X2, + } + + fn test_from_inside() { + let foo = Foo { j: 1, x: X2 { x: X { a: 2 } } }; + let foo2 = foo.clone(); + assert(foo2 == Foo { j: 1, x: X2 { x: X { a: 2 } } }); + } + + pub(crate) fn new() -> Foo { + Foo { j: 1, x: X2 { x: X { a: 2 } } } + } + } + use inner_mod::Foo; + + fn test_from_outside() { + let foo = inner_mod::new(); + let foo2 = foo.clone(); + } + } => Ok(()) +} diff --git a/source/vir/src/ast.rs b/source/vir/src/ast.rs index ae77d96e95..c3ca6a20b7 100644 --- a/source/vir/src/ast.rs +++ b/source/vir/src/ast.rs @@ -897,7 +897,7 @@ pub enum PatternX { /// Arms of match expressions pub type Arm = Arc>; pub type Arms = Arc>; -#[derive(Debug, Serialize, Deserialize, ToDebugSNode)] +#[derive(Debug, Serialize, Deserialize, ToDebugSNode, Clone)] pub struct ArmX { /// pattern pub pattern: Pattern, diff --git a/source/vir/src/def.rs b/source/vir/src/def.rs index bd56d9d13b..5ef0012b3d 100644 --- a/source/vir/src/def.rs +++ b/source/vir/src/def.rs @@ -120,6 +120,7 @@ pub const SUFFIX_SNAP_WHILE_END: &str = "_while_end"; pub const CLOSURE_RETURN_VALUE_PREFIX: &str = "%closure_return"; pub const AUTOSPEC_FUNC_SUFFIX: &str = "%returns_clause_autospec"; +pub const CLONE_FUNC_SUFFIX: &str = "%clone_clause_autoderived"; pub const FNDEF_TYPE: &str = "fndef"; pub const FNDEF_SINGLETON: &str = "fndef_singleton"; @@ -134,6 +135,7 @@ pub const FUEL_BOOL: &str = "fuel_bool"; pub const FUEL_BOOL_DEFAULT: &str = "fuel_bool_default"; pub const FUEL_DEFAULTS: &str = "fuel_defaults"; pub const RETURN_VALUE: &str = "%return"; +pub const OTHER_PARAM_VALUE: &str = "%other"; pub const DEFAULT_ENSURES: &str = "default_ensures"; pub const U_HI: &str = "uHi"; pub const I_LO: &str = "iLo"; @@ -1301,3 +1303,9 @@ pub fn autospec_return_clause_spec_fn_name(path: &Path) -> Fun { let p = path.pop_segment().push_segment(Arc::new(format!("{}{}", name, AUTOSPEC_FUNC_SUFFIX))); Arc::new(FunX { path: p }) } + +pub fn clone_spec_fn_name(path: &Path) -> Fun { + let name = path.last_segment(); + let p = path.pop_segment().push_segment(Arc::new(format!("{}{}", name, CLONE_FUNC_SUFFIX))); + Arc::new(FunX { path: p }) +} diff --git a/source/vstd/pervasive.rs b/source/vstd/pervasive.rs index 6b0027ba57..0860ac4e93 100644 --- a/source/vstd/pervasive.rs +++ b/source/vstd/pervasive.rs @@ -413,6 +413,7 @@ impl VecAdditionalExecFns for alloc::vec::Vec { /// /// It is usually recommended to use [`cloned`] instead, /// which takes the reflexive closure. +#[rustc_diagnostic_item = "verus::vstd::pervasive::strictly_cloned"] pub open spec fn strictly_cloned(a: T, b: T) -> bool { call_ensures(T::clone, (&a,), b) }