From 10a0453a9e1b55223c3e05659224f9eb90a48075 Mon Sep 17 00:00:00 2001 From: fpoli Date: Sat, 15 Oct 2022 07:08:32 +0000 Subject: [PATCH 01/12] Update dependencies (rustc nightly-2022-10-15, viper v4.0.0-RC) --- rust-toolchain | 2 +- viper-toolchain | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/rust-toolchain b/rust-toolchain index 7cc5a01f399..44595b045fb 100644 --- a/rust-toolchain +++ b/rust-toolchain @@ -1,4 +1,4 @@ [toolchain] -channel = "nightly-2022-09-18" +channel = "nightly-2022-10-15" components = [ "rustc-dev", "llvm-tools-preview", "rust-std", "rustfmt", "clippy" ] profile = "minimal" diff --git a/viper-toolchain b/viper-toolchain index 056009df59e..4d0178ce8ef 100644 --- a/viper-toolchain +++ b/viper-toolchain @@ -1 +1 @@ -v-2022-09-02-0742 +v4.0.0-RC From 2204b2c7794ccd7d084b99c5eda0314f04978b0d Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Mon, 17 Oct 2022 14:15:01 +0200 Subject: [PATCH 02/12] Fix new clippy warning --- prusti-utils/src/config.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs index aca64f2a391..54d09d73541 100644 --- a/prusti-utils/src/config.rs +++ b/prusti-utils/src/config.rs @@ -223,8 +223,7 @@ fn get_keys(settings: &Config) -> HashSet { .clone() .into_table() .unwrap() - .into_iter() - .map(|(key, _)| key) + .into_keys() .collect() } From edb4539d090a50a19004ce3ae991e1035fa84e79 Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Mon, 17 Oct 2022 15:41:21 +0200 Subject: [PATCH 03/12] Adapt to changes in rustc --- .../domains/definitely_accessible/state.rs | 1 + analysis/src/mir_utils.rs | 29 +++--- prusti-interface/src/environment/body.rs | 2 +- .../src/environment/borrowck/regions.rs | 7 +- prusti-interface/src/environment/query.rs | 94 ++++++++++-------- .../src/environment/traits/rustc_codegen.rs | 99 +++++++++---------- .../src/environment/traits/rustc_instance.rs | 26 +++-- .../src/specs/checker/predicate_checks.rs | 2 +- .../src/specs/checker/type_model_checks.rs | 2 +- prusti-interface/src/specs/external.rs | 2 +- prusti-viper/src/encoder/encoder.rs | 8 +- .../encoder/elaborate_drops/mir_dataflow.rs | 3 +- .../src/encoder/mir/pure/interpreter/mod.rs | 3 +- .../mir/pure/pure_functions/interpreter.rs | 2 +- .../encoder/mir/specifications/constraints.rs | 2 +- prusti-viper/src/encoder/mir_encoder/mod.rs | 13 ++- prusti-viper/src/encoder/procedure_encoder.rs | 7 +- 17 files changed, 169 insertions(+), 133 deletions(-) diff --git a/analysis/src/domains/definitely_accessible/state.rs b/analysis/src/domains/definitely_accessible/state.rs index 3bb135d5d44..e37af7eaf1f 100644 --- a/analysis/src/domains/definitely_accessible/state.rs +++ b/analysis/src/domains/definitely_accessible/state.rs @@ -227,6 +227,7 @@ fn pretty_print_place<'tcx>( } mir::ProjectionElem::Index(..) | mir::ProjectionElem::ConstantIndex { .. } + | mir::ProjectionElem::OpaqueCast(..) | mir::ProjectionElem::Subslice { .. } => { // It's not possible to move-out or borrow an individual element. unreachable!() diff --git a/analysis/src/mir_utils.rs b/analysis/src/mir_utils.rs index 961a872c62a..91834dba83a 100644 --- a/analysis/src/mir_utils.rs +++ b/analysis/src/mir_utils.rs @@ -220,7 +220,8 @@ pub fn expand_one_level<'tcx>( | mir::ProjectionElem::Index(..) | mir::ProjectionElem::ConstantIndex { .. } | mir::ProjectionElem::Subslice { .. } - | mir::ProjectionElem::Downcast(..) => vec![], + | mir::ProjectionElem::Downcast(..) + | mir::ProjectionElem::OpaqueCast(..) => vec![], }; (new_current_place, other_places) } @@ -326,21 +327,23 @@ pub fn is_copy<'tcx>( // `type_implements_trait` doesn't consider that. matches!(mutability, mir::Mutability::Not) } else if let Some(copy_trait) = tcx.lang_items().copy_trait() { - tcx.infer_ctxt().enter(|infcx| { - // If `ty` has any inference variables (e.g. a region variable), then using it with - // the freshly-created `InferCtxt` (i.e. `tcx.infer_ctxt().enter(..)`) will cause - // a panic, since those inference variables don't exist in the new `InferCtxt`. - // See: https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp/topic/.E2.9C.94.20Panic.20in.20is_copy_modulo_regions - let fresh_ty = infcx.freshen(ty); - infcx - .type_implements_trait(copy_trait, fresh_ty, ty::List::empty(), param_env) - .must_apply_considering_regions() - }) + let infcx = tcx.infer_ctxt().build(); + // If `ty` has any inference variables (e.g. a region variable), then using it with + // the freshly-created `InferCtxt` (i.e. `tcx.infer_ctxt().enter(..)`) will cause + // a panic, since those inference variables don't exist in the new `InferCtxt`. + // See: https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp/topic/.E2.9C.94.20Panic.20in.20is_copy_modulo_regions + let fresh_ty = infcx.freshen(ty); + infcx + .type_implements_trait(copy_trait, fresh_ty, ty::List::empty(), param_env) + .must_apply_considering_regions() } else { false } } +/// Given an assignment `let _ = & `, this function returns the place that is +/// blocked by the loan. +/// For example, `let _ = &x.f.g` blocks just `x.f.g`, but `let _ = &x.f[0].g` blocks `x.f`. pub fn get_blocked_place<'tcx>(tcx: TyCtxt<'tcx>, borrowed: Place<'tcx>) -> Place<'tcx> { for (place_ref, place_elem) in borrowed.iter_projections() { match place_elem { @@ -354,7 +357,9 @@ pub fn get_blocked_place<'tcx>(tcx: TyCtxt<'tcx>, borrowed: Place<'tcx>) -> Plac }) .into(); } - mir::ProjectionElem::Field(..) | mir::ProjectionElem::Downcast(..) => { + mir::ProjectionElem::Field(..) + | mir::ProjectionElem::Downcast(..) + | mir::ProjectionElem::OpaqueCast(..) => { // Continue } } diff --git a/prusti-interface/src/environment/body.rs b/prusti-interface/src/environment/body.rs index acda3bb5915..d28fd778f9f 100644 --- a/prusti-interface/src/environment/body.rs +++ b/prusti-interface/src/environment/body.rs @@ -6,7 +6,7 @@ use prusti_rustc_interface::{ mir, ty::{ self, - subst::{Subst, SubstsRef}, + subst::SubstsRef, TyCtxt, }, }, diff --git a/prusti-interface/src/environment/borrowck/regions.rs b/prusti-interface/src/environment/borrowck/regions.rs index a0775128700..ac3f309bf95 100644 --- a/prusti-interface/src/environment/borrowck/regions.rs +++ b/prusti-interface/src/environment/borrowck/regions.rs @@ -67,11 +67,16 @@ impl PlaceRegions { not supported" .to_string(), )), - mir::ProjectionElem::Downcast(_, _) => Err(PlaceRegionsError::Unsupported( + mir::ProjectionElem::Downcast(..) => Err(PlaceRegionsError::Unsupported( "determining the region of a downcast is \ not supported" .to_string(), )), + mir::ProjectionElem::OpaqueCast(..) => Err(PlaceRegionsError::Unsupported( + "determining the region of an opaque cast is \ + not supported" + .to_string(), + )), }) .collect::>()?; Ok((place.local, indices)) diff --git a/prusti-interface/src/environment/query.rs b/prusti-interface/src/environment/query.rs index c2a613ed0d0..c98a0589ede 100644 --- a/prusti-interface/src/environment/query.rs +++ b/prusti-interface/src/environment/query.rs @@ -7,7 +7,7 @@ use prusti_rustc_interface::{ hir::map::Map, ty::{ self, - subst::{Subst, SubstsRef}, + subst::SubstsRef, Binder, BoundConstness, ImplPolarity, ParamEnv, TraitPredicate, TraitRef, TyCtxt, }, }, @@ -18,7 +18,10 @@ use prusti_rustc_interface::{ }, trait_selection::{ infer::{InferCtxtExt, TyCtxtInferExt}, - traits::{ImplSource, Obligation, ObligationCause, SelectionContext}, + traits::{ + ImplSource, Obligation, ObligationCause, SelectionContext, + query::evaluate_obligation::InferCtxtExt as QueryInferCtxtExt, + }, }, }; use sealed::{IntoParam, IntoParamTcx}; @@ -270,23 +273,22 @@ impl<'tcx> EnvQuery<'tcx> { let proc_def_id = proc_def_id.into_param(); if let Some(trait_id) = self.get_trait_of_item(proc_def_id) { debug!("Fetching implementations of method '{:?}' defined in trait '{}' with substs '{:?}'", proc_def_id, self.tcx.def_path_str(trait_id), substs); - let result = self.tcx.infer_ctxt().enter(|infcx| { - let mut sc = SelectionContext::new(&infcx); - let obligation = Obligation::new( - ObligationCause::dummy(), - // TODO(tymap): don't use reveal_all - ParamEnv::reveal_all(), - Binder::dummy(TraitPredicate { - trait_ref: TraitRef { - def_id: trait_id, - substs, - }, - constness: BoundConstness::NotConst, - polarity: ImplPolarity::Positive, - }), - ); - sc.select(&obligation) - }); + let infcx = self.tcx.infer_ctxt().build(); + let mut sc = SelectionContext::new(&infcx); + let obligation = Obligation::new( + ObligationCause::dummy(), + // TODO(tymap): don't use reveal_all + ParamEnv::reveal_all(), + Binder::dummy(TraitPredicate { + trait_ref: TraitRef { + def_id: trait_id, + substs, + }, + constness: BoundConstness::NotConst, + polarity: ImplPolarity::Positive, + }), + ); + let result = sc.select(&obligation); match result { Ok(Some(ImplSource::UserDefined(data))) => { for item in self @@ -384,21 +386,20 @@ impl<'tcx> EnvQuery<'tcx> { param_env: impl IntoParamTcx<'tcx, ParamEnv<'tcx>>, ) -> bool { assert!(self.tcx.is_trait(trait_def_id)); - self.tcx.infer_ctxt().enter(|infcx| { - // If `ty` has any inference variables (e.g. a region variable), then using it with - // the freshly-created `InferCtxt` (i.e. `tcx.infer_ctxt().enter(..)`) will cause - // a panic, since those inference variables don't exist in the new `InferCtxt`. - // See: https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp/topic/.E2.9C.94.20Panic.20in.20is_copy_modulo_regions - let fresh_ty = infcx.freshen(ty); - infcx - .type_implements_trait( - trait_def_id, - fresh_ty, - trait_substs, - param_env.into_param(self.tcx), - ) - .must_apply_considering_regions() - }) + let infcx = self.tcx.infer_ctxt().build(); + // If `ty` has any inference variables (e.g. a region variable), then using it with + // the freshly-created `InferCtxt` (i.e. `tcx.infer_ctxt().enter(..)`) will cause + // a panic, since those inference variables don't exist in the new `InferCtxt`. + // See: https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp/topic/.E2.9C.94.20Panic.20in.20is_copy_modulo_regions + let fresh_ty = infcx.freshen(ty); + infcx + .type_implements_trait( + trait_def_id, + fresh_ty, + trait_substs, + param_env.into_param(self.tcx), + ) + .must_apply_considering_regions() } /// Return the default substitutions for a particular item, i.e. where each @@ -419,7 +420,6 @@ impl<'tcx> EnvQuery<'tcx> { param_env: impl IntoParamTcx<'tcx, ParamEnv<'tcx>>, ) -> bool { debug!("Evaluating predicate {:?}", predicate); - use prusti_rustc_interface::trait_selection::traits::query::evaluate_obligation::InferCtxtExt; let obligation = Obligation::new( ObligationCause::dummy(), @@ -427,9 +427,7 @@ impl<'tcx> EnvQuery<'tcx> { predicate, ); - self.tcx - .infer_ctxt() - .enter(|infcx| infcx.predicate_must_hold_considering_regions(&obligation)) + self.tcx.infer_ctxt().build().predicate_must_hold_considering_regions(&obligation) } /// Normalizes associated types in foldable types, @@ -466,7 +464,7 @@ impl<'tcx> EnvQuery<'tcx> { mod sealed { use prusti_rustc_interface::{ - hir::hir_id::HirId, + hir::hir_id::{HirId, OwnerId}, middle::ty::{ParamEnv, TyCtxt}, span::def_id::{DefId, LocalDefId}, }; @@ -492,6 +490,18 @@ mod sealed { self.to_def_id() } } + impl IntoParam for OwnerId { + #[inline(always)] + fn into_param(self) -> DefId { + self.to_def_id() + } + } + impl IntoParam for OwnerId { + #[inline(always)] + fn into_param(self) -> LocalDefId { + self.def_id + } + } pub trait IntoParamTcx<'tcx, P> { fn into_param(self, tcx: TyCtxt<'tcx>) -> P; @@ -502,6 +512,12 @@ mod sealed { self.into_param() } } + impl<'tcx> IntoParamTcx<'tcx, HirId> for OwnerId { + #[inline(always)] + fn into_param(self, tcx: TyCtxt<'tcx>) -> HirId { + tcx.hir().local_def_id_to_hir_id(self.def_id) + } + } impl<'tcx> IntoParamTcx<'tcx, HirId> for LocalDefId { #[inline(always)] fn into_param(self, tcx: TyCtxt<'tcx>) -> HirId { diff --git a/prusti-interface/src/environment/traits/rustc_codegen.rs b/prusti-interface/src/environment/traits/rustc_codegen.rs index e217d05f01c..a9a7cd77593 100644 --- a/prusti-interface/src/environment/traits/rustc_codegen.rs +++ b/prusti-interface/src/environment/traits/rustc_codegen.rs @@ -57,62 +57,61 @@ pub(super) fn codegen_fulfill_obligation<'tcx>( // Do the initial selection for the obligation. This yields the // shallow result we are looking for -- that is, what specific impl. - tcx.infer_ctxt().enter(|infcx| { - let mut selcx = SelectionContext::new(&infcx); + let infcx = tcx.infer_ctxt().build(); + let mut selcx = SelectionContext::new(&infcx); - let obligation_cause = ObligationCause::dummy(); - let obligation = Obligation::new( - obligation_cause, - param_env, - trait_ref.to_poly_trait_predicate(), - ); + let obligation_cause = ObligationCause::dummy(); + let obligation = Obligation::new( + obligation_cause, + param_env, + trait_ref.to_poly_trait_predicate(), + ); - let selection = match selcx.select(&obligation) { - Ok(Some(selection)) => selection, - Ok(None) => return Err(CodegenObligationError::Ambiguity), - Err(Unimplemented) => return Err(CodegenObligationError::Unimplemented), - Err(e) => { - panic!( - "Encountered error `{:?}` selecting `{:?}` during codegen", - e, trait_ref - ) - } - }; + let selection = match selcx.select(&obligation) { + Ok(Some(selection)) => selection, + Ok(None) => return Err(CodegenObligationError::Ambiguity), + Err(Unimplemented) => return Err(CodegenObligationError::Unimplemented), + Err(e) => { + panic!( + "Encountered error `{:?}` selecting `{:?}` during codegen", + e, trait_ref + ) + } + }; - debug!("fulfill_obligation: selection={:?}", selection); + debug!("fulfill_obligation: selection={:?}", selection); - // Currently, we use a fulfillment context to completely resolve - // all nested obligations. This is because they can inform the - // inference of the impl's type parameters. - let mut fulfill_cx = FulfillmentContext::new(); - let impl_source = selection.map(|predicate| { - debug!( - "fulfill_obligation: register_predicate_obligation {:?}", - predicate - ); - fulfill_cx.register_predicate_obligation(&infcx, predicate); - }); + // Currently, we use a fulfillment context to completely resolve + // all nested obligations. This is because they can inform the + // inference of the impl's type parameters. + let mut fulfill_cx = FulfillmentContext::new(); + let impl_source = selection.map(|predicate| { + debug!( + "fulfill_obligation: register_predicate_obligation {:?}", + predicate + ); + fulfill_cx.register_predicate_obligation(&infcx, predicate); + }); - // In principle, we only need to do this so long as `impl_source` - // contains unbound type parameters. It could be a slight - // optimization to stop iterating early. - let errors = fulfill_cx.select_all_or_error(&infcx); - if !errors.is_empty() { - return Err(CodegenObligationError::FulfillmentError); - } + // In principle, we only need to do this so long as `impl_source` + // contains unbound type parameters. It could be a slight + // optimization to stop iterating early. + let errors = fulfill_cx.select_all_or_error(&infcx); + if !errors.is_empty() { + return Err(CodegenObligationError::FulfillmentError); + } - let impl_source = infcx.resolve_vars_if_possible(impl_source); - let impl_source = infcx.tcx.erase_regions(impl_source); + let impl_source = infcx.resolve_vars_if_possible(impl_source); + let impl_source = infcx.tcx.erase_regions(impl_source); - // Opaque types may have gotten their hidden types constrained, but we can ignore them safely - // as they will get constrained elsewhere, too. - let _opaque_types = infcx - .inner - .borrow_mut() - .opaque_type_storage - .take_opaque_types(); + // Opaque types may have gotten their hidden types constrained, but we can ignore them safely + // as they will get constrained elsewhere, too. + let _opaque_types = infcx + .inner + .borrow_mut() + .opaque_type_storage + .take_opaque_types(); - debug!("Cache miss: {trait_ref:?} => {impl_source:?}"); - Ok(&*tcx.arena.alloc(impl_source)) - }) + debug!("Cache miss: {trait_ref:?} => {impl_source:?}"); + Ok(&*tcx.arena.alloc(impl_source)) } diff --git a/prusti-interface/src/environment/traits/rustc_instance.rs b/prusti-interface/src/environment/traits/rustc_instance.rs index a9571e6f63b..08d87d7f7e7 100644 --- a/prusti-interface/src/environment/traits/rustc_instance.rs +++ b/prusti-interface/src/environment/traits/rustc_instance.rs @@ -258,18 +258,17 @@ fn resolve_associated_item<'tcx>( ); }); - let substs = tcx.infer_ctxt().enter(|infcx| { - let param_env = param_env.with_reveal_all_normalized(tcx); - let substs = rcvr_substs.rebase_onto(tcx, trait_def_id, impl_data.substs); - let substs = translate_substs( - &infcx, - param_env, - impl_data.impl_def_id, - substs, - leaf_def.defining_node, - ); - infcx.tcx.erase_regions(substs) - }); + let infcx = tcx.infer_ctxt().build(); + let param_env = param_env.with_reveal_all_normalized(tcx); + let substs = rcvr_substs.rebase_onto(tcx, trait_def_id, impl_data.substs); + let substs = translate_substs( + &infcx, + param_env, + impl_data.impl_def_id, + substs, + leaf_def.defining_node, + ); + let substs = infcx.tcx.erase_regions(substs); // Since this is a trait item, we need to see if the item is either a trait default item // or a specialization because we can't resolve those unless we can `Reveal::All`. @@ -403,8 +402,7 @@ fn resolve_associated_item<'tcx>( | traits::ImplSource::DiscriminantKind(..) | traits::ImplSource::Pointee(..) | traits::ImplSource::TraitUpcasting(_) - | traits::ImplSource::ConstDestruct(_) - | traits::ImplSource::Tuple => None, + | traits::ImplSource::ConstDestruct(_) => None, }) } diff --git a/prusti-interface/src/specs/checker/predicate_checks.rs b/prusti-interface/src/specs/checker/predicate_checks.rs index 15f6b72e67b..d37b9d758c8 100644 --- a/prusti-interface/src/specs/checker/predicate_checks.rs +++ b/prusti-interface/src/specs/checker/predicate_checks.rs @@ -159,7 +159,7 @@ impl<'v, 'tcx: 'v> NonSpecExprVisitor<'tcx> for CheckPredicatesVisitor<'tcx> { } fn visit_expr(&mut self, ex: &'tcx hir::Expr<'tcx>) { - let owner_def_id = ex.hir_id.owner; + let owner_def_id = ex.hir_id.owner.def_id; // General check: The "path" of a predicate doesn't appear anywhere // (e.g. as in a function call or an argument when we pass the predicate to another function) diff --git a/prusti-interface/src/specs/checker/type_model_checks.rs b/prusti-interface/src/specs/checker/type_model_checks.rs index a7dd1954559..17e8c4b5cb4 100644 --- a/prusti-interface/src/specs/checker/type_model_checks.rs +++ b/prusti-interface/src/specs/checker/type_model_checks.rs @@ -54,7 +54,7 @@ impl<'tcx> ModelUsageVisitor<'tcx> { let maybe_method_def_id = self .env_query .tcx() - .typeck(expr.hir_id.owner) + .typeck(expr.hir_id.owner.def_id) .type_dependent_def_id(expr.hir_id); if let Some(method_def_id) = maybe_method_def_id { let maybe_local_def_id = method_def_id.as_local(); diff --git a/prusti-interface/src/specs/external.rs b/prusti-interface/src/specs/external.rs index 5592ca71c45..96163ea6855 100644 --- a/prusti-interface/src/specs/external.rs +++ b/prusti-interface/src/specs/external.rs @@ -309,7 +309,7 @@ impl<'tcx> Visitor<'tcx> for ExternSpecVisitor<'tcx> { } if let prusti_rustc_interface::hir::ExprKind::Call(callee_expr, _arguments) = ex.kind { if let prusti_rustc_interface::hir::ExprKind::Path(ref qself) = callee_expr.kind { - let tyck_res = self.env_query.tcx().typeck(callee_expr.hir_id.owner); + let tyck_res = self.env_query.tcx().typeck(callee_expr.hir_id.owner.def_id); let substs = tyck_res.node_substs(callee_expr.hir_id); let res = tyck_res.qpath_res(qself, callee_expr.hir_id); if let prusti_rustc_interface::hir::def::Res::Def(_, def_id) = res { diff --git a/prusti-viper/src/encoder/encoder.rs b/prusti-viper/src/encoder/encoder.rs index d1e3668d6d1..15c33460558 100644 --- a/prusti-viper/src/encoder/encoder.rs +++ b/prusti-viper/src/encoder/encoder.rs @@ -297,7 +297,7 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> { /// Invoke const evaluation to extract scalar value. fn uneval_eval_intlike( &self, - ct: ty::Unevaluated<'tcx>, + ct: mir::UnevaluatedConst<'tcx>, ) -> Option { let tcx = self.env.tcx(); let param_env = tcx.param_env(ct.def.did); @@ -316,8 +316,10 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> { ty::ConstKind::Value(ref const_value) => { const_value.try_to_scalar() } - ty::ConstKind::Unevaluated(ct) => - self.uneval_eval_intlike(ty::Unevaluated { promoted: None, ..ct }), + ty::ConstKind::Unevaluated(ct) => { + let mir_ct = mir::UnevaluatedConst::new(ct.def, ct.substs); + self.uneval_eval_intlike(mir_ct) + }, _ => unimplemented!("{:?}", value), } mir::ConstantKind::Val(val, _) => val.try_to_scalar(), diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs b/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs index a3afe84f7f1..d8913d7c1d1 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder/elaborate_drops/mir_dataflow.rs @@ -837,11 +837,12 @@ where // tmp = &raw mut P; // cur = tmp as *mut T; // end = Offset(cur, len); + let mir_cast_kind = ty::cast::mir_cast_kind(iter_ty, tmp_ty); vec![ self.assign(tmp, Rvalue::AddressOf(Mutability::Mut, self.place)), self.assign( cur, - Rvalue::Cast(CastKind::Misc, Operand::Move(tmp), iter_ty), + Rvalue::Cast(mir_cast_kind, Operand::Move(tmp), iter_ty), ), self.assign( length_or_end, diff --git a/prusti-viper/src/encoder/mir/pure/interpreter/mod.rs b/prusti-viper/src/encoder/mir/pure/interpreter/mod.rs index b8ca98049b0..a726203cf19 100644 --- a/prusti-viper/src/encoder/mir/pure/interpreter/mod.rs +++ b/prusti-viper/src/encoder/mir/pure/interpreter/mod.rs @@ -262,7 +262,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ExpressionBackwardInterpreter<'p, 'v, 'tcx> { // Substitute the place state.substitute_value(&encoded_lhs, encoded_ref); } - mir::Rvalue::Cast(mir::CastKind::Misc, operand, dst_ty) => { + mir::Rvalue::Cast(mir::CastKind::IntToInt, operand, dst_ty) => { let encoded_rhs = self.encoder.encode_cast_expression_high( self.mir, self.caller_def_id, @@ -438,7 +438,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> ExpressionBackwardInterpreter<'p, 'v, 'tcx> { // compose substitutions // TODO(tymap): do we need this? - use prusti_rustc_interface::middle::ty::subst::Subst; let substs = ty::EarlyBinder(*call_substs).subst(self.encoder.env().tcx(), self.substs); let state = if let Some(target_block) = target { diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs index a483d96c96e..b01b8f87fad 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs @@ -1150,7 +1150,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> state.substitute_value(&encoded_lhs, encoded_ref); } - mir::Rvalue::Cast(mir::CastKind::Misc, ref operand, dst_ty) => { + mir::Rvalue::Cast(mir::CastKind::IntToInt, ref operand, dst_ty) => { let encoded_val = self.mir_encoder .encode_cast_expr(operand, *dst_ty, span)?; diff --git a/prusti-viper/src/encoder/mir/specifications/constraints.rs b/prusti-viper/src/encoder/mir/specifications/constraints.rs index 1d45dc28032..95b6327d9c1 100644 --- a/prusti-viper/src/encoder/mir/specifications/constraints.rs +++ b/prusti-viper/src/encoder/mir/specifications/constraints.rs @@ -10,7 +10,7 @@ use prusti_rustc_interface::{ hir::def_id::DefId, middle::{ ty, - ty::subst::{Subst, SubstsRef}, + ty::subst::SubstsRef, }, span::Span, }; diff --git a/prusti-viper/src/encoder/mir_encoder/mod.rs b/prusti-viper/src/encoder/mir_encoder/mod.rs index 6f4aada630f..d1970adf7dc 100644 --- a/prusti-viper/src/encoder/mir_encoder/mod.rs +++ b/prusti-viper/src/encoder/mir_encoder/mod.rs @@ -176,8 +176,8 @@ pub trait PlaceEncoder<'v, 'tcx: 'v> { (encoded_projection, field_ty, None) } - ty::TyKind::Generator(_, _, _) => { - return Err(EncodingError::unsupported("generator fields are not supported yet")); + ty::TyKind::Generator(..) => { + return Err(EncodingError::unsupported("generator fields are not supported")); } x => { @@ -195,7 +195,7 @@ pub trait PlaceEncoder<'v, 'tcx: 'v> { (PlaceEncoding::Expr(e), ty, v) } Err(_) => return Err(EncodingError::unsupported( - "mixed dereferencing and array indexing projections are not supported yet" + "mixed dereferencing and array indexing projections are not supported" )), } } @@ -205,6 +205,11 @@ pub trait PlaceEncoder<'v, 'tcx: 'v> { (encoded_base, base_ty, Some((*variant_index).into())) } + mir::ProjectionElem::OpaqueCast(cast_ty) => { + debug!("Opaque cast projection {:?}", cast_ty); + (encoded_base, *cast_ty, None) + } + mir::ProjectionElem::Index(_) | mir::ProjectionElem::ConstantIndex { .. } => { // FIXME: this avoids some code duplication but the nested @@ -425,7 +430,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> MirEncoder<'p, 'v, 'tcx> { encoded_place .try_into_expr() .map_err(|_| EncodingError::unsupported( - "array indexing is not supported in arbitrary operand positions yet. Try refactoring your code to have only an array access on the right-hand side of assignments using temporary variables".to_string(), + "array indexing is not supported in arbitrary operand positions. Try refactoring your code to have only an array access on the right-hand side of assignments using temporary variables".to_string(), ))?, place_ty, )? diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 69ebee545a6..7700149a268 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -1533,7 +1533,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { } mir::Rvalue::Cast(mir::CastKind::PointerExposeAddress, ref operand, dst_ty) | mir::Rvalue::Cast(mir::CastKind::PointerFromExposedAddress, ref operand, dst_ty) | - mir::Rvalue::Cast(mir::CastKind::Misc, ref operand, dst_ty) => { + mir::Rvalue::Cast(mir::CastKind::IntToInt, ref operand, dst_ty) => { self.encode_cast( operand, dst_ty, @@ -1582,6 +1582,11 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { "raw pointers are not supported" )).with_span(span); } + mir::Rvalue::Cast(cast_kind, _, _) => { + return Err(EncodingError::unsupported( + format!("casts {:?} are not supported", cast_kind) + )).with_span(span); + } mir::Rvalue::AddressOf(_, _) => { return Err(EncodingError::unsupported( "raw addresses of expressions or casting a reference to a raw pointer are not supported" From ea4b3bcac78901547c8b6b9327fd38a1f1911660 Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Mon, 17 Oct 2022 15:42:08 +0200 Subject: [PATCH 04/12] Format code --- prusti-interface/src/environment/body.rs | 6 +----- prusti-interface/src/environment/query.rs | 14 ++++++++------ .../src/encoder/mir/specifications/constraints.rs | 5 +---- 3 files changed, 10 insertions(+), 15 deletions(-) diff --git a/prusti-interface/src/environment/body.rs b/prusti-interface/src/environment/body.rs index d28fd778f9f..8c02460b3a1 100644 --- a/prusti-interface/src/environment/body.rs +++ b/prusti-interface/src/environment/body.rs @@ -4,11 +4,7 @@ use prusti_rustc_interface::{ macros::{TyDecodable, TyEncodable}, middle::{ mir, - ty::{ - self, - subst::SubstsRef, - TyCtxt, - }, + ty::{self, subst::SubstsRef, TyCtxt}, }, span::def_id::{DefId, LocalDefId}, }; diff --git a/prusti-interface/src/environment/query.rs b/prusti-interface/src/environment/query.rs index c98a0589ede..0c7a9eccbf8 100644 --- a/prusti-interface/src/environment/query.rs +++ b/prusti-interface/src/environment/query.rs @@ -6,9 +6,8 @@ use prusti_rustc_interface::{ middle::{ hir::map::Map, ty::{ - self, - subst::SubstsRef, - Binder, BoundConstness, ImplPolarity, ParamEnv, TraitPredicate, TraitRef, TyCtxt, + self, subst::SubstsRef, Binder, BoundConstness, ImplPolarity, ParamEnv, TraitPredicate, + TraitRef, TyCtxt, }, }, span::{ @@ -19,8 +18,8 @@ use prusti_rustc_interface::{ trait_selection::{ infer::{InferCtxtExt, TyCtxtInferExt}, traits::{ - ImplSource, Obligation, ObligationCause, SelectionContext, - query::evaluate_obligation::InferCtxtExt as QueryInferCtxtExt, + query::evaluate_obligation::InferCtxtExt as QueryInferCtxtExt, ImplSource, Obligation, + ObligationCause, SelectionContext, }, }, }; @@ -427,7 +426,10 @@ impl<'tcx> EnvQuery<'tcx> { predicate, ); - self.tcx.infer_ctxt().build().predicate_must_hold_considering_regions(&obligation) + self.tcx + .infer_ctxt() + .build() + .predicate_must_hold_considering_regions(&obligation) } /// Normalizes associated types in foldable types, diff --git a/prusti-viper/src/encoder/mir/specifications/constraints.rs b/prusti-viper/src/encoder/mir/specifications/constraints.rs index 95b6327d9c1..f43ee529e61 100644 --- a/prusti-viper/src/encoder/mir/specifications/constraints.rs +++ b/prusti-viper/src/encoder/mir/specifications/constraints.rs @@ -8,10 +8,7 @@ use prusti_interface::{ use prusti_rustc_interface::{ errors::MultiSpan, hir::def_id::DefId, - middle::{ - ty, - ty::subst::SubstsRef, - }, + middle::{ty, ty::subst::SubstsRef}, span::Span, }; From 5a034be040956e3a4f9b9f2cb4be7fe6cf2b07bf Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Mon, 17 Oct 2022 16:00:47 +0200 Subject: [PATCH 05/12] Update dependencies --- Cargo.lock | 315 +++++++++++++++++++++++++--------------------- prusti/Cargo.toml | 4 +- 2 files changed, 171 insertions(+), 148 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 1d77374b4a3..a3a4cd4a2f9 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -289,15 +289,6 @@ version = "1.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" -[[package]] -name = "block-buffer" -version = "0.9.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4152116fd6e9dadb291ae18fc1ec3575ed6d84c29642d97890f4b4a3417297e4" -dependencies = [ - "generic-array", -] - [[package]] name = "block-buffer" version = "0.10.3" @@ -444,11 +435,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bfd4d1b31faaa3a89d7934dbded3111da0d2ef28e3ebccdb4f0179f5929d1ef1" dependencies = [ "iana-time-zone", - "js-sys", "num-integer", "num-traits", - "time", - "wasm-bindgen", "winapi", ] @@ -497,6 +485,16 @@ dependencies = [ "os_str_bytes", ] +[[package]] +name = "codespan-reporting" +version = "0.11.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3538270d33cc669650c4b093848450d380def10c331d38c768e34cac80576e6e" +dependencies = [ + "termcolor", + "unicode-width", +] + [[package]] name = "color-backtrace" version = "0.5.1" @@ -675,26 +673,24 @@ dependencies = [ [[package]] name = "crossbeam-epoch" -version = "0.9.10" +version = "0.9.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "045ebe27666471bb549370b4b0b3e51b07f56325befa4284db65fc89c02511b1" +checksum = "f916dfc5d356b0ed9dae65f1db9fc9770aa2851d2662b988ccf4fe3516e86348" dependencies = [ "autocfg", "cfg-if", "crossbeam-utils", "memoffset", - "once_cell", "scopeguard", ] [[package]] name = "crossbeam-utils" -version = "0.8.11" +version = "0.8.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "51887d4adc7b564537b15adcfb307936f8075dfcd5f00dde9a9f1d29383682bc" +checksum = "edbafec5fa1f196ca66527c1b12c2ec4745ca14b50f1ad8f9f6f720b55d11fac" dependencies = [ "cfg-if", - "once_cell", ] [[package]] @@ -761,6 +757,50 @@ dependencies = [ "winapi", ] +[[package]] +name = "cxx" +version = "1.0.79" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3f83d0ebf42c6eafb8d7c52f7e5f2d3003b89c7aa4fd2b79229209459a849af8" +dependencies = [ + "cc", + "cxxbridge-flags", + "cxxbridge-macro", + "link-cplusplus", +] + +[[package]] +name = "cxx-build" +version = "1.0.79" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "07d050484b55975889284352b0ffc2ecbda25c0c55978017c132b29ba0818a86" +dependencies = [ + "cc", + "codespan-reporting", + "once_cell", + "proc-macro2", + "quote", + "scratch", + "syn", +] + +[[package]] +name = "cxxbridge-flags" +version = "1.0.79" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "99d2199b00553eda8012dfec8d3b1c75fce747cf27c169a270b3b99e3448ab78" + +[[package]] +name = "cxxbridge-macro" +version = "1.0.79" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dcb67a6de1f602736dd7eaead0080cf3435df806c61b24b13328db128c58868f" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "datafrog" version = "2.0.1" @@ -806,22 +846,13 @@ dependencies = [ "nu-ansi-term", ] -[[package]] -name = "digest" -version = "0.9.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d3dd60d1080a57a05ab032377049e0591415d2b31afd7028356dbf3cc6dcb066" -dependencies = [ - "generic-array", -] - [[package]] name = "digest" version = "0.10.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "adfbc57365a37acbd2ebf2b64d7e69bb766e2fea813521ed536f5d0520dcf86c" dependencies = [ - "block-buffer 0.10.3", + "block-buffer", "crypto-common", ] @@ -854,9 +885,9 @@ checksum = "0688c2a7f92e427f44895cd63841bff7b29f8d7a1648b9e7e07a4a365b2e1257" [[package]] name = "dunce" -version = "1.0.2" +version = "1.0.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "453440c271cf5577fd2a40e4942540cb7d0d2f85e27c8d07dd0023c925a67541" +checksum = "0bd4b30a6560bbd9b4620f4de34c3f14f60848e58a9b7216801afcb4c7b31c3c" [[package]] name = "either" @@ -1136,7 +1167,7 @@ checksum = "4eb1a864a501629691edf6c15a593b7a51eebaa1e8468e9ddc623de7c9b58ec6" dependencies = [ "cfg-if", "libc", - "wasi 0.11.0+wasi-snapshot-preview1", + "wasi", ] [[package]] @@ -1193,7 +1224,7 @@ dependencies = [ "indexmap", "slab", "tokio", - "tokio-util 0.7.4", + "tokio-util", "tracing", ] @@ -1266,7 +1297,7 @@ checksum = "75f43d41e26995c17e71ee126451dd3941010b0514a81a9d11f3b341debc2399" dependencies = [ "bytes", "fnv", - "itoa 1.0.3", + "itoa 1.0.4", ] [[package]] @@ -1313,7 +1344,7 @@ dependencies = [ "http-body", "httparse", "httpdate", - "itoa 1.0.3", + "itoa 1.0.4", "pin-project-lite", "socket2", "tokio", @@ -1337,18 +1368,28 @@ dependencies = [ [[package]] name = "iana-time-zone" -version = "0.1.48" +version = "0.1.51" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "237a0714f28b1ee39ccec0770ccb544eb02c9ef2c82bb096230eefcffa6468b0" +checksum = "f5a6ef98976b22b3b7f2f3a806f858cb862044cfa66805aa3ad84cb3d3b785ed" dependencies = [ "android_system_properties", "core-foundation-sys", + "iana-time-zone-haiku", "js-sys", - "once_cell", "wasm-bindgen", "winapi", ] +[[package]] +name = "iana-time-zone-haiku" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0703ae284fc167426161c2e3f1da3ea71d94b21bedbcc9494e92b28e334e3dca" +dependencies = [ + "cxx", + "cxx-build", +] + [[package]] name = "idna" version = "0.3.0" @@ -1395,9 +1436,9 @@ checksum = "879d54834c8c76457ef4293a689b2a8c59b076067ad77b15efafbb05f92a592b" [[package]] name = "itertools" -version = "0.10.4" +version = "0.10.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d8bf247779e67a9082a4790b45e71ac7cfd1321331a5c856a74a9faebdab78d0" +checksum = "b0fd2260e829bddf4cb6ea802289de2f86d6a7a690192fbe91b3f46e0f2c8473" dependencies = [ "either", ] @@ -1410,9 +1451,9 @@ checksum = "b71991ff56294aa922b450139ee08b3bfc70982c6b2c7562771375cf73542dd4" [[package]] name = "itoa" -version = "1.0.3" +version = "1.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6c8af84674fe1f223a982c933a0ee1086ac4d4052aa0fb8060c12c6ad838e754" +checksum = "4217ad341ebadf8d8e724e264f13e593e0648f5b3e94b3896a5df283be015ecc" [[package]] name = "jni" @@ -1445,9 +1486,9 @@ checksum = "8eaf4bc02d17cbdd7ff4c7438cafcdf7fb9a4613313ad11b4f8fefe7d3fa0130" [[package]] name = "jobserver" -version = "0.1.24" +version = "0.1.25" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "af25a77299a7f711a01975c35a6a424eb6862092cc2d6c72c4ed6cbc56dfc1fa" +checksum = "068b1ee6743e4d11fb9c6a1e6064b3693a1b600e7f5f5988047d98b3dc9fb90b" dependencies = [ "libc", ] @@ -1498,9 +1539,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" [[package]] name = "libc" -version = "0.2.133" +version = "0.2.135" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c0f80d65747a3e43d1596c7c5492d95d5edddaabd45a7fcdb02b95f644164966" +checksum = "68783febc7782c6c5cb401fbda4de5a9898be1762314da0bb2c10ced61f18b0c" [[package]] name = "libgit2-sys" @@ -1542,6 +1583,15 @@ dependencies = [ "vcpkg", ] +[[package]] +name = "link-cplusplus" +version = "1.0.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9272ab7b96c9046fbc5bc56c06c117cb639fe2d509df0c421cad82d2915cf369" +dependencies = [ + "cc", +] + [[package]] name = "linked-hash-map" version = "0.5.6" @@ -1612,7 +1662,7 @@ checksum = "57ee1c23c7c63b0c9250c339ffdc69255f110b298b901b9f6c82547b7b87caaf" dependencies = [ "libc", "log", - "wasi 0.11.0+wasi-snapshot-preview1", + "wasi", "windows-sys", ] @@ -1741,21 +1791,15 @@ dependencies = [ [[package]] name = "once_cell" -version = "1.14.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2f7254b99e31cad77da24b08ebf628882739a608578bb1bcdfc1f9c21260d7c0" - -[[package]] -name = "opaque-debug" -version = "0.3.0" +version = "1.15.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "624a8340c38c1b80fd549087862da4ba43e08858af025b236e509b6649fc13d5" +checksum = "e82dad04139b71a90c080c8463fe0dc7902db5192d939bd0950f074d014339e1" [[package]] name = "openssl" -version = "0.10.41" +version = "0.10.42" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "618febf65336490dfcf20b73f885f5651a0c89c64c2d4a8c3662585a70bf5bd0" +checksum = "12fc0523e3bd51a692c8850d075d74dc062ccf251c0110668cbd921917118a13" dependencies = [ "bitflags", "cfg-if", @@ -1785,9 +1829,9 @@ checksum = "ff011a302c396a5197692431fc1948019154afc178baf7d8e37367442a4601cf" [[package]] name = "openssl-sys" -version = "0.9.75" +version = "0.9.76" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e5f9bd0c2710541a3cda73d6f9ac4f1b240de4ae261065d309dbe73d9dceb42f" +checksum = "5230151e44c0f05157effb743e8d517472843121cf9243e8b81393edb5acd9ce" dependencies = [ "autocfg", "cc", @@ -1838,9 +1882,9 @@ checksum = "478c572c3d73181ff3c2539045f6eb99e5491218eae919370993b890cdbdd98e" [[package]] name = "pest" -version = "2.3.1" +version = "2.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cb779fcf4bb850fbbb0edc96ff6cf34fd90c4b1a112ce042653280d9a7364048" +checksum = "dbc7bc69c062e492337d74d59b120c274fd3d261b6bf6d3207d499b4b379c41a" dependencies = [ "thiserror", "ucd-trie", @@ -1848,9 +1892,9 @@ dependencies = [ [[package]] name = "pest_derive" -version = "2.3.1" +version = "2.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "502b62a6d0245378b04ffe0a7fb4f4419a4815fce813bd8a0ec89a56e07d67b1" +checksum = "60b75706b9642ebcb34dab3bc7750f811609a0eb1dd8b88c2d15bf628c1c65b2" dependencies = [ "pest", "pest_generator", @@ -1858,9 +1902,9 @@ dependencies = [ [[package]] name = "pest_generator" -version = "2.3.1" +version = "2.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "451e629bf49b750254da26132f1a5a9d11fd8a95a3df51d15c4abd1ba154cb6c" +checksum = "f4f9272122f5979a6511a749af9db9bfc810393f63119970d7085fed1c4ea0db" dependencies = [ "pest", "pest_meta", @@ -1871,9 +1915,9 @@ dependencies = [ [[package]] name = "pest_meta" -version = "2.3.1" +version = "2.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bcec162c71c45e269dfc3fc2916eaeb97feab22993a21bcce4721d08cd7801a6" +checksum = "4c8717927f9b79515e565a64fe46c38b8cd0427e64c40680b14a7365ab09ac8d" dependencies = [ "once_cell", "pest", @@ -1964,9 +2008,9 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.43" +version = "1.0.47" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0a2ca2c61bc9f3d74d2886294ab7b9853abd9c1ad903a3ac7815c58989bb7bab" +checksum = "5ea3d908b0e36316caf9e9e2c4625cdde190a7e6f440d794667ed17a1855e725" dependencies = [ "unicode-ident", ] @@ -2272,9 +2316,9 @@ dependencies = [ [[package]] name = "reqwest" -version = "0.11.11" +version = "0.11.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b75aa69a3f06bbcc66ede33af2af253c6f7a86b1ca0033f60c580a27074fbf92" +checksum = "431949c384f4e2ae07605ccaa56d1d9d2ecdb5cadd4f9577ccfab29f2e5149fc" dependencies = [ "base64", "bytes", @@ -2288,10 +2332,10 @@ dependencies = [ "hyper-tls", "ipnet", "js-sys", - "lazy_static", "log", "mime", "native-tls", + "once_cell", "percent-encoding", "pin-project-lite", "serde", @@ -2388,6 +2432,15 @@ dependencies = [ "webpki", ] +[[package]] +name = "rustls-pemfile" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5eebeaeb360c87bfb72e84abdb3447159c0eaececf1bef2aecd65a8be949d1c9" +dependencies = [ + "base64", +] + [[package]] name = "rustversion" version = "1.0.9" @@ -2470,6 +2523,12 @@ version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d29ab0c6d3fc0ee92fe66e2d99f700eab17a8d57d1c1d3b748380fb20baa78cd" +[[package]] +name = "scratch" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9c8132065adcfd6e02db789d9285a0deb2f3fcb04002865ab67d5fb103533898" + [[package]] name = "sct" version = "0.7.0" @@ -2511,18 +2570,18 @@ checksum = "e25dfac463d778e353db5be2449d1cce89bd6fd23c9f1ea21310ce6e5a1b29c4" [[package]] name = "serde" -version = "1.0.144" +version = "1.0.145" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0f747710de3dcd43b88c9168773254e809d8ddbdf9653b84e2554ab219f17860" +checksum = "728eb6351430bccb993660dfffc5a72f91ccc1295abaa8ce19b27ebe4f75568b" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.144" +version = "1.0.145" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "94ed3a816fb1d101812f83e789f888322c34e291f894f19590dc310963e87a00" +checksum = "81fa1584d3d1bcacd84c277a0dfe21f5b0f6accf4a23d04d4c6d61f1af522b4c" dependencies = [ "proc-macro2", "quote", @@ -2531,11 +2590,11 @@ dependencies = [ [[package]] name = "serde_json" -version = "1.0.85" +version = "1.0.86" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e55a28e3aaef9d5ce0506d0a14dbba8054ddc7e499ef522dd8b26859ec9d4a44" +checksum = "41feea4228a6f1cd09ec7a3593a682276702cd67b5273544757dae23c096f074" dependencies = [ - "itoa 1.0.3", + "itoa 1.0.4", "ryu", "serde", ] @@ -2547,22 +2606,20 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d3491c14715ca2294c4d6a88f15e84739788c1d030eed8c110436aafdaa2f3fd" dependencies = [ "form_urlencoded", - "itoa 1.0.3", + "itoa 1.0.4", "ryu", "serde", ] [[package]] name = "sha-1" -version = "0.9.8" +version = "0.10.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "99cd6713db3cf16b6c84e06321e049a9b9f699826e16096d23bbcc44d15d51a6" +checksum = "028f48d513f9678cda28f6e4064755b3fbb2af6acd672f2c209b62323f7aea0f" dependencies = [ - "block-buffer 0.9.0", "cfg-if", "cpufeatures", - "digest 0.9.0", - "opaque-debug", + "digest", ] [[package]] @@ -2573,7 +2630,7 @@ checksum = "f04293dc80c3993519f2d7f6f511707ee7094fe0c6d3406feb330cdb3540eba3" dependencies = [ "cfg-if", "cpufeatures", - "digest 0.10.5", + "digest", ] [[package]] @@ -2677,9 +2734,9 @@ checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623" [[package]] name = "syn" -version = "1.0.100" +version = "1.0.102" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "52205623b1b0f064a4e71182c3b18ae902267282930c6d5462c91b859668426e" +checksum = "3fcd952facd492f9be3ef0d0b7032a6e442ee9b361d4acc2b1d0c4aaa5f613a1" dependencies = [ "proc-macro2", "quote", @@ -2794,35 +2851,24 @@ checksum = "949517c0cf1bf4ee812e2e07e08ab448e3ae0d23472aee8a06c985f0c8815b16" [[package]] name = "thiserror" -version = "1.0.35" +version = "1.0.37" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c53f98874615aea268107765aa1ed8f6116782501d18e53d08b471733bea6c85" +checksum = "10deb33631e3c9018b9baf9dcbbc4f737320d2b576bac10f6aefa048fa407e3e" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.35" +version = "1.0.37" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f8b463991b4eab2d801e724172285ec4195c650e8ec79b149e6c2a8e6dd3f783" +checksum = "982d17546b47146b28f7c22e3d08465f6b8903d0ea13c1660d9d84a6e7adcdbb" dependencies = [ "proc-macro2", "quote", "syn", ] -[[package]] -name = "time" -version = "0.1.44" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6db9e6914ab8b1ae1c260a4ae7a49b6c5611b40328a735b21862567685e73255" -dependencies = [ - "libc", - "wasi 0.10.0+wasi-snapshot-preview1", - "winapi", -] - [[package]] name = "tinyvec" version = "1.6.0" @@ -2840,9 +2886,9 @@ checksum = "cda74da7e1a664f795bb1f8a87ec406fb89a02522cf6e50620d016add6dbbf5c" [[package]] name = "tokio" -version = "1.21.1" +version = "1.21.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0020c875007ad96677dcc890298f4b942882c5d4eb7cc8f439fc3bf813dc9c95" +checksum = "a9e03c497dc955702ba729190dc4aac6f2a0ce97f913e5b1b5912fc5039d9099" dependencies = [ "autocfg", "bytes", @@ -2850,7 +2896,6 @@ dependencies = [ "memchr", "mio", "num_cpus", - "once_cell", "pin-project-lite", "signal-hook-registry", "socket2", @@ -2869,9 +2914,9 @@ dependencies = [ [[package]] name = "tokio-stream" -version = "0.1.10" +version = "0.1.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f6edf2d6bc038a43d31353570e27270603f4648d18f5ed10c0e179abe43255af" +checksum = "d660770404473ccd7bc9f8b28494a811bc18542b915c0855c51e8f419d5223ce" dependencies = [ "futures-core", "pin-project-lite", @@ -2880,31 +2925,16 @@ dependencies = [ [[package]] name = "tokio-tungstenite" -version = "0.15.0" +version = "0.17.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "511de3f85caf1c98983545490c3d09685fa8eb634e57eec22bb4db271f46cbd8" +checksum = "f714dd15bead90401d77e04243611caec13726c2408afd5b31901dfcdcb3b181" dependencies = [ "futures-util", "log", - "pin-project", "tokio", "tungstenite", ] -[[package]] -name = "tokio-util" -version = "0.6.10" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "36943ee01a6d67977dd3f84a5a1d2efeb4ada3a1ae771cadfaa535d9d9fc6507" -dependencies = [ - "bytes", - "futures-core", - "futures-sink", - "log", - "pin-project-lite", - "tokio", -] - [[package]] name = "tokio-util" version = "0.7.4" @@ -2949,9 +2979,9 @@ checksum = "b6bc1c9ce2b5135ac7f93c72918fc37feb872bdc6a5533a8b85eb4b86bfdae52" [[package]] name = "tracing" -version = "0.1.36" +version = "0.1.37" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2fce9567bd60a67d08a16488756721ba392f24f29006402881e43b19aac64307" +checksum = "8ce8c33a8d48bd45d624a6e523445fd21ec13d3653cd51f681abf67418f54eb8" dependencies = [ "cfg-if", "log", @@ -2961,9 +2991,9 @@ dependencies = [ [[package]] name = "tracing-core" -version = "0.1.29" +version = "0.1.30" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5aeea4303076558a00714b823f9ad67d58a3bbda1df83d8827d21193156e22f7" +checksum = "24eb03ba0eab1fd845050058ce5e616558e8f8d8fca633e6b163fe25c797213a" dependencies = [ "once_cell", ] @@ -2976,9 +3006,9 @@ checksum = "59547bce71d9c38b83d9c0e92b6066c4253371f15005def0c30d9657f50c7642" [[package]] name = "tungstenite" -version = "0.14.0" +version = "0.17.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a0b2d8558abd2e276b0a8df5c05a2ec762609344191e5fd23e292c910e9165b5" +checksum = "e27992fd6a8c29ee7eef28fc78349aa244134e10ad447ce3b9f0ac0ed0fa4ce0" dependencies = [ "base64", "byteorder", @@ -3031,9 +3061,9 @@ checksum = "099b7128301d285f79ddd55b9a83d5e6b9e97c92e0ea0daebee7263e932de992" [[package]] name = "unicode-ident" -version = "1.0.4" +version = "1.0.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dcc811dc4066ac62f84f11307873c4850cb653bfa9b1719cee2bd2204a4bc5dd" +checksum = "6ceab39d59e4c9499d4e5a8ee0e2735b891bb7308ac83dfb4e80cad195c9f6f3" [[package]] name = "unicode-normalization" @@ -3098,9 +3128,9 @@ checksum = "09cc8ee72d2a9becf2f2febe0205bbed8fc6615b7cb429ad062dc7b7ddd036a9" [[package]] name = "uuid" -version = "1.1.2" +version = "1.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dd6469f4314d5f1ffec476e05f17cc9a78bc7a27a6a857842170bdf8d6f98d2f" +checksum = "feb41e78f93363bb2df8b0e86a2ca30eed7806ea16ea0c790d757cf93f79be83" dependencies = [ "getrandom", "serde", @@ -3227,9 +3257,9 @@ dependencies = [ [[package]] name = "warp" -version = "0.3.2" +version = "0.3.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3cef4e1e9114a4b7f1ac799f16ce71c14de5778500c5450ec6b7b920c55b587e" +checksum = "ed7b8be92646fc3d18b06147664ebc5f48d222686cb11a8755e561a735aacc6d" dependencies = [ "bytes", "futures-channel", @@ -3243,6 +3273,7 @@ dependencies = [ "multipart", "percent-encoding", "pin-project", + "rustls-pemfile", "scoped-tls", "serde", "serde_json", @@ -3250,17 +3281,11 @@ dependencies = [ "tokio", "tokio-stream", "tokio-tungstenite", - "tokio-util 0.6.10", + "tokio-util", "tower-service", "tracing", ] -[[package]] -name = "wasi" -version = "0.10.0+wasi-snapshot-preview1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1a143597ca7c7793eff794def352d41792a93c481eb1042423ff7ff72ba2c31f" - [[package]] name = "wasi" version = "0.11.0+wasi-snapshot-preview1" @@ -3355,9 +3380,9 @@ dependencies = [ [[package]] name = "webpki-roots" -version = "0.22.4" +version = "0.22.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f1c760f0d366a6c24a02ed7816e23e691f5d92291f94d15e836006fd11b04daf" +checksum = "368bfe657969fb01238bb756d351dcade285e0f6fcbd36dcb23359a5169975be" dependencies = [ "webpki", ] diff --git a/prusti/Cargo.toml b/prusti/Cargo.toml index 94c7dd145ba..a59417f3c1c 100644 --- a/prusti/Cargo.toml +++ b/prusti/Cargo.toml @@ -20,9 +20,7 @@ log = { version = "0.4", features = ["release_max_level_info"] } lazy_static = "1.4.0" [build-dependencies] -# Update to "0.4.20" when available, this fixes the `time` vuln -# (even though `cargo audit` may still report it) -chrono = "0.4" +chrono = { version = "0.4.22", default-features = false, features = ["clock"] } [package.metadata.rust-analyzer] # This crate uses #[feature(rustc_private)] From 24c714867ffbac26a8601f860cd90fbdabafb457 Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Mon, 17 Oct 2022 16:29:24 +0200 Subject: [PATCH 06/12] Fix clippy warnings --- prusti-common/src/vir/to_viper.rs | 2 +- .../src/specs/checker/type_model_checks.rs | 4 ++-- .../counterexample_translation_refactored.rs | 4 ++-- .../src/encoder/high/procedures/inference/state.rs | 4 ++-- .../src/encoder/mir/specifications/constraints.rs | 2 +- vir/defs/low/mod.rs | 2 ++ vir/defs/polymorphic/borrows.rs | 2 +- vir/defs/polymorphic/conversions.rs | 14 +++++++------- vir/src/legacy/borrows.rs | 2 +- vir/src/legacy/conversions.rs | 14 +++++++------- 10 files changed, 26 insertions(+), 24 deletions(-) diff --git a/prusti-common/src/vir/to_viper.rs b/prusti-common/src/vir/to_viper.rs index 2531de393bc..7a151e57401 100644 --- a/prusti-common/src/vir/to_viper.rs +++ b/prusti-common/src/vir/to_viper.rs @@ -1221,7 +1221,7 @@ fn unsigned_max_for_size(size: BitVectorSize) -> u128 { BitVectorSize::BV16 => u16::MAX as u128, BitVectorSize::BV32 => u32::MAX as u128, BitVectorSize::BV64 => u64::MAX as u128, - BitVectorSize::BV128 => u128::MAX as u128, + BitVectorSize::BV128 => u128::MAX, } } diff --git a/prusti-interface/src/specs/checker/type_model_checks.rs b/prusti-interface/src/specs/checker/type_model_checks.rs index 17e8c4b5cb4..33598ddadf5 100644 --- a/prusti-interface/src/specs/checker/type_model_checks.rs +++ b/prusti-interface/src/specs/checker/type_model_checks.rs @@ -101,8 +101,8 @@ impl<'tcx> SpecCheckerStrategy<'tcx> for ModelDefinedOnTypeWithoutFields { // Mark all modelled types as "dangerous", i.e. assume they have no fields let mut modelled_types_has_fields: FxHashMap = collect .modelled_types - .iter() - .map(|(ty_hir_id, _)| (*ty_hir_id, true)) + .keys() + .map(|ty_hir_id| (*ty_hir_id, true)) .collect(); let mut type_names: FxHashMap = FxHashMap::default(); diff --git a/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs b/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs index 695c59ee421..0891db5b538 100644 --- a/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs +++ b/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs @@ -69,8 +69,8 @@ impl<'ce, 'tcx, 'v> CounterexampleTranslator<'ce, 'tcx, 'v> { fn get_label_markers(&self) -> FxHashMap { self.var_mapping .labels_successor_mapping - .iter() - .map(|(label, _)| { + .keys() + .map(|label| { match self .silicon_counterexample .model diff --git a/prusti-viper/src/encoder/high/procedures/inference/state.rs b/prusti-viper/src/encoder/high/procedures/inference/state.rs index 9bfe22b9ce8..f8ed042d829 100644 --- a/prusti-viper/src/encoder/high/procedures/inference/state.rs +++ b/prusti-viper/src/encoder/high/procedures/inference/state.rs @@ -108,7 +108,7 @@ impl<'a> IntoIterator for &'a Places { type IntoIter = Box + 'a>; fn into_iter(self) -> Self::IntoIter { - Box::new(self.places.iter().map(|(_, place)| place)) + Box::new(self.places.values()) } } @@ -118,7 +118,7 @@ impl IntoIterator for Places { type IntoIter = Box>; fn into_iter(self) -> Self::IntoIter { - Box::new(self.places.into_iter().map(|(_, place)| place)) + Box::new(self.places.into_values()) } } diff --git a/prusti-viper/src/encoder/mir/specifications/constraints.rs b/prusti-viper/src/encoder/mir/specifications/constraints.rs index f43ee529e61..d3da4823b5d 100644 --- a/prusti-viper/src/encoder/mir/specifications/constraints.rs +++ b/prusti-viper/src/encoder/mir/specifications/constraints.rs @@ -255,6 +255,6 @@ pub mod trait_bounds { .emit(&env.diagnostic); } - param_envs.into_iter().map(|(k, _)| k).next().unwrap() + param_envs.into_keys().next().unwrap() } } diff --git a/vir/defs/low/mod.rs b/vir/defs/low/mod.rs index 33175df5ec3..2ad1ee231de 100644 --- a/vir/defs/low/mod.rs +++ b/vir/defs/low/mod.rs @@ -1,6 +1,8 @@ //! Monomorphic IR that is very close to Viper and can be directly converted //! into it. +#![allow(clippy::write_with_newline)] + pub mod ast; pub mod cfg; pub mod domain; diff --git a/vir/defs/polymorphic/borrows.rs b/vir/defs/polymorphic/borrows.rs index 893924b5eee..e0396b730c0 100644 --- a/vir/defs/polymorphic/borrows.rs +++ b/vir/defs/polymorphic/borrows.rs @@ -23,7 +23,7 @@ impl From for Borrow { impl From for usize { fn from(borrow: Borrow) -> Self { - borrow.0 as usize + borrow.0 } } diff --git a/vir/defs/polymorphic/conversions.rs b/vir/defs/polymorphic/conversions.rs index a1d39023307..3b426d5bafd 100644 --- a/vir/defs/polymorphic/conversions.rs +++ b/vir/defs/polymorphic/conversions.rs @@ -80,7 +80,7 @@ impl From for Expr { impl From for Const { fn from(val: i8) -> Self { - Const::Int(val as i64) + Const::Int(val.into()) } } @@ -95,7 +95,7 @@ impl From for Expr { impl From for Const { fn from(val: i16) -> Self { - Const::Int(val as i64) + Const::Int(val.into()) } } @@ -110,7 +110,7 @@ impl From for Expr { impl From for Const { fn from(val: i32) -> Self { - Const::Int(val as i64) + Const::Int(val.into()) } } @@ -125,7 +125,7 @@ impl From for Expr { impl From for Const { fn from(val: i64) -> Self { - Const::Int(val as i64) + Const::Int(val) } } @@ -155,7 +155,7 @@ impl From for Expr { impl From for Const { fn from(val: u8) -> Self { - Const::Int(val as i64) + Const::Int(val.into()) } } @@ -170,7 +170,7 @@ impl From for Expr { impl From for Const { fn from(val: u16) -> Self { - Const::Int(val as i64) + Const::Int(val.into()) } } @@ -185,7 +185,7 @@ impl From for Expr { impl From for Const { fn from(val: u32) -> Self { - Const::Int(val as i64) + Const::Int(val.into()) } } diff --git a/vir/src/legacy/borrows.rs b/vir/src/legacy/borrows.rs index 41ffe6b9f5f..797dfff80a6 100644 --- a/vir/src/legacy/borrows.rs +++ b/vir/src/legacy/borrows.rs @@ -25,7 +25,7 @@ impl From for Borrow { impl From for usize { fn from(borrow: Borrow) -> Self { - borrow.0 as usize + borrow.0 } } diff --git a/vir/src/legacy/conversions.rs b/vir/src/legacy/conversions.rs index 7ff16c87a53..b3d46ad7e3f 100644 --- a/vir/src/legacy/conversions.rs +++ b/vir/src/legacy/conversions.rs @@ -62,7 +62,7 @@ impl From for Expr { impl From for Const { fn from(val: i8) -> Self { - Const::Int(val as i64) + Const::Int(val.into()) } } @@ -74,7 +74,7 @@ impl From for Expr { impl From for Const { fn from(val: i16) -> Self { - Const::Int(val as i64) + Const::Int(val.into()) } } @@ -86,7 +86,7 @@ impl From for Expr { impl From for Const { fn from(val: i32) -> Self { - Const::Int(val as i64) + Const::Int(val.into()) } } @@ -98,7 +98,7 @@ impl From for Expr { impl From for Const { fn from(val: i64) -> Self { - Const::Int(val as i64) + Const::Int(val) } } @@ -122,7 +122,7 @@ impl From for Expr { impl From for Const { fn from(val: u8) -> Self { - Const::Int(val as i64) + Const::Int(val.into()) } } @@ -134,7 +134,7 @@ impl From for Expr { impl From for Const { fn from(val: u16) -> Self { - Const::Int(val as i64) + Const::Int(val.into()) } } @@ -146,7 +146,7 @@ impl From for Expr { impl From for Const { fn from(val: u32) -> Self { - Const::Int(val as i64) + Const::Int(val.into()) } } From 271e86297ab145a7318c8fd010cd1acde163a60e Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Mon, 17 Oct 2022 16:37:20 +0200 Subject: [PATCH 07/12] Fix clippy warnings --- prusti-interface/src/environment/mir_body/patch/compiler.rs | 4 ++-- prusti-interface/src/environment/traits/rustc_instance.rs | 4 ++-- prusti-viper/src/encoder/encoder.rs | 2 +- prusti-viper/src/encoder/mir/casts/interface.rs | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/prusti-interface/src/environment/mir_body/patch/compiler.rs b/prusti-interface/src/environment/mir_body/patch/compiler.rs index 44ef984998d..1db472010ca 100644 --- a/prusti-interface/src/environment/mir_body/patch/compiler.rs +++ b/prusti-interface/src/environment/mir_body/patch/compiler.rs @@ -104,14 +104,14 @@ impl<'tcx> MirPatch<'tcx> { let index = self.next_local; self.next_local += 1; self.new_locals.push(LocalDecl::new(ty, span)); - Local::new(index as usize) + Local::new(index) } pub fn new_internal(&mut self, ty: Ty<'tcx>, span: Span) -> Local { let index = self.next_local; self.next_local += 1; self.new_locals.push(LocalDecl::new(ty, span).internal()); - Local::new(index as usize) + Local::new(index) } pub fn new_block(&mut self, data: BasicBlockData<'tcx>) -> BasicBlock { diff --git a/prusti-interface/src/environment/traits/rustc_instance.rs b/prusti-interface/src/environment/traits/rustc_instance.rs index 08d87d7f7e7..664a56299da 100644 --- a/prusti-interface/src/environment/traits/rustc_instance.rs +++ b/prusti-interface/src/environment/traits/rustc_instance.rs @@ -59,14 +59,14 @@ impl<'tcx> BoundVarsCollector<'tcx> { } fn into_vars(self, tcx: TyCtxt<'tcx>) -> &'tcx ty::List { - let max = self.vars.iter().map(|(k, _)| *k).max().unwrap_or(0); + let max = self.vars.keys().copied().max().unwrap_or(0); for i in 0..max { if self.vars.get(&i).is_none() { panic!("Unknown variable: {:?}", i); } } - tcx.mk_bound_variable_kinds(self.vars.into_iter().map(|(_, v)| v)) + tcx.mk_bound_variable_kinds(self.vars.into_values()) } } diff --git a/prusti-viper/src/encoder/encoder.rs b/prusti-viper/src/encoder/encoder.rs index 15c33460558..25bdc2c9029 100644 --- a/prusti-viper/src/encoder/encoder.rs +++ b/prusti-viper/src/encoder/encoder.rs @@ -668,7 +668,7 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> { ty::TyKind::Uint(ty::UintTy::U16) => (value as u16).into(), ty::TyKind::Uint(ty::UintTy::U32) => (value as u32).into(), ty::TyKind::Uint(ty::UintTy::U64) => (value as u64).into(), - ty::TyKind::Uint(ty::UintTy::U128) => (value as u128).into(), + ty::TyKind::Uint(ty::UintTy::U128) => value.into(), ty::TyKind::Uint(ty::UintTy::Usize) => (value as usize).into(), ty::TyKind::Char => value.into(), ref x => unimplemented!("{:?}", x), diff --git a/prusti-viper/src/encoder/mir/casts/interface.rs b/prusti-viper/src/encoder/mir/casts/interface.rs index a06b708b412..e453fb8c19f 100644 --- a/prusti-viper/src/encoder/mir/casts/interface.rs +++ b/prusti-viper/src/encoder/mir/casts/interface.rs @@ -63,7 +63,7 @@ impl<'v, 'tcx: 'v> CastsEncoderInterface<'tcx> for super::super::super::Encoder< number.into() } ty::TyKind::Uint(ty::UintTy::U128) => { - let number = value as u128; + let number = value; number.into() } ty::TyKind::Uint(ty::UintTy::Usize) => { From 99d896cb4505dc15310bf1724183ebb97af8eb7a Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Mon, 17 Oct 2022 17:53:02 +0200 Subject: [PATCH 08/12] Fix test annotation --- .../tests/verify/fail/arrays-slices/complex-array-rhs.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prusti-tests/tests/verify/fail/arrays-slices/complex-array-rhs.rs b/prusti-tests/tests/verify/fail/arrays-slices/complex-array-rhs.rs index 0dc9c25b2c5..94959933d22 100644 --- a/prusti-tests/tests/verify/fail/arrays-slices/complex-array-rhs.rs +++ b/prusti-tests/tests/verify/fail/arrays-slices/complex-array-rhs.rs @@ -1,4 +1,4 @@ fn main() { let mut a = [0; 3]; - a[0] += 1; //~ ERROR array indexing is not supported in arbitrary operand positions yet + a[0] += 1; //~ ERROR array indexing is not supported in arbitrary operand positions } From 3fd43dd6a03301624c493d27e0947e71803f9cf5 Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Tue, 18 Oct 2022 09:26:45 +0200 Subject: [PATCH 09/12] Convert panics to errors --- .../mir/pure/pure_functions/interpreter.rs | 57 ++++++++++++++----- 1 file changed, 43 insertions(+), 14 deletions(-) diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs index b01b8f87fad..be182f33f0a 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs @@ -385,8 +385,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> ExprBackwardInterpreterState::new(final_expr) } - TerminatorKind::DropAndReplace { .. } => unimplemented!(), - TerminatorKind::Call { ref args, destination, @@ -603,14 +601,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> self.caller_def_id, call_substs, ) - .with_span(term.source_info.span)? + .with_span(span)? } else { return Err(SpannedEncodingError::incorrect( format!( "use of impure function {:?} in pure code is not allowed", func_proc_name ), - term.source_info.span, + span, )); }; trace!("Encoding pure function call '{}'", function_name); @@ -695,13 +693,19 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> state } else { // Other kind of calls? - unimplemented!(); + return Err(SpannedEncodingError::internal( + format!("unexpected call kind '{:?}'", term.kind), + span + )); } } TerminatorKind::Call { .. } => { // Other kind of calls? - unimplemented!(); + return Err(SpannedEncodingError::internal( + format!("unexpected call kind '{:?}'", term.kind), + span + )); } TerminatorKind::Assert { @@ -766,10 +770,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> } } - TerminatorKind::Yield { .. } + TerminatorKind::DropAndReplace { .. } + | TerminatorKind::Yield { .. } | TerminatorKind::GeneratorDrop | TerminatorKind::InlineAsm { .. } => { - unimplemented!("{:?}", term.kind) + return Err(SpannedEncodingError::internal( + format!("unimplemented encoding of terminator '{:?}'", term.kind), + span + )); } }; @@ -1008,7 +1016,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> state.substitute_value(&encoded_lhs, snapshot); } - ref x => unimplemented!("{:?}", x), + ref agg => { + return Err(SpannedEncodingError::internal( + format!("unimplemented encoding of RHS aggregate '{:?}'", agg), + span + )); + } } } @@ -1086,8 +1099,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> state.substitute_value(&opt_lhs_value_place.unwrap(), encoded_value); } - mir::Rvalue::NullaryOp(_op, _op_ty) => unimplemented!(), - &mir::Rvalue::Discriminant(src) => { let (encoded_src, src_ty, _) = self.encode_place(src).with_span(span)?; match src_ty.kind() { @@ -1121,7 +1132,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> state.substitute_value(&opt_lhs_value_place.unwrap(), discr_value); } ref x => { - panic!("The discriminant of type {:?} is not defined", x); + return Err(SpannedEncodingError::internal( + format!("the discriminant of type {:?} is not defined", x), + span + )); } } } @@ -1207,6 +1221,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> } } + mir::Rvalue::Cast(unsupported_kind, _, _) => { + return Err(SpannedEncodingError::unsupported( + format!("unsupported cast of kind '{:?}", unsupported_kind), + span, + )); + } + mir::Rvalue::Repeat(ref operand, times) => { let (encoded_operand, _) = self.encode_operand(operand).with_span(span)?; let len: usize = self.encoder.const_eval_intlike(mir::ConstantKind::Ty(*times)).with_span(span)? @@ -1230,12 +1251,20 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> } ref rhs => { - unimplemented!("encoding of '{:?}'", rhs); + return Err(SpannedEncodingError::internal( + format!("unimplemented encoding of RHS '{:?}'", rhs), + span + )); } } } - ref stmt => unimplemented!("encoding of '{:?}'", stmt), + ref stmt => { + return Err(SpannedEncodingError::internal( + format!("unimplemented encoding of statement '{:?}'", stmt), + span + )); + } } self.apply_downcasts(state, location)?; From 086dd34813790fde9f24175a025b30cd0eb645e9 Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Tue, 18 Oct 2022 08:08:18 +0000 Subject: [PATCH 10/12] Add Python 3 to Codespaces --- .devcontainer/devcontainer.json | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index f7688cc5e69..6b3dd2fa508 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -49,9 +49,12 @@ // Comment out to connect as root instead. More info: https://aka.ms/vscode-remote/containers/non-root. "remoteUser": "vscode", + + // See https://containers.dev/features for a list of all available features "features": { "fish": "latest", - "java": "17" + "java": "17", + "python": "latest" }, "updateContentCommand": "python ./x.py" From e2fbc335624093ea521a45157f9a4a2b25e4c3aa Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Tue, 18 Oct 2022 08:08:59 +0000 Subject: [PATCH 11/12] Format code --- .../src/encoder/mir/pure/pure_functions/interpreter.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs index be182f33f0a..daba6077fe5 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs @@ -695,7 +695,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> // Other kind of calls? return Err(SpannedEncodingError::internal( format!("unexpected call kind '{:?}'", term.kind), - span + span, )); } } @@ -704,7 +704,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> // Other kind of calls? return Err(SpannedEncodingError::internal( format!("unexpected call kind '{:?}'", term.kind), - span + span, )); } @@ -776,7 +776,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> | TerminatorKind::InlineAsm { .. } => { return Err(SpannedEncodingError::internal( format!("unimplemented encoding of terminator '{:?}'", term.kind), - span + span, )); } }; From 0d9f2ed3ee417b9c8fd8c1cfba2047bcd71d0b35 Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Tue, 18 Oct 2022 11:38:16 +0200 Subject: [PATCH 12/12] Update test annotation --- prusti-tests/tests/verify_overflow/ui/unsupported_cast.stderr | 2 +- prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/prusti-tests/tests/verify_overflow/ui/unsupported_cast.stderr b/prusti-tests/tests/verify_overflow/ui/unsupported_cast.stderr index 2d30f6242a9..43ff7c5c484 100644 --- a/prusti-tests/tests/verify_overflow/ui/unsupported_cast.stderr +++ b/prusti-tests/tests/verify_overflow/ui/unsupported_cast.stderr @@ -1,4 +1,4 @@ -error: [Prusti: unsupported feature] unsupported cast from type 'f32' to type 'i32' +error: [Prusti: unsupported feature] unsupported cast of kind 'FloatToInt' --> $DIR/unsupported_cast.rs:3:12 | 3 | #[requires(a as f32 as i32 == 0)] diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs index daba6077fe5..1d5ccf9b34b 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs @@ -1223,7 +1223,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> mir::Rvalue::Cast(unsupported_kind, _, _) => { return Err(SpannedEncodingError::unsupported( - format!("unsupported cast of kind '{:?}", unsupported_kind), + format!("unsupported cast of kind '{:?}'", unsupported_kind), span, )); }